From 688a6362516d01756afca1fb8a05859789c4702a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Fri, 6 Dec 2019 16:32:18 +0100 Subject: [PATCH] typer: cleanup --- src/main/compile/of_mini_c.ml | 6 +- src/main/compile/of_simplified.ml | 3 +- src/passes/4-typer-new/PP.ml | 57 +++++++++++ src/passes/4-typer-new/solver.ml | 116 +++++++++++++++-------- src/passes/4-typer-new/typer.ml | 38 ++------ src/passes/4-typer-old/typer.ml | 4 + src/passes/6-transpiler/transpiler.ml | 5 +- src/passes/6-transpiler/untranspiler.ml | 6 ++ src/stages/ast_simplified/PP.ml | 2 +- src/stages/ast_simplified/combinators.ml | 2 +- src/stages/ast_typed/PP.ml | 15 ++- src/stages/ast_typed/combinators.ml | 5 +- src/stages/ast_typed/combinators.mli | 2 +- src/stages/ast_typed/types.ml | 3 +- src/stages/common/PP.ml | 1 + src/stages/common/misc.ml | 8 +- src/stages/common/types.ml | 1 + src/stages/typesystem/misc.ml | 1 - src/test/typer_tests.ml | 2 +- vendors/UnionFind/Partition0.ml | 12 +-- 20 files changed, 191 insertions(+), 98 deletions(-) create mode 100644 src/passes/4-typer-new/PP.ml diff --git a/src/main/compile/of_mini_c.ml b/src/main/compile/of_mini_c.ml index be27f0f6b..46dce71a4 100644 --- a/src/main/compile/of_mini_c.ml +++ b/src/main/compile/of_mini_c.ml @@ -8,15 +8,13 @@ let compile_contract : expression -> Compiler.compiled_expression result = fun e let%bind body = Compiler.Program.translate_function_body body [] input_ty in let expr = Self_michelson.optimize body in let%bind expr_ty = Compiler.Type.Ty.type_ e.type_value in - let open! Compiler.Program in - ok { expr_ty ; expr } + ok ({ expr_ty ; expr } : Compiler.Program.compiled_expression) let compile_expression : expression -> Compiler.compiled_expression result = fun e -> let%bind expr = Compiler.Program.translate_expression e Compiler.Environment.empty in let expr = Self_michelson.optimize expr in let%bind expr_ty = Compiler.Type.Ty.type_ e.type_value in - let open! Compiler.Program in - ok { expr_ty ; expr } + ok ({ expr_ty ; expr } : Compiler.Program.compiled_expression) let aggregate_and_compile = fun program form -> let%bind aggregated = aggregate_entry program form in diff --git a/src/main/compile/of_simplified.ml b/src/main/compile/of_simplified.ml index 59df4d647..56f8721fe 100644 --- a/src/main/compile/of_simplified.ml +++ b/src/main/compile/of_simplified.ml @@ -7,6 +7,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 let apply (entry_point : string) (param : Ast_simplified.expression) : Ast_simplified.expression result = @@ -14,7 +15,7 @@ let apply (entry_point : string) (param : Ast_simplified.expression) : Ast_simpl let entry_point_var : Ast_simplified.expression = { expression = Ast_simplified.E_variable name ; location = Virtual "generated entry-point variable" } in - let applied : Ast_simplified.expression = + let applied : Ast_simplified.expression = { expression = Ast_simplified.E_application (entry_point_var, param) ; location = Virtual "generated application" } in ok applied diff --git a/src/passes/4-typer-new/PP.ml b/src/passes/4-typer-new/PP.ml new file mode 100644 index 000000000..cccd4f6bb --- /dev/null +++ b/src/passes/4-typer-new/PP.ml @@ -0,0 +1,57 @@ +open Solver +open Format + +let c_tag_to_string : Solver.Core.constant_tag -> string = function + | Solver.Core.C_arrow -> "arrow" + | Solver.Core.C_option -> "option" + | Solver.Core.C_tuple -> "tuple" + | Solver.Core.C_record -> failwith "record" + | Solver.Core.C_variant -> failwith "variant" + | Solver.Core.C_map -> "map" + | Solver.Core.C_big_map -> "big_map" + | Solver.Core.C_list -> "list" + | Solver.Core.C_set -> "set" + | Solver.Core.C_unit -> "unit" + | Solver.Core.C_bool -> "bool" + | Solver.Core.C_string -> "string" + | Solver.Core.C_nat -> "nat" + | Solver.Core.C_mutez -> "mutez" + | Solver.Core.C_timestamp -> "timestamp" + | Solver.Core.C_int -> "int" + | Solver.Core.C_address -> "address" + | Solver.Core.C_bytes -> "bytes" + | Solver.Core.C_key_hash -> "key_hash" + | Solver.Core.C_key -> "key" + | Solver.Core.C_signature -> "signature" + | Solver.Core.C_operation -> "operation" + | Solver.Core.C_contract -> "contract" + | Solver.Core.C_chain_id -> "chain_id" + +let type_constraint : _ -> type_constraint_simpl -> unit = fun ppf -> + function + |SC_Constructor { tv; c_tag; tv_list=_ } -> + let ct = c_tag_to_string c_tag in + fprintf ppf "CTOR %a %s()" Var.pp tv ct + |SC_Alias (a, b) -> fprintf ppf "Alias %a %a" Var.pp a Var.pp b + |SC_Poly _ -> fprintf ppf "Poly" + |SC_Typeclass _ -> fprintf ppf "TC" + +let all_constraints ppf ac = + fprintf ppf "[" ; + pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ";\n") type_constraint ppf ac ; + fprintf ppf "]" + +let aliases ppf (al : unionfind) = + fprintf ppf "ALIASES %a" UF.print al + +let structured_dbs : _ -> structured_dbs -> unit = fun ppf structured_dbs -> + let { all_constraints = a ; aliases = b ; _ } = structured_dbs in + fprintf ppf "STRUCTURED_DBS\n %a\n %a" all_constraints a aliases b + +let already_selected : _ -> already_selected -> unit = fun ppf already_selected -> + let _ = already_selected in + fprintf ppf "ALREADY_SELECTED" + +let state : _ -> state -> unit = fun ppf state -> + let { structured_dbs=a ; already_selected=b } = state in + fprintf ppf "STATE %a %a" structured_dbs a already_selected b diff --git a/src/passes/4-typer-new/solver.ml b/src/passes/4-typer-new/solver.ml index 2adac9659..1c0f621ed 100644 --- a/src/passes/4-typer-new/solver.ml +++ b/src/passes/4-typer-new/solver.ml @@ -64,12 +64,13 @@ module Wrap = struct P_constant (csttag, []) | T_operator (type_operator) -> let (csttag, args) = Core.(match type_operator with - | TC_option o -> (C_option, [o]) - | TC_set s -> (C_set, [s]) - | TC_map (k,v) -> (C_map, [k;v]) - | TC_big_map (k,v) -> (C_big_map, [k;v]) - | TC_list l -> (C_list, [l]) - | TC_contract c -> (C_contract, [c]) + | TC_option o -> (C_option, [o]) + | TC_set s -> (C_set, [s]) + | TC_map ( k , v ) -> (C_map, [k;v]) + | TC_big_map ( k , v) -> (C_big_map, [k;v]) + | TC_list l -> (C_list, [l]) + | TC_contract c -> (C_contract, [c]) + | TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ]) ) in P_constant (csttag, List.map type_expression_to_type_value args) @@ -96,12 +97,13 @@ module Wrap = struct P_constant (csttag,[]) | T_operator (type_name) -> let (csttag, args) = Core.(match type_name with - | TC_option o -> (C_option , [o]) - | TC_list l -> (C_list , [l]) - | TC_set s -> (C_set , [s]) - | TC_map (k,v) -> (C_map , [k;v]) - | TC_big_map (k,v) -> (C_big_map, [k;v]) - | TC_contract c -> (C_contract, [c]) + | TC_option o -> (C_option , [o]) + | TC_list l -> (C_list , [l]) + | TC_set s -> (C_set , [s]) + | TC_map ( k , v ) -> (C_map , [k;v]) + | TC_big_map ( k , v ) -> (C_big_map, [k;v]) + | TC_contract c -> (C_contract, [c]) + | TC_arrow ( arg , ret ) -> (C_arrow, [ arg ; ret ]) ) in P_constant (csttag, List.map type_expression_to_type_value_copypasted args) @@ -475,44 +477,69 @@ module UnionFindWrapper = struct in let dbs = { dbs with grouped_by_variable } in dbs - let merge_variables : type_variable -> type_variable -> structured_dbs -> structured_dbs = + + let merge_constraints : type_variable -> type_variable -> structured_dbs -> structured_dbs = fun variable_a variable_b dbs -> + (* get old representant for variable_a *) let variable_repr_a , aliases = UF.get_or_set variable_a dbs.aliases in let dbs = { dbs with aliases } in + (* get old representant for variable_b *) let variable_repr_b , aliases = UF.get_or_set variable_b dbs.aliases in let dbs = { dbs with aliases } in - let default d = function None -> d | Some y -> y in - let get_constraints ab = - TypeVariableMap.find_opt ab dbs.grouped_by_variable - |> default { constructor = [] ; poly = [] ; tc = [] } in - let constraints_a = get_constraints variable_repr_a in - let constraints_b = get_constraints variable_repr_b in - let all_constraints = { - constructor = constraints_a.constructor @ constraints_b.constructor ; - poly = constraints_a.poly @ constraints_b.poly ; - tc = constraints_a.tc @ constraints_b.tc ; - } in - let grouped_by_variable = - TypeVariableMap.add variable_repr_a all_constraints dbs.grouped_by_variable in - let dbs = { dbs with grouped_by_variable} in - let grouped_by_variable = - TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in - let dbs = { dbs with grouped_by_variable} in - dbs + + (* alias variable_a and variable_b together *) + let aliases = UF.alias variable_a variable_b dbs.aliases in + let dbs = { dbs with aliases } in + + (* Replace the two entries in grouped_by_variable by a single one *) + begin + let get_constraints ab = + match TypeVariableMap.find_opt ab dbs.grouped_by_variable with + | Some x -> x + | None -> { constructor = [] ; poly = [] ; tc = [] } in + let constraints_a = get_constraints variable_repr_a in + let constraints_b = get_constraints variable_repr_b in + let all_constraints = { + constructor = constraints_a.constructor @ constraints_b.constructor ; + poly = constraints_a.poly @ constraints_b.poly ; + tc = constraints_a.tc @ constraints_b.tc ; + } in + let grouped_by_variable = + TypeVariableMap.add variable_repr_a all_constraints dbs.grouped_by_variable in + let dbs = { dbs with grouped_by_variable} in + let grouped_by_variable = + TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in + let dbs = { dbs with grouped_by_variable} in + dbs + end end (* sub-sub component: constraint normalizer: remove dupes and give structure * right now: union-find of unification vars * later: better database-like organisation of knowledge *) -(* Each normalizer returns a *) -(* If implemented in a language with decent sets, should be 'b set not 'b list. *) +(* Each normalizer returns an updated database (after storing the + incoming constraint) and a list of constraints, used when the + normalizer rewrites the constraints e.g. into simpler ones. *) +(* TODO: If implemented in a language with decent sets, should be 'b set not 'b list. *) type ('a , 'b) normalizer = structured_dbs -> 'a -> (structured_dbs * 'b list) +(** Updates the dbs.all_constraints field when new constraints are + discovered. + + This field contains a list of all the constraints, without any form of + grouping or sorting. *) let normalizer_all_constraints : (type_constraint_simpl , type_constraint_simpl) normalizer = fun dbs new_constraint -> ({ dbs with all_constraints = new_constraint :: dbs.all_constraints } , [new_constraint]) +(** Updates the dbs.grouped_by_variable field when new constraints are + discovered. + + This field contains a map from type variables to lists of + constraints that are related to that variable (in other words, the + key appears in the equation). + *) let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_simpl) normalizer = fun dbs new_constraint -> let store_constraint tvars constraints = @@ -520,16 +547,18 @@ let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_si UnionFindWrapper.add_constraints_related_to tvar constraints dbs in List.fold_left aux dbs tvars in - let merge_constraints a b = - UnionFindWrapper.merge_variables a b dbs in let dbs = match new_constraint with SC_Constructor ({tv ; c_tag = _ ; tv_list} as c) -> store_constraint (tv :: tv_list) {constructor = [c] ; poly = [] ; tc = []} | SC_Typeclass ({tc = _ ; args} as c) -> store_constraint args {constructor = [] ; poly = [] ; tc = [c]} | SC_Poly ({tv; forall = _} as c) -> store_constraint [tv] {constructor = [] ; poly = [c] ; tc = []} - | SC_Alias (a , b) -> merge_constraints a b + | SC_Alias (a , b) -> UnionFindWrapper.merge_constraints a b dbs in (dbs , [new_constraint]) -(* Stores the first assinment ('a = ctor('b, …)) seen *) +(** Stores the first assinment ('a = ctor('b, …)) that is encountered. + + Subsequent ('a = ctor('b2, …)) with the same 'a are ignored. + + TOOD: are we checking somewhere that 'b … = 'b2 … ? *) let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) normalizer = fun dbs new_constraint -> match new_constraint with @@ -540,9 +569,14 @@ let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) nor | _ -> (dbs , [new_constraint]) +(** Evaluates a type-leval application. For now, only supports + immediate beta-reduction at the root of the type. *) let type_level_eval : type_value -> type_value * type_constraint list = fun tv -> Typesystem.Misc.Substitution.Pattern.eval_beta_root ~tv +(** Checks that a type-level application has been fully reduced. For + now, only some simple cases like applications of `forall` + failwith "internal error: shouldn't happen" (* failwith "could not reduce type-level application. Arbitrary type-level applications are not supported for now." *) @@ -552,6 +586,14 @@ let check_applied ((reduced, _new_constraints) as x) = (* TODO: at some point there may be uses of named type aliases (type foo = int; let x : foo = 42). These should be inlined. *) +(** This function converts constraints from type_constraint to + type_constraint_simpl. The former has more possible cases, and the + latter uses a more minimalistic constraint language. + + It does not modify the dbs, and only rewrites the constraint + + TODO: update the code to show that the dbs are always copied as-is + *) let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer = fun dbs new_constraint -> let insert_fresh a b = diff --git a/src/passes/4-typer-new/typer.ml b/src/passes/4-typer-new/typer.ml index 537a4c485..436f51171 100644 --- a/src/passes/4-typer-new/typer.ml +++ b/src/passes/4-typer-new/typer.ml @@ -382,6 +382,10 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result = | TC_contract c -> let%bind c = evaluate_type e c in ok @@ O.TC_contract c + | TC_arrow ( arg , ret ) -> + let%bind arg' = evaluate_type e arg in + let%bind ret' = evaluate_type e ret in + ok @@ O.TC_arrow ( arg' , ret' ) in return (T_operator (opt)) @@ -469,7 +473,7 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.e return_wrapped (e_operation o) state @@ Wrap.literal (t_operation ()) ) | E_literal (Literal_unit) -> ( - return_wrapped (e_unit) state @@ Wrap.literal (t_unit ()) + return_wrapped (e_unit ()) state @@ Wrap.literal (t_unit ()) ) | E_skip -> ( failwith "TODO: missing implementation for E_skip" @@ -954,34 +958,6 @@ let type_program_returns_state (p:I.program) : (environment * Solver.state * O.p let () = ignore (env' , state') in ok (env', state', declarations) -(* module TSMap = TMap(Solver.TypeVariable) *) - -(* let c_tag_to_string : Solver.Core.constant_tag -> string = function - * | Solver.Core.C_arrow -> "arrow" - * | Solver.Core.C_option -> "option" - * | Solver.Core.C_tuple -> "tuple" - * | Solver.Core.C_record -> failwith "record" - * | Solver.Core.C_variant -> failwith "variant" - * | Solver.Core.C_map -> "map" - * | Solver.Core.C_big_map -> "big" - * | Solver.Core.C_list -> "list" - * | Solver.Core.C_set -> "set" - * | Solver.Core.C_unit -> "unit" - * | Solver.Core.C_bool -> "bool" - * | Solver.Core.C_string -> "string" - * | Solver.Core.C_nat -> "nat" - * | Solver.Core.C_mutez -> "mutez" - * | Solver.Core.C_timestamp -> "timestamp" - * | Solver.Core.C_int -> "int" - * | Solver.Core.C_address -> "address" - * | Solver.Core.C_bytes -> "bytes" - * | Solver.Core.C_key_hash -> "key_hash" - * | Solver.Core.C_key -> "key" - * | Solver.Core.C_signature -> "signature" - * | Solver.Core.C_operation -> "operation" - * | Solver.Core.C_contract -> "contract" - * | Solver.Core.C_chain_id -> "chain_id" *) - let type_program (p : I.program) : (O.program * Solver.state) result = let%bind (env, state, program) = type_program_returns_state p in let subst_all = @@ -1064,6 +1040,10 @@ let rec untype_type_expression (t:O.type_value) : (I.type_expression) result = | O.TC_contract c-> let%bind c = untype_type_expression c in ok @@ I.TC_contract c + | O.TC_arrow ( arg , ret ) -> + let%bind arg' = untype_type_expression arg in + let%bind ret' = untype_type_expression ret in + ok @@ I.TC_arrow ( arg' , ret' ) in ok @@ I.T_operator (type_name) in diff --git a/src/passes/4-typer-old/typer.ml b/src/passes/4-typer-old/typer.ml index 1b9f90fbd..31344a358 100644 --- a/src/passes/4-typer-old/typer.ml +++ b/src/passes/4-typer-old/typer.ml @@ -375,6 +375,10 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result = | TC_contract c -> let%bind c = evaluate_type e c in ok @@ I.TC_contract c + | TC_arrow ( arg , ret ) -> + let%bind arg' = evaluate_type e arg in + let%bind ret' = evaluate_type e ret in + ok @@ I.TC_arrow ( arg' , ret' ) in return (T_operator (opt)) diff --git a/src/passes/6-transpiler/transpiler.ml b/src/passes/6-transpiler/transpiler.ml index 0cde2e3b5..0997da427 100644 --- a/src/passes/6-transpiler/transpiler.ml +++ b/src/passes/6-transpiler/transpiler.ml @@ -181,6 +181,7 @@ let rec transpile_type (t:AST.type_value) : type_value result = ok (T_pair ((None, a), (None, b))) in Append_tree.fold_ne transpile_type aux node + | T_operator (TC_arrow (param, result)) | T_arrow (param, result) -> ( let%bind param' = transpile_type param in let%bind result' = transpile_type result in @@ -320,7 +321,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re | E_tuple_accessor (tpl, ind) -> ( let%bind ty' = transpile_type tpl.type_annotation in let%bind ty_lst = - trace_strong (corner_case ~loc:__LOC__ "not a tuple") @@ + trace_strong (corner_case ~loc:__LOC__ "transpiler: E_tuple_accessor: not a tuple") @@ get_t_tuple tpl.type_annotation in let%bind ty'_lst = bind_map_list transpile_type ty_lst in let%bind path = @@ -509,7 +510,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re match cur with | Access_tuple ind -> ( let%bind ty_lst = - trace_strong (corner_case ~loc:__LOC__ "not a tuple") @@ + trace_strong (corner_case ~loc:__LOC__ "transpiler: E_assign: Access_tuple: not a tuple") @@ AST.Combinators.get_t_tuple prev in let%bind ty'_lst = bind_map_list transpile_type ty_lst in let%bind path = tuple_access_to_lr ty' ty'_lst ind in diff --git a/src/passes/6-transpiler/untranspiler.ml b/src/passes/6-transpiler/untranspiler.ml index a548003b0..f75a31323 100644 --- a/src/passes/6-transpiler/untranspiler.ml +++ b/src/passes/6-transpiler/untranspiler.ml @@ -196,6 +196,12 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression ) | TC_contract _ -> fail @@ bad_untranspile "contract" v + | TC_arrow _ -> ( + let%bind n = + trace_strong (wrong_mini_c_value "lambda as string" v) @@ + get_string v in + return (E_literal (Literal_string n)) + ) ) | T_sum m -> let lst = kv_list_of_cmap m in diff --git a/src/stages/ast_simplified/PP.ml b/src/stages/ast_simplified/PP.ml index 768d6d12a..6f3a2ab50 100644 --- a/src/stages/ast_simplified/PP.ml +++ b/src/stages/ast_simplified/PP.ml @@ -18,7 +18,7 @@ and type_expression ppf (te: type_expression) : unit = te' ppf te.type_expression' let rec expression ppf (e:expression) = match e.expression with - | E_literal l -> literal ppf l + | E_literal l -> fprintf ppf "%a" literal l | E_variable n -> fprintf ppf "%a" name n | E_application (f, arg) -> fprintf ppf "(%a)@(%a)" expression f expression arg | E_constructor (c, ae) -> fprintf ppf "%a(%a)" constructor c expression ae diff --git a/src/stages/ast_simplified/combinators.ml b/src/stages/ast_simplified/combinators.ml index 1077f991a..e103465da 100644 --- a/src/stages/ast_simplified/combinators.ml +++ b/src/stages/ast_simplified/combinators.ml @@ -203,7 +203,7 @@ let get_e_list = fun t -> let get_e_tuple = fun t -> match t with | E_tuple lst -> ok lst - | _ -> simple_fail "not a tuple" + | _ -> simple_fail "ast_simplified: get_e_tuple: not a tuple" let extract_pair : expression -> (expression * expression) result = fun e -> match e.expression with diff --git a/src/stages/ast_typed/PP.ml b/src/stages/ast_typed/PP.ml index 3fc3c2483..b1639462e 100644 --- a/src/stages/ast_typed/PP.ml +++ b/src/stages/ast_typed/PP.ml @@ -15,13 +15,12 @@ and type_value ppf (tv:type_value) : unit = let rec annotated_expression ppf (ae:annotated_expression) : unit = match ae.type_annotation.simplified with - | Some _ -> fprintf ppf "@[%a:%a@]" expression ae.expression type_value ae.type_annotation - | _ -> fprintf ppf "@[%a@]" expression ae.expression + | _ -> fprintf ppf "@[%a:%a@]" expression ae.expression type_value ae.type_annotation and lambda ppf l = let ({ binder ; body } : lambda) = l in - fprintf ppf "lambda (%a) -> %a" - name binder + fprintf ppf "(lambda (%a) -> %a)" + name binder annotated_expression body and option_inline ppf inline = @@ -33,9 +32,9 @@ and option_inline ppf inline = and expression ppf (e:expression) : unit = match e with | E_literal l -> Stage_common.PP.literal ppf l - | E_constant (b, lst) -> fprintf ppf "%a(%a)" constant b (list_sep_d annotated_expression) lst - | E_constructor (c, lst) -> fprintf ppf "%a(%a)" constructor c annotated_expression lst - | E_variable a -> fprintf ppf "%a" name a + | E_constant (b, lst) -> fprintf ppf "(e_constant %a(%a))" constant b (list_sep_d annotated_expression) lst + | E_constructor (c, lst) -> fprintf ppf "(e_constructor %a(%a))" constructor c annotated_expression lst + | E_variable a -> fprintf ppf "(e_var %a)" name a | E_application (f, arg) -> fprintf ppf "(%a) (%a)" annotated_expression f annotated_expression arg | E_lambda l -> fprintf ppf "%a" lambda l | E_tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i @@ -50,7 +49,7 @@ and expression ppf (e:expression) : unit = | E_look_up (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i | E_matching (ae, m) -> fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m - | E_sequence (a , b) -> fprintf ppf "%a ; %a" annotated_expression a annotated_expression b + | E_sequence (a , b) -> fprintf ppf "(e_seq %a ; %a)" annotated_expression a annotated_expression b | E_loop (expr , body) -> fprintf ppf "while %a { %a }" annotated_expression expr annotated_expression body | E_assign (name , path , expr) -> fprintf ppf "%a.%a := %a" diff --git a/src/stages/ast_typed/combinators.ml b/src/stages/ast_typed/combinators.ml index 8ebe2b89d..ec3cc0f28 100644 --- a/src/stages/ast_typed/combinators.ml +++ b/src/stages/ast_typed/combinators.ml @@ -160,6 +160,7 @@ let get_t_pair (t:type_value) : (type_value * type_value) result = match t.type_ let get_t_function (t:type_value) : (type_value * type_value) result = match t.type_value' with | T_arrow (a,r) -> ok (a,r) + | T_operator (TC_arrow (a , b)) -> ok (a , b) | _ -> fail @@ Errors.not_a_x_type "function" t () let get_t_sum (t:type_value) : type_value constructor_map result = match t.type_value' with @@ -257,7 +258,7 @@ let e_none : expression = E_constant (C_NONE, []) let e_map lst : expression = E_map lst -let e_unit : expression = E_literal (Literal_unit) +let e_unit () : expression = E_literal (Literal_unit) let e_int n : expression = E_literal (Literal_int n) let e_nat n : expression = E_literal (Literal_nat n) let e_mutez n : expression = E_literal (Literal_mutez n) @@ -279,7 +280,7 @@ let e_list lst : expression = E_list lst let e_let_in binder inline rhs result = E_let_in { binder ; rhs ; result; inline } let e_tuple lst : expression = E_tuple lst -let e_a_unit = make_a_e e_unit (t_unit ()) +let e_a_unit = make_a_e (e_unit ()) (t_unit ()) let e_a_int n = make_a_e (e_int n) (t_int ()) let e_a_nat n = make_a_e (e_nat n) (t_nat ()) let e_a_mutez n = make_a_e (e_mutez n) (t_mutez ()) diff --git a/src/stages/ast_typed/combinators.mli b/src/stages/ast_typed/combinators.mli index f9cd7d93d..66829d1b6 100644 --- a/src/stages/ast_typed/combinators.mli +++ b/src/stages/ast_typed/combinators.mli @@ -113,7 +113,7 @@ val ez_e_record : ( string * annotated_expression ) list -> expression val e_some : value -> expression val e_none : expression val e_map : ( value * value ) list -> expression -val e_unit : expression +val e_unit : unit -> expression val e_int : int -> expression val e_nat : int -> expression val e_mutez : int -> expression diff --git a/src/stages/ast_typed/types.ml b/src/stages/ast_typed/types.ml index 50d2060ed..7da528e81 100644 --- a/src/stages/ast_typed/types.ml +++ b/src/stages/ast_typed/types.ml @@ -41,6 +41,7 @@ and named_expression = { and ae = annotated_expression and type_value' = type_value type_expression' + and type_value = { type_value' : type_value'; simplified : S.type_expression option ; (* If we have the simplified this AST fragment comes from, it is stored here, for easier untyping. *) @@ -77,7 +78,7 @@ and 'a expression' = | E_application of (('a) * ('a)) | E_lambda of lambda | E_let_in of let_in - (* Tuple *) + (* Tuple, TODO: remove tuples and use records with integer keys instead *) | E_tuple of ('a) list | E_tuple_accessor of (('a) * int) (* Access n'th tuple's element *) (* Sum *) diff --git a/src/stages/common/PP.ml b/src/stages/common/PP.ml index 7d42e0c7e..7600f8064 100644 --- a/src/stages/common/PP.ml +++ b/src/stages/common/PP.ml @@ -178,6 +178,7 @@ and type_operator : type a . (formatter -> a -> unit) -> formatter -> a type_ope | TC_map (k, v) -> Format.asprintf "Map (%a,%a)" f k f v | TC_big_map (k, v) -> Format.asprintf "Big Map (%a,%a)" f k f v | TC_contract (c) -> Format.asprintf "Contract (%a)" f c + | TC_arrow (a , b) -> Format.asprintf "TC_Arrow (%a,%a)" f a f b in fprintf ppf "(TO_%s)" s diff --git a/src/stages/common/misc.ml b/src/stages/common/misc.ml index 7f38acf62..455477861 100644 --- a/src/stages/common/misc.ml +++ b/src/stages/common/misc.ml @@ -7,7 +7,8 @@ let map_type_operator f = function | TC_list x -> TC_list (f x) | TC_set x -> TC_set (f x) | TC_map (x , y) -> TC_map (f x , f y) - | TC_big_map (x , y)-> TC_big_map (f x , f y) + | TC_big_map (x , y) -> TC_big_map (f x , f y) + | TC_arrow (x , y) -> TC_arrow (f x , f y) let bind_map_type_operator f = function TC_contract x -> let%bind x = f x in ok @@ TC_contract x @@ -15,7 +16,8 @@ let bind_map_type_operator f = function | TC_list x -> let%bind x = f x in ok @@ TC_list x | TC_set x -> let%bind x = f x in ok @@ TC_set x | TC_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_map (x , y) - | TC_big_map (x , y)-> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y) + | TC_big_map (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_big_map (x , y) + | TC_arrow (x , y) -> let%bind x = f x in let%bind y = f y in ok @@ TC_arrow (x , y) let type_operator_name = function TC_contract _ -> "TC_contract" @@ -24,6 +26,7 @@ let type_operator_name = function | TC_set _ -> "TC_set" | TC_map _ -> "TC_map" | TC_big_map _ -> "TC_big_map" + | TC_arrow _ -> "TC_arrow" let type_expression'_of_string = function | "TC_contract" , [x] -> ok @@ T_operator(TC_contract x) @@ -61,6 +64,7 @@ let string_of_type_operator = function | TC_set x -> "TC_set" , [x] | TC_map (x , y) -> "TC_map" , [x ; y] | TC_big_map (x , y) -> "TC_big_map" , [x ; y] + | TC_arrow (x , y) -> "TC_arrow" , [x ; y] let string_of_type_constant = function | TC_unit -> "TC_unit", [] diff --git a/src/stages/common/types.ml b/src/stages/common/types.ml index b25eb80a5..2cb20d6d5 100644 --- a/src/stages/common/types.ml +++ b/src/stages/common/types.ml @@ -96,6 +96,7 @@ and 'a type_operator = | TC_set of 'a | TC_map of 'a * 'a | TC_big_map of 'a * 'a + | TC_arrow of 'a * 'a type type_base = | Base_unit diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml index b95c603fc..31a9168ee 100644 --- a/src/stages/typesystem/misc.ml +++ b/src/stages/typesystem/misc.ml @@ -3,7 +3,6 @@ open Core let pair_map = fun f (x , y) -> (f x , f y) module Substitution = struct - module Pattern = struct open Trace diff --git a/src/test/typer_tests.ml b/src/test/typer_tests.ml index 0fc687385..ec0e1c725 100644 --- a/src/test/typer_tests.ml +++ b/src/test/typer_tests.ml @@ -37,7 +37,7 @@ module TestExpressions = struct module E = O let unit () : unit result = test_expression I.(e_unit ()) O.(t_unit ()) - let int () : unit result = test_expression I.(e_int 32) O.(t_int ()) + let int () : unit result = test_expression I.(e_int 32) O.(t_int ()) let bool () : unit result = test_expression I.(e_bool true) O.(t_bool ()) let string () : unit result = test_expression I.(e_string "s") O.(t_string ()) let bytes () : unit result = diff --git a/vendors/UnionFind/Partition0.ml b/vendors/UnionFind/Partition0.ml index cd8b26ffc..33616080b 100644 --- a/vendors/UnionFind/Partition0.ml +++ b/vendors/UnionFind/Partition0.ml @@ -38,12 +38,10 @@ module Make (Item: Partition.Item) = (* Printing *) - let print (p: partition) = - let buffer = Buffer.create 80 in + let print ppf p = let print src dst = - let link = - Printf.sprintf "%s -> %s\n" - (Item.to_string src) (Item.to_string dst) - in Buffer.add_string buffer link - in (ItemMap.iter print p; buffer) + Format.fprintf ppf "%s -> %s (%s)\n" + (Item.to_string src) (Item.to_string dst) (Item.to_string (repr src p)) + in ItemMap.iter print p + end