From 9e2c057edbb53968888f41fc2dbc34ff491a154a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Fri, 11 Oct 2019 15:21:21 -0400 Subject: [PATCH] dune build passes, but not dune build @ligo-test. Threaded the typechecker's state in a bunch of places where it's likely not needed, because I don't know which parts are entrypoints and which parts are intermediate functions, and the role of the state between program fragments is not yet 100% clear to me. --- src/bin/cli.ml | 4 +++- src/main/compile/of_simplified.ml | 11 +++++++---- src/main/compile/of_source.ml | 8 ++++---- src/main/run/of_simplified.ml | 12 ++++++------ src/main/run/of_source.ml | 31 +++++++++++++++++-------------- src/passes/4-typer/solver.ml | 9 +++++++++ src/passes/4-typer/typer.ml | 4 ++-- 7 files changed, 48 insertions(+), 31 deletions(-) diff --git a/src/bin/cli.ml b/src/bin/cli.ml index 31e9261ab..2eacae3bd 100644 --- a/src/bin/cli.ml +++ b/src/bin/cli.ml @@ -154,9 +154,11 @@ let evaluate_value = let compile_expression = let f expression syntax display_format = toplevel ~display_format @@ + (* This is an actual compiler entry-point, so we start with a blank state *) + let state = Typer.Solver.initial_state in let%bind value = trace (simple_error "compile-input") @@ - Ligo.Run.Of_source.compile_expression expression (Syntax_name syntax) in + Ligo.Run.Of_source.compile_expression expression state (Syntax_name syntax) in ok @@ Format.asprintf "%a\n" Tezos_utils.Michelson.pp value in let term = diff --git a/src/main/compile/of_simplified.ml b/src/main/compile/of_simplified.ml index 96d1f6836..a443001a5 100644 --- a/src/main/compile/of_simplified.ml +++ b/src/main/compile/of_simplified.ml @@ -3,15 +3,18 @@ open Trace open Tezos_utils let compile_contract_entry (program : program) entry_point = - let%bind prog_typed = Typer.type_program program in + let%bind (prog_typed , state) = Typer.type_program program in + let () = Typer.Solver.discard_state state in Of_typed.compile_contract_entry prog_typed entry_point let compile_function_entry (program : program) entry_point : _ result = - let%bind prog_typed = Typer.type_program program in + let%bind (prog_typed , state) = Typer.type_program program in + let () = Typer.Solver.discard_state state in Of_typed.compile_function_entry prog_typed entry_point let compile_expression_as_function_entry (program : program) entry_point : _ result = - let%bind typed_program = Typer.type_program program in + let%bind (typed_program , state) = Typer.type_program program in + let () = Typer.Solver.discard_state state in Of_typed.compile_expression_as_function_entry typed_program entry_point (* TODO: do we need to thread the state here? Also, make the state arg. optional. *) @@ -21,7 +24,7 @@ let compile_expression_as_value ?(env = Ast_typed.Environment.full_empty) ~(stat let typed = let () = failwith "TODO : subst all" in let _todo = ignore (env, state) in typed in Of_typed.compile_expression_as_value typed -let compile_expression_as_function ?(env = Ast_typed.Environment.full_empty) ~(state : Typer.Solver.state) ae : _ result = +let compile_expression_as_function ?(env = Ast_typed.Environment.full_empty) ~(state : Typer.Solver.state) (ae : Ast_simplified.expression) : _ result = let%bind (typed , state) = Typer.type_expression env state ae in (* TODO: move this to typer.ml *) let typed = let () = failwith "TODO : subst all" in let _todo = ignore (env, state) in typed in diff --git a/src/main/compile/of_source.ml b/src/main/compile/of_source.ml index f7576ec19..b28244c3a 100644 --- a/src/main/compile/of_source.ml +++ b/src/main/compile/of_source.ml @@ -21,19 +21,19 @@ let compile_expression_as_function : string -> s_syntax -> _ result = fun expression syntax -> let%bind syntax = syntax_to_variant syntax None in let%bind simplified = parsify_expression syntax expression in - Of_simplified.compile_expression_as_function simplified + Of_simplified.compile_expression_as_function ~state:Typer.Solver.initial_state (* TODO: thread state or start with initial? *) simplified let type_file ?(debug_simplify = false) ?(debug_typed = false) - syntax (source_filename:string) : Ast_typed.program result = + syntax (source_filename:string) : (Ast_typed.program * Typer.Solver.state) result = let%bind syntax = syntax_to_variant syntax (Some source_filename) in let%bind simpl = parsify syntax source_filename in (if debug_simplify then Format.(printf "Simplified : %a\n%!" Ast_simplified.PP.program simpl) ) ; - let%bind typed = + let%bind (typed, state) = trace (simple_error "typing") @@ Typer.type_program simpl in (if debug_typed then ( Format.(printf "Typed : %a\n%!" Ast_typed.PP.program typed) )) ; - ok typed + ok (typed, state) diff --git a/src/main/run/of_simplified.ml b/src/main/run/of_simplified.ml index 4bc7729b8..aab84e240 100644 --- a/src/main/run/of_simplified.ml +++ b/src/main/run/of_simplified.ml @@ -1,24 +1,24 @@ open Trace open Ast_simplified -let compile_expression ?(value = false) ?env expr = +let compile_expression ?(value = false) ?env ~state expr = (* TODO: state optional *) if value then ( - Compile.Of_simplified.compile_expression_as_value ?env expr + Compile.Of_simplified.compile_expression_as_value ?env ~state expr ) else ( - let%bind code = Compile.Of_simplified.compile_expression_as_function ?env expr in + let%bind code = Compile.Of_simplified.compile_expression_as_function ?env ~state expr in Of_michelson.evaluate_michelson code ) -let run_typed_program +let run_typed_program (* TODO: this runs an *untyped* program, not a typed one. *) ?options ?input_to_value - (program : Ast_typed.program) (entry : string) + (program : Ast_typed.program) (state : Typer.Solver.state) (entry : string) (input : expression) : expression result = let%bind code = Compile.Of_typed.compile_function_entry program entry in let%bind input = let env = Ast_typed.program_environment program in - compile_expression ?value:input_to_value ~env input + compile_expression ?value:input_to_value ~env ~state input in let%bind ex_ty_value = Of_michelson.run ?options code input in Compile.Of_simplified.uncompile_typed_program_entry_function_result program entry ex_ty_value diff --git a/src/main/run/of_source.ml b/src/main/run/of_source.ml index f9a8e776c..1cdd71cf8 100644 --- a/src/main/run/of_source.ml +++ b/src/main/run/of_source.ml @@ -50,47 +50,48 @@ end let compile_file_contract_parameter : string -> string -> string -> Compile.Helpers.s_syntax -> Michelson.t result = fun source_filename _entry_point expression syntax -> - let%bind program = Compile.Of_source.type_file syntax source_filename in + let%bind (program , state) = Compile.Of_source.type_file syntax source_filename in let env = Ast_typed.program_environment program in let%bind syntax = Compile.Helpers.syntax_to_variant syntax (Some source_filename) in let%bind simplified = Compile.Helpers.parsify_expression syntax expression in - Of_simplified.compile_expression simplified ~env + Of_simplified.compile_expression simplified ~env ~state let compile_file_expression : string -> string -> string -> Compile.Helpers.s_syntax -> Michelson.t result = fun source_filename _entry_point expression syntax -> - let%bind program = Compile.Of_source.type_file syntax source_filename in + let%bind (program , state) = Compile.Of_source.type_file syntax source_filename in let env = Ast_typed.program_environment program in let%bind syntax = Compile.Helpers.syntax_to_variant syntax (Some source_filename) in let%bind simplified = Compile.Helpers.parsify_expression syntax expression in - Of_simplified.compile_expression simplified ~env + Of_simplified.compile_expression simplified ~env ~state -let compile_expression : string -> Compile.Helpers.s_syntax -> Michelson.t result = - fun expression syntax -> +let compile_expression : string -> Typer.Solver.state -> Compile.Helpers.s_syntax -> Michelson.t result = + fun expression state syntax -> let%bind syntax = Compile.Helpers.syntax_to_variant syntax None in let%bind simplified = Compile.Helpers.parsify_expression syntax expression in - Of_simplified.compile_expression simplified + Of_simplified.compile_expression ~state simplified let compile_file_contract_storage ~value : string -> string -> string -> Compile.Helpers.s_syntax -> Michelson.t result = fun source_filename _entry_point expression syntax -> - let%bind program = Compile.Of_source.type_file syntax source_filename in + let%bind (program , state) = Compile.Of_source.type_file syntax source_filename in let env = Ast_typed.program_environment program in let%bind syntax = Compile.Helpers.syntax_to_variant syntax (Some source_filename) in let%bind simplified = Compile.Helpers.parsify_expression syntax expression in - Of_simplified.compile_expression ~value simplified ~env + Of_simplified.compile_expression ~value simplified ~env ~state let compile_file_contract_args = fun ?value source_filename _entry_point storage parameter syntax -> - let%bind program = Compile.Of_source.type_file syntax source_filename in + let%bind (program , state) = Compile.Of_source.type_file syntax source_filename in let env = Ast_typed.program_environment program in let%bind syntax = Compile.Helpers.syntax_to_variant syntax (Some source_filename) in let%bind storage_simplified = Compile.Helpers.parsify_expression syntax storage in let%bind parameter_simplified = Compile.Helpers.parsify_expression syntax parameter in let args = Ast_simplified.e_pair storage_simplified parameter_simplified in - Of_simplified.compile_expression ?value args ~env + Of_simplified.compile_expression ?value args ~env ~state let run_contract ?amount ?storage_value source_filename entry_point storage parameter syntax = - let%bind program = Compile.Of_source.type_file syntax source_filename in + let%bind (program , state) = Compile.Of_source.type_file syntax source_filename in + let () = Typer.Solver.discard_state state in let%bind code = Compile.Of_typed.compile_function_entry program entry_point in let%bind args = compile_file_contract_args ?value:storage_value source_filename entry_point storage parameter syntax in let%bind ex_value_ty = @@ -104,7 +105,8 @@ let run_contract ?amount ?storage_value source_filename entry_point storage para Compile.Of_simplified.uncompile_typed_program_entry_function_result program entry_point ex_value_ty let run_function_entry ?amount source_filename entry_point input syntax = - let%bind program = Compile.Of_source.type_file syntax source_filename in + let%bind (program , state) = Compile.Of_source.type_file syntax source_filename in + let () = Typer.Solver.discard_state state in let%bind code = Compile.Of_typed.compile_function_entry program entry_point in let%bind args = compile_file_expression source_filename entry_point input syntax in let%bind ex_value_ty = @@ -118,7 +120,8 @@ let run_function_entry ?amount source_filename entry_point input syntax = Compile.Of_simplified.uncompile_typed_program_entry_function_result program entry_point ex_value_ty let evaluate_entry ?amount source_filename entry_point syntax = - let%bind program = Compile.Of_source.type_file syntax source_filename in + let%bind (program , state) = Compile.Of_source.type_file syntax source_filename in + let () = Typer.Solver.discard_state state in let%bind code = Compile.Of_typed.compile_expression_as_function_entry program entry_point in let%bind ex_value_ty = let options = diff --git a/src/passes/4-typer/solver.ml b/src/passes/4-typer/solver.ml index f277a7fb4..4898232d4 100644 --- a/src/passes/4-typer/solver.ml +++ b/src/passes/4-typer/solver.ml @@ -804,6 +804,15 @@ let initial_state : state = { assignments = TypeVariableMap.empty ; } +(* This function is called when a program is fully compiled, and the + typechecker's state is discarded. TODO: either get rid of the state + earlier, or perform a sanity check here (e.g. that types have been + inferred for all bindings and expressions, etc. + + Also, we should check at these places that we indeed do not need the + state any further. Suwanne *) +let discard_state (_ : state) = () + (* let replace_var_in_state = fun (v : type_variable) (state : state) -> *) (* let aux_tv : type_value -> _ = function *) (* | P_forall (w , cs , tval) -> failwith "TODO" *) diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml index d209d95aa..a6622e944 100644 --- a/src/passes/4-typer/typer.ml +++ b/src/passes/4-typer/typer.ml @@ -939,10 +939,10 @@ 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 result = +let type_program (p : I.program) : (O.program * Solver.state) result = let%bind (env, state, program) = type_program_returns_state p in let program = let () = failwith "TODO : subst all" in let _todo = ignore (env, state) in program in - ok program + ok (program, state) (* 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