Changeset 3545
- Timestamp:
- Mar 19, 2015, 5:44:48 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/imp.ma
r3544 r3545 394 394 ] qed. 395 395 396 397 396 (* store is actually a stack of pairs 〈environment, return-variable〉 *) 398 definition imp_store:Type[0]≝mk_DeqSet store_t store_eq store_eq_equality. 399 400 definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params DeqEnv. 397 definition imp_store:DeqSet≝mk_DeqSet store_t store_eq store_eq_equality. 398 399 definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params imp_store (*DeqEnv*). 400 401 definition current_env:store_type imp_state_params→ option environment≝λs.match s with [nil⇒ None ? 402 |cons hd tl⇒ match hd with [(mk_Prod env var)⇒ Some ? env]]. 401 403 402 404 definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝λi,s.match i with 403 405 [sNop ⇒ Some ? s 404 |sAss v e ⇒ match (sem_expr s e) with [None ⇒ None ?| Some n⇒ Some ? (assign s v n)] 405 |sInc v ⇒ match (read s v) with [None ⇒ None ?|Some n⇒ Some ? (assign s v (S n))] 406 |sAss v e ⇒ match s with 407 [nil⇒ None ? 408 |cons hd tl⇒ match hd with 409 [(mk_Prod env var) ⇒ match (sem_expr env e) with 410 [None ⇒ None ? 411 | Some n⇒ Some ? (cons ? (mk_Prod ? ? (assign env v n) var) tl) 412 ] 413 ] 414 ] 415 |sInc v ⇒ match s with [nil⇒ None ?|cons hd tl⇒ match hd with [(mk_Prod env var)⇒ 416 match (read env v) with [None ⇒ None ?|Some n⇒ Some ? (cons ? (mk_Prod ? ? (assign env v (S n)) var) tl)]]] 406 417 ]. 407 418 … … 410 421 411 422 definition imp_eval_cond_cond:(cond_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝λc,s.match c with 412 [Eq e1 e2⇒ match (sem_expr s e1) with 413 [None⇒ None ? 414 |Some n ⇒ match (sem_expr s e2) with 423 [Eq e1 e2⇒ match (current_env s) with 424 [None ⇒ None ? 425 |Some env⇒ match (sem_expr env e1) with 426 [None⇒ None ? 427 |Some n ⇒ match (sem_expr env e2) with 428 [None ⇒ None ? 429 |Some m ⇒ Some ? (mk_Prod ?? (eqb n m) s)] 430 ] 431 ] 432 |Not e ⇒ match (current_env s) with 433 [None ⇒ None ? 434 |Some env⇒ match (sem_condition env e) with 415 435 [None ⇒ None ? 416 |Some m ⇒ Some ? (mk_Prod ?? (eqb n m) s)]417 ]418 |Not e ⇒ match (sem_condition s e) with [None ⇒ None ?|Some b ⇒ Some ? (mk_Prod ?? b s)]436 |Some b ⇒ Some ? (mk_Prod ?? b s) 437 ] 438 ] 419 439 ]. 420 440 … … 433 453 [lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]].*) 434 454 435 definition imp_eval_call:(signature imp_state_params imp_state_params)→ DeqExpr→ imp_store→ (option imp_store)≝455 definition imp_eval_call:(signature imp_state_params imp_state_params)→ expr→ imp_store→ (option imp_store)≝ 436 456 λsgn,e,st.match sgn with [mk_signature fun fpt rt ⇒ match st with 437 457 [nil ⇒ None ? … … 445 465 ]. 446 466 447 definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params …imp_eval_seq imp_eval_io448 imp_eval_cond_cond imp_eval_loop_cond ….467 definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params imp_state_params imp_eval_seq imp_eval_io 468 imp_eval_cond_cond imp_eval_loop_cond imp_eval_call …. 449 469 450 470
Note: See TracChangeset
for help on using the changeset viewer.