src/passes/09-typing/08-typer-new/heuristic_break_ctor.ml

@@ -5,9 +5,9 @@ open Ast_typed.Misc
 open Ast_typed.Types
 open Typesystem.Solver_types
 
-let selector :  (type_constraint_simpl, output_break_ctor) selector =
+let selector :  (type_constraint_simpl, output_break_ctor, unit) selector =
   (* find two rules with the shape x = k(var …) and x = k'(var' …) *)
-  fun type_constraint_simpl dbs ->
+  fun type_constraint_simpl () dbs ->
   match type_constraint_simpl with
     SC_Constructor c ->
     (* finding other constraints related to the same type variable and
@@ -18,14 +18,14 @@ let selector :  (type_constraint_simpl, output_break_ctor) selector =
     (* TODO double-check the conditions in the propagator, we had a
        bug here because the selector was too permissive. *)
     let cs_pairs = List.map (fun x -> { a_k_var = c ; a_k'_var' = x }) other_cs in
-    WasSelected cs_pairs
-  | SC_Alias       _                -> WasNotSelected (* TODO: ??? (beware: symmetry) *)
-  | SC_Poly        _                -> WasNotSelected (* TODO: ??? (beware: symmetry) *)
-  | SC_Typeclass   _                -> WasNotSelected
-  | SC_Row         _                -> WasNotSelected
+    () , WasSelected cs_pairs
+  | SC_Alias       _                -> () , WasNotSelected (* TODO: ??? (beware: symmetry) *)
+  | SC_Poly        _                -> () , WasNotSelected (* TODO: ??? (beware: symmetry) *)
+  | SC_Typeclass   _                -> () , WasNotSelected
+  | SC_Row         _                -> () , WasNotSelected
 
-let propagator : output_break_ctor propagator =
-  fun dbs selected ->
+let propagator : (output_break_ctor , unit) propagator =
+  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
@@ -53,7 +53,7 @@ let propagator : output_break_ctor propagator =
   else
     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 *)
+    (() , eqs , []) (* no new assignments *)
 
 let heuristic =
   Propagator_heuristic
@@ -61,5 +61,6 @@ let heuristic =
       selector ;
       propagator ;
       printer = Ast_typed.PP_generic.output_break_ctor ; (* TODO: use an accessor that can get the printer for PP_generic or PP_json alike *)
-      comparator = Solver_should_be_generated.compare_output_break_ctor
+      comparator = Solver_should_be_generated.compare_output_break_ctor ;
+      initial_private_storage = () ;
     }

src/passes/09-typing/08-typer-new/heuristic_specialize1.ml

@@ -8,29 +8,29 @@ open Ast_typed.Misc
 open Ast_typed.Types
 open Typesystem.Solver_types
 
-let selector : (type_constraint_simpl, output_specialize1) selector =
+let selector : (type_constraint_simpl , output_specialize1 , unit) selector =
   (* find two rules with the shape (x = forall b, d) and x = k'(var' …) or vice versa *)
   (* TODO: do the same for two rules with the shape (a = forall b, d) and tc(a…) *)
   (* TODO: do the appropriate thing for two rules with the shape (a = forall b, d) and (a = forall b', d') *)
-  fun type_constraint_simpl dbs ->
+  fun type_constraint_simpl () dbs ->
   match type_constraint_simpl with
     SC_Constructor c                ->
     (* vice versa *)
     let other_cs = (Constraint_databases.get_constraints_related_to c.tv dbs).poly in
     let other_cs = List.filter (fun (x : c_poly_simpl) -> Var.equal c.tv x.tv) other_cs in
     let cs_pairs = List.map (fun x -> { poly = x ; a_k_var = c }) other_cs in
-    WasSelected cs_pairs
-  | SC_Alias       _                -> WasNotSelected (* TODO: ??? *)
+    () , WasSelected cs_pairs
+  | SC_Alias       _                -> () , WasNotSelected (* TODO: ??? *)
   | SC_Poly        p                ->
     let other_cs = (Constraint_databases.get_constraints_related_to p.tv dbs).constructor in
     let other_cs = List.filter (fun (x : c_constructor_simpl) -> Var.equal x.tv p.tv) other_cs in
     let cs_pairs = List.map (fun x -> { poly = p ; a_k_var = x }) other_cs in
-    WasSelected cs_pairs
-  | SC_Typeclass   _                -> WasNotSelected
-  | SC_Row _ -> WasNotSelected
+    () , WasSelected cs_pairs
+  | SC_Typeclass   _                -> () , WasNotSelected
+  | SC_Row _                        -> () , WasNotSelected
 
-let propagator : output_specialize1 propagator =
-  fun dbs selected ->
+let propagator : (output_specialize1 , unit) propagator =
+  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,7 +52,7 @@ let propagator : output_specialize1 propagator =
   (if Ast_typed.Debug.debug_new_typer then Format.printf "apply = %a\nb = %a\nreduced = %a\nnew_constraints = [\n%a\n]\n" Ast_typed.PP_generic.type_value apply Ast_typed.PP_generic.c_constructor_simpl b Ast_typed.PP_generic.type_value reduced (PP_helpers.list_sep Ast_typed.PP_generic.type_constraint (fun ppf () -> Format.fprintf ppf " ;\n")) new_constraints);
   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 *)
+  ((), eqs, []) (* no new assignments *)
 
 let heuristic =
   Propagator_heuristic
@@ -60,5 +60,6 @@ let heuristic =
       selector ;
       propagator ;
       printer = Ast_typed.PP_generic.output_specialize1 ;
