source: extracted/frontend_misc.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 8 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 4.5 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 block_DeqSet : Deqsets.deqSet **)
122let block_DeqSet =
123  Obj.magic Pointers.eq_block
124
125(** val mem_assoc_env :
126    AST.ident -> (AST.ident, Csyntax.type0) Types.prod List.list -> Bool.bool **)
127let rec mem_assoc_env i = function
128| List.Nil -> Bool.False
129| List.Cons (hd, tl) ->
130  let { Types.fst = id; Types.snd = ty } = hd in
131  (match Identifiers.identifier_eq PreIdentifiers.SymbolTag i id with
132   | Types.Inl _ -> Bool.True
133   | Types.Inr _ -> mem_assoc_env i tl)
134
135type 'a lset = 'a List.list
136
137(** val empty_lset : 'a1 List.list **)
138let empty_lset =
139  List.Nil
140
141(** val lset_union : 'a1 lset -> 'a1 lset -> 'a1 List.list **)
142let lset_union l1 l2 =
143  List.append l1 l2
144
145(** val lset_remove : Deqsets.deqSet -> __ lset -> __ -> __ List.list **)
146let lset_remove a l elt =
147  List.filter (fun x -> Bool.notb (Deqsets.eqb a x elt)) l
148
149(** val lset_difference :
150    Deqsets.deqSet -> __ lset -> __ lset -> __ List.list **)
151let lset_difference a l1 l2 =
152  List.filter (fun x -> Bool.notb (Listb.memb a x l2)) l1
153
154(** val wF_rect : ('a1 -> __ -> ('a1 -> __ -> 'a2) -> 'a2) -> 'a1 -> 'a2 **)
155let rec wF_rect f x =
156  f x __ (fun y _ -> wF_rect f y)
157
158(** val one_bv : Nat.nat -> BitVector.bitVector **)
159let one_bv n =
160  (Arithmetic.add_with_carries n (BitVector.zero n) (BitVector.zero n)
161    Bool.True).Types.fst
162
163(** val ith_carry :
164    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
165    Bool.bool **)
166let rec ith_carry n a b init =
167  (match n with
168   | Nat.O -> (fun x x0 -> init)
169   | Nat.S x ->
170     (fun a' b' ->
171       let hd_a = Vector.head' x a' in
172       let hd_b = Vector.head' x b' in
173       let tl_a = Vector.tail x a' in
174       let tl_b = Vector.tail x b' in
175       Arithmetic.carry_of hd_a hd_b (ith_carry x tl_a tl_b init))) a b
176
177(** val ith_bit :
178    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
179    Bool.bool **)
180let ith_bit n a b init =
181  (match n with
182   | Nat.O -> (fun x x0 -> init)
183   | Nat.S x ->
184     (fun a' b' ->
185       let hd_a = Vector.head' x a' in
186       let hd_b = Vector.head' x b' in
187       let tl_a = Vector.tail x a' in
188       let tl_b = Vector.tail x b' in
189       Bool.xorb (Bool.xorb hd_a hd_b) (ith_carry x tl_a tl_b init))) a b
190
191(** val bitvector_fold :
192    Nat.nat -> BitVector.bitVector -> (Nat.nat -> BitVector.bitVector ->
193    Bool.bool) -> BitVector.bitVector **)
194let rec bitvector_fold n v f =
195  match v with
196  | Vector.VEmpty -> Vector.VEmpty
197  | Vector.VCons (sz, elt, tl) ->
198    let bit = f n v in Vector.VCons (sz, bit, (bitvector_fold sz tl f))
199
200(** val bitvector_fold2 :
201    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (Nat.nat ->
202    BitVector.bitVector -> BitVector.bitVector -> Bool.bool) ->
203    BitVector.bitVector **)
204let rec bitvector_fold2 n v1 v2 f =
205  (match v1 with
206   | Vector.VEmpty -> (fun x -> Vector.VEmpty)
207   | Vector.VCons (sz, elt, tl) ->
208     (fun v2' ->
209       let bit = f n v1 v2 in
210       Vector.VCons (sz, bit, (bitvector_fold2 sz tl (Vector.tail sz v2') f))))
211    v2
212
213(** val addition_n_direct :
214    Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
215    BitVector.bitVector **)
216let addition_n_direct n v1 v2 init =
217  bitvector_fold2 n v1 v2 (fun n0 v10 v20 -> ith_bit n0 v10 v20 init)
218
219(** val increment_direct :
220    Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
221let increment_direct n v =
222  addition_n_direct n v (one_bv n) Bool.False
223
224(** val twocomp_neg_direct :
225    Nat.nat -> BitVector.bitVector -> BitVector.bitVector **)
226let twocomp_neg_direct n v =
227  increment_direct n (BitVector.negation_bv n v)
228
229(** val andb_fold : Nat.nat -> BitVector.bitVector -> Bool.bool **)
230let rec andb_fold n = function
231| Vector.VEmpty -> Bool.True
232| Vector.VCons (sz, elt, tl) -> Bool.andb elt (andb_fold sz tl)
233
Note: See TracBrowser for help on using the repository browser.