Revision ca7ff3f7
Added by LĂ©lio Brun over 1 year ago
src/plugins/mpfr/lustrec_mpfr.ml  

17  17 
open Machine_code_common 
18  18  
19  19 
let report = Log.report ~plugin:"MPFR" 
20 


21 
let mpfr_module = mktop (Open(false, "mpfr_lustre")) 

20  
21 
let mpfr_module = mktop (Open (false, "mpfr_lustre")) 

22  
22  23 
let cpt_fresh = ref 0 
23 


24  
24  25 
let mpfr_rnd () = "MPFR_RNDN" 
25  26  
26  27 
let mpfr_prec () = !Options.mpfr_prec 
...  ...  
41  42 
not (Types.is_real_type value.value_type && is_const_value value) 
42  43  
43  44 
let inject_id_id expr = 
44 
let e = mkpredef_call expr.expr_loc inject_id [expr] in 

45 
{ e with 

46 
expr_type = Type_predef.type_real; 

47 
expr_clock = expr.expr_clock; 

48 
} 

45 
let e = mkpredef_call expr.expr_loc inject_id [ expr ] in 

46 
{ e with expr_type = Type_predef.type_real; expr_clock = expr.expr_clock } 

49  47  
50  48 
let pp_inject_real pp_var pp_val fmt (var, value) = 
51 
Format.fprintf fmt "%s(%a, %a, %s);" 

52 
inject_real_id 

53 
pp_var var 

54 
pp_val value 

49 
Format.fprintf fmt "%s(%a, %a, %s);" inject_real_id pp_var var pp_val value 

55  50 
(mpfr_rnd ()) 
56  51  
57  52 
let inject_assign expr = 
58 
let e = mkpredef_call expr.expr_loc inject_copy_id [expr] in 

59 
{ e with 

60 
expr_type = Type_predef.type_real; 

61 
expr_clock = expr.expr_clock; 

62 
} 

53 
let e = mkpredef_call expr.expr_loc inject_copy_id [ expr ] in 

54 
{ e with expr_type = Type_predef.type_real; expr_clock = expr.expr_clock } 

63  55  
64  56 
let pp_inject_copy pp_var fmt (var, value) = 
65 
Format.fprintf fmt "%s(%a, %a, %s);" 

66 
inject_copy_id 

67 
pp_var var 

68 
pp_var value 

57 
Format.fprintf fmt "%s(%a, %a, %s);" inject_copy_id pp_var var pp_var value 

69  58 
(mpfr_rnd ()) 
70  59  
71 
let pp_inject_assign pp_var fmt (_, value as vv) = 

72 
if is_const_value value 

73 
then 

74 
pp_inject_real pp_var pp_var fmt vv 

75 
else 

76 
pp_inject_copy pp_var fmt vv 

60 
let pp_inject_assign pp_var fmt ((_, value) as vv) = 

61 
if is_const_value value then pp_inject_real pp_var pp_var fmt vv 

62 
else pp_inject_copy pp_var fmt vv 

77  63  
78  64 
let pp_inject_init pp_var fmt var = 
79 
Format.fprintf fmt "%s(%a, %i);" 

80 
inject_init_id 

81 
pp_var var 

82 
(mpfr_prec ()) 

65 
Format.fprintf fmt "%s(%a, %i);" inject_init_id pp_var var (mpfr_prec ()) 

83  66  
84  67 
let pp_inject_clear pp_var fmt var = 
85 
Format.fprintf fmt "%s(%a);" 

86 
inject_clear_id 

87 
pp_var var 

68 
Format.fprintf fmt "%s(%a);" inject_clear_id pp_var var 

88  69  
89  70 
let base_inject_op id = 
90  71 
match id with 
91 
 "+" > "MPFRPlus" 

92 
 "" > "MPFRMinus" 

93 
 "*" > "MPFRTimes" 

94 
 "/" > "MPFRDiv" 

95 
 "uminus" > "MPFRUminus" 

96 
 "<=" > "MPFRLe" 

97 
 "<" > "MPFRLt" 

98 
 ">=" > "MPFRGe" 

99 
 ">" > "MPFRGt" 

100 
 "=" > "MPFREq" 

