From 174c028406399bee644d2ec020b5db58833cd04d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Sun, 27 Oct 2019 23:24:21 -0400 Subject: [PATCH] Fixing issues in the new typer --- src/passes/4-typer/solver.ml | 109 +++++++++++++++++++------- src/passes/4-typer/typer.ml | 11 ++- src/passes/6-transpiler/transpiler.ml | 12 ++- src/stages/ast_typed/environment.ml | 5 +- src/stages/typesystem/misc.ml | 16 +++- src/test/test.ml | 3 +- src/union_find/dune | 2 +- 7 files changed, 120 insertions(+), 38 deletions(-) diff --git a/src/passes/4-typer/solver.ml b/src/passes/4-typer/solver.ml index eaaef767b..b940422e0 100644 --- a/src/passes/4-typer/solver.ml +++ b/src/passes/4-typer/solver.ml @@ -7,6 +7,21 @@ module Wrap = struct module T = Ast_typed module O = Core + module Errors = struct + + let unknown_type_constructor (ctor : string) (te : T.type_value) () = + let title = (thunk "unknown type constructor") in + (* TODO: sanitize the "ctor" argument before displaying it. *) + let message () = ctor in + let data = [ + ("ctor" , fun () -> ctor) ; + ("expression" , fun () -> Format.asprintf "%a" T.PP.type_value te) ; + (* ("location" , fun () -> Format.asprintf "%a" Location.pp te.location) *) (* TODO *) + ] in + error ~data title message () + end + + type constraints = O.type_constraint list (* let add_type state t = *) @@ -30,16 +45,33 @@ module Wrap = struct | 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 "unknown type constructor") + | "arrow" -> C_arrow + | "option" -> C_option + | "tuple" -> C_tuple + (* record *) + (* variant *) + | "map" -> C_map + | "big_map" -> C_map + | "list" -> C_list + | "set" -> C_set + | "unit" -> C_unit + | "bool" -> C_bool + | "string" -> C_string + | "nat" -> C_nat + | "mutez" -> C_tez (* TODO: rename tez to mutez*) + | "timestamp" -> C_timestamp + | "int" -> C_int + | "address" -> C_address + | "bytes" -> C_bytes + | "key_hash" -> C_key_hash + | "key" -> C_key + | "signature" -> C_signature + | "operation" -> C_operation + | "contract" -> C_contract + | unknown -> + (* TODO: return a Trace.result *) + let _ = fail (fun () -> Errors.unknown_type_constructor unknown te ()) in + failwith ("unknown type constructor " ^ unknown)) in P_constant (csttag, List.map type_expression_to_type_value args) @@ -336,10 +368,6 @@ 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 *) @@ -521,7 +549,8 @@ let normalizer_assignments : (type_constraint_simpl , type_constraint_simpl) nor | _ -> (dbs , [new_constraint]) -let type_level_eval : type_value -> type_value * type_constraint list = failwith "implemented in other branch" +let type_level_eval : type_value -> type_value * type_constraint list = + fun tv -> Typesystem.Misc.Substitution.Pattern.eval_beta_root ~tv let check_applied ((reduced, _new_constraints) as x) = let () = match reduced with @@ -972,10 +1001,10 @@ let select_and_propagate_all' : _ -> type_constraint_simpl selector_input -> str (* Takes a list of constraints, applies all selector+propagator pairs to each in turn. *) -let rec select_and_propagate_all : _ -> type_constraint selector_input list -> structured_dbs -> structured_dbs = +let rec select_and_propagate_all : _ -> type_constraint selector_input list -> structured_dbs -> _ * structured_dbs = fun already_selected new_constraints dbs -> match new_constraints with - | [] -> dbs + | [] -> (already_selected, dbs) | new_constraint :: tl -> let { state = dbs ; list = modified_constraints } = normalizers new_constraint dbs in let (already_selected , new_constraints' , dbs) = @@ -998,21 +1027,40 @@ let rec select_and_propagate_all : _ -> type_constraint selector_input list -> s (* 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 ; + * } *) + 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 ; + structured_dbs : structured_dbs ; + already_selected : already_selected ; } -let initial_state : state = { - unification_vars = UF.empty ; - constraints = TypeVariableMap.empty ; - assignments = TypeVariableMap.empty ; +let initial_state : state = (* { + * unification_vars = UF.empty ; + * constraints = TypeVariableMap.empty ; + * assignments = TypeVariableMap.empty ; + * } *) +{ + structured_dbs = + { + all_constraints = [] ; (* type_constraint_simpl list *) + aliases = UF.empty ; (* unionfind *) + assignments = TypeVariableMap.empty; (* c_constructor_simpl TypeVariableMap.t *) + grouped_by_variable = TypeVariableMap.empty; (* constraints TypeVariableMap.t *) + cycle_detection_toposort = (); (* unit *) + } ; + already_selected = { + break_ctor = M_break_ctor.AlreadySelected.empty ; + specialize1 = M_specialize1.AlreadySelected.empty ; + } } (* This function is called when a program is fully compiled, and the @@ -1045,7 +1093,8 @@ let discard_state (_ : state) = () let aggregate_constraints : state -> type_constraint list -> state result = fun state newc -> (* TODO: Iterate over constraints *) let _todo = ignore (state, newc) in - failwith "TODO" + let (a, b) = select_and_propagate_all state.already_selected newc state.structured_dbs in + ok { already_selected = a ; structured_dbs = b } (*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 906766540..d743aa11f 100644 --- a/src/passes/4-typer/typer.ml +++ b/src/passes/4-typer/typer.ml @@ -920,7 +920,7 @@ let untype_type_value (t:O.type_value) : (I.type_expression) result = (* TODO: we ended up with two versions of type_program… ??? *) (* -Apply type_declaration on all the node of the AST_simplified from the root p +Apply type_declaration on all the node of the AST_simplified from the root p *) let type_program_returns_state (p:I.program) : (environment * Solver.state * O.program) result = let env = Ast_typed.Environment.full_empty in @@ -941,7 +941,14 @@ let type_program_returns_state (p:I.program) : (environment * Solver.state * O.p let type_program (p : I.program) : (O.program * Solver.state) result = let%bind (env, state, program) = type_program_returns_state p in - let program = let () = failwith "TODO : subst all" in let _todo = ignore (env, state) in program in + let subst_all = + let assignments = state.structured_dbs.assignments in + let aux (v : O.type_name) (expr : Solver.c_constructor_simpl) (p:O.program) = + Typesystem.Misc.Substitution.Pattern.program ~p ~v ~expr in + let p = SMap.fold aux assignments program in + p in + let program = subst_all in + let () = ignore env in (* TODO: shouldn't we use the `env` somewhere? *) ok (program, state) (* diff --git a/src/passes/6-transpiler/transpiler.ml b/src/passes/6-transpiler/transpiler.ml index 9d53b6ea3..66e841689 100644 --- a/src/passes/6-transpiler/transpiler.ml +++ b/src/passes/6-transpiler/transpiler.ml @@ -102,6 +102,13 @@ them. please report this to the developers." in ("value" , fun () -> Format.asprintf "%a" Mini_c.PP.value value) ; ] in error ~data title content + + let not_found content = + let title () = "Not_found" in + let content () = content in + let data = [ + ] in + error ~data title content end open Errors @@ -539,7 +546,10 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re let%bind ty'_map = bind_map_smap transpile_type ty_map in let%bind path = record_access_to_lr ty' ty'_map prop in let path' = List.map snd path in - ok (Map.String.find prop ty_map, acc @ path') + let%bind prop_in_ty_map = trace_option + (Errors.not_found "acessing prop in ty_map [TODO: better error message]") + (Map.String.find_opt prop ty_map) in + ok (prop_in_ty_map, acc @ path') ) | Access_map _k -> fail (corner_case ~loc:__LOC__ "no patch for map yet") in diff --git a/src/stages/ast_typed/environment.ml b/src/stages/ast_typed/environment.ml index 673f8645f..6281f0094 100644 --- a/src/stages/ast_typed/environment.ml +++ b/src/stages/ast_typed/environment.ml @@ -43,7 +43,10 @@ let get_constructor : string -> t -> (type_value * type_value) option = fun k x let aux = fun x -> let aux = fun (_type_name , x) -> match x.type_value' with - | T_sum m when Map.String.mem k m -> Some (Map.String.find k m , x) + | T_sum m -> + (match Map.String.find_opt k m with + Some km -> Some (km , x) + | None -> None) | _ -> None in List.find_map aux (Small.get_type_environment x) in diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml index 96baf197b..096a5cea8 100644 --- a/src/stages/typesystem/misc.ml +++ b/src/stages/typesystem/misc.ml @@ -6,10 +6,17 @@ module Substitution = struct module Pattern = struct + let rec declaration ~(d : Ast_typed.declaration Location.wrap) ~v ~expr : Ast_typed.declaration Location.wrap = + let _TODO = (d, v, expr) in + failwith "TODO: subst declaration" + + and program ~(p : Ast_typed.program) ~v ~expr : Ast_typed.program = + List.map (fun d -> declaration ~d ~v ~expr) p + (* Computes `P[v := expr]`. *) - let rec type_value ~tv ~v ~expr = + and type_value ~tv ~v ~expr = let self tv = type_value ~tv ~v ~expr in match tv with | P_variable v' when v' = v -> expr @@ -52,6 +59,13 @@ module Substitution = struct and typeclass ~tc ~v ~expr = List.map (List.map (fun tv -> type_value ~tv ~v ~expr)) tc + (* Performs beta-reduction at the root of the type *) + let eval_beta_root ~(tv : type_value) = + match tv with + P_apply (P_forall { binder; constraints; body }, arg) -> + let constraints = List.map (fun c -> constraint_ ~c ~v:binder ~expr:arg) constraints in + (type_value ~tv:body ~v:binder ~expr:arg , constraints) + | _ -> (tv , []) end end diff --git a/src/test/test.ml b/src/test/test.ml index a3709700e..aebade390 100644 --- a/src/test/test.ml +++ b/src/test/test.ml @@ -2,9 +2,8 @@ open Test_helpers - let () = - (* Printexc.record_backtrace true ; *) + Printexc.record_backtrace true ; run_test @@ test_suite "LIGO" [ Integration_tests.main ; Compiler_tests.main ; diff --git a/src/union_find/dune b/src/union_find/dune index a4c27e725..fad355c7a 100644 --- a/src/union_find/dune +++ b/src/union_find/dune @@ -12,5 +12,5 @@ (test (modules PartitionMain) - (libraries UnionFind) + (libraries union_find) (name PartitionMain))