Changeset 2773 for extracted/util.ml


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

    r2743 r2773  
    123123let rec forall f = function
    124124| List.Nil -> Bool.True
    125 | List.Cons (hd0, tl) -> Bool.andb (f hd0) (forall f tl)
     125| List.Cons (hd, tl) -> Bool.andb (f hd) (forall f tl)
    126126
    127127(** val prefix : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
    128128let rec prefix k = function
    129129| List.Nil -> List.Nil
    130 | List.Cons (hd0, tl) ->
     130| List.Cons (hd, tl) ->
    131131  (match k with
    132132   | Nat.O -> List.Nil
    133    | Nat.S k' -> List.Cons (hd0, (prefix k' tl)))
     133   | Nat.S k' -> List.Cons (hd, (prefix k' tl)))
    134134
    135135(** val fold_left2 :
     
    142142       (match right with
    143143        | List.Nil -> (fun _ -> accu)
    144         | List.Cons (hd0, tl) ->
     144        | List.Cons (hd, tl) ->
    145145          (fun _ ->
    146146            Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)) __)
    147    | List.Cons (hd0, tl) ->
     147   | List.Cons (hd, tl) ->
    148148     (fun _ ->
    149149       (match right with
     
    152152            Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
    153153        | List.Cons (hd', tl') ->
    154           (fun _ -> fold_left2 f (f accu hd0 hd') tl tl')) __)) __
     154          (fun _ -> fold_left2 f (f accu hd hd') tl tl')) __)) __
    155155
    156156(** val remove_n_first_internal :
     
    159159  match l with
    160160  | List.Nil -> List.Nil
    161   | List.Cons (hd0, tl) ->
     161  | List.Cons (hd, tl) ->
    162162    (match eq_nat i n with
    163163     | Bool.True -> l
     
    174174  match rem with
    175175  | List.Nil -> res
    176   | List.Cons (e0, tl) ->
     176  | List.Cons (e, tl) ->
    177177    (match geb i m with
    178178     | Bool.True -> res
    179      | Bool.False -> foldi_from_until_internal (Nat.S i) (f i res e0) tl m f)
     179     | Bool.False -> foldi_from_until_internal (Nat.S i) (f i res e) tl m f)
    180180
    181181(** val foldi_from_until :
     
    207207  (match l with
    208208   | List.Nil -> (fun _ -> assert false (* absurd case *))
    209    | List.Cons (hd0, tl) -> (fun _ -> hd0)) __
     209   | List.Cons (hd, tl) -> (fun _ -> hd)) __
    210210
    211211(** val tail_safe : 'a1 List.list -> 'a1 List.list **)
     
    213213  (match l with
    214214   | List.Nil -> (fun _ -> assert false (* absurd case *))
    215    | List.Cons (hd0, tl) -> (fun _ -> tl)) __
     215   | List.Cons (hd, tl) -> (fun _ -> tl)) __
    216216
    217217(** val safe_split :
     
    224224       (match l with
    225225        | List.Nil -> (fun _ -> assert false (* absurd case *))
    226         | List.Cons (hd0, tl) ->
     226        | List.Cons (hd, tl) ->
    227227          (fun _ ->
    228228            let { Types.fst = l1; Types.snd = l2 } = safe_split tl index' in
    229             { Types.fst = (List.Cons (hd0, l1)); Types.snd = l2 })) __)) __
     229            { Types.fst = (List.Cons (hd, l1)); Types.snd = l2 })) __)) __
    230230
    231231(** val nth_safe : Nat.nat -> 'a1 List.list -> 'a1 **)
     
    235235     (match the_list with
    236236      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
    237       | List.Cons (hd0, tl) -> (fun _ -> hd0))
     237      | List.Cons (hd, tl) -> (fun _ -> hd))
    238238   | Nat.S index' ->
    239239     (match the_list with
    240240      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
    241       | List.Cons (hd0, tl) -> (fun _ -> nth_safe index' tl))) __
     241      | List.Cons (hd, tl) -> (fun _ -> nth_safe index' tl))) __
    242242
    243243(** val last_safe : 'a1 List.list -> 'a1 **)
     
    253253    { Types.fst = { Types.fst = List.Nil; Types.snd = List.Nil }; Types.snd =
    254254      { Types.fst = List.Nil; Types.snd = right } }
    255   | List.Cons (hd0, tl) ->
     255  | List.Cons (hd, tl) ->
    256256    (match right with
    257257     | List.Nil ->
     
    262262       let { Types.fst = commonl; Types.snd = restl } = cleft in
    263263       let { Types.fst = commonr; Types.snd = restr } = cright in
    264        { Types.fst = { Types.fst = (List.Cons (hd0, commonl)); Types.snd =
     264       { Types.fst = { Types.fst = (List.Cons (hd, commonl)); Types.snd =
    265265       restl }; Types.snd = { Types.fst = (List.Cons (hd', commonr));
    266266       Types.snd = restr } })
     
    275275     (fun _ -> { Types.fst = { Types.fst = List.Nil; Types.snd = List.Nil };
    276276       Types.snd = { Types.fst = List.Nil; Types.snd = right } })
    277    | List.Cons (hd0, tl) ->
     277   | List.Cons (hd, tl) ->
    278278     (fun _ ->
    279279       (match right with
     
    290290            (fun _ ->
    291291            (let { Types.fst = commonr; Types.snd = restr } = cright in
    292             (fun _ -> { Types.fst = { Types.fst = (List.Cons (hd0, commonl));
     292            (fun _ -> { Types.fst = { Types.fst = (List.Cons (hd, commonl));
    293293            Types.snd = restl }; Types.snd = { Types.fst = (List.Cons (hd',
    294294            commonr)); Types.snd = restr } })) __)) __)) __)) __)) __
     
    303303     | List.Nil -> Types.Some List.Nil
    304304     | List.Cons (x, x0) -> Types.None)
    305   | List.Cons (hd0, tl) ->
     305  | List.Cons (hd, tl) ->
    306306    (match right with
    307307     | List.Nil -> Types.None
     
    309309       (match map2_opt f tl tl' with
    310310        | Types.None -> Types.None
    311         | Types.Some tail0 -> Types.Some (List.Cons ((f hd0 hd'), tail0))))
     311        | Types.Some tail -> Types.Some (List.Cons ((f hd hd'), tail))))
    312312
    313313(** val map2 :
     
    320320      | List.Cons (x, x0) ->
    321321        (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length x0)) __))
    322    | List.Cons (hd0, tl) ->
     322   | List.Cons (hd, tl) ->
    323323     (match right with
    324324      | List.Nil ->
    325325        (fun _ -> Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
    326326      | List.Cons (hd', tl') ->
    327         (fun _ -> List.Cons ((f hd0 hd'), (map2 f tl tl'))))) __
     327        (fun _ -> List.Cons ((f hd hd'), (map2 f tl tl'))))) __
    328328
    329329(** val map3 :
     
    339339            (match right with
    340340             | List.Nil -> (fun _ -> List.Nil)
    341              | List.Cons (hd0, tl) ->
     341             | List.Cons (hd, tl) ->
    342342               (fun _ ->
    343343                 Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __))
    344344              __)
    345         | List.Cons (hd0, tl) ->
     345        | List.Cons (hd, tl) ->
    346346          (fun _ ->
    347347            Logic.eq_rect_Type0 (List.length centre)
     
    349349                Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
    350350                (List.length centre)) (List.length right) __)) __)
    351    | List.Cons (hd0, tl) ->
     351   | List.Cons (hd, tl) ->
    352352     (fun _ ->
    353353       (match centre with
     
    355355          (fun _ ->
    356356            Logic.eq_rect_Type0 (List.length centre)
    357               (Logic.eq_rect_Type0 (List.length (List.Cons (hd0, tl)))
     357              (Logic.eq_rect_Type0 (List.length (List.Cons (hd, tl)))
    358358                (fun _ ->
    359359                Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)
     
    366366                 Obj.magic Nat.nat_discr (Nat.S (List.length tl')) Nat.O __)
    367367             | List.Cons (hd'', tl'') ->
    368                (fun _ _ -> List.Cons ((f hd0 hd' hd''),
    369                  (map3 f tl tl' tl'')))) __ __)) __)) __
    370 
    371 (** val eq_rect_Type0_r0 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
    372 let eq_rect_Type0_r0 a h x =
     368               (fun _ _ -> List.Cons ((f hd hd' hd''), (map3 f tl tl' tl''))))
     369              __ __)) __)) __
     370
     371(** val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
     372let eq_rect_Type0_r a h x =
    373373  (fun _ auto -> auto) __ h
    374374
     
    379379     (match l with
    380380      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
    381       | List.Cons (hd0, tl) -> (fun _ -> hd0))
     381      | List.Cons (hd, tl) -> (fun _ -> hd))
    382382   | Nat.S n' ->
    383383     (match l with
    384384      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
    385       | List.Cons (hd0, tl) -> (fun _ -> safe_nth n' tl))) __
     385      | List.Cons (hd, tl) -> (fun _ -> safe_nth n' tl))) __
    386386
    387387(** val nub_by_internal :
     
    391391  (match l with
    392392   | List.Nil -> List.Nil
    393    | List.Cons (hd0, tl) -> l)
     393   | List.Cons (hd, tl) -> l)
    394394| Nat.S n0 ->
    395395  (match l with
    396396   | List.Nil -> List.Nil
    397    | List.Cons (hd0, tl) ->
    398      List.Cons (hd0,
    399        (nub_by_internal f (List.filter (fun y -> Bool.notb (f y hd0)) tl) n0)))
     397   | List.Cons (hd, tl) ->
     398     List.Cons (hd,
     399       (nub_by_internal f (List.filter (fun y -> Bool.notb (f y hd)) tl) n0)))
    400400
    401401(** val nub_by :
     
    408408let rec member eq a = function
    409409| List.Nil -> Bool.False
    410 | List.Cons (hd0, tl) -> Bool.orb (eq a hd0) (member eq a tl)
     410| List.Cons (hd, tl) -> Bool.orb (eq a hd) (member eq a tl)
    411411
    412412(** val take : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
     
    417417    (match l with
    418418     | List.Nil -> List.Nil
    419      | List.Cons (hd0, tl) -> List.Cons (hd0, (take n0 tl)))
     419     | List.Cons (hd, tl) -> List.Cons (hd, (take n0 tl)))
    420420
    421421(** val drop : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
     
    426426    (match l with
    427427     | List.Nil -> List.Nil
    428      | List.Cons (hd0, tl) -> drop n0 tl)
     428     | List.Cons (hd, tl) -> drop n0 tl)
    429429
    430430(** val list_split :
     
    437437let rec mapi_internal n f = function
    438438| List.Nil -> List.Nil
    439 | List.Cons (hd0, tl) ->
    440   List.Cons ((f n hd0), (mapi_internal (Nat.plus n (Nat.S Nat.O)) f tl))
     439| List.Cons (hd, tl) ->
     440  List.Cons ((f n hd), (mapi_internal (Nat.plus n (Nat.S Nat.O)) f tl))
    441441
    442442(** val mapi : (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
     
    449449  match left with
    450450  | List.Nil -> List.Nil
    451   | List.Cons (hd0, tl) ->
     451  | List.Cons (hd, tl) ->
    452452    (match right with
    453453     | List.Nil -> List.Nil
    454454     | List.Cons (hd', tl') ->
    455        List.Cons ({ Types.fst = hd0; Types.snd = hd' }, (zip_pottier tl tl')))
     455       List.Cons ({ Types.fst = hd; Types.snd = hd' }, (zip_pottier tl tl')))
    456456
    457457(** val zip_safe :
     
    463463       (match right with
    464464        | List.Nil -> (fun _ -> List.Nil)
    465         | List.Cons (hd0, tl) ->
     465        | List.Cons (hd, tl) ->
    466466          (fun _ ->
    467467            Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)) __)
    468    | List.Cons (hd0, tl) ->
     468   | List.Cons (hd, tl) ->
    469469     (fun _ ->
    470470       (match right with
     
    473473            Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
    474474        | List.Cons (hd', tl') ->
    475           (fun _ -> List.Cons ({ Types.fst = hd0; Types.snd = hd' },
     475          (fun _ -> List.Cons ({ Types.fst = hd; Types.snd = hd' },
    476476            (zip_safe tl tl')))) __)) __
    477477
     
    482482  match l with
    483483  | List.Nil -> Types.Some List.Nil
    484   | List.Cons (hd0, tl) ->
     484  | List.Cons (hd, tl) ->
    485485    (match r with
    486486     | List.Nil -> Types.None
     
    488488       (match zip tl tl' with
    489489        | Types.None -> Types.None
    490         | Types.Some tail0 ->
    491           Types.Some (List.Cons ({ Types.fst = hd0; Types.snd = hd' },
    492             tail0))))
     490        | Types.Some tail ->
     491          Types.Some (List.Cons ({ Types.fst = hd; Types.snd = hd' }, tail))))
    493492
    494493(** val foldl : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1 **)
    495494let rec foldl f a = function
    496495| List.Nil -> a
    497 | List.Cons (hd0, tl) -> foldl f (f a hd0) tl
     496| List.Cons (hd, tl) -> foldl f (f a hd) tl
    498497
    499498(** val rev : 'a1 List.list -> 'a1 List.list **)
     
    505504let rec fold_left_i_aux f x i = function
    506505| List.Nil -> x
    507 | List.Cons (hd0, tl) -> fold_left_i_aux f (f i x hd0) (Nat.S i) tl
     506| List.Cons (hd, tl) -> fold_left_i_aux f (f i x hd) (Nat.S i) tl
    508507
    509508(** val fold_left_i :
     
    607606(** val if_then_else_safe :
    608607    Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
    609 let if_then_else_safe b f g0 =
     608let if_then_else_safe b f g =
    610609  (match b with
    611610   | Bool.True -> f
    612    | Bool.False -> g0) __
     611   | Bool.False -> g) __
    613612
    614613(** val dpi1__o__not_neq_None__o__inject :
     
    633632    Obj.magic (fun _ dH -> dH __ __)) y
    634633
    635 (** val eq_rect_Type1_r0 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
    636 let eq_rect_Type1_r0 a h x =
     634(** val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
     635let eq_rect_Type1_r a h x =
    637636  (fun _ auto -> auto) __ h
    638637
Note: See TracChangeset for help on using the changeset viewer.