101 
 "!=" > "MPFRNeq" 

72 
 "+" > 

73 
"MPFRPlus" 

74 
 "" > 

75 
"MPFRMinus" 

76 
 "*" > 

77 
"MPFRTimes" 

78 
 "/" > 

79 
"MPFRDiv" 

80 
 "uminus" > 

81 
"MPFRUminus" 

82 
 "<=" > 

83 
"MPFRLe" 

84 
 "<" > 

85 
"MPFRLt" 

86 
 ">=" > 

87 
"MPFRGe" 

88 
 ">" > 

89 
"MPFRGt" 

90 
 "=" > 

91 
"MPFREq" 

92 
 "!=" > 

93 
"MPFRNeq" 

102  94 
(* Conv functions *) 
103 
 "int_to_real" > "MPFRint_to_real" 

104 
 "real_to_int" > "MPFRreal_to_int" 

105 
 "_floor" > "MPFRfloor" 

106 
 "_ceil" > "MPFRceil" 

107 
 "_round" > "MPFRround" 

108 
 "_Floor" > "MPFRFloor" 

109 
 "_Ceiling" > "MPFRCeiling" 

110 
 "_Round" > "MPFRRound" 

111 


95 
 "int_to_real" > 

96 
"MPFRint_to_real" 

97 
 "real_to_int" > 

98 
"MPFRreal_to_int" 

99 
 "_floor" > 

100 
"MPFRfloor" 

101 
 "_ceil" > 

102 
"MPFRceil" 

103 
 "_round" > 

104 
"MPFRround" 

105 
 "_Floor" > 

106 
"MPFRFloor" 

107 
 "_Ceiling" > 

108 
"MPFRCeiling" 

109 
 "_Round" > 

110 
"MPFRRound" 

112  111 
(* Math library functions *) 
113 
 "acos" > "MPFRacos" 

114 
 "acosh" > "MPFRacosh" 

115 
 "asin" > "MPFRasin" 

116 
 "asinh" > "MPFRasinh" 

117 
 "atan" > "MPFRatan" 

118 
 "atan2" > "MPFRatan2" 

119 
 "atanh" > "MPFRatanh" 

120 
 "cbrt" > "MPFRcbrt" 

121 
 "cos" > "MPFRcos" 

122 
 "cosh" > "MPFRcosh" 

123 
 "ceil" > "MPFRceil" 

124 
 "erf" > "MPFRerf" 

125 
 "exp" > "MPFRexp" 

126 
 "fabs" > "MPFRfabs" 

127 
 "floor" > "MPFRfloor" 

128 
 "fmod" > "MPFRfmod" 

129 
 "log" > "MPFRlog" 

130 
 "log10" > "MPFRlog10" 

131 
 "pow" > "MPFRpow" 

132 
 "round" > "MPFRround" 

133 
 "sin" > "MPFRsin" 

134 
 "sinh" > "MPFRsinh" 

135 
 "sqrt" > "MPFRsqrt" 

136 
 "trunc" > "MPFRtrunc" 

137 
 "tan" > "MPFRtan" 

138 
 _ > raise Not_found 

112 
 "acos" > 

113 
"MPFRacos" 

114 
 "acosh" > 

115 
"MPFRacosh" 

116 
 "asin" > 

117 
"MPFRasin" 

118 
 "asinh" > 

119 
"MPFRasinh" 

120 
 "atan" > 

121 
"MPFRatan" 

122 
 "atan2" > 

123 
"MPFRatan2" 

124 
 "atanh" > 

125 
"MPFRatanh" 

126 
 "cbrt" > 

127 
"MPFRcbrt" 

128 
 "cos" > 

129 
"MPFRcos" 

130 
 "cosh" > 

131 
"MPFRcosh" 

132 
 "ceil" > 

133 
"MPFRceil" 

134 
 "erf" > 

135 
"MPFRerf" 

136 
 "exp" > 

137 
"MPFRexp" 

138 
 "fabs" > 

139 
"MPFRfabs" 

140 
 "floor" > 

141 
"MPFRfloor" 

142 
 "fmod" > 

143 
"MPFRfmod" 

144 
 "log" > 

145 
"MPFRlog" 

