Changeset 3546
- Timestamp:
- Mar 20, 2015, 4:14:52 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/imp.ma
r3545 r3546 465 465 ]. 466 466 467 definition imp_return_call:(return_type imp_state_params)→ imp_store→ (option imp_store)≝ 468 λr,s.match s with [nil⇒ None ? 469 |cons hd tl⇒ match hd with 470 [mk_Prod env v ⇒ match (sem_expr env r) with 471 [None ⇒ None ? 472 |Some n⇒ Some ? (cons ? (mk_Prod …(assign env v n) v) tl) 473 ] 474 ] 475 ]. 476 477 definition imp_init_store: (store_type imp_state_params)≝(mk_Prod DeqEnv variable (nil ?) O)::(nil ?). 478 479 467 480 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 ….481 imp_eval_cond_cond imp_eval_loop_cond imp_eval_call imp_return_call imp_init_store. 469 482 470 483
Note: See TracChangeset
for help on using the changeset viewer.