Revision ca7ff3f7
Added by LĂ©lio Brun over 1 year ago
src/backends/Ada/misc_lustre_function.ml  

1  
2  1 
open Machine_code_types 
3  2 
open Lustre_types 
4  3 
open Corelang 
5 
(* 

6 
open Machine_code_common 

7 
*) 

4 
(* open Machine_code_common *) 

8  5  
9  6 
let is_machine_statefull m = not m.mname.node_dec_stateless 
10  7  
11 
(** Return true if its the arrow machine 

12 
@param machine the machine to test 

13 
*) 

8 
(** Return true if its the arrow machine @param machine the machine to test *) 

14  9 
let is_arrow machine = String.equal Arrow.arrow_id machine.mname.node_id 
15  10  
16 
(** Extract a node from an instance. 

17 
@param instance the instance 

18 
**) 

11 
(** Extract a node from an instance. @param instance the instance **) 

19  12 
let extract_node instance = 
20 
let (_, (node, _)) = instance in 

21 
match node.top_decl_desc with 

22 
 Node nd > nd 

23 
 _ > assert false (*TODO*) 

13 
let _, (node, _) = instance in 

14 
match node.top_decl_desc with Node nd > nd  _ > assert false 

15 
(*TODO*) 

24  16  
25  17 
(** Extract from a machine list the one corresponding to the given instance. 
26 
assume that the machine is in the list. 

27 
@param machines list of all machines 

28 
@param instance instance of a machine 

29 
@return the machine corresponding to hte given instance 

30 
**) 

18 
assume that the machine is in the list. @param machines list of all machines 

19 
@param instance instance of a machine @return the machine corresponding to 

20 
hte given instance **) 

31  21 
let get_machine machines instance = 
32 
let id = (extract_node instance).node_id in 

33 
try 

34 
List.find (function m > m.mname.node_id=id) machines 

35 
with 

36 
Not_found > assert false (*TODO*) 

22 
let id = (extract_node instance).node_id in 

23 
try List.find (function m > m.mname.node_id = id) machines 

24 
with Not_found > assert false 

25 
(*TODO*) 

37  26  
38 
(** Extract all the inputs and outputs. 

39 
@param machine the machine 

40 
@return a list of all the var_decl of a macine 

41 
**) 

27 
(** Extract all the inputs and outputs. @param machine the machine @return a 

28 
list of all the var_decl of a macine **) 

42  29 
let get_all_vars_machine m = 
43 
m.mmemory@m.mstep.step_inputs@m.mstep.step_outputs@m.mstatic


30 
m.mmemory @ m.mstep.step_inputs @ m.mstep.step_outputs @ m.mstatic


44  31  
45 
(** Check if a type is polymorphic. 

46 
@param typ the type 

47 
@return true if its polymorphic 

48 
**) 

32 
(** Check if a type is polymorphic. @param typ the type @return true if its 

33 
polymorphic **) 

49  34 
let is_Tunivar typ = (Types.repr typ).tdesc == Types.Tunivar 
50  35  
51 
(** Find all polymorphic type : Types.Tunivar in a machine. 

52 
@param machine the machine 

53 
@return a list of id corresponding to polymorphic type 

54 
**) 

36 
(** Find all polymorphic type : Types.Tunivar in a machine. @param machine the 

37 
machine @return a list of id corresponding to polymorphic type **) 

55  38 
let find_all_polymorphic_type m = 
56  39 
let vars = get_all_vars_machine m in 
57  40 
let extract id = id.var_type.tid in 
58  41 
let polymorphic_type_vars = 
59 
List.filter (function x> is_Tunivar x.var_type) vars in


60 
List.sort_uniq () (List.map extract polymorphic_type_vars)


61  
42 
List.filter (function x > is_Tunivar x.var_type) vars


43 
in


44 
List.sort_uniq (  ) (List.map extract polymorphic_type_vars) 

62  45  
63 
(** Check if a submachine is statefull. 

64 
@param submachine a submachine 

65 
@return true if the submachine is statefull 

66 
**) 

46 
(** Check if a submachine is statefull. @param submachine a submachine @return 

47 
true if the submachine is statefull **) 

