Changeset 1247


Ignore:
Timestamp:
Sep 22, 2011, 3:03:41 AM (8 years ago)
Author:
sacerdot
Message:

Code (almost) ported to latest joint/Joint.ma datatype.
I still need to figure out the new unification hint...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1246 r1247  
    1717  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
    1818
    19 record more_sem_params (p:params): Type[1] ≝
     19record more_sem_params (p:params_): Type[1] ≝
    2020 { framesT: Type[0]
    2121 ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
     
    4141
    4242record sem_params: Type[1] ≝
    43  { spp :> params
     43 { spp :> params_
    4444 ; more_sem_pars :> more_sem_params spp
    4545 }.
     
    5454 }.
    5555
    56 definition genv ≝ λp:params.λglobals. (genv_t Genv) (joint_function p globals).
     56definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
    5757
    5858(*
     
    6363*)
    6464
    65 record more_sem_params2 (p: params) (globals: list ident): Type[1] ≝
     65record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
    6666 { more_sparams:> more_sem_params p
    6767 
     
    7171 ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val
    7272
    73  ; exec_extended: genv p globals → extend_statements (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams)))
     73 ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams)))
    7474 }.
    7575
    7676record sem_params2 (globals: list ident): Type[1] ≝
    77  { p2:> params
    78  ; more_sparams2:> more_sem_params2 p2 globals
     77 { p2:> params globals
     78 ; more_sparams2:> more_sem_params2 globals p2
    7979 }.
    8080
     
    8282coercion sem_params_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params
    8383 ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params.
    84 
     84(*
    8585unification hint  0 ≔ globals: (list ident), p: sem_params2 globals;
    8686   S ≟ sem_params_of_sem_params2 globals p
     
    8989    (more_sparams (p2 globals p) globals
    9090    (more_sparams2 globals p)))) ≡ spp__o__pars_ S.
    91 
     91*)
    9292definition address_of_label: sem_params → label → address.
    9393 #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label … p l)))
     
    211211coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
    212212
    213 definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv p globals → state p → IO io_out io_in (trace × (state p)) ≝
     213definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
    214214 λglobals,p,ge,st.
    215215  ! s ← fetch_statement … st;
     
    336336 ; exit: address
    337337 ; registersno: nat
    338  ; genv2: genv sparams2 globals
     338 ; genv2: genv globals sparams2
    339339 }.
    340340
     
    345345
    346346definition make_global :
    347  ∀pars:params. ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
     347 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
    348348  joint_program pars → evaluation_parameters
    349349
    350350 λpars,sparams.
    351351  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ?? (globalenv Genv … (λx.[Init_space x]) p)).
    352 [1,2: cases daemon ]
     352[1,2: cases daemon (*CSC: XXXXXXXXXXXXX*) ]
    353353qed.
    354354
    355355definition make_initial_state :
    356  ∀pars:params. ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
    357  ∀p: joint_program … pars. res (state (mk_sem_params pars (sparams p))) ≝
     356 ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
     357 ∀p: joint_program … pars. res (state (mk_sem_params (pars (prog_var_names … p)) (sparams p))) ≝
    358358λpars,sparams,p.
    359359  let ge ≝ genv2 (make_global pars sparams p) in
     
    376376
    377377definition joint_fullexec :
    378  ∀pars:params.
    379  ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
     378 ∀pars:∀globals.params globals.
     379 ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
    380380 fullexec io_out io_in ≝
    381381 λpars,sparams.
Note: See TracChangeset for help on using the changeset viewer.