source: extracted/registers.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: 863 bytes
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open PreIdentifiers
10
11open Errors
12
13open Extralib
14
15open Setoids
16
17open Monad
18
19open Option
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open Util
28
29open Lists
30
31open Positive
32
33open Char
34
35open Bool
36
37open Relations
38
39open Nat
40
41open List
42
43open String
44
45open Hints_declaration
46
47open Core_notation
48
49open Pts
50
51open Logic
52
53open Types
54
55open Identifiers
56
57open Order
58
59(** val registerTag : String.string **)
60let registerTag = "register tag"
61  (*failwith "AXIOM TO BE REALIZED"*)
62
63type register = PreIdentifiers.identifier
64
65(** val register_eq : register -> register -> (__, __) Types.sum **)
66let register_eq =
67  Identifiers.identifier_eq registerTag
68
69type 'a register_env = 'a Identifiers.identifier_map
70
71(** val register_ord : register -> register -> Order.order **)
72let register_ord =
73  failwith "AXIOM TO BE REALIZED"
74
Note: See TracBrowser for help on using the repository browser.