source: extracted/setoids.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: 2.4 KB
Line 
1open Preamble
2
3open Core_notation
4
5open Pts
6
7open Hints_declaration
8
9open Logic
10
11open Types
12
13open Relations
14
15type setoid =
16| Mk_Setoid
17
18(** val setoid_rect_Type4 :
19    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
20let rec setoid_rect_Type4 h_mk_Setoid = function
21| Mk_Setoid -> h_mk_Setoid __ __ __ __ __
22
23(** val setoid_rect_Type5 :
24    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
25let rec setoid_rect_Type5 h_mk_Setoid = function
26| Mk_Setoid -> h_mk_Setoid __ __ __ __ __
27
28(** val setoid_rect_Type3 :
29    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
30let rec setoid_rect_Type3 h_mk_Setoid = function
31| Mk_Setoid -> h_mk_Setoid __ __ __ __ __
32
33(** val setoid_rect_Type2 :
34    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
35let rec setoid_rect_Type2 h_mk_Setoid = function
36| Mk_Setoid -> h_mk_Setoid __ __ __ __ __
37
38(** val setoid_rect_Type1 :
39    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
40let rec setoid_rect_Type1 h_mk_Setoid = function
41| Mk_Setoid -> h_mk_Setoid __ __ __ __ __
42
43(** val setoid_rect_Type0 :
44    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
45let rec setoid_rect_Type0 h_mk_Setoid = function
46| Mk_Setoid -> h_mk_Setoid __ __ __ __ __
47
48type std_supp = __
49
50type std_eq = __
51
52(** val setoid_inv_rect_Type4 :
53    setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
54let setoid_inv_rect_Type4 hterm h1 =
55  let hcut = setoid_rect_Type4 h1 hterm in hcut __
56
57(** val setoid_inv_rect_Type3 :
58    setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
59let setoid_inv_rect_Type3 hterm h1 =
60  let hcut = setoid_rect_Type3 h1 hterm in hcut __
61
62(** val setoid_inv_rect_Type2 :
63    setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
64let setoid_inv_rect_Type2 hterm h1 =
65  let hcut = setoid_rect_Type2 h1 hterm in hcut __
66
67(** val setoid_inv_rect_Type1 :
68    setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
69let setoid_inv_rect_Type1 hterm h1 =
70  let hcut = setoid_rect_Type1 h1 hterm in hcut __
71
72(** val setoid_inv_rect_Type0 :
73    setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
74let setoid_inv_rect_Type0 hterm h1 =
75  let hcut = setoid_rect_Type0 h1 hterm in hcut __
76
77(** val as_std : setoid **)
78let as_std =
79  Mk_Setoid
80
81(** val std_prod : setoid -> setoid -> setoid **)
82let std_prod x y =
83  Mk_Setoid
84
85(** val std_union : setoid -> setoid -> setoid **)
86let std_union x y =
87  Mk_Setoid
88
Note: See TracBrowser for help on using the repository browser.