Changeset 2422 for src/joint/Joint.ma


Ignore:
Timestamp:
Oct 30, 2012, 4:23:09 PM (8 years ago)
Author:
tranquil
Message:

adapted joint to cl_call f

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2286 r2422  
    77include "common/LabelledObjects.ma".
    88include "ASM/Util.ma".
    9 include "common/StructuredTraces.ma".
    109
    1110(* Here is the structure of parameter records (downward edges are coercions,
     
    169168λp,g,P,inst. All … P (step_labels … inst).
    170169
    171 definition step_classifier :
    172   ∀p.∀globals.
    173     joint_step p globals → status_class ≝ λp,g,s.
    174   match s with
    175   [ step_seq s ⇒
    176     match s with
    177     [ CALL_ID _ _ _ ⇒ cl_call
    178     | extension_call _ ⇒ cl_call
    179     | _ ⇒ cl_other
    180     ]
    181   | COND _ _ ⇒ cl_jump
    182   ].
    183 
    184170record stmt_params : Type[1] ≝
    185171  { uns_pars :> unserialized_params
     
    207193    ].
    208194
    209 definition fin_step_classifier :
    210   ∀p : stmt_params.
    211     joint_fin_step p → status_class
    212   ≝ λp,s.
    213   match s with
    214   [ GOTO _ ⇒ cl_other
    215   | _ ⇒ cl_return
    216   ].
    217 
    218195inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    219196  | sequential: joint_step p globals → succ p → joint_statement p globals
    220197  | final: joint_fin_step p → joint_statement p globals.
    221 
    222 definition stmt_classifier :
    223   ∀p : stmt_params.∀globals.
    224     joint_statement p globals → status_class
    225   ≝ λp,g,s.
    226   match s with
    227   [ sequential stp _ ⇒ step_classifier p g stp
    228   | final stp ⇒ fin_step_classifier p stp
    229   ].
    230198
    231199coercion extension_fin_to_fin_step : ∀p : stmt_params.
     
    466434definition joint_closed_internal_function ≝
    467435  λp,globals.
    468     Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
     436    Σdef : joint_internal_function p globals. code_closed … (joint_if_code … def).
    469437
    470438definition set_joint_code ≝
     
    534502    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
    535503
    536 definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
     504definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals).
    537505
    538506definition joint_program ≝
Note: See TracChangeset for help on using the changeset viewer.