Revision f2c916b4
Added by Guillaume DAVY over 4 years ago
src/backends/Ada/ada_backend_ads.ml | ||
---|---|---|
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 |
Also available in: Unified diff
Ada: Correct some errors on the type checking due to polymorphic type.