Ignore:
Timestamp:
Jul 19, 2012, 6:13:54 PM (8 years ago)
Author:
tranquil
Message:
  • collapsed step_params, unserialized_params, funct_params and local_params into one (unserialized_params)
  • completed update of RTL, LTL and LIN semantics
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r2214 r2217  
    2424              |       |    /   
    2525          unserialized_params             
    26             |            \       
    27             |             \     
    28             |         local_params
    29             |              |   
    30     step_params       funct_params
    31 
    32 step_params : types needed to define steps (stmts with a default fallthrough)
     26
     27unserialized_params : things unrelated to serialization (i.e. graph or linear
     28                      form)
    3329stmt_params : adds successor type needed to define statements
    3430funct_params : types of result register and parameters of function
    35 local_params : adds types of local registers
    3631params : adds type of code and related properties *)
    3732
     
    7570definition zero_byte : Byte ≝ bv_zero 8.
    7671
    77 record step_params : Type[1] ≝
     72record unserialized_params : Type[1] ≝
    7873 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
    7974 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
     
    9590 ; ext_tailcall : Type[0]
    9691 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
     92 ; paramsT : Type[0]
     93 ; localsT: Type[0]
    9794 }.
    9895
    99 inductive joint_seq (p:step_params) (globals: list ident): Type[0] ≝
     96inductive joint_seq (p:unserialized_params) (globals: list ident): Type[0] ≝
    10097  | COMMENT: String → joint_seq p globals
    10198  | COST_LABEL: costlabel → joint_seq p globals
     
    145142  extension_branch on _s : ext_branch ? to joint_branch ?.*)
    146143
    147 inductive joint_step (p : step_params) (globals : list ident) : Type[0] ≝
     144inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝
    148145  | step_seq : joint_seq p globals → joint_step p globals
    149146  | COND: acc_a_reg p → label → joint_step p globals.
     
    170167    ].
    171168
    172 definition step_forall_labels : ∀p : step_params.∀globals.
     169definition step_forall_labels : ∀p.∀globals.
    173170    (label → Prop) → joint_step p globals → Prop ≝
    174171λp,g,P,inst. All … P (step_labels … inst).
    175172
    176173definition step_classifier :
    177   ∀p : step_params.∀globals.
     174  ∀p.∀globals.
    178175    joint_step p globals → status_class ≝ λp,g,s.
    179176  match s with
     
    187184  ].
    188185
    189 record funct_params : Type[1] ≝
    190   { resultT : Type[0]
    191   ; paramsT : Type[0]
    192   }.
    193  
    194 record local_params : Type[1] ≝
    195  { funct_pars :> funct_params
    196  ; localsT: Type[0]
    197  }.
    198 
    199 record unserialized_params : Type[1] ≝
    200  { u_inst_pars :> step_params
    201  ; u_local_pars :> local_params
    202  }.
    203 
    204186record stmt_params : Type[1] ≝
    205187  { uns_pars :> unserialized_params
     
    208190  }.
    209191
    210 inductive joint_fin_step (p: step_params): Type[0] ≝
     192inductive joint_fin_step (p: unserialized_params): Type[0] ≝
    211193  | GOTO: label → joint_fin_step p
    212194  | RETURN: joint_fin_step p
     
    468450    forall_statements_i … (statement_closed … code) code.
    469451
    470 (* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
    471 definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.
    472   (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))).
    473 
    474452record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
    475453{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
     
    478456     following, right? *)
    479457(*  joint_if_sig: signature;  -- dropped in front end *)
    480   joint_if_result   : resultT p;
     458  joint_if_result   : call_dest p;
    481459  joint_if_params   : paramsT p;
    482460  joint_if_locals   : list (localsT p); (* use void where no locals are present *)
Note: See TracChangeset for help on using the changeset viewer.