Changeset 3546 for LTS/imp.ma


Ignore:
Timestamp:
Mar 20, 2015, 4:14:52 PM (5 years ago)
Author:
pellitta
Message:

abitato record semantico

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3545 r3546  
    465465].
    466466
     467definition 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
     477definition imp_init_store: (store_type imp_state_params)≝(mk_Prod DeqEnv variable (nil ?) O)::(nil ?).
     478
     479
    467480definition 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 .
     481imp_eval_cond_cond imp_eval_loop_cond imp_eval_call imp_return_call imp_init_store.
    469482
    470483
Note: See TracChangeset for help on using the changeset viewer.