Changeset 3544

Timestamp:

Mar 19, 2015, 4:55:46 PM (5 years ago)

Author:

pellitta

Message:

record semantico: abitato eval_call

File:

• LTS/imp.ma (modified) (4 diffs)

LTS/imp.ma

@@ -174 +174 @@
   (* syntactical record *)
 
+definition DeqExpr:DeqSet≝(mk_DeqSet expr expr_eq expr_eq_equality).
+
 definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?.
 [@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality)
@@ -179 +181 @@
 |@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
 |@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
-|@(mk_DeqSet expr expr_eq expr_eq_equality)
+|@DeqExpr
 |@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.
 
@@ -336 +338 @@
 
 
-definition imp_env_params:env_params≝mk_env_params environment.
+definition imp_env_params:env_params≝mk_env_params variable.
 
 let rec env_eq (env1:environment) (env2:environment):bool≝match env1 with
@@ -425 +427 @@
 *)
 
+
+
 definition imp_eval_loop_cond:(loop_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝imp_eval_cond_cond.
 (*λl,s.match l with
 [lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]].*)
+
+definition imp_eval_call:(signature imp_state_params imp_state_params)→ DeqExpr→ imp_store→ (option imp_store)≝
+λsgn,e,st.match sgn with [mk_signature fun fpt rt ⇒ match st with
+  [nil ⇒ None ?
+  |cons hd tl⇒ match hd with
+    [mk_Prod env v ⇒ match (sem_expr env e) with
+      [None ⇒ None ?
+      |Some n⇒ Some ? (cons ? (mk_Prod … (assign default_env fpt n) v) st)
+      ]
+    ]
+  ]
+].
 
 definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params … imp_eval_seq imp_eval_io