31 |
31 |
let search_instr instruction =
|
32 |
32 |
match instruction.instr_desc with
|
33 |
33 |
| MStep (il, i, vl) when String.equal i ident -> [
|
34 |
|
(List.map (function x-> x.var_type) il,
|
35 |
|
List.map (function x-> x.value_type) vl)]
|
|
34 |
(List.map (function x-> x.value_type) vl,
|
|
35 |
List.map (function x-> x.var_type) il)]
|
36 |
36 |
| MBranch (_, l) -> List.flatten
|
37 |
37 |
(List.map (function x, y -> find_submachine_step_call ident y) l)
|
38 |
38 |
| _ -> []
|
... | ... | |
44 |
44 |
@param t2 an other type
|
45 |
45 |
@param return true if the two types are Tbasic or Tunivar and equal
|
46 |
46 |
**)
|
47 |
|
let check_type_equal (t1:Types.type_expr) (t2:Types.type_expr) =
|
|
47 |
let rec check_type_equal (t1:Types.type_expr) (t2:Types.type_expr) =
|
48 |
48 |
match (Types.repr t1).Types.tdesc, (Types.repr t2).Types.tdesc with
|
49 |
49 |
| Types.Tbasic x, Types.Tbasic y -> x = y
|
50 |
50 |
| Types.Tunivar, Types.Tunivar -> t1.tid = t2.tid
|
51 |
|
| _ -> assert false (* TODO *)
|
|
51 |
| Types.Ttuple l, _ -> assert (List.length l = 1); check_type_equal (List.hd l) t2
|
|
52 |
| _, Types.Ttuple l -> assert (List.length l = 1); check_type_equal t1 (List.hd l)
|
|
53 |
| Types.Tstatic (_, t), _ -> check_type_equal t t2
|
|
54 |
| _, Types.Tstatic (_, t) -> check_type_equal t1 t
|
|
55 |
| _ -> eprintf "ERROR: %a | %a" pp_type t1 pp_type t2; assert false (* TODO *)
|
52 |
56 |
|
53 |
57 |
(** Extend a substitution to unify the two given types. Only the
|
54 |
58 |
first type can be polymorphic.
|
... | ... | |
107 |
111 |
@return the correspondance between polymorphic type id and their instantiation
|
108 |
112 |
**)
|
109 |
113 |
let get_substitution machine ident submachine =
|
|
114 |
eprintf "%s %s %s@." machine.mname.node_id ident submachine.mname.node_id;
|
110 |
115 |
(* extract the calls to submachines from the machine *)
|
111 |
116 |
let calls = find_submachine_step_call ident machine.mstep.step_instrs in
|
112 |
117 |
(* extract the first call *)
|
... | ... | |
126 |
131 |
and the call *)
|
127 |
132 |
assert (List.length machine_types = List.length call_types);
|
128 |
133 |
(* Unify the two lists of types *)
|
129 |
|
let substituion = List.fold_left unification [] (List.combine machine_types call_types) in
|
|
134 |
let substitution = List.fold_left unification [] (List.combine machine_types call_types) in
|
130 |
135 |
(* Assume that our substitution match all the possible
|
131 |
136 |
polymorphic type of the node *)
|
132 |
137 |
let polymorphic_types = find_all_polymorphic_type submachine in
|
133 |
|
assert (List.length polymorphic_types = List.length substituion);
|
134 |
|
assert (List.for_all (function x->List.mem_assoc x substituion) polymorphic_types);
|
135 |
|
substituion
|
|
138 |
assert (List.length polymorphic_types = List.length substitution);
|
|
139 |
assert (List.for_all (function x->List.mem_assoc x substitution) polymorphic_types);
|
|
140 |
substitution
|
136 |
141 |
|
137 |
142 |
(** Print the declaration of a state element of a subinstance of a machine.
|
138 |
143 |
@param machine the machine
|
Ada: Correct some errors on the type checking due to polymorphic type.