79 open Hints_declaration
98 | Id of AST.typ * AST.ident
99 | Cst of AST.typ * FrontEndOps.constant
100 | Op1 of AST.typ * AST.typ * FrontEndOps.unary_operation * expr
101 | Op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation *
103 | Mem of AST.typ * expr
104 | Cond of AST.intsize * AST.signedness * AST.typ * expr * expr * expr
105 | Ecost of AST.typ * CostLabel.costlabel * expr
107 (** val expr_rect_Type4 :
108 (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
109 -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
110 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
111 expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
112 (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
113 -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
114 -> 'a1) -> AST.typ -> expr -> 'a1 **)
115 let rec expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13742 = function
116 | Id (t, x_13744) -> h_Id t x_13744
117 | Cst (t, x_13745) -> h_Cst t x_13745
118 | Op1 (t, t', x_13747, x_13746) ->
119 h_Op1 t t' x_13747 x_13746
120 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13746)
121 | Op2 (t1, t2, t', x_13750, x_13749, x_13748) ->
122 h_Op2 t1 t2 t' x_13750 x_13749 x_13748
123 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13749)
124 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13748)
125 | Mem (t, x_13751) ->
127 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
129 | Cond (sz, sg, t, x_13754, x_13753, x_13752) ->
130 h_Cond sz sg t x_13754 x_13753 x_13752
131 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
133 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13753)
134 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13752)
135 | Ecost (t, x_13756, x_13755) ->
136 h_Ecost t x_13756 x_13755
137 (expr_rect_Type4 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13755)
139 (** val expr_rect_Type3 :
140 (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
141 -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
142 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
143 expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
144 (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
145 -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
146 -> 'a1) -> AST.typ -> expr -> 'a1 **)
147 let rec expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13786 = function
148 | Id (t, x_13788) -> h_Id t x_13788
149 | Cst (t, x_13789) -> h_Cst t x_13789
150 | Op1 (t, t', x_13791, x_13790) ->
151 h_Op1 t t' x_13791 x_13790
152 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13790)
153 | Op2 (t1, t2, t', x_13794, x_13793, x_13792) ->
154 h_Op2 t1 t2 t' x_13794 x_13793 x_13792
155 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13793)
156 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13792)
157 | Mem (t, x_13795) ->
159 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
161 | Cond (sz, sg, t, x_13798, x_13797, x_13796) ->
162 h_Cond sz sg t x_13798 x_13797 x_13796
163 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
165 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13797)
166 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13796)
167 | Ecost (t, x_13800, x_13799) ->
168 h_Ecost t x_13800 x_13799
169 (expr_rect_Type3 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13799)
171 (** val expr_rect_Type2 :
172 (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
173 -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
174 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
175 expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
176 (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
177 -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
178 -> 'a1) -> AST.typ -> expr -> 'a1 **)
179 let rec expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13808 = function
180 | Id (t, x_13810) -> h_Id t x_13810
181 | Cst (t, x_13811) -> h_Cst t x_13811
182 | Op1 (t, t', x_13813, x_13812) ->
183 h_Op1 t t' x_13813 x_13812
184 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13812)
185 | Op2 (t1, t2, t', x_13816, x_13815, x_13814) ->
186 h_Op2 t1 t2 t' x_13816 x_13815 x_13814
187 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13815)
188 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13814)
189 | Mem (t, x_13817) ->
191 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
193 | Cond (sz, sg, t, x_13820, x_13819, x_13818) ->
194 h_Cond sz sg t x_13820 x_13819 x_13818
195 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
197 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13819)
198 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13818)
199 | Ecost (t, x_13822, x_13821) ->
200 h_Ecost t x_13822 x_13821
201 (expr_rect_Type2 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13821)
203 (** val expr_rect_Type1 :
204 (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
205 -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
206 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
207 expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
208 (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
209 -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
210 -> 'a1) -> AST.typ -> expr -> 'a1 **)
211 let rec expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13830 = function
212 | Id (t, x_13832) -> h_Id t x_13832
213 | Cst (t, x_13833) -> h_Cst t x_13833
214 | Op1 (t, t', x_13835, x_13834) ->
215 h_Op1 t t' x_13835 x_13834
216 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13834)
217 | Op2 (t1, t2, t', x_13838, x_13837, x_13836) ->
218 h_Op2 t1 t2 t' x_13838 x_13837 x_13836
219 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13837)
220 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13836)
221 | Mem (t, x_13839) ->
223 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
225 | Cond (sz, sg, t, x_13842, x_13841, x_13840) ->
226 h_Cond sz sg t x_13842 x_13841 x_13840
227 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
229 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13841)
230 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13840)
231 | Ecost (t, x_13844, x_13843) ->
232 h_Ecost t x_13844 x_13843
233 (expr_rect_Type1 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13843)
235 (** val expr_rect_Type0 :
236 (AST.typ -> AST.ident -> 'a1) -> (AST.typ -> FrontEndOps.constant -> 'a1)
237 -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation -> expr -> 'a1 ->
238 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
239 expr -> expr -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> expr -> 'a1 -> 'a1) ->
240 (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> 'a1
241 -> 'a1 -> 'a1 -> 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> 'a1
242 -> 'a1) -> AST.typ -> expr -> 'a1 **)
243 let rec expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost x_13852 = function
244 | Id (t, x_13854) -> h_Id t x_13854
245 | Cst (t, x_13855) -> h_Cst t x_13855
246 | Op1 (t, t', x_13857, x_13856) ->
247 h_Op1 t t' x_13857 x_13856
248 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13856)
249 | Op2 (t1, t2, t', x_13860, x_13859, x_13858) ->
250 h_Op2 t1 t2 t' x_13860 x_13859 x_13858
251 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t1 x_13859)
252 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t2 x_13858)
253 | Mem (t, x_13861) ->
255 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost AST.ASTptr
257 | Cond (sz, sg, t, x_13864, x_13863, x_13862) ->
258 h_Cond sz sg t x_13864 x_13863 x_13862
259 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost (AST.ASTint
261 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13863)
262 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13862)
263 | Ecost (t, x_13866, x_13865) ->
264 h_Ecost t x_13866 x_13865
265 (expr_rect_Type0 h_Id h_Cst h_Op1 h_Op2 h_Mem h_Cond h_Ecost t x_13865)
267 (** val expr_inv_rect_Type4 :
268 AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
269 -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
270 FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
271 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
272 expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
273 'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
274 (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
275 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
276 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
277 __ -> __ -> 'a1) -> 'a1 **)
278 let expr_inv_rect_Type4 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
279 let hcut = expr_rect_Type4 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
281 (** val expr_inv_rect_Type3 :
282 AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
283 -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
284 FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
285 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
286 expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
287 'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
288 (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
289 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
290 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
291 __ -> __ -> 'a1) -> 'a1 **)
292 let expr_inv_rect_Type3 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
293 let hcut = expr_rect_Type3 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
295 (** val expr_inv_rect_Type2 :
296 AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
297 -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
298 FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
299 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
300 expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
301 'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
302 (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
303 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
304 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
305 __ -> __ -> 'a1) -> 'a1 **)
306 let expr_inv_rect_Type2 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
307 let hcut = expr_rect_Type2 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
309 (** val expr_inv_rect_Type1 :
310 AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
311 -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
312 FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
313 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
314 expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
315 'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
316 (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
317 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
318 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
319 __ -> __ -> 'a1) -> 'a1 **)
320 let expr_inv_rect_Type1 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
321 let hcut = expr_rect_Type1 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
323 (** val expr_inv_rect_Type0 :
324 AST.typ -> expr -> (AST.typ -> AST.ident -> __ -> __ -> 'a1) -> (AST.typ
325 -> FrontEndOps.constant -> __ -> __ -> 'a1) -> (AST.typ -> AST.typ ->
326 FrontEndOps.unary_operation -> expr -> (__ -> __ -> 'a1) -> __ -> __ ->
327 'a1) -> (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
328 expr -> expr -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
329 'a1) -> (AST.typ -> expr -> (__ -> __ -> 'a1) -> __ -> __ -> 'a1) ->
330 (AST.intsize -> AST.signedness -> AST.typ -> expr -> expr -> expr -> (__
331 -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> __ -> __ ->
332 'a1) -> (AST.typ -> CostLabel.costlabel -> expr -> (__ -> __ -> 'a1) ->
333 __ -> __ -> 'a1) -> 'a1 **)
334 let expr_inv_rect_Type0 x1 hterm h1 h2 h3 h4 h5 h6 h7 =
335 let hcut = expr_rect_Type0 h1 h2 h3 h4 h5 h6 h7 x1 hterm in hcut __ __
337 (** val expr_jmdiscr : AST.typ -> expr -> expr -> __ **)
338 let expr_jmdiscr a1 x y =
339 Logic.eq_rect_Type2 x
341 | Id (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
342 | Cst (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
343 | Op1 (a0, a10, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
344 | Op2 (a0, a10, a2, a3, a4, a5) ->
345 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
346 | Mem (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
347 | Cond (a0, a10, a2, a3, a4, a5) ->
348 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
349 | Ecost (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
353 | St_assign of AST.typ * AST.ident * expr
354 | St_store of AST.typ * expr * expr
355 | St_call of (AST.ident, AST.typ) Types.prod Types.option * expr
356 * (AST.typ, expr) Types.dPair List.list
357 | St_seq of stmt * stmt
358 | St_ifthenelse of AST.intsize * AST.signedness * expr * stmt * stmt
359 | St_return of (AST.typ, expr) Types.dPair Types.option
360 | St_label of PreIdentifiers.identifier * stmt
361 | St_goto of PreIdentifiers.identifier
362 | St_cost of CostLabel.costlabel * stmt
364 (** val stmt_rect_Type4 :
365 'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
366 -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
367 (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
368 'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
369 'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
370 -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
371 (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
372 -> 'a1) -> stmt -> 'a1 **)
373 let rec stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
374 | St_skip -> h_St_skip
375 | St_assign (t, x_14037, x_14036) -> h_St_assign t x_14037 x_14036
376 | St_store (t, x_14039, x_14038) -> h_St_store t x_14039 x_14038
377 | St_call (x_14042, x_14041, x_14040) -> h_St_call x_14042 x_14041 x_14040
378 | St_seq (x_14044, x_14043) ->
379 h_St_seq x_14044 x_14043
380 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
381 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14044)
382 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
383 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14043)
384 | St_ifthenelse (sz, sg, x_14047, x_14046, x_14045) ->
385 h_St_ifthenelse sz sg x_14047 x_14046 x_14045
386 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
387 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14046)
388 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
389 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14045)
390 | St_return x_14048 -> h_St_return x_14048
391 | St_label (x_14050, x_14049) ->
392 h_St_label x_14050 x_14049
393 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
394 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14049)
395 | St_goto x_14051 -> h_St_goto x_14051
396 | St_cost (x_14053, x_14052) ->
397 h_St_cost x_14053 x_14052
398 (stmt_rect_Type4 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
399 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14052)
401 (** val stmt_rect_Type3 :
402 'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
403 -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
404 (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
405 'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
406 'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
407 -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
408 (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
409 -> 'a1) -> stmt -> 'a1 **)
410 let rec stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
411 | St_skip -> h_St_skip
412 | St_assign (t, x_14095, x_14094) -> h_St_assign t x_14095 x_14094
413 | St_store (t, x_14097, x_14096) -> h_St_store t x_14097 x_14096
414 | St_call (x_14100, x_14099, x_14098) -> h_St_call x_14100 x_14099 x_14098
415 | St_seq (x_14102, x_14101) ->
416 h_St_seq x_14102 x_14101
417 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
418 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14102)
419 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
420 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14101)
421 | St_ifthenelse (sz, sg, x_14105, x_14104, x_14103) ->
422 h_St_ifthenelse sz sg x_14105 x_14104 x_14103
423 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
424 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14104)
425 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
426 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14103)
427 | St_return x_14106 -> h_St_return x_14106
428 | St_label (x_14108, x_14107) ->
429 h_St_label x_14108 x_14107
430 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
431 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14107)
432 | St_goto x_14109 -> h_St_goto x_14109
433 | St_cost (x_14111, x_14110) ->
434 h_St_cost x_14111 x_14110
435 (stmt_rect_Type3 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
436 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14110)
438 (** val stmt_rect_Type2 :
439 'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
440 -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
441 (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
442 'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
443 'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
444 -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
445 (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
446 -> 'a1) -> stmt -> 'a1 **)
447 let rec stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
448 | St_skip -> h_St_skip
449 | St_assign (t, x_14124, x_14123) -> h_St_assign t x_14124 x_14123
450 | St_store (t, x_14126, x_14125) -> h_St_store t x_14126 x_14125
451 | St_call (x_14129, x_14128, x_14127) -> h_St_call x_14129 x_14128 x_14127
452 | St_seq (x_14131, x_14130) ->
453 h_St_seq x_14131 x_14130
454 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
455 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14131)
456 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
457 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14130)
458 | St_ifthenelse (sz, sg, x_14134, x_14133, x_14132) ->
459 h_St_ifthenelse sz sg x_14134 x_14133 x_14132
460 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
461 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14133)
462 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
463 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14132)
464 | St_return x_14135 -> h_St_return x_14135
465 | St_label (x_14137, x_14136) ->
466 h_St_label x_14137 x_14136
467 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
468 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14136)
469 | St_goto x_14138 -> h_St_goto x_14138
470 | St_cost (x_14140, x_14139) ->
471 h_St_cost x_14140 x_14139
472 (stmt_rect_Type2 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
473 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14139)
475 (** val stmt_rect_Type1 :
476 'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
477 -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
478 (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
479 'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
480 'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
481 -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
482 (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
483 -> 'a1) -> stmt -> 'a1 **)
484 let rec stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
485 | St_skip -> h_St_skip
486 | St_assign (t, x_14153, x_14152) -> h_St_assign t x_14153 x_14152
487 | St_store (t, x_14155, x_14154) -> h_St_store t x_14155 x_14154
488 | St_call (x_14158, x_14157, x_14156) -> h_St_call x_14158 x_14157 x_14156
489 | St_seq (x_14160, x_14159) ->
490 h_St_seq x_14160 x_14159
491 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
492 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14160)
493 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
494 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14159)
495 | St_ifthenelse (sz, sg, x_14163, x_14162, x_14161) ->
496 h_St_ifthenelse sz sg x_14163 x_14162 x_14161
497 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
498 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14162)
499 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
500 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14161)
501 | St_return x_14164 -> h_St_return x_14164
502 | St_label (x_14166, x_14165) ->
503 h_St_label x_14166 x_14165
504 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
505 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14165)
506 | St_goto x_14167 -> h_St_goto x_14167
507 | St_cost (x_14169, x_14168) ->
508 h_St_cost x_14169 x_14168
509 (stmt_rect_Type1 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
510 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14168)
512 (** val stmt_rect_Type0 :
513 'a1 -> (AST.typ -> AST.ident -> expr -> 'a1) -> (AST.typ -> expr -> expr
514 -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option -> expr ->
515 (AST.typ, expr) Types.dPair List.list -> 'a1) -> (stmt -> stmt -> 'a1 ->
516 'a1 -> 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt ->
517 'a1 -> 'a1 -> 'a1) -> ((AST.typ, expr) Types.dPair Types.option -> 'a1)
518 -> (PreIdentifiers.identifier -> stmt -> 'a1 -> 'a1) ->
519 (PreIdentifiers.identifier -> 'a1) -> (CostLabel.costlabel -> stmt -> 'a1
520 -> 'a1) -> stmt -> 'a1 **)
521 let rec stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost = function
522 | St_skip -> h_St_skip
523 | St_assign (t, x_14182, x_14181) -> h_St_assign t x_14182 x_14181
524 | St_store (t, x_14184, x_14183) -> h_St_store t x_14184 x_14183
525 | St_call (x_14187, x_14186, x_14185) -> h_St_call x_14187 x_14186 x_14185
526 | St_seq (x_14189, x_14188) ->
527 h_St_seq x_14189 x_14188
528 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
529 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14189)
530 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
531 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14188)
532 | St_ifthenelse (sz, sg, x_14192, x_14191, x_14190) ->
533 h_St_ifthenelse sz sg x_14192 x_14191 x_14190
534 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
535 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14191)
536 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
537 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14190)
538 | St_return x_14193 -> h_St_return x_14193
539 | St_label (x_14195, x_14194) ->
540 h_St_label x_14195 x_14194
541 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
542 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14194)
543 | St_goto x_14196 -> h_St_goto x_14196
544 | St_cost (x_14198, x_14197) ->
545 h_St_cost x_14198 x_14197
546 (stmt_rect_Type0 h_St_skip h_St_assign h_St_store h_St_call h_St_seq
547 h_St_ifthenelse h_St_return h_St_label h_St_goto h_St_cost x_14197)
549 (** val stmt_inv_rect_Type4 :
550 stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
551 (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
552 Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
553 -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
554 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
555 'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
556 Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
557 -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
558 (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
559 let stmt_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
560 let hcut = stmt_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
562 (** val stmt_inv_rect_Type3 :
563 stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
564 (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
565 Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
566 -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
567 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
568 'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
569 Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
570 -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
571 (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
572 let stmt_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
573 let hcut = stmt_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
575 (** val stmt_inv_rect_Type2 :
576 stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
577 (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
578 Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
579 -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
580 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
581 'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
582 Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
583 -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
584 (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
585 let stmt_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
586 let hcut = stmt_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
588 (** val stmt_inv_rect_Type1 :
589 stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
590 (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
591 Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
592 -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
593 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
594 'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
595 Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
596 -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
597 (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
598 let stmt_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
599 let hcut = stmt_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
601 (** val stmt_inv_rect_Type0 :
602 stmt -> (__ -> 'a1) -> (AST.typ -> AST.ident -> expr -> __ -> 'a1) ->
603 (AST.typ -> expr -> expr -> __ -> 'a1) -> ((AST.ident, AST.typ)
604 Types.prod Types.option -> expr -> (AST.typ, expr) Types.dPair List.list
605 -> __ -> 'a1) -> (stmt -> stmt -> (__ -> 'a1) -> (__ -> 'a1) -> __ ->
606 'a1) -> (AST.intsize -> AST.signedness -> expr -> stmt -> stmt -> (__ ->
607 'a1) -> (__ -> 'a1) -> __ -> 'a1) -> ((AST.typ, expr) Types.dPair
608 Types.option -> __ -> 'a1) -> (PreIdentifiers.identifier -> stmt -> (__
609 -> 'a1) -> __ -> 'a1) -> (PreIdentifiers.identifier -> __ -> 'a1) ->
610 (CostLabel.costlabel -> stmt -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
611 let stmt_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 =
612 let hcut = stmt_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 hterm in hcut __
614 (** val stmt_discr : stmt -> stmt -> __ **)
616 Logic.eq_rect_Type2 x
618 | St_skip -> Obj.magic (fun _ dH -> dH)
619 | St_assign (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
620 | St_store (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
621 | St_call (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
622 | St_seq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
623 | St_ifthenelse (a0, a1, a2, a3, a4) ->
624 Obj.magic (fun _ dH -> dH __ __ __ __ __)
625 | St_return a0 -> Obj.magic (fun _ dH -> dH __)
626 | St_label (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
627 | St_goto a0 -> Obj.magic (fun _ dH -> dH __)
628 | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
630 (** val stmt_jmdiscr : stmt -> stmt -> __ **)
631 let stmt_jmdiscr x y =
632 Logic.eq_rect_Type2 x
634 | St_skip -> Obj.magic (fun _ dH -> dH)
635 | St_assign (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
636 | St_store (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
637 | St_call (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
638 | St_seq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
639 | St_ifthenelse (a0, a1, a2, a3, a4) ->
640 Obj.magic (fun _ dH -> dH __ __ __ __ __)
641 | St_return a0 -> Obj.magic (fun _ dH -> dH __)
642 | St_label (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
643 | St_goto a0 -> Obj.magic (fun _ dH -> dH __)
644 | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
646 (** val labels_of : stmt -> PreIdentifiers.identifier List.list **)
647 let rec labels_of = function
648 | St_skip -> List.Nil
649 | St_assign (x, x0, x1) -> List.Nil
650 | St_store (x, x0, x1) -> List.Nil
651 | St_call (x, x0, x1) -> List.Nil
652 | St_seq (s1, s2) -> List.append (labels_of s1) (labels_of s2)
653 | St_ifthenelse (x, x0, x1, s1, s2) ->
654 List.append (labels_of s1) (labels_of s2)
655 | St_return x -> List.Nil
656 | St_label (l, s0) -> List.Cons (l, (labels_of s0))
657 | St_goto x -> List.Nil
658 | St_cost (x, s0) -> labels_of s0
660 (** val cminor_stmt_inv_rect_Type4 :
661 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
662 List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
664 let rec cminor_stmt_inv_rect_Type4 env labels rettyp s h_mk_cminor_stmt_inv =
665 h_mk_cminor_stmt_inv __ __ __
667 (** val cminor_stmt_inv_rect_Type5 :
668 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
669 List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
671 let rec cminor_stmt_inv_rect_Type5 env labels rettyp s h_mk_cminor_stmt_inv =
672 h_mk_cminor_stmt_inv __ __ __
674 (** val cminor_stmt_inv_rect_Type3 :
675 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
676 List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
678 let rec cminor_stmt_inv_rect_Type3 env labels rettyp s h_mk_cminor_stmt_inv =
679 h_mk_cminor_stmt_inv __ __ __
681 (** val cminor_stmt_inv_rect_Type2 :
682 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
683 List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
685 let rec cminor_stmt_inv_rect_Type2 env labels rettyp s h_mk_cminor_stmt_inv =
686 h_mk_cminor_stmt_inv __ __ __
688 (** val cminor_stmt_inv_rect_Type1 :
689 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
690 List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
692 let rec cminor_stmt_inv_rect_Type1 env labels rettyp s h_mk_cminor_stmt_inv =
693 h_mk_cminor_stmt_inv __ __ __
695 (** val cminor_stmt_inv_rect_Type0 :
696 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
697 List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> 'a1) ->
699 let rec cminor_stmt_inv_rect_Type0 env labels rettyp s h_mk_cminor_stmt_inv =
700 h_mk_cminor_stmt_inv __ __ __
702 (** val cminor_stmt_inv_inv_rect_Type4 :
703 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
704 List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
706 let cminor_stmt_inv_inv_rect_Type4 x1 x2 x3 x4 h1 =
707 let hcut = cminor_stmt_inv_rect_Type4 x1 x2 x3 x4 h1 in hcut __
709 (** val cminor_stmt_inv_inv_rect_Type3 :
710 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
711 List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
713 let cminor_stmt_inv_inv_rect_Type3 x1 x2 x3 x4 h1 =
714 let hcut = cminor_stmt_inv_rect_Type3 x1 x2 x3 x4 h1 in hcut __
716 (** val cminor_stmt_inv_inv_rect_Type2 :
717 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
718 List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
720 let cminor_stmt_inv_inv_rect_Type2 x1 x2 x3 x4 h1 =
721 let hcut = cminor_stmt_inv_rect_Type2 x1 x2 x3 x4 h1 in hcut __
723 (** val cminor_stmt_inv_inv_rect_Type1 :
724 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
725 List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
727 let cminor_stmt_inv_inv_rect_Type1 x1 x2 x3 x4 h1 =
728 let hcut = cminor_stmt_inv_rect_Type1 x1 x2 x3 x4 h1 in hcut __
730 (** val cminor_stmt_inv_inv_rect_Type0 :
731 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
732 List.list -> AST.typ Types.option -> stmt -> (__ -> __ -> __ -> __ ->
734 let cminor_stmt_inv_inv_rect_Type0 x1 x2 x3 x4 h1 =
735 let hcut = cminor_stmt_inv_rect_Type0 x1 x2 x3 x4 h1 in hcut __
737 (** val cminor_stmt_inv_discr :
738 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
739 List.list -> AST.typ Types.option -> stmt -> __ **)
740 let cminor_stmt_inv_discr a1 a2 a3 a4 =
741 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
743 (** val cminor_stmt_inv_jmdiscr :
744 (AST.ident, AST.typ) Types.prod List.list -> PreIdentifiers.identifier
745 List.list -> AST.typ Types.option -> stmt -> __ **)
746 let cminor_stmt_inv_jmdiscr a1 a2 a3 a4 =
747 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
749 type internal_function = { f_return : AST.typ Types.option;
750 f_params : (AST.ident, AST.typ) Types.prod
752 f_vars : (AST.ident, AST.typ) Types.prod List.list;
753 f_stacksize : Nat.nat; f_body : stmt }
755 (** val internal_function_rect_Type4 :
756 (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
757 (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
758 -> 'a1) -> internal_function -> 'a1 **)
759 let rec internal_function_rect_Type4 h_mk_internal_function x_14493 =
760 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
761 f_stacksize = f_stacksize0; f_body = f_body0 } = x_14493
763 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
766 (** val internal_function_rect_Type5 :
767 (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
768 (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
769 -> 'a1) -> internal_function -> 'a1 **)
770 let rec internal_function_rect_Type5 h_mk_internal_function x_14495 =
771 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
772 f_stacksize = f_stacksize0; f_body = f_body0 } = x_14495
774 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
777 (** val internal_function_rect_Type3 :
778 (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
779 (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
780 -> 'a1) -> internal_function -> 'a1 **)
781 let rec internal_function_rect_Type3 h_mk_internal_function x_14497 =
782 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
783 f_stacksize = f_stacksize0; f_body = f_body0 } = x_14497
785 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
788 (** val internal_function_rect_Type2 :
789 (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
790 (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
791 -> 'a1) -> internal_function -> 'a1 **)
792 let rec internal_function_rect_Type2 h_mk_internal_function x_14499 =
793 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
794 f_stacksize = f_stacksize0; f_body = f_body0 } = x_14499
796 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
799 (** val internal_function_rect_Type1 :
800 (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
801 (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
802 -> 'a1) -> internal_function -> 'a1 **)
803 let rec internal_function_rect_Type1 h_mk_internal_function x_14501 =
804 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
805 f_stacksize = f_stacksize0; f_body = f_body0 } = x_14501
807 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
810 (** val internal_function_rect_Type0 :
811 (AST.typ Types.option -> (AST.ident, AST.typ) Types.prod List.list ->
812 (AST.ident, AST.typ) Types.prod List.list -> __ -> Nat.nat -> stmt -> __
813 -> 'a1) -> internal_function -> 'a1 **)
814 let rec internal_function_rect_Type0 h_mk_internal_function x_14503 =
815 let { f_return = f_return0; f_params = f_params0; f_vars = f_vars0;
816 f_stacksize = f_stacksize0; f_body = f_body0 } = x_14503
818 h_mk_internal_function f_return0 f_params0 f_vars0 __ f_stacksize0 f_body0
821 (** val f_return : internal_function -> AST.typ Types.option **)
822 let rec f_return xxx =
826 internal_function -> (AST.ident, AST.typ) Types.prod List.list **)
827 let rec f_params xxx =
831 internal_function -> (AST.ident, AST.typ) Types.prod List.list **)
835 (** val f_stacksize : internal_function -> Nat.nat **)
836 let rec f_stacksize xxx =
839 (** val f_body : internal_function -> stmt **)
843 (** val internal_function_inv_rect_Type4 :
844 internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
845 Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
846 -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
847 let internal_function_inv_rect_Type4 hterm h1 =
848 let hcut = internal_function_rect_Type4 h1 hterm in hcut __
850 (** val internal_function_inv_rect_Type3 :
851 internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
852 Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
853 -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
854 let internal_function_inv_rect_Type3 hterm h1 =
855 let hcut = internal_function_rect_Type3 h1 hterm in hcut __
857 (** val internal_function_inv_rect_Type2 :
858 internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
859 Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
860 -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
861 let internal_function_inv_rect_Type2 hterm h1 =
862 let hcut = internal_function_rect_Type2 h1 hterm in hcut __
864 (** val internal_function_inv_rect_Type1 :
865 internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
866 Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
867 -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
868 let internal_function_inv_rect_Type1 hterm h1 =
869 let hcut = internal_function_rect_Type1 h1 hterm in hcut __
871 (** val internal_function_inv_rect_Type0 :
872 internal_function -> (AST.typ Types.option -> (AST.ident, AST.typ)
873 Types.prod List.list -> (AST.ident, AST.typ) Types.prod List.list -> __
874 -> Nat.nat -> stmt -> __ -> __ -> 'a1) -> 'a1 **)
875 let internal_function_inv_rect_Type0 hterm h1 =
876 let hcut = internal_function_rect_Type0 h1 hterm in hcut __
878 (** val internal_function_jmdiscr :
879 internal_function -> internal_function -> __ **)
880 let internal_function_jmdiscr x y =
881 Logic.eq_rect_Type2 x
882 (let { f_return = a0; f_params = a1; f_vars = a2; f_stacksize = a4;
885 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
887 type cminor_program =
888 (internal_function AST.fundef, AST.init_data List.list) AST.program
890 type cminor_noinit_program =
891 (internal_function AST.fundef, Nat.nat) AST.program