source: driver/extracted/frontEndVal.mli @ 3106

Last change on this file since 3106 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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 Integers
16
17open AST
18
19open Division
20
21open Exp
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 ErrorMessages
40
41open Option
42
43open Setoids
44
45open Monad
46
47open Positive
48
49open PreIdentifiers
50
51open Errors
52
53open Div_and_mod
54
55open Jmeq
56
57open Russell
58
59open Util
60
61open Bool
62
63open Relations
64
65open Nat
66
67open List
68
69open Hints_declaration
70
71open Core_notation
72
73open Pts
74
75open Logic
76
77open Types
78
79open Coqlib
80
81open Values
82
83open Hide
84
85open ByteValues
86
87val make_parts : ByteValues.part List.list
88
89val make_be_null : ByteValues.beval List.list
90
91val bytes_of_bitvector :
92  Nat.nat -> BitVector.bitVector -> BitVector.byte List.list
93
94val fe_to_be_values : AST.typ -> Values.val0 -> ByteValues.beval List.list
95
96val check_be_null : Nat.nat -> ByteValues.beval List.list -> Bool.bool
97
98val build_integer :
99  Nat.nat -> ByteValues.beval List.list -> BitVector.bitVector Types.option
100
101val build_integer_val : AST.typ -> ByteValues.beval List.list -> Values.val0
102
103val be_to_fe_value : AST.typ -> ByteValues.beval List.list -> Values.val0
104
Note: See TracBrowser for help on using the repository browser.