Changeset 3546

Timestamp:

Mar 20, 2015, 4:14:52 PM (6 years ago)

Author:

pellitta

Message:

abitato record semantico

File:

• LTS/imp.ma (modified) (1 diff)

LTS/imp.ma

@@ -465 +465 @@
 ].
 
+definition imp_return_call:(return_type imp_state_params)→ imp_store→ (option imp_store)≝
+λr,s.match s with [nil⇒ None ?
+|cons hd tl⇒ match hd with
+  [mk_Prod env v ⇒ match (sem_expr env r) with
+    [None ⇒ None ?
+    |Some n⇒ Some ? (cons ? (mk_Prod …(assign env v n) v) tl)
+    ]
+  ]
+].
+
+definition imp_init_store: (store_type imp_state_params)≝(mk_Prod DeqEnv variable (nil ?) O)::(nil ?).
+
+
 definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params imp_state_params imp_eval_seq imp_eval_io
-imp_eval_cond_cond imp_eval_loop_cond imp_eval_call ….
+imp_eval_cond_cond imp_eval_loop_cond imp_eval_call imp_return_call imp_init_store.