source: extracted/preIdentifiers.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.
File size: 6.7 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19open Positive
20
21type identifierTag =
22| Label
23| CostTag
24| RegisterTag
25| LabelTag
26| SymbolTag
27| ASMTag
28
29(** val identifierTag_rect_Type4 :
30    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
31let rec identifierTag_rect_Type4 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
32| Label -> h_Label
33| CostTag -> h_CostTag
34| RegisterTag -> h_RegisterTag
35| LabelTag -> h_LabelTag
36| SymbolTag -> h_SymbolTag
37| ASMTag -> h_ASMTag
38
39(** val identifierTag_rect_Type5 :
40    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
41let rec identifierTag_rect_Type5 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
42| Label -> h_Label
43| CostTag -> h_CostTag
44| RegisterTag -> h_RegisterTag
45| LabelTag -> h_LabelTag
46| SymbolTag -> h_SymbolTag
47| ASMTag -> h_ASMTag
48
49(** val identifierTag_rect_Type3 :
50    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
51let rec identifierTag_rect_Type3 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
52| Label -> h_Label
53| CostTag -> h_CostTag
54| RegisterTag -> h_RegisterTag
55| LabelTag -> h_LabelTag
56| SymbolTag -> h_SymbolTag
57| ASMTag -> h_ASMTag
58
59(** val identifierTag_rect_Type2 :
60    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
61let rec identifierTag_rect_Type2 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
62| Label -> h_Label
63| CostTag -> h_CostTag
64| RegisterTag -> h_RegisterTag
65| LabelTag -> h_LabelTag
66| SymbolTag -> h_SymbolTag
67| ASMTag -> h_ASMTag
68
69(** val identifierTag_rect_Type1 :
70    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
71let rec identifierTag_rect_Type1 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
72| Label -> h_Label
73| CostTag -> h_CostTag
74| RegisterTag -> h_RegisterTag
75| LabelTag -> h_LabelTag
76| SymbolTag -> h_SymbolTag
77| ASMTag -> h_ASMTag
78
79(** val identifierTag_rect_Type0 :
80    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
81let rec identifierTag_rect_Type0 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
82| Label -> h_Label
83| CostTag -> h_CostTag
84| RegisterTag -> h_RegisterTag
85| LabelTag -> h_LabelTag
86| SymbolTag -> h_SymbolTag
87| ASMTag -> h_ASMTag
88
89(** val identifierTag_inv_rect_Type4 :
90    identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
91    -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
92let identifierTag_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 =
93  let hcut = identifierTag_rect_Type4 h1 h2 h3 h4 h5 h6 hterm in hcut __
94
95(** val identifierTag_inv_rect_Type3 :
96    identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
97    -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
98let identifierTag_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 =
99  let hcut = identifierTag_rect_Type3 h1 h2 h3 h4 h5 h6 hterm in hcut __
100
101(** val identifierTag_inv_rect_Type2 :
102    identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
103    -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
104let identifierTag_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 =
105  let hcut = identifierTag_rect_Type2 h1 h2 h3 h4 h5 h6 hterm in hcut __
106
107(** val identifierTag_inv_rect_Type1 :
108    identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
109    -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
110let identifierTag_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 =
111  let hcut = identifierTag_rect_Type1 h1 h2 h3 h4 h5 h6 hterm in hcut __
112
113(** val identifierTag_inv_rect_Type0 :
114    identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
115    -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
116let identifierTag_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 =
117  let hcut = identifierTag_rect_Type0 h1 h2 h3 h4 h5 h6 hterm in hcut __
118
119(** val identifierTag_discr : identifierTag -> identifierTag -> __ **)
120let identifierTag_discr x y =
121  Logic.eq_rect_Type2 x
122    (match x with
123     | Label -> Obj.magic (fun _ dH -> dH)
124     | CostTag -> Obj.magic (fun _ dH -> dH)
125     | RegisterTag -> Obj.magic (fun _ dH -> dH)
126     | LabelTag -> Obj.magic (fun _ dH -> dH)
127     | SymbolTag -> Obj.magic (fun _ dH -> dH)
128     | ASMTag -> Obj.magic (fun _ dH -> dH)) y
129
130type identifier =
131  Positive.pos
132  (* singleton inductive, whose constructor was an_identifier *)
133
134(** val identifier_rect_Type4 :
135    identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
136let rec identifier_rect_Type4 tag h_an_identifier x_2031 =
137  let x_2032 = x_2031 in h_an_identifier x_2032
138
139(** val identifier_rect_Type5 :
140    identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
141let rec identifier_rect_Type5 tag h_an_identifier x_2034 =
142  let x_2035 = x_2034 in h_an_identifier x_2035
143
144(** val identifier_rect_Type3 :
145    identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
146let rec identifier_rect_Type3 tag h_an_identifier x_2037 =
147  let x_2038 = x_2037 in h_an_identifier x_2038
148
149(** val identifier_rect_Type2 :
150    identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
151let rec identifier_rect_Type2 tag h_an_identifier x_2040 =
152  let x_2041 = x_2040 in h_an_identifier x_2041
153
154(** val identifier_rect_Type1 :
155    identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
156let rec identifier_rect_Type1 tag h_an_identifier x_2043 =
157  let x_2044 = x_2043 in h_an_identifier x_2044
158
159(** val identifier_rect_Type0 :
160    identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
161let rec identifier_rect_Type0 tag h_an_identifier x_2046 =
162  let x_2047 = x_2046 in h_an_identifier x_2047
163
164(** val identifier_inv_rect_Type4 :
165    identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
166let identifier_inv_rect_Type4 x1 hterm h1 =
167  let hcut = identifier_rect_Type4 x1 h1 hterm in hcut __
168
169(** val identifier_inv_rect_Type3 :
170    identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
171let identifier_inv_rect_Type3 x1 hterm h1 =
172  let hcut = identifier_rect_Type3 x1 h1 hterm in hcut __
173
174(** val identifier_inv_rect_Type2 :
175    identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
176let identifier_inv_rect_Type2 x1 hterm h1 =
177  let hcut = identifier_rect_Type2 x1 h1 hterm in hcut __
178
179(** val identifier_inv_rect_Type1 :
180    identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
181let identifier_inv_rect_Type1 x1 hterm h1 =
182  let hcut = identifier_rect_Type1 x1 h1 hterm in hcut __
183
184(** val identifier_inv_rect_Type0 :
185    identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
186let identifier_inv_rect_Type0 x1 hterm h1 =
187  let hcut = identifier_rect_Type0 x1 h1 hterm in hcut __
188
189(** val identifier_discr :
190    identifierTag -> identifier -> identifier -> __ **)
191let identifier_discr a1 x y =
192  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
193
Note: See TracBrowser for help on using the repository browser.