source: extracted/frontend_misc.ml @ 2716

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

...

File size: 4.5 KB
RevLine 
[2601]1open Preamble
2
3open CostLabel
4
[2649]5open Coqlib
6
[2601]7open Proper
8
9open PositiveMap
10
11open Deqsets
12
[2649]13open ErrorMessages
14
[2601]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
119(** val block_DeqSet : Deqsets.deqSet **)
120let block_DeqSet =
121  Obj.magic Pointers.eq_block
122
123(** val mem_assoc_env :
124    AST.ident -> (AST.ident, Csyntax.type0) Types.prod List.list -> Bool.bool **)
125let rec mem_assoc_env i = function
126| List.Nil -> Bool.False
127| List.Cons (hd0, tl) ->
128  let { Types.fst = id; Types.snd = ty } = hd0 in
[2649]129  (match Identifiers.identifier_eq PreIdentifiers.SymbolTag i id with
[2601]130   | Types.Inl _ -> Bool.True
131   | Types.Inr _ -> mem_assoc_env i tl)
132
133type 'a lset = 'a List.list
134
135(** val empty_lset : 'a1 List.list **)
136let empty_lset =
137  List.Nil
138
139(** val lset_union : 'a1 lset -> 'a1 lset -> 'a1 List.list **)
140let lset_union l1 l2 =
141  List.append l1 l2
142
143(** val lset_remove : Deqsets.deqSet -> __ lset -> __ -> __ List.list **)
144let lset_remove a l elt =
145  List.filter (fun x -> Bool.notb (Deqsets.eqb a x elt)) l
146
147(** val lset_difference :
148    Deqsets.deqSet -> __ lset -> __ lset -> __ List.list **)
149let lset_difference a l1 l2 =
150  List.filter (fun x -> Bool.notb (Listb.memb a x l2)) l1
151
152(** val wF_rect : ('a1 -> __ -> ('a1 -> __ -> 'a2) -> 'a2) -> 'a1 -> 'a2 **)
153let rec wF_rect f x =
154  f x __ (fun y _ -> wF_rect f y)
155
156(** val one_bv : Nat.nat -> BitVector.bitVector **)
157let one_bv n =
158  (Arithmetic.add_with_carries n (BitVector.zero n) (BitVector.zero n)
159    Bool.True).Types.fst
160
161(** val ith_carry :
162    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
163    Bool.bool **)
164let rec ith_carry n a b init =
165  (match n with
166   | Nat.O -> (fun x x0 -> init)
167   | Nat.S x ->
168     (fun a' b' ->
169       let hd_a = Vector.head' x a' in
170       let hd_b = Vector.head' x b' in
171       let tl_a = Vector.tail0 x a' in
172       let tl_b = Vector.tail0 x b' in
173       Arithmetic.carry_of hd_a hd_b (ith_carry x tl_a tl_b init))) a b
174
175(** val ith_bit :
176    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
177    Bool.bool **)
178let ith_bit n a b init =
179  (match n with
180   | Nat.O -> (fun x x0 -> init)
181   | Nat.S x ->
182     (fun a' b' ->
183       let hd_a = Vector.head' x a' in
184       let hd_b = Vector.head' x b' in
185       let tl_a = Vector.tail0 x a' in
186       let tl_b = Vector.tail0 x b' in
187       Bool.xorb (Bool.xorb hd_a hd_b) (ith_carry x tl_a tl_b init))) a b
188
189(** val bitvector_fold :
190    Nat.nat -> BitVector.bitVector -> (Nat.nat -> BitVector.bitVector ->
191    Bool.bool) -> BitVector.bitVector **)
192let rec bitvector_fold n v f =
193  match v with
194  | Vector.VEmpty -> Vector.VEmpty
195  | Vector.VCons (sz, elt, tl) ->
196    let bit0 = f n v in Vector.VCons (sz, bit0, (bitvector_fold sz tl f))
197
198(** val bitvector_fold2 :
199    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (Nat.nat ->
200    BitVector.bitVector -> BitVector.bitVector -> Bool.bool) ->
201    BitVector.bitVector **)
202let rec bitvector_fold2 n v1 v2 f =
203  (match v1 with
204   | Vector.VEmpty -> (fun x -> Vector.VEmpty)
205   | Vector.VCons (sz, elt, tl) ->
206     (fun v2' ->
207       let bit0 = f n v1 v2 in
208       Vector.VCons (sz, bit0,
209       (bitvector_fold2 sz tl (Vector.tail0 sz v2') f)))) v2
210
211(** val addition_n_direct :
212    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
213    BitVector.bitVector **)
214let addition_n_direct n v1 v2 init =
215  bitvector_fold2 n v1 v2 (fun n0 v10 v20 -> ith_bit n0 v10 v20 init)
216
217(** val increment_direct :
218    Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
219let increment_direct n v =
220  addition_n_direct n v (one_bv n) Bool.False
221
222(** val twocomp_neg_direct :
223    Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
224let twocomp_neg_direct n v =
225  increment_direct n (BitVector.negation_bv n v)
226
227(** val andb_fold : Nat.nat -> BitVector.bitVector -> Bool.bool **)
228let rec andb_fold n = function
229| Vector.VEmpty -> Bool.True
230| Vector.VCons (sz, elt, tl) -> Bool.andb elt (andb_fold sz tl)
231
Note: See TracBrowser for help on using the repository browser.