Changeset 3528 for LTS/imp.ma


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3526 r3528  
    1313(**************************************************************************)
    1414
    15 (*include "basics/chapter5.ma".*)
    1615include "basics/lists/list.ma".
    1716include "arithmetics/nat.ma".
     
    3231 | Not: condition → condition.
    3332
     33(* | IfThenElse: condition → command → command → command*)
     34(* | For: variable → expr → list command → command*)
    3435inductive command: Type[0] ≝
    3536   Nop: command
    3637 | Ass: variable → expr → command
    3738 | Inc: variable → command
    38  | IfThenElse: condition → command → command → command
    39  | IfThenElseList: condition → list command → list command → command
     39 | IfThenElse: condition → list command → list command → command
    4040 | While: condition → list command → command
    41  | For: variable → expr → list command → command
    4241 | Call: variable → expr → function → command
    4342 | Return: expr → command
    4443with function: Type[0] ≝
    45  | Fun: variable → list command → function
    46  .
     44 | Fun: variable → list command → function.
    4745
    4846definition program ≝ list command.
     
    113111definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1).
    114112
     113(* | mIfThenElse1:
     114   ∀env,st,cond,c1,c2,cont.
     115    sem_condition env cond = true →
     116    moves ((IfThenElse cond c1 c2)::cont) env st (c1::cont) env st
     117 | mIfThenElse2:
     118   ∀env,st,cond,c1,c2,cont.
     119    sem_condition env cond = false →
     120    moves ((IfThenElse cond c1 c2)::cont) env st (c2::cont) env st
     121*)
     122(* | mFor1:
     123    ∀env,st,v,e,l,cont.
     124    (sem_condition env (Lt (Var v) e))=true
     125       → moves ((For v e l)::cont) env st (l@((Inc v)::(For v e l)::cont)) env st
     126 | mFor2:
     127    ∀env,st,v,e,l,cont.
     128    (sem_condition env (Lt (Var v) e ))=false
     129     → moves ((For v e l)::cont) env st cont env st
     130*)
     131
    115132inductive moves: list command → environment → stack → list command → environment → stack → Prop ≝
    116133   mNop: ∀env,st,cont. moves (Nop::cont) env st cont env st
    117134 | mAss: ∀env,st,v,e,cont.moves ((Ass v e)::cont) env st cont (assign env v (sem_expr env e)) st
    118  | mInc: ∀env,st,v,cont.moves ((Inc v)::cont) env st cont
    119  (increment env v)
    120 (* (assign env v
    121   (sem_expr env (Plus (Var v) (Const 1))))*)
    122  
    123   st
    124 (* | mInc: ∀env,v. moves (Inc v) env (increment env v) *)
     135 | mInc: ∀env,st,v,cont.moves ((Inc v)::cont) env st cont (increment env v) st
    125136 | mIfThenElse1:
    126    ∀env,st,cond,c1,c2,cont.
    127     sem_condition env cond = true (* → moves (c1::cont) env st cont env' st *)→
    128     moves ((IfThenElse cond c1 c2)::cont) env st (c1::cont) env st
     137   ∀env,st,cond,l1,l2,cont.
     138    sem_condition env cond = true  →
     139    moves ((IfThenElse cond l1 l2)::cont) env st (l1@cont) env st
    129140 | mIfThenElse2:
    130    ∀env,st,cond,c1,c2,cont.
    131     sem_condition env cond = false (* → moves (c2::cont) env st cont env' st *)→
    132     moves ((IfThenElse cond c1 c2)::cont) env st (c2::cont) env st
    133  | mIfThenElseList1:
    134141   ∀env,st,cond,l1,l2,cont.
    135     sem_condition env cond = true (* → moves (l1@cont) env st cont env' st *) →
    136     moves ((IfThenElseList cond l1 l2)::cont) env st (l1@cont) env st
    137  | mIfThenElseList2:
    138    ∀env,st,cond,l1,l2,cont.
    139     sem_condition env cond = false (* → moves (l2@cont) env st cont env' st*) →
    140     moves ((IfThenElseList cond l1 l2)::cont) env st (l2@cont) env st
     142    sem_condition env cond = false →
     143    moves ((IfThenElse cond l1 l2)::cont) env st (l2@cont) env st
    141144 | mWhile1:
    142145   ∀env,st,cond,l,cont.
     
    147150    sem_condition env cond = false →
    148151    moves ((While cond l)::cont) env st cont env st
    149  | mFor1: (* entra nel for *)
    150     ∀env,st,v,e,l,cont.
    151     (sem_condition env (Lt (Var v) e))=true
    152        → moves ((For v e l)::cont) env st (l@((Inc v)::(For v e l)::cont)) env st
    153  | mFor2: (* non entra nel for *)
    154     ∀env,st,v,e,l,cont.
    155     (sem_condition env (Lt (Var v) e ))=false(*(sem_condition env (Eq (Minus (Var v) e) (Const 0)))=true*) (* v>=e *)
    156      → moves ((For v e l)::cont) env st cont env st
    157  | mCall: (* CALL v e f *)
     152 | mCall:
    158153    ∀env,st,v,e,cont.∀v',l.
    159154    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)))
    160  | mReturn:  (* Return e *)
     155 | mReturn:
    161156    ∀env,env',st,v,e,cont,cont'.
    162157    moves ((Return e)::cont) env ((mk_Prod ? ? v (mk_Prod ? ? cont' env'))::st) ((Ass v e)::cont') env' st.
Note: See TracChangeset for help on using the changeset viewer.