Changeset 2773 for extracted/vector.ml


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (8 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/vector.ml

    r2601 r2773  
    2626
    2727open Util
     28
     29open Setoids
     30
     31open Monad
     32
     33open Option
    2834
    2935open Extranat
     
    3642    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    3743    vector -> 'a2 **)
    38 let rec vector_rect_Type4 h_VEmpty h_VCons x_1062 = function
     44let rec vector_rect_Type4 h_VEmpty h_VCons x_1761 = function
    3945| VEmpty -> h_VEmpty
    40 | VCons (n, x_1065, x_1064) ->
    41   h_VCons n x_1065 x_1064 (vector_rect_Type4 h_VEmpty h_VCons n x_1064)
     46| VCons (n, x_1764, x_1763) ->
     47  h_VCons n x_1764 x_1763 (vector_rect_Type4 h_VEmpty h_VCons n x_1763)
    4248
    4349(** val vector_rect_Type3 :
    4450    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    4551    vector -> 'a2 **)
    46 let rec vector_rect_Type3 h_VEmpty h_VCons x_1074 = function
     52let rec vector_rect_Type3 h_VEmpty h_VCons x_1773 = function
    4753| VEmpty -> h_VEmpty
    48 | VCons (n, x_1077, x_1076) ->
    49   h_VCons n x_1077 x_1076 (vector_rect_Type3 h_VEmpty h_VCons n x_1076)
     54| VCons (n, x_1776, x_1775) ->
     55  h_VCons n x_1776 x_1775 (vector_rect_Type3 h_VEmpty h_VCons n x_1775)
    5056
    5157(** val vector_rect_Type2 :
    5258    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    5359    vector -> 'a2 **)
    54 let rec vector_rect_Type2 h_VEmpty h_VCons x_1080 = function
     60let rec vector_rect_Type2 h_VEmpty h_VCons x_1779 = function
    5561| VEmpty -> h_VEmpty
    56 | VCons (n, x_1083, x_1082) ->
    57   h_VCons n x_1083 x_1082 (vector_rect_Type2 h_VEmpty h_VCons n x_1082)
     62| VCons (n, x_1782, x_1781) ->
     63  h_VCons n x_1782 x_1781 (vector_rect_Type2 h_VEmpty h_VCons n x_1781)
    5864
    5965(** val vector_rect_Type1 :
    6066    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    6167    vector -> 'a2 **)
    62 let rec vector_rect_Type1 h_VEmpty h_VCons x_1086 = function
     68let rec vector_rect_Type1 h_VEmpty h_VCons x_1785 = function
    6369| VEmpty -> h_VEmpty
    64 | VCons (n, x_1089, x_1088) ->
    65   h_VCons n x_1089 x_1088 (vector_rect_Type1 h_VEmpty h_VCons n x_1088)
     70| VCons (n, x_1788, x_1787) ->
     71  h_VCons n x_1788 x_1787 (vector_rect_Type1 h_VEmpty h_VCons n x_1787)
    6672
    6773(** val vector_rect_Type0 :
    6874    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    6975    vector -> 'a2 **)
    70 let rec vector_rect_Type0 h_VEmpty h_VCons x_1092 = function
     76let rec vector_rect_Type0 h_VEmpty h_VCons x_1791 = function
    7177| VEmpty -> h_VEmpty
    72 | VCons (n, x_1095, x_1094) ->
    73   h_VCons n x_1095 x_1094 (vector_rect_Type0 h_VEmpty h_VCons n x_1094)
     78| VCons (n, x_1794, x_1793) ->
     79  h_VCons n x_1794 x_1793 (vector_rect_Type0 h_VEmpty h_VCons n x_1793)
    7480
    7581(** val vector_inv_rect_Type4 :
     
    123129     (match v with
    124130      | VEmpty -> (fun _ -> assert false (* absurd case *))
    125       | VCons (p, hd0, tl) -> (fun _ -> hd0))
     131      | VCons (p, hd, tl) -> (fun _ -> hd))
    126132   | Nat.S o ->
    127133     (match v with
    128134      | VEmpty -> (fun _ -> assert false (* absurd case *))
    129       | VCons (p, hd0, tl) -> (fun _ -> get_index_v p tl o))) __
     135      | VCons (p, hd, tl) -> (fun _ -> get_index_v p tl o))) __
    130136
    131137(** val get_index' : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 **)
     
    139145  (match v with
    140146   | VEmpty -> Types.None
    141    | VCons (p, hd0, tl) -> Types.Some hd0)
     147   | VCons (p, hd, tl) -> Types.Some hd)
    142148| Nat.S o ->
    143149  (match v with
    144150   | VEmpty -> Types.None
    145    | VCons (p, hd0, tl) -> get_index_weak_v p tl o)
     151   | VCons (p, hd, tl) -> get_index_weak_v p tl o)
    146152
    147153(** val set_index : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector **)
     
    151157     (match v with
    152158      | VEmpty -> (fun _ -> VEmpty)
    153       | VCons (p, hd0, tl) -> (fun _ -> VCons (p, a, tl)))
     159      | VCons (p, hd, tl) -> (fun _ -> VCons (p, a, tl)))
    154160   | Nat.S o ->
    155161     (match v with
    156162      | VEmpty -> (fun _ -> VEmpty)
    157       | VCons (p, hd0, tl) -> (fun _ -> VCons (p, hd0, (set_index p tl o a)))))
     163      | VCons (p, hd, tl) -> (fun _ -> VCons (p, hd, (set_index p tl o a)))))
    158164    __
    159165
     
    165171    (match v with
    166172     | VEmpty -> Types.None
    167      | VCons (o, hd0, tl) -> Types.Some v)
     173     | VCons (o, hd, tl) -> Types.Some v)
    168174  | Nat.S o ->
    169175    (match v with
    170176     | VEmpty -> Types.None
    171      | VCons (p, hd0, tl) ->
     177     | VCons (p, hd, tl) ->
    172178       let settail = set_index_weak p tl o a in
    173179       (match settail with
     
    175181        | Types.Some j -> Types.Some v))
    176182
    177 (** val drop0 :
     183(** val drop :
    178184    Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 vector Types.option **)
    179 let rec drop0 n v = function
     185let rec drop n v = function
    180186| Nat.O -> Types.Some v
    181187| Nat.S o ->
    182188  (match v with
    183189   | VEmpty -> Types.None
    184    | VCons (p, hd0, tl) -> Types.None)
     190   | VCons (p, hd, tl) -> Types.None)
    185191
    186192(** val head' : Nat.nat -> 'a1 vector -> 'a1 **)
    187193let head' n = function
    188194| VEmpty -> Obj.magic __
    189 | VCons (x, hd0, x0) -> hd0
    190 
    191 (** val tail0 : Nat.nat -> 'a1 vector -> 'a1 vector **)
    192 let tail0 n = function
     195| VCons (x, hd, x0) -> hd
     196
     197(** val tail : Nat.nat -> 'a1 vector -> 'a1 vector **)
     198let tail n = function
    193199| VEmpty -> Obj.magic __
    194 | VCons (m, hd0, tl) -> tl
     200| VCons (m, hd, tl) -> tl
    195201
    196202(** val vsplit' :
     
    202208    (fun v ->
    203209      let { Types.fst = l; Types.snd = r } =
    204         vsplit' m' n (tail0 (Nat.plus m' n) v)
     210        vsplit' m' n (tail (Nat.plus m' n) v)
    205211      in
    206212      { Types.fst = (VCons (m', (head' (Nat.plus m' n) v), l)); Types.snd =
     
    226232let rec fold_right n f x = function
    227233| VEmpty -> x
    228 | VCons (n0, hd0, tl) -> f hd0 (fold_right n0 f x tl)
     234| VCons (n0, hd, tl) -> f hd (fold_right n0 f x tl)
    229235
    230236(** val fold_right_i :
     
    232238let rec fold_right_i n f x = function
    233239| VEmpty -> x
    234 | VCons (n0, hd0, tl) -> f n0 hd0 (fold_right_i n0 f x tl)
     240| VCons (n0, hd, tl) -> f n0 hd (fold_right_i n0 f x tl)
    235241
    236242(** val fold_right2_i :
     
    242248     (match q with
    243249      | VEmpty -> (fun _ -> c)
    244       | VCons (o, hd0, tl) -> (fun _ -> assert false (* absurd case *)))
    245    | VCons (o, hd0, tl) ->
     250      | VCons (o, hd, tl) -> (fun _ -> assert false (* absurd case *)))
     251   | VCons (o, hd, tl) ->
    246252     (match q with
    247253      | VEmpty -> (fun _ -> assert false (* absurd case *))
    248254      | VCons (p, hd', tl') ->
    249         (fun _ -> f o hd0 hd' (fold_right2_i f c o tl tl')))) __
     255        (fun _ -> f o hd hd' (fold_right2_i f c o tl tl')))) __
    250256
    251257(** val fold_left :
     
    253259let rec fold_left n f x = function
    254260| VEmpty -> x
    255 | VCons (n0, hd0, tl) -> fold_left n0 f (f x hd0) tl
    256 
    257 (** val map0 : Nat.nat -> ('a1 -> 'a2) -> 'a1 vector -> 'a2 vector **)
    258 let rec map0 n f = function
     261| VCons (n0, hd, tl) -> fold_left n0 f (f x hd) tl
     262
     263(** val map : Nat.nat -> ('a1 -> 'a2) -> 'a1 vector -> 'a2 vector **)
     264let rec map n f = function
    259265| VEmpty -> VEmpty
    260 | VCons (n0, hd0, tl) -> VCons (n0, (f hd0), (map0 n0 f tl))
     266| VCons (n0, hd, tl) -> VCons (n0, (f hd), (map n0 f tl))
    261267
    262268(** val zip_with :
     
    265271  (match v with
    266272   | VEmpty -> (fun _ -> VEmpty)
    267    | VCons (n0, hd0, tl) ->
     273   | VCons (n0, hd, tl) ->
    268274     (match q with
    269275      | VEmpty -> (fun _ -> Obj.magic Nat.nat_discr (Nat.S n0) Nat.O __)
    270276      | VCons (m, hd', tl') ->
    271         (fun _ -> VCons (n0, (f hd0 hd'),
    272           (zip_with n0 f tl (Util.eq_rect_Type0_r0 m tl' n0)))))) __
    273 
    274 (** val zip0 :
     277        (fun _ -> VCons (n0, (f hd hd'),
     278          (zip_with n0 f tl (Util.eq_rect_Type0_r m tl' n0)))))) __
     279
     280(** val zip :
    275281    Nat.nat -> 'a1 vector -> 'a2 vector -> ('a1, 'a2) Types.prod vector **)
    276 let zip0 n v q =
     282let zip n v q =
    277283  zip_with n (fun x x0 -> { Types.fst = x; Types.snd = x0 }) v q
    278284
     
    283289  | Nat.S m -> VCons (m, h, (replicate m h))
    284290
    285 (** val append0 :
     291(** val append :
    286292    Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector **)
    287 let rec append0 n m v q =
     293let rec append n m v q =
    288294  match v with
    289295  | VEmpty -> q
    290   | VCons (o, hd0, tl) -> VCons ((Nat.plus o m), hd0, (append0 o m tl q))
     296  | VCons (o, hd, tl) -> VCons ((Nat.plus o m), hd, (append o m tl q))
    291297
    292298(** val scan_left :
     
    296302    (match v with
    297303     | VEmpty -> VEmpty
    298      | VCons (o, hd0, tl) -> scan_left o f (f a hd0) tl))
     304     | VCons (o, hd, tl) -> scan_left o f (f a hd) tl))
    299305
    300306(** val scan_right :
     
    302308let rec scan_right n f b = function
    303309| VEmpty -> List.Nil
    304 | VCons (o, hd0, tl) -> List.Cons ((f hd0 b), (scan_right o f b tl))
     310| VCons (o, hd, tl) -> List.Cons ((f hd b), (scan_right o f b tl))
    305311
    306312(** val revapp :
     
    309315  match v with
    310316  | VEmpty -> acc
    311   | VCons (o, hd0, tl) -> revapp o (Nat.S m) tl (VCons (m, hd0, acc))
    312 
    313 (** val reverse0 : Nat.nat -> 'a1 vector -> 'a1 vector **)
    314 let rec reverse0 n v =
     317  | VCons (o, hd, tl) -> revapp o (Nat.S m) tl (VCons (m, hd, acc))
     318
     319(** val reverse : Nat.nat -> 'a1 vector -> 'a1 vector **)
     320let rec reverse n v =
    315321  revapp n Nat.O v VEmpty
    316322
     
    325331let rec list_of_vector n = function
    326332| VEmpty -> List.Nil
    327 | VCons (o, hd0, tl) -> List.Cons (hd0, (list_of_vector o tl))
     333| VCons (o, hd, tl) -> List.Cons (hd, (list_of_vector o tl))
    328334
    329335(** val vector_of_list : 'a1 List.list -> 'a1 vector **)
    330336let rec vector_of_list = function
    331337| List.Nil -> VEmpty
    332 | List.Cons (hd0, tl) -> VCons ((List.length tl), hd0, (vector_of_list tl))
     338| List.Cons (hd, tl) -> VCons ((List.length tl), hd, (vector_of_list tl))
    333339
    334340(** val rotate_left : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
     
    339345    (match v with
    340346     | VEmpty -> VEmpty
    341      | VCons (p, hd0, tl) ->
     347     | VCons (p, hd, tl) ->
    342348       rotate_left (Nat.S p) o
    343          (append0 p (Nat.S Nat.O) tl (VCons (Nat.O, hd0, VEmpty))))
     349         (append p (Nat.S Nat.O) tl (VCons (Nat.O, hd, VEmpty))))
    344350
    345351(** val rotate_right : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
    346352let rotate_right n m v =
    347   reverse0 n (rotate_left n m (reverse0 n v))
     353  reverse n (rotate_left n m (reverse n v))
    348354
    349355(** val shift_left_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector **)
     
    351357  (match v with
    352358   | VEmpty -> (fun _ -> assert false (* absurd case *))
    353    | VCons (o, hd0, tl) ->
    354      (fun _ -> reverse0 (Nat.S o) (VCons (o, a, (reverse0 o tl))))) __
     359   | VCons (o, hd, tl) ->
     360     (fun _ -> reverse (Nat.S o) (VCons (o, a, (reverse o tl))))) __
    355361
    356362(** val switch_bv_plus : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector **)
     
    374380    (fun v a ->
    375381      let { Types.fst = v0; Types.snd = v' } = vsplit m0 (Nat.S d) v in
    376       switch_bv_plus (Nat.S d) m0 (append0 (Nat.S d) m0 v' (replicate m0 a)))
     382      switch_bv_plus (Nat.S d) m0 (append (Nat.S d) m0 v' (replicate m0 a)))
    377383
    378384(** val shift_right :
     
    391397       | VEmpty -> Bool.True
    392398       | VCons (x, x0, x1) -> Obj.magic __ x x0 x1)
    393    | VCons (m, hd0, tl) ->
    394      (fun c0 -> Bool.andb (f hd0 (head' m c0)) (eq_v m f tl (tail0 m c0)))) c
     399   | VCons (m, hd, tl) ->
     400     (fun c0 -> Bool.andb (f hd (head' m c0)) (eq_v m f tl (tail m c0)))) c
    395401
    396402(** val vector_inv_n : Nat.nat -> 'a1 vector -> __ **)
     
    411417    Obj.magic vector_inv_n (Nat.S m) y (fun h' t' ht hf ->
    412418      Obj.magic f_elim __ h h' (fun _ ->
    413         iH (tail0 m (VCons (m, h', t'))) (fun _ -> ht __) (fun _ -> hf __))
     419        iH (tail m (VCons (m, h', t'))) (fun _ -> ht __) (fun _ -> hf __))
    414420        (fun _ -> hf __))) n x
    415421
    416 (** val mem0 :
     422(** val mem :
    417423    ('a1 -> 'a1 -> Bool.bool) -> Nat.nat -> 'a1 vector -> 'a1 -> Bool.bool **)
    418 let mem0 eq_a n l x =
     424let mem eq_a n l x =
    419425  fold_right n (fun y v -> Bool.orb (eq_a x y) v) Bool.False l
    420426
     
    425431  match sub with
    426432  | VEmpty -> Bool.True
    427   | VCons (n', hd0, tl) ->
    428     (match mem0 eq m sup hd0 with
     433  | VCons (n', hd, tl) ->
     434    (match mem eq m sup hd with
    429435     | Bool.True -> subvector_with n' m eq tl sup
    430436     | Bool.False -> Bool.False)
     
    468474let rec vflatten n m = function
    469475| VEmpty -> VEmpty
    470 | VCons (n', hd0, tl) -> append0 m (Nat.times n' m) hd0 (vflatten n' m tl)
    471 
     476| VCons (n', hd, tl) -> append m (Nat.times n' m) hd (vflatten n' m tl)
     477
Note: See TracChangeset for help on using the changeset viewer.