67  48 
let is_submachine_statefull submachine = 
68 
not (snd (snd submachine)).mname.node_dec_stateless


49 
not (snd (snd submachine)).mname.node_dec_stateless 

69  50  
70 
(** Find a submachine step call in a list of instructions. 

71 
@param ident submachine instance ident 

72 
@param instr_list List of instruction sto search 

73 
@return a list of pair containing input types and output types for each step call found 

74 
**) 

51 
(** Find a submachine step call in a list of instructions. @param ident 

52 
submachine instance ident @param instr_list List of instruction sto search 

53 
@return a list of pair containing input types and output types for each step 

54 
call found **) 

75  55 
let rec find_submachine_step_call ident instr_list = 
76 
let search_instr instruction =


56 
let search_instr instruction = 

77  57 
match instruction.instr_desc with 
78 
 MStep (il, i, vl) when String.equal i ident > [ 

79 
(List.map (function x> x.value_type) vl, 

80 
List.map (function x> x.var_type) il)] 

81 
 MBranch (_, l) > List.flatten 

82 
(List.map (function _, y > find_submachine_step_call ident y) l) 

83 
 _ > [] 

58 
 MStep (il, i, vl) when String.equal i ident > 

59 
[ 

60 
( List.map (function x > x.value_type) vl, 

61 
List.map (function x > x.var_type) il ); 

62 
] 

63 
 MBranch (_, l) > 

64 
List.flatten 

65 
(List.map (function _, y > find_submachine_step_call ident y) l) 

66 
 _ > 

67 
[] 

84  68 
in 
85  69 
List.flatten (List.map search_instr instr_list) 
86  70  
87  71 
(* Replace this function by check_type_equal but be careful to the fact that 
88 
this function chck equality and that it is both basic type. 

89 
This might be a required feature when it used *) 

90 
(** Test if two types are the same. 

91 
@param typ1 the first type 

92 
@param typ2 the second type 

93 
**) 

94 
let pp_eq_type typ1 typ2 = 

95 
let get_basic typ = match (Types.repr typ).Types.tdesc with 

96 
 Types.Tbasic Types.Basic.Tint > Types.Basic.Tint 

97 
 Types.Tbasic Types.Basic.Treal > Types.Basic.Treal 

98 
 Types.Tbasic Types.Basic.Tbool > Types.Basic.Tbool 

99 
 _ > assert false (*TODO*) 

72 
this function chck equality and that it is both basic type. This might be a 

73 
required feature when it used *) 

74  
75 
(** Test if two types are the same. @param typ1 the first type @param typ2 the 

76 
second type **) 

77 
let pp_eq_type typ1 typ2 = 

78 
let get_basic typ = 

79 
match (Types.repr typ).Types.tdesc with 

80 
 Types.Tbasic Types.Basic.Tint > 

81 
Types.Basic.Tint 

82 
 Types.Tbasic Types.Basic.Treal > 

83 
Types.Basic.Treal 

84 
 Types.Tbasic Types.Basic.Tbool > 

85 
Types.Basic.Tbool 

86 
 _ > 

87 
assert false 

88 
(*TODO*) 

100  89 
in 
101  90 
get_basic typ1 = get_basic typ2 
102  91  
103 
(** Check that two types are the same. 

104 
@param t1 a type 

105 
@param t2 an other type 

106 
@param return true if the two types are Tbasic or Tunivar and equal 

107 
**) 

108 
let rec check_type_equal (t1:Types.type_expr) (t2:Types.type_expr) = 

92 
(** Check that two types are the same. @param t1 a type @param t2 an other type 

93 
@param return true if the two types are Tbasic or Tunivar and equal **) 

94 
let rec check_type_equal (t1 : Types.type_expr) (t2 : Types.type_expr) = 

109  95 
match (Types.repr t1).Types.tdesc, (Types.repr t2).Types.tdesc with 
110 
 Types.Tbasic x, Types.Tbasic y > x = y 

111 
 Types.Tunivar, Types.Tunivar > t1.tid = t2.tid 

112 
 Types.Ttuple l, _ > assert (List.length l = 1); check_type_equal (List.hd l) t2 

113 
 _, Types.Ttuple l > assert (List.length l = 1); check_type_equal t1 (List.hd l) 

