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

    r2730 r2773  
    1717open Extralib
    1818
     19open Lists
     20
     21open Positive
     22
     23open Identifiers
     24
     25open Registers
     26
     27open Exp
     28
    1929open Setoids
    2030
     
    2333open Option
    2434
    25 open Lists
    26 
    27 open Positive
    28 
    29 open Identifiers
    30 
    31 open Registers
    32 
    33 open Exp
    34 
    3535open Extranat
    3636
     
    8181open LabelledObjects
    8282
     83open BitVectorTrie
     84
    8385open Graphs
    84 
    85 open BitVectorTrie
    8686
    8787open CostLabel
     
    146146    AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
    147147    List.list **)
    148 let get_params_hdw globals params0 =
    149   save_hdws globals (Util.zip_pottier params0 I8051.registerParams)
     148let get_params_hdw globals params =
     149  save_hdws globals (Util.zip_pottier params I8051.registerParams)
    150150
    151151(** val get_param_stack :
     
    167167    AST.ident List.list -> Registers.register List.list ->
    168168    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
    169 let get_params_stack globals params0 =
     169let get_params_stack globals params =
    170170  Bind_new.Bnew (fun tmpr -> Bind_new.Bnew (fun addr1 -> Bind_new.Bnew
    171171    (fun addr2 ->
    172172    let params_length_byte =
    173173      Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    174         (Nat.S (Nat.S Nat.O)))))))) (List.length params0)
     174        (Nat.S (Nat.S Nat.O)))))))) (List.length params)
    175175    in
    176176    let l =
     
    198198        List.Nil))))))))))))))
    199199        (List.flatten
    200           (List.map (get_param_stack globals addr1 addr2) params0))
     200          (List.map (get_param_stack globals addr1 addr2) params))
    201201    in
    202202    Bind_new.Bret l)))
     
    205205    AST.ident List.list -> Registers.register List.list ->
    206206    (Registers.register, Joint.joint_seq) BindLists.bind_list **)
    207 let get_params globals params0 =
    208   let n = Nat.min (List.length params0) (List.length I8051.registerParams) in
     207let get_params globals params =
     208  let n = Nat.min (List.length params) (List.length I8051.registerParams) in
    209209  let { Types.fst = hdw_params; Types.snd = stack_params } =
    210     Util.list_split n params0
     210    Util.list_split n params
    211211  in
    212212  BindLists.bappend
     
    263263    List.list -> (Registers.register, Joint.joint_seq List.list)
    264264    Bind_new.bind_new **)
    265 let prologue globals params0 sral srah sregs =
     265let prologue globals params sral srah sregs =
    266266  BindLists.bappend
    267267    (let l = List.Cons
     
    273273    Bind_new.Bret l)
    274274    (BindLists.bappend (let l = save_hdws globals sregs in Bind_new.Bret l)
    275       (get_params globals params0))
     275      (get_params globals params))
    276276
    277277(** val set_params_hdw :
    278278    AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
    279279    List.list **)
    280 let set_params_hdw globals params0 =
    281   restore_hdws globals (Util.zip_pottier params0 I8051.registerParams)
     280let set_params_hdw globals params =
     281  restore_hdws globals (Util.zip_pottier params I8051.registerParams)
    282282
    283283(** val set_param_stack :
     
    298298    AST.ident List.list -> Joint.psd_argument List.list ->
    299299    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
    300 let set_params_stack globals params0 =
     300let set_params_stack globals params =
    301301  Bind_new.Bnew (fun addr1 -> Bind_new.Bnew (fun addr2 ->
    302302    let params_length_byte =
    303303      Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    304         (Nat.S (Nat.S Nat.O)))))))) (List.length params0)
     304        (Nat.S (Nat.S Nat.O)))))))) (List.length params)
    305305    in
    306306    let l =
     
    320320        List.Nil))))))))))
    321321        (List.flatten
    322           (List.map (set_param_stack globals addr1 addr2) params0))
     322          (List.map (set_param_stack globals addr1 addr2) params))
    323323    in
    324324    Bind_new.Bret l))
     
    328328    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
    329329    Types.sig0 **)
    330 let set_params globals params0 =
    331   let n = Nat.min (List.length params0) (List.length I8051.registerParams) in
    332   let hdw_stack_params = List.split params0 n in
     330let set_params globals params =
     331  let n = Nat.min (List.length params) (List.length I8051.registerParams) in
     332  let hdw_stack_params = List.split params n in
    333333  let hdw_params = hdw_stack_params.Types.fst in
    334334  let stack_params = hdw_stack_params.Types.snd in
     
    378378| Joint.Step_seq s0 ->
    379379  (match s0 with
    380    | Joint.COMMENT msg0 ->
    381      Bind_new.Bret
    382        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    383          globals (List.Cons ((Joint.COMMENT msg0), List.Nil)))
     380   | Joint.COMMENT msg ->
     381     Bind_new.Bret
     382       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     383         globals (List.Cons ((Joint.COMMENT msg), List.Nil)))
    384384   | Joint.MOVE rs ->
    385385     Bind_new.Bret
     
    398398       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    399399         globals List.Nil)
    400    | Joint.ADDRESS (x0, r5, r6) ->
    401      Bind_new.Bret
    402        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    403          globals (List.Cons ((Joint.ADDRESS (x0, r5, r6)), List.Nil)))
    404    | Joint.OPACCS (op4, destr1, destr2, srcr1, srcr2) ->
    405      Bind_new.Bret
    406        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    407          globals (List.Cons ((Joint.OPACCS (op4, destr1, destr2, srcr1,
     400   | Joint.ADDRESS (x0, r1, r2) ->
     401     Bind_new.Bret
     402       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     403         globals (List.Cons ((Joint.ADDRESS (x0, r1, r2)), List.Nil)))
     404   | Joint.OPACCS (op, destr1, destr2, srcr1, srcr2) ->
     405     Bind_new.Bret
     406       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     407         globals (List.Cons ((Joint.OPACCS (op, destr1, destr2, srcr1,
    408408         srcr2)), List.Nil)))
    409    | Joint.OP1 (op4, destr, srcr) ->
    410      Bind_new.Bret
    411        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    412          globals (List.Cons ((Joint.OP1 (op4, destr, srcr)), List.Nil)))
    413    | Joint.OP2 (op4, destr, srcr1, srcr2) ->
    414      Bind_new.Bret
    415        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    416          globals (List.Cons ((Joint.OP2 (op4, destr, srcr1, srcr2)),
     409   | Joint.OP1 (op1, destr, srcr) ->
     410     Bind_new.Bret
     411       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     412         globals (List.Cons ((Joint.OP1 (op1, destr, srcr)), List.Nil)))
     413   | Joint.OP2 (op2, destr, srcr1, srcr2) ->
     414     Bind_new.Bret
     415       (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     416         globals (List.Cons ((Joint.OP2 (op2, destr, srcr1, srcr2)),
    417417         List.Nil)))
    418418   | Joint.CLEAR_CARRY ->
     
    483483    Bind_new.bind_new **)
    484484let translate_data globals def =
    485   let params0 = (Types.pi1 def).Joint.joint_if_params in
     485  let params = (Types.pi1 def).Joint.joint_if_params in
    486486  let new_stacksize =
    487487    Nat.plus (Types.pi1 def).Joint.joint_if_stacksize
    488       (Nat.minus (List.length (Obj.magic params0))
     488      (Nat.minus (List.length (Obj.magic params))
    489489        (List.length I8051.registerParams))
    490490  in
     
    492492    Obj.magic
    493493      (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
    494         (Obj.magic (prologue globals (Obj.magic params0) ral rah to_save))
     494        (Obj.magic (prologue globals (Obj.magic params) ral rah to_save))
    495495        (fun prologue0 ->
    496496        Monad.m_return0 (Monad.max_def Bind_new.bindNew)
    497497          { TranslateUtils.init_ret = (Obj.magic Types.It);
    498498          TranslateUtils.init_params =
    499           (Obj.magic (List.length (Obj.magic params0)));
     499          (Obj.magic (List.length (Obj.magic params)));
    500500          TranslateUtils.init_stack_size = new_stacksize;
    501501          TranslateUtils.added_prologue = prologue0; TranslateUtils.f_step =
Note: See TracChangeset for help on using the changeset viewer.