From 9eeac11628cfa79b71d10f4b9bd4b7e2d7d82972 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Thu, 7 May 2020 16:08:31 +0200 Subject: [PATCH] some environment cleanup --- src/bin/expect_tests/contract_tests.ml | 4 +- src/bin/expect_tests/typer_error_tests.ml | 2 +- src/environment/environment.ml | 12 +-- src/main/compile/of_core.ml | 2 +- src/passes/10-transpiler/untranspiler.ml | 4 +- src/passes/8-typer-new/errors.ml | 6 +- src/passes/8-typer-new/typer.ml | 4 +- src/passes/8-typer-old/typer.ml | 12 +-- .../9-self_ast_typed/michelson_layout.ml | 2 +- src/stages/1-ast_imperative/types.ml | 8 +- src/stages/2-ast_sugar/types.ml | 8 +- src/stages/3-ast_core/types.ml | 8 +- src/stages/4-ast_typed/PP_generic.ml | 5 +- src/stages/4-ast_typed/combinators.mli | 38 ++++----- .../4-ast_typed/combinators_environment.ml | 30 +++---- .../4-ast_typed/combinators_environment.mli | 2 +- src/stages/4-ast_typed/environment.ml | 81 +++++++------------ src/stages/4-ast_typed/environment.mli | 48 +---------- src/stages/4-ast_typed/misc.ml | 4 +- src/stages/4-ast_typed/misc.mli | 2 +- src/stages/4-ast_typed/misc_smart.ml | 4 +- src/stages/4-ast_typed/types.ml | 17 ++-- src/stages/typesystem/misc.ml | 20 ++--- src/test/typer_tests.ml | 2 +- 24 files changed, 122 insertions(+), 203 deletions(-) diff --git a/src/bin/expect_tests/contract_tests.ml b/src/bin/expect_tests/contract_tests.ml index 3e9c0199a..7025aa1a2 100644 --- a/src/bin/expect_tests/contract_tests.ml +++ b/src/bin/expect_tests/contract_tests.ml @@ -1425,7 +1425,7 @@ let%expect_test _ = let%expect_test _ = run_ligo_bad [ "compile-contract" ; bad_contract "redundant_constructors.mligo" ; "main" ] ; [%expect {| - ligo: redundant constructor: {"constructor":"Add","environment":"- E[]\tT[union_a -> sum[Add -> int , Remove -> int]]\n- E[]\tT[bool -> sum[false -> unit , true -> unit]]]"} + ligo: redundant constructor: {"constructor":"Add","environment":"- E[]\tT[union_a -> sum[Add -> int , Remove -> int]\nbool -> sum[false -> unit , true -> unit]]"} If you're not sure how to fix this error, you can @@ -1465,7 +1465,7 @@ ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, char run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_no_inline.mligo" ; "main" ] ; [%expect {| - ligo: in file "create_contract_no_inline.mligo", line 3, characters 40-46. unbound type variable: {"variable":"return","location":"in file \"create_contract_no_inline.mligo\", line 3, characters 40-46","in":"- E[foo -> int]\tT[] - E[]\tT[bool -> sum[false -> unit , true -> unit]]]","did_you_mean":"no suggestion"} + ligo: in file "create_contract_no_inline.mligo", line 3, characters 40-46. unbound type variable: {"variable":"return","location":"in file \"create_contract_no_inline.mligo\", line 3, characters 40-46","in":"- E[foo -> int]\tT[bool -> sum[false -> unit , true -> unit]]","did_you_mean":"no suggestion"} If you're not sure how to fix this error, you can diff --git a/src/bin/expect_tests/typer_error_tests.ml b/src/bin/expect_tests/typer_error_tests.ml index 14162cd5a..1718b83a0 100644 --- a/src/bin/expect_tests/typer_error_tests.ml +++ b/src/bin/expect_tests/typer_error_tests.ml @@ -119,7 +119,7 @@ let%expect_test _ = run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_typer_5.mligo" ; "main" ] ; [%expect {| - ligo: in file "error_typer_5.mligo", line 1, characters 10-17. unbound type variable: {"variable":"boolean","location":"in file \"error_typer_5.mligo\", line 1, characters 10-17","in":"- E[]\tT[] - E[]\tT[bool -> sum[false -> unit , true -> unit]]]","did_you_mean":"bool"} + ligo: in file "error_typer_5.mligo", line 1, characters 10-17. unbound type variable: {"variable":"boolean","location":"in file \"error_typer_5.mligo\", line 1, characters 10-17","in":"- E[]\tT[bool -> sum[false -> unit , true -> unit]]","did_you_mean":"bool"} If you're not sure how to fix this error, you can diff --git a/src/environment/environment.ml b/src/environment/environment.ml index 523531836..a4fbc6e34 100644 --- a/src/environment/environment.ml +++ b/src/environment/environment.ml @@ -1,11 +1 @@ -open Ast_typed - -let merge e1 e2 = - let e1 = List.Ne.to_list e1 in - let e2 = List.Ne.to_list e2 in - List.Ne.of_list @@ e1 @ e2 - - -let default = Environment.full_empty - -let default = merge default Bool.environment +let default = Bool.environment \ No newline at end of file diff --git a/src/main/compile/of_core.ml b/src/main/compile/of_core.ml index c7992399e..6e1eb30b6 100644 --- a/src/main/compile/of_core.ml +++ b/src/main/compile/of_core.ml @@ -13,7 +13,7 @@ let compile (cform: form) (program : Ast_core.program) : (Ast_typed.program * As | Env -> ok applied in ok @@ (applied', state) -let compile_expression ?(env = Ast_typed.Environment.full_empty) ~(state : Ast_typed.typer_state) (e : Ast_core.expression) +let compile_expression ?(env = Ast_typed.Environment.empty) ~(state : Ast_typed.typer_state) (e : Ast_core.expression) : (Ast_typed.expression * Ast_typed.typer_state) result = let%bind (ae_typed,state) = Typer.type_expression_subst env state e in let () = Typer.Solver.discard_state state in diff --git a/src/passes/10-transpiler/untranspiler.ml b/src/passes/10-transpiler/untranspiler.ml index edec0b53f..26e2dd287 100644 --- a/src/passes/10-transpiler/untranspiler.ml +++ b/src/passes/10-transpiler/untranspiler.ml @@ -48,13 +48,13 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul let%bind b = trace_strong (wrong_mini_c_value "bool" v) @@ get_bool v in - return (e_bool b Environment.full_empty) + return (e_bool b Environment.empty) ) | t when (compare t (t_bool ()).type_content) = 0-> ( let%bind b = trace_strong (wrong_mini_c_value "bool" v) @@ get_bool v in - return (e_bool b Environment.full_empty) + return (e_bool b Environment.empty) ) | T_constant type_constant -> ( match type_constant with diff --git a/src/passes/8-typer-new/errors.ml b/src/passes/8-typer-new/errors.ml index 50056d9e4..7446d2f40 100644 --- a/src/passes/8-typer-new/errors.ml +++ b/src/passes/8-typer-new/errors.ml @@ -10,7 +10,7 @@ let unbound_type_variable (e:environment) (tv:I.type_variable) (loc:Location.t) let data = [ ("variable" , fun () -> Format.asprintf "%a" I.PP.type_variable tv) ; ("location" , fun () -> Format.asprintf "%a" Location.pp loc) ; - ("in" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) + ("in" , fun () -> Format.asprintf "%a" Environment.PP.environment e) ] in error ~data title message () @@ -20,7 +20,7 @@ let unbound_variable (e:environment) (n:I.expression_variable) (loc:Location.t) let message () = "" in let data = [ ("variable" , name) ; - ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ; + ("environment" , fun () -> Format.asprintf "%a" Environment.PP.environment e) ; ("location" , fun () -> Format.asprintf "%a" Location.pp loc) ] in error ~data title message () @@ -60,7 +60,7 @@ let unbound_constructor (e:environment) (c:I.constructor') (loc:Location.t) () = let message () = "" in let data = [ ("constructor" , fun () -> Format.asprintf "%a" I.PP.constructor c) ; - ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ; + ("environment" , fun () -> Format.asprintf "%a" Environment.PP.environment e) ; ("location" , fun () -> Format.asprintf "%a" Location.pp loc) ] in error ~data title message () diff --git a/src/passes/8-typer-new/typer.ml b/src/passes/8-typer-new/typer.ml index f524af386..36fa997fe 100644 --- a/src/passes/8-typer-new/typer.ml +++ b/src/passes/8-typer-new/typer.ml @@ -28,7 +28,7 @@ let rec type_declaration env state : I.declaration -> (environment * O.typer_sta let%bind (expr , state') = trace (constant_declaration_error binder expression tv'_opt) @@ type_expression env state expression in - let post_env = Environment.add_ez_ae binder expr env in + let post_env = Environment.add_ez_declaration binder expr env in ok (post_env, state' , Some (O.Declaration_constant { binder ; expr ; inline ; post_env} )) ) @@ -286,7 +286,7 @@ and type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression let content () = Format.asprintf "%a in:\n%a\n" Stage_common.PP.constructor constructor - O.Environment.PP.full_environment e + O.Environment.PP.environment e in error title content in trace_option error @@ diff --git a/src/passes/8-typer-old/typer.ml b/src/passes/8-typer-old/typer.ml index cfe39ee30..85079b11c 100644 --- a/src/passes/8-typer-old/typer.ml +++ b/src/passes/8-typer-old/typer.ml @@ -40,7 +40,7 @@ module Errors = struct let data = [ ("variable" , fun () -> Format.asprintf "%a" I.PP.type_variable tv) ; ("location" , fun () -> Format.asprintf "%a" Location.pp loc) ; - ("in" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ; + ("in" , fun () -> Format.asprintf "%a" Environment.PP.environment e) ; ("did_you_mean" , fun () -> suggestion) ] in error ~data title message () @@ -51,7 +51,7 @@ module Errors = struct let message () = "" in let data = [ ("variable" , name) ; - ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ; + ("environment" , fun () -> Format.asprintf "%a" Environment.PP.environment e) ; ("location" , fun () -> Format.asprintf "%a" Location.pp loc) ] in error ~data title message () @@ -91,7 +91,7 @@ module Errors = struct let message () = "" in let data = [ ("constructor" , fun () -> Format.asprintf "%a" I.PP.constructor c); - ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ; + ("environment" , fun () -> Format.asprintf "%a" Environment.PP.environment e) ; ("location" , fun () -> Format.asprintf "%a" Location.pp loc) ] in error ~data title message () @@ -101,7 +101,7 @@ module Errors = struct let message () = "" in let data = [ ("constructor" , fun () -> Format.asprintf "%a" I.PP.constructor c); - ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ; + ("environment" , fun () -> Format.asprintf "%a" Environment.PP.environment e) ; ] in error ~data title message () @@ -514,7 +514,7 @@ and type_declaration env (_placeholder_for_state_of_new_typer : O.typer_state) : let%bind expr = trace (constant_declaration_error binder expression tv'_opt) @@ type_expression' ?tv_opt:tv'_opt env expression in - let post_env = Environment.add_ez_ae binder expr env in + let post_env = Environment.add_ez_declaration binder expr env in ok (post_env, (Solver.placeholder_for_state_of_new_typer ()) , Some (O.Declaration_constant { binder ; expr ; inline ; post_env})) ) @@ -766,7 +766,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression let content () = Format.asprintf "%a in:\n%a\n" Stage_common.PP.constructor constructor - O.Environment.PP.full_environment e + O.Environment.PP.environment e in error title content in trace_option error @@ diff --git a/src/passes/9-self_ast_typed/michelson_layout.ml b/src/passes/9-self_ast_typed/michelson_layout.ml index cd6af6142..2211715b9 100644 --- a/src/passes/9-self_ast_typed/michelson_layout.ml +++ b/src/passes/9-self_ast_typed/michelson_layout.ml @@ -25,7 +25,7 @@ let match_var (t:type_expression) = { expression_content = E_variable (Var.of_name "x") ; location = Location.generated ; type_expression = t ; - environment = Environment.add_ez_binder (Var.of_name "x") t Environment.full_empty} + environment = Environment.add_ez_binder (Var.of_name "x") t Environment.empty} let matching (e:expression) matchee cases = { expression_content = E_matching {matchee ; cases}; diff --git a/src/stages/1-ast_imperative/types.ml b/src/stages/1-ast_imperative/types.ml index baaefc48a..4651c1f9f 100644 --- a/src/stages/1-ast_imperative/types.ml +++ b/src/stages/1-ast_imperative/types.ml @@ -189,17 +189,15 @@ and free_variables = expression_variable list and environment_element = { type_value: type_expression - ; source_environment: full_environment + ; source_environment: environment ; definition: environment_element_definition } -and environment = (expression_variable * environment_element) list +and expr_environment = (expression_variable * environment_element) list and type_environment = (type_variable * type_expression) list (* SUBST ??? *) -and small_environment = environment * type_environment - -and full_environment = small_environment List.Ne.t +and environment = expr_environment * type_environment and expr = expression diff --git a/src/stages/2-ast_sugar/types.ml b/src/stages/2-ast_sugar/types.ml index 566f8ec35..88df116fb 100644 --- a/src/stages/2-ast_sugar/types.ml +++ b/src/stages/2-ast_sugar/types.ml @@ -147,17 +147,15 @@ and free_variables = expression_variable list and environment_element = { type_value: type_expression - ; source_environment: full_environment + ; source_environment: environment ; definition: environment_element_definition } -and environment = (expression_variable * environment_element) list +and expr_environment = (expression_variable * environment_element) list and type_environment = (type_variable * type_expression) list (* SUBST ??? *) -and small_environment = environment * type_environment - -and full_environment = small_environment List.Ne.t +and environment = expr_environment * type_environment and expr = expression diff --git a/src/stages/3-ast_core/types.ml b/src/stages/3-ast_core/types.ml index e925c5f3b..2a76591df 100644 --- a/src/stages/3-ast_core/types.ml +++ b/src/stages/3-ast_core/types.ml @@ -92,17 +92,15 @@ and free_variables = expression_variable list and environment_element = { type_value: type_expression - ; source_environment: full_environment + ; source_environment: environment ; definition: environment_element_definition } -and environment = (expression_variable * environment_element) list +and expr_environment = (expression_variable * environment_element) list and type_environment = (type_variable * type_expression) list (* SUBST ??? *) -and small_environment = environment * type_environment - -and full_environment = small_environment List.Ne.t +and environment = expr_environment * type_environment and expr = expression diff --git a/src/stages/4-ast_typed/PP_generic.ml b/src/stages/4-ast_typed/PP_generic.ml index d28e164ee..b2a2bf179 100644 --- a/src/stages/4-ast_typed/PP_generic.ml +++ b/src/stages/4-ast_typed/PP_generic.ml @@ -27,7 +27,6 @@ let needs_parens = { label_map = (fun _ _ _ _ -> false) ; list = (fun _ _ _ _ -> false) ; location_wrap = (fun _ _ _ _ -> false) ; - list_ne = (fun _ _ _ _ -> false) ; option = (fun _visitor _continue _state o -> match o with None -> false | Some _ -> true) ; poly_unionfind = (fun _ _ _ _ -> false) ; @@ -80,10 +79,10 @@ let op ppf = { location_wrap = (fun _visitor continue () lwrap -> let ({ wrap_content; location } : _ Location.wrap) = lwrap in fprintf ppf "{ wrap_content = %a ; location = %a }" (fun _ppf -> continue ()) wrap_content Location.pp location); - list_ne = (fun _visitor continue () (first, lst) -> + (* list_ne = (fun _visitor continue () (first, lst) -> let aux ppf elt = fprintf ppf "%a" (fun _ppf -> continue ()) elt in - fprintf ppf "[@,@[ %a @]@,]" (list_sep aux (fun ppf () -> fprintf ppf " ;@ ")) (first::lst)); + fprintf ppf "[@,@[ %a @]@,]" (list_sep aux (fun ppf () -> fprintf ppf " ;@ ")) (first::lst)); *) option = (fun _visitor continue () o -> match o with | None -> fprintf ppf "None" diff --git a/src/stages/4-ast_typed/combinators.mli b/src/stages/4-ast_typed/combinators.mli index 485dc6185..e3ce6a156 100644 --- a/src/stages/4-ast_typed/combinators.mli +++ b/src/stages/4-ast_typed/combinators.mli @@ -3,7 +3,7 @@ open Types val make_n_t : type_variable -> type_expression -> named_type_content val make_t : ?loc:Location.t -> type_content -> S.type_expression option -> type_expression -val make_e : ?location:Location.t -> expression_content -> type_expression -> full_environment -> expression +val make_e : ?location:Location.t -> expression_content -> type_expression -> environment -> expression val t_bool : ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression val t_string : ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression @@ -38,7 +38,7 @@ val t_function : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.t val t_shallow_closure : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression val get_type_expression : expression -> type_expression val get_type' : type_expression -> type_content -val get_environment : expression -> full_environment +val get_environment : expression -> environment val get_expression : expression -> expression_content val get_lambda : expression -> lambda result val get_lambda_with_type : expression -> (lambda * ( type_expression * type_expression) ) result @@ -115,7 +115,7 @@ val e_unit : unit -> expression_content val e_int : Z.t -> expression_content val e_nat : Z.t -> expression_content val e_mutez : Z.t -> expression_content -val e_bool : bool -> full_environment -> expression_content +val e_bool : bool -> environment -> expression_content val e_string : string -> expression_content val e_bytes : bytes -> expression_content val e_timestamp : Z.t -> expression_content @@ -131,22 +131,22 @@ val e_application : expression -> expression -> expression_content val e_variable : expression_variable -> expression_content val e_let_in : expression_variable -> inline -> expression -> expression -> expression_content -val e_a_unit : full_environment -> expression -val e_a_int : Z.t -> full_environment -> expression -val e_a_nat : Z.t -> full_environment -> expression -val e_a_mutez : Z.t -> full_environment -> expression -val e_a_bool : bool -> full_environment -> expression -val e_a_string : string -> full_environment -> expression -val e_a_address : string -> full_environment -> expression -val e_a_pair : expression -> expression -> full_environment -> expression -val e_a_some : expression -> full_environment -> expression -val e_a_lambda : lambda -> type_expression -> type_expression -> full_environment -> expression -val e_a_none : type_expression -> full_environment -> expression -val e_a_record : expression label_map -> full_environment -> expression -val e_a_application : expression -> expression -> full_environment -> expression -val e_a_variable : expression_variable -> type_expression -> full_environment -> expression -val ez_e_a_record : ( label * expression ) list -> full_environment -> expression -val e_a_let_in : expression_variable -> bool -> expression -> expression -> full_environment -> expression +val e_a_unit : environment -> expression +val e_a_int : Z.t -> environment -> expression +val e_a_nat : Z.t -> environment -> expression +val e_a_mutez : Z.t -> environment -> expression +val e_a_bool : bool -> environment -> expression +val e_a_string : string -> environment -> expression +val e_a_address : string -> environment -> expression +val e_a_pair : expression -> expression -> environment -> expression +val e_a_some : expression -> environment -> expression +val e_a_lambda : lambda -> type_expression -> type_expression -> environment -> expression +val e_a_none : type_expression -> environment -> expression +val e_a_record : expression label_map -> environment -> expression +val e_a_application : expression -> expression -> environment -> expression +val e_a_variable : expression_variable -> type_expression -> environment -> expression +val ez_e_a_record : ( label * expression ) list -> environment -> expression +val e_a_let_in : expression_variable -> bool -> expression -> expression -> environment -> expression val get_a_int : expression -> Z.t result val get_a_unit : expression -> unit result diff --git a/src/stages/4-ast_typed/combinators_environment.ml b/src/stages/4-ast_typed/combinators_environment.ml index 5fcb358fa..78e11ad9a 100644 --- a/src/stages/4-ast_typed/combinators_environment.ml +++ b/src/stages/4-ast_typed/combinators_environment.ml @@ -1,25 +1,25 @@ open Types open Combinators -let make_a_e_empty expression type_annotation = make_e expression type_annotation Environment.full_empty +let make_a_e_empty expression type_annotation = make_e expression type_annotation Environment.empty -let e_a_empty_unit = e_a_unit Environment.full_empty -let e_a_empty_int n = e_a_int n Environment.full_empty -let e_a_empty_nat n = e_a_nat n Environment.full_empty -let e_a_empty_mutez n = e_a_mutez n Environment.full_empty -let e_a_empty_bool b = e_a_bool b Environment.full_empty -let e_a_empty_string s = e_a_string s Environment.full_empty -let e_a_empty_address s = e_a_address s Environment.full_empty -let e_a_empty_pair a b = e_a_pair a b Environment.full_empty -let e_a_empty_some s = e_a_some s Environment.full_empty -let e_a_empty_none t = e_a_none t Environment.full_empty -let e_a_empty_record r = e_a_record r Environment.full_empty -let ez_e_a_empty_record r = ez_e_a_record r Environment.full_empty -let e_a_empty_lambda l i o = e_a_lambda l i o Environment.full_empty +let e_a_empty_unit = e_a_unit Environment.empty +let e_a_empty_int n = e_a_int n Environment.empty +let e_a_empty_nat n = e_a_nat n Environment.empty +let e_a_empty_mutez n = e_a_mutez n Environment.empty +let e_a_empty_bool b = e_a_bool b Environment.empty +let e_a_empty_string s = e_a_string s Environment.empty +let e_a_empty_address s = e_a_address s Environment.empty +let e_a_empty_pair a b = e_a_pair a b Environment.empty +let e_a_empty_some s = e_a_some s Environment.empty +let e_a_empty_none t = e_a_none t Environment.empty +let e_a_empty_record r = e_a_record r Environment.empty +let ez_e_a_empty_record r = ez_e_a_record r Environment.empty +let e_a_empty_lambda l i o = e_a_lambda l i o Environment.empty open Environment -let env_sum_type ?(env = full_empty) +let env_sum_type ?(env = empty) ?(type_name = Var.of_name "a_sum_type") (lst : (constructor' * ctor_content) list) = add_type type_name (make_t_ez_sum lst) env diff --git a/src/stages/4-ast_typed/combinators_environment.mli b/src/stages/4-ast_typed/combinators_environment.mli index 55c345b47..861d67083 100644 --- a/src/stages/4-ast_typed/combinators_environment.mli +++ b/src/stages/4-ast_typed/combinators_environment.mli @@ -16,4 +16,4 @@ val e_a_empty_record : expression label_map -> expression val ez_e_a_empty_record : ( label * expression ) list -> expression val e_a_empty_lambda : lambda -> type_expression -> type_expression -> expression -val env_sum_type : ?env:full_environment -> ?type_name:type_variable -> (constructor' * ctor_content) list -> full_environment +val env_sum_type : ?env:environment -> ?type_name:type_variable -> (constructor' * ctor_content) list -> environment diff --git a/src/stages/4-ast_typed/environment.ml b/src/stages/4-ast_typed/environment.ml index d1bc6dc73..30e59ebab 100644 --- a/src/stages/4-ast_typed/environment.ml +++ b/src/stages/4-ast_typed/environment.ml @@ -1,52 +1,46 @@ open Types open Combinators +type t = environment type element = environment_element -let make_element : type_expression -> full_environment -> environment_element_definition -> element = + +let make_element : type_expression -> environment -> environment_element_definition -> element = fun type_value source_environment definition -> {type_value ; source_environment ; definition} let make_element_binder = fun t s -> make_element t s ED_binder + let make_element_declaration = fun s (expr : expression) -> let free_variables = Misc.Free_variables.(expression empty expr) in make_element (get_type_expression expr) s (ED_declaration {expr ; free_variables}) -module Small = struct - type t = small_environment +let empty : t = { expression_environment = [] ; type_environment = [] } - let empty : t = { expression_environment = [] ; type_environment = [] } +let get_expr_environment : t -> expression_environment = fun { expression_environment ; type_environment=_ } -> expression_environment +(* TODO: generate *) +let get_type_environment : t -> type_environment = fun { expression_environment=_ ; type_environment } -> type_environment +(* TODO: generate *) +let map_expr_environment : _ -> t -> t = fun f { expression_environment ; type_environment } -> { expression_environment = f expression_environment ; type_environment } +let map_type_environment : _ -> t -> t = fun f { expression_environment ; type_environment } -> { expression_environment ; type_environment = f type_environment } - (* TODO: generate *) - let get_environment : t -> environment = fun { expression_environment ; type_environment=_ } -> expression_environment - (* TODO: generate *) - let get_type_environment : t -> type_environment = fun { expression_environment=_ ; type_environment } -> type_environment - (* TODO: generate *) - let map_environment : _ -> t -> t = fun f { expression_environment ; type_environment } -> { expression_environment = f expression_environment ; type_environment } - let map_type_environment : _ -> t -> t = fun f { expression_environment ; type_environment } -> { expression_environment ; type_environment = f type_environment } +let add_expr : expression_variable -> element -> t -> t = fun expr_var env_elt -> map_expr_environment (fun x -> {expr_var ; env_elt} :: x) +let add_type : type_variable -> type_expression -> t -> t = fun type_variable type_ -> map_type_environment (fun x -> { type_variable ; type_ } :: x) +(* TODO: generate : these are now messy, clean them up. *) +let get_opt : expression_variable -> t -> element option = fun k x -> + Option.bind (fun {expr_var=_ ; env_elt} -> Some env_elt) @@ + List.find_opt (fun {expr_var ; env_elt=_} -> Var.equal expr_var k) (get_expr_environment x) +let get_type_opt : type_variable -> t -> type_expression option = fun k x -> + Option.bind (fun {type_variable=_ ; type_} -> Some type_) @@ + List.find_opt (fun {type_variable ; type_=_} -> Var.equal type_variable k) (get_type_environment x) - let add : expression_variable -> element -> t -> t = fun expr_var env_elt -> map_environment (fun x -> {expr_var ; env_elt} :: x) - let add_type : type_variable -> type_expression -> t -> t = fun type_variable type_ -> map_type_environment (fun x -> { type_variable ; type_ } :: x) - (* TODO: generate : these are now messy, clean them up. *) - let get_opt : expression_variable -> t -> element option = fun k x -> Option.bind (fun {expr_var=_ ; env_elt} -> Some env_elt) @@ List.find_opt (fun {expr_var ; env_elt=_} -> Var.equal expr_var k) (get_environment x) - let get_type_opt : type_variable -> t -> type_expression option = fun k x -> Option.bind (fun {type_variable=_ ; type_} -> Some type_) @@ List.find_opt (fun {type_variable ; type_=_} -> Var.equal type_variable k) (get_type_environment x) -end - -type t = full_environment -let empty : environment = Small.(get_environment empty) -let full_empty : t = List.Ne.singleton Small.empty -let add : expression_variable -> element -> t -> t = fun k v -> List.Ne.hd_map (Small.add k v) let add_ez_binder : expression_variable -> type_expression -> t -> t = fun k v e -> - List.Ne.hd_map (Small.add k (make_element_binder v e)) e + add_expr k (make_element_binder v e) e + let add_ez_declaration : expression_variable -> expression -> t -> t = fun k ae e -> - List.Ne.hd_map (Small.add k (make_element_declaration e ae)) e -let add_ez_ae = add_ez_declaration -let add_type : type_variable -> type_expression -> t -> t = fun k v -> List.Ne.hd_map (Small.add_type k v) -let get_opt : expression_variable -> t -> element option = fun k x -> List.Ne.find_map (Small.get_opt k) x -let get_type_opt : type_variable -> t -> type_expression option = fun k x -> List.Ne.find_map (Small.get_type_opt k) x + add_expr k (make_element_declaration e ae) e let convert_constructor' (S.Constructor c) = Constructor c let get_constructor : Ast_core.constructor' -> t -> (type_expression * type_expression) option = fun k x -> (* Left is the constructor, right is the sum type *) - let aux = fun x -> let aux = fun {type_variable=_ ; type_} -> match type_.type_content with | T_sum m -> @@ -55,8 +49,7 @@ let get_constructor : Ast_core.constructor' -> t -> (type_expression * type_expr | None -> None) | _ -> None in - List.find_map aux (Small.get_type_environment x) in - List.Ne.find_map aux x + List.find_map aux (get_type_environment x) module PP = struct @@ -72,27 +65,15 @@ module PP = struct let type_environment_element = fun ppf {type_variable ; type_} -> fprintf ppf "%a -> %a" PP.type_variable type_variable PP.type_expression type_ - let environment : _ -> environment -> unit = fun ppf lst -> - fprintf ppf "E[%a]" (list_sep environment_element (const " , ")) lst + let expr_environment : _ -> expression_environment -> unit = fun ppf lst -> + fprintf ppf "E[%a]" (list_sep environment_element (tag "@,")) lst let type_environment = fun ppf lst -> - fprintf ppf "T[%a]" (list_sep type_environment_element (const " , ")) lst + fprintf ppf "T[%a]" (list_sep type_environment_element (tag "@,")) lst - let small_environment : _ -> small_environment -> unit = fun ppf e -> + let environment : _ -> environment -> unit = fun ppf e -> fprintf ppf "- %a\t%a" - environment (Small.get_environment e) - type_environment (Small.get_type_environment e) + expr_environment (get_expr_environment e) + type_environment (get_type_environment e) - let full_environment : _ -> full_environment -> unit = fun ppf e -> - fprintf ppf "@[%a]" - (ne_list_sep small_environment (tag "@;")) e -end - -open Trace - -let get_trace : expression_variable -> t -> element result = fun s env -> - let error = - let title () = "missing var not in env" in - let content () = Format.asprintf "\nvar: %a\nenv: %a\n" PP. expression_variable s PP.full_environment env in - error title content in - trace_option error @@ get_opt s env +end \ No newline at end of file diff --git a/src/stages/4-ast_typed/environment.mli b/src/stages/4-ast_typed/environment.mli index 657552937..6b3fb52e2 100644 --- a/src/stages/4-ast_typed/environment.mli +++ b/src/stages/4-ast_typed/environment.mli @@ -1,62 +1,20 @@ open Types -open Trace -type t = full_environment +type t = environment type element = environment_element -val get_trace : expression_variable -> t -> element result -val empty : environment -val full_empty : t -val add : expression_variable -> element -> t -> t +val empty : t val add_ez_binder : expression_variable -> type_expression -> t -> t val add_ez_declaration : expression_variable -> expression -> t -> t -val add_ez_ae : expression_variable -> expression -> t -> t val add_type : type_variable -> type_expression -> t -> t val get_opt : expression_variable -> t -> element option val get_type_opt : type_variable -> t -> type_expression option val get_constructor : Ast_core.constructor' -> t -> (type_expression * type_expression) option -module Small : sig - type t = small_environment - val get_environment : t -> environment -(* - - val empty : t - - val get_type_environment : t -> type_environment - val map_environment : ( environment -> environment ) -> t -> t - val map_type_environment : ( type_environment -> type_environment ) -> t -> t - - val add : string -> element -> t -> t - val add_type : string -> type_expression -> t -> t - val get_opt : string -> t -> element option - val get_type_opt : string -> t -> type_expression option - *) -end -(* - -val make_element : type_expression -> full_environment -> environment_element_definition -> element -val make_element_binder : type_expression -> full_environment -> element -val make_element_declaration : full_environment -> expression -> element -*) - - - module PP : sig open Format val list_sep_scope : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit - val full_environment : formatter -> full_environment -> unit -(* - val environment_element : formatter -> ( string * environment_element ) -> unit + val environment : formatter -> environment -> unit - val type_environment_element : formatter -> ( string * type_expression ) -> unit - - val environment : formatter -> environment -> unit - - val type_environment : formatter -> type_environment -> unit - - val small_environment : formatter -> small_environment -> unit - - *) end diff --git a/src/stages/4-ast_typed/misc.ml b/src/stages/4-ast_typed/misc.ml index a2c5c9b87..a3df9718f 100644 --- a/src/stages/4-ast_typed/misc.ml +++ b/src/stages/4-ast_typed/misc.ml @@ -255,7 +255,7 @@ end * let empty : bindings = [] * let of_list : string list -> bindings = fun x -> x * - * let rec expression : bindings -> full_environment -> expression -> bindings = fun b _env e -> + * let rec expression : bindings -> environment -> expression -> bindings = fun b _env e -> * let self = annotated_expression b in * match e with * | E_lambda l -> @@ -519,7 +519,7 @@ let get_entry (lst : program) (name : string) : expression result = in List.find_map aux lst -let program_environment (program : program) : full_environment = +let program_environment (program : program) : environment = let last_declaration = Location.unwrap List.(hd @@ rev program) in match last_declaration with | Declaration_constant { binder=_ ; expr=_ ; inline=_ ; post_env } -> post_env diff --git a/src/stages/4-ast_typed/misc.mli b/src/stages/4-ast_typed/misc.mli index 76727dbdc..ae0bb692f 100644 --- a/src/stages/4-ast_typed/misc.mli +++ b/src/stages/4-ast_typed/misc.mli @@ -70,7 +70,7 @@ val assert_literal_eq : ( literal * literal ) -> unit result *) val get_entry : program -> string -> expression result -val program_environment : program -> full_environment +val program_environment : program -> environment val p_constant : constant_tag -> p_ctor_args -> type_value val c_equation : type_value -> type_value -> string -> type_constraint diff --git a/src/stages/4-ast_typed/misc_smart.ml b/src/stages/4-ast_typed/misc_smart.ml index 679789804..a09ed2acc 100644 --- a/src/stages/4-ast_typed/misc_smart.ml +++ b/src/stages/4-ast_typed/misc_smart.ml @@ -24,7 +24,7 @@ let program_to_main : program -> string -> lambda result = fun p s -> let aux = fun _ d -> match d with | Declaration_constant {binder=_ ; expr= _ ; inline=_ ; post_env } -> post_env in - List.fold_left aux Environment.full_empty (List.map Location.unwrap p) in + List.fold_left aux Environment.empty (List.map Location.unwrap p) in let binder = Var.of_name "@contract_input" in let result = let input_expr = e_a_variable binder input_type env in @@ -47,7 +47,7 @@ module Captured_variables = struct let rec expression : bindings -> expression -> bindings result = fun b e -> expression_content b e.environment e.expression_content - and expression_content : bindings -> full_environment -> expression_content -> bindings result = fun b env ec -> + and expression_content : bindings -> environment -> expression_content -> bindings result = fun b env ec -> let self = expression b in match ec with | E_lambda l -> ok @@ Free_variables.lambda empty l diff --git a/src/stages/4-ast_typed/types.ml b/src/stages/4-ast_typed/types.ml index 047988907..195efe054 100644 --- a/src/stages/4-ast_typed/types.ml +++ b/src/stages/4-ast_typed/types.ml @@ -269,7 +269,7 @@ and declaration_constant = { binder : expression_variable ; expr : expression ; inline : bool ; - post_env : full_environment ; + post_env : environment ; } and declaration = @@ -281,7 +281,7 @@ and declaration = | Declaration_constant of declaration_constant (* | Declaration_type of (type_variable * type_expression) - | Declaration_constant of (named_expression * (full_environment * full_environment)) + | Declaration_constant of (named_expression * (environment * environment)) *) (* | Macro_declaration of macro_declaration *) @@ -289,7 +289,7 @@ and expression = { expression_content: expression_content ; location: location ; type_expression: type_expression ; - environment: full_environment ; + environment: environment ; } and map_kv = { @@ -392,11 +392,11 @@ and free_variables = expression_variable list and environment_element = { type_value: type_expression ; - source_environment: full_environment ; + source_environment: environment ; definition: environment_element_definition ; } -and environment = environment_binding list +and expression_environment = environment_binding list and environment_binding = { expr_var: expression_variable ; @@ -410,14 +410,11 @@ and type_environment_binding = { type_: type_expression ; } -(* SUBST ??? *) -and small_environment = { - expression_environment: environment ; +and environment = { + expression_environment: expression_environment ; type_environment: type_environment ; } -and full_environment = small_environment list_ne - and named_type_content = { type_name : type_variable; type_value : type_expression; diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml index cbb90084d..d7662698a 100644 --- a/src/stages/typesystem/misc.ml +++ b/src/stages/typesystem/misc.ml @@ -21,10 +21,10 @@ module Substitution = struct let%bind expr = s_expression ~substs expr in let%bind free_variables = bind_map_list (s_variable ~substs) free_variables in ok @@ T.ED_declaration {expr ; free_variables} - and s_environment : T.environment w = fun ~substs env -> + and s_expr_environment : T.expression_environment w = fun ~substs env -> bind_map_list (fun T.{expr_var=variable ; env_elt={ type_value; source_environment; definition }} -> let%bind type_value = s_type_expression ~substs type_value in - let%bind source_environment = s_full_environment ~substs source_environment in + let%bind source_environment = s_environment ~substs source_environment in let%bind definition = s_environment_element_definition ~substs definition in ok @@ T.{expr_var=variable ; env_elt={ type_value; source_environment; definition }}) env and s_type_environment : T.type_environment w = fun ~substs tenv -> @@ -32,14 +32,14 @@ module Substitution = struct let%bind type_variable = s_type_variable ~substs type_variable in let%bind type_ = s_type_expression ~substs type_ in ok @@ T.{type_variable ; type_}) tenv - and s_small_environment : T.small_environment w = fun ~substs T.{expression_environment ; type_environment} -> - let%bind expression_environment = s_environment ~substs expression_environment in + and s_environment : T.environment w = fun ~substs T.{expression_environment ; type_environment} -> + let%bind expression_environment = s_expr_environment ~substs expression_environment in let%bind type_environment = s_type_environment ~substs type_environment in ok @@ T.{ expression_environment ; type_environment } - and s_full_environment : T.full_environment w = fun ~substs (a , b) -> - let%bind a = s_small_environment ~substs a in - let%bind b = bind_map_list (s_small_environment ~substs) b in - ok (a , b) + (* and s_environment : T.environment w = fun ~substs (a , b) -> + let%bind a = s_environment ~substs a in + let%bind b = bind_map_list (s_environment ~substs) b in + ok (a , b) *) and s_variable : T.expression_variable w = fun ~substs var -> let () = ignore @@ substs in @@ -198,7 +198,7 @@ module Substitution = struct and s_expression : T.expression w = fun ~(substs:substs) { expression_content; type_expression; environment; location } -> let%bind expression_content = s_expression_content ~substs expression_content in let%bind type_expr = s_type_expression ~substs type_expression in - let%bind environment = s_full_environment ~substs environment in + let%bind environment = s_environment ~substs environment in let location = location in ok T.{ expression_content;type_expression=type_expr; environment; location } @@ -207,7 +207,7 @@ module Substitution = struct Ast_typed.Declaration_constant {binder ; expr ; inline ; post_env} -> let%bind binder = s_variable ~substs binder in let%bind expr = s_expression ~substs expr in - let%bind post_env = s_full_environment ~substs post_env in + let%bind post_env = s_environment ~substs post_env in ok @@ Ast_typed.Declaration_constant {binder; expr; inline; post_env} and s_declaration_wrap :T.declaration Location.wrap w = fun ~substs d -> diff --git a/src/test/typer_tests.ml b/src/test/typer_tests.ml index 7c22aa842..92df6e911 100644 --- a/src/test/typer_tests.ml +++ b/src/test/typer_tests.ml @@ -10,7 +10,7 @@ let int () : unit result = let open Combinators in let pre = e_int (Z.of_int 32) in let open Typer in - let e = Environment.full_empty in + let e = Environment.empty in let state = Typer.Solver.initial_state in let%bind (post , new_state) = type_expression_subst e state pre in let () = Typer.Solver.discard_state new_state in