114 
 Types.Tstatic (_, t), _ > check_type_equal t t2 

115 
 _, Types.Tstatic (_, t) > check_type_equal t1 t 

116 
 _ > assert false 

96 
 Types.Tbasic x, Types.Tbasic y > 

97 
x = y 

98 
 Types.Tunivar, Types.Tunivar > 

99 
t1.tid = t2.tid 

100 
 Types.Ttuple l, _ > 

101 
assert (List.length l = 1); 

102 
check_type_equal (List.hd l) t2 

103 
 _, Types.Ttuple l > 

104 
assert (List.length l = 1); 

105 
check_type_equal t1 (List.hd l) 

106 
 Types.Tstatic (_, t), _ > 

107 
check_type_equal t t2 

108 
 _, Types.Tstatic (_, t) > 

109 
check_type_equal t1 t 

110 
 _ > 

111 
assert false 

117  112  
118 
(** Extend a substitution to unify the two given types. Only the 

119 
first type can be polymorphic. 

120 
@param subsitution the base substitution 

121 
@param type_poly the type which can be polymorphic 

122 
@param typ the type to match type_poly with 

123 
**) 

124 
let unification (substituion:(int*Types.type_expr) list) ((type_poly:Types.type_expr), (typ:Types.type_expr)) = 

125 
assert(not (is_Tunivar typ)); 

113 
(** Extend a substitution to unify the two given types. Only the first type can 

114 
be polymorphic. @param subsitution the base substitution @param type_poly 

115 
the type which can be polymorphic @param typ the type to match type_poly 

116 
with **) 

117 
let unification (substituion : (int * Types.type_expr) list) 

118 
((type_poly : Types.type_expr), (typ : Types.type_expr)) = 

119 
assert (not (is_Tunivar typ)); 

126  120 
(* If type_poly is polymorphic *) 
127  121 
if is_Tunivar type_poly then 
128  122 
(* If a subsitution exists for it *) 
129 
if List.mem_assoc type_poly.tid substituion then 

130 
begin 

123 
if List.mem_assoc type_poly.tid substituion then ( 

131  124 
(* We check that the type corresponding to type_poly in the subsitution 
132  125 
match typ *) 
133 
(try 

134 
assert(check_type_equal (List.assoc type_poly.tid substituion) typ) 

135 
with 

136 
Not_found > assert false); 

126 
(try assert (check_type_equal (List.assoc type_poly.tid substituion) typ) 

127 
with Not_found > assert false); 

137  128 
(* We return the original substituion, it is already correct *) 
138  129 
substituion 
139 
end 

140 
(* If type_poly is not in the subsitution *) 

141 
else 

142 
(* We add it to the substituion *) 

143 
(type_poly.tid, typ)::substituion 

144 
(* iftype_poly is not polymorphic *) 

145 
else 

146 
begin 

130 
(* If type_poly is not in the subsitution *)) 

131 
else (* We add it to the substituion *) 

132 
(type_poly.tid, typ) :: substituion (* iftype_poly is not polymorphic *) 

133 
else ( 

147  134 
(* We check that type_poly and typ are the same *) 
148 
assert(check_type_equal type_poly typ); 

135 
assert (check_type_equal type_poly typ);


149  136 
(* We return the original substituion, it is already correct *) 
150 
substituion 

151 
end 

137 
substituion) 

152  138  
153 
(** Check that two calls are equal. A call is 

154 
a pair of list of types, the inputs and the outputs. 

155 
@param calls a list of pair of list of types 

156 
@param return true if the two pairs are equal 

157 
**) 

139 
(** Check that two calls are equal. A call is a pair of list of types, the 

140 
inputs and the outputs. @param calls a list of pair of list of types @param 

141 
return true if the two pairs are equal **) 

158  142 
let check_call_equal (i1, _) (i2, _) = 
159 
(List.for_all2 check_type_equal i1 i2) 

160 
&& (List.for_all2 check_type_equal i1 i2) 

143 
List.for_all2 check_type_equal i1 i2 && List.for_all2 check_type_equal i1 i2 

