Changeset 2437 for src/joint/Joint.ma


Ignore:
Timestamp:
Nov 6, 2012, 5:00:01 PM (7 years ago)
Author:
tranquil
Message:

generalised calls to calls with pointers

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2422 r2437  
    107107  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
    108108  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
    109   | CALL_ID: ident → call_args p → call_dest p → joint_seq p globals
    110   | extension_seq : ext_seq p → joint_seq p globals
    111   | extension_call : ext_call p → joint_seq p globals.
     109  | CALL: (ident + dpl_arg p×(dph_arg p)) → call_args p → call_dest p → joint_seq p globals
     110  | extension_seq : ext_seq p → joint_seq p globals.
    112111
    113112axiom EmptyString : String.
     
    129128coercion extension_seq_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
    130129  extension_seq on _s : ext_seq ? to joint_seq ??.
    131 coercion extension_call_to_seq : ∀p,globals.∀s : ext_call p.joint_seq p globals ≝
    132   extension_call on _s : ext_call ? to joint_seq ??.
    133  
     130
    134131(* inductive joint_branch (p : step_params) : Type[0] ≝
    135132  | COND: acc_a_reg p → label → joint_branch p
     
    150147  [ step_seq s ⇒
    151148    match s with
    152     [ CALL_ID _ _ _ ⇒ Call
    153     | extension_call _ ⇒ Call
     149    [ CALL _ _ _ ⇒ Call
    154150    | _ ⇒ Labels … [ ]
    155151    ]
Note: See TracChangeset for help on using the changeset viewer.