Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  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:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/frontend_misc.ml

    r2717 r2773  
    11open Preamble
    22
    3 open BitVectorTrie
    4 
    53open CostLabel
    64
     
    2119open Extralib
    2220
     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
    2347open Setoids
    2448
     
    2650
    2751open Option
    28 
    29 open Lists
    30 
    31 open Positive
    32 
    33 open Identifiers
    34 
    35 open Exp
    36 
    37 open Arithmetic
    38 
    39 open Vector
    40 
    41 open Div_and_mod
    42 
    43 open Jmeq
    44 
    45 open Russell
    46 
    47 open List
    48 
    49 open Util
    50 
    51 open FoldStuff
    52 
    53 open BitVector
    5452
    5553open Extranat
     
    129127let rec mem_assoc_env i = function
    130128| List.Nil -> Bool.False
    131 | List.Cons (hd0, tl) ->
    132   let { Types.fst = id; Types.snd = ty } = hd0 in
     129| List.Cons (hd, tl) ->
     130  let { Types.fst = id; Types.snd = ty } = hd in
    133131  (match Identifiers.identifier_eq PreIdentifiers.SymbolTag i id with
    134132   | Types.Inl _ -> Bool.True
     
    173171       let hd_a = Vector.head' x a' in
    174172       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
     173       let tl_a = Vector.tail x a' in
     174       let tl_b = Vector.tail x b' in
    177175       Arithmetic.carry_of hd_a hd_b (ith_carry x tl_a tl_b init))) a b
    178176
     
    187185       let hd_a = Vector.head' x a' in
    188186       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
     187       let tl_a = Vector.tail x a' in
     188       let tl_b = Vector.tail x b' in
    191189       Bool.xorb (Bool.xorb hd_a hd_b) (ith_carry x tl_a tl_b init))) a b
    192190
     
    198196  | Vector.VEmpty -> Vector.VEmpty
    199197  | Vector.VCons (sz, elt, tl) ->
    200     let bit0 = f n v in Vector.VCons (sz, bit0, (bitvector_fold sz tl f))
     198    let bit = f n v in Vector.VCons (sz, bit, (bitvector_fold sz tl f))
    201199
    202200(** val bitvector_fold2 :
     
    209207   | Vector.VCons (sz, elt, tl) ->
    210208     (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
     209       let bit = f n v1 v2 in
     210       Vector.VCons (sz, bit, (bitvector_fold2 sz tl (Vector.tail sz v2') f))))
     211    v2
    214212
    215213(** val addition_n_direct :
Note: See TracChangeset for help on using the changeset viewer.