Changeset 1386 for src/joint


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

Structure of semantic parameters simplified.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.