Changeset 3545

Timestamp:

Mar 19, 2015, 5:44:48 PM (6 years ago)

Author:

pellitta

Message:

risolto un problema di mismatch di tipo legato al fatto che lo store precedentemente era un ambiente e non uno stack di coppie ambiente variabile di ritorno

File:

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

LTS/imp.ma

@@ -394 +394 @@
 ] qed.
 
-
 (* store is actually a stack of pairs 〈environment, return-variable〉 *)
-definition imp_store:Type[0]≝mk_DeqSet store_t store_eq store_eq_equality.
-
-definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params DeqEnv.
+definition imp_store:DeqSet≝mk_DeqSet store_t store_eq store_eq_equality.
+
+definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params imp_store (*DeqEnv*).
+
+definition current_env:store_type imp_state_params→ option environment≝λs.match s with [nil⇒ None ?
+|cons hd tl⇒ match hd with [(mk_Prod env var)⇒ Some ? env]].
 
 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
 [sNop ⇒ Some ? s
-|sAss v e ⇒ match (sem_expr s e) with [None ⇒ None ?| Some n⇒ Some ? (assign s v n)]
-|sInc v ⇒ match (read s v) with [None ⇒ None ?|Some n⇒ Some ? (assign s v (S n))]
+|sAss v e ⇒ match s with
+  [nil⇒ None ?
+  |cons hd tl⇒ match hd with
+    [(mk_Prod env var) ⇒ match (sem_expr env e) with
+      [None ⇒ None ?
+      | Some n⇒ Some ? (cons ? (mk_Prod ? ? (assign env v n) var) tl)
+      ]
+    ]
+  ]
+|sInc v ⇒ match s with [nil⇒ None ?|cons hd tl⇒ match hd with [(mk_Prod env var)⇒ 
+match (read env v) with [None ⇒ None ?|Some n⇒ Some ? (cons ? (mk_Prod ? ? (assign env v (S n)) var) tl)]]]
 ].
 
@@ -410 +421 @@
 
 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
-[Eq e1 e2⇒ match (sem_expr s e1) with
-  [None⇒ None ?
-  |Some n ⇒ match (sem_expr s e2) with
+[Eq e1 e2⇒ match (current_env s) with
+  [None ⇒ None ?
+  |Some env⇒ match (sem_expr env e1) with 
+    [None⇒ None ?
+    |Some n ⇒ match (sem_expr env e2) with
+      [None ⇒ None ?
+      |Some m ⇒ Some ? (mk_Prod ?? (eqb n m) s)]
+    ]
+  ]
+|Not e ⇒ match (current_env s) with
+  [None ⇒ None ?
+  |Some env⇒ match (sem_condition env e) with
     [None ⇒ None ?
-    |Some m ⇒ Some ? (mk_Prod ?? (eqb n m) s)]
-  ]
-|Not e ⇒ match (sem_condition s e) with [None ⇒ None ?|Some b ⇒ Some ? (mk_Prod ?? b s)]
+    |Some b ⇒ Some ? (mk_Prod ?? b s)
+    ]
+  ]
 ].
 
@@ -433 +453 @@
 [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)≝
+definition imp_eval_call:(signature imp_state_params imp_state_params)→ expr→ imp_store→ (option imp_store)≝
 λsgn,e,st.match sgn with [mk_signature fun fpt rt ⇒ match st with
   [nil ⇒ None ?
@@ -445 +465 @@
 ].
 
-definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params … imp_eval_seq imp_eval_io
-imp_eval_cond_cond imp_eval_loop_cond ….
+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 ….