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

Solver: use a list of heuristics instead of hardcoding them.

Browse Source
This commit is contained in:
Suzanne Dupéron 2020-06-02 20:34:23 +01:00
parent 861ab57a43
commit 7257aaaff4
15 changed files with 95 additions and 78 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/main/compile/of_core.ml
View File

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

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

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

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

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

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

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

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

@ -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
(* 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 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 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). *)
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 }*)

37
src/passes/8-typer-new/typer.ml
View File

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

9
src/passes/8-typer-new/typer.mli
View File

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

7
src/passes/8-typer-old/typer.ml
View File

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

7
src/passes/8-typer-old/typer.mli
View File

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

1
src/passes/8-typer/typer.ml
View File

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

5
src/passes/8-typer/typer.mli
View File

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

5
src/stages/4-ast_typed/ast.ml
View File

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

2
src/stages/typesystem/core.ml
View File

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

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

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

6
src/test/test_helpers.ml
View File

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