From f657c71753d0570039636d379991c79a7cb0f3cd Mon Sep 17 00:00:00 2001 From: Pierre-Emmanuel Wulfman Date: Fri, 27 Sep 2019 14:55:09 +0200 Subject: [PATCH] Merge done and repo build with no error --- src/passes/4-typer/dune | 1 + src/passes/4-typer/solver.ml | 716 ++++++++++++++++++ src/passes/4-typer/typer.ml | 16 + src/passes/4-typer/typer.ml.old | 879 +++++++++++++++++++++++ src/passes/operators/dune | 1 + src/passes/operators/operators.ml | 60 ++ src/typesystem/core.ml | 60 ++ src/typesystem/dune | 14 + src/typesystem/shorthands.ml | 62 ++ src/typesystem/typesystem.ml | 2 + src/union_find/.PartitionMain.tag | 0 src/union_find/.links | 1 + src/union_find/LICENSE | 21 + src/union_find/Makefile.cfg | 4 + src/union_find/Partition.mli | 64 ++ src/union_find/Partition0.ml | 47 ++ src/union_find/Partition1.ml | 69 ++ src/union_find/Partition2.ml | 115 +++ src/union_find/Partition3.ml | 86 +++ src/union_find/PartitionMain.ml | 40 ++ src/union_find/README.md | 39 + src/union_find/build.sh | 14 + src/union_find/clean.sh | 3 + src/union_find/dune | 16 + src/union_find/union_find.ml | 2 + vendors/ligo-utils/simple-utils/trace.ml | 1 + 26 files changed, 2333 insertions(+) create mode 100644 src/passes/4-typer/solver.ml create mode 100644 src/passes/4-typer/typer.ml.old create mode 100644 src/typesystem/core.ml create mode 100644 src/typesystem/dune create mode 100644 src/typesystem/shorthands.ml create mode 100644 src/typesystem/typesystem.ml create mode 100644 src/union_find/.PartitionMain.tag create mode 100644 src/union_find/.links create mode 100644 src/union_find/LICENSE create mode 100644 src/union_find/Makefile.cfg create mode 100644 src/union_find/Partition.mli create mode 100644 src/union_find/Partition0.ml create mode 100644 src/union_find/Partition1.ml create mode 100644 src/union_find/Partition2.ml create mode 100644 src/union_find/Partition3.ml create mode 100644 src/union_find/PartitionMain.ml create mode 100644 src/union_find/README.md create mode 100755 src/union_find/build.sh create mode 100755 src/union_find/clean.sh create mode 100644 src/union_find/dune create mode 100644 src/union_find/union_find.ml diff --git a/src/passes/4-typer/dune b/src/passes/4-typer/dune index 0ee58cc43..ec35ab2ce 100644 --- a/src/passes/4-typer/dune +++ b/src/passes/4-typer/dune @@ -7,6 +7,7 @@ ast_simplified ast_typed operators + union_find ) (preprocess (pps ppx_let) diff --git a/src/passes/4-typer/solver.ml b/src/passes/4-typer/solver.ml new file mode 100644 index 000000000..890d067e3 --- /dev/null +++ b/src/passes/4-typer/solver.ml @@ -0,0 +1,716 @@ +open Trace + +module Core = Typesystem.Core + +module Wrap = struct + module I = Ast_simplified + module O = Core + + type constraints = O.type_constraint list + + (* let add_type state t = *) + (* let constraints = Wrap.variable type_name t in *) + (* let%bind state' = aggregate_constraints state constraints in *) + (* ok state' in *) + (* let return_add_type ?(state = state) expr t = *) + (* let%bind state' = add_type state t in *) + (* return expr state' in *) + + let rec type_expression_to_type_value : I.type_expression -> O.type_value = fun te -> + match te with + | T_tuple types -> + P_constant (C_tuple, List.map type_expression_to_type_value types) + | T_sum kvmap -> + P_constant (C_variant, Map.String.to_list @@ Map.String.map type_expression_to_type_value kvmap) + | T_record kvmap -> + P_constant (C_record, Map.String.to_list @@ Map.String.map type_expression_to_type_value kvmap) + | T_function (arg , ret) -> + P_constant (C_arrow, List.map type_expression_to_type_value [ arg ; ret ]) + | T_variable type_name -> P_variable type_name + | T_constant (type_name , args) -> + let csttag = Core.(match type_name with + | "arrow" -> C_arrow + | "option" -> C_option + | "tuple" -> C_tuple + | "map" -> C_map + | "list" -> C_list + | "set" -> C_set + | "unit" -> C_unit + | "bool" -> C_bool + | "string" -> C_string + | _ -> failwith "TODO") + in + P_constant (csttag, List.map type_expression_to_type_value args) + + (** TODO *) + let type_declaration : I.declaration -> constraints = fun td -> + match td with + | Declaration_type (name , te) -> + let pattern = type_expression_to_type_value te in + [C_equation (P_variable (name) , pattern)] (* TODO: this looks wrong. If this is a type declaration, it should not set any constraints. *) + | Declaration_constant (name, te, _) ->( + match te with + | Some (exp) -> + let pattern = type_expression_to_type_value exp in + [C_equation (P_variable (name) , pattern)] (* TODO: this looks wrong. If this is a type declaration, it should not set any constraints. *) + | None -> + (** TODO *) + [] + ) + + (* TODO: this should be renamed to failwith_ *) + let failwith : unit -> (constraints * O.type_variable) = fun () -> + let type_name = Core.fresh_type_variable () in + [] , type_name + + let variable : I.name -> I.type_expression -> (constraints * O.type_variable) = fun _name expr -> + let pattern = type_expression_to_type_value expr in + let type_name = Core.fresh_type_variable () in + [C_equation (P_variable (type_name) , pattern)] , type_name + + let literal : I.type_expression -> (constraints * O.type_variable) = fun t -> + let pattern = type_expression_to_type_value t in + let type_name = Core.fresh_type_variable () in + [C_equation (P_variable (type_name) , pattern)] , type_name + + (* + let literal_bool : unit -> (constraints * O.type_variable) = fun () -> + let pattern = type_expression_to_type_value I.t_bool in + let type_name = Core.fresh_type_variable () in + [C_equation (P_variable (type_name) , pattern)] , type_name + + let literal_string : unit -> (constraints * O.type_variable) = fun () -> + let pattern = type_expression_to_type_value I.t_string in + let type_name = Core.fresh_type_variable () in + [C_equation (P_variable (type_name) , pattern)] , type_name + *) + + let tuple : I.type_expression list -> (constraints * O.type_variable) = fun tys -> + let patterns = List.map type_expression_to_type_value tys in + let pattern = O.(P_constant (C_tuple , patterns)) in + let type_name = Core.fresh_type_variable () in + [C_equation (P_variable (type_name) , pattern)] , type_name + + (* let t_tuple = ('label:int, 'v) … -> record ('label : 'v) … *) + (* let t_constructor = ('label:string, 'v) -> variant ('label : 'v) *) + (* let t_record = ('label:string, 'v) … -> record ('label : 'v) … with independent choices for each 'label and 'v *) + (* let t_variable = t_of_var_in_env *) + (* let t_access_int = record ('label:int , 'v) … -> 'label:int -> 'v *) + (* let t_access_string = record ('label:string , 'v) … -> 'label:string -> 'v *) + + module Prim_types = struct + open Typesystem.Shorthands + + let t_cons = forall "v" @@ fun v -> v --> list v --> list v (* was: list *) + let t_setcons = forall "v" @@ fun v -> v --> set v --> set v (* was: set *) + let t_mapcons = forall2 "k" "v" @@ fun k v -> (k * v) --> map k v --> map k v (* was: map *) + let t_failwith = forall "a" @@ fun a -> a + (* let t_literal_t = t *) + let t_literal_bool = bool + let t_literal_string = string + let t_access_map = forall2 "k" "v" @@ fun k v -> map k v --> k --> v + let t_application = forall2 "a" "b" @@ fun a b -> (a --> b) --> a --> b + let t_look_up = forall2 "ind" "v" @@ fun ind v -> map ind v --> ind --> option v + let t_sequence = forall "b" @@ fun b -> unit --> b --> b + let t_loop = bool --> unit --> unit + end + + (* TODO: I think we should take an I.expression for the base+label *) + let access_label ~base ~label : (constraints * O.type_variable) = + let base' = type_expression_to_type_value base in + let expr_type = Core.fresh_type_variable () in + [O.C_access_label (base' , label , expr_type)] , expr_type + + let access_int ~base ~index = access_label ~base ~label:(L_int index) + let access_string ~base ~property = access_label ~base ~label:(L_string property) + + let access_map : base:I.type_expression -> key:I.type_expression -> (constraints * O.type_variable) = + let mk_map_type key_type element_type = + O.P_constant O.(C_map , [P_variable element_type; P_variable key_type]) in + fun ~base ~key -> + let key_type = Core.fresh_type_variable () in + let element_type = Core.fresh_type_variable () in + let base' = type_expression_to_type_value base in + let key' = type_expression_to_type_value key in + let base_expected = mk_map_type key_type element_type in + let expr_type = Core.fresh_type_variable () in + O.[C_equation (base' , base_expected); + C_equation (key' , P_variable key_type); + C_equation (P_variable expr_type , P_variable element_type)] , expr_type + + let constructor + : I.type_expression -> I.type_expression -> I.type_expression -> (constraints * O.type_variable) + = fun t_arg c_arg sum -> + let t_arg = type_expression_to_type_value t_arg in + let c_arg = type_expression_to_type_value c_arg in + let sum = type_expression_to_type_value sum in + let whole_expr = Core.fresh_type_variable () in + [ + C_equation (P_variable (whole_expr) , sum) ; + C_equation (t_arg , c_arg) + ] , whole_expr + + let record : I.type_expression I.type_name_map -> (constraints * O.type_variable) = fun fields -> + let record_type = type_expression_to_type_value (I.t_record fields) in + let whole_expr = Core.fresh_type_variable () in + [C_equation (P_variable whole_expr , record_type)] , whole_expr + + let collection : O.constant_tag -> I.type_expression list -> (constraints * O.type_variable) = + fun ctor element_tys -> + let elttype = O.P_variable (Core.fresh_type_variable ()) in + let aux elt = + let elt' = type_expression_to_type_value elt + in O.C_equation (elttype , elt') in + let equations = List.map aux element_tys in + let whole_expr = Core.fresh_type_variable () in + O.[ + C_equation (P_variable whole_expr , O.P_constant (ctor , [elttype])) + ] @ equations , whole_expr + + let list = collection O.C_list + let set = collection O.C_set + + let map : (I.type_expression * I.type_expression) list -> (constraints * O.type_variable) = + fun kv_tys -> + let k_type = O.P_variable (Core.fresh_type_variable ()) in + let v_type = O.P_variable (Core.fresh_type_variable ()) in + let aux_k (k , _v) = + let k' = type_expression_to_type_value k in + O.C_equation (k_type , k') in + let aux_v (_k , v) = + let v' = type_expression_to_type_value v in + O.C_equation (v_type , v') in + let equations_k = List.map aux_k kv_tys in + let equations_v = List.map aux_v kv_tys in + let whole_expr = Core.fresh_type_variable () in + O.[ + C_equation (P_variable whole_expr , O.P_constant (C_map , [k_type ; v_type])) + ] @ equations_k @ equations_v , whole_expr + + let application : I.type_expression -> I.type_expression -> (constraints * O.type_variable) = + fun f arg -> + let whole_expr = Core.fresh_type_variable () in + let f' = type_expression_to_type_value f in + let arg' = type_expression_to_type_value arg in + O.[ + C_equation (f' , P_constant (C_arrow , [arg' ; P_variable whole_expr])) + ] , whole_expr + + let look_up : I.type_expression -> I.type_expression -> (constraints * O.type_variable) = + fun ds ind -> + let ds' = type_expression_to_type_value ds in + let ind' = type_expression_to_type_value ind in + let whole_expr = Core.fresh_type_variable () in + let v = Core.fresh_type_variable () in + O.[ + C_equation (ds' , P_constant (C_map, [ind' ; P_variable v])) ; + C_equation (P_variable whole_expr , P_constant (C_option , [P_variable v])) + ] , whole_expr + + let sequence : I.type_expression -> I.type_expression -> (constraints * O.type_variable) = + fun a b -> + let a' = type_expression_to_type_value a in + let b' = type_expression_to_type_value b in + let whole_expr = Core.fresh_type_variable () in + O.[ + C_equation (a' , P_constant (C_unit , [])) ; + C_equation (b' , P_variable whole_expr) + ] , whole_expr + + let loop : I.type_expression -> I.type_expression -> (constraints * O.type_variable) = + fun expr body -> + let expr' = type_expression_to_type_value expr in + let body' = type_expression_to_type_value body in + let whole_expr = Core.fresh_type_variable () in + O.[ + C_equation (expr' , P_constant (C_bool , [])) ; + C_equation (body' , P_constant (C_unit , [])) ; + C_equation (P_variable whole_expr , P_constant (C_unit , [])) + ] , whole_expr + + let let_in : I.type_expression -> I.type_expression option -> I.type_expression -> (constraints * O.type_variable) = + fun rhs rhs_tv_opt result -> + let rhs' = type_expression_to_type_value rhs in + let result' = type_expression_to_type_value result in + let rhs_tv_opt' = match rhs_tv_opt with + None -> [] + | Some annot -> O.[C_equation (rhs' , type_expression_to_type_value annot)] in + let whole_expr = Core.fresh_type_variable () in + O.[ + C_equation (result' , P_variable whole_expr) + ] @ rhs_tv_opt', whole_expr + + let assign : I.type_expression -> I.type_expression -> (constraints * O.type_variable) = + fun v e -> + let v' = type_expression_to_type_value v in + let e' = type_expression_to_type_value e in + let whole_expr = Core.fresh_type_variable () in + O.[ + C_equation (v' , e') ; + C_equation (P_variable whole_expr , P_constant (C_unit , [])) + ] , whole_expr + + let annotation : I.type_expression -> I.type_expression -> (constraints * O.type_variable) = + fun e annot -> + let e' = type_expression_to_type_value e in + let annot' = type_expression_to_type_value annot in + let whole_expr = Core.fresh_type_variable () in + O.[ + C_equation (e' , annot') ; + C_equation (e' , P_variable whole_expr) + ] , whole_expr + + let matching : I.type_expression list -> (constraints * O.type_variable) = + fun es -> + let whole_expr = Core.fresh_type_variable () in + let type_values = (List.map type_expression_to_type_value es) in + let cs = List.map (fun e -> O.C_equation (P_variable whole_expr , e)) type_values + in cs, whole_expr + + let fresh_binder () = + Core.fresh_type_variable () + + let lambda + : I.type_expression -> + I.type_expression option -> + I.type_expression option -> + (constraints * O.type_variable) = + fun fresh arg body -> + let whole_expr = Core.fresh_type_variable () in + let unification_arg = Core.fresh_type_variable () in + let unification_body = Core.fresh_type_variable () in + let arg' = match arg with + None -> [] + | Some arg -> O.[C_equation (P_variable unification_arg , type_expression_to_type_value arg)] in + let body' = match body with + None -> [] + | Some body -> O.[C_equation (P_variable unification_body , type_expression_to_type_value body)] + in O.[ + C_equation (type_expression_to_type_value fresh , P_variable unification_arg) ; + C_equation (P_variable whole_expr , + P_constant (C_arrow , [P_variable unification_arg ; + P_variable unification_body])) + ] @ arg' @ body' , whole_expr + +end + +(* begin unionfind *) + +module TV = +struct + type t = Core.type_variable + let compare = String.compare + let to_string = (fun s -> s) +end + +module UF = Union_find.Partition0.Make(TV) + +type unionfind = UF.t + +let empty = UF.empty (* DEMO *) +let representative_toto = UF.repr "toto" empty (* DEMO *) +let merge x y = UF.equiv x y (* DEMO *) + +(* end unionfind *) + +(* representant for an equivalence class of type variables *) +module TypeVariable = String +module TypeVariableMap = Map.Make(TypeVariable) + + +(* + +Components: +* assignments (passive data structure). + Now: just a map from unification vars to types (pb: what about partial types?) + maybe just local assignments (allow only vars as children of pair(α,β)) +* constraint propagation: (buch of constraints) → (new constraints * assignments) + * sub-component: constraint selector (worklist / dynamic queries) + * sub-sub component: constraint normalizer: remove dupes and give structure + right now: union-find of unification vars + later: better database-like organisation of knowledge + * sub-sub component: lazy selector (don't re-try all selectors every time) + For now: just re-try everytime + * sub-component: propagation rule + For now: break pair(a, b) = pair(c, d) into a = c, b = d +* generalizer + For now: ? + +Workflow: + Start with empty assignments and structured database + Receive a new constraint + For each normalizer: + Use the pre-selector to see if it can be applied + Apply the normalizer, get some new items to insert in the structured database + For each propagator: + Use the selector to query the structured database and see if it can be applied + Apply the propagator, get some new constraints and assignments + Add the new assignments to the data structure. + + At some point (when?) + For each generalizer: + Use the generalizer's selector to see if it can be applied + Apply the generalizer to produce a new type, possibly with some ∀s injected + +*) + +open Core + +type structured_dbs = { + all_constraints : type_constraint_simpl list ; + aliases : unionfind ; + (* assignments (passive data structure). + Now: just a map from unification vars to types (pb: what about partial types?) + maybe just local assignments (allow only vars as children of pair(α,β)) *) + assignments : c_constructor_simpl TypeVariableMap.t ; + grouped_by_variable : constraints TypeVariableMap.t ; (* map from (unionfind) variables to constraints containing them *) + cycle_detection_toposort : unit ; (* example of structured db that we'll add later *) +} + +and constraints = { + constructor : c_constructor_simpl list ; + tc : c_typeclass_simpl list ; +} + +and c_constructor_simpl = { + tv : type_variable; + c_tag : constant_tag; + tv_list : type_variable list; +} +(* copy-pasted from core.ml *) +and c_const = (type_variable * type_value) +and c_equation = (type_value * type_value) +and c_typeclass_simpl = { + tc : typeclass ; + args : type_variable list ; +} +and type_constraint_simpl = + SC_Constructor of c_constructor_simpl (* α = ctor(β, …) *) + | SC_Alias of (type_variable * type_variable) (* α = β *) + | SC_Typeclass of c_typeclass_simpl (* TC(α, …) *) + +module UnionFindWrapper = struct + (* TODO: API for the structured db, to access it modulo unification variable aliases. *) + let get_constraints_related_to : type_variable -> structured_dbs -> constraints = + fun variable dbs -> + let variable , aliases = UF.get_or_set variable dbs.aliases in + let dbs = { dbs with aliases } in + match TypeVariableMap.find_opt variable dbs.grouped_by_variable with + Some l -> l + | None -> { + constructor = [] ; + tc = [] ; + } + let add_constraints_related_to : type_variable -> constraints -> structured_dbs -> structured_dbs = + fun variable c dbs -> + (* let (variable_repr , _height) , aliases = UF.get_or_set variable dbs.aliases in + let dbs = { dbs with aliases } in *) + let variable_repr , aliases = UF.get_or_set variable dbs.aliases in + let dbs = { dbs with aliases } in + let grouped_by_variable = TypeVariableMap.update variable_repr (function + None -> Some c + | Some x -> Some { + constructor = c.constructor @ x.constructor ; + tc = c.tc @ x.tc ; + }) + dbs.grouped_by_variable + in + let dbs = { dbs with grouped_by_variable } in + dbs + let merge_variables : type_variable -> type_variable -> structured_dbs -> structured_dbs = + fun variable_a variable_b dbs -> + let variable_repr_a , aliases = UF.get_or_set variable_a dbs.aliases in + let dbs = { dbs with aliases } in + 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 = [] ; tc = [] } in + let constraints_a = get_constraints variable_repr_a in + let constraints_b = get_constraints variable_repr_b in + let all_constraints = { + (* TODO: should be a Set.union, not @ *) + constructor = constraints_a.constructor @ constraints_b.constructor ; + 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 + +(* 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 *) +type ('a , 'b) normalizer = structured_dbs -> 'a -> (structured_dbs * 'b list) + +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]) + +let normalizer_grouped_by_variable : (type_constraint_simpl , type_constraint_simpl) normalizer = + fun dbs new_constraint -> + let store_constraint tvars constraints = + let aux dbs (tvar : type_variable) = + 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] ; tc = []} + | SC_Typeclass ({tc = _ ; args} as c) -> store_constraint args {constructor = [] ; tc = [c]} + | SC_Alias (a , b) -> merge_constraints a b + in (dbs , [new_constraint]) + +(* Stores the first assinment ('a = ctor('b, …)) seen *) +let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) normalizer = + fun dbs new_constraint -> + match new_constraint with + | SC_Constructor ({tv ; c_tag = _ ; tv_list = _} as c) -> + let assignments = TypeVariableMap.update tv (function None -> Some c | e -> e) dbs.assignments in + let dbs = {dbs with assignments} in + (dbs , [new_constraint]) + | _ -> + (dbs , [new_constraint]) + +let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer = + fun dbs new_constraint -> + match new_constraint with + | C_equation (P_forall _, P_forall _) -> failwith "TODO" + | C_equation ((P_forall _ as a), (P_variable _ as b)) -> normalizer_simpl dbs (C_equation (b , a)) + | C_equation (P_forall _, P_constant _) -> failwith "TODO" + | C_equation (P_variable _, P_forall _) -> failwith "TODO" + | C_equation (P_variable a, P_variable b) -> (dbs , [SC_Alias (a, b)]) + | C_equation (P_variable a, P_constant (c_tag, args)) -> + let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in + let fresh_eqns = List.map (fun (v,t) -> C_equation (P_variable v, t)) (List.combine fresh_vars args) in + let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in + (dbs , [SC_Constructor {tv=a;c_tag;tv_list=fresh_vars}] @ List.flatten recur) + | C_equation (P_constant _, P_forall _) -> failwith "TODO" + | C_equation ((P_constant _ as a), (P_variable _ as b)) -> normalizer_simpl dbs (C_equation (b , a)) + | C_equation ((P_constant _ as a), (P_constant _ as b)) -> + (* break down c(args) = c'(args') into 'a = c(args) and 'a = c'(args') *) + let fresh = Core.fresh_type_variable () in + let (dbs , cs1) = normalizer_simpl dbs (C_equation (P_variable fresh, a)) in + let (dbs , cs2) = normalizer_simpl dbs (C_equation (P_variable fresh, b)) in + (dbs , cs1 @ cs2) (* TODO: O(n) concatenation! *) + | C_typeclass (args, tc) -> + (* break down TC(args) into TC('a, …) and ('a = arg) … *) + let fresh_vars = List.map (fun _ -> Core.fresh_type_variable ()) args in + let fresh_eqns = List.map (fun (v,t) -> C_equation (P_variable v, t)) (List.combine fresh_vars args) in + let (dbs , recur) = List.fold_map_acc normalizer_simpl dbs fresh_eqns in + (dbs, [SC_Typeclass { tc ; args = fresh_vars }] @ List.flatten recur) + | C_access_label (tv, label, result) -> let _todo = ignore (tv, label, result) in failwith "TODO" + +type ('state, 'elt) state_list_monad = { state: 'state ; list : 'elt list } +let lift_state_list_monad ~state ~list = { state ; list } +let lift f = + fun { state ; list } -> + let (new_state , new_lists) = List.fold_map_acc f state list in + { state = new_state ; list = List.flatten new_lists } + +(* TODO: move this to the List module *) +let named_fold_left f ~acc ~lst = List.fold_left (fun acc lst -> f ~acc ~lst) acc lst + +(* TODO: place the list of normalizers in a map *) +(* (\* cons for heterogeneous lists *\) + * type 'b f = { f : 'a . ('a -> 'b) -> 'a -> 'b } + * type ('hd , 'tl) hcons = { hd : 'hd ; tl : 'tl ; map : 'b . 'b f -> ('b , 'tl) hcons } + * let (+::) hd tl = { hd ; tl ; map = fun x -> } + * + * let list_of_normalizers = + * normalizer_simpl +:: + * normalizer_all_constraints +:: + * normalizer_assignments +:: + * normalizer_grouped_by_variable +:: + * () *) + +module Fun = struct let id x = x end (* in stdlib as of 4.08, we're in 4.07 for now *) + +let normalizers : type_constraint -> structured_dbs -> (structured_dbs , 'modified_constraint) state_list_monad = + fun new_constraint dbs -> + Fun.id + @@ lift normalizer_grouped_by_variable + @@ lift normalizer_assignments + @@ lift normalizer_all_constraints + @@ lift normalizer_simpl + @@ lift_state_list_monad ~state:dbs ~list:[new_constraint] + +(* sub-sub component: lazy selector (don't re-try all selectors every time) + * For now: just re-try everytime *) + +type todo = unit +let todo : todo = () +type 'old_constraint_type selector_input = 'old_constraint_type (* some info about the constraint just added, so that we know what to look for *) +type 'selector_output selector_outputs = + WasSelected of 'selector_output list + | WasNotSelected +type new_constraints = type_constraint list +type new_assignments = c_constructor_simpl list + +type ('old_constraint_type, 'selector_output) selector = 'old_constraint_type selector_input -> structured_dbs -> 'selector_output selector_outputs + +(* selector / propagation rule for breaking down composite types + * For now: do something with ('a = 'b) constraints. + + Or maybe this one should be a normalizer. *) + +(* selector / propagation rule for breaking down composite types + * For now: break pair(a, b) = pair(c, d) into a = c, b = d *) + +type output_break_ctor = < a_k_var : c_constructor_simpl ; a_k'_var' : c_constructor_simpl > +let selector_break_ctor : (type_constraint_simpl, output_break_ctor) selector = + (* find two rules with the shape a = k(var …) and a = k'(var' …) *) + fun todo dbs -> + match todo with + SC_Constructor c -> + let other_cs = (UnionFindWrapper.get_constraints_related_to c.tv dbs).constructor in + let cs_pairs = List.map (fun x -> object method a_k_var = c method a_k'_var' = x end) other_cs in + WasSelected cs_pairs + | SC_Alias _ -> WasNotSelected (* TODO: ??? *) + | SC_Typeclass _ -> WasNotSelected + +type 'selector_output propagator = 'selector_output -> structured_dbs -> new_constraints * new_assignments + +let propagator_break_ctor : output_break_ctor propagator = + fun selected dbs -> + let () = ignore (dbs) in (* this propagator doesn't need to use the dbs *) + let a = selected#a_k_var in + let b = selected#a_k'_var' in + (* produce constraints: *) + + (* a.tv = b.tv *) + let eq1 = C_equation (P_variable a.tv, P_variable b.tv) in + (* a.c_tag = b.c_tag *) + if a.c_tag <> b.c_tag then + failwith "type error: incompatible types, not same ctor (TODO error message)" + else + (* a.tv_list = b.tv_list *) + if List.length a.tv_list <> List.length b.tv_list then + failwith "type error: incompatible types, not same length (TODO error message)" + else + let eqs3 = List.map2 (fun aa bb -> C_equation (P_variable aa, P_variable bb)) a.tv_list b.tv_list in + let eqs = eq1 :: eqs3 in + (eqs , []) (* no new assignments *) + +let select_and_propagate : ('old_input, 'selector_output) selector -> 'selector_output propagator -> 'a -> structured_dbs -> new_constraints * new_assignments = + fun selector propagator -> + fun todo dbs -> + match selector todo dbs with + WasSelected selected_outputs -> + (* Call the propagation rule *) + let new_contraints_and_assignments = List.map (fun s -> propagator s dbs) selected_outputs in + let (new_constraints , new_assignments) = List.split new_contraints_and_assignments in + (* return so that the new constraints are pushed to some kind of work queue and the new assignments stored *) + (List.flatten new_constraints , List.flatten new_assignments) + | WasNotSelected -> + ([] , []) + +let select_and_propagate_break_ctor = select_and_propagate selector_break_ctor propagator_break_ctor + +let select_and_propagate_all' : type_constraint_simpl selector_input -> structured_dbs -> 'todo_result = + fun new_constraint dbs -> + let (new_constraints, new_assignments) = select_and_propagate_break_ctor new_constraint dbs in + let assignments = List.fold_left (fun acc ({tv;c_tag=_;tv_list=_} as ele) -> TypeVariableMap.update tv (function None -> Some ele | x -> x) acc) dbs.assignments new_assignments in + let dbs = { dbs with assignments } in + (* let blah2 = select_ … in … *) + (* We should try each selector in turn. If multiple selectors work, what should we do? *) + (new_constraints , dbs) + +let rec select_and_propagate_all : type_constraint selector_input list -> structured_dbs -> 'todo_result = + fun new_constraints dbs -> + match new_constraints with + | [] -> dbs + | new_constraint :: tl -> + let { state = dbs ; list = modified_constraints } = normalizers new_constraint dbs in + let (new_constraints' , dbs) = + List.fold_left + (fun (nc , dbs) c -> + let (new_constraints' , dbs) = select_and_propagate_all' c dbs in + (new_constraints' @ nc , dbs)) + ([] , dbs) + modified_constraints in + let new_constraints = new_constraints' @ tl in + select_and_propagate_all new_constraints dbs + +(* sub-component: constraint selector (worklist / dynamic queries) *) + +(* constraint propagation: (buch of constraints) → (new constraints * assignments) *) + + + + + +(* Below is a draft *) + +type state = { + (* when α-renaming x to y, we put them in the same union-find class *) + unification_vars : unionfind ; + + (* assigns a value to the representant in the unionfind *) + assignments : type_value TypeVariableMap.t ; + + (* constraints related to a type variable *) + constraints : constraints TypeVariableMap.t ; +} + +let initial_state : state = { + unification_vars = UF.empty ; + constraints = TypeVariableMap.empty ; + assignments = TypeVariableMap.empty ; +} + +(* let replace_var_in_state = fun (v : type_variable) (state : state) -> *) +(* let aux_tv : type_value -> _ = function *) +(* | P_forall (w , cs , tval) -> failwith "TODO" *) +(* | P_variable (w) -> *) +(* if w = v then *) +(* (*…*) *) +(* else *) +(* (*…*) *) +(* | P_constant (c , args) -> failwith "TODO" *) +(* | P_access_label (tv , label) -> failwith "TODO" in *) +(* let aux_tc tc = *) +(* List.map (fun l -> List.map aux_tv l) tc in *) +(* let aux : type_constraint -> _ = function *) +(* | C_equation (l , r) -> C_equation (aux_tv l , aux_tv r) *) +(* | C_typeclass (l , rs) -> C_typeclass (List.map aux_tv l , aux_tc rs) *) +(* in List.map aux state *) + +(* let check_equal a b = failwith "TODO" + * let check_same_length l1 l2 = failwith "TODO" + * + * let rec unify : type_value * type_value -> type_constraint list result = function + * | (P_variable v , P_constant (y , argsy)) -> + * failwith "TODO: replace v with the constant everywhere." + * | (P_constant (x , argsx) , P_variable w) -> + * failwith "TODO: " + * | (P_variable v , P_variable w) -> + * failwith "TODO: replace v with w everywhere" + * | (P_constant (x , argsx) , P_constant (y , argsy)) -> + * let%bind () = check_equal x y in + * let%bind () = check_same_length argsx argsy in + * let%bind _ = bind_map_list unify (List.combine argsx argsy) in + * ok [] + * | _ -> failwith "TODO" *) + +(* (\* unify a and b, possibly produce new constraints *\) *) +(* let () = ignore (a,b) in *) +(* ok [] *) + +(* This is the solver *) +let aggregate_constraints : state -> type_constraint list -> state result = fun state newc -> + (* TODO: Iterate over constraints *) + (* TODO: try to unify things: + if we have a = X and b = Y, try to unify X and Y *) + let _todo = ignore (state, newc) in + failwith "TODO" +(*let { constraints ; eqv } = state in + ok { constraints = constraints @ newc ; eqv }*) diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml index 391239506..efa65ae1b 100644 --- a/src/passes/4-typer/typer.ml +++ b/src/passes/4-typer/typer.ml @@ -8,6 +8,8 @@ module SMap = O.SMap module Environment = O.Environment +module Solver = Solver + type environment = Environment.t module Errors = struct @@ -216,6 +218,7 @@ module Errors = struct ] in error ~data title message end + open Errors let rec type_program (p:I.program) : O.program result = @@ -238,6 +241,9 @@ and type_declaration env : I.declaration -> (environment * O.declaration option) let env' = Environment.add_type type_name tv env in ok (env', None) | Declaration_constant (name , tv_opt , expression) -> ( + (* + Determine the type of the expression and add it to the environment + *) let%bind tv'_opt = bind_map_option (evaluate_type env) tv_opt in let%bind ae' = trace (constant_declaration_error name expression tv'_opt) @@ @@ -340,6 +346,10 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t bind_map_list aux lst in ok (O.Match_variant (lst' , variant)) +(* + Recursively search the type_expression and return a result containing the + type_value at the leaves +*) and evaluate_type (e:environment) (t:I.type_expression) : O.type_value result = let return tv' = ok (make_t tv' (Some t)) in match t with @@ -782,6 +792,9 @@ let untype_literal (l:O.literal) : I.literal result = | Literal_address s -> ok (Literal_address s) | Literal_operation s -> ok (Literal_operation s) +(* + Tranform a Ast_typed expression into an ast_simplified matching +*) let rec untype_expression (e:O.annotated_expression) : (I.expression) result = let open I in let return e = ok e in @@ -849,6 +862,9 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result = let%bind result = untype_expression result in return (e_let_in (binder , (Some tv)) rhs result) +(* + Tranform a Ast_typed matching into an ast_simplified matching +*) and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m -> let open I in match m with diff --git a/src/passes/4-typer/typer.ml.old b/src/passes/4-typer/typer.ml.old new file mode 100644 index 000000000..dfd99cbbe --- /dev/null +++ b/src/passes/4-typer/typer.ml.old @@ -0,0 +1,879 @@ +open Trace + +module I = Ast_simplified +module O = Ast_typed +open O.Combinators + +module SMap = O.SMap + +module Environment = O.Environment + +type environment = Environment.t + +module Errors = struct + let unbound_type_variable (e:environment) (n:string) () = + let title = (thunk "unbound type variable") in + let message () = "" in + let data = [ + ("variable" , fun () -> Format.asprintf "%s" n) ; + (* TODO: types don't have srclocs for now. *) + (* ("location" , fun () -> Format.asprintf "%a" Location.pp (n.location)) ; *) + ("in" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) + ] in + error ~data title message () + + let unbound_variable (e:environment) (n:string) (loc:Location.t) () = + let title = (thunk "unbound variable") in + let message () = "" in + let data = [ + ("variable" , fun () -> Format.asprintf "%s" n) ; + ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () + + let match_empty_variant : type a . a I.matching -> Location.t -> unit -> _ = + fun matching loc () -> + let title = (thunk "match with no cases") in + let message () = "" in + let data = [ + ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () + + let match_missing_case : type a . a I.matching -> Location.t -> unit -> _ = + fun matching loc () -> + let title = (thunk "missing case in match") in + let message () = "" in + let data = [ + ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () + + let match_redundant_case : type a . a I.matching -> Location.t -> unit -> _ = + fun matching loc () -> + let title = (thunk "missing case in match") in + let message () = "" in + let data = [ + ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () + + let unbound_constructor (e:environment) (n:string) (loc:Location.t) () = + let title = (thunk "unbound constructor") in + let message () = "" in + let data = [ + ("constructor" , fun () -> Format.asprintf "%s" n) ; + ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () + + let unrecognized_constant (n:string) (loc:Location.t) () = + let title = (thunk "unrecognized constant") in + let message () = "" in + let data = [ + ("constant" , fun () -> Format.asprintf "%s" n) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () + + let wrong_arity (n:string) (expected:int) (actual:int) (loc : Location.t) () = + let title () = "wrong arity" in + let message () = "" in + let data = [ + ("function" , fun () -> Format.asprintf "%s" n) ; + ("expected" , fun () -> Format.asprintf "%d" expected) ; + ("actual" , fun () -> Format.asprintf "%d" actual) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () + + let match_tuple_wrong_arity (expected:'a list) (actual:'b list) (loc:Location.t) () = + let title () = "matching tuple of different size" in + let message () = "" in + let data = [ + ("expected" , fun () -> Format.asprintf "%d" (List.length expected)) ; + ("actual" , fun () -> Format.asprintf "%d" (List.length actual)) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () + + (* TODO: this should be a trace_info? *) + let program_error (p:I.program) () = + let message () = "" in + let title = (thunk "typing program") in + let data = [ + ("program" , fun () -> Format.asprintf "%a" I.PP.program p) + ] in + error ~data title message () + + let constant_declaration_error (name:string) (ae:I.expr) (expected: O.type_expression option) () = + let title = (thunk "typing constant declaration") in + let message () = "" in + let data = [ + ("constant" , fun () -> Format.asprintf "%s" name) ; + ("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ; + ("expected" , fun () -> + match expected with + None -> "(no annotation for the expected type)" + | Some expected -> Format.asprintf "%a" O.PP.type_expression expected) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp ae.location) + ] in + error ~data title message () + + let match_error : type a . ?msg:string -> expected: a I.matching -> actual: O.type_expression -> Location.t -> unit -> _ = + fun ?(msg = "") ~expected ~actual loc () -> + let title = (thunk "typing match") in + let message () = msg in + let data = [ + ("expected" , fun () -> Format.asprintf "%a" I.PP.matching_type expected); + ("actual" , fun () -> Format.asprintf "%a" O.PP.type_expression actual) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () + + let needs_annotation (e : I.expression) (case : string) () = + let title = (thunk "this expression must be annotated with its type") in + let message () = Format.asprintf "%s needs an annotation" case in + let data = [ + ("expression" , fun () -> Format.asprintf "%a" I.PP.expression e) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp e.location) + ] in + error ~data title message () + + let type_error_approximate ?(msg="") ~(expected: string) ~(actual: O.type_expression) ~(expression : I.expression) (loc:Location.t) () = + let title = (thunk "type error") in + let message () = msg in + let data = [ + ("expected" , fun () -> Format.asprintf "%s" expected); + ("actual" , fun () -> Format.asprintf "%a" O.PP.type_expression actual); + ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () + + let type_error ?(msg="") ~(expected: O.type_expression) ~(actual: O.type_expression) ~(expression : I.expression) (loc:Location.t) () = + let title = (thunk "type error") in + let message () = msg in + let data = [ + ("expected" , fun () -> Format.asprintf "%a" O.PP.type_expression expected); + ("actual" , fun () -> Format.asprintf "%a" O.PP.type_expression actual); + ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () + + let bad_tuple_index (index : int) (ae : I.expression) (t : O.type_expression) (loc:Location.t) () = + let title = (thunk "invalid tuple index") in + let message () = "" in + let data = [ + ("index" , fun () -> Format.asprintf "%d" index) ; + ("tuple_value" , fun () -> Format.asprintf "%a" I.PP.expression ae) ; + ("tuple_type" , fun () -> Format.asprintf "%a" O.PP.type_expression t) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () + + let bad_record_access (field : string) (ae : I.expression) (t : O.type_expression) (loc:Location.t) () = + let title = (thunk "invalid record field") in + let message () = "" in + let data = [ + ("field" , fun () -> Format.asprintf "%s" field) ; + ("record_value" , fun () -> Format.asprintf "%a" I.PP.expression ae) ; + ("tuple_type" , fun () -> Format.asprintf "%a" O.PP.type_expression t) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp loc) + ] in + error ~data title message () + + let not_supported_yet (message : string) (ae : I.expression) () = + let title = (thunk "not supported yet") in + let message () = message in + let data = [ + ("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp ae.location) + ] in + error ~data title message () + + let not_supported_yet_untranspile (message : string) (ae : O.expression) () = + let title = (thunk "not supported yet") in + let message () = message in + let data = [ + ("expression" , fun () -> Format.asprintf "%a" O.PP.expression ae) + ] in + error ~data title message () + + let constant_error loc lst tv_opt = + let title () = "typing constant" in + let message () = "" in + let data = [ + ("location" , fun () -> Format.asprintf "%a" Location.pp loc ) ; + ("argument_types" , fun () -> Format.asprintf "%a" PP_helpers.(list_sep Ast_typed.PP.type_expression (const " , ")) lst) ; + ("type_opt" , fun () -> Format.asprintf "%a" PP_helpers.(option Ast_typed.PP.type_expression) tv_opt) ; + ] in + error ~data title message +end +open Errors + +let rec type_program (p:I.program) : O.program result = + let aux (e, acc:(environment * O.declaration Location.wrap list)) (d:I.declaration Location.wrap) = + let%bind ed' = (bind_map_location (type_declaration e)) d in + let loc : 'a . 'a Location.wrap -> _ -> _ = fun x v -> Location.wrap ~loc:x.location v in + let (e', d') = Location.unwrap ed' in + match d' with + | None -> ok (e', acc) + | Some d' -> ok (e', loc ed' d' :: acc) + in + let%bind (_, lst) = + trace (fun () -> program_error p ()) @@ + bind_fold_list aux (Environment.full_empty, []) p in + ok @@ List.rev lst + +and type_declaration env : I.declaration -> (environment * O.declaration option) result = function + | Declaration_type (type_name , type_expression) -> + let%bind tv = evaluate_type env type_expression in + let env' = Environment.add_type type_name tv env in + ok (env', None) + | Declaration_constant (name , tv_opt , expression) -> ( + let%bind tv'_opt = bind_map_option (evaluate_type env) tv_opt in + let%bind ae' = + trace (constant_declaration_error name expression tv'_opt) @@ + type_expression ?tv_opt:tv'_opt env expression in + let env' = Environment.add_ez_ae name ae' env in + ok (env', Some (O.Declaration_constant ((make_n_e name ae') , (env , env')))) + ) + +and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_expression -> i I.matching -> I.expression -> Location.t -> o O.matching result = + fun f e t i ae loc -> match i with + | Match_bool {match_true ; match_false} -> + let%bind _ = + trace_strong (match_error ~expected:i ~actual:t loc) + @@ get_t_bool t in + let%bind match_true = f e match_true in + let%bind match_false = f e match_false in + ok (O.Match_bool {match_true ; match_false}) + | Match_option {match_none ; match_some} -> + let%bind t_opt = + trace_strong (match_error ~expected:i ~actual:t loc) + @@ get_t_option t in + let%bind match_none = f e match_none in + let (n, b) = match_some in + let n' = n, t_opt in + let e' = Environment.add_ez_binder n t_opt e in + let%bind b' = f e' b in + ok (O.Match_option {match_none ; match_some = (n', b')}) + | Match_list {match_nil ; match_cons} -> + let%bind t_list = + trace_strong (match_error ~expected:i ~actual:t loc) + @@ get_t_list t in + let%bind match_nil = f e match_nil in + let (hd, tl, b) = match_cons in + let e' = Environment.add_ez_binder hd t_list e in + let e' = Environment.add_ez_binder tl t e' in + let%bind b' = f e' b in + ok (O.Match_list {match_nil ; match_cons = (hd, tl, b')}) + | Match_tuple (lst, b) -> + let%bind t_tuple = + trace_strong (match_error ~expected:i ~actual:t loc) + @@ get_t_tuple t in + let%bind lst' = + generic_try (match_tuple_wrong_arity t_tuple lst loc) + @@ (fun () -> List.combine lst t_tuple) in + let aux prev (name, tv) = Environment.add_ez_binder name tv prev in + let e' = List.fold_left aux e lst' in + let%bind b' = f e' b in + ok (O.Match_tuple (lst, b')) + | Match_variant lst -> + let%bind variant_opt = + let aux acc ((constructor_name , _) , _) = + let%bind (_ , variant) = + trace_option (unbound_constructor e constructor_name loc) @@ + Environment.get_constructor constructor_name e in + let%bind acc = match acc with + | None -> ok (Some variant) + | Some variant' -> ( + trace (type_error + ~msg:"in match variant" + ~expected:variant + ~actual:variant' + ~expression:ae + loc + ) @@ + Ast_typed.assert_type_expression_eq (variant , variant') >>? fun () -> + ok (Some variant) + ) in + ok acc in + trace (simple_info "in match variant") @@ + bind_fold_list aux None lst in + let%bind variant = + trace_option (match_empty_variant i loc) @@ + variant_opt in + let%bind () = + let%bind variant_cases' = + trace (match_error ~expected:i ~actual:t loc) + @@ Ast_typed.Combinators.get_t_sum variant in + let variant_cases = List.map fst @@ Map.String.to_kv_list variant_cases' in + let match_cases = List.map (Function.compose fst fst) lst in + let test_case = fun c -> + Assert.assert_true (List.mem c match_cases) + in + let%bind () = + trace_strong (match_missing_case i loc) @@ + bind_iter_list test_case variant_cases in + let%bind () = + trace_strong (match_redundant_case i loc) @@ + Assert.assert_true List.(length variant_cases = length match_cases) in + ok () + in + let%bind lst' = + let aux ((constructor_name , name) , b) = + let%bind (constructor , _) = + trace_option (unbound_constructor e constructor_name loc) @@ + Environment.get_constructor constructor_name e in + let e' = Environment.add_ez_binder name constructor e in + let%bind b' = f e' b in + ok ((constructor_name , name) , b') + in + bind_map_list aux lst in + ok (O.Match_variant (lst' , variant)) + +and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression result = + let return tv' = ok (make_t tv' (Some t)) in + match t with + | T_function (a, b) -> + let%bind a' = evaluate_type e a in + let%bind b' = evaluate_type e b in + return (T_function (a', b')) + | T_tuple lst -> + let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in + return (T_tuple lst') + | T_sum m -> + let aux k v prev = + let%bind prev' = prev in + let%bind v' = evaluate_type e v in + ok @@ SMap.add k v' prev' + in + let%bind m = SMap.fold aux m (ok SMap.empty) in + return (T_sum m) + | T_record m -> + let aux k v prev = + let%bind prev' = prev in + let%bind v' = evaluate_type e v in + ok @@ SMap.add k v' prev' + in + let%bind m = SMap.fold aux m (ok SMap.empty) in + return (T_record m) + | T_variable name -> + let%bind tv = + trace_option (unbound_type_variable e name) + @@ Environment.get_type_opt name e in + ok tv + | T_constant (cst, lst) -> + let%bind lst' = bind_list @@ List.map (evaluate_type e) lst in + return (T_constant(cst, lst')) + +and type_expression : environment -> ?tv_opt:O.type_expression -> I.expression -> O.annotated_expression result = fun e ?tv_opt ae -> + let module L = Logger.Stateful() in + let return expr tv = + let%bind () = + match tv_opt with + | None -> ok () + | Some tv' -> O.assert_type_expression_eq (tv' , tv) in + let location = Location.get_location ae in + ok @@ make_a_e ~location expr tv e in + let main_error = + let title () = "typing expression" in + let content () = "" in + let data = [ + ("expression" , fun () -> Format.asprintf "%a" I.PP.expression ae) ; + ("location" , fun () -> Format.asprintf "%a" Location.pp @@ Location.get_location ae) ; + ("misc" , fun () -> L.get ()) ; + ] in + error ~data title content in + trace main_error @@ + match Location.unwrap ae with + (* Basic *) + | E_failwith _ -> fail @@ needs_annotation ae "the failwith keyword" + | E_variable name -> + let%bind tv' = + trace_option (unbound_variable e name ae.location) + @@ Environment.get_opt name e in + return (E_variable name) tv'.type_expression + | E_literal (Literal_bool b) -> + return (E_literal (Literal_bool b)) (t_bool ()) + | E_literal Literal_unit | E_skip -> + return (E_literal (Literal_unit)) (t_unit ()) + | E_literal (Literal_string s) -> ( + L.log (Format.asprintf "literal_string option type: %a" PP_helpers.(option O.PP.type_expression) tv_opt) ; + match Option.map Ast_typed.get_type' tv_opt with + | Some (T_constant ("address" , [])) -> return (E_literal (Literal_address s)) (t_address ()) + | _ -> return (E_literal (Literal_string s)) (t_string ()) + ) + | E_literal (Literal_bytes s) -> + return (E_literal (Literal_bytes s)) (t_bytes ()) + | E_literal (Literal_int n) -> + return (E_literal (Literal_int n)) (t_int ()) + | E_literal (Literal_nat n) -> + return (E_literal (Literal_nat n)) (t_nat ()) + | E_literal (Literal_timestamp n) -> + return (E_literal (Literal_timestamp n)) (t_timestamp ()) + | E_literal (Literal_tez n) -> + return (E_literal (Literal_tez n)) (t_tez ()) + | E_literal (Literal_address s) -> + return (e_address s) (t_address ()) + | E_literal (Literal_operation op) -> + return (e_operation op) (t_operation ()) + (* Tuple *) + | E_tuple lst -> + let%bind lst' = bind_list @@ List.map (type_expression e) lst in + let tv_lst = List.map get_type_annotation lst' in + return (E_tuple lst') (t_tuple tv_lst ()) + | E_accessor (ae', path) -> + let%bind e' = type_expression e ae' in + let aux (prev:O.annotated_expression) (a:I.access) : O.annotated_expression result = + match a with + | Access_tuple index -> ( + let%bind tpl_tv = get_t_tuple prev.type_annotation in + let%bind tv = + generic_try (bad_tuple_index index ae' prev.type_annotation ae.location) + @@ (fun () -> List.nth tpl_tv index) in + return (E_tuple_accessor (prev , index)) tv + ) + | Access_record property -> ( + let%bind r_tv = get_t_record prev.type_annotation in + let%bind tv = + generic_try (bad_record_access property ae' prev.type_annotation ae.location) + @@ (fun () -> SMap.find property r_tv) in + return (E_record_accessor (prev , property)) tv + ) + | Access_map ae' -> ( + let%bind ae'' = type_expression e ae' in + let%bind (k , v) = get_t_map prev.type_annotation in + let%bind () = + Ast_typed.assert_type_expression_eq (k , get_type_annotation ae'') in + return (E_look_up (prev , ae'')) v + ) + in + trace (simple_info "accessing") @@ + bind_fold_list aux e' path + + (* Sum *) + | E_constructor (c, expr) -> + let%bind (c_tv, sum_tv) = + let error = + let title () = "no such constructor" in + let content () = + Format.asprintf "%s in:\n%a\n" + c O.Environment.PP.full_environment e + in + error title content in + trace_option error @@ + Environment.get_constructor c e in + let%bind expr' = type_expression e expr in + let%bind _assert = O.assert_type_expression_eq (expr'.type_annotation, c_tv) in + return (E_constructor (c , expr')) sum_tv + (* Record *) + | E_record m -> + let aux prev k expr = + let%bind expr' = type_expression e expr in + ok (SMap.add k expr' prev) + in + let%bind m' = bind_fold_smap aux (ok SMap.empty) m in + return (E_record m') (t_record (SMap.map get_type_annotation m') ()) + (* Data-structure *) + | E_list lst -> + let%bind lst' = bind_map_list (type_expression e) lst in + let%bind tv = + let aux opt c = + match opt with + | None -> ok (Some c) + | Some c' -> + let%bind _eq = Ast_typed.assert_type_expression_eq (c, c') in + ok (Some c') in + let%bind init = match tv_opt with + | None -> ok None + | Some ty -> + let%bind ty' = get_t_list ty in + ok (Some ty') in + let%bind ty = + let%bind opt = bind_fold_list aux init + @@ List.map get_type_annotation lst' in + trace_option (needs_annotation ae "empty list") opt in + ok (t_list ty ()) + in + return (E_list lst') tv + | E_set lst -> + let%bind lst' = bind_map_list (type_expression e) lst in + let%bind tv = + let aux opt c = + match opt with + | None -> ok (Some c) + | Some c' -> + let%bind _eq = Ast_typed.assert_type_expression_eq (c, c') in + ok (Some c') in + let%bind init = match tv_opt with + | None -> ok None + | Some ty -> + let%bind ty' = get_t_set ty in + ok (Some ty') in + let%bind ty = + let%bind opt = bind_fold_list aux init + @@ List.map get_type_annotation lst' in + trace_option (needs_annotation ae "empty set") opt in + ok (t_set ty ()) + in + return (E_set lst') tv + | E_map lst -> + let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in + let%bind tv = + let aux opt c = + match opt with + | None -> ok (Some c) + | Some c' -> + let%bind _eq = Ast_typed.assert_type_expression_eq (c, c') in + ok (Some c') in + let%bind key_type = + let%bind sub = + bind_fold_list aux None + @@ List.map get_type_annotation + @@ List.map fst lst' in + let%bind annot = bind_map_option get_t_map_key tv_opt in + trace (simple_info "empty map expression without a type annotation") @@ + O.merge_annotation annot sub (needs_annotation ae "this map literal") + in + let%bind value_type = + let%bind sub = + bind_fold_list aux None + @@ List.map get_type_annotation + @@ List.map snd lst' in + let%bind annot = bind_map_option get_t_map_value tv_opt in + trace (simple_info "empty map expression without a type annotation") @@ + O.merge_annotation annot sub (needs_annotation ae "this map literal") + in + ok (t_map key_type value_type ()) + in + return (E_map lst') tv + | E_lambda { + binder ; + input_type ; + output_type ; + result ; + } -> ( + let%bind input_type = + let%bind input_type = + (* Hack to take care of let_in introduced by `simplify/ligodity.ml` in ECase's hack *) + let default_action e () = fail @@ (needs_annotation e "the returned value") in + match input_type with + | Some ty -> ok ty + | None -> ( + match Location.unwrap result with + | I.E_let_in li -> ( + match Location.unwrap li.rhs with + | I.E_variable name when name = (fst binder) -> ( + match snd li.binder with + | Some ty -> ok ty + | None -> default_action li.rhs () + ) + | _ -> default_action li.rhs () + ) + | _ -> default_action result () + ) + in + evaluate_type e input_type in + let%bind output_type = + bind_map_option (evaluate_type e) output_type + in + let e' = Environment.add_ez_binder (fst binder) input_type e in + let%bind result = type_expression ?tv_opt:output_type e' result in + let output_type = result.type_annotation in + return (E_lambda {binder = fst binder;input_type;output_type;result}) (t_function input_type output_type ()) + ) + | E_constant (name, lst) -> + let%bind lst' = bind_list @@ List.map (type_expression e) lst in + let tv_lst = List.map get_type_annotation lst' in + let%bind (name', tv) = + type_constant name tv_lst tv_opt ae.location in + return (E_constant (name' , lst')) tv + | E_application (f, arg) -> + let%bind f' = type_expression e f in + let%bind arg = type_expression e arg in + let%bind tv = match f'.type_annotation.type_expression' with + | T_function (param, result) -> + let%bind _ = O.assert_type_expression_eq (param, arg.type_annotation) in + ok result + | _ -> + fail @@ type_error_approximate + ~expected:"should be a function type" + ~expression:f + ~actual:f'.type_annotation + f'.location + in + return (E_application (f' , arg)) tv + | E_look_up dsi -> + let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in + let%bind (src, dst) = get_t_map ds.type_annotation in + let%bind _ = O.assert_type_expression_eq (ind.type_annotation, src) in + return (E_look_up (ds , ind)) (t_option dst ()) + (* Advanced *) + | E_matching (ex, m) -> ( + let%bind ex' = type_expression e ex in + match m with + (* Special case for assert-like failwiths. TODO: CLEAN THIS. *) + | I.Match_bool { match_false ; match_true } when I.is_e_failwith match_true -> ( + let%bind fw = I.get_e_failwith match_true in + let%bind fw' = type_expression e fw in + let%bind mf' = type_expression e match_false in + let t = get_type_annotation ex' in + let%bind () = + trace_strong (match_error ~expected:m ~actual:t ae.location) + @@ assert_t_bool t in + let%bind () = + trace_strong (match_error + ~msg:"matching not-unit on an assert" + ~expected:m + ~actual:t + ae.location) + @@ assert_t_unit (get_type_annotation mf') in + let mt' = make_a_e + (E_constant ("ASSERT_INFERRED" , [ex' ; fw'])) + (t_unit ()) + e + in + let m' = O.Match_bool { match_true = mt' ; match_false = mf' } in + return (O.E_matching (ex' , m')) (t_unit ()) + ) + | _ -> ( + let%bind m' = type_match (type_expression ?tv_opt:None) e ex'.type_annotation m ae ae.location in + let tvs = + let aux (cur:O.value O.matching) = + match cur with + | Match_bool { match_true ; match_false } -> [ match_true ; match_false ] + | Match_list { match_nil ; match_cons = (_ , _ , match_cons) } -> [ match_nil ; match_cons ] + | Match_option { match_none ; match_some = (_ , match_some) } -> [ match_none ; match_some ] + | Match_tuple (_ , match_tuple) -> [ match_tuple ] + | Match_variant (lst , _) -> List.map snd lst in + List.map get_type_annotation @@ aux m' in + let aux prec cur = + let%bind () = + match prec with + | None -> ok () + | Some cur' -> Ast_typed.assert_type_expression_eq (cur , cur') in + ok (Some cur) in + let%bind tv_opt = bind_fold_list aux None tvs in + let%bind tv = + trace_option (match_empty_variant m ae.location) @@ + tv_opt in + return (O.E_matching (ex', m')) tv + ) + ) + | E_sequence (a , b) -> + let%bind a' = type_expression e a in + let%bind b' = type_expression e b in + let a'_type_annot = get_type_annotation a' in + let%bind () = + trace_strong (type_error + ~msg:"first part of the sequence should be of unit type" + ~expected:(O.t_unit ()) + ~actual:a'_type_annot + ~expression:a + a'.location) @@ + Ast_typed.assert_type_expression_eq (t_unit () , a'_type_annot) in + return (O.E_sequence (a' , b')) (get_type_annotation b') + | E_loop (expr , body) -> + let%bind expr' = type_expression e expr in + let%bind body' = type_expression e body in + let t_expr' = get_type_annotation expr' in + let%bind () = + trace_strong (type_error + ~msg:"while condition isn't of type bool" + ~expected:(O.t_bool ()) + ~actual:t_expr' + ~expression:expr + expr'.location) @@ + Ast_typed.assert_type_expression_eq (t_bool () , t_expr') in + let t_body' = get_type_annotation body' in + let%bind () = + trace_strong (type_error + ~msg:"while body isn't of unit type" + ~expected:(O.t_unit ()) + ~actual:t_body' + ~expression:body + body'.location) @@ + Ast_typed.assert_type_expression_eq (t_unit () , t_body') in + return (O.E_loop (expr' , body')) (t_unit ()) + | E_assign (name , path , expr) -> + let%bind typed_name = + let%bind ele = Environment.get_trace name e in + ok @@ make_n_t name ele.type_expression in + let%bind (assign_tv , path') = + let aux : ((_ * O.access_path) as 'a) -> I.access -> 'a result = fun (prec_tv , prec_path) cur_path -> + match cur_path with + | Access_tuple index -> ( + let%bind tpl = get_t_tuple prec_tv in + let%bind tv' = + trace_option (bad_tuple_index index ae prec_tv ae.location) @@ + List.nth_opt tpl index in + ok (tv' , prec_path @ [O.Access_tuple index]) + ) + | Access_record property -> ( + let%bind m = get_t_record prec_tv in + let%bind tv' = + trace_option (bad_record_access property ae prec_tv ae.location) @@ + Map.String.find_opt property m in + ok (tv' , prec_path @ [O.Access_record property]) + ) + | Access_map _ -> + fail @@ not_supported_yet "assign expressions with maps are not supported yet" ae + in + bind_fold_list aux (typed_name.type_expression , []) path in + let%bind expr' = type_expression e expr in + let t_expr' = get_type_annotation expr' in + let%bind () = + trace_strong (type_error + ~msg:"type of the expression to assign doesn't match left-hand-side" + ~expected:assign_tv + ~actual:t_expr' + ~expression:expr + expr'.location) @@ + Ast_typed.assert_type_expression_eq (assign_tv , t_expr') in + return (O.E_assign (typed_name , path' , expr')) (t_unit ()) + | E_let_in {binder ; rhs ; result} -> + let%bind rhs_tv_opt = bind_map_option (evaluate_type e) (snd binder) in + let%bind rhs = type_expression ?tv_opt:rhs_tv_opt e rhs in + let e' = Environment.add_ez_declaration (fst binder) rhs e in + let%bind result = type_expression e' result in + return (E_let_in {binder = fst binder; rhs; result}) result.type_annotation + | E_annotation (expr , te) -> + let%bind tv = evaluate_type e te in + let%bind expr' = type_expression ~tv_opt:tv e expr in + let%bind type_annotation = + O.merge_annotation + (Some tv) + (Some expr'.type_annotation) + (internal_assertion_failure "merge_annotations (Some ...) (Some ...) failed") in + ok {expr' with type_annotation} + + +and type_constant (name:string) (lst:O.type_expression list) (tv_opt:O.type_expression option) (loc : Location.t) : (string * O.type_expression) result = + (* Constant poorman's polymorphism *) + let ct = Operators.Typer.constant_typers in + let%bind typer = + trace_option (unrecognized_constant name loc) @@ + Map.String.find_opt name ct in + trace (constant_error loc lst tv_opt) @@ + typer lst tv_opt + +let untype_type_expression (t:O.type_expression) : (I.type_expression) result = + match t.simplified with + | Some s -> ok s + | _ -> fail @@ internal_assertion_failure "trying to untype generated type" + +let untype_literal (l:O.literal) : I.literal result = + let open I in + match l with + | Literal_unit -> ok Literal_unit + | Literal_bool b -> ok (Literal_bool b) + | Literal_nat n -> ok (Literal_nat n) + | Literal_timestamp n -> ok (Literal_timestamp n) + | Literal_tez n -> ok (Literal_tez n) + | Literal_int n -> ok (Literal_int n) + | Literal_string s -> ok (Literal_string s) + | Literal_bytes b -> ok (Literal_bytes b) + | Literal_address s -> ok (Literal_address s) + | Literal_operation s -> ok (Literal_operation s) + +let rec untype_expression (e:O.annotated_expression) : (I.expression) result = + let open I in + let return e = ok e in + match e.expression with + | E_literal l -> + let%bind l = untype_literal l in + return (e_literal l) + | E_constant (n, lst) -> + let%bind lst' = bind_map_list untype_expression lst in + return (e_constant n lst') + | E_variable n -> + return (e_variable n) + | E_application (f, arg) -> + let%bind f' = untype_expression f in + let%bind arg' = untype_expression arg in + return (e_application f' arg') + | E_lambda {binder;input_type;output_type;result} -> + let%bind input_type = untype_type_expression input_type in + let%bind output_type = untype_type_expression output_type in + let%bind result = untype_expression result in + return (e_lambda binder (Some input_type) (Some output_type) result) + | E_tuple lst -> + let%bind lst' = bind_list + @@ List.map untype_expression lst in + return (e_tuple lst') + | E_tuple_accessor (tpl, ind) -> + let%bind tpl' = untype_expression tpl in + return (e_accessor tpl' [Access_tuple ind]) + | E_constructor (n, p) -> + let%bind p' = untype_expression p in + return (e_constructor n p') + | E_record r -> + let%bind r' = bind_smap + @@ SMap.map untype_expression r in + return (e_record r') + | E_record_accessor (r, s) -> + let%bind r' = untype_expression r in + return (e_accessor r' [Access_record s]) + | E_map m -> + let%bind m' = bind_map_list (bind_map_pair untype_expression) m in + return (e_map m') + | E_list lst -> + let%bind lst' = bind_map_list untype_expression lst in + return (e_list lst') + | E_set lst -> + let%bind lst' = bind_map_list untype_expression lst in + return (e_set lst') + | E_look_up dsi -> + let%bind (a , b) = bind_map_pair untype_expression dsi in + return (e_look_up a b) + | E_matching (ae, m) -> + let%bind ae' = untype_expression ae in + let%bind m' = untype_matching untype_expression m in + return (e_matching ae' m') + | E_failwith ae -> + let%bind ae' = untype_expression ae in + return (e_failwith ae') + | E_sequence _ + | E_loop _ + | E_assign _ -> fail @@ not_supported_yet_untranspile "not possible to untranspile statements yet" e.expression + | E_let_in {binder;rhs;result} -> + let%bind tv = untype_type_expression rhs.type_annotation in + let%bind rhs = untype_expression rhs in + let%bind result = untype_expression result in + return (e_let_in (binder , (Some tv)) rhs result) + +and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m -> + let open I in + match m with + | Match_bool {match_true ; match_false} -> + let%bind match_true = f match_true in + let%bind match_false = f match_false in + ok @@ Match_bool {match_true ; match_false} + | Match_tuple (lst, b) -> + let%bind b = f b in + ok @@ Match_tuple (lst, b) + | Match_option {match_none ; match_some = (v, some)} -> + let%bind match_none = f match_none in + let%bind some = f some in + let match_some = fst v, some in + ok @@ Match_option {match_none ; match_some} + | Match_list {match_nil ; match_cons = (hd, tl, cons)} -> + let%bind match_nil = f match_nil in + let%bind cons = f cons in + let match_cons = hd, tl, cons in + ok @@ Match_list {match_nil ; match_cons} + | Match_variant (lst , _) -> + let aux ((a,b),c) = + let%bind c' = f c in + ok ((a,b),c') in + let%bind lst' = bind_map_list aux lst in + ok @@ Match_variant lst' diff --git a/src/passes/operators/dune b/src/passes/operators/dune index 0bd5db43d..f2125905a 100644 --- a/src/passes/operators/dune +++ b/src/passes/operators/dune @@ -5,6 +5,7 @@ simple-utils tezos-utils ast_typed + typesystem mini_c ) (preprocess diff --git a/src/passes/operators/operators.ml b/src/passes/operators/operators.ml index 47627a440..5eb1dfb91 100644 --- a/src/passes/operators/operators.ml +++ b/src/passes/operators/operators.ml @@ -219,6 +219,65 @@ module Typer = struct open Helpers.Typer open Ast_typed + module Operators_types = struct + open Typesystem.Shorthands + + let tc_subarg a b c = tc [a;b;c] [ (*TODO…*) ] + let tc_sizearg a = tc [a] [ [int] ] + let tc_packable a = tc [a] [ [int] ; [string] ; [bool] (*TODO…*) ] + let tc_timargs a b c = tc [a;b;c] [ [nat;nat;nat] ; [int;int;int] (*TODO…*) ] + let tc_divargs a b c = tc [a;b;c] [ (*TODO…*) ] + let tc_modargs a b c = tc [a;b;c] [ (*TODO…*) ] + let tc_addargs a b c = tc [a;b;c] [ (*TODO…*) ] + + let t_none = forall "a" @@ fun a -> option a + let t_sub = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_subarg a b c] => a --> b --> c (* TYPECLASS *) + let t_some = forall "a" @@ fun a -> a --> option a + let t_map_remove = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> map src dst + let t_map_add = forall2 "src" "dst" @@ fun src dst -> src --> dst --> map src dst --> map src dst + let t_map_update = forall2 "src" "dst" @@ fun src dst -> src --> option dst --> map src dst --> map src dst + let t_map_mem = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> bool + let t_map_find = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> dst + let t_map_find_opt = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> option dst + let t_map_fold = forall3 "src" "dst" "acc" @@ fun src dst acc -> ( ( (src * dst) * acc ) --> acc ) --> map src dst --> acc --> acc + let t_map_map = forall3 "k" "v" "result" @@ fun k v result -> ((k * v) --> result) --> map k v --> map k result + + (* TODO: the type of map_map_fold might be wrong, check it. *) + let t_map_map_fold = forall4 "k" "v" "acc" "dst" @@ fun k v acc dst -> ( ((k * v) * acc) --> acc * dst ) --> map k v --> (k * v) --> (map k dst * acc) + let t_map_iter = forall2 "k" "v" @@ fun k v -> ( (k * v) --> unit ) --> map k v --> unit + let t_size = forall_tc "c" @@ fun c -> [tc_sizearg c] => c --> nat (* TYPECLASS *) + let t_slice = nat --> nat --> string --> string + let t_failwith = string --> unit + let t_get_force = forall2 "src" "dst" @@ fun src dst -> src --> map src dst --> dst + let t_int = nat --> int + let t_bytes_pack = forall_tc "a" @@ fun a -> [tc_packable a] => a --> bytes (* TYPECLASS *) + let t_bytes_unpack = forall_tc "a" @@ fun a -> [tc_packable a] => bytes --> a (* TYPECLASS *) + let t_hash256 = bytes --> bytes + let t_hash512 = bytes --> bytes + let t_blake2b = bytes --> bytes + let t_hash_key = key --> key_hash + let t_check_signature = key --> signature --> bytes --> bool + let t_sender = address + let t_source = address + let t_unit = unit + let t_amount = tez + let t_address = address + let t_now = timestamp + let t_transaction = forall "a" @@ fun a -> a --> tez --> contract a --> operation + let t_get_contract = forall "a" @@ fun a -> contract a + let t_abs = int --> nat + let t_cons = forall "a" @@ fun a -> a --> list a --> list a + let t_assertion = bool --> unit + let t_times = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_timargs a b c] => a --> b --> c (* TYPECLASS *) + let t_div = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_divargs a b c] => a --> b --> c (* TYPECLASS *) + let t_mod = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_modargs a b c] => a --> b --> c (* TYPECLASS *) + let t_add = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_addargs a b c] => a --> b --> c (* TYPECLASS *) + let t_set_mem = forall "a" @@ fun a -> a --> set a --> bool + let t_set_add = forall "a" @@ fun a -> a --> set a --> set a + let t_set_remove = forall "a" @@ fun a -> a --> set a --> set a + let t_not = bool --> bool + end + let none = typer_0 "NONE" @@ fun tv_opt -> match tv_opt with | None -> simple_fail "untyped NONE" @@ -647,6 +706,7 @@ module Typer = struct get_contract ; neg ; abs ; + cons ; now ; slice ; address ; diff --git a/src/typesystem/core.ml b/src/typesystem/core.ml new file mode 100644 index 000000000..69a5d413c --- /dev/null +++ b/src/typesystem/core.ml @@ -0,0 +1,60 @@ + type type_variable = string + + let fresh_type_variable : ?name:string -> unit -> type_variable = + let id = ref 0 in + let inc () = id := !id + 1 in + fun ?name () -> + inc () ; + match name with + | None -> "type_variable_" ^ (string_of_int !id) + | Some name -> "tv_" ^ name ^ "_" ^ (string_of_int !id) + + + type constant_tag = + | C_arrow (* * -> * -> * *) + | C_option (* * -> * *) + | C_tuple (* * … -> * *) + | C_record (* ( label , * ) … -> * *) + | C_variant (* ( label , * ) … -> * *) + | C_map (* * -> * -> * *) + | C_list (* * -> * *) + | C_set (* * -> * *) + | C_unit (* * *) + | C_bool (* * *) + | C_string (* * *) + | C_nat (* * *) + | C_tez (* * *) + | C_timestamp (* * *) + | C_int (* * *) + | C_address (* * *) + | C_bytes (* * *) + | C_key_hash (* * *) + | C_key (* * *) + | C_signature (* * *) + | C_operation (* * *) + | C_contract (* * -> * *) + + type label = + | L_int of int + | L_string of string + + type type_value = + | P_forall of (type_variable * type_constraint list * type_value) + | P_variable of type_variable + | P_constant of (constant_tag * type_value list) + + and simple_c_constructor = (constant_tag * type_variable list) (* non-empty list *) + and simple_c_constant = (constant_tag) (* for type constructors that do not take arguments *) + and c_const = (type_variable * type_value) + and c_equation = (type_value * type_value) + and c_typeclass = (type_value list * typeclass) + and c_access_label = (type_value * label * type_variable) + + and type_constraint = + (* | C_assignment of (type_variable * type_pattern) *) + | C_equation of c_equation (* TVA = TVB *) + | C_typeclass of c_typeclass (* TVL ∈ TVLs, for now in extension, later add intensional (rule-based system for inclusion in the typeclass) *) + | C_access_label of c_access_label (* poor man's type-level computation to ensure that TV.label is type_variable *) + (* | … *) + + and typeclass = type_value list list diff --git a/src/typesystem/dune b/src/typesystem/dune new file mode 100644 index 000000000..d5e1deaf6 --- /dev/null +++ b/src/typesystem/dune @@ -0,0 +1,14 @@ +(library + (name typesystem) + (public_name ligo.typesystem) + (libraries + simple-utils + tezos-utils + ast_typed + mini_c + ) + (preprocess + (pps ppx_let) + ) + (flags (:standard -w +1..62-4-9-44-40-42-48-30@39@33 -open Simple_utils )) +) diff --git a/src/typesystem/shorthands.ml b/src/typesystem/shorthands.ml new file mode 100644 index 000000000..2bf16dd9c --- /dev/null +++ b/src/typesystem/shorthands.ml @@ -0,0 +1,62 @@ +open Core + +let tc type_vars allowed_list = + Core.C_typeclass (type_vars , allowed_list) + +let forall binder f = + let () = ignore binder in + let freshvar = fresh_type_variable () in + P_forall (freshvar , [] , f (P_variable freshvar)) + +let forall_tc binder f = + let () = ignore binder in + let freshvar = fresh_type_variable () in + let (tc, ty) = f (P_variable freshvar) in + P_forall (freshvar , tc , ty) + +let forall2 a b f = + forall a @@ fun a' -> + forall b @@ fun b' -> + f a' b' + +let forall3 a b c f = + forall a @@ fun a' -> + forall b @@ fun b' -> + forall c @@ fun c' -> + f a' b' c' + +let forall4 a b c d f = + forall a @@ fun a' -> + forall b @@ fun b' -> + forall c @@ fun c' -> + forall d @@ fun d' -> + f a' b' c' d' + +let forall3_tc a b c f = + forall a @@ fun a' -> + forall b @@ fun b' -> + forall_tc c @@ fun c' -> + f a' b' c' + +let (-->) arg ret = P_constant (C_arrow , [arg; ret]) +let (=>) tc ty = (tc , ty) +let option t = P_constant (C_option , [t]) +let pair a b = P_constant (C_tuple , [a; b]) +let map k v = P_constant (C_map , [k; v]) +let unit = P_constant (C_unit , []) +let list t = P_constant (C_list , [t]) +let set t = P_constant (C_set , [t]) +let bool = P_constant (C_bool , []) +let string = P_constant (C_string , []) +let nat = P_constant (C_nat , []) +let tez = P_constant (C_tez , []) +let timestamp = P_constant (C_timestamp , []) +let int = P_constant (C_int , []) +let address = P_constant (C_address , []) +let bytes = P_constant (C_bytes , []) +let key = P_constant (C_key , []) +let key_hash = P_constant (C_key_hash , []) +let signature = P_constant (C_signature , []) +let operation = P_constant (C_operation , []) +let contract t = P_constant (C_contract , [t]) +let ( * ) a b = pair a b diff --git a/src/typesystem/typesystem.ml b/src/typesystem/typesystem.ml new file mode 100644 index 000000000..b97e373e9 --- /dev/null +++ b/src/typesystem/typesystem.ml @@ -0,0 +1,2 @@ +module Core = Core +module Shorthands = Shorthands diff --git a/src/union_find/.PartitionMain.tag b/src/union_find/.PartitionMain.tag new file mode 100644 index 000000000..e69de29bb diff --git a/src/union_find/.links b/src/union_find/.links new file mode 100644 index 000000000..b79d096bc --- /dev/null +++ b/src/union_find/.links @@ -0,0 +1 @@ +../OCaml-build/Makefile diff --git a/src/union_find/LICENSE b/src/union_find/LICENSE new file mode 100644 index 000000000..33a225af0 --- /dev/null +++ b/src/union_find/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2018 Christian Rinderknecht + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/src/union_find/Makefile.cfg b/src/union_find/Makefile.cfg new file mode 100644 index 000000000..13c016eb6 --- /dev/null +++ b/src/union_find/Makefile.cfg @@ -0,0 +1,4 @@ +SHELL := dash +BFLAGS := -strict-sequence -w +A-48-4 +#OCAMLC := ocamlcp +#OCAMLOPT := ocamloptp diff --git a/src/union_find/Partition.mli b/src/union_find/Partition.mli new file mode 100644 index 000000000..657b3c007 --- /dev/null +++ b/src/union_find/Partition.mli @@ -0,0 +1,64 @@ +(** This module offers the abstract data type of a partition of + classes of equivalent items (Union & Find). *) + +(** The items are of type [Item.t], that is, they have to obey + a total order, but also they must be printable to ease + debugging. The signature [Item] is the input signature of + the functor {!Partition.Make}. *) +module type Item = + sig + (** Type of items *) + type t + + (** Same convention as {!Pervasives.compare} *) + val compare : t -> t -> int + + val to_string : t -> string + end + +(** The module signature [S] is the output signature of the functor + {!Partition.Make}. *) +module type S = + sig + type item + type partition + type t = partition + + (** {1 Creation} *) + + (** The value [empty] is an empty partition. *) + val empty : partition + + (** The value of [equiv i j p] is the partition [p] extended with + the equivalence of items [i] and [j]. If both [i] and [j] are + already known to be equivalent, then [equiv i j p == p]. *) + val equiv : item -> item -> partition -> partition + + (** The value of [alias i j p] is the partition [p] extended with + the fact that item [i] is an alias of item [j]. This is the + same as [equiv i j p], except that it is guaranteed that the + item [i] is not the representative of its equivalence class in + [alias i j p]. *) + val alias : item -> item -> partition -> partition + + (** {1 Projection} *) + + (** The value of the call [repr i p] is the representative of item + [i] in the partition [p]. The built-in exception [Not_found] + is raised if [i] is not in [p]. *) + val repr : item -> partition -> item + + (** The side-effect of the call [print p] is the printing of the + partition [p] on standard output, based on [Ord.to_string]. *) + val print : partition -> unit + + (** {1 Predicates} *) + + (** The value of [is_equiv i j p] is [true] if, and only if, the + items [i] and [j] belong to the same equivalence class in the + partition [p], that is, [i] and [j] have the same + representative. *) + val is_equiv : item -> item -> partition -> bool + end + +module Make (Ord : Item) : S with type item = Ord.t diff --git a/src/union_find/Partition0.ml b/src/union_find/Partition0.ml new file mode 100644 index 000000000..968bb8dd4 --- /dev/null +++ b/src/union_find/Partition0.ml @@ -0,0 +1,47 @@ +(* Naive persistent implementation of Union/Find: O(n^2) worst case *) + +module Make (Item: Partition.Item) = + struct + + type item = Item.t + type repr = item (** Class representatives *) + + let equal i j = Item.compare i j = 0 + + module ItemMap = Map.Make (Item) + + type height = int + + type partition = item ItemMap.t + type t = partition + + let empty = ItemMap.empty + + let rec repr item partition = + let parent = ItemMap.find item partition in + if equal parent item + then item + else repr parent partition + + let is_equiv (i: item) (j: item) (p: partition) = + equal (repr i p) (repr j p) + + let get_or_set (i: item) (p: partition) : item * partition = + try repr i p, p with Not_found -> i, ItemMap.add i i p + + let equiv (i: item) (j :item) (p: partition) : partition = + let ri, p = get_or_set i p in + let rj, p = get_or_set j p in + if equal ri rj then p else ItemMap.add ri rj p + + let alias = equiv + + (* Printing *) + + let print p = + let print src dst = + Printf.printf "%s -> %s\n" + (Item.to_string src) (Item.to_string dst) + in ItemMap.iter print p + + end diff --git a/src/union_find/Partition1.ml b/src/union_find/Partition1.ml new file mode 100644 index 000000000..764d98d49 --- /dev/null +++ b/src/union_find/Partition1.ml @@ -0,0 +1,69 @@ +(* Persistent implementation of Union/Find with height-balanced + forests and without path compression: O(n*log(n)). + + In the definition of type [t], the height component is that of the + source, that is, if [ItemMap.find i m = (j,h)], then [h] is the + height of [i] (_not_ [j]). +*) + +module Make (Item: Partition.Item) = + struct + + type item = Item.t + type repr = item (** Class representatives *) + + let equal i j = Item.compare i j = 0 + + module ItemMap = Map.Make (Item) + + type height = int + + type partition = (item * height) ItemMap.t + type t = partition + + let empty = ItemMap.empty + + let rec seek (i: item) (p: partition) : repr * height = + let j, _ as i' = ItemMap.find i p in + if equal i j then i' else seek j p + + let repr item partition = fst (seek item partition) + + let is_equiv (i: item) (j: item) (p: partition) = + equal (repr i p) (repr j p) + + let get_or_set (i: item) (p: partition) = + try seek i p, p with + Not_found -> let i' = i,0 in (i', ItemMap.add i i' p) + + let equiv (i: item) (j: item) (p: partition) : partition = + let (ri,hi), p = get_or_set i p in + let (rj,hj), p = get_or_set j p in + let add = ItemMap.add in + if equal ri rj + then p + else if hi > hj + then add rj (ri,hj) p + else add ri (rj,hi) (if hi < hj then p else add rj (rj,hj+1) p) + + let alias (i: item) (j: item) (p: partition) : partition = + let (ri,hi), p = get_or_set i p in + let (rj,hj), p = get_or_set j p in + let add = ItemMap.add in + if equal ri rj + then p + else if hi = hj || equal ri i + then add ri (rj,hi) @@ add rj (rj, max hj (hi+1)) p + else if hi < hj then add ri (rj,hi) p + else add rj (ri,hj) p + + (* Printing *) + + let print (p: partition) = + let print i (j,hi) = + let _,hj = ItemMap.find j p in + Printf.printf "%s,%d -> %s,%d\n" + (Item.to_string i) hi (Item.to_string j) hj + in ItemMap.iter print p + + end diff --git a/src/union_find/Partition2.ml b/src/union_find/Partition2.ml new file mode 100644 index 000000000..e1372b2fd --- /dev/null +++ b/src/union_find/Partition2.ml @@ -0,0 +1,115 @@ +(** Persistent implementation of the Union/Find algorithm with + height-balanced forests and without path compression. *) + +module Make (Item: Partition.Item) = + struct + + type item = Item.t + type repr = item (** Class representatives *) + + let equal i j = Item.compare i j = 0 + + type height = int + + (** Each equivalence class is implemented by a Catalan tree linked + upwardly and otherwise is a link to another node. Those trees + are height-balanced. The type [node] implements nodes in those + trees. *) + type node = + Root of height + (** The value of [Root h] denotes the root of a tree, that is, + the representative of the associated class. The height [h] + is that of the tree, so a tree reduced to its root alone has + heigh 0. *) + + | Link of item * height + (** If not a root, a node is a link to another node. Because the + links are upward, that is, bottom-up, and we seek a purely + functional implementation, we need to uncouple the nodes and + the items here, so the first component of [Link] is an item, + not a node. That is why the type [node] is not recursive, + and called [node], not [tree]: to become a traversable tree, + it needs to be complemented by the type [partition] below to + associate items back to nodes. In order to follow a path + upward in the tree until the root, we start from a link node + giving us the next item, then find the node corresponding to + the item thanks to [partition], and again until we arrive at + the root. + + The height component is that of the source of the link, that + is, [h] is the height of the node linking to the node [Link + (j,h)], _not_ of [j], except when [equal i j]. *) + + module ItemMap = Map.Make (Item) + + (** The type [partition] implements a partition of classes of + equivalent items by means of a map from items to nodes of type + [node] in trees. *) + type partition = node ItemMap.t + + type t = partition + + let empty = ItemMap.empty + + let root (item, height) = ItemMap.add item (Root height) + + let link (src, height) dst = ItemMap.add src (Link (dst, height)) + + let rec seek (i: item) (p: partition) : repr * height = + match ItemMap.find i p with + Root hi -> i,hi + | Link (j,_) -> seek j p + + let repr item partition = fst (seek item partition) + + let is_equiv (i: item) (j: item) (p: partition) = + equal (repr i p) (repr j p) + + let get_or_set (i: item) (p: partition) = + try seek i p, p with + Not_found -> let n = i,0 in (n, root n p) + + let equiv (i: item) (j: item) (p: partition) : partition = + let (ri,hi as ni), p = get_or_set i p in + let (rj,hj as nj), p = get_or_set j p in + if equal ri rj + then p + else if hi > hj + then link nj ri p + else link ni rj (if hi < hj then p else root (rj, hj+1) p) + + (** The call [alias i j p] results in the same partition as [equiv + i j p], except that [i] is not the representative of its class + in [alias i j p] (whilst it may be in [equiv i j p]). + + This property is irrespective of the heights of the + representatives of [i] and [j], that is, of the trees + implementing their classes. If [i] is not a representative of + its class before calling [alias], then the height criteria is + applied (which, without the constraint above, would yield a + height-balanced new tree). *) + let alias (i: item) (j: item) (p: partition) : partition = + let (ri,hi as ni), p = get_or_set i p in + let (rj,hj as nj), p = get_or_set j p in + if equal ri rj + then p + else if hi = hj || equal ri i + then link ni rj @@ root (rj, max hj (hi+1)) p + else if hi < hj then link ni rj p + else link nj ri p + + (** {1 Printing} *) + + let print (p: partition) = + let print i node = + let hi, hj, j = + match node with + Root hi -> hi,hi,i + | Link (j,hi) -> + match ItemMap.find j p with + Root hj | Link (_,hj) -> hi,hj,j in + Printf.printf "%s,%d -> %s,%d\n" + (Item.to_string i) hi (Item.to_string j) hj + in ItemMap.iter print p + + end diff --git a/src/union_find/Partition3.ml b/src/union_find/Partition3.ml new file mode 100644 index 000000000..593292025 --- /dev/null +++ b/src/union_find/Partition3.ml @@ -0,0 +1,86 @@ +(* Destructive implementation of union/find with height-balanced + forests but without path compression: O(n*log(n)). *) + +module Make (Item: Partition.Item) = + struct + + type item = Item.t + type repr = item (** Class representatives *) + + let equal i j = Item.compare i j = 0 + + type height = int + + (** Each equivalence class is implemented by a Catalan tree linked + upwardly and otherwise is a link to another node. Those trees + are height-balanced. The type [node] implements nodes in those + trees. *) + type node = {item: item; mutable height: int; mutable parent: node} + + module ItemMap = Map.Make (Item) + + (** The type [partition] implements a partition of classes of + equivalent items by means of a map from items to nodes of type + [node] in trees. *) + type partition = node ItemMap.t + + type t = partition + + let empty = ItemMap.empty + + (** The function [repr] is faster than a persistent implementation + in the worst case because, in the latter case, the cost is O(log n) + for accessing each node in the path to the root, whereas, in the + former, only the access to the first node in the path incurs a cost + of O(log n) -- the other nodes are accessed in constant time by + following the [next] field of type [node]. *) + let seek (i: item) (p: partition) : node = + let rec find_root node = + if node.parent == node then node else find_root node.parent + in find_root (ItemMap.find i p) + + let repr item partition = (seek item partition).item + + let is_equiv (i: item) (j: item) (p: partition) = + equal (repr i p) (repr j p) + + let get_or_set item (p: partition) = + try seek item p, p with + Not_found -> let rec loop = {item; height=0; parent=loop} + in loop, ItemMap.add item loop p + + let link src dst = src.parent <- dst + + let equiv (i: item) (j: item) (p: partition) : partition = + let ni,p = get_or_set i p in + let nj,p = get_or_set j p in + let hi,hj = ni.height, nj.height in + let () = + if not (equal ni.item nj.item) + then if hi > hj + then link nj ni + else (link ni nj; nj.height <- max hj (hi+1)) + in p + + let alias (i: item) (j: item) (p: partition) : partition = + let ni,p = get_or_set i p in + let nj,p = get_or_set j p in + let hi,hj = ni.height, nj.height in + let () = + if not (equal ni.item nj.item) + then if hi = hj || equal ni.item i + then (link ni nj; nj.height <- max hj (hi+1)) + else if hi < hj then link ni nj + else link nj ni + in p + + (* Printing *) + + let print p = + let print _ node = + Printf.printf "%s,%d -> %s,%d\n" + (Item.to_string node.item) node.height + (Item.to_string node.parent.item) node.parent.height + in ItemMap.iter print p + + end diff --git a/src/union_find/PartitionMain.ml b/src/union_find/PartitionMain.ml new file mode 100644 index 000000000..4e69dbd87 --- /dev/null +++ b/src/union_find/PartitionMain.ml @@ -0,0 +1,40 @@ +module Int = + struct + type t = int + let compare (i: int) (j: int) = Pervasives.compare i j + let to_string = string_of_int + end + +module Test (Part: Partition.S with type item = Int.t) = + struct + open Part + + let () = empty + |> equiv 4 3 + |> equiv 3 8 + |> equiv 6 5 + |> equiv 9 4 + |> equiv 2 1 + |> equiv 8 9 + |> equiv 5 0 + |> equiv 7 2 + |> equiv 6 1 + |> equiv 1 0 + |> equiv 6 7 + |> equiv 8 0 + |> equiv 7 7 + |> equiv 10 10 + |> print + end + + +module Test0 = Test (Partition0.Make(Int)) +let () = print_newline () + +module Test1 = Test (Partition1.Make(Int)) +let () = print_newline () + +module Test2 = Test (Partition2.Make(Int)) +let () = print_newline () + +module Test3 = Test (Partition3.Make(Int)) diff --git a/src/union_find/README.md b/src/union_find/README.md new file mode 100644 index 000000000..16c7b5bf9 --- /dev/null +++ b/src/union_find/README.md @@ -0,0 +1,39 @@ +# Some implementations in OCaml of the Union/Find algorithm + +All modules implementing Union/Find can be coerced by the same +signature `Partition.S`. + +Note the function `alias` which is equivalent to `equiv`, but not +symmetric: `alias x y` means that `x` is an alias of `y`, which +translates in the present context as `x` not being the representative +of the equivalence class containing the equivalence between `x` and +`y`. The function `alias` is useful when managing aliases during the +static analyses of programming languages, so the representatives of +the classes are always the original object. + +The module `PartitionMain` tests each with the same equivalence +relations. + +## `Partition0.ml` + +This is a naive, persistent implementation of Union/Find featuring an +asymptotic worst case cost of O(n^2). + +## `Partition1.ml` + +This is a persistent implementation of Union/Find with height-balanced +forests and without path compression, featuring an asymptotic worst +case cost of O(n*log(n)). + +## `Partition2.ml` + +This is an alternate version of `Partition1.ml`, using a different +data type. + +## `Partition3.ml` + +This is a destructive implementation of Union/Find with +height-balanced forests but without path compression, featuring an +asymptotic worst case of O(n*log(n)). In practice, though, this +implementation should be faster than the previous ones, due to a +smaller multiplicative constant term. diff --git a/src/union_find/build.sh b/src/union_find/build.sh new file mode 100755 index 000000000..8453429fa --- /dev/null +++ b/src/union_find/build.sh @@ -0,0 +1,14 @@ +#!/bin/sh +set -x +ocamlfind ocamlc -strict-sequence -w +A-48-4 -c Partition.mli +ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition0.ml +ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition2.ml +ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition1.ml +ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition3.ml +ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition1.ml +ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition3.ml +ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition0.ml +ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c Partition2.ml +ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c PartitionMain.ml +ocamlfind ocamlopt -strict-sequence -w +A-48-4 -c PartitionMain.ml +ocamlfind ocamlopt -o PartitionMain.opt Partition0.cmx Partition1.cmx Partition2.cmx Partition3.cmx PartitionMain.cmx diff --git a/src/union_find/clean.sh b/src/union_find/clean.sh new file mode 100755 index 000000000..75ded7c50 --- /dev/null +++ b/src/union_find/clean.sh @@ -0,0 +1,3 @@ +#!/bin/sh + +\rm -f *.cmi *.cmo *.cmx *.o *.byte *.opt diff --git a/src/union_find/dune b/src/union_find/dune new file mode 100644 index 000000000..a4c27e725 --- /dev/null +++ b/src/union_find/dune @@ -0,0 +1,16 @@ +(library + (name union_find) + (public_name ligo.union_find) + (wrapped false) ;; TODO: do we need this? + (modules Partition0 Partition1 Partition2 Partition3 Partition Union_find) + (modules_without_implementation Partition) +;; (preprocess +;; (pps simple-utils.ppx_let_generalized) +;; ) +;; (flags (:standard -w +1..62-4-9-44-40-42-48-30@39@33 -open Simple_utils )) + ) + +(test + (modules PartitionMain) + (libraries UnionFind) + (name PartitionMain)) diff --git a/src/union_find/union_find.ml b/src/union_find/union_find.ml new file mode 100644 index 000000000..17850f743 --- /dev/null +++ b/src/union_find/union_find.ml @@ -0,0 +1,2 @@ +module Partition = Partition +module Partition0 = Partition0 diff --git a/vendors/ligo-utils/simple-utils/trace.ml b/vendors/ligo-utils/simple-utils/trace.ml index 329203a46..1ae5360dd 100644 --- a/vendors/ligo-utils/simple-utils/trace.ml +++ b/vendors/ligo-utils/simple-utils/trace.ml @@ -667,6 +667,7 @@ let bind_map_pair f (a, b) = bind_pair (f a, f b) + (** Wraps a call that might trigger an exception in a result. *)