source: extracted/frontEndVal.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 Proper
4
5open PositiveMap
6
7open Deqsets
8
9open Extralib
10
11open Lists
12
13open Identifiers
14
15open Floats
16
17open Integers
18
19open AST
20
21open Division
22
23open Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
39open Option
40
41open Setoids
42
43open Monad
44
45open Positive
46
47open Char
48
49open String
50
51open PreIdentifiers
52
53open Errors
54
55open Div_and_mod
56
57open Jmeq
58
59open Russell
60
61open Util
62
63open Bool
64
65open Relations
66
67open Nat
68
69open List
70
71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
79open Types
80
81open Coqlib
82
83open Values
84
85open Hide
86
87open ByteValues
88
89val make_parts : ByteValues.part List.list
90
91val make_be_null : ByteValues.beval List.list
92
93val bytes_of_bitvector :
94  Nat.nat -> BitVector.bitVector -> BitVector.byte List.list
95
96val fe_to_be_values : AST.typ -> Values.val0 -> ByteValues.beval List.list
97
98val check_be_null : Nat.nat -> ByteValues.beval List.list -> Bool.bool
99
100val build_integer :
101  Nat.nat -> ByteValues.beval List.list -> BitVector.bitVector Types.option
102
103val build_integer_val : AST.typ -> ByteValues.beval List.list -> Values.val0
104
105val be_to_fe_value : AST.typ -> ByteValues.beval List.list -> Values.val0
106
Note: See TracBrowser for help on using the repository browser.