source: driver/extracted/frontend_misc.ml @ 3106

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

Everything extracted again.

File size: 6.1 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
121(** val typ_eq_dec : AST.typ -> AST.typ -> (__, __) Types.sum **)
122let typ_eq_dec t1 t2 =
123  match t1 with
124  | AST.ASTint (x, x0) ->
125    (match t2 with
126     | AST.ASTint (sz, sg) ->
127       (fun sz' sg' ->
128         match sz with
129         | AST.I8 ->
130           (match sz' with
131            | AST.I8 ->
132              AST.typ_eq (AST.ASTint (AST.I8, sg')) (AST.ASTint (AST.I8, sg))
133            | AST.I16 ->
134              AST.typ_eq (AST.ASTint (AST.I16, sg')) (AST.ASTint (AST.I8,
135                sg))
136            | AST.I32 ->
137              AST.typ_eq (AST.ASTint (AST.I32, sg')) (AST.ASTint (AST.I8,
138                sg)))
139         | AST.I16 ->
140           (match sz' with
141            | AST.I8 ->
142              AST.typ_eq (AST.ASTint (AST.I8, sg')) (AST.ASTint (AST.I16,
143                sg))
144            | AST.I16 ->
145              AST.typ_eq (AST.ASTint (AST.I16, sg')) (AST.ASTint (AST.I16,
146                sg))
147            | AST.I32 ->
148              AST.typ_eq (AST.ASTint (AST.I32, sg')) (AST.ASTint (AST.I16,
149                sg)))
150         | AST.I32 ->
151           (match sz' with
152            | AST.I8 ->
153              AST.typ_eq (AST.ASTint (AST.I8, sg')) (AST.ASTint (AST.I32,
154                sg))
155            | AST.I16 ->
156              AST.typ_eq (AST.ASTint (AST.I16, sg')) (AST.ASTint (AST.I32,
157                sg))
158            | AST.I32 ->
159              AST.typ_eq (AST.ASTint (AST.I32, sg')) (AST.ASTint (AST.I32,
160                sg))))
161     | AST.ASTptr -> (fun sz sg -> Types.Inr __)) x x0
162  | AST.ASTptr ->
163    (match t2 with
164     | AST.ASTint (sz, sg) -> Types.Inr __
165     | AST.ASTptr -> Types.Inl __)
166
167(** val block_DeqSet : Deqsets.deqSet **)
168let block_DeqSet =
169  Obj.magic Pointers.eq_block
170
171(** val mem_assoc_env :
172    AST.ident -> (AST.ident, Csyntax.type0) Types.prod List.list -> Bool.bool **)
173let rec mem_assoc_env i = function
174| List.Nil -> Bool.False
175| List.Cons (hd, tl) ->
176  let { Types.fst = id; Types.snd = ty } = hd in
177  (match Identifiers.identifier_eq PreIdentifiers.SymbolTag i id with
178   | Types.Inl _ -> Bool.True
179   | Types.Inr _ -> mem_assoc_env i tl)
180
181type 'a lset = 'a List.list
182
183(** val empty_lset : 'a1 List.list **)
184let empty_lset =
185  List.Nil
186
187(** val lset_union : 'a1 lset -> 'a1 lset -> 'a1 List.list **)
188let lset_union l1 l2 =
189  List.append l1 l2
190
191(** val lset_remove : Deqsets.deqSet -> __ lset -> __ -> __ List.list **)
192let lset_remove a l elt =
193  List.filter (fun x -> Bool.notb (Deqsets.eqb a x elt)) l
194
195(** val lset_difference :
196    Deqsets.deqSet -> __ lset -> __ lset -> __ List.list **)
197let lset_difference a l1 l2 =
198  List.filter (fun x -> Bool.notb (Listb.memb a x l2)) l1
199
200(** val wF_rect : ('a1 -> __ -> ('a1 -> __ -> 'a2) -> 'a2) -> 'a1 -> 'a2 **)
201let rec wF_rect f x =
202  f x __ (fun y _ -> wF_rect f y)
203
204(** val one_bv : Nat.nat -> BitVector.bitVector **)
205let one_bv n =
206  (Arithmetic.add_with_carries n (BitVector.zero n) (BitVector.zero n)
207    Bool.True).Types.fst
208
209(** val ith_carry :
210    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
211    Bool.bool **)
212let rec ith_carry n a b init =
213  (match n with
214   | Nat.O -> (fun x x0 -> init)
215   | Nat.S x ->
216     (fun a' b' ->
217       let hd_a = Vector.head' x a' in
218       let hd_b = Vector.head' x b' in
219       let tl_a = Vector.tail x a' in
220       let tl_b = Vector.tail x b' in
221       Arithmetic.carry_of hd_a hd_b (ith_carry x tl_a tl_b init))) a b
222
223(** val ith_bit :
224    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
225    Bool.bool **)
226let ith_bit n a b init =
227  (match n with
228   | Nat.O -> (fun x x0 -> init)
229   | Nat.S x ->
230     (fun a' b' ->
231       let hd_a = Vector.head' x a' in
232       let hd_b = Vector.head' x b' in
233       let tl_a = Vector.tail x a' in
234       let tl_b = Vector.tail x b' in
235       Bool.xorb (Bool.xorb hd_a hd_b) (ith_carry x tl_a tl_b init))) a b
236
237(** val bitvector_fold :
238    Nat.nat -> BitVector.bitVector -> (Nat.nat -> BitVector.bitVector ->
239    Bool.bool) -> BitVector.bitVector **)
240let rec bitvector_fold n v f =
241  match v with
242  | Vector.VEmpty -> Vector.VEmpty
243  | Vector.VCons (sz, elt, tl) ->
244    let bit = f n v in Vector.VCons (sz, bit, (bitvector_fold sz tl f))
245
246(** val bitvector_fold2 :
247    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (Nat.nat ->
248    BitVector.bitVector -> BitVector.bitVector -> Bool.bool) ->
249    BitVector.bitVector **)
250let rec bitvector_fold2 n v1 v2 f =
251  (match v1 with
252   | Vector.VEmpty -> (fun x -> Vector.VEmpty)
253   | Vector.VCons (sz, elt, tl) ->
254     (fun v2' ->
255       let bit = f n v1 v2 in
256       Vector.VCons (sz, bit, (bitvector_fold2 sz tl (Vector.tail sz v2') f))))
257    v2
258
259(** val addition_n_direct :
260    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
261    BitVector.bitVector **)
262let addition_n_direct n v1 v2 init =
263  bitvector_fold2 n v1 v2 (fun n0 v10 v20 -> ith_bit n0 v10 v20 init)
264
265(** val increment_direct :
266    Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
267let increment_direct n v =
268  addition_n_direct n v (one_bv n) Bool.False
269
270(** val twocomp_neg_direct :
271    Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
272let twocomp_neg_direct n v =
273  increment_direct n (BitVector.negation_bv n v)
274
275(** val andb_fold : Nat.nat -> BitVector.bitVector -> Bool.bool **)
276let rec andb_fold n = function
277| Vector.VEmpty -> Bool.True
278| Vector.VCons (sz, elt, tl) -> Bool.andb elt (andb_fold sz tl)
279
Note: See TracBrowser for help on using the repository browser.