Changeset 1290


Ignore:
Timestamp:
Oct 4, 2011, 2:00:54 AM (8 years ago)
Author:
sacerdot
Message:

One more function ported to new Joint.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1288 r1290  
    942942  let f ≝ λsrcr. sequential rtl_params_ globals (OP2 rtl_params_ globals Or tmpr tmpr srcr) in
    943943  let def ≝ adds_graph rtl_params1 globals (init :: (map ? ? f srcrs)) start_lbl tmp_lbl def in
    944     add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true lbl_false)) def.
     944    add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true) lbl_false) def.
    945945
    946946definition translate_load ≝
     
    966966        let translates ≝ translates @ [
    967967          adds_graph [
    968             rtl_st_int tmpr off start_lbl
     968            INT tmpr off start_lbl
    969969          ];
    970970          translate_op2 Oaddp tmp_addr ? save_addr [tmpr] ? ?;
    971971          adds_graph [
    972             rtl_st_load r tmp_addr1 tmp_addr2 dest_lbl
     972            LOAD r tmp_addr1 tmp_addr2 dest_lbl
    973973          ]
    974974        ]
     
    10391039  match stmt with
    10401040  [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def
    1041   | _ ⇒ ? ].
    1042 (*
    10431041  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
    10441042  | St_const destr cst lbl' ⇒
     
    10801078  |*: cases daemon (* TODO: proofs regarding lengths of lists, examine! *)
    10811079  ]
    1082 *) cases daemon
    10831080qed.
    10841081
Note: See TracChangeset for help on using the changeset viewer.