source: driver/extracted/order.ml @ 3106

Last change on this file since 3106 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.6 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13type order =
14| Order_lt
15| Order_eq
16| Order_gt
17
18(** val order_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
19let rec order_rect_Type4 h_order_lt h_order_eq h_order_gt = function
20| Order_lt -> h_order_lt
21| Order_eq -> h_order_eq
22| Order_gt -> h_order_gt
23
24(** val order_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
25let rec order_rect_Type5 h_order_lt h_order_eq h_order_gt = function
26| Order_lt -> h_order_lt
27| Order_eq -> h_order_eq
28| Order_gt -> h_order_gt
29
30(** val order_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
31let rec order_rect_Type3 h_order_lt h_order_eq h_order_gt = function
32| Order_lt -> h_order_lt
33| Order_eq -> h_order_eq
34| Order_gt -> h_order_gt
35
36(** val order_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
37let rec order_rect_Type2 h_order_lt h_order_eq h_order_gt = function
38| Order_lt -> h_order_lt
39| Order_eq -> h_order_eq
40| Order_gt -> h_order_gt
41
42(** val order_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
43let rec order_rect_Type1 h_order_lt h_order_eq h_order_gt = function
44| Order_lt -> h_order_lt
45| Order_eq -> h_order_eq
46| Order_gt -> h_order_gt
47
48(** val order_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
49let rec order_rect_Type0 h_order_lt h_order_eq h_order_gt = function
50| Order_lt -> h_order_lt
51| Order_eq -> h_order_eq
52| Order_gt -> h_order_gt
53
54(** val order_inv_rect_Type4 :
55    order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
56let order_inv_rect_Type4 hterm h1 h2 h3 =
57  let hcut = order_rect_Type4 h1 h2 h3 hterm in hcut __
58
59(** val order_inv_rect_Type3 :
60    order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
61let order_inv_rect_Type3 hterm h1 h2 h3 =
62  let hcut = order_rect_Type3 h1 h2 h3 hterm in hcut __
63
64(** val order_inv_rect_Type2 :
65    order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
66let order_inv_rect_Type2 hterm h1 h2 h3 =
67  let hcut = order_rect_Type2 h1 h2 h3 hterm in hcut __
68
69(** val order_inv_rect_Type1 :
70    order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
71let order_inv_rect_Type1 hterm h1 h2 h3 =
72  let hcut = order_rect_Type1 h1 h2 h3 hterm in hcut __
73
74(** val order_inv_rect_Type0 :
75    order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
76let order_inv_rect_Type0 hterm h1 h2 h3 =
77  let hcut = order_rect_Type0 h1 h2 h3 hterm in hcut __
78
79(** val order_discr : order -> order -> __ **)
80let order_discr x y =
81  Logic.eq_rect_Type2 x
82    (match x with
83     | Order_lt -> Obj.magic (fun _ dH -> dH)
84     | Order_eq -> Obj.magic (fun _ dH -> dH)
85     | Order_gt -> Obj.magic (fun _ dH -> dH)) y
86
Note: See TracBrowser for help on using the repository browser.