Changeset 3528
- Timestamp:
- Mar 12, 2015, 12:58:43 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/imp.ma
r3526 r3528 13 13 (**************************************************************************) 14 14 15 (*include "basics/chapter5.ma".*)16 15 include "basics/lists/list.ma". 17 16 include "arithmetics/nat.ma". … … 32 31 | Not: condition → condition. 33 32 33 (* | IfThenElse: condition → command → command → command*) 34 (* | For: variable → expr → list command → command*) 34 35 inductive command: Type[0] ≝ 35 36 Nop: command 36 37 | Ass: variable → expr → command 37 38 | 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 40 40 | While: condition → list command → command 41 | For: variable → expr → list command → command42 41 | Call: variable → expr → function → command 43 42 | Return: expr → command 44 43 with function: Type[0] ≝ 45 | Fun: variable → list command → function 46 . 44 | Fun: variable → list command → function. 47 45 48 46 definition program ≝ list command. … … 113 111 definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1). 114 112 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 115 132 inductive moves: list command → environment → stack → list command → environment → stack → Prop ≝ 116 133 mNop: ∀env,st,cont. moves (Nop::cont) env st cont env st 117 134 | 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 125 136 | 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 st137 ∀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 129 140 | 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 st133 | mIfThenElseList1:134 141 ∀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 141 144 | mWhile1: 142 145 ∀env,st,cond,l,cont. … … 147 150 sem_condition env cond = false → 148 151 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: 158 153 ∀env,st,v,e,cont.∀v',l. 159 154 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: 161 156 ∀env,env',st,v,e,cont,cont'. 162 157 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.