146 
 "log10" > 

147 
"MPFRlog10" 

148 
 "pow" > 

149 
"MPFRpow" 

150 
 "round" > 

151 
"MPFRround" 

152 
 "sin" > 

153 
"MPFRsin" 

154 
 "sinh" > 

155 
"MPFRsinh" 

156 
 "sqrt" > 

157 
"MPFRsqrt" 

158 
 "trunc" > 

159 
"MPFRtrunc" 

160 
 "tan" > 

161 
"MPFRtan" 

162 
 _ > 

163 
raise Not_found 

139  164  
140  165 
let inject_op id = 
141 
report ~level:3 (fun fmt > Format.fprintf fmt "trying to inject mpfr into function %s@." id); 

142 
try 

143 
base_inject_op id 

144 
with Not_found > id 

166 
report ~level:3 (fun fmt > 

167 
Format.fprintf fmt "trying to inject mpfr into function %s@." id); 

168 
try base_inject_op id with Not_found > id 

145  169  
146  170 
let homomorphic_funs = 
147 
List.fold_right (fun id res > try base_inject_op id :: res with Not_found > res) Basic_library.internal_funs [] 

171 
List.fold_right 

172 
(fun id res > try base_inject_op id :: res with Not_found > res) 

173 
Basic_library.internal_funs [] 

148  174  
149 
let is_homomorphic_fun id = 

150 
List.mem id homomorphic_funs 

175 
let is_homomorphic_fun id = List.mem id homomorphic_funs 

151  176  
152  177 
let inject_call expr = 
153  178 
match expr.expr_desc with 
154 
 Expr_appl (id, args, None) when not (Basic_library.is_expr_internal_fun expr) > 

179 
 Expr_appl (id, args, None) 

180 
when not (Basic_library.is_expr_internal_fun expr) > 

155  181 
{ expr with expr_desc = Expr_appl (inject_op id, args, None) } 
156 
 _ > expr 

182 
 _ > 

183 
expr 

157  184  
158  185 
let expr_of_const_array expr = 
159  186 
match expr.expr_desc with 
160  187 
 Expr_const (Const_array cl) > 
