open Domains;; let binary_operator_type operator_name type1 type2 = match (operator_name, type1, type2) with | ("=", TInt, TInt) -> TBool | ("<", TInt, TInt) -> TBool | ("<=", TInt, TInt) -> TBool | (">", TInt, TInt) -> TBool | (">=", TInt, TInt) -> TBool | ("+", TInt, TInt) -> TInt | ("-", TInt, TInt) -> TInt | ("*", TInt, TInt) -> TInt | ("/", TInt, TInt) -> TInt | ("&&", TBool, TBool) -> TBool | ("||", TBool, TBool) -> TBool | (",", left_type, right_type) -> TPair(left_type, right_type) | _ -> Printf.printf "%s\n" operator_name; failwith "type error in primitive call";; let value_type value = match value with | VInt _ -> TInt | VBool _ -> TBool | VClosure _ | VPair _ -> failwith "impossible to reach";; let rec expression_type expression rho gamma = match expression with | EValue c -> value_type c | EVariable x -> Environment.lookup x (Environment.extend gamma rho) | ELambda(x, x_type, e) -> TFunction(x_type, expression_type e (Environment.bind x x_type rho) gamma) | EApply(e1, e2) -> let e1_type = expression_type e1 rho gamma in let e2_type = expression_type e2 rho gamma in (match e1_type with | TFunction(parameter_type, result_type) -> if parameter_type = e2_type then result_type else failwith "type error: the parameter has a wrong type" | _ -> failwith "type error: the operator is not a function") | EBinaryPrimitive(e1, name, e2) -> (binary_operator_type name) (expression_type e1 rho gamma) (expression_type e2 rho gamma) | EIf(e1, e2, e3) -> let e1_type = expression_type e1 rho gamma in let e2_type = expression_type e2 rho gamma in let e3_type = expression_type e3 rho gamma in if e1_type = TBool then if e2_type = e3_type then e2_type else failwith "conditional branches have different types" else failwith "condition hasn't boolean type" | ELet(x, x_type, e1, e2) -> let e1_type = expression_type e1 rho gamma in if x_type = e1_type then let e2_type = expression_type e1 (Environment.bind x x_type rho)gamma in e2_type else failwith "wrong type declaration in let";; let rec toplevel_type toplevel gamma = match toplevel with | TDefine(x, e) -> let e_type = expression_type e Environment.empty gamma in if Environment.is_bound x gamma then let declared_type = Environment.lookup x gamma in if declared_type = e_type then Environment.bind x e_type gamma else failwith "You didn't respect your previous global declaration" else Environment.bind x e_type gamma | TDeclare(x, x_type) -> Environment.bind x x_type gamma;; let rec program_type program gamma = match program with | PExpression main_expression -> expression_type main_expression Environment.empty gamma | PNonTrivial (toplevel_form, program_rest) -> let extended_gamma = toplevel_type toplevel_form gamma in program_type program_rest extended_gamma;;