161  144  
162 
(** Check that all the elements of list of calls are equal to one. 

163 
A call is a pair of list of types, the inputs and the outputs. 

164 
@param call a pair of list of types 

165 
@param calls a list of pair of list of types 

166 
@param return true if all the elements are equal 

167 
**) 

168 
let check_calls call calls = 

169 
List.for_all (check_call_equal call) calls 

145 
(** Check that all the elements of list of calls are equal to one. A call is a 

146 
pair of list of types, the inputs and the outputs. @param call a pair of 

147 
list of types @param calls a list of pair of list of types @param return 

148 
true if all the elements are equal **) 

149 
let check_calls call calls = List.for_all (check_call_equal call) calls 

170  150  
171  151 
(** Extract from a subinstance that can have polymorphic type the instantiation 
172  152 
of all its polymorphic type instanciation for a given machine. It searches 
173 
the step calls and extract a substitution for all polymorphic type from 

174 
it. 

175 
@param machine the machine which instantiate the subinstance 

176 
@param ident the identifier of the instance which permits to find the step call 

177 
@param submachine the machine corresponding to the subinstance 

178 
@return the correspondance between polymorphic type id and their instantiation 

179 
**) 

153 
the step calls and extract a substitution for all polymorphic type from it. 

154 
@param machine the machine which instantiate the subinstance @param ident 

155 
the identifier of the instance which permits to find the step call @param 

156 
submachine the machine corresponding to the subinstance @return the 

157 
correspondance between polymorphic type id and their instantiation **) 

180  158 
let get_substitution machine ident submachine = 
181  159 
(* extract the calls to submachines from the machine *) 
182  160 
let calls = find_submachine_step_call ident machine.mstep.step_instrs in 
183 
(* extract the first call *) 

184 
let call = match calls with 

185 
(* assume that there is always one call to a subinstance *) 

186 
 [] > assert(false) 

187 
 h::_ > h in 

161 
(* extract the first call *) 

162 
let call = 

163 
match calls with 

164 
(* assume that there is always one call to a subinstance *) 

165 
 [] > 

166 
assert false 

167 
 h :: _ > 

168 
h 

169 
in 

188  170 
(* assume that all the calls to a subinstance are using the same type *) 
189 
assert(check_calls call calls); 

171 
assert (check_calls call calls);


190  172 
(* make a list of all types from input and output vars *) 
191 
let call_types = (fst call)@(snd call) in


173 
let call_types = fst call @ snd call in


192  174 
(* extract all the input and output vars from the submachine *) 
193 
let machine_vars = submachine.mstep.step_inputs@submachine.mstep.step_outputs in 

175 
let machine_vars = 

176 
submachine.mstep.step_inputs @ submachine.mstep.step_outputs 

177 
in 

194  178 
(* keep only the type of vars *) 
195 
let machine_types = List.map (function x> x.var_type) machine_vars in 

179 
let machine_types = List.map (function x > x.var_type) machine_vars in


196  180 
(* assume that there is the same numer of input and output in the submachine 
197 
and the call *)


181 
and the call *) 

198  182 
assert (List.length machine_types = List.length call_types); 
199  183 
(* Unify the two lists of types *) 
200 
let substitution = List.fold_left unification [] (List.combine machine_types call_types) in 

201 
(* Assume that our substitution match all the possible 

202 
polymorphic type of the node *) 

184 
let substitution = 

185 
List.fold_left unification [] (List.combine machine_types call_types) 

186 
in 

187 
(* Assume that our substitution match all the possible polymorphic type of the 

188 
node *) 

203  189 
let polymorphic_types = find_all_polymorphic_type submachine in 
204  190 
assert (List.length polymorphic_types = List.length substitution); 
205  191 
(try 
206 
assert (List.for_all (fun x > List.mem_assoc x substitution) polymorphic_types)


207 
with


208 
Not_found > assert false); 

192 
assert (


193 
List.for_all (fun x > List.mem_assoc x substitution) polymorphic_types)


194 
with Not_found > assert false);


