Ignore:
Timestamp:
Mar 6, 2013, 12:09:52 PM (8 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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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)).
Note: See TracChangeset for help on using the changeset viewer.