revert indentation change
This commit is contained in:
parent
fc80c627fd
commit
4dbd2d5873
@ -427,29 +427,29 @@ module UnionFindWrapper = struct
|
|||||||
dbs
|
dbs
|
||||||
let merge_variables : type_variable -> type_variable -> structured_dbs -> structured_dbs =
|
let merge_variables : type_variable -> type_variable -> structured_dbs -> structured_dbs =
|
||||||
fun variable_a variable_b dbs ->
|
fun variable_a variable_b dbs ->
|
||||||
let variable_repr_a , aliases = UF.get_or_set variable_a dbs.aliases in
|
let variable_repr_a , aliases = UF.get_or_set variable_a dbs.aliases in
|
||||||
let dbs = { dbs with aliases } in
|
let dbs = { dbs with aliases } in
|
||||||
let variable_repr_b , aliases = UF.get_or_set variable_b dbs.aliases in
|
let variable_repr_b , aliases = UF.get_or_set variable_b dbs.aliases in
|
||||||
let dbs = { dbs with aliases } in
|
let dbs = { dbs with aliases } in
|
||||||
let default d = function None -> d | Some y -> y in
|
let default d = function None -> d | Some y -> y in
|
||||||
let get_constraints ab =
|
let get_constraints ab =
|
||||||
TypeVariableMap.find_opt ab dbs.grouped_by_variable
|
TypeVariableMap.find_opt ab dbs.grouped_by_variable
|
||||||
|> default { constructor = [] ; poly = [] ; tc = [] } in
|
|> default { constructor = [] ; poly = [] ; tc = [] } in
|
||||||
let constraints_a = get_constraints variable_repr_a in
|
let constraints_a = get_constraints variable_repr_a in
|
||||||
let constraints_b = get_constraints variable_repr_b in
|
let constraints_b = get_constraints variable_repr_b in
|
||||||
let all_constraints = {
|
let all_constraints = {
|
||||||
(* TODO: should be a Set.union, not @ *)
|
(* TODO: should be a Set.union, not @ *)
|
||||||
constructor = constraints_a.constructor @ constraints_b.constructor ;
|
constructor = constraints_a.constructor @ constraints_b.constructor ;
|
||||||
poly = constraints_a.poly @ constraints_b.poly ;
|
poly = constraints_a.poly @ constraints_b.poly ;
|
||||||
tc = constraints_a.tc @ constraints_b.tc ;
|
tc = constraints_a.tc @ constraints_b.tc ;
|
||||||
} in
|
} in
|
||||||
let grouped_by_variable =
|
let grouped_by_variable =
|
||||||
TypeVariableMap.add variable_repr_a all_constraints dbs.grouped_by_variable in
|
TypeVariableMap.add variable_repr_a all_constraints dbs.grouped_by_variable in
|
||||||
let dbs = { dbs with grouped_by_variable} in
|
let dbs = { dbs with grouped_by_variable} in
|
||||||
let grouped_by_variable =
|
let grouped_by_variable =
|
||||||
TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in
|
TypeVariableMap.remove variable_repr_b dbs.grouped_by_variable in
|
||||||
let dbs = { dbs with grouped_by_variable} in
|
let dbs = { dbs with grouped_by_variable} in
|
||||||
dbs
|
dbs
|
||||||
end
|
end
|
||||||
|
|
||||||
(* sub-sub component: constraint normalizer: remove dupes and give structure
|
(* sub-sub component: constraint normalizer: remove dupes and give structure
|
||||||
@ -642,24 +642,24 @@ let selector_break_ctor : (type_constraint_simpl, output_break_ctor) selector =
|
|||||||
|
|
||||||
let propagator_break_ctor : output_break_ctor propagator =
|
let propagator_break_ctor : output_break_ctor propagator =
|
||||||
fun selected dbs ->
|
fun selected dbs ->
|
||||||
let () = ignore (dbs) in (* this propagator doesn't need to use the dbs *)
|
let () = ignore (dbs) in (* this propagator doesn't need to use the dbs *)
|
||||||
let a = selected#a_k_var in
|
let a = selected#a_k_var in
|
||||||
let b = selected#a_k'_var' in
|
let b = selected#a_k'_var' in
|
||||||
(* produce constraints: *)
|
(* produce constraints: *)
|
||||||
|
|
||||||
(* a.tv = b.tv *)
|
(* a.tv = b.tv *)
|
||||||
let eq1 = C_equation (P_variable a.tv, P_variable b.tv) in
|
let eq1 = C_equation (P_variable a.tv, P_variable b.tv) in
|
||||||
(* a.c_tag = b.c_tag *)
|
(* a.c_tag = b.c_tag *)
|
||||||
if a.c_tag <> b.c_tag then
|
if a.c_tag <> b.c_tag then
|
||||||
failwith "type error: incompatible types, not same ctor (TODO error message)"
|
failwith "type error: incompatible types, not same ctor (TODO error message)"
|
||||||
else
|
else
|
||||||
(* a.tv_list = b.tv_list *)
|
(* a.tv_list = b.tv_list *)
|
||||||
if List.length a.tv_list <> List.length b.tv_list then
|
if List.length a.tv_list <> List.length b.tv_list then
|
||||||
failwith "type error: incompatible types, not same length (TODO error message)"
|
failwith "type error: incompatible types, not same length (TODO error message)"
|
||||||
else
|
else
|
||||||
let eqs3 = List.map2 (fun aa bb -> C_equation (P_variable aa, P_variable bb)) a.tv_list b.tv_list in
|
let eqs3 = List.map2 (fun aa bb -> C_equation (P_variable aa, P_variable bb)) a.tv_list b.tv_list in
|
||||||
let eqs = eq1 :: eqs3 in
|
let eqs = eq1 :: eqs3 in
|
||||||
(eqs , []) (* no new assignments *)
|
(eqs , []) (* no new assignments *)
|
||||||
|
|
||||||
(* TODO : with our selectors, the selection depends on the order in which the constraints are added :-( :-( :-( :-(
|
(* 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. *)
|
We need to return a lazy stream of constraints. *)
|
||||||
@ -700,15 +700,15 @@ let propagator_specialize1 : output_specialize1 propagator =
|
|||||||
let select_and_propagate : ('old_input, 'selector_output) selector -> 'selector_output propagator -> 'a -> structured_dbs -> new_constraints * new_assignments =
|
let select_and_propagate : ('old_input, 'selector_output) selector -> 'selector_output propagator -> 'a -> structured_dbs -> new_constraints * new_assignments =
|
||||||
fun selector propagator ->
|
fun selector propagator ->
|
||||||
fun todo dbs ->
|
fun todo dbs ->
|
||||||
match selector todo dbs with
|
match selector todo dbs with
|
||||||
WasSelected selected_outputs ->
|
WasSelected selected_outputs ->
|
||||||
(* Call the propagation rule *)
|
(* Call the propagation rule *)
|
||||||
let new_contraints_and_assignments = List.map (fun s -> propagator s dbs) selected_outputs in
|
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
|
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 *)
|
(* return so that the new constraints are pushed to some kind of work queue and the new assignments stored *)
|
||||||
(List.flatten new_constraints , List.flatten new_assignments)
|
(List.flatten new_constraints , List.flatten new_assignments)
|
||||||
| WasNotSelected ->
|
| WasNotSelected ->
|
||||||
([] , [])
|
([] , [])
|
||||||
|
|
||||||
let select_and_propagate_break_ctor = select_and_propagate selector_break_ctor propagator_break_ctor
|
let select_and_propagate_break_ctor = select_and_propagate selector_break_ctor propagator_break_ctor
|
||||||
let select_and_propagate_specialize1 = select_and_propagate selector_specialize1 propagator_specialize1
|
let select_and_propagate_specialize1 = select_and_propagate selector_specialize1 propagator_specialize1
|
||||||
|
Loading…
Reference in New Issue
Block a user