161  188 
let typ = Types.array_element_type expr.expr_type in 
162  189 
let expr_of_const c = 
163 
{ expr_desc = Expr_const c; 

164 
expr_type = typ; 

165 
expr_clock = expr.expr_clock; 

166 
expr_loc = expr.expr_loc; 

167 
expr_delay = Delay.new_var (); 

168 
expr_annot = None; 

169 
expr_tag = new_tag (); 

190 
{ 

191 
expr_desc = Expr_const c; 

192 
expr_type = typ; 

193 
expr_clock = expr.expr_clock; 

194 
expr_loc = expr.expr_loc; 

195 
expr_delay = Delay.new_var (); 

196 
expr_annot = None; 

197 
expr_tag = new_tag (); 

170  198 
} 
171 
in { expr with expr_desc = Expr_array (List.map expr_of_const cl) } 

172 
 _ > assert false 

199 
in 

200 
{ expr with expr_desc = Expr_array (List.map expr_of_const cl) } 

201 
 _ > 

202 
assert false 

173  203  
174 
(* inject_<foo> : defs * used vars > <foo> > (updated defs * updated vars) * normalized <foo> *) 

204 
(* inject_<foo> : defs * used vars > <foo> > (updated defs * updated vars) * 

205 
normalized <foo> *) 

175  206 
let inject_list alias node inject_element defvars elist = 
176  207 
List.fold_right 
177  208 
(fun t (defvars, qlist) > 
178  209 
let defvars, norm_t = inject_element alias node defvars t in 
179 
(defvars, norm_t :: qlist) 

180 
) elist (defvars, []) 

181  
182 
let rec inject_expr ?(alias=true) node defvars expr = 

183 
let res = 

184 
match expr.expr_desc with 

185 
 Expr_const (Const_real _) > mk_expr_alias_opt alias node defvars expr 

186 
 Expr_const (Const_array _) > inject_expr ~alias:alias node defvars (expr_of_const_array expr) 

187 
 Expr_const (Const_struct _) > assert false 

188 
 Expr_ident _ 

189 
 Expr_const _ > defvars, expr 

190 
 Expr_array elist > 

191 
let defvars, norm_elist = inject_list alias node (fun _ > inject_expr ~alias:true) defvars elist in 

192 
let norm_expr = { expr with expr_desc = Expr_array norm_elist } in 

193 
defvars, norm_expr 

194 
 Expr_power (e1, d) > 

195 
let defvars, norm_e1 = inject_expr node defvars e1 in 

196 
let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in 

197 
defvars, norm_expr 

198 
 Expr_access (e1, d) > 

199 
let defvars, norm_e1 = inject_expr node defvars e1 in 

200 
let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in 

201 
defvars, norm_expr 

202 
 Expr_tuple elist > 

203 
let defvars, norm_elist = 

204 
inject_list alias node (fun alias > inject_expr ~alias:alias) defvars elist in 

205 
let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in 

206 
defvars, norm_expr 

207 
 Expr_appl (id, args, r) > 

208 
let defvars, norm_args = inject_expr node defvars args in 

209 
let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in 

210 
mk_expr_alias_opt alias node defvars (inject_call norm_expr) 

211 
 Expr_arrow _ > defvars, expr 

212 
 Expr_pre e > 

213 
let defvars, norm_e = inject_expr node defvars e in 

214 
let norm_expr = { expr with expr_desc = Expr_pre norm_e } in 

215 
defvars, norm_expr 

216 
 Expr_fby (e1, e2) > 

217 
let defvars, norm_e1 = inject_expr node defvars e1 in 

218 
let defvars, norm_e2 = inject_expr node defvars e2 in 

219 
let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in 

220 
defvars, norm_expr 

221 
 Expr_when (e, c, l) > 

222 
let defvars, norm_e = inject_expr node defvars e in 

223 
let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in 

224 
defvars, norm_expr 

225 
 Expr_ite (c, t, e) > 

226 
let defvars, norm_c = inject_expr node defvars c in 

227 
let defvars, norm_t = inject_expr node defvars t in 

228 
let defvars, norm_e = inject_expr node defvars e in 

229 
let norm_expr = { expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) } in 

230 
defvars, norm_expr 

231 
 Expr_merge (c, hl) > 

232 
let defvars, norm_hl = inject_branches node defvars hl in 

233 
let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in 

234 
defvars, norm_expr 

235 
in 

236 
(*Format.eprintf "inject_expr %B %a = %a@." alias Printers.pp_expr expr Printers.pp_expr (snd res);*) 

237 
res 

210 
defvars, norm_t :: qlist) 

211 
elist (defvars, []) 

212  
213 
let rec inject_expr ?(alias = true) node defvars expr = 

214 
let res = 

215 
match expr.expr_desc with 

216 
 Expr_const (Const_real _) > 

217 
mk_expr_alias_opt alias node defvars expr 

218 
 Expr_const (Const_array _) > 

219 
inject_expr ~alias node defvars (expr_of_const_array expr) 

220 
 Expr_const (Const_struct _) > 

221 
assert false 

222 
 Expr_ident _  Expr_const _ > 

223 
defvars, expr 

224 
 Expr_array elist > 

225 
let defvars, norm_elist = 

226 
inject_list alias node (fun _ > inject_expr ~alias:true) defvars elist 

227 
in 

228 
let norm_expr = { expr with expr_desc = Expr_array norm_elist } in 

229 
defvars, norm_expr 

230 
 Expr_power (e1, d) > 

231 
let defvars, norm_e1 = inject_expr node defvars e1 in 

232 
let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in 

233 
defvars, norm_expr 

234 
 Expr_access (e1, d) > 

235 
let defvars, norm_e1 = inject_expr node defvars e1 in 

236 
let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in 

237 
defvars, norm_expr 

238 
 Expr_tuple elist > 

239 
let defvars, norm_elist = 

240 
inject_list alias node (fun alias > inject_expr ~alias) defvars elist 

241 
in 

242 
let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in 

243 
defvars, norm_expr 

244 
 Expr_appl (id, args, r) > 

245 
let defvars, norm_args = inject_expr node defvars args in 

246 
let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in 