-      comparator = Solver_should_be_generated.compare_output_specialize1
+      comparator = Solver_should_be_generated.compare_output_specialize1 ;
+      initial_private_storage = () ;
     }

src/passes/09-typing/08-typer-new/solver.ml

@@ -13,8 +13,8 @@ let propagator_heuristics =
     Heuristic_specialize1.heuristic ;
   ]
 
-let init_propagator_heuristic (Propagator_heuristic { selector ; propagator ; printer ; comparator }) =
-  Propagator_state { selector ; propagator ; printer ; already_selected = Set.create ~cmp:comparator }
+let init_propagator_heuristic (Propagator_heuristic { selector ; propagator ; printer ; comparator ; initial_private_storage }) =
+  Propagator_state { selector ; propagator ; printer ; already_selected = Set.create ~cmp:comparator ; private_storage = initial_private_storage }
 
 let initial_state : typer_state = {
     structured_dbs =
@@ -35,15 +35,17 @@ let initial_state : typer_state = {
    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 =
+let select_and_propagate : 'old_input 'selector_output 'private_storage . ('old_input, 'selector_output, 'private_storage) selector -> ('selector_output , 'private_storage) propagator -> 'selector_output poly_set -> 'private_storage -> 'old_input -> structured_dbs -> 'selector_output poly_set * 'private_storage * new_constraints * new_assignments =
   fun selector propagator ->
-  fun already_selected old_type_constraint dbs ->
+  fun already_selected private_storage old_type_constraint dbs ->
   (* TODO: thread some state to know which selector outputs were already seen *)
-  match selector old_type_constraint dbs with
+  let private_storage , x = selector old_type_constraint private_storage dbs in
+  match x 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
+     let (private_storage, l) = List.fold_map_acc (fun private_storage selected -> let (a, b, c) = propagator private_storage dbs selected in (a, (b, c))) private_storage selected_outputs in
+     let (new_constraints , new_assignments) = List.split l in
      (* return so that the new constraints are pushed to some kind of work queue and the new assignments stored *)
 let () =
   (if Ast_typed.Debug.debug_new_typer && false then
@@ -54,16 +56,16 @@ let () =
      (PP_helpers.list_sep (PP_helpers.list_sep Ast_typed.PP_generic.c_constructor_simpl (s "\n")) (s "\n"))
      new_assignments)
 in
-     (already_selected , List.flatten new_constraints , List.flatten new_assignments)
+     (already_selected , private_storage , List.flatten new_constraints , List.flatten new_assignments)
   | WasNotSelected ->
-     (already_selected, [] , [])
+     (already_selected, private_storage , [] , [])
 
-let select_and_propagate_one new_constraint (new_states , new_constraints , dbs) (Propagator_state { selector; propagator; printer ; already_selected }) =
+let select_and_propagate_one new_constraint (new_states , new_constraints , dbs) (Propagator_state { selector; propagator; printer ; already_selected ; private_storage }) =
   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 (already_selected , private_storage, new_constraints', new_assignments) = sel_propag already_selected private_storage 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; printer ; already_selected } :: new_states, new_constraints' @ new_constraints, dbs
+  Propagator_state { selector; propagator; printer ; already_selected ; private_storage } :: 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. *)

src/stages/typesystem/solver_types.ml

@@ -7,32 +7,34 @@ type 'selector_output selector_outputs =
   | WasNotSelected
 type new_constraints = type_constraint list
 type new_assignments = c_constructor_simpl list
-type ('old_constraint_type, 'selector_output) selector = 'old_constraint_type selector_input -> structured_dbs -> 'selector_output selector_outputs
-type 'selector_output propagator = structured_dbs -> 'selector_output -> new_constraints * new_assignments
-type ('old_constraint_type , 'selector_output ) propagator_heuristic = {
+type ('old_constraint_type, 'selector_output , 'private_storage) selector = 'old_constraint_type selector_input -> 'private_storage -> structured_dbs -> 'private_storage * 'selector_output selector_outputs
+type ('selector_output , 'private_storage) propagator = 'private_storage -> structured_dbs -> 'selector_output -> 'private_storage * new_constraints * new_assignments
+type ('old_constraint_type , 'selector_output , 'private_storage) propagator_heuristic = {
   (* 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 ;
+  selector          : ('old_constraint_type , 'selector_output , 'private_storage) selector ;
   (* constraint propagation: (buch of constraints) → (new constraints * assignments) *)
-  propagator        : 'selector_output propagator ;
+  propagator        : ('selector_output , 'private_storage) propagator ;
   printer           : Format.formatter -> 'selector_output -> unit ;
   comparator        : 'selector_output -> 'selector_output -> int ;
+  initial_private_storage : 'private_storage;
 }
 
-type ('old_constraint_type , 'selector_output ) propagator_state = {
-  selector          : ('old_constraint_type, 'selector_output) selector ;
-  propagator        : 'selector_output propagator ;
+type ('old_constraint_type , 'selector_output , 'private_storage) propagator_state = {
+  selector          : ('old_constraint_type , 'selector_output , 'private_storage) selector ;
+  propagator        : ('selector_output , 'private_storage) propagator ;
   printer           : Format.formatter -> 'selector_output -> unit ;
   already_selected  : 'selector_output Set.t;
+  private_storage   : 'private_storage;
 }
 
 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
+  | Propagator_heuristic : (type_constraint_simpl , 'selector_output , 'private_storage) 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
+  | Propagator_state : (type_constraint_simpl , 'selector_output , 'private_storage) propagator_state -> ex_propagator_state
 
 type typer_state = {
   structured_dbs                   : structured_dbs   ;