source: extracted/labelledObjects.mli @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 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: 1.1 KB
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
57type 'a labelled_obj =
58  (PreIdentifiers.identifier Types.option, 'a) Types.prod
59
60val instruction_matches_identifier :
61  String.string -> PreIdentifiers.identifier -> 'a1 labelled_obj -> Bool.bool
62
63val does_not_occur :
64  String.string -> PreIdentifiers.identifier -> 'a1 labelled_obj List.list ->
65  Bool.bool
66
67val occurs_exactly_once :
68  String.string -> PreIdentifiers.identifier -> 'a1 labelled_obj List.list ->
69  Bool.bool
70
71val index_of_internal :
72  ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> Nat.nat
73
74val index_of0 : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat
75
76val index_of_label :
77  String.string -> PreIdentifiers.identifier -> 'a1 labelled_obj List.list ->
78  Nat.nat
79
Note: See TracBrowser for help on using the repository browser.