Changeset 1386


Ignore:
Timestamp:
Oct 17, 2011, 1:58:47 AM (8 years ago)
Author:
sacerdot
Message:

Structure of semantic parameters simplified.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1385 r1386  
    6060    (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)).
    6161
    62 definition ertl_more_sem_params1 : more_sem_params1 … ertl_params1 ≝
    63  mk_more_sem_params1 ? ertl_params1 ertl_more_sem_params
    64   ertl_init_locals ertl_save_frame.
    65 
    6662(*CSC: XXXXX, for is_final only *)
    6763axiom ertl_fetch_result:
     
    118114definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
    119115 λglobals.
    120   mk_more_sem_params2 … ertl_more_sem_params1
     116  mk_more_sem_params2 … ertl_more_sem_params
    121117   (graph_fetch_statement …) (load_ra …) (ertl_fetch_result …)
    122    (ertl_pop_frame …) ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
     118   ertl_init_locals ertl_save_frame (ertl_pop_frame …)
     119   ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
    123120
    124121definition ertl_fullexec ≝
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1385 r1386  
    3636 λ_.λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    3737
    38 definition ltl_lin_more_sem_params1 : ∀succT,succ,pointer_of_label.more_sem_params1 … ltl_lin_params1 ≝
    39  λsuccT,succ,pointer_of_label.
    40  mk_more_sem_params1 ? ltl_lin_params1 (ltl_lin_more_sem_params succT succ pointer_of_label)
    41   ltl_lin_init_locals (ltl_lin_save_frame …).
    42 
    4338(*CSC: XXXXX, for is_final only *)
    4439axiom ltl_lin_fetch_result:
     
    5954 ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝
    6055 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
    61   mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ pointer_of_label)
    62    (fetch globals) (load_ra …) (ltl_lin_fetch_result …) (ltl_lin_pop_frame …)
     56  mk_more_sem_params2 … (ltl_lin_more_sem_params … succ pointer_of_label)
     57   (fetch globals) (load_ra …) (ltl_lin_fetch_result …)
     58   ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
    6359   (ltl_lin_fetch_external_args …) (ltl_lin_set_result …) (ltl_lin_exec_extended …).
    6460
  • src/RTL/semantics.ma

    r1385 r1386  
    8888qed.
    8989
    90 definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝
    91  mk_more_sem_params1 ? rtl_params1 rtl_more_sem_params
    92   rtl_init_locals rtl_save_frame.
    93 
    9490(*CSC: XXXX, for external functions only*)
    9591axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val).
     
    117113definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
    118114 λglobals.
    119   mk_more_sem_params2 … rtl_more_sem_params1
     115  mk_more_sem_params2 … rtl_more_sem_params
    120116   (graph_fetch_statement …) rtl_fetch_ra (rtl_fetch_result …)
    121    (rtl_pop_frame …) rtl_fetch_external_args rtl_set_result (rtl_exec_extended …).
     117   rtl_init_locals rtl_save_frame (rtl_pop_frame …)
     118   rtl_fetch_external_args rtl_set_result (rtl_exec_extended …).
    122119
    123120definition rtl_fullexec ≝
  • src/joint/semantics.ma

    r1385 r1386  
    4848 }.
    4949
    50 record more_sem_params1 (succT: Type[0]) (p:params1): Type[1] ≝
    51  { more_sparams :> more_sem_params (mk_params_ p succT)
    52 
    53  ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
    54    (*CSC: save_frame returns a res only because we can call a function with the wrong number and
    55      type of arguments. To be fixed using a dependent type *)
    56  ; save_frame: address → nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    57  }.
    58 
    5950record sem_params1: Type[1] ≝
    6051 { spp1 :> params1
    6152 ; ssucc_ : Type[0]
    62  ; more_sem_params1 :> more_sem_params1 ssucc_ spp1
     53 ; more_sem_params1 :> more_sem_params (mk_params_ spp1 ssucc_)
    6354 }.
    6455
     
    7061
    7162record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
    72  { more_sparams1 :> more_sem_params1 (succ p) p
     63 { more_sparams1 :> more_sem_params p
    7364
    7465 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams1) → res (joint_statement (mk_sem_params … more_sparams1) globals)
     
    7768 ; fetch_result: genv globals p → state (mk_sem_params … more_sparams1) → res (list beval)
    7869
     70 ; init_locals : localsT p → regsT … more_sparams1 → regsT … more_sparams1
     71   (*CSC: save_frame returns a res only because we can call a function with the wrong number and
     72     type of arguments. To be fixed using a dependent type *)
     73 ; save_frame: address → nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1))
    7974 ; pop_frame: genv globals p → state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)))
    8075
     
    9388coercion sem_params_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params
    9489 ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params.
    95 (*
    96 unification hint  0 ≔ globals: (list ident), p: sem_params2 globals;
    97    S ≟ sem_params_of_sem_params2 globals p
    98 (* ---------------------------------------- *) ⊢
    99    pars_ (spp (mk_sem_params (p2 globals p)
    100     (more_sparams (p2 globals p) globals
    101     (more_sparams2 globals p)))) ≡ spp__o__pars_ S.
    102 *)
     90
    10391definition sem_params1_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params1 sp2 (succ sp2) sp2.
    10492coercion sem_params1_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params1
Note: See TracChangeset for help on using the changeset viewer.