209  195 
substitution 
210  196  
197 
(** Extract from a machine the instance corresponding to the identifier, assume 

198 
that the identifier exists in the instances of the machine. 

211  199  
212 
(** Extract from a machine the instance corresponding to the identifier, 

213 
assume that the identifier exists in the instances of the machine. 

214  
215 
@param identifier the instance identifier 

216 
@param machine a machine 

217 
@return the instance of machine.minstances corresponding to identifier 

218 
**) 

200 
@param identifier the instance identifier @param machine a machine @return 

201 
the instance of machine.minstances corresponding to identifier **) 

219  202 
let get_instance identifier typed_submachines = 
220 
try 

221 
List.assoc identifier typed_submachines 

222 
with Not_found > assert false 

203 
try List.assoc identifier typed_submachines with Not_found > assert false 

223  204  
224  205 
(*Usefull for debug*) 
225 
let pp_type_debug fmt typ = 

226 
(match (Types.repr typ).Types.tdesc with 

227 
 Types.Tbasic Types.Basic.Tint > Format.fprintf fmt "INTEGER" 

228 
 Types.Tbasic Types.Basic.Treal > Format.fprintf fmt "FLOAT" 

229 
 Types.Tbasic Types.Basic.Tbool > Format.fprintf fmt "BOOLEAN" 

230 
 Types.Tunivar > Format.fprintf fmt "POLY(%i)" typ.Types.tid 

231 
 _ > assert false 

232 
) 

206 
let pp_type_debug fmt typ = 

207 
match (Types.repr typ).Types.tdesc with 

208 
 Types.Tbasic Types.Basic.Tint > 

209 
Format.fprintf fmt "INTEGER" 

210 
 Types.Tbasic Types.Basic.Treal > 

211 
Format.fprintf fmt "FLOAT" 

212 
 Types.Tbasic Types.Basic.Tbool > 

213 
Format.fprintf fmt "BOOLEAN" 

214 
 Types.Tunivar > 

215 
Format.fprintf fmt "POLY(%i)" typ.Types.tid 

216 
 _ > 

217 
assert false 

233  218  
234  219 
let build_if g c1 i1 tl = 
235 
let neg = c1=tag_false in 

236 
let other = match tl with 

237 
 [] > None 

238 
 [(_, i2)] > Some i2 

239 
 _ > assert false 

220 
let neg = c1 = tag_false in 

221 
let other = 

222 
match tl with [] > None  [ (_, i2) ] > Some i2  _ > assert false 

240  223 
in 
241  224 
match neg, other with 
242 
 true, Some x > (false, g, x, Some i1) 

243 
 _ > 

244 
(neg, g, i1, other) 

225 
 true, Some x > 

226 
false, g, x, Some i1 

227 
 _ > 

228 
neg, g, i1, other 

245  229  
246  230 
let rec push_if_in_expr = function 
247 
 [] > [] 

248 
 instr::q > 

249 
( 

250 
match get_instr_desc instr with 

251 
 MBranch (g, (c1, i1)::tl) when c1=tag_false  c1=tag_true > 

252 
let (_, g, instrs1, instrs2) = build_if g c1 i1 tl in 

253 
let instrs1_pushed = push_if_in_expr instrs1 in 

254 
let get_assign instr = match get_instr_desc instr with 

255 
 MLocalAssign (id, value) > (false, id, value) 

256 
 MStateAssign (id, value) > (true, id, value) 

257 
 _ > assert false 

258 
in 

259 
let gen_eq ident state value1 value2 = 

260 
assert(check_type_equal ident.var_type value1.value_type); 

261 
assert(check_type_equal ident.var_type value2.value_type); 

262 
let value = { 

263 
value_desc = Fun ("ite", [g;value1;value2]); 

264 
value_type = ident.var_type; 

265 
value_annot = None 

266 
} 

267 
in 

268 
let assign = if state then MStateAssign (ident, value) else MLocalAssign (ident, value) in 

269 
{ instr_desc = assign; 

270 
lustre_eq = None; 

271 
instr_spec = [] 

272 
} 

273 
in 

274 
let mkval_var id = { 

275 
value_desc = Var id; 

276 
value_type = id.var_type; 

277 
value_annot = None 

278 
} 

279 
in 

280 
let rec find_split s1 id1 accu = function 

281 
 [] > [], accu, mkval_var id1 

282 
 (s2, id2, v2)::q when s1 = s2 

283 
&& id1.var_id = id2.var_id > accu, q, v2 

284 
 t::q > find_split s1 id1 (t::accu) q 

285 
in 

286 
let gen_from_else l = 

287 
List.map 

288 
(fun (s2, id2, v2) > gen_eq id2 s2 (mkval_var id2) v2) 

289 
l 

290 
in 

291 
let rec gen_assigns if_assigns else_assigns = 

292 
let res, accu_else = match if_assigns with 

293 
 (s1, id1, v1)::q > 

294 
let accu, remain, v2 = find_split s1 id1 [] else_assigns in 

295 
(gen_eq id1 s1 v1 v2)::(gen_assigns q remain), accu 

296 
 [] > [], else_assigns 

297 
in 

298 
(gen_from_else accu_else)@res 

299 
in 

300 
let if_assigns = List.map get_assign instrs1_pushed in 

301 
let else_assigns = match instrs2 with 

302 
 None > [] 

303 
 Some instrs2 > 

304 
let instrs2_pushed = push_if_in_expr instrs2 in 

305 
List.map get_assign instrs2_pushed 

306 
in 

307 
gen_assigns if_assigns else_assigns 

308 
 _ > [instr] 

309 
)@(push_if_in_expr q) 