247 
mk_expr_alias_opt alias node defvars (inject_call norm_expr) 

248 
 Expr_arrow _ > 

249 
defvars, expr 

250 
 Expr_pre e > 

251 
let defvars, norm_e = inject_expr node defvars e in 

252 
let norm_expr = { expr with expr_desc = Expr_pre norm_e } in 

253 
defvars, norm_expr 

254 
 Expr_fby (e1, e2) > 

255 
let defvars, norm_e1 = inject_expr node defvars e1 in 

256 
let defvars, norm_e2 = inject_expr node defvars e2 in 

257 
let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in 

258 
defvars, norm_expr 

259 
 Expr_when (e, c, l) > 

260 
let defvars, norm_e = inject_expr node defvars e in 

261 
let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in 

262 
defvars, norm_expr 

263 
 Expr_ite (c, t, e) > 

264 
let defvars, norm_c = inject_expr node defvars c in 

265 
let defvars, norm_t = inject_expr node defvars t in 

266 
let defvars, norm_e = inject_expr node defvars e in 

267 
let norm_expr = 

268 
{ expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) } 

269 
in 

270 
defvars, norm_expr 

271 
 Expr_merge (c, hl) > 

272 
let defvars, norm_hl = inject_branches node defvars hl in 

273 
let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in 

274 
defvars, norm_expr 

275 
in 

276 
(*Format.eprintf "inject_expr %B %a = %a@." alias Printers.pp_expr expr 

277 
Printers.pp_expr (snd res);*) 

278 
res 

238  279  
239  280 
and inject_branches node defvars hl = 
240 
List.fold_right 

241 
(fun (t, h) (defvars, norm_q) > 

242 
let (defvars, norm_h) = inject_expr node defvars h in 

243 
defvars, (t, norm_h) :: norm_q 

244 
) 

245 
hl (defvars, []) 

246  
281 
List.fold_right 

282 
(fun (t, h) (defvars, norm_q) > 

283 
let defvars, norm_h = inject_expr node defvars h in 

284 
defvars, (t, norm_h) :: norm_q) 

285 
hl (defvars, []) 

247  286  
248  287 
let inject_eq node defvars eq = 
249 
let (defs', vars'), norm_rhs = inject_expr ~alias:false node defvars eq.eq_rhs in 

288 
let (defs', vars'), norm_rhs = 

289 
inject_expr ~alias:false node defvars eq.eq_rhs 

290 
in 

250  291 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
251 
norm_eq::defs', vars'


292 
norm_eq :: defs', vars'


252  293  
253  294 
(* let inject_eexpr ee = 
254  295 
* { ee with eexpr_qfexpr = inject_expr ee.eexpr_qfexpr } 
...  ...  
264  305 
* } 
265  306 
* ) s.modes 
266  307 
* } *) 
267 


268 
(** normalize_node node returns a normalized node, 

269 
ie. 

270 
 updated locals 

271 
 new equations 

272 
 

273 
*) 

274 
let inject_node node = 

308  
309 
(** normalize_node node returns a normalized node, ie.  updated locals  new 

310 
equations  *) 

311 
let inject_node node = 

275  312 
cpt_fresh := 0; 
276 
let inputs_outputs = node.node_inputs@node.node_outputs in 

277 
let norm_ctx = (node.node_id, get_node_vars node) in 

278 
let is_local v = 

279 
List.for_all ((!=) v) inputs_outputs in 

280 
let orig_vars = inputs_outputs@node.node_locals in 

313 
let inputs_outputs = node.node_inputs @ node.node_outputs in 

314 
let norm_ctx = node.node_id, get_node_vars node in 

315 
let is_local v = List.for_all (( != ) v) inputs_outputs in 

316 
let orig_vars = inputs_outputs @ node.node_locals in 

281  317 
let defs, vars = 
282  318 
let eqs, auts = get_node_eqs node in 
283 
if auts != [] then assert false; (* Automata should be expanded by now. *) 

284 
List.fold_left (inject_eq norm_ctx) ([], orig_vars) eqs in 

319 
if auts != [] then assert false; 

320 
(* Automata should be expanded by now. *) 

321 
List.fold_left (inject_eq norm_ctx) ([], orig_vars) eqs 

