source: driver/extracted/rTLabs_syntax.ml @ 3106

Last change on this file since 3106 was 3059, checked in by sacerdot, 7 years ago

New extraction

File size: 30.4 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_14903 -> h_St_skip x_14903
142| St_cost (x_14905, x_14904) -> h_St_cost x_14905 x_14904
143| St_const (t, x_14908, x_14907, x_14906) ->
144  h_St_const t x_14908 x_14907 x_14906
145| St_op1 (t', t, x_14912, x_14911, x_14910, x_14909) ->
146  h_St_op1 t' t x_14912 x_14911 x_14910 x_14909
147| St_op2 (t', t1, t2, x_14917, x_14916, x_14915, x_14914, x_14913) ->
148  h_St_op2 t' t1 t2 x_14917 x_14916 x_14915 x_14914 x_14913
149| St_load (x_14921, x_14920, x_14919, x_14918) ->
150  h_St_load x_14921 x_14920 x_14919 x_14918
151| St_store (x_14925, x_14924, x_14923, x_14922) ->
152  h_St_store x_14925 x_14924 x_14923 x_14922
153| St_call_id (x_14929, x_14928, x_14927, x_14926) ->
154  h_St_call_id x_14929 x_14928 x_14927 x_14926
155| St_call_ptr (x_14933, x_14932, x_14931, x_14930) ->
156  h_St_call_ptr x_14933 x_14932 x_14931 x_14930
157| St_cond (x_14936, x_14935, x_14934) -> h_St_cond x_14936 x_14935 x_14934
158| St_return -> h_St_return
159
160(** val statement_rect_Type5 :
161    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
162    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
163    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
164    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
165    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
166    Registers.register -> Registers.register -> Registers.register ->
167    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
168    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
169    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
170    (AST.ident -> Registers.register List.list -> Registers.register
171    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
172    Registers.register List.list -> Registers.register Types.option ->
173    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
174    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
175let 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
176| St_skip x_14949 -> h_St_skip x_14949
177| St_cost (x_14951, x_14950) -> h_St_cost x_14951 x_14950
178| St_const (t, x_14954, x_14953, x_14952) ->
179  h_St_const t x_14954 x_14953 x_14952
180| St_op1 (t', t, x_14958, x_14957, x_14956, x_14955) ->
181  h_St_op1 t' t x_14958 x_14957 x_14956 x_14955
182| St_op2 (t', t1, t2, x_14963, x_14962, x_14961, x_14960, x_14959) ->
183  h_St_op2 t' t1 t2 x_14963 x_14962 x_14961 x_14960 x_14959
184| St_load (x_14967, x_14966, x_14965, x_14964) ->
185  h_St_load x_14967 x_14966 x_14965 x_14964
186| St_store (x_14971, x_14970, x_14969, x_14968) ->
187  h_St_store x_14971 x_14970 x_14969 x_14968
188| St_call_id (x_14975, x_14974, x_14973, x_14972) ->
189  h_St_call_id x_14975 x_14974 x_14973 x_14972
190| St_call_ptr (x_14979, x_14978, x_14977, x_14976) ->
191  h_St_call_ptr x_14979 x_14978 x_14977 x_14976
192| St_cond (x_14982, x_14981, x_14980) -> h_St_cond x_14982 x_14981 x_14980
193| St_return -> h_St_return
194
195(** val statement_rect_Type3 :
196    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
197    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
198    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
199    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
200    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
201    Registers.register -> Registers.register -> Registers.register ->
202    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
203    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
204    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
205    (AST.ident -> Registers.register List.list -> Registers.register
206    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
207    Registers.register List.list -> Registers.register Types.option ->
208    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
209    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
210let 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
211| St_skip x_14995 -> h_St_skip x_14995
212| St_cost (x_14997, x_14996) -> h_St_cost x_14997 x_14996
213| St_const (t, x_15000, x_14999, x_14998) ->
214  h_St_const t x_15000 x_14999 x_14998
215| St_op1 (t', t, x_15004, x_15003, x_15002, x_15001) ->
216  h_St_op1 t' t x_15004 x_15003 x_15002 x_15001
217| St_op2 (t', t1, t2, x_15009, x_15008, x_15007, x_15006, x_15005) ->
218  h_St_op2 t' t1 t2 x_15009 x_15008 x_15007 x_15006 x_15005
219| St_load (x_15013, x_15012, x_15011, x_15010) ->
220  h_St_load x_15013 x_15012 x_15011 x_15010
221| St_store (x_15017, x_15016, x_15015, x_15014) ->
222  h_St_store x_15017 x_15016 x_15015 x_15014
223| St_call_id (x_15021, x_15020, x_15019, x_15018) ->
224  h_St_call_id x_15021 x_15020 x_15019 x_15018
225| St_call_ptr (x_15025, x_15024, x_15023, x_15022) ->
226  h_St_call_ptr x_15025 x_15024 x_15023 x_15022
227| St_cond (x_15028, x_15027, x_15026) -> h_St_cond x_15028 x_15027 x_15026
228| St_return -> h_St_return
229
230(** val statement_rect_Type2 :
231    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
232    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
233    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
234    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
235    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
236    Registers.register -> Registers.register -> Registers.register ->
237    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
238    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
239    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
240    (AST.ident -> Registers.register List.list -> Registers.register
241    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
242    Registers.register List.list -> Registers.register Types.option ->
243    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
244    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
245let 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
246| St_skip x_15041 -> h_St_skip x_15041
247| St_cost (x_15043, x_15042) -> h_St_cost x_15043 x_15042
248| St_const (t, x_15046, x_15045, x_15044) ->
249  h_St_const t x_15046 x_15045 x_15044
250| St_op1 (t', t, x_15050, x_15049, x_15048, x_15047) ->
251  h_St_op1 t' t x_15050 x_15049 x_15048 x_15047
252| St_op2 (t', t1, t2, x_15055, x_15054, x_15053, x_15052, x_15051) ->
253  h_St_op2 t' t1 t2 x_15055 x_15054 x_15053 x_15052 x_15051
254| St_load (x_15059, x_15058, x_15057, x_15056) ->
255  h_St_load x_15059 x_15058 x_15057 x_15056
256| St_store (x_15063, x_15062, x_15061, x_15060) ->
257  h_St_store x_15063 x_15062 x_15061 x_15060
258| St_call_id (x_15067, x_15066, x_15065, x_15064) ->
259  h_St_call_id x_15067 x_15066 x_15065 x_15064
260| St_call_ptr (x_15071, x_15070, x_15069, x_15068) ->
261  h_St_call_ptr x_15071 x_15070 x_15069 x_15068
262| St_cond (x_15074, x_15073, x_15072) -> h_St_cond x_15074 x_15073 x_15072
263| St_return -> h_St_return
264
265(** val statement_rect_Type1 :
266    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
267    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
268    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
269    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
270    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
271    Registers.register -> Registers.register -> Registers.register ->
272    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
273    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
274    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
275    (AST.ident -> Registers.register List.list -> Registers.register
276    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
277    Registers.register List.list -> Registers.register Types.option ->
278    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
279    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
280let 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
281| St_skip x_15087 -> h_St_skip x_15087
282| St_cost (x_15089, x_15088) -> h_St_cost x_15089 x_15088
283| St_const (t, x_15092, x_15091, x_15090) ->
284  h_St_const t x_15092 x_15091 x_15090
285| St_op1 (t', t, x_15096, x_15095, x_15094, x_15093) ->
286  h_St_op1 t' t x_15096 x_15095 x_15094 x_15093
287| St_op2 (t', t1, t2, x_15101, x_15100, x_15099, x_15098, x_15097) ->
288  h_St_op2 t' t1 t2 x_15101 x_15100 x_15099 x_15098 x_15097
289| St_load (x_15105, x_15104, x_15103, x_15102) ->
290  h_St_load x_15105 x_15104 x_15103 x_15102
291| St_store (x_15109, x_15108, x_15107, x_15106) ->
292  h_St_store x_15109 x_15108 x_15107 x_15106
293| St_call_id (x_15113, x_15112, x_15111, x_15110) ->
294  h_St_call_id x_15113 x_15112 x_15111 x_15110
295| St_call_ptr (x_15117, x_15116, x_15115, x_15114) ->
296  h_St_call_ptr x_15117 x_15116 x_15115 x_15114
297| St_cond (x_15120, x_15119, x_15118) -> h_St_cond x_15120 x_15119 x_15118
298| St_return -> h_St_return
299
300(** val statement_rect_Type0 :
301    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
302    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
303    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
304    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
305    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
306    Registers.register -> Registers.register -> Registers.register ->
307    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
308    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
309    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
310    (AST.ident -> Registers.register List.list -> Registers.register
311    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
312    Registers.register List.list -> Registers.register Types.option ->
313    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
314    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
315let 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
316| St_skip x_15133 -> h_St_skip x_15133
317| St_cost (x_15135, x_15134) -> h_St_cost x_15135 x_15134
318| St_const (t, x_15138, x_15137, x_15136) ->
319  h_St_const t x_15138 x_15137 x_15136
320| St_op1 (t', t, x_15142, x_15141, x_15140, x_15139) ->
321  h_St_op1 t' t x_15142 x_15141 x_15140 x_15139
322| St_op2 (t', t1, t2, x_15147, x_15146, x_15145, x_15144, x_15143) ->
323  h_St_op2 t' t1 t2 x_15147 x_15146 x_15145 x_15144 x_15143
324| St_load (x_15151, x_15150, x_15149, x_15148) ->
325  h_St_load x_15151 x_15150 x_15149 x_15148
326| St_store (x_15155, x_15154, x_15153, x_15152) ->
327  h_St_store x_15155 x_15154 x_15153 x_15152
328| St_call_id (x_15159, x_15158, x_15157, x_15156) ->
329  h_St_call_id x_15159 x_15158 x_15157 x_15156
330| St_call_ptr (x_15163, x_15162, x_15161, x_15160) ->
331  h_St_call_ptr x_15163 x_15162 x_15161 x_15160
332| St_cond (x_15166, x_15165, x_15164) -> h_St_cond x_15166 x_15165 x_15164
333| St_return -> h_St_return
334
335(** val statement_inv_rect_Type4 :
336    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
337    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
338    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
339    -> FrontEndOps.unary_operation -> Registers.register ->
340    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
341    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
342    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
343    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
344    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
345    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
346    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
347    (Registers.register -> Registers.register List.list -> Registers.register
348    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
349    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
350let statement_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
351  let hcut = statement_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
352  hcut __
353
354(** val statement_inv_rect_Type3 :
355    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
356    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
357    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
358    -> FrontEndOps.unary_operation -> Registers.register ->
359    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
360    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
361    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
362    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
363    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
364    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
365    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
366    (Registers.register -> Registers.register List.list -> Registers.register
367    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
368    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
369let statement_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
370  let hcut = statement_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
371  hcut __
372
373(** val statement_inv_rect_Type2 :
374    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
375    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
376    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
377    -> FrontEndOps.unary_operation -> Registers.register ->
378    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
379    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
380    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
381    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
382    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
383    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
384    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
385    (Registers.register -> Registers.register List.list -> Registers.register
386    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
387    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
388let statement_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
389  let hcut = statement_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
390  hcut __
391
392(** val statement_inv_rect_Type1 :
393    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
394    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
395    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
396    -> FrontEndOps.unary_operation -> Registers.register ->
397    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
398    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
399    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
400    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
401    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
402    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
403    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
404    (Registers.register -> Registers.register List.list -> Registers.register
405    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
406    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
407let statement_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
408  let hcut = statement_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
409  hcut __
410
411(** val statement_inv_rect_Type0 :
412    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
413    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
414    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
415    -> FrontEndOps.unary_operation -> Registers.register ->
416    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
417    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
418    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
419    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
420    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
421    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
422    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
423    (Registers.register -> Registers.register List.list -> Registers.register
424    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
425    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
426let statement_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
427  let hcut = statement_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
428  hcut __
429
430(** val statement_jmdiscr : statement -> statement -> __ **)
431let statement_jmdiscr x y =
432  Logic.eq_rect_Type2 x
433    (match x with
434     | St_skip a0 -> Obj.magic (fun _ dH -> dH __)
435     | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
436     | St_const (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
437     | St_op1 (a0, a1, a2, a3, a4, a5) ->
438       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
439     | St_op2 (a0, a1, a2, a3, a4, a5, a6, a7) ->
440       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
441     | St_load (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
442     | St_store (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
443     | St_call_id (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
444     | St_call_ptr (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
445     | St_cond (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
446     | St_return -> Obj.magic (fun _ dH -> dH)) y
447
448type internal_function = { f_labgen : Identifiers.universe;
449                           f_reggen : Identifiers.universe;
450                           f_result : (Registers.register, AST.typ)
451                                      Types.prod Types.option;
452                           f_params : (Registers.register, AST.typ)
453                                      Types.prod List.list;
454                           f_locals : (Registers.register, AST.typ)
455                                      Types.prod List.list;
456                           f_stacksize : Nat.nat;
457                           f_graph : statement Graphs.graph;
458                           f_entry : Graphs.label Types.sig0;
459                           f_exit : Graphs.label Types.sig0 }
460
461(** val internal_function_rect_Type4 :
462    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
463    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
464    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
465    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
466    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
467    internal_function -> 'a1 **)
468let rec internal_function_rect_Type4 h_mk_internal_function x_15456 =
469  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
470    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
471    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15456
472  in
473  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
474    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
475
476(** val internal_function_rect_Type5 :
477    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
478    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
479    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
480    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
481    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
482    internal_function -> 'a1 **)
483let rec internal_function_rect_Type5 h_mk_internal_function x_15458 =
484  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
485    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
486    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15458
487  in
488  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
489    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
490
491(** val internal_function_rect_Type3 :
492    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
493    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
494    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
495    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
496    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
497    internal_function -> 'a1 **)
498let rec internal_function_rect_Type3 h_mk_internal_function x_15460 =
499  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
500    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
501    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15460
502  in
503  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
504    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
505
506(** val internal_function_rect_Type2 :
507    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
508    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
509    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
510    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
511    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
512    internal_function -> 'a1 **)
513let rec internal_function_rect_Type2 h_mk_internal_function x_15462 =
514  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
515    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
516    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15462
517  in
518  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
519    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
520
521(** val internal_function_rect_Type1 :
522    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
523    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
524    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
525    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
526    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
527    internal_function -> 'a1 **)
528let rec internal_function_rect_Type1 h_mk_internal_function x_15464 =
529  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
530    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
531    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15464
532  in
533  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
534    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
535
536(** val internal_function_rect_Type0 :
537    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
538    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
539    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
540    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
541    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
542    internal_function -> 'a1 **)
543let rec internal_function_rect_Type0 h_mk_internal_function x_15466 =
544  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
545    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
546    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15466
547  in
548  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
549    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
550
551(** val f_labgen : internal_function -> Identifiers.universe **)
552let rec f_labgen xxx =
553  xxx.f_labgen
554
555(** val f_reggen : internal_function -> Identifiers.universe **)
556let rec f_reggen xxx =
557  xxx.f_reggen
558
559(** val f_result :
560    internal_function -> (Registers.register, AST.typ) Types.prod
561    Types.option **)
562let rec f_result xxx =
563  xxx.f_result
564
565(** val f_params :
566    internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
567let rec f_params xxx =
568  xxx.f_params
569
570(** val f_locals :
571    internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
572let rec f_locals xxx =
573  xxx.f_locals
574
575(** val f_stacksize : internal_function -> Nat.nat **)
576let rec f_stacksize xxx =
577  xxx.f_stacksize
578
579(** val f_graph : internal_function -> statement Graphs.graph **)
580let rec f_graph xxx =
581  xxx.f_graph
582
583(** val f_entry : internal_function -> Graphs.label Types.sig0 **)
584let rec f_entry xxx =
585  xxx.f_entry
586
587(** val f_exit : internal_function -> Graphs.label Types.sig0 **)
588let rec f_exit xxx =
589  xxx.f_exit
590
591(** val internal_function_inv_rect_Type4 :
592    internal_function -> (Identifiers.universe -> Identifiers.universe ->
593    (Registers.register, AST.typ) Types.prod Types.option ->
594    (Registers.register, AST.typ) Types.prod List.list ->
595    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
596    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
597    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
598let internal_function_inv_rect_Type4 hterm h1 =
599  let hcut = internal_function_rect_Type4 h1 hterm in hcut __
600
601(** val internal_function_inv_rect_Type3 :
602    internal_function -> (Identifiers.universe -> Identifiers.universe ->
603    (Registers.register, AST.typ) Types.prod Types.option ->
604    (Registers.register, AST.typ) Types.prod List.list ->
605    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
606    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
607    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
608let internal_function_inv_rect_Type3 hterm h1 =
609  let hcut = internal_function_rect_Type3 h1 hterm in hcut __
610
611(** val internal_function_inv_rect_Type2 :
612    internal_function -> (Identifiers.universe -> Identifiers.universe ->
613    (Registers.register, AST.typ) Types.prod Types.option ->
614    (Registers.register, AST.typ) Types.prod List.list ->
615    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
616    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
617    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
618let internal_function_inv_rect_Type2 hterm h1 =
619  let hcut = internal_function_rect_Type2 h1 hterm in hcut __
620
621(** val internal_function_inv_rect_Type1 :
622    internal_function -> (Identifiers.universe -> Identifiers.universe ->
623    (Registers.register, AST.typ) Types.prod Types.option ->
624    (Registers.register, AST.typ) Types.prod List.list ->
625    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
626    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
627    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
628let internal_function_inv_rect_Type1 hterm h1 =
629  let hcut = internal_function_rect_Type1 h1 hterm in hcut __
630
631(** val internal_function_inv_rect_Type0 :
632    internal_function -> (Identifiers.universe -> Identifiers.universe ->
633    (Registers.register, AST.typ) Types.prod Types.option ->
634    (Registers.register, AST.typ) Types.prod List.list ->
635    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
636    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
637    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
638let internal_function_inv_rect_Type0 hterm h1 =
639  let hcut = internal_function_rect_Type0 h1 hterm in hcut __
640
641(** val internal_function_jmdiscr :
642    internal_function -> internal_function -> __ **)
643let internal_function_jmdiscr x y =
644  Logic.eq_rect_Type2 x
645    (let { f_labgen = a0; f_reggen = a1; f_result = a2; f_params = a3;
646       f_locals = a4; f_stacksize = a5; f_graph = a6; f_entry = a9; f_exit =
647       a10 } = x
648     in
649    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __)) y
650
651type rTLabs_program =
652  (internal_function AST.fundef, AST.init_data List.list) AST.program
653
Note: See TracBrowser for help on using the repository browser.