source: driver/extracted/frontend_misc.mli @ 3106

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

Everything extracted again.

File size: 2.2 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
27open Exp
28
29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Setoids
48
49open Monad
50
51open Option
52
53open Extranat
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Integers
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open AST
74
75open Csyntax
76
77open TypeComparison
78
79open ClassifyOp
80
81open Events
82
83open Smallstep
84
85open Extra_bool
86
87open Values
88
89open FrontEndVal
90
91open Hide
92
93open ByteValues
94
95open Division
96
97open Z
98
99open BitVectorZ
100
101open Pointers
102
103open GenMem
104
105open FrontEndMem
106
107open Globalenvs
108
109open Csem
110
111open Star
112
113open IOMonad
114
115open IO
116
117open Sets
118
119open Listb
120
121val typ_eq_dec : AST.typ -> AST.typ -> (__, __) Types.sum
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.