source: extracted/fresh.mli @ 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: 1.2 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open PreIdentifiers
12
13open Errors
14
15open Extralib
16
17open Setoids
18
19open Monad
20
21open Option
22
23open Lists
24
25open Positive
26
27open Identifiers
28
29open Coqlib
30
31open Floats
32
33open Arithmetic
34
35open Char
36
37open String
38
39open Vector
40
41open Div_and_mod
42
43open Jmeq
44
45open Russell
46
47open List
48
49open Util
50
51open FoldStuff
52
53open BitVector
54
55open Extranat
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Integers
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Types
74
75open AST
76
77open Csyntax
78
79val max_id : AST.ident -> AST.ident -> AST.ident
80
81val max_id_of_env :
82  (AST.ident, Csyntax.type0) Types.prod List.list -> AST.ident
83
84val max_id_of_fn : Csyntax.function0 -> AST.ident
85
86val max_id_of_fundef : Csyntax.clight_fundef -> AST.ident
87
88val max_id_of_functs :
89  (AST.ident, Csyntax.clight_fundef) Types.prod List.list -> AST.ident
90
91val max_id_of_globvars :
92  ((AST.ident, AST.region) Types.prod, (AST.init_data List.list,
93  Csyntax.type0) Types.prod) Types.prod List.list -> AST.ident
94
95val max_id_of_program : Csyntax.clight_program -> AST.ident
96
97val universe_of_max : AST.ident -> Identifiers.universe
98
99val universe_for_program : Csyntax.clight_program -> Identifiers.universe
100
Note: See TracBrowser for help on using the repository browser.