Ignore:
Timestamp:
Jul 6, 2012, 5:53:01 PM (8 years ago)
Author:
tranquil
Message:
  • yet another correction to joint
  • added functions adding prologues and epilogues in TranslateUtils?. Adding a prologue will preserve the invariant of having a cost label at the start of the function, without needing transformations later
  • redefined ERTL and rewritten RTLToERTL (with suffix "_paolo")
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r2155 r2162  
    7878  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
    7979  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
    80   | extension_seq : ext_seq p → joint_seq p globals.
     80  | CALL_ID: ident → call_args p → call_dest p → joint_seq p globals
     81  | extension_seq : ext_seq p → joint_seq p globals
     82  | extension_call : ext_call p → joint_seq p globals.
    8183
    8284axiom EmptyString : String.
     
    9698interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
    9799
    98 coercion extension_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
     100coercion extension_seq_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
    99101  extension_seq on _s : ext_seq ? to joint_seq ??.
    100 
    101 inductive joint_call (p : step_params) : Type[0] ≝
    102   | CALL_ID: ident → call_args p → call_dest p → joint_call p
    103   | extension_call : ext_call p → joint_call p.
    104 
    105 coercion extension_to_call : ∀p.∀s : ext_call p.joint_call p ≝
    106   extension_call on _s : ext_call ? to joint_call ?.
     102coercion extension_call_to_seq : ∀p,globals.∀s : ext_call p.joint_seq p globals ≝
     103  extension_call on _s : ext_call ? to joint_seq ??.
    107104 
    108 inductive joint_branch (p : step_params) : Type[0] ≝
     105(* inductive joint_branch (p : step_params) : Type[0] ≝
    109106  | COND: acc_a_reg p → label → joint_branch p
    110   (*| extension_branch : ext_branch p → joint_branch p*).
     107  | extension_branch : ext_branch p → joint_branch p.*)
    111108
    112109(*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝
     
    115112inductive joint_step (p : step_params) (globals : list ident) : Type[0] ≝
    116113  | step_seq : joint_seq p globals → joint_step p globals
    117   | step_call : joint_call p → joint_step p globals
    118   | step_branch : joint_branch p → joint_step p globals.
     114  | COND: acc_a_reg p → label → joint_step p globals.
    119115
    120116coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝
    121117  step_seq on _s : joint_seq ?? to joint_step ??.
    122 coercion call_to_step : ∀p,globals.∀s : joint_call p.joint_step p globals ≝
    123   step_call on _s : joint_call ? to joint_step ??.
    124 coercion branch_to_step : ∀p,globals.∀s : joint_branch p.joint_step p globals ≝
    125   step_branch on _s : joint_branch ? to joint_step ??.
    126118
    127119definition step_flows ≝ λp,globals.λs : joint_step p globals.
    128120  match s with
    129   [ step_seq _ ⇒ Labels … [ ]
    130   | step_call _ ⇒ Call
    131   | step_branch s ⇒
     121  [ step_seq s ⇒
    132122    match s with
    133     [ COND _ l ⇒ Labels … [l]
    134     (*| extension_branch s' ⇒ Labels … (ext_branch_labels … s')*)
     123    [ CALL_ID _ _ _ ⇒ Call
     124    | extension_call _ ⇒ Call
     125    | _ ⇒ Labels … [ ]
    135126    ]
     127  | COND _ l ⇒ Labels … [l]
    136128  ].
    137129
     
    151143    joint_step p globals → status_class ≝ λp,g,s.
    152144  match s with
    153   [ step_seq _ ⇒ cl_other
    154   | step_call _ ⇒ cl_call
    155   | step_branch _ ⇒ cl_jump
     145  [ step_seq s ⇒
     146    match s with
     147    [ CALL_ID _ _ _ ⇒ cl_call
     148    | extension_call _ ⇒ cl_call
     149    | _ ⇒ cl_other
     150    ]
     151  | COND _ _ ⇒ cl_jump
    156152  ].
    157153
Note: See TracChangeset for help on using the changeset viewer.