- Timestamp:
- Sep 22, 2011, 3:03:41 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/semantics.ma
r1246 r1247 17 17 eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2). 18 18 19 record more_sem_params (p:params ): Type[1] ≝19 record more_sem_params (p:params_): Type[1] ≝ 20 20 { framesT: Type[0] 21 21 ; regsT: Type[0] (* regs = pseudo-registers + hw registers *) … … 41 41 42 42 record sem_params: Type[1] ≝ 43 { spp :> params 43 { spp :> params_ 44 44 ; more_sem_pars :> more_sem_params spp 45 45 }. … … 54 54 }. 55 55 56 definition genv ≝ λ p:params.λglobals. (genv_t Genv) (joint_function p globals).56 definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p). 57 57 58 58 (* … … 63 63 *) 64 64 65 record more_sem_params2 ( p: params) (globals: list ident): Type[1] ≝65 record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝ 66 66 { more_sparams:> more_sem_params p 67 67 … … 71 71 ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val 72 72 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))) 74 74 }. 75 75 76 76 record sem_params2 (globals: list ident): Type[1] ≝ 77 { p2:> params 78 ; more_sparams2:> more_sem_params2 p2 globals77 { p2:> params globals 78 ; more_sparams2:> more_sem_params2 globals p2 79 79 }. 80 80 … … 82 82 coercion sem_params_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params 83 83 ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params. 84 84 (* 85 85 unification hint 0 ≔ globals: (list ident), p: sem_params2 globals; 86 86 S ≟ sem_params_of_sem_params2 globals p … … 89 89 (more_sparams (p2 globals p) globals 90 90 (more_sparams2 globals p)))) ≡ spp__o__pars_ S. 91 91 *) 92 92 definition address_of_label: sem_params → label → address. 93 93 #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label … p l))) … … 211 211 coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?. 212 212 213 definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv p globals→ state p → IO io_out io_in (trace × (state p)) ≝213 definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝ 214 214 λglobals,p,ge,st. 215 215 ! s ← fetch_statement … st; … … 336 336 ; exit: address 337 337 ; registersno: nat 338 ; genv2: genv sparams2 globals338 ; genv2: genv globals sparams2 339 339 }. 340 340 … … 345 345 346 346 definition 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)). 348 348 joint_program pars → evaluation_parameters 349 349 ≝ 350 350 λpars,sparams. 351 351 (λ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*) ] 353 353 qed. 354 354 355 355 definition 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))) ≝ 358 358 λpars,sparams,p. 359 359 let ge ≝ genv2 (make_global pars sparams p) in … … 376 376 377 377 definition 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)). 380 380 fullexec io_out io_in ≝ 381 381 λpars,sparams.
Note: See TracChangeset
for help on using the changeset viewer.