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 *)