]> matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/blob - extracted/frontend_misc.mli
Imported Upstream version 0.1
[pkg-cerco/acc-trusted.git] / extracted / frontend_misc.mli
1 open Preamble
2
3 open CostLabel
4
5 open Coqlib
6
7 open Proper
8
9 open PositiveMap
10
11 open Deqsets
12
13 open ErrorMessages
14
15 open PreIdentifiers
16
17 open Errors
18
19 open Extralib
20
21 open Lists
22
23 open Positive
24
25 open Identifiers
26
27 open Exp
28
29 open Arithmetic
30
31 open Vector
32
33 open Div_and_mod
34
35 open Util
36
37 open FoldStuff
38
39 open BitVector
40
41 open Jmeq
42
43 open Russell
44
45 open List
46
47 open Setoids
48
49 open Monad
50
51 open Option
52
53 open Extranat
54
55 open Bool
56
57 open Relations
58
59 open Nat
60
61 open Integers
62
63 open Hints_declaration
64
65 open Core_notation
66
67 open Pts
68
69 open Logic
70
71 open Types
72
73 open AST
74
75 open Csyntax
76
77 open TypeComparison
78
79 open ClassifyOp
80
81 open Events
82
83 open Smallstep
84
85 open Extra_bool
86
87 open Values
88
89 open FrontEndVal
90
91 open Hide
92
93 open ByteValues
94
95 open Division
96
97 open Z
98
99 open BitVectorZ
100
101 open Pointers
102
103 open GenMem
104
105 open FrontEndMem
106
107 open Globalenvs
108
109 open Csem
110
111 open Star
112
113 open IOMonad
114
115 open IO
116
117 open Sets
118
119 open Listb
120
121 val typ_eq_dec : AST.typ -> AST.typ -> (__, __) Types.sum
122
123 val block_DeqSet : Deqsets.deqSet
124
125 val mem_assoc_env :
126   AST.ident -> (AST.ident, Csyntax.type0) Types.prod List.list -> Bool.bool
127
128 type 'a lset = 'a List.list
129
130 val empty_lset : 'a1 List.list
131
132 val lset_union : 'a1 lset -> 'a1 lset -> 'a1 List.list
133
134 val lset_remove : Deqsets.deqSet -> __ lset -> __ -> __ List.list
135
136 val lset_difference : Deqsets.deqSet -> __ lset -> __ lset -> __ List.list
137
138 val wF_rect : ('a1 -> __ -> ('a1 -> __ -> 'a2) -> 'a2) -> 'a1 -> 'a2
139
140 val one_bv : Nat.nat -> BitVector.bitVector
141
142 val ith_carry :
143   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
144   Bool.bool
145
146 val ith_bit :
147   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
148   Bool.bool
149
150 val bitvector_fold :
151   Nat.nat -> BitVector.bitVector -> (Nat.nat -> BitVector.bitVector ->
152   Bool.bool) -> BitVector.bitVector
153
154 val bitvector_fold2 :
155   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (Nat.nat ->
156   BitVector.bitVector -> BitVector.bitVector -> Bool.bool) ->
157   BitVector.bitVector
158
159 val addition_n_direct :
160   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
161   BitVector.bitVector
162
163 val increment_direct : Nat.nat -> BitVector.bitVector -> BitVector.bitVector
164
165 val twocomp_neg_direct :
166   Nat.nat -> BitVector.bitVector -> BitVector.bitVector
167
168 val andb_fold : Nat.nat -> BitVector.bitVector -> Bool.bool
169