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

blabla

Browse Source
This commit is contained in:
Suzanne Dupéron 2019-10-23 10:45:48 -04:00
parent 10362426aa
commit 535c291b3f
1 changed files with 173 additions and 177 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
src/passes/4-typer/solver.ml
View File

@ -688,34 +688,31 @@ let propagator_break_ctor : output_break_ctor propagator =
(* 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. *)
module type BLABLA = Set.OrderedType (* Set.S *)
type output_specialize1 = { poly : c_poly_simpl ; a_k_var : c_constructor_simpl }
module Comparators = struct
module Int = struct
module Int = struct
(* Restrict use of Pervasives.compare to just `int`, because we
don't want to risk the type of a field changing from int to
something not compatible with Pervasives.compare, and not
noticing that the comparator needs to be updated. *)
let compare (a : int) (b : int) = Pervasives.compare a b
end
let (<?) ca cb =
end
let (<?) ca cb =
if ca = 0 then cb () else ca
let rec compare_list f = function
let rec compare_list f = function
| hd1::tl1 -> (function
[] -> 1
| hd2::tl2 ->
f hd1 hd2 <? fun () ->
compare_list f tl1 tl2)
| [] -> (function [] -> 0 | _::_ -> -1) (* This follows the behaviour of Pervasives.compare for lists of different length *)
let compare_type_variable a b =
let compare_type_variable a b =
String.compare a b
let compare_label = function
let compare_label = function
| L_int a -> (function L_int b -> Int.compare a b | L_string _ -> -1)
| L_string a -> (function L_int _ -> 1 | L_string b -> String.compare a b)
let compare_simple_c_constant = function
let compare_simple_c_constant = function
| C_arrow -> (function
(* N/A -> 1 *)
| C_arrow -> 0
@ -809,8 +806,8 @@ module Comparators = struct
| C_contract -> 0
(* N/A -> -1 *)
)
let rec compare_typeclass a b = compare_list (compare_list compare_type_value) a b
and compare_type_value = function
let rec compare_typeclass a b = compare_list (compare_list compare_type_value) a b
and compare_type_value = function
| P_forall { binder=a1; constraints=a2; body=a3 } -> (function
| P_forall { binder=b1; constraints=b2; body=b3 } ->
compare_type_variable a1 b1 <? fun () ->
@ -834,7 +831,7 @@ module Comparators = struct
| P_variable _ -> 1
| P_constant _ -> 1
| P_apply (b1, b2) -> compare_type_value a1 b1 <? fun () -> compare_type_value a2 b2)
and compare_type_constraint = function
and compare_type_constraint = function
| C_equation (a1, a2) -> (function
| C_equation (b1, b2) -> compare_type_value a1 b1 <? fun () -> compare_type_value a2 b2
| C_typeclass _ -> -1
@ -847,36 +844,35 @@ module Comparators = struct
| C_equation _ -> 1
| C_typeclass _ -> 1
| C_access_label (b1, b2, b3) -> compare_type_value a1 b1 <? fun () -> compare_label a2 b2 <? fun () -> compare_type_variable a3 b3)
let rec compare_type_constraint_list = compare_list compare_type_constraint
let compare_p_forall
let rec compare_type_constraint_list = compare_list compare_type_constraint
let compare_p_forall
{ binder = a1; constraints = a2; body = a3 }
{ binder = b1; constraints = b2; body = b3 } =
compare_type_variable a1 b1 <? fun () ->
compare_type_constraint_list a2 b2 <? fun () ->
compare_type_value a3 b3
let compare_c_poly_simpl { tv = a1; forall = a2 } { tv = b1; forall = b2 } =
let compare_c_poly_simpl { tv = a1; forall = a2 } { tv = b1; forall = b2 } =
compare_type_variable a1 b1 <? fun () ->
compare_p_forall a2 b2
let compare_c_constructor_simpl { tv=a1; c_tag=a2; tv_list=a3 } { tv=b1; c_tag=b2; tv_list=b3 } =
let compare_c_constructor_simpl { tv=a1; c_tag=a2; tv_list=a3 } { tv=b1; c_tag=b2; tv_list=b3 } =
compare_type_variable a1 b1 <? fun () -> compare_simple_c_constant a2 b2 <? fun () -> compare_list compare_type_variable a3 b3
let compare_output_specialize1 { poly = a1; a_k_var = a2 } { poly = b1; a_k_var = b2 } =
let compare_output_specialize1 { poly = a1; a_k_var = a2 } { poly = b1; a_k_var = b2 } =
compare_c_poly_simpl a1 b1 <? fun () ->
compare_c_constructor_simpl a2 b2
let compare_output_break_ctor { a_k_var=a1; a_k'_var'=a2 } { a_k_var=b1; a_k'_var'=b2 } =
let compare_output_break_ctor { a_k_var=a1; a_k'_var'=a2 } { a_k_var=b1; a_k'_var'=b2 } =
compare_c_constructor_simpl a1 b1 <? fun () -> compare_c_constructor_simpl a2 b2
end
module OutputSpecialize1 : BLABLA = struct
module OutputSpecialize1 : Set.OrderedType = struct
type t = output_specialize1
let compare = Comparators.compare_output_specialize1
let compare = compare_output_specialize1
end
module BreakCtor : BLABLA = struct
module BreakCtor : Set.OrderedType = struct
type t = output_break_ctor
let compare = Comparators.compare_output_break_ctor
let compare = compare_output_break_ctor
end
let selector_specialize1 : (type_constraint_simpl, output_specialize1) selector =
@ -918,7 +914,7 @@ let propagator_specialize1 : output_specialize1 propagator =
let eqs = eq1 :: new_constraints in
(eqs, []) (* no new assignments *)
module M (BlaBla : BLABLA) = struct
module M (BlaBla : Set.OrderedType) = struct
module AlreadySelected = Set.Make(BlaBla)
let select_and_propagate : ('old_input, 'selector_output) selector -> BlaBla.t propagator -> 'a -> structured_dbs -> new_constraints * new_assignments =