source: extracted/rTLabs_syntax.ml @ 2746

Last change on this file since 2746 was 2743, checked in by sacerdot, 7 years ago

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

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 Setoids
26
27open Monad
28
29open Option
30
31open Lists
32
33open Positive
34
35open Identifiers
36
37open Exp
38
39open Arithmetic
40
41open Vector
42
43open Div_and_mod
44
45open Jmeq
46
47open Russell
48
49open List
50
51open Util
52
53open FoldStuff
54
55open BitVector
56
57open Extranat
58
59open Bool
60
61open Relations
62
63open Nat
64
65open Integers
66
67open Types
68
69open AST
70
71open BitVectorTrie
72
73open CostLabel
74
75open FrontEndVal
76
77open Hide
78
79open ByteValues
80
81open GenMem
82
83open FrontEndMem
84
85open Division
86
87open Z
88
89open BitVectorZ
90
91open Pointers
92
93open Coqlib
94
95open Values
96
97open FrontEndOps
98
99open Order
100
101open Registers
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_14764 -> h_St_skip x_14764
142| St_cost (x_14766, x_14765) -> h_St_cost x_14766 x_14765
143| St_const (t, x_14769, x_14768, x_14767) ->
144  h_St_const t x_14769 x_14768 x_14767
145| St_op1 (t', t, x_14773, x_14772, x_14771, x_14770) ->
146  h_St_op1 t' t x_14773 x_14772 x_14771 x_14770
147| St_op2 (t', t1, t2, x_14778, x_14777, x_14776, x_14775, x_14774) ->
148  h_St_op2 t' t1 t2 x_14778 x_14777 x_14776 x_14775 x_14774
149| St_load (x_14782, x_14781, x_14780, x_14779) ->
150  h_St_load x_14782 x_14781 x_14780 x_14779
151| St_store (x_14786, x_14785, x_14784, x_14783) ->
152  h_St_store x_14786 x_14785 x_14784 x_14783
153| St_call_id (x_14790, x_14789, x_14788, x_14787) ->
154  h_St_call_id x_14790 x_14789 x_14788 x_14787
155| St_call_ptr (x_14794, x_14793, x_14792, x_14791) ->
156  h_St_call_ptr x_14794 x_14793 x_14792 x_14791
157| St_cond (x_14797, x_14796, x_14795) -> h_St_cond x_14797 x_14796 x_14795
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_14810 -> h_St_skip x_14810
177| St_cost (x_14812, x_14811) -> h_St_cost x_14812 x_14811
178| St_const (t, x_14815, x_14814, x_14813) ->
179  h_St_const t x_14815 x_14814 x_14813
180| St_op1 (t', t, x_14819, x_14818, x_14817, x_14816) ->
181  h_St_op1 t' t x_14819 x_14818 x_14817 x_14816
182| St_op2 (t', t1, t2, x_14824, x_14823, x_14822, x_14821, x_14820) ->
183  h_St_op2 t' t1 t2 x_14824 x_14823 x_14822 x_14821 x_14820
184| St_load (x_14828, x_14827, x_14826, x_14825) ->
185  h_St_load x_14828 x_14827 x_14826 x_14825
186| St_store (x_14832, x_14831, x_14830, x_14829) ->
187  h_St_store x_14832 x_14831 x_14830 x_14829
188| St_call_id (x_14836, x_14835, x_14834, x_14833) ->
189  h_St_call_id x_14836 x_14835 x_14834 x_14833
190| St_call_ptr (x_14840, x_14839, x_14838, x_14837) ->
191  h_St_call_ptr x_14840 x_14839 x_14838 x_14837
192| St_cond (x_14843, x_14842, x_14841) -> h_St_cond x_14843 x_14842 x_14841
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_14856 -> h_St_skip x_14856
212| St_cost (x_14858, x_14857) -> h_St_cost x_14858 x_14857
213| St_const (t, x_14861, x_14860, x_14859) ->
214  h_St_const t x_14861 x_14860 x_14859
215| St_op1 (t', t, x_14865, x_14864, x_14863, x_14862) ->
216  h_St_op1 t' t x_14865 x_14864 x_14863 x_14862
217| St_op2 (t', t1, t2, x_14870, x_14869, x_14868, x_14867, x_14866) ->
218  h_St_op2 t' t1 t2 x_14870 x_14869 x_14868 x_14867 x_14866
219| St_load (x_14874, x_14873, x_14872, x_14871) ->
220  h_St_load x_14874 x_14873 x_14872 x_14871
221| St_store (x_14878, x_14877, x_14876, x_14875) ->
222  h_St_store x_14878 x_14877 x_14876 x_14875
223| St_call_id (x_14882, x_14881, x_14880, x_14879) ->
224  h_St_call_id x_14882 x_14881 x_14880 x_14879
225| St_call_ptr (x_14886, x_14885, x_14884, x_14883) ->
226  h_St_call_ptr x_14886 x_14885 x_14884 x_14883
227| St_cond (x_14889, x_14888, x_14887) -> h_St_cond x_14889 x_14888 x_14887
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_14902 -> h_St_skip x_14902
247| St_cost (x_14904, x_14903) -> h_St_cost x_14904 x_14903
248| St_const (t, x_14907, x_14906, x_14905) ->
249  h_St_const t x_14907 x_14906 x_14905
250| St_op1 (t', t, x_14911, x_14910, x_14909, x_14908) ->
251  h_St_op1 t' t x_14911 x_14910 x_14909 x_14908
252| St_op2 (t', t1, t2, x_14916, x_14915, x_14914, x_14913, x_14912) ->
253  h_St_op2 t' t1 t2 x_14916 x_14915 x_14914 x_14913 x_14912
254| St_load (x_14920, x_14919, x_14918, x_14917) ->
255  h_St_load x_14920 x_14919 x_14918 x_14917
256| St_store (x_14924, x_14923, x_14922, x_14921) ->
257  h_St_store x_14924 x_14923 x_14922 x_14921
258| St_call_id (x_14928, x_14927, x_14926, x_14925) ->
259  h_St_call_id x_14928 x_14927 x_14926 x_14925
260| St_call_ptr (x_14932, x_14931, x_14930, x_14929) ->
261  h_St_call_ptr x_14932 x_14931 x_14930 x_14929
262| St_cond (x_14935, x_14934, x_14933) -> h_St_cond x_14935 x_14934 x_14933
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_14948 -> h_St_skip x_14948
282| St_cost (x_14950, x_14949) -> h_St_cost x_14950 x_14949
283| St_const (t, x_14953, x_14952, x_14951) ->
284  h_St_const t x_14953 x_14952 x_14951
285| St_op1 (t', t, x_14957, x_14956, x_14955, x_14954) ->
286  h_St_op1 t' t x_14957 x_14956 x_14955 x_14954
287| St_op2 (t', t1, t2, x_14962, x_14961, x_14960, x_14959, x_14958) ->
288  h_St_op2 t' t1 t2 x_14962 x_14961 x_14960 x_14959 x_14958
289| St_load (x_14966, x_14965, x_14964, x_14963) ->
290  h_St_load x_14966 x_14965 x_14964 x_14963
291| St_store (x_14970, x_14969, x_14968, x_14967) ->
292  h_St_store x_14970 x_14969 x_14968 x_14967
293| St_call_id (x_14974, x_14973, x_14972, x_14971) ->
294  h_St_call_id x_14974 x_14973 x_14972 x_14971
295| St_call_ptr (x_14978, x_14977, x_14976, x_14975) ->
296  h_St_call_ptr x_14978 x_14977 x_14976 x_14975
297| St_cond (x_14981, x_14980, x_14979) -> h_St_cond x_14981 x_14980 x_14979
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_14994 -> h_St_skip x_14994
317| St_cost (x_14996, x_14995) -> h_St_cost x_14996 x_14995
318| St_const (t, x_14999, x_14998, x_14997) ->
319  h_St_const t x_14999 x_14998 x_14997
320| St_op1 (t', t, x_15003, x_15002, x_15001, x_15000) ->
321  h_St_op1 t' t x_15003 x_15002 x_15001 x_15000
322| St_op2 (t', t1, t2, x_15008, x_15007, x_15006, x_15005, x_15004) ->
323  h_St_op2 t' t1 t2 x_15008 x_15007 x_15006 x_15005 x_15004
324| St_load (x_15012, x_15011, x_15010, x_15009) ->
325  h_St_load x_15012 x_15011 x_15010 x_15009
326| St_store (x_15016, x_15015, x_15014, x_15013) ->
327  h_St_store x_15016 x_15015 x_15014 x_15013
328| St_call_id (x_15020, x_15019, x_15018, x_15017) ->
329  h_St_call_id x_15020 x_15019 x_15018 x_15017
330| St_call_ptr (x_15024, x_15023, x_15022, x_15021) ->
331  h_St_call_ptr x_15024 x_15023 x_15022 x_15021
332| St_cond (x_15027, x_15026, x_15025) -> h_St_cond x_15027 x_15026 x_15025
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_15317 =
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_15317
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_15319 =
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_15319
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_15321 =
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_15321
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_15323 =
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_15323
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_15325 =
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_15325
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_15327 =
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_15327
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.