source: extracted/rTLabs_syntax.ml @ 2817

Last change on this file since 2817 was 2797, checked in by sacerdot, 7 years ago

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File size: 30.3 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_14790 -> h_St_skip x_14790
142| St_cost (x_14792, x_14791) -> h_St_cost x_14792 x_14791
143| St_const (t, x_14795, x_14794, x_14793) ->
144  h_St_const t x_14795 x_14794 x_14793
145| St_op1 (t', t, x_14799, x_14798, x_14797, x_14796) ->
146  h_St_op1 t' t x_14799 x_14798 x_14797 x_14796
147| St_op2 (t', t1, t2, x_14804, x_14803, x_14802, x_14801, x_14800) ->
148  h_St_op2 t' t1 t2 x_14804 x_14803 x_14802 x_14801 x_14800
149| St_load (x_14808, x_14807, x_14806, x_14805) ->
150  h_St_load x_14808 x_14807 x_14806 x_14805
151| St_store (x_14812, x_14811, x_14810, x_14809) ->
152  h_St_store x_14812 x_14811 x_14810 x_14809
153| St_call_id (x_14816, x_14815, x_14814, x_14813) ->
154  h_St_call_id x_14816 x_14815 x_14814 x_14813
155| St_call_ptr (x_14820, x_14819, x_14818, x_14817) ->
156  h_St_call_ptr x_14820 x_14819 x_14818 x_14817
157| St_cond (x_14823, x_14822, x_14821) -> h_St_cond x_14823 x_14822 x_14821
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_14836 -> h_St_skip x_14836
177| St_cost (x_14838, x_14837) -> h_St_cost x_14838 x_14837
178| St_const (t, x_14841, x_14840, x_14839) ->
179  h_St_const t x_14841 x_14840 x_14839
180| St_op1 (t', t, x_14845, x_14844, x_14843, x_14842) ->
181  h_St_op1 t' t x_14845 x_14844 x_14843 x_14842
182| St_op2 (t', t1, t2, x_14850, x_14849, x_14848, x_14847, x_14846) ->
183  h_St_op2 t' t1 t2 x_14850 x_14849 x_14848 x_14847 x_14846
184| St_load (x_14854, x_14853, x_14852, x_14851) ->
185  h_St_load x_14854 x_14853 x_14852 x_14851
186| St_store (x_14858, x_14857, x_14856, x_14855) ->
187  h_St_store x_14858 x_14857 x_14856 x_14855
188| St_call_id (x_14862, x_14861, x_14860, x_14859) ->
189  h_St_call_id x_14862 x_14861 x_14860 x_14859
190| St_call_ptr (x_14866, x_14865, x_14864, x_14863) ->
191  h_St_call_ptr x_14866 x_14865 x_14864 x_14863
192| St_cond (x_14869, x_14868, x_14867) -> h_St_cond x_14869 x_14868 x_14867
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_14882 -> h_St_skip x_14882
212| St_cost (x_14884, x_14883) -> h_St_cost x_14884 x_14883
213| St_const (t, x_14887, x_14886, x_14885) ->
214  h_St_const t x_14887 x_14886 x_14885
215| St_op1 (t', t, x_14891, x_14890, x_14889, x_14888) ->
216  h_St_op1 t' t x_14891 x_14890 x_14889 x_14888
217| St_op2 (t', t1, t2, x_14896, x_14895, x_14894, x_14893, x_14892) ->
218  h_St_op2 t' t1 t2 x_14896 x_14895 x_14894 x_14893 x_14892
219| St_load (x_14900, x_14899, x_14898, x_14897) ->
220  h_St_load x_14900 x_14899 x_14898 x_14897
221| St_store (x_14904, x_14903, x_14902, x_14901) ->
222  h_St_store x_14904 x_14903 x_14902 x_14901
223| St_call_id (x_14908, x_14907, x_14906, x_14905) ->
224  h_St_call_id x_14908 x_14907 x_14906 x_14905
225| St_call_ptr (x_14912, x_14911, x_14910, x_14909) ->
226  h_St_call_ptr x_14912 x_14911 x_14910 x_14909
227| St_cond (x_14915, x_14914, x_14913) -> h_St_cond x_14915 x_14914 x_14913
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_14928 -> h_St_skip x_14928
247| St_cost (x_14930, x_14929) -> h_St_cost x_14930 x_14929
248| St_const (t, x_14933, x_14932, x_14931) ->
249  h_St_const t x_14933 x_14932 x_14931
250| St_op1 (t', t, x_14937, x_14936, x_14935, x_14934) ->
251  h_St_op1 t' t x_14937 x_14936 x_14935 x_14934
252| St_op2 (t', t1, t2, x_14942, x_14941, x_14940, x_14939, x_14938) ->
253  h_St_op2 t' t1 t2 x_14942 x_14941 x_14940 x_14939 x_14938
254| St_load (x_14946, x_14945, x_14944, x_14943) ->
255  h_St_load x_14946 x_14945 x_14944 x_14943
256| St_store (x_14950, x_14949, x_14948, x_14947) ->
257  h_St_store x_14950 x_14949 x_14948 x_14947
258| St_call_id (x_14954, x_14953, x_14952, x_14951) ->
259  h_St_call_id x_14954 x_14953 x_14952 x_14951
260| St_call_ptr (x_14958, x_14957, x_14956, x_14955) ->
261  h_St_call_ptr x_14958 x_14957 x_14956 x_14955
262| St_cond (x_14961, x_14960, x_14959) -> h_St_cond x_14961 x_14960 x_14959
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_14974 -> h_St_skip x_14974
282| St_cost (x_14976, x_14975) -> h_St_cost x_14976 x_14975
283| St_const (t, x_14979, x_14978, x_14977) ->
284  h_St_const t x_14979 x_14978 x_14977
285| St_op1 (t', t, x_14983, x_14982, x_14981, x_14980) ->
286  h_St_op1 t' t x_14983 x_14982 x_14981 x_14980
287| St_op2 (t', t1, t2, x_14988, x_14987, x_14986, x_14985, x_14984) ->
288  h_St_op2 t' t1 t2 x_14988 x_14987 x_14986 x_14985 x_14984
289| St_load (x_14992, x_14991, x_14990, x_14989) ->
290  h_St_load x_14992 x_14991 x_14990 x_14989
291| St_store (x_14996, x_14995, x_14994, x_14993) ->
292  h_St_store x_14996 x_14995 x_14994 x_14993
293| St_call_id (x_15000, x_14999, x_14998, x_14997) ->
294  h_St_call_id x_15000 x_14999 x_14998 x_14997
295| St_call_ptr (x_15004, x_15003, x_15002, x_15001) ->
296  h_St_call_ptr x_15004 x_15003 x_15002 x_15001
297| St_cond (x_15007, x_15006, x_15005) -> h_St_cond x_15007 x_15006 x_15005
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_15020 -> h_St_skip x_15020
317| St_cost (x_15022, x_15021) -> h_St_cost x_15022 x_15021
318| St_const (t, x_15025, x_15024, x_15023) ->
319  h_St_const t x_15025 x_15024 x_15023
320| St_op1 (t', t, x_15029, x_15028, x_15027, x_15026) ->
321  h_St_op1 t' t x_15029 x_15028 x_15027 x_15026
322| St_op2 (t', t1, t2, x_15034, x_15033, x_15032, x_15031, x_15030) ->
323  h_St_op2 t' t1 t2 x_15034 x_15033 x_15032 x_15031 x_15030
324| St_load (x_15038, x_15037, x_15036, x_15035) ->
325  h_St_load x_15038 x_15037 x_15036 x_15035
326| St_store (x_15042, x_15041, x_15040, x_15039) ->
327  h_St_store x_15042 x_15041 x_15040 x_15039
328| St_call_id (x_15046, x_15045, x_15044, x_15043) ->
329  h_St_call_id x_15046 x_15045 x_15044 x_15043
330| St_call_ptr (x_15050, x_15049, x_15048, x_15047) ->
331  h_St_call_ptr x_15050 x_15049 x_15048 x_15047
332| St_cond (x_15053, x_15052, x_15051) -> h_St_cond x_15053 x_15052 x_15051
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_15343 =
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_15343
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_15345 =
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_15345
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_15347 =
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_15347
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_15349 =
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_15349
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_15351 =
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_15351
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_15353 =
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_15353
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 = (internal_function AST.fundef, Nat.nat) AST.program
652
Note: See TracBrowser for help on using the repository browser.