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/arithmetic.ml

    r2717 r2773  
    11open Preamble
     2
     3open Setoids
     4
     5open Monad
     6
     7open Option
    28
    39open Extranat
     
    6369  let p5 = Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) n2 Nat.O
    6470  in
    65   Vector.append0
     71  Vector.append
    6672    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S
    6773      (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    6874    (Nat.S Nat.O))))))))
    69     (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
    70       (Nat.S (Nat.S Nat.O)))) n1 (Vector.VCons ((Nat.S (Nat.S (Nat.S
    71       Nat.O))), p5, (Vector.VCons ((Nat.S (Nat.S Nat.O)), b1, (Vector.VCons
    72       ((Nat.S Nat.O), b2, (Vector.VCons (Nat.O, b3, Vector.VEmpty))))))))) b
     75    (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S (Nat.S
     76      (Nat.S Nat.O)))) n1 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), p5,
     77      (Vector.VCons ((Nat.S (Nat.S Nat.O)), b1, (Vector.VCons ((Nat.S Nat.O),
     78      b2, (Vector.VCons (Nat.O, b3, Vector.VEmpty))))))))) b
    7379
    7480(** val nat_of_bool : Bool.bool -> Nat.nat **)
     
    96102    (match last_carry with
    97103     | Bool.True ->
    98        let bit0 = Bool.xorb (Bool.xorb b c) Bool.True in
     104       let bit = Bool.xorb (Bool.xorb b c) Bool.True in
    99105       let carry = carry_of b c Bool.True in
    100        { Types.fst = (Vector.VCons (n0, bit0, lower_bits)); Types.snd =
     106       { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
    101107       (Vector.VCons (n0, carry, carries)) }
    102108     | Bool.False ->
    103        let bit0 = Bool.xorb (Bool.xorb b c) Bool.False in
     109       let bit = Bool.xorb (Bool.xorb b c) Bool.False in
    104110       let carry = carry_of b c Bool.False in
    105        { Types.fst = (Vector.VCons (n0, bit0, lower_bits)); Types.snd =
     111       { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
    106112       (Vector.VCons (n0, carry, carries)) })) { Types.fst = Vector.VEmpty;
    107113    Types.snd = Vector.VEmpty } n x y
     
    124130      | Vector.VCons (x0, bw, x1) -> bw
    125131    in
    126     let bit0 = Bool.xorb (Bool.xorb b c) last_borrow in
     132    let bit = Bool.xorb (Bool.xorb b c) last_borrow in
    127133    let borrow = borrow_of b c last_borrow in
    128     { Types.fst = (Vector.VCons (n0, bit0, lower_bits)); Types.snd =
     134    { Types.fst = (Vector.VCons (n0, bit, lower_bits)); Types.snd =
    129135    (Vector.VCons (n0, borrow, borrows)) }) { Types.fst = Vector.VEmpty;
    130136    Types.snd = Vector.VEmpty } n x y
     
    226232let rec nat_of_bitvector_aux n m = function
    227233| Vector.VEmpty -> m
    228 | Vector.VCons (n', hd0, tl) ->
     234| Vector.VCons (n', hd, tl) ->
    229235  nat_of_bitvector_aux n'
    230     (match hd0 with
     236    (match hd with
    231237     | Bool.True ->
    232238       Nat.plus (Nat.times (Nat.S (Nat.S Nat.O)) m) (Nat.S Nat.O)
     
    260266  match b with
    261267  | Vector.VEmpty -> acc
    262   | Vector.VCons (m', hd0, tl) ->
     268  | Vector.VCons (m', hd, tl) ->
    263269    let acc' =
    264       match hd0 with
     270      match hd with
    265271      | Bool.True -> addition_n (Nat.S n) c acc
    266272      | Bool.False -> acc
     
    291297(** val fbs_diff_rect_Type4 :
    292298    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    293 let rec fbs_diff_rect_Type4 h_fbs_diff' x_1137 = function
     299let rec fbs_diff_rect_Type4 h_fbs_diff' x_1836 = function
    294300| Fbs_diff' (n, m) -> h_fbs_diff' n m
    295301
    296302(** val fbs_diff_rect_Type5 :
    297303    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    298 let rec fbs_diff_rect_Type5 h_fbs_diff' x_1140 = function
     304let rec fbs_diff_rect_Type5 h_fbs_diff' x_1839 = function
    299305| Fbs_diff' (n, m) -> h_fbs_diff' n m
    300306
    301307(** val fbs_diff_rect_Type3 :
    302308    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    303 let rec fbs_diff_rect_Type3 h_fbs_diff' x_1143 = function
     309let rec fbs_diff_rect_Type3 h_fbs_diff' x_1842 = function
    304310| Fbs_diff' (n, m) -> h_fbs_diff' n m
    305311
    306312(** val fbs_diff_rect_Type2 :
    307313    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    308 let rec fbs_diff_rect_Type2 h_fbs_diff' x_1146 = function
     314let rec fbs_diff_rect_Type2 h_fbs_diff' x_1845 = function
    309315| Fbs_diff' (n, m) -> h_fbs_diff' n m
    310316
    311317(** val fbs_diff_rect_Type1 :
    312318    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    313 let rec fbs_diff_rect_Type1 h_fbs_diff' x_1149 = function
     319let rec fbs_diff_rect_Type1 h_fbs_diff' x_1848 = function
    314320| Fbs_diff' (n, m) -> h_fbs_diff' n m
    315321
    316322(** val fbs_diff_rect_Type0 :
    317323    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    318 let rec fbs_diff_rect_Type0 h_fbs_diff' x_1152 = function
     324let rec fbs_diff_rect_Type0 h_fbs_diff' x_1851 = function
    319325| Fbs_diff' (n, m) -> h_fbs_diff' n m
    320326
     
    378384        Bool.False
    379385    in
    380     let bit0 = Vector.head' n flags in
     386    let bit = Vector.head' n flags in
    381387    let q'' =
    382       match bit0 with
     388      match bit with
    383389      | Bool.True -> q'
    384390      | Bool.False -> q
     
    387393      divmod_u_aux n m' q'' (Vector.shift_right_1 n d Bool.False)
    388394    in
    389     { Types.fst = (Vector.VCons (m', bit0, tl)); Types.snd = md }
     395    { Types.fst = (Vector.VCons (m', bit, tl)); Types.snd = md }
    390396
    391397(** val divmod_u :
     
    668674       let xb = Vector.head' sz' b' in
    669675       let xc = Vector.head' sz' c' in
    670        let tlb = Vector.tail0 sz' b' in
    671        let tlc = Vector.tail0 sz' c' in
     676       let tlb = Vector.tail sz' b' in
     677       let tlc = Vector.tail sz' c' in
    672678       let { Types.fst = bits; Types.snd = last } =
    673679         canonical_add sz' tla tlb tlc init
    674680       in
    675        let { Types.fst = bit0; Types.snd = carry } =
     681       let { Types.fst = bit; Types.snd = carry } =
    676682         ternary_carry_of xa xb xc last
    677683       in
    678        { Types.fst = (Vector.VCons (sz', bit0, bits)); Types.snd = carry }))
    679     b c
     684       { Types.fst = (Vector.VCons (sz', bit, bits)); Types.snd = carry })) b
     685    c
    680686
    681687(** val carries_to_ternary : Bool.bool -> Bool.bool -> ternary **)
     
    756762      (Nat.S Nat.O)))))))) c (Nat.S Nat.O)
    757763  in
    758   Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     764  Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    759765    Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    760766    Nat.O)))))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
Note: See TracChangeset for help on using the changeset viewer.