source: extracted/frontend_misc.ml @ 2746

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 4.6 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open CostLabel
6
7open Coqlib
8
9open Proper
10
11open PositiveMap
12
13open Deqsets
14
15open ErrorMessages
16
17open PreIdentifiers
18
19open Errors
20
21open Extralib
22
23open Setoids
24
25open Monad
26
27open Option
28
29open Lists
30
31open Positive
32
33open Identifiers
34
35open Exp
36
37open Arithmetic
38
39open Vector
40
41open Div_and_mod
42
43open Jmeq
44
45open Russell
46
47open List
48
49open Util
50
51open FoldStuff
52
53open BitVector
54
55open Extranat
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Integers
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Types
74
75open AST
76
77open Csyntax
78
79open TypeComparison
80
81open ClassifyOp
82
83open Events
84
85open Smallstep
86
87open Extra_bool
88
89open Values
90
91open FrontEndVal
92
93open Hide
94
95open ByteValues
96
97open Division
98
99open Z
100
101open BitVectorZ
102
103open Pointers
104
105open GenMem
106
107open FrontEndMem
108
109open Globalenvs
110
111open Csem
112
113open Star
114
115open IOMonad
116
117open IO
118
119open Sets
120
121open Listb
122
123(** val block_DeqSet : Deqsets.deqSet **)
124let block_DeqSet =
125  Obj.magic Pointers.eq_block
126
127(** val mem_assoc_env :
128    AST.ident -> (AST.ident, Csyntax.type0) Types.prod List.list -> Bool.bool **)
129let rec mem_assoc_env i = function
130| List.Nil -> Bool.False
131| List.Cons (hd0, tl) ->
132  let { Types.fst = id; Types.snd = ty } = hd0 in
133  (match Identifiers.identifier_eq PreIdentifiers.SymbolTag i id with
134   | Types.Inl _ -> Bool.True
135   | Types.Inr _ -> mem_assoc_env i tl)
136
137type 'a lset = 'a List.list
138
139(** val empty_lset : 'a1 List.list **)
140let empty_lset =
141  List.Nil
142
143(** val lset_union : 'a1 lset -> 'a1 lset -> 'a1 List.list **)
144let lset_union l1 l2 =
145  List.append l1 l2
146
147(** val lset_remove : Deqsets.deqSet -> __ lset -> __ -> __ List.list **)
148let lset_remove a l elt =
149  List.filter (fun x -> Bool.notb (Deqsets.eqb a x elt)) l
150
151(** val lset_difference :
152    Deqsets.deqSet -> __ lset -> __ lset -> __ List.list **)
153let lset_difference a l1 l2 =
154  List.filter (fun x -> Bool.notb (Listb.memb a x l2)) l1
155
156(** val wF_rect : ('a1 -> __ -> ('a1 -> __ -> 'a2) -> 'a2) -> 'a1 -> 'a2 **)
157let rec wF_rect f x =
158  f x __ (fun y _ -> wF_rect f y)
159
160(** val one_bv : Nat.nat -> BitVector.bitVector **)
161let one_bv n =
162  (Arithmetic.add_with_carries n (BitVector.zero n) (BitVector.zero n)
163    Bool.True).Types.fst
164
165(** val ith_carry :
166    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
167    Bool.bool **)
168let rec ith_carry n a b init =
169  (match n with
170   | Nat.O -> (fun x x0 -> init)
171   | Nat.S x ->
172     (fun a' b' ->
173       let hd_a = Vector.head' x a' in
174       let hd_b = Vector.head' x b' in
175       let tl_a = Vector.tail0 x a' in
176       let tl_b = Vector.tail0 x b' in
177       Arithmetic.carry_of hd_a hd_b (ith_carry x tl_a tl_b init))) a b
178
179(** val ith_bit :
180    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
181    Bool.bool **)
182let ith_bit n a b init =
183  (match n with
184   | Nat.O -> (fun x x0 -> init)
185   | Nat.S x ->
186     (fun a' b' ->
187       let hd_a = Vector.head' x a' in
188       let hd_b = Vector.head' x b' in
189       let tl_a = Vector.tail0 x a' in
190       let tl_b = Vector.tail0 x b' in
191       Bool.xorb (Bool.xorb hd_a hd_b) (ith_carry x tl_a tl_b init))) a b
192
193(** val bitvector_fold :
194    Nat.nat -> BitVector.bitVector -> (Nat.nat -> BitVector.bitVector ->
195    Bool.bool) -> BitVector.bitVector **)
196let rec bitvector_fold n v f =
197  match v with
198  | Vector.VEmpty -> Vector.VEmpty
199  | Vector.VCons (sz, elt, tl) ->
200    let bit0 = f n v in Vector.VCons (sz, bit0, (bitvector_fold sz tl f))
201
202(** val bitvector_fold2 :
203    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (Nat.nat ->
204    BitVector.bitVector -> BitVector.bitVector -> Bool.bool) ->
205    BitVector.bitVector **)
206let rec bitvector_fold2 n v1 v2 f =
207  (match v1 with
208   | Vector.VEmpty -> (fun x -> Vector.VEmpty)
209   | Vector.VCons (sz, elt, tl) ->
210     (fun v2' ->
211       let bit0 = f n v1 v2 in
212       Vector.VCons (sz, bit0,
213       (bitvector_fold2 sz tl (Vector.tail0 sz v2') f)))) v2
214
215(** val addition_n_direct :
216    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
217    BitVector.bitVector **)
218let addition_n_direct n v1 v2 init =
219  bitvector_fold2 n v1 v2 (fun n0 v10 v20 -> ith_bit n0 v10 v20 init)
220
221(** val increment_direct :
222    Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
223let increment_direct n v =
224  addition_n_direct n v (one_bv n) Bool.False
225
226(** val twocomp_neg_direct :
227    Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
228let twocomp_neg_direct n v =
229  increment_direct n (BitVector.negation_bv n v)
230
231(** val andb_fold : Nat.nat -> BitVector.bitVector -> Bool.bool **)
232let rec andb_fold n = function
233| Vector.VEmpty -> Bool.True
234| Vector.VCons (sz, elt, tl) -> Bool.andb elt (andb_fold sz tl)
235
Note: See TracBrowser for help on using the repository browser.