[Question][Hw7] (Several Questions) Casting, (ret (type_env f)), fun_of

[sjoon2455]

Hi, I have several questions. I successfully(?) made my way to implement almost everything, but few questions are left in my mind.

1. Casting.
   Llvm question: How could I extract i32from %conv = sext i8 %4 to i32?
   Z3 question: While adding constraints(or assertions) one by one, we could encounter casting instruction. For example in the above case, one should tell Z3 that the type of %4 just changed. But is this possible? I don't think so, because (assert (= c1 c2)) where c1 = (assert (= %4 i8)), c2 = (assert (= %4 i32)) would contradict. Could anyone share idea/hint on this?

2. ret_of, param_of
   Since retrieving callee function's return type or parameter type is necessary, I used these given functions and it seems to be working. But the thing is, despite checking constraint.smt2 and function definition in typesystem.ml, I couldn't understand how it actually get to retrieve return value through (ret (type_env f)), and same for parameter. Could anyone share your knowledge on this?

3. fun_of
   I'm afraid I might not be allowed to ask anything about this but let me try. When do we have to use this function? All after implementation, I am having difficulty understand ing the necessity/usage of the function.

Sorry for too much question. I would appreciate any partial answer!
Thanks in advance (_ _).

[kangwoosukeq]

1. You can use Llvm.type_of to extract the instruction type. Also, this instruction does not change the type of %4. It makes i32 type %conv by casting i8 type %4.

2. You can debug your code using functions like print_endline. In typesystem.ml, all definitions of types and utility functions are defined. ret_of and param_of are just matching functions for the given value.

3. Actually, you don't need to use all functions in typesystem.ml. Use them for your purpose.

[sjoon2455]

@kangwoosukeq Thank you!!!