Changeset 2743 for extracted/lINToASM.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/lINToASM.ml

    r2730 r2743  
    127127    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    128128    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    129 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_7759 =
     129let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_24106 =
    130130  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    131     ident_map0; label_map = label_map0; address_map = address_map0 } = x_7759
     131    ident_map0; label_map = label_map0; address_map = address_map0 } =
     132    x_24106
    132133  in
    133134  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    139140    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    140141    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    141 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_7761 =
     142let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_24108 =
    142143  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    143     ident_map0; label_map = label_map0; address_map = address_map0 } = x_7761
     144    ident_map0; label_map = label_map0; address_map = address_map0 } =
     145    x_24108
    144146  in
    145147  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    151153    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    152154    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    153 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_7763 =
     155let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_24110 =
    154156  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    155     ident_map0; label_map = label_map0; address_map = address_map0 } = x_7763
     157    ident_map0; label_map = label_map0; address_map = address_map0 } =
     158    x_24110
    156159  in
    157160  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    163166    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    164167    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    165 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_7765 =
     168let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_24112 =
    166169  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    167     ident_map0; label_map = label_map0; address_map = address_map0 } = x_7765
     170    ident_map0; label_map = label_map0; address_map = address_map0 } =
     171    x_24112
    168172  in
    169173  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    175179    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    176180    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    177 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_7767 =
     181let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_24114 =
    178182  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    179     ident_map0; label_map = label_map0; address_map = address_map0 } = x_7767
     183    ident_map0; label_map = label_map0; address_map = address_map0 } =
     184    x_24114
    180185  in
    181186  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    187192    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    188193    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    189 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_7769 =
     194let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_24116 =
    190195  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    191     ident_map0; label_map = label_map0; address_map = address_map0 } = x_7769
     196    ident_map0; label_map = label_map0; address_map = address_map0 } =
     197    x_24116
    192198  in
    193199  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    274280  let globals_addr_internal = fun res_offset x_size ->
    275281    let { Types.fst = res1; Types.snd = offset0 } = res_offset in
    276     let { Types.fst = eta27663; Types.snd = size } = x_size in
    277     let { Types.fst = x; Types.snd = region0 } = eta27663 in
     282    let { Types.fst = eta28996; Types.snd = size } = x_size in
     283    let { Types.fst = x; Types.snd = region0 } = eta28996 in
    278284    { Types.fst =
    279285    (Identifiers.add PreIdentifiers.SymbolTag res1 x
     
    303309        (Identifiers.empty_map PreIdentifiers.LabelTag)
    304310    in
    305     let { Types.fst = eta27664; Types.snd = lmap0 } =
     311    let { Types.fst = eta28997; Types.snd = lmap0 } =
    306312      match Identifiers.lookup0 PreIdentifiers.LabelTag lmap l with
    307313      | Types.None ->
     
    315321          lmap }
    316322    in
    317     let { Types.fst = id; Types.snd = univ } = eta27664 in
     323    let { Types.fst = id; Types.snd = univ } = eta28997 in
    318324    { Types.fst = { id_univ = univ; current_funct = current; ident_map =
    319325    u.ident_map; label_map =
     
    327333  Obj.magic (fun u ->
    328334    let imap = u.ident_map in
    329     let { Types.fst = eta27665; Types.snd = imap0 } =
     335    let { Types.fst = eta28998; Types.snd = imap0 } =
    330336      match Identifiers.lookup0 PreIdentifiers.SymbolTag imap i with
    331337      | Types.None ->
     
    339345          imap }
    340346    in
    341     let { Types.fst = id; Types.snd = univ } = eta27665 in
     347    let { Types.fst = id; Types.snd = univ } = eta28998 in
    342348    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
    343349    ident_map = imap0; label_map = u.label_map; address_map =
Note: See TracChangeset for help on using the changeset viewer.