Changeset 2743 for extracted/eRTLptr.ml


Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (7 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/eRTLptr.ml

    r2730 r2743  
    116116    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    117117let rec ertlptr_seq_rect_Type4 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    118 | Ertlptr_ertl x_281 -> h_ertlptr_ertl x_281
    119 | LOW_ADDRESS (x_283, x_282) -> h_LOW_ADDRESS x_283 x_282
    120 | HIGH_ADDRESS (x_285, x_284) -> h_HIGH_ADDRESS x_285 x_284
     118| Ertlptr_ertl x_21035 -> h_ertlptr_ertl x_21035
     119| LOW_ADDRESS (x_21037, x_21036) -> h_LOW_ADDRESS x_21037 x_21036
     120| HIGH_ADDRESS (x_21039, x_21038) -> h_HIGH_ADDRESS x_21039 x_21038
    121121
    122122(** val ertlptr_seq_rect_Type5 :
     
    124124    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    125125let rec ertlptr_seq_rect_Type5 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    126 | Ertlptr_ertl x_290 -> h_ertlptr_ertl x_290
    127 | LOW_ADDRESS (x_292, x_291) -> h_LOW_ADDRESS x_292 x_291
    128 | HIGH_ADDRESS (x_294, x_293) -> h_HIGH_ADDRESS x_294 x_293
     126| Ertlptr_ertl x_21044 -> h_ertlptr_ertl x_21044
     127| LOW_ADDRESS (x_21046, x_21045) -> h_LOW_ADDRESS x_21046 x_21045
     128| HIGH_ADDRESS (x_21048, x_21047) -> h_HIGH_ADDRESS x_21048 x_21047
    129129
    130130(** val ertlptr_seq_rect_Type3 :
     
    132132    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    133133let rec ertlptr_seq_rect_Type3 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    134 | Ertlptr_ertl x_299 -> h_ertlptr_ertl x_299
    135 | LOW_ADDRESS (x_301, x_300) -> h_LOW_ADDRESS x_301 x_300
    136 | HIGH_ADDRESS (x_303, x_302) -> h_HIGH_ADDRESS x_303 x_302
     134| Ertlptr_ertl x_21053 -> h_ertlptr_ertl x_21053
     135| LOW_ADDRESS (x_21055, x_21054) -> h_LOW_ADDRESS x_21055 x_21054
     136| HIGH_ADDRESS (x_21057, x_21056) -> h_HIGH_ADDRESS x_21057 x_21056
    137137
    138138(** val ertlptr_seq_rect_Type2 :
     
    140140    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    141141let rec ertlptr_seq_rect_Type2 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    142 | Ertlptr_ertl x_308 -> h_ertlptr_ertl x_308
    143 | LOW_ADDRESS (x_310, x_309) -> h_LOW_ADDRESS x_310 x_309
    144 | HIGH_ADDRESS (x_312, x_311) -> h_HIGH_ADDRESS x_312 x_311
     142| Ertlptr_ertl x_21062 -> h_ertlptr_ertl x_21062
     143| LOW_ADDRESS (x_21064, x_21063) -> h_LOW_ADDRESS x_21064 x_21063
     144| HIGH_ADDRESS (x_21066, x_21065) -> h_HIGH_ADDRESS x_21066 x_21065
    145145
    146146(** val ertlptr_seq_rect_Type1 :
     
    148148    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    149149let rec ertlptr_seq_rect_Type1 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    150 | Ertlptr_ertl x_317 -> h_ertlptr_ertl x_317
    151 | LOW_ADDRESS (x_319, x_318) -> h_LOW_ADDRESS x_319 x_318
    152 | HIGH_ADDRESS (x_321, x_320) -> h_HIGH_ADDRESS x_321 x_320
     150| Ertlptr_ertl x_21071 -> h_ertlptr_ertl x_21071
     151| LOW_ADDRESS (x_21073, x_21072) -> h_LOW_ADDRESS x_21073 x_21072
     152| HIGH_ADDRESS (x_21075, x_21074) -> h_HIGH_ADDRESS x_21075 x_21074
    153153
    154154(** val ertlptr_seq_rect_Type0 :
     
    156156    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    157157let rec ertlptr_seq_rect_Type0 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    158 | Ertlptr_ertl x_326 -> h_ertlptr_ertl x_326
    159 | LOW_ADDRESS (x_328, x_327) -> h_LOW_ADDRESS x_328 x_327
    160 | HIGH_ADDRESS (x_330, x_329) -> h_HIGH_ADDRESS x_330 x_329
     158| Ertlptr_ertl x_21080 -> h_ertlptr_ertl x_21080
     159| LOW_ADDRESS (x_21082, x_21081) -> h_LOW_ADDRESS x_21082 x_21081
     160| HIGH_ADDRESS (x_21084, x_21083) -> h_HIGH_ADDRESS x_21084 x_21083
    161161
    162162(** val ertlptr_seq_inv_rect_Type4 :
     
    230230  Obj.magic (fun _ x -> Joint.Extension_seq x)
    231231
     232(** val dpi1__o__ertlptr_seq_to_joint_seq__o__inject :
     233    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
     234    Types.sig0 **)
     235let dpi1__o__ertlptr_seq_to_joint_seq__o__inject x1 x2 =
     236  ertlptr_seq_joint x1 x2.Types.dpi1
     237
     238(** val dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
     239    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
     240    Types.sig0 **)
     241let dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
     242  Joint.seq_to_step__o__inject
     243    (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTLptr) x1
     244    (ertlptr_seq_joint x1 x2.Types.dpi1)
     245
     246(** val dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step :
     247    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step **)
     248let dpi1__o__ertlptr_seq_to_joint_seq__o__seq_to_step x1 x2 =
     249  Joint.Step_seq (ertlptr_seq_joint x1 x2.Types.dpi1)
     250
     251(** val eject__o__ertlptr_seq_to_joint_seq__o__inject :
     252    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0 **)
     253let eject__o__ertlptr_seq_to_joint_seq__o__inject x1 x2 =
     254  ertlptr_seq_joint x1 (Types.pi1 x2)
     255
     256(** val eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
     257    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0 **)
     258let eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x1 x2 =
     259  Joint.seq_to_step__o__inject
     260    (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTLptr) x1
     261    (ertlptr_seq_joint x1 (Types.pi1 x2))
     262
     263(** val eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step :
     264    AST.ident List.list -> __ Types.sig0 -> Joint.joint_step **)
     265let eject__o__ertlptr_seq_to_joint_seq__o__seq_to_step x1 x2 =
     266  Joint.Step_seq (ertlptr_seq_joint x1 (Types.pi1 x2))
     267
     268(** val ertlptr_seq_to_joint_seq__o__seq_to_step :
     269    AST.ident List.list -> __ -> Joint.joint_step **)
     270let ertlptr_seq_to_joint_seq__o__seq_to_step x0 x1 =
     271  Joint.Step_seq (ertlptr_seq_joint x0 x1)
     272
     273(** val ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject :
     274    AST.ident List.list -> __ -> Joint.joint_step Types.sig0 **)
     275let ertlptr_seq_to_joint_seq__o__seq_to_step__o__inject x0 x1 =
     276  Joint.seq_to_step__o__inject
     277    (Joint.gp_to_p__o__stmt_pars__o__uns_pars eRTLptr) x0
     278    (ertlptr_seq_joint x0 x1)
     279
     280(** val ertlptr_seq_to_joint_seq__o__inject :
     281    AST.ident List.list -> __ -> Joint.joint_seq Types.sig0 **)
     282let ertlptr_seq_to_joint_seq__o__inject x0 x1 =
     283  ertlptr_seq_joint x0 x1
     284
     285(** val dpi1__o__ertlptr_seq_to_joint_seq :
     286    AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq **)
     287let dpi1__o__ertlptr_seq_to_joint_seq x1 x2 =
     288  ertlptr_seq_joint x1 x2.Types.dpi1
     289
     290(** val eject__o__ertlptr_seq_to_joint_seq :
     291    AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq **)
     292let eject__o__ertlptr_seq_to_joint_seq x1 x2 =
     293  ertlptr_seq_joint x1 (Types.pi1 x2)
     294
Note: See TracChangeset for help on using the changeset viewer.