322 
in 

285  323 
(* Normalize the asserts *) 
286  324 
let vars, assert_defs, _ = 
287 
List.fold_left ( 

288 
fun (vars, def_accu, assert_accu) assert_ > 

289 
let assert_expr = assert_.assert_expr in 

290 
let (defs, vars'), expr = 

291 
inject_expr 

292 
~alias:false 

293 
norm_ctx 

294 
([], vars) (* defvar only contains vars *) 

295 
assert_expr 

296 
in 

297 
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu 

298 
) (vars, [], []) node.node_asserts in 

325 
List.fold_left 

326 
(fun (vars, def_accu, assert_accu) assert_ > 

327 
let assert_expr = assert_.assert_expr in 

328 
let (defs, vars'), expr = 

329 
inject_expr ~alias:false norm_ctx ([], vars) 

330 
(* defvar only contains vars *) 

331 
assert_expr 

332 
in 

333 
( vars', 

334 
defs @ def_accu, 

335 
{ assert_ with assert_expr = expr } :: assert_accu )) 

336 
(vars, [], []) node.node_asserts 

337 
in 

299  338 
let new_locals = List.filter is_local vars in 
300 
(* Compute traceability info: 

301 
 gather newly bound variables 

302 
 compute the associated expression without aliases 

303 
*) 

304 
(* let diff_vars = List.filter (fun v > not (List.mem v node.node_locals)) new_locals in *) 

339 
(* Compute traceability info:  gather newly bound variables  compute the 

340 
associated expression without aliases *) 

341 
(* let diff_vars = List.filter (fun v > not (List.mem v node.node_locals)) 

342 
new_locals in *) 

305  343 
(* See comment below 
306  344 
* let spec = match node.node_spec with 
307  345 
*  None > None 
308  346 
*  Some spec > Some (inject_spec spec) 
309  347 
* in *) 
310  348 
let node = 
311 
{ node with 

312 
node_locals = new_locals; 

313 
node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs); 

314 
(* Incomplete work: TODO. Do we have to inject MPFR code here? 

315 
Does it make sense for annotations? For me, only if we produce 

316 
C code for annotations. Otherwise the various verification 

317 
backend should have their own understanding, but would not 

318 
necessarily require this additional normalization. *) 

319 
(* 

320 
node_spec = spec; 

321 
node_annot = List.map (fun ann > {ann with 

322 
annots = List.map (fun (ids, ee) > ids, inject_eexpr ee) ann.annots} 

323 
) node.node_annot *) 

324 
} 

325 
in ((*Printers.pp_node Format.err_formatter node;*) node) 

349 
{ 

350 
node with 

351 
node_locals = new_locals; 

352 
node_stmts = 

353 
List.map (fun eq > Eq eq) (defs @ assert_defs) 

354 
(* Incomplete work: TODO. Do we have to inject MPFR code here? Does it 

355 
make sense for annotations? For me, only if we produce C code for 

356 
annotations. Otherwise the various verification backend should have 

357 
their own understanding, but would not necessarily require this 

358 
additional normalization. *) 

359 
(* node_spec = spec; node_annot = List.map (fun ann > {ann with annots 

360 
= List.map (fun (ids, ee) > ids, inject_eexpr ee) ann.annots} ) 

361 
node.node_annot *); 

362 
} 

363 
in 

364 
(*Printers.pp_node Format.err_formatter node;*) 

365 
node 

326  366  
327  367 
let inject_decl decl = 
328  368 
match decl.top_decl_desc with 
329  369 
 Node nd > 
330 
{decl with top_decl_desc = Node (inject_node nd)} 

331 
 Include _  Open _  ImportedNode _  Const _  TypeDef _ > decl 

332 


333 
let inject_prog decls = 

334 
List.map inject_decl decls 

370 
{ decl with top_decl_desc = Node (inject_node nd) } 

371 
 Include _  Open _  ImportedNode _  Const _  TypeDef _ > 

372 
decl 

335  373  
374 
let inject_prog decls = List.map inject_decl decls 

336  375  
337  376 
(* Local Variables: *) 
338  377 
(* compilecommand:"make C .." *) 
Also available in: Unified diff
reformatting