310  
311  
312  
313  
231 
 [] > 

232 
[] 

233 
 instr :: q > 

234 
(match get_instr_desc instr with 

235 
 MBranch (g, (c1, i1) :: tl) when c1 = tag_false  c1 = tag_true > 

236 
let _, g, instrs1, instrs2 = build_if g c1 i1 tl in 

237 
let instrs1_pushed = push_if_in_expr instrs1 in 

238 
let get_assign instr = 

239 
match get_instr_desc instr with 

240 
 MLocalAssign (id, value) > 

241 
false, id, value 

242 
 MStateAssign (id, value) > 

243 
true, id, value 

244 
 _ > 

245 
assert false 

246 
in 

247 
let gen_eq ident state value1 value2 = 

248 
assert (check_type_equal ident.var_type value1.value_type); 

249 
assert (check_type_equal ident.var_type value2.value_type); 

250 
let value = 

251 
{ 

252 
value_desc = Fun ("ite", [ g; value1; value2 ]); 

253 
value_type = ident.var_type; 

254 
value_annot = None; 

255 
} 

256 
in 

257 
let assign = 

258 
if state then MStateAssign (ident, value) 

259 
else MLocalAssign (ident, value) 

260 
in 

261 
{ instr_desc = assign; lustre_eq = None; instr_spec = [] } 

262 
in 

263 
let mkval_var id = 

264 
{ value_desc = Var id; value_type = id.var_type; value_annot = None } 

265 
in 

266 
let rec find_split s1 id1 accu = function 

267 
 [] > 

268 
[], accu, mkval_var id1 

269 
 (s2, id2, v2) :: q when s1 = s2 && id1.var_id = id2.var_id > 

270 
accu, q, v2 

271 
 t :: q > 

272 
find_split s1 id1 (t :: accu) q 

273 
in 

274 
let gen_from_else l = 

275 
List.map (fun (s2, id2, v2) > gen_eq id2 s2 (mkval_var id2) v2) l 

276 
in 

277 
let rec gen_assigns if_assigns else_assigns = 

278 
let res, accu_else = 

279 
match if_assigns with 

280 
 (s1, id1, v1) :: q > 

281 
let accu, remain, v2 = find_split s1 id1 [] else_assigns in 

282 
gen_eq id1 s1 v1 v2 :: gen_assigns q remain, accu 

283 
 [] > 

284 
[], else_assigns 

285 
in 

286 
gen_from_else accu_else @ res 

287 
in 

288 
let if_assigns = List.map get_assign instrs1_pushed in 

289 
let else_assigns = 

290 
match instrs2 with 

291 
 None > 

292 
[] 

293 
 Some instrs2 > 

294 
let instrs2_pushed = push_if_in_expr instrs2 in 

295 
List.map get_assign instrs2_pushed 

296 
in 

297 
gen_assigns if_assigns else_assigns 

298 
 _ > 

299 
[ instr ]) 

300 
@ push_if_in_expr q 
Also available in: Unified diff
reformatting