source: extracted/rTLabs_syntax.ml @ 2730

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

Exported again.

File size: 29.9 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_1809 -> h_St_skip x_1809
142| St_cost (x_1811, x_1810) -> h_St_cost x_1811 x_1810
143| St_const (t, x_1814, x_1813, x_1812) -> h_St_const t x_1814 x_1813 x_1812
144| St_op1 (t', t, x_1818, x_1817, x_1816, x_1815) ->
145  h_St_op1 t' t x_1818 x_1817 x_1816 x_1815
146| St_op2 (t', t1, t2, x_1823, x_1822, x_1821, x_1820, x_1819) ->
147  h_St_op2 t' t1 t2 x_1823 x_1822 x_1821 x_1820 x_1819
148| St_load (x_1827, x_1826, x_1825, x_1824) ->
149  h_St_load x_1827 x_1826 x_1825 x_1824
150| St_store (x_1831, x_1830, x_1829, x_1828) ->
151  h_St_store x_1831 x_1830 x_1829 x_1828
152| St_call_id (x_1835, x_1834, x_1833, x_1832) ->
153  h_St_call_id x_1835 x_1834 x_1833 x_1832
154| St_call_ptr (x_1839, x_1838, x_1837, x_1836) ->
155  h_St_call_ptr x_1839 x_1838 x_1837 x_1836
156| St_cond (x_1842, x_1841, x_1840) -> h_St_cond x_1842 x_1841 x_1840
157| St_return -> h_St_return
158
159(** val statement_rect_Type5 :
160    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
161    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
162    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
163    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
164    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
165    Registers.register -> Registers.register -> Registers.register ->
166    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
167    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
168    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
169    (AST.ident -> Registers.register List.list -> Registers.register
170    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
171    Registers.register List.list -> Registers.register Types.option ->
172    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
173    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
174let rec statement_rect_Type5 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
175| St_skip x_1855 -> h_St_skip x_1855
176| St_cost (x_1857, x_1856) -> h_St_cost x_1857 x_1856
177| St_const (t, x_1860, x_1859, x_1858) -> h_St_const t x_1860 x_1859 x_1858
178| St_op1 (t', t, x_1864, x_1863, x_1862, x_1861) ->
179  h_St_op1 t' t x_1864 x_1863 x_1862 x_1861
180| St_op2 (t', t1, t2, x_1869, x_1868, x_1867, x_1866, x_1865) ->
181  h_St_op2 t' t1 t2 x_1869 x_1868 x_1867 x_1866 x_1865
182| St_load (x_1873, x_1872, x_1871, x_1870) ->
183  h_St_load x_1873 x_1872 x_1871 x_1870
184| St_store (x_1877, x_1876, x_1875, x_1874) ->
185  h_St_store x_1877 x_1876 x_1875 x_1874
186| St_call_id (x_1881, x_1880, x_1879, x_1878) ->
187  h_St_call_id x_1881 x_1880 x_1879 x_1878
188| St_call_ptr (x_1885, x_1884, x_1883, x_1882) ->
189  h_St_call_ptr x_1885 x_1884 x_1883 x_1882
190| St_cond (x_1888, x_1887, x_1886) -> h_St_cond x_1888 x_1887 x_1886
191| St_return -> h_St_return
192
193(** val statement_rect_Type3 :
194    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
195    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
196    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
197    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
198    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
199    Registers.register -> Registers.register -> Registers.register ->
200    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
201    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
202    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
203    (AST.ident -> Registers.register List.list -> Registers.register
204    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
205    Registers.register List.list -> Registers.register Types.option ->
206    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
207    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
208let rec statement_rect_Type3 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
209| St_skip x_1901 -> h_St_skip x_1901
210| St_cost (x_1903, x_1902) -> h_St_cost x_1903 x_1902
211| St_const (t, x_1906, x_1905, x_1904) -> h_St_const t x_1906 x_1905 x_1904
212| St_op1 (t', t, x_1910, x_1909, x_1908, x_1907) ->
213  h_St_op1 t' t x_1910 x_1909 x_1908 x_1907
214| St_op2 (t', t1, t2, x_1915, x_1914, x_1913, x_1912, x_1911) ->
215  h_St_op2 t' t1 t2 x_1915 x_1914 x_1913 x_1912 x_1911
216| St_load (x_1919, x_1918, x_1917, x_1916) ->
217  h_St_load x_1919 x_1918 x_1917 x_1916
218| St_store (x_1923, x_1922, x_1921, x_1920) ->
219  h_St_store x_1923 x_1922 x_1921 x_1920
220| St_call_id (x_1927, x_1926, x_1925, x_1924) ->
221  h_St_call_id x_1927 x_1926 x_1925 x_1924
222| St_call_ptr (x_1931, x_1930, x_1929, x_1928) ->
223  h_St_call_ptr x_1931 x_1930 x_1929 x_1928
224| St_cond (x_1934, x_1933, x_1932) -> h_St_cond x_1934 x_1933 x_1932
225| St_return -> h_St_return
226
227(** val statement_rect_Type2 :
228    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
229    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
230    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
231    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
232    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
233    Registers.register -> Registers.register -> Registers.register ->
234    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
235    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
236    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
237    (AST.ident -> Registers.register List.list -> Registers.register
238    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
239    Registers.register List.list -> Registers.register Types.option ->
240    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
241    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
242let 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
243| St_skip x_1947 -> h_St_skip x_1947
244| St_cost (x_1949, x_1948) -> h_St_cost x_1949 x_1948
245| St_const (t, x_1952, x_1951, x_1950) -> h_St_const t x_1952 x_1951 x_1950
246| St_op1 (t', t, x_1956, x_1955, x_1954, x_1953) ->
247  h_St_op1 t' t x_1956 x_1955 x_1954 x_1953
248| St_op2 (t', t1, t2, x_1961, x_1960, x_1959, x_1958, x_1957) ->
249  h_St_op2 t' t1 t2 x_1961 x_1960 x_1959 x_1958 x_1957
250| St_load (x_1965, x_1964, x_1963, x_1962) ->
251  h_St_load x_1965 x_1964 x_1963 x_1962
252| St_store (x_1969, x_1968, x_1967, x_1966) ->
253  h_St_store x_1969 x_1968 x_1967 x_1966
254| St_call_id (x_1973, x_1972, x_1971, x_1970) ->
255  h_St_call_id x_1973 x_1972 x_1971 x_1970
256| St_call_ptr (x_1977, x_1976, x_1975, x_1974) ->
257  h_St_call_ptr x_1977 x_1976 x_1975 x_1974
258| St_cond (x_1980, x_1979, x_1978) -> h_St_cond x_1980 x_1979 x_1978
259| St_return -> h_St_return
260
261(** val statement_rect_Type1 :
262    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
263    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
264    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
265    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
266    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
267    Registers.register -> Registers.register -> Registers.register ->
268    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
269    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
270    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
271    (AST.ident -> Registers.register List.list -> Registers.register
272    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
273    Registers.register List.list -> Registers.register Types.option ->
274    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
275    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
276let 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
277| St_skip x_1993 -> h_St_skip x_1993
278| St_cost (x_1995, x_1994) -> h_St_cost x_1995 x_1994
279| St_const (t, x_1998, x_1997, x_1996) -> h_St_const t x_1998 x_1997 x_1996
280| St_op1 (t', t, x_2002, x_2001, x_2000, x_1999) ->
281  h_St_op1 t' t x_2002 x_2001 x_2000 x_1999
282| St_op2 (t', t1, t2, x_2007, x_2006, x_2005, x_2004, x_2003) ->
283  h_St_op2 t' t1 t2 x_2007 x_2006 x_2005 x_2004 x_2003
284| St_load (x_2011, x_2010, x_2009, x_2008) ->
285  h_St_load x_2011 x_2010 x_2009 x_2008
286| St_store (x_2015, x_2014, x_2013, x_2012) ->
287  h_St_store x_2015 x_2014 x_2013 x_2012
288| St_call_id (x_2019, x_2018, x_2017, x_2016) ->
289  h_St_call_id x_2019 x_2018 x_2017 x_2016
290| St_call_ptr (x_2023, x_2022, x_2021, x_2020) ->
291  h_St_call_ptr x_2023 x_2022 x_2021 x_2020
292| St_cond (x_2026, x_2025, x_2024) -> h_St_cond x_2026 x_2025 x_2024
293| St_return -> h_St_return
294
295(** val statement_rect_Type0 :
296    (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
297    (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
298    'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
299    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
300    (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
301    Registers.register -> Registers.register -> Registers.register ->
302    Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
303    Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
304    Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
305    (AST.ident -> Registers.register List.list -> Registers.register
306    Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
307    Registers.register List.list -> Registers.register Types.option ->
308    Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
309    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
310let 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
311| St_skip x_2039 -> h_St_skip x_2039
312| St_cost (x_2041, x_2040) -> h_St_cost x_2041 x_2040
313| St_const (t, x_2044, x_2043, x_2042) -> h_St_const t x_2044 x_2043 x_2042
314| St_op1 (t', t, x_2048, x_2047, x_2046, x_2045) ->
315  h_St_op1 t' t x_2048 x_2047 x_2046 x_2045
316| St_op2 (t', t1, t2, x_2053, x_2052, x_2051, x_2050, x_2049) ->
317  h_St_op2 t' t1 t2 x_2053 x_2052 x_2051 x_2050 x_2049
318| St_load (x_2057, x_2056, x_2055, x_2054) ->
319  h_St_load x_2057 x_2056 x_2055 x_2054
320| St_store (x_2061, x_2060, x_2059, x_2058) ->
321  h_St_store x_2061 x_2060 x_2059 x_2058
322| St_call_id (x_2065, x_2064, x_2063, x_2062) ->
323  h_St_call_id x_2065 x_2064 x_2063 x_2062
324| St_call_ptr (x_2069, x_2068, x_2067, x_2066) ->
325  h_St_call_ptr x_2069 x_2068 x_2067 x_2066
326| St_cond (x_2072, x_2071, x_2070) -> h_St_cond x_2072 x_2071 x_2070
327| St_return -> h_St_return
328
329(** val statement_inv_rect_Type4 :
330    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
331    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
332    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
333    -> FrontEndOps.unary_operation -> Registers.register ->
334    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
335    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
336    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
337    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
338    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
339    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
340    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
341    (Registers.register -> Registers.register List.list -> Registers.register
342    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
343    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
344let statement_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
345  let hcut = statement_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
346  hcut __
347
348(** val statement_inv_rect_Type3 :
349    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
350    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
351    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
352    -> FrontEndOps.unary_operation -> Registers.register ->
353    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
354    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
355    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
356    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
357    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
358    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
359    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
360    (Registers.register -> Registers.register List.list -> Registers.register
361    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
362    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
363let statement_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
364  let hcut = statement_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
365  hcut __
366
367(** val statement_inv_rect_Type2 :
368    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
369    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
370    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
371    -> FrontEndOps.unary_operation -> Registers.register ->
372    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
373    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
374    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
375    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
376    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
377    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
378    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
379    (Registers.register -> Registers.register List.list -> Registers.register
380    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
381    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
382let statement_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
383  let hcut = statement_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
384  hcut __
385
386(** val statement_inv_rect_Type1 :
387    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
388    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
389    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
390    -> FrontEndOps.unary_operation -> Registers.register ->
391    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
392    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
393    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
394    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
395    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
396    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
397    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
398    (Registers.register -> Registers.register List.list -> Registers.register
399    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
400    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
401let statement_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
402  let hcut = statement_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
403  hcut __
404
405(** val statement_inv_rect_Type0 :
406    statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
407    Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
408    FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
409    -> FrontEndOps.unary_operation -> Registers.register ->
410    Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
411    -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
412    Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
413    (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
414    __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
415    Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
416    -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
417    (Registers.register -> Registers.register List.list -> Registers.register
418    Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
419    Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
420let statement_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
421  let hcut = statement_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
422  hcut __
423
424(** val statement_jmdiscr : statement -> statement -> __ **)
425let statement_jmdiscr x y =
426  Logic.eq_rect_Type2 x
427    (match x with
428     | St_skip a0 -> Obj.magic (fun _ dH -> dH __)
429     | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
430     | St_const (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
431     | St_op1 (a0, a1, a2, a3, a4, a5) ->
432       Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
433     | St_op2 (a0, a1, a2, a3, a4, a5, a6, a7) ->
434       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
435     | St_load (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
436     | St_store (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
437     | St_call_id (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
438     | St_call_ptr (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
439     | St_cond (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
440     | St_return -> Obj.magic (fun _ dH -> dH)) y
441
442type internal_function = { f_labgen : Identifiers.universe;
443                           f_reggen : Identifiers.universe;
444                           f_result : (Registers.register, AST.typ)
445                                      Types.prod Types.option;
446                           f_params : (Registers.register, AST.typ)
447                                      Types.prod List.list;
448                           f_locals : (Registers.register, AST.typ)
449                                      Types.prod List.list;
450                           f_stacksize : Nat.nat;
451                           f_graph : statement Graphs.graph;
452                           f_entry : Graphs.label Types.sig0;
453                           f_exit : Graphs.label Types.sig0 }
454
455(** val internal_function_rect_Type4 :
456    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
457    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
458    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
459    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
460    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
461    internal_function -> 'a1 **)
462let rec internal_function_rect_Type4 h_mk_internal_function x_2362 =
463  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
464    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
465    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_2362
466  in
467  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
468    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
469
470(** val internal_function_rect_Type5 :
471    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
472    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
473    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
474    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
475    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
476    internal_function -> 'a1 **)
477let rec internal_function_rect_Type5 h_mk_internal_function x_2364 =
478  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
479    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
480    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_2364
481  in
482  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
483    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
484
485(** val internal_function_rect_Type3 :
486    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
487    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
488    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
489    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
490    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
491    internal_function -> 'a1 **)
492let rec internal_function_rect_Type3 h_mk_internal_function x_2366 =
493  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
494    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
495    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_2366
496  in
497  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
498    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
499
500(** val internal_function_rect_Type2 :
501    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
502    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
503    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
504    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
505    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
506    internal_function -> 'a1 **)
507let rec internal_function_rect_Type2 h_mk_internal_function x_2368 =
508  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
509    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
510    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_2368
511  in
512  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
513    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
514
515(** val internal_function_rect_Type1 :
516    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
517    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
518    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
519    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
520    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
521    internal_function -> 'a1 **)
522let rec internal_function_rect_Type1 h_mk_internal_function x_2370 =
523  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
524    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
525    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_2370
526  in
527  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
528    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
529
530(** val internal_function_rect_Type0 :
531    (Identifiers.universe -> Identifiers.universe -> (Registers.register,
532    AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
533    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
534    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
535    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
536    internal_function -> 'a1 **)
537let rec internal_function_rect_Type0 h_mk_internal_function x_2372 =
538  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
539    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
540    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_2372
541  in
542  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
543    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
544
545(** val f_labgen : internal_function -> Identifiers.universe **)
546let rec f_labgen xxx =
547  xxx.f_labgen
548
549(** val f_reggen : internal_function -> Identifiers.universe **)
550let rec f_reggen xxx =
551  xxx.f_reggen
552
553(** val f_result :
554    internal_function -> (Registers.register, AST.typ) Types.prod
555    Types.option **)
556let rec f_result xxx =
557  xxx.f_result
558
559(** val f_params :
560    internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
561let rec f_params xxx =
562  xxx.f_params
563
564(** val f_locals :
565    internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
566let rec f_locals xxx =
567  xxx.f_locals
568
569(** val f_stacksize : internal_function -> Nat.nat **)
570let rec f_stacksize xxx =
571  xxx.f_stacksize
572
573(** val f_graph : internal_function -> statement Graphs.graph **)
574let rec f_graph xxx =
575  xxx.f_graph
576
577(** val f_entry : internal_function -> Graphs.label Types.sig0 **)
578let rec f_entry xxx =
579  xxx.f_entry
580
581(** val f_exit : internal_function -> Graphs.label Types.sig0 **)
582let rec f_exit xxx =
583  xxx.f_exit
584
585(** val internal_function_inv_rect_Type4 :
586    internal_function -> (Identifiers.universe -> Identifiers.universe ->
587    (Registers.register, AST.typ) Types.prod Types.option ->
588    (Registers.register, AST.typ) Types.prod List.list ->
589    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
590    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
591    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
592let internal_function_inv_rect_Type4 hterm h1 =
593  let hcut = internal_function_rect_Type4 h1 hterm in hcut __
594
595(** val internal_function_inv_rect_Type3 :
596    internal_function -> (Identifiers.universe -> Identifiers.universe ->
597    (Registers.register, AST.typ) Types.prod Types.option ->
598    (Registers.register, AST.typ) Types.prod List.list ->
599    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
600    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
601    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
602let internal_function_inv_rect_Type3 hterm h1 =
603  let hcut = internal_function_rect_Type3 h1 hterm in hcut __
604
605(** val internal_function_inv_rect_Type2 :
606    internal_function -> (Identifiers.universe -> Identifiers.universe ->
607    (Registers.register, AST.typ) Types.prod Types.option ->
608    (Registers.register, AST.typ) Types.prod List.list ->
609    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
610    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
611    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
612let internal_function_inv_rect_Type2 hterm h1 =
613  let hcut = internal_function_rect_Type2 h1 hterm in hcut __
614
615(** val internal_function_inv_rect_Type1 :
616    internal_function -> (Identifiers.universe -> Identifiers.universe ->
617    (Registers.register, AST.typ) Types.prod Types.option ->
618    (Registers.register, AST.typ) Types.prod List.list ->
619    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
620    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
621    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
622let internal_function_inv_rect_Type1 hterm h1 =
623  let hcut = internal_function_rect_Type1 h1 hterm in hcut __
624
625(** val internal_function_inv_rect_Type0 :
626    internal_function -> (Identifiers.universe -> Identifiers.universe ->
627    (Registers.register, AST.typ) Types.prod Types.option ->
628    (Registers.register, AST.typ) Types.prod List.list ->
629    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
630    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
631    Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
632let internal_function_inv_rect_Type0 hterm h1 =
633  let hcut = internal_function_rect_Type0 h1 hterm in hcut __
634
635(** val internal_function_jmdiscr :
636    internal_function -> internal_function -> __ **)
637let internal_function_jmdiscr x y =
638  Logic.eq_rect_Type2 x
639    (let { f_labgen = a0; f_reggen = a1; f_result = a2; f_params = a3;
640       f_locals = a4; f_stacksize = a5; f_graph = a6; f_entry = a9; f_exit =
641       a10 } = x
642     in
643    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y
644
645type rTLabs_program = (internal_function AST.fundef, Nat.nat) AST.program
646
Note: See TracBrowser for help on using the repository browser.