Changeset 2783 for src/LIN


Ignore:
Timestamp:
Mar 6, 2013, 12:09:52 PM (7 years ago)
Author:
piccolo
Message:

modified joint_closed_internal_function definition (added condition on pseudo-registers)
added new record for parameters
modified state definition with option for framesT

Location:
src/LIN
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN_semantics.ma

    r2601 r2783  
    33
    44definition LIN_semantics : sem_params ≝
    5   make_sem_lin_params LIN LTL_LIN_semantics.
     5  mk_sem_lin_params LIN LTL_LIN_semantics.
  • src/LIN/joint_LTL_LIN.ma

    r2645 r2783  
    2020].
    2121
    22 definition LTL_LIN : unserialized_params ≝ mk_unserialized_params
     22definition LTL_LIN_uns : unserialized_params ≝ mk_unserialized_params
    2323    (* acc_a_reg ≝ *) unit
    2424    (* acc_b_reg ≝ *) unit
     
    3838    (* paramsT ≝ *) unit.
    3939
     40definition LTL_LIN_functs : get_pseudo_reg_functs LTL_LIN_uns ≝
     41mk_get_pseudo_reg_functs ?
     42(* acc_a_regs *) (λ_.[ ])
     43(* acc_b_regs *) (λ_.[ ])
     44(* acc_a_args *) (λ_.[ ])
     45(* acc_b_args *) (λ_.[ ])
     46(* dpl_regs *) (λ_.[ ])
     47(* dph_regs *) (λ_.[ ])
     48(* dpl_args *) (λ_.[ ])
     49(* dph_args *) (λ_.[ ])
     50(* snd_args *) (λ_.[ ])
     51(* pair_move_regs *) (λ_.[ ])
     52(* f_call_args *) (λ_.[ ])
     53(* f_call_dest *) (λ_.[ ])
     54(* ext_seq_regs *) (λ_.[ ])
     55(* params_regs *) (λ_.[ ]).
     56
     57definition LTL_LIN ≝  mk_uns_params LTL_LIN_uns LTL_LIN_functs.
     58
    4059interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
    4160interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)).
  • src/LIN/joint_LTL_LIN_semantics.ma

    r2645 r2783  
    3838axiom eval_ltl_lin_seq : ltl_lin_seq → state LTL_LIN_state → IO io_out io_in (state LTL_LIN_state).
    3939
     40definition LTL_LIN_save_frame :
     41call_kind → unit → state_pc LTL_LIN_state → res(state LTL_LIN_state) ≝
     42λk.λ_.λst. match k with
     43[ PTR ⇒ return (st_no_pc … st)
     44| ID ⇒ push_ra … st (pc … st)
     45].
     46
    4047definition LTL_LIN_semantics ≝
    4148  λF.mk_sem_unserialized_params LTL_LIN F
     
    5764(*  (* fetch_ra           ≝ *) (load_ra …)
    5865  (* allocate_local     ≝ *) (λabs.match abs in void with [ ])
    59 *)  (* save_frame         ≝ *) ?(*(λp.λ_.λst.save_ra … st p)*)
     66*)  (* save_frame         ≝ *) LTL_LIN_save_frame
    6067  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
    6168  (* fetch_external_args≝ *) ?(*ltl_lin_fetch_external_args*)
     
    6875(*  (* eval_ext_tailcall  ≝ *) ?(*(λ_.λ_.λabs.match abs in void with [ ])*)
    6976  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
    70 *)  (* pop_frame          ≝ *) ?(*(λ_.λ_.λ_.λst.return st)*)
     77*)  (* pop_frame          ≝ *) ((λ_.λ_.λ_.λ_.λst.pop_ra … st))
    7178(*  (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)*).
     79cases daemon
     80qed.
Note: See TracChangeset for help on using the changeset viewer.