Changeset 3528

Timestamp:

Mar 12, 2015, 12:58:43 PM (5 years ago)

Author:

pellitta

Message:

eliminati dal linguaggio i comandi For e IfThenElse?, ridondanti rispetto a While e IfThenElse? generalizzato o IfThenElseList? (rinominato semplicemente IfThenElse?)

File:

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

LTS/imp.ma

@@ -13 +13 @@
 (**************************************************************************)
 
-(*include "basics/chapter5.ma".*)
 include "basics/lists/list.ma".
 include "arithmetics/nat.ma".
@@ -32 +31 @@
  | Not: condition → condition.
 
+(* | IfThenElse: condition → command → command → command*)
+(* | For: variable → expr → list command → command*)
 inductive command: Type[0] ≝
    Nop: command 
  | Ass: variable → expr → command
  | Inc: variable → command
- | IfThenElse: condition → command → command → command
- | IfThenElseList: condition → list command → list command → command
+ | IfThenElse: condition → list command → list command → command
  | While: condition → list command → command
- | For: variable → expr → list command → command
  | Call: variable → expr → function → command
  | Return: expr → command
 with function: Type[0] ≝
- | Fun: variable → list command → function
- .
+ | Fun: variable → list command → function.
 
 definition program ≝ list command.
@@ -113 +111 @@
 definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1).
 
+(* | mIfThenElse1:
+   ∀env,st,cond,c1,c2,cont.
+    sem_condition env cond = true →
+    moves ((IfThenElse cond c1 c2)::cont) env st (c1::cont) env st
+ | mIfThenElse2:
+   ∀env,st,cond,c1,c2,cont.
+    sem_condition env cond = false →
+    moves ((IfThenElse cond c1 c2)::cont) env st (c2::cont) env st
+*)
+(* | mFor1:
+    ∀env,st,v,e,l,cont.
+    (sem_condition env (Lt (Var v) e))=true 
+       → moves ((For v e l)::cont) env st (l@((Inc v)::(For v e l)::cont)) env st
+ | mFor2:
+    ∀env,st,v,e,l,cont.
+    (sem_condition env (Lt (Var v) e ))=false
+     → moves ((For v e l)::cont) env st cont env st
+*)
+
 inductive moves: list command → environment → stack → list command → environment → stack → Prop ≝
    mNop: ∀env,st,cont. moves (Nop::cont) env st cont env st
  | mAss: ∀env,st,v,e,cont.moves ((Ass v e)::cont) env st cont (assign env v (sem_expr env e)) st
- | mInc: ∀env,st,v,cont.moves ((Inc v)::cont) env st cont 
- (increment env v)
-(* (assign env v
-  (sem_expr env (Plus (Var v) (Const 1))))*)
-  
-  st
-(* | mInc: ∀env,v. moves (Inc v) env (increment env v) *)
+ | mInc: ∀env,st,v,cont.moves ((Inc v)::cont) env st cont (increment env v) st
  | mIfThenElse1:
-   ∀env,st,cond,c1,c2,cont.
-    sem_condition env cond = true (* → moves (c1::cont) env st cont env' st *)→
-    moves ((IfThenElse cond c1 c2)::cont) env st (c1::cont) env st
+   ∀env,st,cond,l1,l2,cont.
+    sem_condition env cond = true  → 
+    moves ((IfThenElse cond l1 l2)::cont) env st (l1@cont) env st
  | mIfThenElse2:
-   ∀env,st,cond,c1,c2,cont.
-    sem_condition env cond = false (* → moves (c2::cont) env st cont env' st *)→
-    moves ((IfThenElse cond c1 c2)::cont) env st (c2::cont) env st
- | mIfThenElseList1:
    ∀env,st,cond,l1,l2,cont.
-    sem_condition env cond = true (* → moves (l1@cont) env st cont env' st *) → 
-    moves ((IfThenElseList cond l1 l2)::cont) env st (l1@cont) env st
- | mIfThenElseList2:
-   ∀env,st,cond,l1,l2,cont.
-    sem_condition env cond = false (* → moves (l2@cont) env st cont env' st*) → 
-    moves ((IfThenElseList cond l1 l2)::cont) env st (l2@cont) env st
+    sem_condition env cond = false → 
+    moves ((IfThenElse cond l1 l2)::cont) env st (l2@cont) env st
  | mWhile1:
    ∀env,st,cond,l,cont.
@@ -147 +150 @@
     sem_condition env cond = false →
     moves ((While cond l)::cont) env st cont env st
- | mFor1: (* entra nel for *)
-    ∀env,st,v,e,l,cont.
-    (sem_condition env (Lt (Var v) e))=true 
-       → moves ((For v e l)::cont) env st (l@((Inc v)::(For v e l)::cont)) env st
- | mFor2: (* non entra nel for *)
-    ∀env,st,v,e,l,cont.
-    (sem_condition env (Lt (Var v) e ))=false(*(sem_condition env (Eq (Minus (Var v) e) (Const 0)))=true*) (* v>=e *)
-     → moves ((For v e l)::cont) env st cont env st
- | mCall: (* CALL v e f *)
+ | mCall: 
     ∀env,st,v,e,cont.∀v',l.
     moves ((Call v e (Fun v' l))::cont) env st l (assign default_env v' (sem_expr env e)) (push st (mk_Prod ? ? v (mk_Prod ? ? cont env)))
- | mReturn:  (* Return e *)
+ | mReturn:
     ∀env,env',st,v,e,cont,cont'.
     moves ((Return e)::cont) env ((mk_Prod ? ? v (mk_Prod ? ? cont' env'))::st) ((Ass v e)::cont') env' st.