Merge branch 'feature-cleanup-typer-13' into 'dev'

Cleanup of the solver, use a list of heuristics instead of hardcoding them

See merge request ligolang/ligo!657

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)
+let compile_expression ?(env = Ast_typed.Environment.empty) ~(state : Typesystem.Solver_types.typer_state) (e : Ast_core.expression)
-    : (Ast_typed.expression * Ast_typed.typer_state) result =
+    : (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

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_state 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
+  let { structured_dbs=a ; already_selected_and_propagators =b } = state in
-  fprintf ppf "STATE %a %a" structured_dbs a already_selected b
+  fprintf ppf "STATE %a %a" structured_dbs a already_selected_and_propagators 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' …) *)
@@ -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
@@ -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 ; comparator = Solver_should_be_generated.compare_output_break_ctor }

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 *)
@@ -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
@@ -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 ; comparator = Solver_should_be_generated.compare_output_specialize1 }

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

src/passes/8-typer-new/solver.ml

@@ -4,80 +4,17 @@ 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)
+(* TODO: move the propagator_heuristics list to a separate module which calls the solver with a bunch of heuristics *)
- * For now: just re-try everytime *)
+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 :-( :-( :-( :-(
+let init_propagator_heuristic (Propagator_heuristic { selector ; propagator ; comparator }) =
-   We need to return a lazy stream of constraints. *)
+  Propagator_state { selector ; propagator ; already_selected = Set.create ~cmp:comparator }
-
-let select_and_propagate : ('old_input, 'selector_output) selector -> _ propagator -> _ -> 'a -> structured_dbs -> _ * 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, [] , [])
-
-(* 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
-
-(* 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 ->
-    (* 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)
-
-(* 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 ->
-    match new_constraints with
-    | [] -> (already_selected, 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 , [] , 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 initial_state : typer_state = {
     structured_dbs =
@@ -88,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 = {
+    already_selected_and_propagators = List.map init_propagator_heuristic propagator_heuristics
-        break_ctor = Set.create ~cmp:Solver_should_be_generated.compare_output_break_ctor;
-        specialize1 = Set.create ~cmp:Solver_should_be_generated.compare_output_specialize1 ;
-      }
   }
 
-(* This function is called when a program is fully compiled, and the
+(* TODO : with our selectors, the selection depends on the order in which the constraints are added :-( :-( :-( :-(
-   typechecker's state is discarded. TODO: either get rid of the state
+   We need to return a lazy stream of constraints. *)
-   earlier, or perform a sanity check here (e.g. that types have been
+
-   inferred for all bindings and expressions, etc.
+(* 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 newc state.structured_dbs in
-  ok { already_selected = 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
@@ -121,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

src/passes/8-typer-new/solver_types.ml

@@ -1,18 +0,0 @@
-open Ast_typed.Types
-
-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 =
-    WasSelected of 'selector_output list
-  | 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 = 'selector_output -> structured_dbs -> new_constraints * new_assignments
-
-(* state+list monad *)
-type ('state, 'elt) state_list_monad = { state: 'state ; list : 'elt list }
-let lift_state_list_monad ~state ~list = { state ; list }
-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 }

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 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 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
+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"] 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_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_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_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_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_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

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_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_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 : 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_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

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

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

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
 

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

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

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

src/stages/typesystem/solver_types.ml

@@ -0,0 +1,47 @@
+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 =
+    WasSelected of 'selector_output list
+  | 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 = {
+  (* 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_state list ;
+}
+
+(* state+list monad *)
+type ('state, 'elt) state_list_monad = { state: 'state ; list : 'elt list }
+let lift_state_list_monad ~state ~list = { state ; list }
+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 }
+

src/stages/typesystem/typesystem.ml

@@ -1,3 +1,4 @@
 module Core = Core
 module Shorthands = Shorthands
 module Misc = Misc
+module Solver_types = Solver_types

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