From 861ab57a431864d668f5527d20696651f83c9ad3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Tue, 2 Jun 2020 15:04:03 +0100 Subject: [PATCH 1/3] move solver_types to typesystem/ (because of dependencies. It should be merged with the AST really) --- src/passes/8-typer-new/heuristic_break_ctor.ml | 2 +- src/passes/8-typer-new/heuristic_specialize1.ml | 2 +- src/passes/8-typer-new/normalizer.ml | 2 +- src/passes/8-typer-new/solver.ml | 2 +- src/{passes/8-typer-new => stages/typesystem}/solver_types.ml | 0 src/stages/typesystem/typesystem.ml | 1 + 6 files changed, 5 insertions(+), 4 deletions(-) rename src/{passes/8-typer-new => stages/typesystem}/solver_types.ml (100%) diff --git a/src/passes/8-typer-new/heuristic_break_ctor.ml b/src/passes/8-typer-new/heuristic_break_ctor.ml index e676f2500..1c0c63e60 100644 --- a/src/passes/8-typer-new/heuristic_break_ctor.ml +++ b/src/passes/8-typer-new/heuristic_break_ctor.ml @@ -3,7 +3,7 @@ open Ast_typed.Misc open Ast_typed.Types -open Solver_types +open Typesystem.Solver_types let selector : (type_constraint_simpl, output_break_ctor) selector = (* find two rules with the shape x = k(var …) and x = k'(var' …) *) diff --git a/src/passes/8-typer-new/heuristic_specialize1.ml b/src/passes/8-typer-new/heuristic_specialize1.ml index 6e481fc12..271f695f6 100644 --- a/src/passes/8-typer-new/heuristic_specialize1.ml +++ b/src/passes/8-typer-new/heuristic_specialize1.ml @@ -6,7 +6,7 @@ module Core = Typesystem.Core open Ast_typed.Misc open Ast_typed.Types -open Solver_types +open Typesystem.Solver_types let selector : (type_constraint_simpl, output_specialize1) selector = (* find two rules with the shape (x = forall b, d) and x = k'(var' …) or vice versa *) diff --git a/src/passes/8-typer-new/normalizer.ml b/src/passes/8-typer-new/normalizer.ml index 8c391c2d5..5c6549c03 100644 --- a/src/passes/8-typer-new/normalizer.ml +++ b/src/passes/8-typer-new/normalizer.ml @@ -2,7 +2,7 @@ module Core = Typesystem.Core module Map = RedBlackTrees.PolyMap open Ast_typed.Misc open Ast_typed.Types -open Solver_types +open Typesystem.Solver_types (* sub-sub component: constraint normalizer: remove dupes and give structure * right now: union-find of unification vars diff --git a/src/passes/8-typer-new/solver.ml b/src/passes/8-typer-new/solver.ml index 0bcbe1260..c302befaf 100644 --- a/src/passes/8-typer-new/solver.ml +++ b/src/passes/8-typer-new/solver.ml @@ -4,7 +4,7 @@ module Map = RedBlackTrees.PolyMap module Set = RedBlackTrees.PolySet module UF = UnionFind.Poly2 open Ast_typed.Types -open Solver_types +open Typesystem.Solver_types (* sub-sub component: lazy selector (don't re-try all selectors every time) * For now: just re-try everytime *) diff --git a/src/passes/8-typer-new/solver_types.ml b/src/stages/typesystem/solver_types.ml similarity index 100% rename from src/passes/8-typer-new/solver_types.ml rename to src/stages/typesystem/solver_types.ml diff --git a/src/stages/typesystem/typesystem.ml b/src/stages/typesystem/typesystem.ml index 75d8ee5b8..852d7543c 100644 --- a/src/stages/typesystem/typesystem.ml +++ b/src/stages/typesystem/typesystem.ml @@ -1,3 +1,4 @@ module Core = Core module Shorthands = Shorthands module Misc = Misc +module Solver_types = Solver_types From 7257aaaff40d57a1a79bd814603f212c77d9dbdb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Tue, 2 Jun 2020 20:34:23 +0100 Subject: [PATCH 2/3] Solver: use a list of heuristics instead of hardcoding them. --- src/main/compile/of_core.ml | 6 +- src/passes/8-typer-new/PP.ml | 7 ++- .../8-typer-new/heuristic_break_ctor.ml | 2 + .../8-typer-new/heuristic_specialize1.ml | 2 + src/passes/8-typer-new/solver.ml | 61 +++++++++---------- src/passes/8-typer-new/typer.ml | 37 +++++------ src/passes/8-typer-new/typer.mli | 9 +-- src/passes/8-typer-old/typer.ml | 7 ++- src/passes/8-typer-old/typer.mli | 7 ++- src/passes/8-typer/typer.ml | 1 + src/passes/8-typer/typer.mli | 5 +- src/stages/4-ast_typed/ast.ml | 5 -- src/stages/typesystem/core.ml | 2 +- src/stages/typesystem/solver_types.ml | 16 +++++ src/test/test_helpers.ml | 6 +- 15 files changed, 95 insertions(+), 78 deletions(-) diff --git a/src/main/compile/of_core.ml b/src/main/compile/of_core.ml index 6e1eb30b6..27c6f6b55 100644 --- a/src/main/compile/of_core.ml +++ b/src/main/compile/of_core.ml @@ -4,7 +4,7 @@ type form = | Contract of string | Env -let compile (cform: form) (program : Ast_core.program) : (Ast_typed.program * Ast_typed.typer_state) result = +let compile (cform: form) (program : Ast_core.program) : (Ast_typed.program * Typesystem.Solver_types.typer_state) result = let%bind (prog_typed , state) = Typer.type_program program in let () = Typer.Solver.discard_state state in let%bind applied = Self_ast_typed.all_program prog_typed in @@ -13,8 +13,8 @@ let compile (cform: form) (program : Ast_core.program) : (Ast_typed.program * As | Env -> ok applied in ok @@ (applied', state) -let compile_expression ?(env = Ast_typed.Environment.empty) ~(state : Ast_typed.typer_state) (e : Ast_core.expression) - : (Ast_typed.expression * Ast_typed.typer_state) result = +let compile_expression ?(env = Ast_typed.Environment.empty) ~(state : Typesystem.Solver_types.typer_state) (e : Ast_core.expression) + : (Ast_typed.expression * Typesystem.Solver_types.typer_state) result = let%bind (ae_typed,state) = Typer.type_expression_subst env state e in let () = Typer.Solver.discard_state state in let%bind ae_typed' = Self_ast_typed.all_expression ae_typed in diff --git a/src/passes/8-typer-new/PP.ml b/src/passes/8-typer-new/PP.ml index c5199f60d..9ef484180 100644 --- a/src/passes/8-typer-new/PP.ml +++ b/src/passes/8-typer-new/PP.ml @@ -1,4 +1,5 @@ open Ast_typed +open Typesystem.Solver_types open Format module UF = UnionFind.Poly2 @@ -47,10 +48,10 @@ let structured_dbs : _ -> structured_dbs -> unit = fun ppf structured_dbs -> let { all_constraints = a ; aliases = b ; _ } = structured_dbs in fprintf ppf "STRUCTURED_DBS\n %a\n %a" all_constraints a aliases b -let already_selected : _ -> already_selected -> unit = fun ppf already_selected -> +let already_selected_and_propagators : _ -> ex_propagator_heuristic list -> unit = fun ppf already_selected -> let _ = already_selected in fprintf ppf "ALREADY_SELECTED" let state : _ -> typer_state -> unit = fun ppf state -> - let { structured_dbs=a ; already_selected=b } = state in - fprintf ppf "STATE %a %a" structured_dbs a already_selected b + let { structured_dbs=a ; already_selected_and_propagators =b } = state in + fprintf ppf "STATE %a %a" structured_dbs a already_selected_and_propagators b diff --git a/src/passes/8-typer-new/heuristic_break_ctor.ml b/src/passes/8-typer-new/heuristic_break_ctor.ml index 1c0c63e60..6c145173f 100644 --- a/src/passes/8-typer-new/heuristic_break_ctor.ml +++ b/src/passes/8-typer-new/heuristic_break_ctor.ml @@ -50,3 +50,5 @@ let propagator : output_break_ctor propagator = let eqs3 = List.map2 (fun aa bb -> c_equation { tsrc = "solver: propagator: break_ctor aa" ; t = P_variable aa} { tsrc = "solver: propagator: break_ctor bb" ; t = P_variable bb} "propagator: break_ctor") a.tv_list b.tv_list in let eqs = eq1 :: eqs3 in (eqs , []) (* no new assignments *) + +let heuristic = Propagator_heuristic { selector ; propagator ; empty_already_selected = Set.create ~cmp:Solver_should_be_generated.compare_output_break_ctor } diff --git a/src/passes/8-typer-new/heuristic_specialize1.ml b/src/passes/8-typer-new/heuristic_specialize1.ml index 271f695f6..37e4f206c 100644 --- a/src/passes/8-typer-new/heuristic_specialize1.ml +++ b/src/passes/8-typer-new/heuristic_specialize1.ml @@ -51,3 +51,5 @@ let propagator : output_specialize1 propagator = let eq1 = c_equation { tsrc = "solver: propagator: specialize1 eq1" ; t = P_variable b.tv } reduced "propagator: specialize1" in let eqs = eq1 :: new_constraints in (eqs, []) (* no new assignments *) + +let heuristic = Propagator_heuristic { selector ; propagator ; empty_already_selected = Set.create ~cmp:Solver_should_be_generated.compare_output_specialize1 } diff --git a/src/passes/8-typer-new/solver.ml b/src/passes/8-typer-new/solver.ml index c302befaf..48990d294 100644 --- a/src/passes/8-typer-new/solver.ml +++ b/src/passes/8-typer-new/solver.ml @@ -12,7 +12,7 @@ open Typesystem.Solver_types (* TODO : with our selectors, the selection depends on the order in which the constraints are added :-( :-( :-( :-( We need to return a lazy stream of constraints. *) -let select_and_propagate : ('old_input, 'selector_output) selector -> _ propagator -> _ -> 'a -> structured_dbs -> _ * new_constraints * new_assignments = +let select_and_propagate : ('old_input, 'selector_output) selector -> 'selector_output propagator -> 'selector_output poly_set -> 'old_input -> structured_dbs -> 'selector_output poly_set * new_constraints * new_assignments = fun selector propagator -> fun already_selected old_type_constraint dbs -> (* TODO: thread some state to know which selector outputs were already seen *) @@ -27,40 +27,35 @@ let select_and_propagate : ('old_input, 'selector_output) selector -> _ propagat | WasNotSelected -> (already_selected, [] , []) -(* TODO: put the heuristics with their state in a list. *) -let select_and_propagate_break_ctor = select_and_propagate Heuristic_break_ctor.selector Heuristic_break_ctor.propagator -let select_and_propagate_specialize1 = select_and_propagate Heuristic_specialize1.selector Heuristic_specialize1.propagator +let aux sel_propag new_constraint (already_selected , new_constraints , dbs) = + let (already_selected , new_constraints', new_assignments) = sel_propag already_selected new_constraint dbs in + let assignments = List.fold_left (fun acc ({tv;c_tag=_;tv_list=_} as ele) -> Map.update tv (function None -> Some ele | x -> x) acc) dbs.assignments new_assignments in + let dbs = { dbs with assignments } in + (already_selected , new_constraints' @ new_constraints , dbs) + +let step = fun (Propagator_heuristic { selector; propagator; empty_already_selected }) dbs new_constraint new_constraints -> + let (already_selected , new_constraints , dbs) = aux (select_and_propagate selector propagator) new_constraint (empty_already_selected , new_constraints , dbs) in + Propagator_heuristic { selector; propagator; empty_already_selected=already_selected }, new_constraints, dbs (* Takes a constraint, applies all selector+propagator pairs to it. Keeps track of which constraints have already been selected. *) -let select_and_propagate_all' : _ -> type_constraint_simpl selector_input -> structured_dbs -> _ * new_constraints * structured_dbs = - let aux sel_propag new_constraint (already_selected , new_constraints , dbs) = - let (already_selected , new_constraints', new_assignments) = sel_propag already_selected new_constraint dbs in - let assignments = List.fold_left (fun acc ({tv;c_tag=_;tv_list=_} as ele) -> Map.update tv (function None -> Some ele | x -> x) acc) dbs.assignments new_assignments in - let dbs = { dbs with assignments } in - (already_selected , new_constraints' @ new_constraints , dbs) - in - fun already_selected new_constraint dbs -> +let select_and_propagate_all' : ex_propagator_heuristic list -> type_constraint_simpl selector_input -> structured_dbs -> ex_propagator_heuristic list * new_constraints * structured_dbs = + fun already_selected_and_propagators new_constraint dbs -> (* The order in which the propagators are applied to constraints is entirely accidental (dfs/bfs/something in-between). *) - let (already_selected , new_constraints , dbs) = (already_selected , [] , dbs) in - - (* We must have a different already_selected for each selector, - so this is more verbose than a few uses of `aux'. *) - let (already_selected' , new_constraints , dbs) = aux select_and_propagate_break_ctor new_constraint (already_selected.break_ctor , new_constraints , dbs) in - let (already_selected , new_constraints , dbs) = ({already_selected with break_ctor = already_selected'}, new_constraints , dbs) in - - let (already_selected' , new_constraints , dbs) = aux select_and_propagate_specialize1 new_constraint (already_selected.specialize1 , new_constraints , dbs) in - let (already_selected , new_constraints , dbs) = ({already_selected with specialize1 = already_selected'}, new_constraints , dbs) in - - (already_selected , new_constraints , dbs) + List.fold_left + (fun (hs , new_constraints , dbs) sp -> + let (h , a , b) = step sp dbs new_constraint new_constraints in + (h :: hs , a , b)) + ([], [] , dbs) + already_selected_and_propagators (* 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 = - fun already_selected new_constraints dbs -> +let rec select_and_propagate_all : ex_propagator_heuristic list -> type_constraint selector_input list -> structured_dbs -> ex_propagator_heuristic list * structured_dbs = + fun already_selected_and_propagators new_constraints dbs -> match new_constraints with - | [] -> (already_selected, dbs) + | [] -> (already_selected_and_propagators, dbs) | new_constraint :: tl -> let { state = dbs ; list = modified_constraints } = Normalizer.normalizers new_constraint dbs in let (already_selected , new_constraints' , dbs) = @@ -68,7 +63,7 @@ let rec select_and_propagate_all : _ -> type_constraint selector_input list -> s (fun (already_selected , nc , dbs) c -> let (already_selected , new_constraints' , dbs) = select_and_propagate_all' already_selected c dbs in (already_selected , new_constraints' @ nc , dbs)) - (already_selected , [] , dbs) + (already_selected_and_propagators , [] , dbs) modified_constraints in let new_constraints = new_constraints' @ tl in select_and_propagate_all already_selected new_constraints dbs @@ -88,10 +83,10 @@ let initial_state : typer_state = { grouped_by_variable = (Map.create ~cmp:Var.compare : (type_variable, constraints) Map.t); cycle_detection_toposort = (); } ; - already_selected = { - break_ctor = Set.create ~cmp:Solver_should_be_generated.compare_output_break_ctor; - specialize1 = Set.create ~cmp:Solver_should_be_generated.compare_output_specialize1 ; - } + already_selected_and_propagators = [ + Heuristic_break_ctor.heuristic ; + Heuristic_specialize1.heuristic ; + ] } (* This function is called when a program is fully compiled, and the @@ -107,8 +102,8 @@ let discard_state (_ : typer_state) = () let aggregate_constraints : typer_state -> type_constraint list -> typer_state result = fun state newc -> (* TODO: Iterate over constraints *) let _todo = ignore (state, newc) in - let (a, b) = select_and_propagate_all state.already_selected newc state.structured_dbs in - ok { already_selected = a ; structured_dbs = b } + let (a, b) = select_and_propagate_all state.already_selected_and_propagators newc state.structured_dbs in + ok { already_selected_and_propagators = a ; structured_dbs = b } (*let { constraints ; eqv } = state in ok { constraints = constraints @ newc ; eqv }*) diff --git a/src/passes/8-typer-new/typer.ml b/src/passes/8-typer-new/typer.ml index 604740583..d81a8e690 100644 --- a/src/passes/8-typer-new/typer.ml +++ b/src/passes/8-typer-new/typer.ml @@ -1,6 +1,7 @@ open Trace module I = Ast_core module O = Ast_typed +module O' = Typesystem.Solver_types open O.Combinators module DEnv = Environment module Environment = O.Environment @@ -15,7 +16,7 @@ open Todo_use_fold_generator (* Extract pairs of (name,type) in the declaration and add it to the environment *) -let rec type_declaration env state : I.declaration -> (environment * O.typer_state * O.declaration option) result = function +let rec type_declaration env state : I.declaration -> (environment * O'.typer_state * 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 @@ -32,7 +33,7 @@ let rec type_declaration env state : I.declaration -> (environment * O.typer_sta ok (post_env, state' , Some (O.Declaration_constant { binder ; expr ; inline} )) ) -and type_match : environment -> O.typer_state -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> (O.matching_expr * O.typer_state) result = +and type_match : environment -> O'.typer_state -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> (O.matching_expr * O'.typer_state) result = fun e state t i ae loc -> match i with | Match_option {match_none ; match_some} -> let%bind tv = @@ -188,11 +189,11 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression resu in return (T_operator (opt)) -and type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result = fun e state ?tv_opt ae -> +and type_expression : environment -> O'.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O'.typer_state) result = fun e state ?tv_opt ae -> let () = ignore tv_opt in (* For compatibility with the old typer's API, this argument can be removed once the new typer is used. *) let open Solver in let module L = Logger.Stateful() in - let return : _ -> O.typer_state -> _ -> _ (* return of type_expression *) = fun expr state constraints type_name -> + let return : _ -> O'.typer_state -> _ -> _ (* return of type_expression *) = fun expr state constraints type_name -> let%bind new_state = aggregate_constraints state constraints in let tv = t_variable type_name () in let location = ae.location in @@ -430,8 +431,8 @@ and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type ok(name, tv) (* Apply type_declaration on every node of the AST_core from the root p *) -let type_program_returns_state ((env, state, p) : environment * O.typer_state * I.program) : (environment * O.typer_state * O.program) result = - let aux ((e : environment), (s : O.typer_state) , (ds : O.declaration Location.wrap list)) (d:I.declaration Location.wrap) = +let type_program_returns_state ((env, state, p) : environment * O'.typer_state * I.program) : (environment * O'.typer_state * O.program) result = + let aux ((e : environment), (s : O'.typer_state) , (ds : O.declaration Location.wrap list)) (d:I.declaration Location.wrap) = let%bind (e' , s' , d'_opt) = type_declaration e s (Location.unwrap d) in let ds' = match d'_opt with | None -> ds @@ -445,7 +446,7 @@ let type_program_returns_state ((env, state, p) : environment * O.typer_state * let declarations = List.rev declarations in (* Common hack to have O(1) append: prepend and then reverse *) ok (env', state', declarations) -let type_and_subst_xyz (env_state_node : environment * O.typer_state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * O.typer_state * 'a) -> (environment * O.typer_state * 'b) Trace.result) : ('b * O.typer_state) result = +let type_and_subst_xyz (env_state_node : environment * O'.typer_state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * O'.typer_state * 'a) -> (environment * O'.typer_state * 'b) Trace.result) : ('b * O'.typer_state) result = let%bind (env, state, node) = type_xyz_returns_state env_state_node in let subst_all = let aliases = state.structured_dbs.aliases in @@ -470,17 +471,17 @@ let type_and_subst_xyz (env_state_node : environment * O.typer_state * 'a) (appl let () = ignore env in (* TODO: shouldn't we use the `env` somewhere? *) ok (node, state) -let type_program (p : I.program) : (O.program * O.typer_state) result = +let type_program (p : I.program) : (O.program * O'.typer_state) result = let empty_env = DEnv.default in let empty_state = Solver.initial_state in type_and_subst_xyz (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state -let type_expression_returns_state : (environment * O.typer_state * I.expression) -> (environment * O.typer_state * O.expression) Trace.result = +let type_expression_returns_state : (environment * O'.typer_state * I.expression) -> (environment * O'.typer_state * O.expression) Trace.result = fun (env, state, e) -> let%bind (e , state) = type_expression env state e in ok (env, state, e) -let type_expression_subst (env : environment) (state : O.typer_state) ?(tv_opt : O.type_expression option) (e : I.expression) : (O.expression * O.typer_state) result = +let type_expression_subst (env : environment) (state : O'.typer_state) ?(tv_opt : O.type_expression option) (e : I.expression) : (O.expression * O'.typer_state) result = let () = ignore tv_opt in (* For compatibility with the old typer's API, this argument can be removed once the new typer is used. *) type_and_subst_xyz (env , state , e) Typesystem.Misc.Substitution.Pattern.s_expression type_expression_returns_state @@ -488,14 +489,14 @@ let untype_type_expression = Untyper.untype_type_expression let untype_expression = Untyper.untype_expression (* These aliases are just here for quick navigation during debug, and can safely be removed later *) -let [@warning "-32"] (*rec*) type_declaration _env _state : I.declaration -> (environment * O.typer_state * O.declaration option) result = type_declaration _env _state -and [@warning "-32"] type_match : environment -> O.typer_state -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> (O.matching_expr * O.typer_state) result = type_match +let [@warning "-32"] (*rec*) type_declaration _env _state : I.declaration -> (environment * O'.typer_state * O.declaration option) result = type_declaration _env _state +and [@warning "-32"] type_match : environment -> O'.typer_state -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> (O.matching_expr * O'.typer_state) result = type_match and [@warning "-32"] evaluate_type (e:environment) (t:I.type_expression) : O.type_expression result = evaluate_type e t -and [@warning "-32"] type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result = type_expression +and [@warning "-32"] type_expression : environment -> O'.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O'.typer_state) result = type_expression and [@warning "-32"] type_lambda e state lam = type_lambda e state lam and [@warning "-32"] type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result = type_constant name lst tv_opt -let [@warning "-32"] type_program_returns_state ((env, state, p) : environment * O.typer_state * I.program) : (environment * O.typer_state * O.program) result = type_program_returns_state (env, state, p) -let [@warning "-32"] type_and_subst_xyz (env_state_node : environment * O.typer_state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * O.typer_state * 'a) -> (environment * O.typer_state * 'b) Trace.result) : ('b * O.typer_state) result = type_and_subst_xyz env_state_node apply_substs type_xyz_returns_state -let [@warning "-32"] type_program (p : I.program) : (O.program * O.typer_state) result = type_program p -let [@warning "-32"] type_expression_returns_state : (environment * O.typer_state * I.expression) -> (environment * O.typer_state * O.expression) Trace.result = type_expression_returns_state -let [@warning "-32"] type_expression_subst (env : environment) (state : O.typer_state) ?(tv_opt : O.type_expression option) (e : I.expression) : (O.expression * O.typer_state) result = type_expression_subst env state ?tv_opt e +let [@warning "-32"] type_program_returns_state ((env, state, p) : environment * O'.typer_state * I.program) : (environment * O'.typer_state * O.program) result = type_program_returns_state (env, state, p) +let [@warning "-32"] type_and_subst_xyz (env_state_node : environment * O'.typer_state * 'a) (apply_substs : 'b Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * O'.typer_state * 'a) -> (environment * O'.typer_state * 'b) Trace.result) : ('b * O'.typer_state) result = type_and_subst_xyz env_state_node apply_substs type_xyz_returns_state +let [@warning "-32"] type_program (p : I.program) : (O.program * O'.typer_state) result = type_program p +let [@warning "-32"] type_expression_returns_state : (environment * O'.typer_state * I.expression) -> (environment * O'.typer_state * O.expression) Trace.result = type_expression_returns_state +let [@warning "-32"] type_expression_subst (env : environment) (state : O'.typer_state) ?(tv_opt : O.type_expression option) (e : I.expression) : (O.expression * O'.typer_state) result = type_expression_subst env state ?tv_opt e diff --git a/src/passes/8-typer-new/typer.mli b/src/passes/8-typer-new/typer.mli index 9c2e267fc..626dc29ea 100644 --- a/src/passes/8-typer-new/typer.mli +++ b/src/passes/8-typer-new/typer.mli @@ -2,6 +2,7 @@ open Trace module I = Ast_core module O = Ast_typed +module O' = Typesystem.Solver_types module Environment = O.Environment @@ -38,11 +39,11 @@ module Errors : sig *) end -val type_program : I.program -> (O.program * O.typer_state) result -val type_declaration : environment -> O.typer_state -> I.declaration -> (environment * O.typer_state * O.declaration option) result +val type_program : I.program -> (O.program * O'.typer_state) result +val type_declaration : environment -> O'.typer_state -> I.declaration -> (environment * O'.typer_state * O.declaration option) result val evaluate_type : environment -> I.type_expression -> O.type_expression result -val type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result -val type_expression_subst : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result +val type_expression : environment -> O'.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O'.typer_state) result +val type_expression_subst : environment -> O'.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O'.typer_state) result val type_constant : I.constant' -> O.type_expression list -> O.type_expression option -> (O.constant' * O.type_expression) result val untype_type_expression : O.type_expression -> I.type_expression result diff --git a/src/passes/8-typer-old/typer.ml b/src/passes/8-typer-old/typer.ml index ca2a123a7..d31c41dc5 100644 --- a/src/passes/8-typer-old/typer.ml +++ b/src/passes/8-typer-old/typer.ml @@ -2,6 +2,7 @@ open Trace module I = Ast_core module O = Ast_typed +module O' = Typesystem.Solver_types open O.Combinators module DEnv = Environment @@ -489,7 +490,7 @@ let unconvert_constant' : O.constant' -> I.constant' = function | C_CONVERT_FROM_LEFT_COMB -> C_CONVERT_FROM_LEFT_COMB | C_CONVERT_FROM_RIGHT_COMB -> C_CONVERT_FROM_RIGHT_COMB -let rec type_program (p:I.program) : (O.program * O.typer_state) result = +let rec type_program (p:I.program) : (O.program * O'.typer_state) 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 (Solver.placeholder_for_state_of_new_typer ()))) d in let loc : 'a . 'a Location.wrap -> _ -> _ = fun x v -> Location.wrap ~loc:x.location v in @@ -501,7 +502,7 @@ let rec type_program (p:I.program) : (O.program * O.typer_state) result = bind_fold_list aux (DEnv.default, []) p in ok @@ (List.rev lst , (Solver.placeholder_for_state_of_new_typer ())) -and type_declaration env (_placeholder_for_state_of_new_typer : O.typer_state) : I.declaration -> (environment * O.typer_state * O.declaration) result = function +and type_declaration env (_placeholder_for_state_of_new_typer : O'.typer_state) : I.declaration -> (environment * O'.typer_state * O.declaration) result = function | Declaration_type (type_binder , type_expr) -> let%bind tv = evaluate_type env type_expr in let env' = Environment.add_type (type_binder) tv env in @@ -668,7 +669,7 @@ and evaluate_type (e:environment) (t:I.type_expression) : O.type_expression resu return @@ pair ) -and type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result +and type_expression : environment -> O'.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O'.typer_state) result = fun e _placeholder_for_state_of_new_typer ?tv_opt ae -> let%bind res = type_expression' e ?tv_opt ae in ok (res, (Solver.placeholder_for_state_of_new_typer ())) diff --git a/src/passes/8-typer-old/typer.mli b/src/passes/8-typer-old/typer.mli index 531a6b751..b0dda96e3 100644 --- a/src/passes/8-typer-old/typer.mli +++ b/src/passes/8-typer-old/typer.mli @@ -2,6 +2,7 @@ open Trace module I = Ast_core module O = Ast_typed +module O' = Typesystem.Solver_types module Environment = O.Environment @@ -38,11 +39,11 @@ module Errors : sig *) end -val type_program : I.program -> (O.program * O.typer_state) result -val type_declaration : environment -> O.typer_state -> I.declaration -> (environment * O.typer_state * O.declaration) result +val type_program : I.program -> (O.program * O'.typer_state) result +val type_declaration : environment -> O'.typer_state -> I.declaration -> (environment * O'.typer_state * O.declaration) result (* val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result *) val evaluate_type : environment -> I.type_expression -> O.type_expression result -val type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result +val type_expression : environment -> O'.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O'.typer_state) result val type_constant : I.constant' -> O.type_expression list -> O.type_expression option -> (O.constant' * O.type_expression) result (* val untype_type_value : O.type_value -> (I.type_expression) result diff --git a/src/passes/8-typer/typer.ml b/src/passes/8-typer/typer.ml index 48f1ac011..b1577a514 100644 --- a/src/passes/8-typer/typer.ml +++ b/src/passes/8-typer/typer.ml @@ -2,6 +2,7 @@ let use_new_typer = false module I = Ast_core module O = Ast_typed +module O' = Typesystem.Solver_types module Environment = O.Environment diff --git a/src/passes/8-typer/typer.mli b/src/passes/8-typer/typer.mli index 8069ab943..062b4aab4 100644 --- a/src/passes/8-typer/typer.mli +++ b/src/passes/8-typer/typer.mli @@ -4,6 +4,7 @@ open Trace module I = Ast_core module O = Ast_typed +module O' = Typesystem.Solver_types module Environment = O.Environment @@ -11,6 +12,6 @@ module Solver = Typer_new.Solver type environment = Environment.t -val type_program : I.program -> (O.program * O.typer_state) result -val type_expression_subst : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result +val type_program : I.program -> (O.program * O'.typer_state) result +val type_expression_subst : environment -> O'.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O'.typer_state) result val untype_expression : O.expression -> I.expression result diff --git a/src/stages/4-ast_typed/ast.ml b/src/stages/4-ast_typed/ast.ml index 99b532754..84a939ba4 100644 --- a/src/stages/4-ast_typed/ast.ml +++ b/src/stages/4-ast_typed/ast.ml @@ -618,8 +618,3 @@ type already_selected = { break_ctor : m_break_ctor__already_selected ; specialize1 : m_specialize1__already_selected ; } - -type typer_state = { - structured_dbs : structured_dbs ; - already_selected : already_selected ; -} diff --git a/src/stages/typesystem/core.ml b/src/stages/typesystem/core.ml index 1fc668ace..8fa44fa87 100644 --- a/src/stages/typesystem/core.ml +++ b/src/stages/typesystem/core.ml @@ -21,7 +21,7 @@ type c_equation_e = Ast_typed.c_equation_e type c_typeclass_simpl = Ast_typed.c_typeclass_simpl type c_poly_simpl = Ast_typed.c_poly_simpl type type_constraint_simpl = Ast_typed.type_constraint_simpl -type state = Ast_typed.typer_state +type state = Solver_types.typer_state type type_variable = Ast_typed.type_variable type type_expression = Ast_typed.type_expression diff --git a/src/stages/typesystem/solver_types.ml b/src/stages/typesystem/solver_types.ml index 9690d9c0a..7d1fd3623 100644 --- a/src/stages/typesystem/solver_types.ml +++ b/src/stages/typesystem/solver_types.ml @@ -1,4 +1,5 @@ open Ast_typed.Types +module Set = RedBlackTrees.PolySet 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 = @@ -8,6 +9,20 @@ 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 type 'selector_output propagator = 'selector_output -> structured_dbs -> new_constraints * new_assignments +type ('old_constraint_type , 'selector_output ) propagator_heuristic = { + selector : ('old_constraint_type, 'selector_output) selector ; + propagator : 'selector_output propagator ; + empty_already_selected : 'selector_output Set.t; +} + +type ex_propagator_heuristic = + (* For now only support a single type of input, make this polymorphic as needed. *) + | Propagator_heuristic : (type_constraint_simpl, 'selector_output) propagator_heuristic -> ex_propagator_heuristic + +type typer_state = { + structured_dbs : structured_dbs ; + already_selected_and_propagators : ex_propagator_heuristic list ; +} (* state+list monad *) type ('state, 'elt) state_list_monad = { state: 'state ; list : 'elt list } @@ -16,3 +31,4 @@ 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 } + diff --git a/src/test/test_helpers.ml b/src/test/test_helpers.ml index cc1e25afb..89983f082 100644 --- a/src/test/test_helpers.ml +++ b/src/test/test_helpers.ml @@ -86,7 +86,7 @@ let sha_256_hash pl = open Ast_imperative.Combinators let typed_program_with_imperative_input_to_michelson - ((program , state): Ast_typed.program * Ast_typed.typer_state) (entry_point: string) + ((program , state): Ast_typed.program * Typesystem.Solver_types.typer_state) (entry_point: string) (input: Ast_imperative.expression) : Compiler.compiled_expression result = Printexc.record_backtrace true; let env = Ast_typed.program_environment Environment.default program in @@ -99,7 +99,7 @@ let typed_program_with_imperative_input_to_michelson Compile.Of_mini_c.aggregate_and_compile_expression mini_c_prg compiled_applied let run_typed_program_with_imperative_input ?options - ((program , state): Ast_typed.program * Ast_typed.typer_state) (entry_point: string) + ((program , state): Ast_typed.program * Typesystem.Solver_types.typer_state) (entry_point: string) (input: Ast_imperative.expression) : Ast_core.expression result = let%bind michelson_program = typed_program_with_imperative_input_to_michelson (program , state) entry_point input in let%bind michelson_output = Ligo.Run.Of_michelson.run_no_failwith ?options michelson_program.expr michelson_program.expr_ty in @@ -172,7 +172,7 @@ let expect_evaluate (program, _state) entry_point expecter = let%bind res_simpl = Uncompile.uncompile_typed_program_entry_expression_result program entry_point res_michelson in expecter res_simpl -let expect_eq_evaluate ((program , state) : Ast_typed.program * Ast_typed.typer_state) entry_point expected = +let expect_eq_evaluate ((program , state) : Ast_typed.program * Typesystem.Solver_types.typer_state) entry_point expected = let%bind expected = expression_to_core expected in let expecter = fun result -> Ast_core.Misc.assert_value_eq (expected , result) in From 81358db582ad4bc9d7200ef68465b6facf37a496 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Wed, 3 Jun 2020 01:01:08 +0100 Subject: [PATCH 3/3] Cleanup of solver.ml, separated the heuristic's definition from its state in the solver (propagator_heuristic vs. propagator_state) --- src/passes/8-typer-new/PP.ml | 2 +- .../8-typer-new/heuristic_break_ctor.ml | 4 +- .../8-typer-new/heuristic_specialize1.ml | 4 +- src/passes/8-typer-new/solver.ml | 162 +++++++++--------- src/stages/typesystem/solver_types.ml | 23 ++- 5 files changed, 100 insertions(+), 95 deletions(-) diff --git a/src/passes/8-typer-new/PP.ml b/src/passes/8-typer-new/PP.ml index 9ef484180..e9cca2cfb 100644 --- a/src/passes/8-typer-new/PP.ml +++ b/src/passes/8-typer-new/PP.ml @@ -48,7 +48,7 @@ let structured_dbs : _ -> structured_dbs -> unit = fun ppf structured_dbs -> let { all_constraints = a ; aliases = b ; _ } = structured_dbs in fprintf ppf "STRUCTURED_DBS\n %a\n %a" all_constraints a aliases b -let already_selected_and_propagators : _ -> ex_propagator_heuristic list -> unit = fun ppf already_selected -> +let already_selected_and_propagators : _ -> ex_propagator_state list -> unit = fun ppf already_selected -> let _ = already_selected in fprintf ppf "ALREADY_SELECTED" diff --git a/src/passes/8-typer-new/heuristic_break_ctor.ml b/src/passes/8-typer-new/heuristic_break_ctor.ml index 6c145173f..ab8842443 100644 --- a/src/passes/8-typer-new/heuristic_break_ctor.ml +++ b/src/passes/8-typer-new/heuristic_break_ctor.ml @@ -24,7 +24,7 @@ let selector : (type_constraint_simpl, output_break_ctor) selector = | SC_Typeclass _ -> WasNotSelected let propagator : output_break_ctor propagator = - fun selected dbs -> + fun dbs selected -> 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 @@ -51,4 +51,4 @@ let propagator : output_break_ctor propagator = let eqs = eq1 :: eqs3 in (eqs , []) (* no new assignments *) -let heuristic = Propagator_heuristic { selector ; propagator ; empty_already_selected = Set.create ~cmp:Solver_should_be_generated.compare_output_break_ctor } +let heuristic = Propagator_heuristic { selector ; propagator ; comparator = Solver_should_be_generated.compare_output_break_ctor } diff --git a/src/passes/8-typer-new/heuristic_specialize1.ml b/src/passes/8-typer-new/heuristic_specialize1.ml index 37e4f206c..5d7bc863f 100644 --- a/src/passes/8-typer-new/heuristic_specialize1.ml +++ b/src/passes/8-typer-new/heuristic_specialize1.ml @@ -29,7 +29,7 @@ let selector : (type_constraint_simpl, output_specialize1) selector = | SC_Typeclass _ -> WasNotSelected let propagator : output_specialize1 propagator = - fun selected dbs -> + fun dbs selected -> let () = ignore (dbs) in (* this propagator doesn't need to use the dbs *) let a = selected.poly in let b = selected.a_k_var in @@ -52,4 +52,4 @@ let propagator : output_specialize1 propagator = let eqs = eq1 :: new_constraints in (eqs, []) (* no new assignments *) -let heuristic = Propagator_heuristic { selector ; propagator ; empty_already_selected = Set.create ~cmp:Solver_should_be_generated.compare_output_specialize1 } +let heuristic = Propagator_heuristic { selector ; propagator ; comparator = Solver_should_be_generated.compare_output_specialize1 } diff --git a/src/passes/8-typer-new/solver.ml b/src/passes/8-typer-new/solver.ml index 48990d294..504035733 100644 --- a/src/passes/8-typer-new/solver.ml +++ b/src/passes/8-typer-new/solver.ml @@ -6,73 +6,15 @@ module UF = UnionFind.Poly2 open Ast_typed.Types open Typesystem.Solver_types -(* sub-sub component: lazy selector (don't re-try all selectors every time) - * For now: just re-try everytime *) +(* TODO: move the propagator_heuristics list to a separate module which calls the solver with a bunch of heuristics *) +let propagator_heuristics = + [ + Heuristic_break_ctor.heuristic ; + Heuristic_specialize1.heuristic ; + ] -(* TODO : with our selectors, the selection depends on the order in which the constraints are added :-( :-( :-( :-( - We need to return a lazy stream of constraints. *) - -let select_and_propagate : ('old_input, 'selector_output) selector -> 'selector_output propagator -> 'selector_output poly_set -> 'old_input -> structured_dbs -> 'selector_output poly_set * new_constraints * new_assignments = - fun selector propagator -> - fun already_selected old_type_constraint dbs -> - (* TODO: thread some state to know which selector outputs were already seen *) - match selector old_type_constraint dbs with - WasSelected selected_outputs -> - let Set.{ set = already_selected ; duplicates = _ ; added = selected_outputs } = Set.add_list selected_outputs already_selected in - (* 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 *) - (already_selected , List.flatten new_constraints , List.flatten new_assignments) - | WasNotSelected -> - (already_selected, [] , []) - -let aux sel_propag new_constraint (already_selected , new_constraints , dbs) = - let (already_selected , new_constraints', new_assignments) = sel_propag already_selected new_constraint dbs in - let assignments = List.fold_left (fun acc ({tv;c_tag=_;tv_list=_} as ele) -> Map.update tv (function None -> Some ele | x -> x) acc) dbs.assignments new_assignments in - let dbs = { dbs with assignments } in - (already_selected , new_constraints' @ new_constraints , dbs) - -let step = fun (Propagator_heuristic { selector; propagator; empty_already_selected }) dbs new_constraint new_constraints -> - let (already_selected , new_constraints , dbs) = aux (select_and_propagate selector propagator) new_constraint (empty_already_selected , new_constraints , dbs) in - Propagator_heuristic { selector; propagator; empty_already_selected=already_selected }, new_constraints, dbs - -(* Takes a constraint, applies all selector+propagator pairs to it. - Keeps track of which constraints have already been selected. *) -let select_and_propagate_all' : ex_propagator_heuristic list -> type_constraint_simpl selector_input -> structured_dbs -> ex_propagator_heuristic list * new_constraints * structured_dbs = - fun already_selected_and_propagators new_constraint dbs -> - (* The order in which the propagators are applied to constraints - is entirely accidental (dfs/bfs/something in-between). *) - List.fold_left - (fun (hs , new_constraints , dbs) sp -> - let (h , a , b) = step sp dbs new_constraint new_constraints in - (h :: hs , a , b)) - ([], [] , dbs) - already_selected_and_propagators - -(* Takes a list of constraints, applies all selector+propagator pairs - to each in turn. *) -let rec select_and_propagate_all : ex_propagator_heuristic list -> type_constraint selector_input list -> structured_dbs -> ex_propagator_heuristic list * structured_dbs = - fun already_selected_and_propagators new_constraints dbs -> - match new_constraints with - | [] -> (already_selected_and_propagators, dbs) - | new_constraint :: tl -> - let { state = dbs ; list = modified_constraints } = Normalizer.normalizers new_constraint dbs in - let (already_selected , new_constraints' , dbs) = - List.fold_left - (fun (already_selected , nc , dbs) c -> - let (already_selected , new_constraints' , dbs) = select_and_propagate_all' already_selected c dbs in - (already_selected , new_constraints' @ nc , dbs)) - (already_selected_and_propagators , [] , dbs) - modified_constraints in - let new_constraints = new_constraints' @ tl in - select_and_propagate_all already_selected new_constraints dbs - -(* sub-component: constraint selector (worklist / dynamic queries) *) - -(* constraint propagation: (buch of constraints) → (new constraints * assignments) *) - -(* Below is a draft *) +let init_propagator_heuristic (Propagator_heuristic { selector ; propagator ; comparator }) = + Propagator_state { selector ; propagator ; already_selected = Set.create ~cmp:comparator } let initial_state : typer_state = { structured_dbs = @@ -83,29 +25,68 @@ let initial_state : typer_state = { grouped_by_variable = (Map.create ~cmp:Var.compare : (type_variable, constraints) Map.t); cycle_detection_toposort = (); } ; - already_selected_and_propagators = [ - Heuristic_break_ctor.heuristic ; - Heuristic_specialize1.heuristic ; - ] + already_selected_and_propagators = List.map init_propagator_heuristic propagator_heuristics } -(* This function is called when a program is fully compiled, and the - typechecker's state is discarded. TODO: either get rid of the state - earlier, or perform a sanity check here (e.g. that types have been - inferred for all bindings and expressions, etc. +(* TODO : with our selectors, the selection depends on the order in which the constraints are added :-( :-( :-( :-( + We need to return a lazy stream of constraints. *) + +(* The order in which the propagators are applied to constraints is + entirely accidental (dfs/bfs/something in-between). *) + +(* sub-component: constraint selector (worklist / dynamic queries) *) +let select_and_propagate : ('old_input, 'selector_output) selector -> 'selector_output propagator -> 'selector_output poly_set -> 'old_input -> structured_dbs -> 'selector_output poly_set * new_constraints * new_assignments = + fun selector propagator -> + fun already_selected old_type_constraint dbs -> + (* TODO: thread some state to know which selector outputs were already seen *) + match selector old_type_constraint dbs with + WasSelected selected_outputs -> + let Set.{ set = already_selected ; duplicates = _ ; added = selected_outputs } = Set.add_list selected_outputs already_selected in + (* Call the propagation rule *) + let (new_constraints , new_assignments) = List.split @@ List.map (propagator dbs) selected_outputs in + (* return so that the new constraints are pushed to some kind of work queue and the new assignments stored *) + (already_selected , List.flatten new_constraints , List.flatten new_assignments) + | WasNotSelected -> + (already_selected, [] , []) + +let select_and_propagate_one new_constraint (new_states , new_constraints , dbs) (Propagator_state { selector; propagator; already_selected }) = + let sel_propag = (select_and_propagate selector propagator) in + let (already_selected , new_constraints', new_assignments) = sel_propag already_selected new_constraint dbs in + let assignments = List.fold_left (fun acc ({tv;c_tag=_;tv_list=_} as ele) -> Map.update tv (function None -> Some ele | x -> x) acc) dbs.assignments new_assignments in + let dbs = { dbs with assignments } in + Propagator_state { selector; propagator; already_selected } :: new_states, new_constraints' @ new_constraints, dbs + +(* Takes a constraint, applies all selector+propagator pairs to it. + Keeps track of which constraints have already been selected. *) +let select_and_propagate_all' : ex_propagator_state list -> type_constraint_simpl selector_input -> structured_dbs -> ex_propagator_state list * new_constraints * structured_dbs = + fun already_selected_and_propagators new_constraint dbs -> + List.fold_left + (select_and_propagate_one new_constraint) + ([], [] , dbs) + already_selected_and_propagators + +(* Takes a list of constraints, applies all selector+propagator pairs + to each in turn. *) +let rec select_and_propagate_all : typer_state -> type_constraint selector_input list -> typer_state result = + fun { already_selected_and_propagators ; structured_dbs } new_constraints -> + match new_constraints with + | [] -> ok { already_selected_and_propagators ; structured_dbs } + | new_constraint :: tl -> + let { state = dbs ; list = modified_constraints } = Normalizer.normalizers new_constraint structured_dbs in + let (already_selected_and_propagators , new_constraints' , structured_dbs) = + List.fold_left + (fun (already_selected , nc , dbs) c -> + let (already_selected , new_constraints' , dbs) = select_and_propagate_all' already_selected c dbs in + (already_selected , new_constraints' @ nc , dbs)) + (already_selected_and_propagators , [] , dbs) + modified_constraints in + let new_constraints = new_constraints' @ tl in + select_and_propagate_all { already_selected_and_propagators ; structured_dbs } new_constraints + +(* This is the solver. *) +let aggregate_constraints = select_and_propagate_all - Also, we should check at these places that we indeed do not need the - state any further. Suzanne *) -let discard_state (_ : typer_state) = () -(* This is the solver *) -let aggregate_constraints : typer_state -> type_constraint list -> typer_state result = fun state newc -> - (* TODO: Iterate over constraints *) - let _todo = ignore (state, newc) in - let (a, b) = select_and_propagate_all state.already_selected_and_propagators newc state.structured_dbs in - ok { already_selected_and_propagators = a ; structured_dbs = b } -(*let { constraints ; eqv } = state in - ok { constraints = constraints @ newc ; eqv }*) (* Later on, we'll ensure that all the heuristics register the existential/unification variables that they create, as well as the @@ -116,4 +97,15 @@ let aggregate_constraints : typer_state -> type_constraint list -> typer_state r (possibly by first generalizing the type and then using the polymorphic type argument to instantiate the existential). *) + + +(* This function is called when a program is fully compiled, and the + typechecker's state is discarded. TODO: either get rid of the state + earlier, or perform a sanity check here (e.g. that types have been + inferred for all bindings and expressions, etc. + + Also, we should check at these places that we indeed do not need the + state any further. Suzanne *) +let discard_state (_ : typer_state) = () + let placeholder_for_state_of_new_typer () = initial_state diff --git a/src/stages/typesystem/solver_types.ml b/src/stages/typesystem/solver_types.ml index 7d1fd3623..8c9b547c3 100644 --- a/src/stages/typesystem/solver_types.ml +++ b/src/stages/typesystem/solver_types.ml @@ -8,20 +8,33 @@ type 'selector_output selector_outputs = 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 -type 'selector_output propagator = 'selector_output -> structured_dbs -> new_constraints * new_assignments +type 'selector_output propagator = structured_dbs -> 'selector_output -> new_constraints * new_assignments type ('old_constraint_type , 'selector_output ) propagator_heuristic = { - selector : ('old_constraint_type, 'selector_output) selector ; - propagator : 'selector_output propagator ; - empty_already_selected : 'selector_output Set.t; + (* sub-sub component: lazy selector (don't re-try all selectors every time) + * For now: just re-try everytime *) + selector : ('old_constraint_type, 'selector_output) selector ; + (* constraint propagation: (buch of constraints) → (new constraints * assignments) *) + propagator : 'selector_output propagator ; + comparator : 'selector_output -> 'selector_output -> int ; +} + +type ('old_constraint_type , 'selector_output ) propagator_state = { + selector : ('old_constraint_type, 'selector_output) selector ; + propagator : 'selector_output propagator ; + already_selected : 'selector_output Set.t; } type ex_propagator_heuristic = (* For now only support a single type of input, make this polymorphic as needed. *) | Propagator_heuristic : (type_constraint_simpl, 'selector_output) propagator_heuristic -> ex_propagator_heuristic +type ex_propagator_state = + (* For now only support a single type of input, make this polymorphic as needed. *) + | Propagator_state : (type_constraint_simpl, 'selector_output) propagator_state -> ex_propagator_state + type typer_state = { structured_dbs : structured_dbs ; - already_selected_and_propagators : ex_propagator_heuristic list ; + already_selected_and_propagators : ex_propagator_state list ; } (* state+list monad *)