Changeset 1380


Ignore:
Timestamp:
Oct 14, 2011, 10:25:03 PM (8 years ago)
Author:
sacerdot
Message:

LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma.
Very cool.

Location:
src
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/semantics.ma

    r1378 r1380  
    1 include "joint/SemanticUtils.ma".
     1include "LIN/joint_LTL_LIN_semantics.ma".
    22include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *)
    33
     
    55axiom lin_succ_pc: unit → address → address.
    66
    7 (*CSC: re-organize to take succ_pc out of lin_more_sem_params to share the
    8   following definition between LTL and LIN *)
    9 definition lin_more_sem_params: more_sem_params lin_params_ :=
    10  mk_more_sem_params lin_params_
    11   unit hw_register_env lin_succ_pc
    12    hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
    13     (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
    14     (λ_.hwreg_store RegisterDPL) (λe.λ_.hwreg_retrieve e RegisterDPL)
    15     (λ_.hwreg_store RegisterDPH) (λe.λ_.hwreg_retrieve e RegisterDPH)
    16      (λlocals,dest_src.
    17        match dest_src with
    18        [ from_acc reg ⇒
    19           do v ← hwreg_retrieve locals RegisterA ;
    20           hwreg_store reg v locals
    21        | to_acc reg ⇒
    22           do v ← hwreg_retrieve locals reg ;
    23           hwreg_store RegisterA v locals ])
    24      pointer_of_label.
    25 definition lin_sem_params: sem_params ≝ mk_sem_params … lin_more_sem_params.
     7(*CSC: XXXXXXXXXX *)
     8axiom lin_fetch_statement: ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc) → res (pre_lin_statement globals).
    269
    27 definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    28 definition lin_pop_frame: state … lin_sem_params → res ((state … lin_sem_params) × address) ≝
    29  fetch_ra ….
    30 definition lin_save_frame:
    31  address → nat → unit → nat → unit → state … lin_sem_params → res (state … lin_sem_params) ≝
    32  λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    33 
    34 definition lin_more_sem_params1 : more_sem_params1 … ltl_lin_params1 ≝
    35  mk_more_sem_params1 ? ltl_lin_params1 lin_more_sem_params
    36   lin_init_locals lin_pop_frame lin_save_frame.
    37 
    38 (*CSC: XXXXXXXXXX *)
    39 axiom lin_fetch_statement: ∀globals. genv … (lin_params globals) → state lin_sem_params → res (pre_lin_statement globals).
    40 
    41 (*CSC: XXXXX, for is_final only *)
    42 axiom lin_fetch_result: state lin_sem_params → res (list beval).
    43 
    44 (*CSC: XXXX, for external functions only*)
    45 axiom lin_fetch_external_args: external_function → state lin_sem_params → res (list val).
    46 axiom lin_set_result: list val → state lin_sem_params → res (state lin_sem_params).
    47 
    48 definition lin_exec_extended: ∀globals. genv globals (lin_params globals) → False → unit → state lin_sem_params → IO io_out io_in (trace × (state lin_sem_params))
    49  ≝ λglobals,ge,abs. ⊥.
    50 @abs qed.
    51 
    52 definition lin_more_sem_params2: ∀globals. more_sem_params2 … (lin_params globals) ≝
    53  λglobals.
    54   mk_more_sem_params2 … lin_more_sem_params1
    55    (lin_fetch_statement …) lin_fetch_result lin_fetch_external_args lin_set_result
    56     (lin_exec_extended …).
    57 
    58 definition lin_fullexec ≝
    59  joint_fullexec … (λp. lin_more_sem_params2 (prog_var_names … p)).
     10definition lin_fullexec ≝ ltl_lin_fullexec … lin_succ_pc … lin_fetch_statement.
  • src/LTL/semantics.ma

    r1378 r1380  
    1 include "joint/SemanticUtils.ma".
     1include "LIN/joint_LTL_LIN_semantics.ma".
    22include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *)
    33
    4 definition ltl_more_sem_params: more_sem_params ltl_params_ :=
    5  mk_more_sem_params ltl_params_
    6   unit hw_register_env graph_succ_p
    7    hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
    8     (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
    9     (λ_.hwreg_store RegisterDPL) (λe.λ_.hwreg_retrieve e RegisterDPL)
    10     (λ_.hwreg_store RegisterDPH) (λe.λ_.hwreg_retrieve e RegisterDPH)
    11      (λlocals,dest_src.
    12        match dest_src with
    13        [ from_acc reg ⇒
    14           do v ← hwreg_retrieve locals RegisterA ;
    15           hwreg_store reg v locals
    16        | to_acc reg ⇒
    17           do v ← hwreg_retrieve locals reg ;
    18           hwreg_store RegisterA v locals ])
    19      pointer_of_label.
    20 definition ltl_sem_params: sem_params ≝ mk_sem_params … ltl_more_sem_params.
    21 
    22 definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    23 definition ltl_pop_frame: state … ltl_sem_params → res ((state … ltl_sem_params) × address) ≝
    24  fetch_ra ….
    25 definition ltl_save_frame:
    26  address → nat → unit → nat → unit → state … ltl_sem_params → res (state … ltl_sem_params) ≝
    27  λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    28 
    29 definition ltl_more_sem_params1 : more_sem_params1 … ltl_lin_params1 ≝
    30  mk_more_sem_params1 ? ltl_lin_params1 ltl_more_sem_params
    31   ltl_init_locals ltl_pop_frame ltl_save_frame.
    32 
    33 (*CSC: XXXXX, for is_final only *)
    34 axiom ltl_fetch_result: state ltl_sem_params → res (list beval).
    35 
    36 (*CSC: XXXX, for external functions only*)
    37 axiom ltl_fetch_external_args: external_function → state ltl_sem_params → res (list val).
    38 axiom ltl_set_result: list val → state ltl_sem_params → res (state ltl_sem_params).
    39 
    40 definition ltl_exec_extended: ∀globals. genv globals (ltl_params globals) → False → label → state ltl_sem_params → IO io_out io_in (trace × (state ltl_sem_params))
    41  ≝ λglobals,ge,abs. ⊥.
    42 @abs qed.
    43 
    44 definition ltl_more_sem_params2: ∀globals. more_sem_params2 … (ltl_params globals) ≝
    45  λglobals.
    46   mk_more_sem_params2 … ltl_more_sem_params1
    47    (graph_fetch_statement …) ltl_fetch_result ltl_fetch_external_args ltl_set_result
    48     (ltl_exec_extended …).
    49 
    504definition ltl_fullexec ≝
    51  joint_fullexec … (λp. ltl_more_sem_params2 (prog_var_names … p)).
    52 
     5 ltl_lin_fullexec … (graph_succ_p …) … (graph_fetch_statement … (ltl_lin_sem_params …)).
    536
    547(*
  • src/joint/Joint.ma

    r1282 r1380  
    172172definition joint_program ≝
    173173 λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
    174 
    175 (****************************************************************************)
    176 
    177 (* Used in LTL and LIN *) 
    178 inductive registers_move: Type[0] ≝
    179  | from_acc: Register → registers_move
    180  | to_acc: Register → registers_move.
Note: See TracChangeset for help on using the changeset viewer.