source: extracted/frontend_misc.mli @ 2746

Last change on this file since 2746 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: 2.2 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open CostLabel
6
7open Coqlib
8
9open Proper
10
11open PositiveMap
12
13open Deqsets
14
15open ErrorMessages
16
17open PreIdentifiers
18
19open Errors
20
21open Extralib
22
23open Setoids
24
25open Monad
26
27open Option
28
29open Lists
30
31open Positive
32
33open Identifiers
34
35open Exp
36
37open Arithmetic
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
79open TypeComparison
80
81open ClassifyOp
82
83open Events
84
85open Smallstep
86
87open Extra_bool
88
89open Values
90
91open FrontEndVal
92
93open Hide
94
95open ByteValues
96
97open Division
98
99open Z
100
101open BitVectorZ
102
103open Pointers
104
105open GenMem
106
107open FrontEndMem
108
109open Globalenvs
110
111open Csem
112
113open Star
114
115open IOMonad
116
117open IO
118
119open Sets
120
121open Listb
122
123val block_DeqSet : Deqsets.deqSet
124
125val mem_assoc_env :
126  AST.ident -> (AST.ident, Csyntax.type0) Types.prod List.list -> Bool.bool
127
128type 'a lset = 'a List.list
129
130val empty_lset : 'a1 List.list
131
132val lset_union : 'a1 lset -> 'a1 lset -> 'a1 List.list
133
134val lset_remove : Deqsets.deqSet -> __ lset -> __ -> __ List.list
135
136val lset_difference : Deqsets.deqSet -> __ lset -> __ lset -> __ List.list
137
138val wF_rect : ('a1 -> __ -> ('a1 -> __ -> 'a2) -> 'a2) -> 'a1 -> 'a2
139
140val one_bv : Nat.nat -> BitVector.bitVector
141
142val ith_carry :
143  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
144  Bool.bool
145
146val ith_bit :
147  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
148  Bool.bool
149
150val bitvector_fold :
151  Nat.nat -> BitVector.bitVector -> (Nat.nat -> BitVector.bitVector ->
152  Bool.bool) -> BitVector.bitVector
153
154val bitvector_fold2 :
155  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (Nat.nat ->
156  BitVector.bitVector -> BitVector.bitVector -> Bool.bool) ->
157  BitVector.bitVector
158
159val addition_n_direct :
160  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
161  BitVector.bitVector
162
163val increment_direct : Nat.nat -> BitVector.bitVector -> BitVector.bitVector
164
165val twocomp_neg_direct :
166  Nat.nat -> BitVector.bitVector -> BitVector.bitVector
167
168val andb_fold : Nat.nat -> BitVector.bitVector -> Bool.bool
169
Note: See TracBrowser for help on using the repository browser.