source: extracted/deqsets.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: 4.0 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Relations
14
15open Bool
16
17type deqSet =
18  __ -> __ -> Bool.bool
19  (* singleton inductive, whose constructor was mk_DeqSet *)
20
21(** val deqSet_rect_Type4 :
22    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
23let rec deqSet_rect_Type4 h_mk_DeqSet x_3083 =
24  let eqb = x_3083 in h_mk_DeqSet __ eqb __
25
26(** val deqSet_rect_Type5 :
27    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
28let rec deqSet_rect_Type5 h_mk_DeqSet x_3085 =
29  let eqb = x_3085 in h_mk_DeqSet __ eqb __
30
31(** val deqSet_rect_Type3 :
32    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
33let rec deqSet_rect_Type3 h_mk_DeqSet x_3087 =
34  let eqb = x_3087 in h_mk_DeqSet __ eqb __
35
36(** val deqSet_rect_Type2 :
37    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
38let rec deqSet_rect_Type2 h_mk_DeqSet x_3089 =
39  let eqb = x_3089 in h_mk_DeqSet __ eqb __
40
41(** val deqSet_rect_Type1 :
42    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
43let rec deqSet_rect_Type1 h_mk_DeqSet x_3091 =
44  let eqb = x_3091 in h_mk_DeqSet __ eqb __
45
46(** val deqSet_rect_Type0 :
47    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
48let rec deqSet_rect_Type0 h_mk_DeqSet x_3093 =
49  let eqb = x_3093 in h_mk_DeqSet __ eqb __
50
51type carr = __
52
53(** val eqb : deqSet -> __ -> __ -> Bool.bool **)
54let rec eqb xxx =
55  let yyy = xxx in yyy
56
57(** val deqSet_inv_rect_Type4 :
58    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
59let deqSet_inv_rect_Type4 hterm h1 =
60  let hcut = deqSet_rect_Type4 h1 hterm in hcut __
61
62(** val deqSet_inv_rect_Type3 :
63    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
64let deqSet_inv_rect_Type3 hterm h1 =
65  let hcut = deqSet_rect_Type3 h1 hterm in hcut __
66
67(** val deqSet_inv_rect_Type2 :
68    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
69let deqSet_inv_rect_Type2 hterm h1 =
70  let hcut = deqSet_rect_Type2 h1 hterm in hcut __
71
72(** val deqSet_inv_rect_Type1 :
73    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
74let deqSet_inv_rect_Type1 hterm h1 =
75  let hcut = deqSet_rect_Type1 h1 hterm in hcut __
76
77(** val deqSet_inv_rect_Type0 :
78    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
79let deqSet_inv_rect_Type0 hterm h1 =
80  let hcut = deqSet_rect_Type0 h1 hterm in hcut __
81
82(** val beqb : Bool.bool -> Bool.bool -> Bool.bool **)
83let beqb b1 b2 =
84  match b1 with
85  | Bool.True -> b2
86  | Bool.False -> Bool.notb b2
87
88(** val deqBool : deqSet **)
89let deqBool =
90  Obj.magic beqb
91
92(** val eq_option :
93    deqSet -> __ Types.option -> __ Types.option -> Bool.bool **)
94let eq_option a a1 a2 =
95  match a1 with
96  | Types.None ->
97    (match a2 with
98     | Types.None -> Bool.True
99     | Types.Some x -> Bool.False)
100  | Types.Some a1' ->
101    (match a2 with
102     | Types.None -> Bool.False
103     | Types.Some a2' -> eqb a a1' a2')
104
105(** val deqOption : deqSet -> deqSet **)
106let deqOption a =
107  Obj.magic (eq_option a)
108
109(** val eq_pairs :
110    deqSet -> deqSet -> (__, __) Types.prod -> (__, __) Types.prod ->
111    Bool.bool **)
112let eq_pairs a b p1 p2 =
113  Bool.andb (eqb a p1.Types.fst p2.Types.fst)
114    (eqb b p1.Types.snd p2.Types.snd)
115
116(** val deqProd : deqSet -> deqSet -> deqSet **)
117let deqProd a b =
118  Obj.magic (eq_pairs a b)
119
120(** val eq_sum :
121    deqSet -> deqSet -> (__, __) Types.sum -> (__, __) Types.sum -> Bool.bool **)
122let eq_sum a b p1 p2 =
123  match p1 with
124  | Types.Inl a1 ->
125    (match p2 with
126     | Types.Inl a2 -> eqb a a1 a2
127     | Types.Inr b2 -> Bool.False)
128  | Types.Inr b1 ->
129    (match p2 with
130     | Types.Inl a2 -> Bool.False
131     | Types.Inr b2 -> eqb b b1 b2)
132
133(** val deqSum : deqSet -> deqSet -> deqSet **)
134let deqSum a b =
135  Obj.magic (eq_sum a b)
136
137(** val eq_sigma : deqSet -> __ Types.sig0 -> __ Types.sig0 -> Bool.bool **)
138let eq_sigma a p1 p2 =
139  let a1 = p1 in let a2 = p2 in eqb a a1 a2
140
141(** val deqSig : deqSet -> deqSet **)
142let deqSig a =
143  Obj.magic (eq_sigma a)
144
Note: See TracBrowser for help on using the repository browser.