From 77fdb739b6e3238cefe6f3f26639480602ef538d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Fri, 6 Dec 2019 18:30:04 +0100 Subject: [PATCH] typer: typecheck expression and subst (used e.g. to typecheck arguments of contracts) --- src/main/compile/of_simplified.ml | 2 +- src/passes/4-typer-new/typer.ml | 24 ++++++++++++++++++------ src/passes/4-typer-new/typer.mli | 1 + src/passes/4-typer/typer.ml | 2 +- src/passes/4-typer/typer.mli | 2 +- src/test/typer_tests.ml | 4 ++-- 6 files changed, 24 insertions(+), 11 deletions(-) diff --git a/src/main/compile/of_simplified.ml b/src/main/compile/of_simplified.ml index 56f8721fe..3e98e7658 100644 --- a/src/main/compile/of_simplified.ml +++ b/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 diff --git a/src/passes/4-typer-new/typer.ml b/src/passes/4-typer-new/typer.ml index 431bc228c..7126f3a3e 100644 --- a/src/passes/4-typer-new/typer.ml +++ b/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 env = Ast_typed.Environment.full_empty in - let state = Solver.initial_state in +let type_program_returns_state ((env, state, p) : environment * Solver.state * I.program) : (environment * Solver.state * O.program) result = 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%bind (env, state, program) = type_program_returns_state p in +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_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 *) diff --git a/src/passes/4-typer-new/typer.mli b/src/passes/4-typer-new/typer.mli index 07c28338b..379b31b1e 100644 --- a/src/passes/4-typer-new/typer.mli +++ b/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 diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml index c59346c8b..8ab5576a0 100644 --- a/src/passes/4-typer/typer.ml +++ b/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 diff --git a/src/passes/4-typer/typer.mli b/src/passes/4-typer/typer.mli index cd11ec423..b7c410383 100644 --- a/src/passes/4-typer/typer.mli +++ b/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 diff --git a/src/test/typer_tests.ml b/src/test/typer_tests.ml index ec0e1c725..abeb7b2e8 100644 --- a/src/test/typer_tests.ml +++ b/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 ()