source: extracted/rTLabs_syntax.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 30.2 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Proper
12
13open PositiveMap
14
15open Deqsets
16
17open ErrorMessages
18
19open PreIdentifiers
20
21open Errors
22
23open Extralib
24
25open Lists
26
27open Positive
28
29open Identifiers
30
31open Exp
32
33open Arithmetic
34
35open Vector
36
37open Div_and_mod
38
39open Util
40
41open FoldStuff
42
43open BitVector
44
45open Jmeq
46
47open Russell
48
49open List
50
51open Setoids
52
53open Monad
54
55open Option
56
57open Extranat
58
59open Bool
60
61open Relations
62
63open Nat
64
65open Integers
66
67open Types
68
69open AST
70
71open CostLabel
72
73open FrontEndVal
74
75open Hide
76
77open ByteValues
78
79open GenMem
80
81open FrontEndMem
82
83open Division
84
85open Z
86
87open BitVectorZ
88
89open Pointers
90
91open Coqlib
92
93open Values
94
95open FrontEndOps
96
97open Order
98
99open Registers
100
101open BitVectorTrie
102
103open Graphs
104
105type statement =
106| St_skip of Graphs.label
107| St_cost of CostLabel.costlabel * Graphs.label
108| St_const of AST.typ * Registers.register * FrontEndOps.constant
109   * Graphs.label
110| St_op1 of AST.typ * AST.typ * FrontEndOps.unary_operation
111   * Registers.register * Registers.register * Graphs.label
112| St_op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation
113   * Registers.register * Registers.register * Registers.register
114   * Graphs.label
115| St_load of AST.typ * Registers.register * Registers.register * Graphs.label
116| St_store of AST.typ * Registers.register * Registers.register
117   * Graphs.label
118| St_call_id of AST.ident * Registers.register List.list
119   * Registers.register Types.option * Graphs.label
120| St_call_ptr of Registers.register * Registers.register List.list
121   * Registers.register Types.option * Graphs.label
122| St_cond of Registers.register * Graphs.label * Graphs.label
123| St_return
124
125(** val statement_rect_Type4 :
126    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
127    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
128    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
129    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
130    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
131    Registers.register -> Registers.register -> Registers.register ->
132    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
133    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
134    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
135    (AST.ident -> Registers.register List.list -> Registers.register
136    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
137    Registers.register List.list -> Registers.register Types.option ->
138    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
139    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
140let rec statement_rect_Type4 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
141| St_skip x_9946 -> h_St_skip x_9946
142| St_cost (x_9948, x_9947) -> h_St_cost x_9948 x_9947
143| St_const (t, x_9951, x_9950, x_9949) -> h_St_const t x_9951 x_9950 x_9949
144| St_op1 (t', t, x_9955, x_9954, x_9953, x_9952) ->
145  h_St_op1 t' t x_9955 x_9954 x_9953 x_9952
146| St_op2 (t', t1, t2, x_9960, x_9959, x_9958, x_9957, x_9956) ->
147  h_St_op2 t' t1 t2 x_9960 x_9959 x_9958 x_9957 x_9956
148| St_load (x_9964, x_9963, x_9962, x_9961) ->
149  h_St_load x_9964 x_9963 x_9962 x_9961
150| St_store (x_9968, x_9967, x_9966, x_9965) ->
151  h_St_store x_9968 x_9967 x_9966 x_9965
152| St_call_id (x_9972, x_9971, x_9970, x_9969) ->
153  h_St_call_id x_9972 x_9971 x_9970 x_9969
154| St_call_ptr (x_9976, x_9975, x_9974, x_9973) ->
155  h_St_call_ptr x_9976 x_9975 x_9974 x_9973
156| St_cond (x_9979, x_9978, x_9977) -> h_St_cond x_9979 x_9978 x_9977
157| St_return -> h_St_return
158
159(** val statement_rect_Type5 :
160    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
161    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
162    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
163    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
164    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
165    Registers.register -> Registers.register -> Registers.register ->
166    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
167    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
168    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
169    (AST.ident -> Registers.register List.list -> Registers.register
170    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
171    Registers.register List.list -> Registers.register Types.option ->
172    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
173    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
174let rec statement_rect_Type5 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
175| St_skip x_9992 -> h_St_skip x_9992
176| St_cost (x_9994, x_9993) -> h_St_cost x_9994 x_9993
177| St_const (t, x_9997, x_9996, x_9995) -> h_St_const t x_9997 x_9996 x_9995
178| St_op1 (t', t, x_10001, x_10000, x_9999, x_9998) ->
179  h_St_op1 t' t x_10001 x_10000 x_9999 x_9998
180| St_op2 (t', t1, t2, x_10006, x_10005, x_10004, x_10003, x_10002) ->
181  h_St_op2 t' t1 t2 x_10006 x_10005 x_10004 x_10003 x_10002
182| St_load (x_10010, x_10009, x_10008, x_10007) ->
183  h_St_load x_10010 x_10009 x_10008 x_10007
184| St_store (x_10014, x_10013, x_10012, x_10011) ->
185  h_St_store x_10014 x_10013 x_10012 x_10011
186| St_call_id (x_10018, x_10017, x_10016, x_10015) ->
187  h_St_call_id x_10018 x_10017 x_10016 x_10015
188| St_call_ptr (x_10022, x_10021, x_10020, x_10019) ->
189  h_St_call_ptr x_10022 x_10021 x_10020 x_10019
190| St_cond (x_10025, x_10024, x_10023) -> h_St_cond x_10025 x_10024 x_10023
191| St_return -> h_St_return
192
193(** val statement_rect_Type3 :
194    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
195    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
196    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
197    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
198    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
199    Registers.register -> Registers.register -> Registers.register ->
200    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
201    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
202    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
203    (AST.ident -> Registers.register List.list -> Registers.register
204    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
205    Registers.register List.list -> Registers.register Types.option ->
206    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
207    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
208let rec statement_rect_Type3 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
209| St_skip x_10038 -> h_St_skip x_10038
210| St_cost (x_10040, x_10039) -> h_St_cost x_10040 x_10039
211| St_const (t, x_10043, x_10042, x_10041) ->
212  h_St_const t x_10043 x_10042 x_10041
213| St_op1 (t', t, x_10047, x_10046, x_10045, x_10044) ->
214  h_St_op1 t' t x_10047 x_10046 x_10045 x_10044
215| St_op2 (t', t1, t2, x_10052, x_10051, x_10050, x_10049, x_10048) ->
216  h_St_op2 t' t1 t2 x_10052 x_10051 x_10050 x_10049 x_10048
217| St_load (x_10056, x_10055, x_10054, x_10053) ->
218  h_St_load x_10056 x_10055 x_10054 x_10053
219| St_store (x_10060, x_10059, x_10058, x_10057) ->
220  h_St_store x_10060 x_10059 x_10058 x_10057
221| St_call_id (x_10064, x_10063, x_10062, x_10061) ->
222  h_St_call_id x_10064 x_10063 x_10062 x_10061
223| St_call_ptr (x_10068, x_10067, x_10066, x_10065) ->
224  h_St_call_ptr x_10068 x_10067 x_10066 x_10065
225| St_cond (x_10071, x_10070, x_10069) -> h_St_cond x_10071 x_10070 x_10069
226| St_return -> h_St_return
227
228(** val statement_rect_Type2 :
229    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
230    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
231    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
232    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
233    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
234    Registers.register -> Registers.register -> Registers.register ->
235    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
236    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
237    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
238    (AST.ident -> Registers.register List.list -> Registers.register
239    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
240    Registers.register List.list -> Registers.register Types.option ->
241    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
242    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
243let rec statement_rect_Type2 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
244| St_skip x_10084 -> h_St_skip x_10084
245| St_cost (x_10086, x_10085) -> h_St_cost x_10086 x_10085
246| St_const (t, x_10089, x_10088, x_10087) ->
247  h_St_const t x_10089 x_10088 x_10087
248| St_op1 (t', t, x_10093, x_10092, x_10091, x_10090) ->
249  h_St_op1 t' t x_10093 x_10092 x_10091 x_10090
250| St_op2 (t', t1, t2, x_10098, x_10097, x_10096, x_10095, x_10094) ->
251  h_St_op2 t' t1 t2 x_10098 x_10097 x_10096 x_10095 x_10094
252| St_load (x_10102, x_10101, x_10100, x_10099) ->
253  h_St_load x_10102 x_10101 x_10100 x_10099
254| St_store (x_10106, x_10105, x_10104, x_10103) ->
255  h_St_store x_10106 x_10105 x_10104 x_10103
256| St_call_id (x_10110, x_10109, x_10108, x_10107) ->
257  h_St_call_id x_10110 x_10109 x_10108 x_10107
258| St_call_ptr (x_10114, x_10113, x_10112, x_10111) ->
259  h_St_call_ptr x_10114 x_10113 x_10112 x_10111
260| St_cond (x_10117, x_10116, x_10115) -> h_St_cond x_10117 x_10116 x_10115
261| St_return -> h_St_return
262
263(** val statement_rect_Type1 :
264    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
265    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
266    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
267    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
268    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
269    Registers.register -> Registers.register -> Registers.register ->
270    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
271    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
272    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
273    (AST.ident -> Registers.register List.list -> Registers.register
274    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
275    Registers.register List.list -> Registers.register Types.option ->
276    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
277    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
278let rec statement_rect_Type1 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
279| St_skip x_10130 -> h_St_skip x_10130
280| St_cost (x_10132, x_10131) -> h_St_cost x_10132 x_10131
281| St_const (t, x_10135, x_10134, x_10133) ->
282  h_St_const t x_10135 x_10134 x_10133
283| St_op1 (t', t, x_10139, x_10138, x_10137, x_10136) ->
284  h_St_op1 t' t x_10139 x_10138 x_10137 x_10136
285| St_op2 (t', t1, t2, x_10144, x_10143, x_10142, x_10141, x_10140) ->
286  h_St_op2 t' t1 t2 x_10144 x_10143 x_10142 x_10141 x_10140
287| St_load (x_10148, x_10147, x_10146, x_10145) ->
288  h_St_load x_10148 x_10147 x_10146 x_10145
289| St_store (x_10152, x_10151, x_10150, x_10149) ->
290  h_St_store x_10152 x_10151 x_10150 x_10149
291| St_call_id (x_10156, x_10155, x_10154, x_10153) ->
292  h_St_call_id x_10156 x_10155 x_10154 x_10153
293| St_call_ptr (x_10160, x_10159, x_10158, x_10157) ->
294  h_St_call_ptr x_10160 x_10159 x_10158 x_10157
295| St_cond (x_10163, x_10162, x_10161) -> h_St_cond x_10163 x_10162 x_10161
296| St_return -> h_St_return
297
298(** val statement_rect_Type0 :
299    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
300    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
301    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
302    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
303    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
304    Registers.register -> Registers.register -> Registers.register ->
305    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
306    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
307    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
308    (AST.ident -> Registers.register List.list -> Registers.register
309    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
310    Registers.register List.list -> Registers.register Types.option ->
311    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
312    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
313let rec statement_rect_Type0 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
314| St_skip x_10176 -> h_St_skip x_10176
315| St_cost (x_10178, x_10177) -> h_St_cost x_10178 x_10177
316| St_const (t, x_10181, x_10180, x_10179) ->
317  h_St_const t x_10181 x_10180 x_10179
318| St_op1 (t', t, x_10185, x_10184, x_10183, x_10182) ->
319  h_St_op1 t' t x_10185 x_10184 x_10183 x_10182
320| St_op2 (t', t1, t2, x_10190, x_10189, x_10188, x_10187, x_10186) ->
321  h_St_op2 t' t1 t2 x_10190 x_10189 x_10188 x_10187 x_10186
322| St_load (x_10194, x_10193, x_10192, x_10191) ->
323  h_St_load x_10194 x_10193 x_10192 x_10191
324| St_store (x_10198, x_10197, x_10196, x_10195) ->
325  h_St_store x_10198 x_10197 x_10196 x_10195
326| St_call_id (x_10202, x_10201, x_10200, x_10199) ->
327  h_St_call_id x_10202 x_10201 x_10200 x_10199
328| St_call_ptr (x_10206, x_10205, x_10204, x_10203) ->
329  h_St_call_ptr x_10206 x_10205 x_10204 x_10203
330| St_cond (x_10209, x_10208, x_10207) -> h_St_cond x_10209 x_10208 x_10207
331| St_return -> h_St_return
332
333(** val statement_inv_rect_Type4 :
334    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
335    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
336    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
337    -> FrontEndOps.unary_operation -> Registers.register ->
338    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
339    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
340    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
341    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
342    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
343    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
344    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
345    (Registers.register -> Registers.register List.list -> Registers.register
346    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
347    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
348let statement_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
349  let hcut = statement_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
350  hcut __
351
352(** val statement_inv_rect_Type3 :
353    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
354    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
355    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
356    -> FrontEndOps.unary_operation -> Registers.register ->
357    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
358    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
359    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
360    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
361    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
362    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
363    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
364    (Registers.register -> Registers.register List.list -> Registers.register
365    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
366    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
367let statement_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
368  let hcut = statement_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
369  hcut __
370
371(** val statement_inv_rect_Type2 :
372    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
373    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
374    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
375    -> FrontEndOps.unary_operation -> Registers.register ->
376    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
377    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
378    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
379    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
380    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
381    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
382    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
383    (Registers.register -> Registers.register List.list -> Registers.register
384    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
385    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
386let statement_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
387  let hcut = statement_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
388  hcut __
389
390(** val statement_inv_rect_Type1 :
391    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
392    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
393    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
394    -> FrontEndOps.unary_operation -> Registers.register ->
395    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
396    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
397    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
398    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
399    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
400    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
401    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
402    (Registers.register -> Registers.register List.list -> Registers.register
403    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
404    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
405let statement_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
406  let hcut = statement_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
407  hcut __
408
409(** val statement_inv_rect_Type0 :
410    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
411    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
412    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
413    -> FrontEndOps.unary_operation -> Registers.register ->
414    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
415    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
416    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
417    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
418    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
419    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
420    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
421    (Registers.register -> Registers.register List.list -> Registers.register
422    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
423    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
424let statement_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
425  let hcut = statement_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
426  hcut __
427
428(** val statement_jmdiscr : statement -> statement -> __ **)
429let statement_jmdiscr x y =
430  Logic.eq_rect_Type2 x
431    (match x with
432     | St_skip a0 -> Obj.magic (fun _ dH -> dH __)
433     | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
434     | St_const (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
435     | St_op1 (a0, a1, a2, a3, a4, a5) ->
436       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
437     | St_op2 (a0, a1, a2, a3, a4, a5, a6, a7) ->
438       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
439     | St_load (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
440     | St_store (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
441     | St_call_id (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
442     | St_call_ptr (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
443     | St_cond (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
444     | St_return -> Obj.magic (fun _ dH -> dH)) y
445
446type internal_function = { f_labgen : Identifiers.universe;
447                           f_reggen : Identifiers.universe;
448                           f_result : (Registers.register, AST.typ)
449                                      Types.prod Types.option;
450                           f_params : (Registers.register, AST.typ)
451                                      Types.prod List.list;
452                           f_locals : (Registers.register, AST.typ)
453                                      Types.prod List.list;
454                           f_stacksize : Nat.nat;
455                           f_graph : statement Graphs.graph;
456                           f_entry : Graphs.label Types.sig0;
457                           f_exit : Graphs.label Types.sig0 }
458
459(** val internal_function_rect_Type4 :
460    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
461    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
462    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
463    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
464    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
465    internal_function -> 'a1 **)
466let rec internal_function_rect_Type4 h_mk_internal_function x_10499 =
467  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
468    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
469    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_10499
470  in
471  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
472    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
473
474(** val internal_function_rect_Type5 :
475    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
476    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
477    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
478    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
479    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
480    internal_function -> 'a1 **)
481let rec internal_function_rect_Type5 h_mk_internal_function x_10501 =
482  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
483    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
484    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_10501
485  in
486  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
487    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
488
489(** val internal_function_rect_Type3 :
490    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
491    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
492    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
493    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
494    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
495    internal_function -> 'a1 **)
496let rec internal_function_rect_Type3 h_mk_internal_function x_10503 =
497  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
498    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
499    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_10503
500  in
501  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
502    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
503
504(** val internal_function_rect_Type2 :
505    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
506    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
507    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
508    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
509    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
510    internal_function -> 'a1 **)
511let rec internal_function_rect_Type2 h_mk_internal_function x_10505 =
512  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
513    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
514    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_10505
515  in
516  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
517    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
518
519(** val internal_function_rect_Type1 :
520    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
521    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
522    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
523    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
524    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
525    internal_function -> 'a1 **)
526let rec internal_function_rect_Type1 h_mk_internal_function x_10507 =
527  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
528    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
529    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_10507
530  in
531  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
532    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
533
534(** val internal_function_rect_Type0 :
535    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
536    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
537    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
538    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
539    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
540    internal_function -> 'a1 **)
541let rec internal_function_rect_Type0 h_mk_internal_function x_10509 =
542  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
543    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
544    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_10509
545  in
546  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
547    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
548
549(** val f_labgen : internal_function -> Identifiers.universe **)
550let rec f_labgen xxx =
551  xxx.f_labgen
552
553(** val f_reggen : internal_function -> Identifiers.universe **)
554let rec f_reggen xxx =
555  xxx.f_reggen
556
557(** val f_result :
558    internal_function -> (Registers.register, AST.typ) Types.prod
559    Types.option **)
560let rec f_result xxx =
561  xxx.f_result
562
563(** val f_params :
564    internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
565let rec f_params xxx =
566  xxx.f_params
567
568(** val f_locals :
569    internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
570let rec f_locals xxx =
571  xxx.f_locals
572
573(** val f_stacksize : internal_function -> Nat.nat **)
574let rec f_stacksize xxx =
575  xxx.f_stacksize
576
577(** val f_graph : internal_function -> statement Graphs.graph **)
578let rec f_graph xxx =
579  xxx.f_graph
580
581(** val f_entry : internal_function -> Graphs.label Types.sig0 **)
582let rec f_entry xxx =
583  xxx.f_entry
584
585(** val f_exit : internal_function -> Graphs.label Types.sig0 **)
586let rec f_exit xxx =
587  xxx.f_exit
588
589(** val internal_function_inv_rect_Type4 :
590    internal_function -> (Identifiers.universe -> Identifiers.universe ->
591    (Registers.register, AST.typ) Types.prod Types.option ->
592    (Registers.register, AST.typ) Types.prod List.list ->
593    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
594    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
595    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
596let internal_function_inv_rect_Type4 hterm h1 =
597  let hcut = internal_function_rect_Type4 h1 hterm in hcut __
598
599(** val internal_function_inv_rect_Type3 :
600    internal_function -> (Identifiers.universe -> Identifiers.universe ->
601    (Registers.register, AST.typ) Types.prod Types.option ->
602    (Registers.register, AST.typ) Types.prod List.list ->
603    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
604    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
605    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
606let internal_function_inv_rect_Type3 hterm h1 =
607  let hcut = internal_function_rect_Type3 h1 hterm in hcut __
608
609(** val internal_function_inv_rect_Type2 :
610    internal_function -> (Identifiers.universe -> Identifiers.universe ->
611    (Registers.register, AST.typ) Types.prod Types.option ->
612    (Registers.register, AST.typ) Types.prod List.list ->
613    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
614    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
615    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
616let internal_function_inv_rect_Type2 hterm h1 =
617  let hcut = internal_function_rect_Type2 h1 hterm in hcut __
618
619(** val internal_function_inv_rect_Type1 :
620    internal_function -> (Identifiers.universe -> Identifiers.universe ->
621    (Registers.register, AST.typ) Types.prod Types.option ->
622    (Registers.register, AST.typ) Types.prod List.list ->
623    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
624    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
625    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
626let internal_function_inv_rect_Type1 hterm h1 =
627  let hcut = internal_function_rect_Type1 h1 hterm in hcut __
628
629(** val internal_function_inv_rect_Type0 :
630    internal_function -> (Identifiers.universe -> Identifiers.universe ->
631    (Registers.register, AST.typ) Types.prod Types.option ->
632    (Registers.register, AST.typ) Types.prod List.list ->
633    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
634    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
635    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
636let internal_function_inv_rect_Type0 hterm h1 =
637  let hcut = internal_function_rect_Type0 h1 hterm in hcut __
638
639(** val internal_function_jmdiscr :
640    internal_function -> internal_function -> __ **)
641let internal_function_jmdiscr x y =
642  Logic.eq_rect_Type2 x
643    (let { f_labgen = a0; f_reggen = a1; f_result = a2; f_params = a3;
644       f_locals = a4; f_stacksize = a5; f_graph = a6; f_entry = a9; f_exit =
645       a10 } = x
646     in
647    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y
648
649type rTLabs_program = (internal_function AST.fundef, Nat.nat) AST.program
650
Note: See TracBrowser for help on using the repository browser.