typer: typecheck expression and subst (used e.g. to typecheck arguments of contracts)

src/main/compile/of_simplified.ml

@@ -8,7 +8,7 @@ let compile (program : Ast_simplified.program) : (Ast_typed.program * Typer.Solv
 let compile_expression ?(env = Ast_typed.Environment.full_empty) ~(state : Typer.Solver.state) (ae : Ast_simplified.expression)
     : (Ast_typed.value * Typer.Solver.state) result =
   let () = Typer.Solver.discard_state state in
-  Typer.type_expression env state ae
+  Typer.type_expression_subst env state ae
 
 let apply (entry_point : string) (param : Ast_simplified.expression) : Ast_simplified.expression result =
   let name = Var.of_name entry_point in

src/passes/4-typer-new/typer.ml

@@ -941,9 +941,7 @@ let untype_type_value (t:O.type_value) : (I.type_expression) result =
 (*
 Apply type_declaration on all the node of the AST_simplified from the root p
 *)
-let type_program_returns_state (p:I.program) : (environment * Solver.state * O.program) result =
+let type_program_returns_state ((env, state, p) : environment * Solver.state * I.program) : (environment * Solver.state * O.program) result =
-  let env = Ast_typed.Environment.full_empty in
-  let state = Solver.initial_state in
   let aux ((e : environment), (s : Solver.state) , (ds : O.declaration Location.wrap list)) (d:I.declaration Location.wrap) =
     let%bind (e' , s' , d'_opt) = type_declaration e s (Location.unwrap d) in
     let ds' = match d'_opt with
@@ -958,8 +956,8 @@ let type_program_returns_state (p:I.program) : (environment * Solver.state * O.p
   let () = ignore (env' , state') in
   ok (env', state', declarations)
 
-let type_program (p : I.program) : (O.program * Solver.state) result =
+let type_and_subst_xyz (env_state_node : environment * Solver.state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * Solver.state * 'a) -> (environment * Solver.state * 'b) Trace.result) : ('b * Solver.state) result =
-  let%bind (env, state, program) = type_program_returns_state p in
+  let%bind (env, state, program) = type_xyz_returns_state env_state_node in
   let subst_all =
     let aliases = state.structured_dbs.aliases in
     let assignments = state.structured_dbs.assignments in
@@ -977,12 +975,26 @@ let type_program (p : I.program) : (O.program * Solver.state) result =
       let%bind (expr : O.type_value') = Typesystem.Core.type_expression'_of_simple_c_constant (c_tag , (List.map (fun s -> O.{ type_value' = T_variable s ; simplified = None }) tv_list)) in
       ok @@ expr
     in
-    let p = Typesystem.Misc.Substitution.Pattern.s_program ~substs program in
+    let p = apply_substs ~substs program in
     p in
   let%bind program = subst_all in
   let () = ignore env in        (* TODO: shouldn't we use the `env` somewhere? *)
   ok (program, state)
 
+let type_program (p : I.program) : (O.program * Solver.state) result =
+  let empty_env = Ast_typed.Environment.full_empty in
+  let empty_state = Solver.initial_state in
+  type_and_subst_xyz (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state
+
+let type_expression_returns_state : (environment * Solver.state * I.expression) -> (environment * Solver.state * O.annotated_expression) Trace.result =
+  fun (env, state, e) ->
+  let%bind (e , state) = type_expression env state e in
+  ok (env, state, e)
+
+let type_expression_subst (env : environment) (state : Solver.state) ?(tv_opt : O.type_value option) (e : I.expression) : (O.annotated_expression * Solver.state) result =
+  let () = ignore tv_opt in     (* For compatibility with the old typer's API, this argument can be removed once the new typer is used. *)
+  type_and_subst_xyz (env , state , e) Typesystem.Misc.Substitution.Pattern.s_annotated_expression type_expression_returns_state
+
  (*
 TODO: Similar to type_program but use a fold_map_list and List.fold_left and add element to the left or the list which gives a better complexity
  *)

src/passes/4-typer-new/typer.mli

@@ -44,6 +44,7 @@ val type_declaration : environment -> Solver.state -> I.declaration -> (environm
 (* val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result *)
 val evaluate_type : environment -> I.type_expression -> O.type_value result
 val type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
+val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
 val type_constant : I.constant -> O.type_value list -> O.type_value option -> (O.constant * O.type_value) result
 (*
 val untype_type_value : O.type_value -> (I.type_expression) result

src/passes/4-typer/typer.ml

@@ -10,5 +10,5 @@ module Solver = Typer_new.Solver (* Both the old typer and the new typer use the
 type environment = Environment.t
 
 let type_program = if use_new_typer then Typer_new.type_program else Typer_old.type_program
-let type_expression = if use_new_typer then Typer_new.type_expression else Typer_old.type_expression
+let type_expression_subst = if use_new_typer then Typer_new.type_expression_subst else Typer_old.type_expression (* the old typer does not have unification variables that would need substitution, so no need to "subst" anything. *)
 let untype_expression = if use_new_typer then Typer_new.untype_expression else Typer_old.untype_expression

src/passes/4-typer/typer.mli

@@ -12,5 +12,5 @@ module Solver = Typer_new.Solver
 type environment = Environment.t
 
 val type_program : I.program -> (O.program * Solver.state) result
-val type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
+val type_expression_subst : environment -> Solver.state -> ?tv_opt:O.type_value -> I.expression -> (O.annotated_expression * Solver.state) result
 val untype_expression : O.annotated_expression -> I.expression result

src/test/typer_tests.ml

@@ -12,7 +12,7 @@ let int () : unit result =
   let open Typer in
   let e = Environment.full_empty in
   let state = Typer.Solver.initial_state in
-  let%bind (post , new_state) = type_expression e state pre in
+  let%bind (post , new_state) = type_expression_subst e state pre in
   let () = Typer.Solver.discard_state new_state in
   let open! Typed in
   let open Combinators in
@@ -27,7 +27,7 @@ module TestExpressions = struct
     let pre = expr in
     let open Typer in
     let open! Typed in
-    let%bind (post , new_state) = type_expression env state pre in
+    let%bind (post , new_state) = type_expression_subst env state pre in
     let () = Typer.Solver.discard_state new_state in
     let%bind () = assert_type_value_eq (post.type_annotation, test_expected_ty) in
     ok ()