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

    r2743 r2773  
    5151(** val universe_rect_Type4 :
    5252    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    53 let rec universe_rect_Type4 tag h_mk_universe x_3083 =
    54   let next_identifier = x_3083 in h_mk_universe next_identifier
     53let rec universe_rect_Type4 tag h_mk_universe x_3343 =
     54  let next_identifier = x_3343 in h_mk_universe next_identifier
    5555
    5656(** val universe_rect_Type5 :
    5757    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    58 let rec universe_rect_Type5 tag h_mk_universe x_3085 =
    59   let next_identifier = x_3085 in h_mk_universe next_identifier
     58let rec universe_rect_Type5 tag h_mk_universe x_3345 =
     59  let next_identifier = x_3345 in h_mk_universe next_identifier
    6060
    6161(** val universe_rect_Type3 :
    6262    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    63 let rec universe_rect_Type3 tag h_mk_universe x_3087 =
    64   let next_identifier = x_3087 in h_mk_universe next_identifier
     63let rec universe_rect_Type3 tag h_mk_universe x_3347 =
     64  let next_identifier = x_3347 in h_mk_universe next_identifier
    6565
    6666(** val universe_rect_Type2 :
    6767    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    68 let rec universe_rect_Type2 tag h_mk_universe x_3089 =
    69   let next_identifier = x_3089 in h_mk_universe next_identifier
     68let rec universe_rect_Type2 tag h_mk_universe x_3349 =
     69  let next_identifier = x_3349 in h_mk_universe next_identifier
    7070
    7171(** val universe_rect_Type1 :
    7272    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    73 let rec universe_rect_Type1 tag h_mk_universe x_3091 =
    74   let next_identifier = x_3091 in h_mk_universe next_identifier
     73let rec universe_rect_Type1 tag h_mk_universe x_3351 =
     74  let next_identifier = x_3351 in h_mk_universe next_identifier
    7575
    7676(** val universe_rect_Type0 :
    7777    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
    78 let rec universe_rect_Type0 tag h_mk_universe x_3093 =
    79   let next_identifier = x_3093 in h_mk_universe next_identifier
     78let rec universe_rect_Type0 tag h_mk_universe x_3353 =
     79  let next_identifier = x_3353 in h_mk_universe next_identifier
    8080
    8181(** val next_identifier :
     
    135135  { Types.fst = id; Types.snd = (Positive.succ id) }
    136136
    137 type fresh_for_univ = __
    138 
    139 type 'x env_fresh_for_univ = __
    140 
    141137(** val eq_identifier :
    142138    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
    143139    PreIdentifiers.identifier -> Bool.bool **)
    144140let eq_identifier t l r =
    145   let l' = l in let r' = r in Positive.eqb0 l' r'
     141  let l' = l in let r' = r in Positive.eqb l' r'
    146142
    147143(** val eq_identifier_elim :
     
    172168  (fun clearme0 ->
    173169  let y = clearme0 in
    174   (match Positive.eqb0 x y with
     170  (match Positive.eqb x y with
    175171   | Bool.True -> (fun _ -> Types.Inl __)
    176172   | Bool.False -> (fun _ -> Types.Inr __)) __)
     
    180176let identifier_of_nat tag n =
    181177  Positive.succ_pos_of_nat n
    182 
    183 type 'x distinct_env = __
    184178
    185179(** val check_member_env :
     
    188182let rec check_member_env tag id = function
    189183| List.Nil -> Errors.OK __
    190 | List.Cons (hd0, tl) ->
    191   (match identifier_eq tag id hd0.Types.fst with
     184| List.Cons (hd, tl) ->
     185  (match identifier_eq tag id hd.Types.fst with
    192186   | Types.Inl _ ->
    193187     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.DuplicateVariable),
     
    204198let rec check_distinct_env tag = function
    205199| List.Nil -> Errors.OK __
    206 | List.Cons (hd0, tl) ->
     200| List.Cons (hd, tl) ->
    207201  Obj.magic
    208202    (Monad.m_bind0 (Monad.max_def Errors.res0)
    209       (Obj.magic (check_member_env tag hd0.Types.fst tl)) (fun _ ->
     203      (Obj.magic (check_member_env tag hd.Types.fst tl)) (fun _ ->
    210204      Monad.m_bind0 (Monad.max_def Errors.res0)
    211205        (Obj.magic (check_distinct_env tag tl)) (fun _ ->
     
    221215    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    222216    'a1 identifier_map -> 'a2 **)
    223 let rec identifier_map_rect_Type4 tag h_an_id_map x_3255 =
    224   let x_3256 = x_3255 in h_an_id_map x_3256
     217let rec identifier_map_rect_Type4 tag h_an_id_map x_3515 =
     218  let x_3516 = x_3515 in h_an_id_map x_3516
    225219
    226220(** val identifier_map_rect_Type5 :
    227221    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    228222    'a1 identifier_map -> 'a2 **)
    229 let rec identifier_map_rect_Type5 tag h_an_id_map x_3258 =
    230   let x_3259 = x_3258 in h_an_id_map x_3259
     223let rec identifier_map_rect_Type5 tag h_an_id_map x_3518 =
     224  let x_3519 = x_3518 in h_an_id_map x_3519
    231225
    232226(** val identifier_map_rect_Type3 :
    233227    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    234228    'a1 identifier_map -> 'a2 **)
    235 let rec identifier_map_rect_Type3 tag h_an_id_map x_3261 =
    236   let x_3262 = x_3261 in h_an_id_map x_3262
     229let rec identifier_map_rect_Type3 tag h_an_id_map x_3521 =
     230  let x_3522 = x_3521 in h_an_id_map x_3522
    237231
    238232(** val identifier_map_rect_Type2 :
    239233    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    240234    'a1 identifier_map -> 'a2 **)
    241 let rec identifier_map_rect_Type2 tag h_an_id_map x_3264 =
    242   let x_3265 = x_3264 in h_an_id_map x_3265
     235let rec identifier_map_rect_Type2 tag h_an_id_map x_3524 =
     236  let x_3525 = x_3524 in h_an_id_map x_3525
    243237
    244238(** val identifier_map_rect_Type1 :
    245239    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    246240    'a1 identifier_map -> 'a2 **)
    247 let rec identifier_map_rect_Type1 tag h_an_id_map x_3267 =
    248   let x_3268 = x_3267 in h_an_id_map x_3268
     241let rec identifier_map_rect_Type1 tag h_an_id_map x_3527 =
     242  let x_3528 = x_3527 in h_an_id_map x_3528
    249243
    250244(** val identifier_map_rect_Type0 :
    251245    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
    252246    'a1 identifier_map -> 'a2 **)
    253 let rec identifier_map_rect_Type0 tag h_an_id_map x_3270 =
    254   let x_3271 = x_3270 in h_an_id_map x_3271
     247let rec identifier_map_rect_Type0 tag h_an_id_map x_3530 =
     248  let x_3531 = x_3530 in h_an_id_map x_3531
    255249
    256250(** val identifier_map_inv_rect_Type4 :
     
    300294  PositiveMap.Pm_leaf
    301295
    302 (** val lookup0 :
     296(** val lookup :
    303297    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    304298    PreIdentifiers.identifier -> 'a1 Types.option **)
    305 let rec lookup0 tag m l =
     299let rec lookup tag m l =
    306300  PositiveMap.lookup_opt (let l' = l in l') (let m' = m in m')
    307301
     
    310304    PreIdentifiers.identifier -> 'a1 -> 'a1 **)
    311305let lookup_def tag m l d =
    312   match lookup0 tag m l with
     306  match lookup tag m l with
    313307  | Types.None -> d
    314308  | Types.Some x -> x
    315309
    316 (** val member0 :
     310(** val member :
    317311    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    318312    PreIdentifiers.identifier -> Bool.bool **)
    319 let member0 tag m l =
    320   match lookup0 tag m l with
     313let member tag m l =
     314  match lookup tag m l with
    321315  | Types.None -> Bool.False
    322316  | Types.Some x -> Bool.True
     
    326320    PreIdentifiers.identifier -> 'a1 **)
    327321let lookup_safe tag m i =
    328   (match lookup0 tag m i with
     322  (match lookup tag m i with
    329323   | Types.None -> (fun _ -> assert false (* absurd case *))
    330324   | Types.Some x -> (fun _ -> x)) __
     
    340334    (PreIdentifiers.identifier, 'a1) Types.prod List.list **)
    341335let elements tag m =
    342   PositiveMap.fold0 (fun l a el -> List.Cons ({ Types.fst = l; Types.snd =
     336  PositiveMap.fold (fun l a el -> List.Cons ({ Types.fst = l; Types.snd =
    343337    a }, el)) (let m' = m in m') List.Nil
    344338
     
    349343  PositiveMap.pm_all (let m' = m in m') (fun p a _ -> f p a __)
    350344
    351 (** val update0 :
     345(** val update :
    352346    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    353347    PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map Errors.res **)
    354 let update0 tag m l a =
     348let update tag m l a =
    355349  match PositiveMap.update (let l' = l in l') a (let m' = m in m') with
    356350  | Types.None ->
     
    365359  PositiveMap.pm_set (let p = id in p) Types.None (let m0 = m in m0)
    366360
    367 (** val foldi0 :
     361(** val foldi :
    368362    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> 'a1 -> 'a2
    369363    -> 'a2) -> 'a1 identifier_map -> 'a2 -> 'a2 **)
    370 let foldi0 tag f m b =
    371   let m' = m in PositiveMap.fold0 (fun bv -> f bv) m' b
     364let foldi tag f m b =
     365  let m' = m in PositiveMap.fold (fun bv -> f bv) m' b
    372366
    373367(** val fold_inf :
     
    378372  (fun f b -> PositiveMap.pm_fold_inf m' (fun bv a _ -> f bv a __) b)
    379373
    380 (** val find0 :
     374(** val find :
    381375    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
    382376    (PreIdentifiers.identifier -> 'a1 -> Bool.bool) ->
    383377    (PreIdentifiers.identifier, 'a1) Types.prod Types.option **)
    384 let find0 tag m p =
     378let find tag m p =
    385379  let m' = m in
    386380  Types.option_map (fun x -> { Types.fst = x.Types.fst; Types.snd =
     
    391385    PreIdentifiers.identifier -> 'a1 **)
    392386let lookup_present tag m id =
    393   (match lookup0 tag m id with
     387  (match lookup tag m id with
    394388   | Types.None -> (fun _ -> assert false (* absurd case *))
    395389   | Types.Some a -> (fun _ -> a)) __
     
    406400   | Types.Some m'0 -> (fun _ -> m'0)) __
    407401
    408 type 'x fresh_for_map = __
    409 
    410402type identifier_set = Types.unit0 identifier_map
    411403
     
    434426    | Types.None ->
    435427      Obj.magic
    436         (Monad.m_bind0 (Monad.max_def Option.option0) (Obj.magic o')
    437           (fun x -> Monad.m_return0 (Monad.max_def Option.option0) Types.It))
     428        (Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic o') (fun x ->
     429          Monad.m_return0 (Monad.max_def Option.option) Types.It))
    438430    | Types.Some x -> Types.Some Types.It) (let s0 = s in s0)
    439431    (let s1 = s' in s1)
     
    519511    PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set **)
    520512let id_set_of_map tag m =
    521   PositiveMap.map0 (fun x -> Types.It) (let m' = m in m')
     513  PositiveMap.map (fun x -> Types.It) (let m' = m in m')
    522514
    523515(** val set_of_list :
Note: See TracChangeset for help on using the changeset viewer.