source: extracted/deqsets.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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_2134 =
24  let eqb = x_2134 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_2136 =
29  let eqb = x_2136 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_2138 =
34  let eqb = x_2138 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_2140 =
39  let eqb = x_2140 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_2142 =
44  let eqb = x_2142 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_2144 =
49  let eqb = x_2144 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.