balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Cleanup of solver.ml, separated the heuristic's definition from its state in the solver (propagator_heuristic vs. propagator_state)

Browse Source
This commit is contained in:
Suzanne Dupéron 2020-06-03 01:01:08 +01:00
parent 7257aaaff4
commit 81358db582
5 changed files with 100 additions and 95 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/passes/8-typer-new/PP.ml
View File

@ -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"

4
src/passes/8-typer-new/heuristic_break_ctor.ml
View File

@ -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 }

4
src/passes/8-typer-new/heuristic_specialize1.ml
View File

@ -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 }

162
src/passes/8-typer-new/solver.ml
View File

@ -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

23
src/stages/typesystem/solver_types.ml
View File

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