source: extracted/bool.ml @ 2746

Last change on this file since 2746 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.5 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Relations
12
13type bool =
14| True
15| False
16
17(** val bool_rect_Type4 : 'a1 -> 'a1 -> bool -> 'a1 **)
18let rec bool_rect_Type4 h_true h_false = function
19| True -> h_true
20| False -> h_false
21
22(** val bool_rect_Type5 : 'a1 -> 'a1 -> bool -> 'a1 **)
23let rec bool_rect_Type5 h_true h_false = function
24| True -> h_true
25| False -> h_false
26
27(** val bool_rect_Type3 : 'a1 -> 'a1 -> bool -> 'a1 **)
28let rec bool_rect_Type3 h_true h_false = function
29| True -> h_true
30| False -> h_false
31
32(** val bool_rect_Type2 : 'a1 -> 'a1 -> bool -> 'a1 **)
33let rec bool_rect_Type2 h_true h_false = function
34| True -> h_true
35| False -> h_false
36
37(** val bool_rect_Type1 : 'a1 -> 'a1 -> bool -> 'a1 **)
38let rec bool_rect_Type1 h_true h_false = function
39| True -> h_true
40| False -> h_false
41
42(** val bool_rect_Type0 : 'a1 -> 'a1 -> bool -> 'a1 **)
43let rec bool_rect_Type0 h_true h_false = function
44| True -> h_true
45| False -> h_false
46
47(** val bool_inv_rect_Type4 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
48let bool_inv_rect_Type4 hterm h1 h2 =
49  let hcut = bool_rect_Type4 h1 h2 hterm in hcut __
50
51(** val bool_inv_rect_Type3 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
52let bool_inv_rect_Type3 hterm h1 h2 =
53  let hcut = bool_rect_Type3 h1 h2 hterm in hcut __
54
55(** val bool_inv_rect_Type2 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
56let bool_inv_rect_Type2 hterm h1 h2 =
57  let hcut = bool_rect_Type2 h1 h2 hterm in hcut __
58
59(** val bool_inv_rect_Type1 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
60let bool_inv_rect_Type1 hterm h1 h2 =
61  let hcut = bool_rect_Type1 h1 h2 hterm in hcut __
62
63(** val bool_inv_rect_Type0 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
64let bool_inv_rect_Type0 hterm h1 h2 =
65  let hcut = bool_rect_Type0 h1 h2 hterm in hcut __
66
67(** val bool_discr : bool -> bool -> __ **)
68let bool_discr x y =
69  Logic.eq_rect_Type2 x
70    (match x with
71     | True -> Obj.magic (fun _ dH -> dH)
72     | False -> Obj.magic (fun _ dH -> dH)) y
73
74(** val notb : bool -> bool **)
75let notb = function
76| True -> False
77| False -> True
78
79(** val andb : bool -> bool -> bool **)
80let andb b1 b2 =
81  match b1 with
82  | True -> b2
83  | False -> False
84
85(** val orb : bool -> bool -> bool **)
86let orb b1 b2 =
87  match b1 with
88  | True -> True
89  | False -> b2
90
91(** val xorb : bool -> bool -> bool **)
92let xorb b1 b2 =
93  match b1 with
94  | True ->
95    (match b2 with
96     | True -> False
97     | False -> True)
98  | False ->
99    (match b2 with
100     | True -> True
101     | False -> False)
102
Note: See TracBrowser for help on using the repository browser.