Changeset 2977


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

New extraction after several bug fixes.

Location:
extracted
Files:
4 edited

Legend:

Unmodified
Added
Removed

  • extracted/backEndOps.ml

    r2951 r2977  
    402402    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    403403    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    404 let rec eval_rect_Type4 h_mk_Eval x_16349 =
    405   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16349 in
     404let rec eval_rect_Type4 h_mk_Eval x_185 =
     405  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_185 in
    406406  h_mk_Eval opaccs0 op4 op5
    407407
    … …  
    411411    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    412412    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    413 let rec eval_rect_Type5 h_mk_Eval x_16351 =
    414   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16351 in
     413let rec eval_rect_Type5 h_mk_Eval x_187 =
     414  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_187 in
    415415  h_mk_Eval opaccs0 op4 op5
    416416
    … …  
    420420    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    421421    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    422 let rec eval_rect_Type3 h_mk_Eval x_16353 =
    423   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16353 in
     422let rec eval_rect_Type3 h_mk_Eval x_189 =
     423  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_189 in
    424424  h_mk_Eval opaccs0 op4 op5
    425425
    … …  
    429429    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    430430    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    431 let rec eval_rect_Type2 h_mk_Eval x_16355 =
    432   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16355 in
     431let rec eval_rect_Type2 h_mk_Eval x_191 =
     432  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_191 in
    433433  h_mk_Eval opaccs0 op4 op5
    434434
    … …  
    438438    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    439439    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    440 let rec eval_rect_Type1 h_mk_Eval x_16357 =
    441   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16357 in
     440let rec eval_rect_Type1 h_mk_Eval x_193 =
     441  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_193 in
    442442  h_mk_Eval opaccs0 op4 op5
    443443
    … …  
    447447    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    448448    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    449 let rec eval_rect_Type0 h_mk_Eval x_16359 =
    450   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_16359 in
     449let rec eval_rect_Type0 h_mk_Eval x_195 =
     450  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_195 in
    451451  h_mk_Eval opaccs0 op4 op5
    452452
    … …  
    705705                 in
    706706                 let { Types.fst = rslt; Types.snd = carry0 } =
    707                    eval0.op3 Bool.False op b2 o1o0.Types.snd
     707                   eval0.op3 Bool.False op o1o0.Types.snd b2
    708708                 in
    709709                 let p0 = Nat.O in

  • 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

  • extracted/lINToASM.mli

    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
    139138val aSM_universe_rect_Type4 :
    … …  
    141140  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    142141  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    143   __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
     142  __ -> 'a1) -> aSM_universe -> 'a1
    144143
    145144val aSM_universe_rect_Type5 :
    … …  
    147146  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    148147  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    149   __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
     148  __ -> 'a1) -> aSM_universe -> 'a1
    150149
    151150val aSM_universe_rect_Type3 :
    … …  
    153152  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    154153  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    155   __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
     154  __ -> 'a1) -> aSM_universe -> 'a1
    156155
    157156val aSM_universe_rect_Type2 :
    … …  
    159158  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    160159  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    161   __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
     160  __ -> 'a1) -> aSM_universe -> 'a1
    162161
    163162val aSM_universe_rect_Type1 :
    … …  
    165164  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    166165  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    167   __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
     166  __ -> 'a1) -> aSM_universe -> 'a1
    168167
    169168val aSM_universe_rect_Type0 :
    … …  
    171170  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
    172171  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
    173   __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
     172  __ -> 'a1) -> aSM_universe -> 'a1
    174173
    175174val id_univ : AST.ident List.list -> aSM_universe -> Identifiers.universe
    … …  
    189188  Identifiers.identifier_map
    190189
    191 val fresh_cost_label : AST.ident List.list -> aSM_universe -> Positive.pos
    192 
    193190val aSM_universe_inv_rect_Type4 :
    194191  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    195192  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    196193  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    197   Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
     194  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
    198195
    199196val aSM_universe_inv_rect_Type3 :
    … …  
    201198  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    202199  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    203   Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
     200  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
    204201
    205202val aSM_universe_inv_rect_Type2 :
    … …  
    207204  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    208205  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    209   Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
     206  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
    210207
    211208val aSM_universe_inv_rect_Type1 :
    … …  
    213210  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    214211  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    215   Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
     212  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
    216213
    217214val aSM_universe_inv_rect_Type0 :
    … …  
    219216  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    220217  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    221   Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
     218  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
    222219
    223220val aSM_universe_jmdiscr :
    224221  AST.ident List.list -> aSM_universe -> aSM_universe -> __
    225 
    226 val report_cost :
    227   AST.ident List.list -> CostLabel.costlabel -> Types.unit0
    228   Monad.smax_def__o__monad
    229222
    230223val new_ASM_universe : Joint.joint_program -> aSM_universe

  • extracted/rTL.ml

    r2961 r2977  
    125125    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    126126let rec rtl_seq_rect_Type4 h_rtl_stack_address = function
    127 | Rtl_stack_address (x_7, x_6) -> h_rtl_stack_address x_7 x_6
     127| Rtl_stack_address (x_1495, x_1494) -> h_rtl_stack_address x_1495 x_1494
    128128
    129129(** val rtl_seq_rect_Type5 :
    130130    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    131131let rec rtl_seq_rect_Type5 h_rtl_stack_address = function
    132 | Rtl_stack_address (x_11, x_10) -> h_rtl_stack_address x_11 x_10
     132| Rtl_stack_address (x_1499, x_1498) -> h_rtl_stack_address x_1499 x_1498
    133133
    134134(** val rtl_seq_rect_Type3 :
    135135    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    136136let rec rtl_seq_rect_Type3 h_rtl_stack_address = function
    137 | Rtl_stack_address (x_15, x_14) -> h_rtl_stack_address x_15 x_14
     137| Rtl_stack_address (x_1503, x_1502) -> h_rtl_stack_address x_1503 x_1502
    138138
    139139(** val rtl_seq_rect_Type2 :
    140140    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    141141let rec rtl_seq_rect_Type2 h_rtl_stack_address = function
    142 | Rtl_stack_address (x_19, x_18) -> h_rtl_stack_address x_19 x_18
     142| Rtl_stack_address (x_1507, x_1506) -> h_rtl_stack_address x_1507 x_1506
    143143
    144144(** val rtl_seq_rect_Type1 :
    145145    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    146146let rec rtl_seq_rect_Type1 h_rtl_stack_address = function
    147 | Rtl_stack_address (x_23, x_22) -> h_rtl_stack_address x_23 x_22
     147| Rtl_stack_address (x_1511, x_1510) -> h_rtl_stack_address x_1511 x_1510
    148148
    149149(** val rtl_seq_rect_Type0 :
    150150    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    151151let rec rtl_seq_rect_Type0 h_rtl_stack_address = function
    152 | Rtl_stack_address (x_27, x_26) -> h_rtl_stack_address x_27 x_26
     152| Rtl_stack_address (x_1515, x_1514) -> h_rtl_stack_address x_1515 x_1514
    153153
    154154(** val rtl_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.