source: extracted/frontend_misc.mli @ 2649

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

...

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 Setoids
22
23open Monad
24
25open Option
26
27open Lists
28
29open Positive
30
31open Identifiers
32
33open Arithmetic
34
35open Vector
36
37open Div_and_mod
38
39open Jmeq
40
41open Russell
42
43open List
44
45open Util
46
47open FoldStuff
48
49open BitVector
50
51open Extranat
52
53open Bool
54
55open Relations
56
57open Nat
58
59open Integers
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Types
70
71open AST
72
73open Csyntax
74
75open TypeComparison
76
77open ClassifyOp
78
79open Events
80
81open Smallstep
82
83open Extra_bool
84
85open Values
86
87open FrontEndVal
88
89open Hide
90
91open ByteValues
92
93open Division
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open GenMem
102
103open FrontEndMem
104
105open Globalenvs
106
107open Csem
108
109open Star
110
111open IOMonad
112
113open IO
114
115open Sets
116
117open Listb
118
119val block_DeqSet : Deqsets.deqSet
120
121val mem_assoc_env :
122  AST.ident -> (AST.ident, Csyntax.type0) Types.prod List.list -> Bool.bool
123
124type 'a lset = 'a List.list
125
126val empty_lset : 'a1 List.list
127
128val lset_union : 'a1 lset -> 'a1 lset -> 'a1 List.list
129
130val lset_remove : Deqsets.deqSet -> __ lset -> __ -> __ List.list
131
132val lset_difference : Deqsets.deqSet -> __ lset -> __ lset -> __ List.list
133
134val wF_rect : ('a1 -> __ -> ('a1 -> __ -> 'a2) -> 'a2) -> 'a1 -> 'a2
135
136val one_bv : Nat.nat -> BitVector.bitVector
137
138val ith_carry :
139  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
140  Bool.bool
141
142val ith_bit :
143  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
144  Bool.bool
145
146val bitvector_fold :
147  Nat.nat -> BitVector.bitVector -> (Nat.nat -> BitVector.bitVector ->
148  Bool.bool) -> BitVector.bitVector
149
150val bitvector_fold2 :
151  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (Nat.nat ->
152  BitVector.bitVector -> BitVector.bitVector -> Bool.bool) ->
153  BitVector.bitVector
154
155val addition_n_direct :
156  Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
157  BitVector.bitVector
158
159val increment_direct : Nat.nat -> BitVector.bitVector -> BitVector.bitVector
160
161val twocomp_neg_direct :
162  Nat.nat -> BitVector.bitVector -> BitVector.bitVector
163
164val andb_fold : Nat.nat -> BitVector.bitVector -> Bool.bool
165
Note: See TracBrowser for help on using the repository browser.