Mercurial > cpdt > repo

comparison src/Impure.v @ 204:cbf2f74a5130

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parts I want to keep compile with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 10:52:43 -0500
parents 32ce9b28d7e7
children 2a34c4dc6a10
comparison
equal deleted inserted replaced
203:71ade09024ac 204:cbf2f74a5130
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *)
11 Require Import Arith List Omega.
12
13 Require Import Axioms Tactics.
14
15 Set Implicit Arguments.
16 (* end hide *)
17 10
18 11
19 (** %\chapter{Modeling Impure Languages}% *) 12 (** %\chapter{Modeling Impure Languages}% *)
20 13
21 (** TODO: Prose for this chapter *) 14 (** TODO: This chapter! (Old version was too impredicative) *)
22
23 Section var.
24 Variable var : Type.
25
26 Inductive term : Type :=
27 | Var : var -> term
28 | App : term -> term -> term
29 | Abs : (var -> term) -> term
30 | Unit : term.
31 End var.
32
33 Implicit Arguments Unit [var].
34
35 Notation "# v" := (Var v) (at level 70).
36 Notation "()" := Unit.
37
38 Infix "@" := App (left associativity, at level 72).
39 Notation "\ x , e" := (Abs (fun x => e)) (at level 73).
40 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 73).
41
42 Definition Term := forall var, term var.
43
44 Definition ident : Term := fun _ => \x, #x.
45 Definition unite : Term := fun _ => ().
46 Definition ident_self : Term := fun _ => ident _ @ ident _.
47 Definition ident_unit : Term := fun _ => ident _ @ unite _.
48
49
50 Module impredicative.
51 Inductive dynamic : Set :=
52 | Dyn : forall (dynTy : Type), dynTy -> dynamic.
53
54 Inductive computation (T : Type) : Set :=
55 | Return : T -> computation T
56 | Bind : forall (T' : Type),
57 computation T' -> (T' -> computation T) -> computation T
58 | Unpack : dynamic -> computation T.
59
60 Inductive eval : forall T, computation T -> T -> Prop :=
61 | EvalReturn : forall T (v : T),
62 eval (Return v) v
63 | EvalUnpack : forall T (v : T),
64 eval (Unpack T (Dyn v)) v
65 | EvalBind : forall T1 T2 (c1 : computation T1) (c2 : T1 -> computation T2) v1 v2,
66 eval c1 v1
67 -> eval (c2 v1) v2
68 -> eval (Bind c1 c2) v2.
69
70 (* begin thide *)
71 Fixpoint termDenote (e : term dynamic) : computation dynamic :=
72 match e with
73 | Var v => Return v
74 | App e1 e2 => Bind (termDenote e1) (fun f =>
75 Bind (termDenote e2) (fun x =>
76 Bind (Unpack (dynamic -> computation dynamic) f) (fun f' =>
77 f' x)))
78 | Abs e' => Return (Dyn (fun x => termDenote (e' x)))
79
80 | Unit => Return (Dyn tt)
81 end.
82 (* end thide *)
83
84 Definition TermDenote (E : Term) := termDenote (E _).
85
86 Eval compute in TermDenote ident.
87 Eval compute in TermDenote unite.
88 Eval compute in TermDenote ident_self.
89 Eval compute in TermDenote ident_unit.
90
91 Theorem eval_ident_unit : eval (TermDenote ident_unit) (Dyn tt).
92 (* begin thide *)
93 compute.
94 repeat econstructor.
95 simpl.
96 constructor.
97 Qed.
98 (* end thide *)
99
100 Theorem invert_ident : forall (E : Term) d,
101 eval (TermDenote (fun _ => ident _ @ E _)) d
102 -> eval (TermDenote E) d.
103 (* begin thide *)
104 inversion 1.
105
106 crush.
107
108 Focus 3.
109 crush.
110 unfold TermDenote in H0.
111 simpl in H0.
112 (** [injection H0.] *)
113 Abort.
114 (* end thide *)
115
116 End impredicative.
117
118
119 Module predicative.
120
121 Inductive val : Type :=
122 | Func : nat -> val
123 | VUnit.
124
125 Inductive computation : Type :=
126 | Return : val -> computation
127 | Bind : computation -> (val -> computation) -> computation
128 | CAbs : (val -> computation) -> computation
129 | CApp : val -> val -> computation.
130
131 Definition func := val -> computation.
132
133 Fixpoint get (n : nat) (ls : list func) {struct ls} : option func :=
134 match ls with
135 | nil => None
136 | x :: ls' =>
137 if eq_nat_dec n (length ls')
138 then Some x
139 else get n ls'
140 end.
141
142 Inductive eval : list func -> computation -> list func -> val -> Prop :=
143 | EvalReturn : forall ds d,
144 eval ds (Return d) ds d
145 | EvalBind : forall ds c1 c2 ds' d1 ds'' d2,
146 eval ds c1 ds' d1
147 -> eval ds' (c2 d1) ds'' d2
148 -> eval ds (Bind c1 c2) ds'' d2
149 | EvalCAbs : forall ds f,
150 eval ds (CAbs f) (f :: ds) (Func (length ds))
151 | EvalCApp : forall ds i d2 f ds' d3,
152 get i ds = Some f
153 -> eval ds (f d2) ds' d3
154 -> eval ds (CApp (Func i) d2) ds' d3.
155
156 (* begin thide *)
157 Fixpoint termDenote (e : term val) : computation :=
158 match e with
159 | Var v => Return v
160 | App e1 e2 => Bind (termDenote e1) (fun f =>
161 Bind (termDenote e2) (fun x =>
162 CApp f x))
163 | Abs e' => CAbs (fun x => termDenote (e' x))
164
165 | Unit => Return VUnit
166 end.
167 (* end thide *)
168
169 Definition TermDenote (E : Term) := termDenote (E _).
170
171 Eval compute in TermDenote ident.
172 Eval compute in TermDenote unite.
173 Eval compute in TermDenote ident_self.
174 Eval compute in TermDenote ident_unit.
175
176 Theorem eval_ident_unit : exists ds, eval nil (TermDenote ident_unit) ds VUnit.
177 (* begin thide *)
178 compute.
179 repeat econstructor.
180 simpl.
181 rewrite (eta Return).
182 reflexivity.
183 Qed.
184
185 Hint Constructors eval.
186
187 Lemma app_nil_start : forall A (ls : list A),
188 ls = nil ++ ls.
189 reflexivity.
190 Qed.
191
192 Lemma app_cons : forall A (x : A) (ls : list A),
193 x :: ls = (x :: nil) ++ ls.
194 reflexivity.
195 Qed.
196
197 Theorem eval_monotone : forall ds c ds' d,
198 eval ds c ds' d
199 -> exists ds'', ds' = ds'' ++ ds.
200 Hint Resolve app_nil_start app_ass app_cons.
201
202 induction 1; firstorder; subst; eauto.
203 Qed.
204
205 Lemma length_app : forall A (ds2 ds1 : list A),
206 length (ds1 ++ ds2) = length ds1 + length ds2.
207 induction ds1; simpl; intuition.
208 Qed.
209
210 Lemma get_app : forall ds2 d ds1,
211 get (length ds2) (ds1 ++ d :: ds2) = Some d.
212 Hint Rewrite length_app : cpdt.
213
214 induction ds1; crush;
215 match goal with
216 | [ |- context[if ?E then _ else _] ] => destruct E
217 end; crush.
218 Qed.
219 (* end thide *)
220
221 Theorem invert_ident : forall (E : Term) ds ds' d,
222 eval ds (TermDenote (fun _ => ident _ @ E _)) ds' d
223 -> eval ((fun x => Return x) :: ds) (TermDenote E) ds' d.
224 (* begin thide *)
225 inversion 1; subst.
226 clear H.
227 inversion H3; clear H3; subst.
228 inversion H6; clear H6; subst.
229 generalize (eval_monotone H2); crush.
230 inversion H5; clear H5; subst.
231 rewrite get_app in H3.
232 inversion H3; clear H3; subst.
233 inversion H7; clear H7; subst.
234 assumption.
235 Qed.
236 (* end thide *)
237
238 End predicative.