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.

This commit is contained in:
Suzanne Dupéron 2019-10-11 15:21:21 -04:00
parent 1356159281
commit 9e2c057edb
7 changed files with 48 additions and 31 deletions

View File

@ -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 =

View File

@ -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

View File

@ -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)

View File

@ -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

View File

@ -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 =

View File

@ -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" *)

View File

@ -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