Changeset 2977 for extracted/lINToASM.ml


Ignore:
Timestamp:
Mar 27, 2013, 4:09:56 PM (7 years ago)
Author:
sacerdot
Message:

New extraction after several bug fixes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/lINToASM.ml

    r2963 r2977  
    134134                      label_map : ASM.identifier Identifiers.identifier_map
    135135                                  Identifiers.identifier_map;
    136                       address_map : BitVector.word Identifiers.identifier_map;
    137                       fresh_cost_label : Positive.pos }
     136                      address_map : BitVector.word Identifiers.identifier_map }
    138137
    139138(** val aSM_universe_rect_Type4 :
     
    141140    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    142141    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    143     Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    144     -> 'a1 **)
     142    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    145143let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_3 =
    146144  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    147     ident_map0; label_map = label_map0; address_map = address_map0;
    148     fresh_cost_label = fresh_cost_label0 } = x_3
     145    ident_map0; label_map = label_map0; address_map = address_map0 } = x_3
    149146  in
    150147  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
    151     address_map0 __ fresh_cost_label0
     148    address_map0 __
    152149
    153150(** val aSM_universe_rect_Type5 :
     
    155152    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    156153    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    157     Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    158     -> 'a1 **)
     154    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    159155let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_5 =
    160156  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    161     ident_map0; label_map = label_map0; address_map = address_map0;
    162     fresh_cost_label = fresh_cost_label0 } = x_5
     157    ident_map0; label_map = label_map0; address_map = address_map0 } = x_5
    163158  in
    164159  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
    165     address_map0 __ fresh_cost_label0
     160    address_map0 __
    166161
    167162(** val aSM_universe_rect_Type3 :
     
    169164    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    170165    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    171     Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    172     -> 'a1 **)
     166    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    173167let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_7 =
    174168  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    175     ident_map0; label_map = label_map0; address_map = address_map0;
    176     fresh_cost_label = fresh_cost_label0 } = x_7
     169    ident_map0; label_map = label_map0; address_map = address_map0 } = x_7
    177170  in
    178171  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
    179     address_map0 __ fresh_cost_label0
     172    address_map0 __
    180173
    181174(** val aSM_universe_rect_Type2 :
     
    183176    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    184177    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    185     Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    186     -> 'a1 **)
     178    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    187179let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_9 =
    188180  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    189     ident_map0; label_map = label_map0; address_map = address_map0;
    190     fresh_cost_label = fresh_cost_label0 } = x_9
     181    ident_map0; label_map = label_map0; address_map = address_map0 } = x_9
    191182  in
    192183  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
    193     address_map0 __ fresh_cost_label0
     184    address_map0 __
    194185
    195186(** val aSM_universe_rect_Type1 :
     
    197188    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    198189    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    199     Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    200     -> 'a1 **)
     190    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    201191let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_11 =
    202192  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    203     ident_map0; label_map = label_map0; address_map = address_map0;
    204     fresh_cost_label = fresh_cost_label0 } = x_11
     193    ident_map0; label_map = label_map0; address_map = address_map0 } = x_11
    205194  in
    206195  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
    207     address_map0 __ fresh_cost_label0
     196    address_map0 __
    208197
    209198(** val aSM_universe_rect_Type0 :
     
    211200    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    212201    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    213     Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    214     -> 'a1 **)
     202    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    215203let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_13 =
    216204  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    217     ident_map0; label_map = label_map0; address_map = address_map0;
    218     fresh_cost_label = fresh_cost_label0 } = x_13
     205    ident_map0; label_map = label_map0; address_map = address_map0 } = x_13
    219206  in
    220207  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
    221     address_map0 __ fresh_cost_label0
     208    address_map0 __
    222209
    223210(** val id_univ :
     
    248235  xxx.address_map
    249236
    250 (** val fresh_cost_label :
    251     AST.ident List.list -> aSM_universe -> Positive.pos **)
    252 let rec fresh_cost_label globals xxx =
    253   xxx.fresh_cost_label
    254 
    255237(** val aSM_universe_inv_rect_Type4 :
    256238    AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    257239    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    258240    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    259     Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **)
     241    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
    260242let aSM_universe_inv_rect_Type4 x1 hterm h1 =
    261243  let hcut = aSM_universe_rect_Type4 x1 h1 hterm in hcut __
     
    265247    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    266248    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    267     Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **)
     249    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
    268250let aSM_universe_inv_rect_Type3 x1 hterm h1 =
    269251  let hcut = aSM_universe_rect_Type3 x1 h1 hterm in hcut __
     
    273255    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    274256    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    275     Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **)
     257    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
    276258let aSM_universe_inv_rect_Type2 x1 hterm h1 =
    277259  let hcut = aSM_universe_rect_Type2 x1 h1 hterm in hcut __
     
    281263    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    282264    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    283     Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **)
     265    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
    284266let aSM_universe_inv_rect_Type1 x1 hterm h1 =
    285267  let hcut = aSM_universe_rect_Type1 x1 h1 hterm in hcut __
     
    289271    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    290272    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    291     Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **)
     273    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
    292274let aSM_universe_inv_rect_Type0 x1 hterm h1 =
    293275  let hcut = aSM_universe_rect_Type0 x1 h1 hterm in hcut __
     
    298280  Logic.eq_rect_Type2 x
    299281    (let { id_univ = a0; current_funct = a10; ident_map = a2; label_map = a3;
    300        address_map = a4; fresh_cost_label = a6 } = x
     282       address_map = a4 } = x
    301283     in
    302     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
    303 
    304 (** val report_cost :
    305     AST.ident List.list -> CostLabel.costlabel -> Types.unit0
    306     Monad.smax_def__o__monad **)
    307 let report_cost globals cl =
    308   Obj.magic (fun u ->
    309     let clw = Identifiers.word_of_identifier PreIdentifiers.CostTag cl in
    310     (match Positive.leb u.fresh_cost_label clw with
    311      | Bool.True ->
    312        { Types.fst = { id_univ = u.id_univ; current_funct = u.current_funct;
    313          ident_map = u.ident_map; label_map = u.label_map; address_map =
    314          u.address_map; fresh_cost_label = (Positive.succ clw) }; Types.snd =
    315          Types.It }
    316      | Bool.False -> { Types.fst = u; Types.snd = Types.It }))
     284    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
    317285
    318286(** val new_ASM_universe : Joint.joint_program -> aSM_universe **)
     
    340308  (Identifiers.empty_map PreIdentifiers.SymbolTag); label_map =
    341309  (Identifiers.empty_map PreIdentifiers.SymbolTag); address_map =
    342   addresses.Types.fst; fresh_cost_label = Positive.One }
     310  addresses.Types.fst }
    343311
    344312(** val identifier_of_label :
     
    368336    u.ident_map; label_map =
    369337    (Identifiers.add PreIdentifiers.SymbolTag u.label_map current lmap0);
    370     address_map = u.address_map; fresh_cost_label = u.fresh_cost_label };
    371     Types.snd = id })
     338    address_map = u.address_map }; Types.snd = id })
    372339
    373340(** val identifier_of_ident :
     
    391358    let { Types.fst = id; Types.snd = univ } = eta8 in
    392359    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
    393     ident_map = imap0; label_map = u.label_map; address_map = u.address_map;
    394     fresh_cost_label = u.fresh_cost_label }; Types.snd = id })
     360    ident_map = imap0; label_map = u.label_map; address_map =
     361    u.address_map }; Types.snd = id })
    395362
    396363(** val start_funct_translation :
     
    400367  Obj.magic (fun u -> { Types.fst = { id_univ = u.id_univ; current_funct =
    401368    id_f.Types.fst; ident_map = u.ident_map; label_map = u.label_map;
    402     address_map = u.address_map; fresh_cost_label = u.fresh_cost_label };
    403     Types.snd = Types.It })
     369    address_map = u.address_map }; Types.snd = Types.It })
    404370
    405371(** val address_of_ident :
     
    419385    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
    420386    ident_map = u.ident_map; label_map = u.label_map; address_map =
    421     u.address_map; fresh_cost_label = u.fresh_cost_label }; Types.snd = id })
     387    u.address_map }; Types.snd = id })
    422388
    423389(** val register_address : I8051.register -> ASM.subaddressing_mode **)
     
    693659  (match instr with
    694660   | Joint.COST_LABEL lbl ->
    695      Monad.m_bind0 (Monad.smax_def State.state_monad)
    696        (report_cost globals lbl) (fun x0 ->
    697        Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Cost lbl))
     661     Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Cost lbl)
    698662   | Joint.CALL (f, x0, x1) ->
    699663     (match f with
     
    11721136    (List.append (do_store_init_data globals u nxt_dptr data0) acc) }
    11731137  in
    1174   (List.foldr f { Types.fst = start_dptr; Types.snd = List.Nil } data).Types.snd
     1138  List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV
     1139  (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR; Types.snd =
     1140  (ASM.DATA16
     1141  (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1142    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     1143    Nat.O)))))))))))))))) start_dptr)) }))))) },
     1144  (List.foldr f { Types.fst = start_dptr; Types.snd = List.Nil } data).Types.snd)
    11751145
    11761146(** val translate_initialization :
     
    12761246            Monad.m_bind0 (Monad.smax_def State.state_monad)
    12771247              (translate_initialization p) (fun init ->
    1278               Monad.m_bind0 (Monad.smax_def State.state_monad)
    1279                 State.state_get (fun u ->
    1280                 Monad.m_return0 (Monad.smax_def State.state_monad)
    1281                   (let code0 =
    1282                      List.append init (List.Cons ({ Types.fst = Types.None;
    1283                        Types.snd = (ASM.Call main) }, (List.Cons
    1284                        ({ Types.fst = (Types.Some exit_label); Types.snd =
    1285                        (ASM.Cost u.fresh_cost_label) }, (List.Cons
    1286                        ({ Types.fst = Types.None; Types.snd = (ASM.Jmp
    1287                        exit_label) }, code))))))
    1288                    in
    1289                   Monad.m_bind0 (Monad.max_def Option.option)
    1290                     (Obj.magic (ASM.code_size_opt code0)) (fun _ ->
    1291                     Monad.m_return0 (Monad.max_def Option.option)
    1292                       { ASM.preamble = List.Nil; ASM.code = code0;
    1293                       ASM.renamed_symbols = symboltable; ASM.final_label =
    1294                       exit_label })))))))))
    1295 
     1248              Monad.m_return0 (Monad.smax_def State.state_monad)
     1249                (let code0 =
     1250                   List.append init (List.Cons ({ Types.fst = Types.None;
     1251                     Types.snd = (ASM.Call main) }, (List.Cons ({ Types.fst =
     1252                     (Types.Some exit_label); Types.snd = (ASM.Jmp
     1253                     exit_label) }, code))))
     1254                 in
     1255                Monad.m_bind0 (Monad.max_def Option.option)
     1256                  (Obj.magic (ASM.code_size_opt code0)) (fun _ ->
     1257                  Monad.m_return0 (Monad.max_def Option.option)
     1258                    { ASM.preamble = List.Nil; ASM.code = code0;
     1259                    ASM.renamed_symbols = symboltable; ASM.final_label =
     1260                    exit_label }))))))))
     1261
Note: See TracChangeset for help on using the changeset viewer.