source: extracted/frontEndVal.mli @ 2960

Last change on this file since 2960 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
RevLine 
[2601]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
[2717]21open Exp
22
[2601]23open Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
[2649]39open ErrorMessages
40
[2601]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.