Mercurial > cpdt > repo

comparison src/Intensional.v @ 182:24b99e025fe8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of Intensional
author Adam Chlipala <adamc@hcoop.net>
date Sun, 16 Nov 2008 11:54:51 -0500
parents
children 02569049397b
comparison
equal deleted inserted replaced
181:ec44782bffdd 182:24b99e025fe8
1 (* Copyright (c) 2008, Adam Chlipala
2 *
3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License.
6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *)
9
10 (* begin hide *)
11 Require Import String List.
12
13 Require Import Axioms Tactics DepList.
14
15 Set Implicit Arguments.
16 (* end hide *)
17
18
19 (** %\chapter{Intensional Transformations}% *)
20
21 (** TODO: Prose for this chapter *)
22
23
24 (** * Closure Conversion *)
25
26 Module Source.
27 Inductive type : Type :=
28 | TNat : type
29 | Arrow : type -> type -> type.
30
31 Notation "'Nat'" := TNat : source_scope.
32 Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
33
34 Open Scope source_scope.
35 Bind Scope source_scope with type.
36 Delimit Scope source_scope with source.
37
38 Section vars.
39 Variable var : type -> Type.
40
41 Inductive exp : type -> Type :=
42 | Var : forall t,
43 var t
44 -> exp t
45
46 | Const : nat -> exp Nat
47 | Plus : exp Nat -> exp Nat -> exp Nat
48
49 | App : forall t1 t2,
50 exp (t1 --> t2)
51 -> exp t1
52 -> exp t2
53 | Abs : forall t1 t2,
54 (var t1 -> exp t2)
55 -> exp (t1 --> t2).
56 End vars.
57
58 Definition Exp t := forall var, exp var t.
59
60 Implicit Arguments Var [var t].
61 Implicit Arguments Const [var].
62 Implicit Arguments Plus [var].
63 Implicit Arguments App [var t1 t2].
64 Implicit Arguments Abs [var t1 t2].
65
66 Notation "# v" := (Var v) (at level 70) : source_scope.
67
68 Notation "^ n" := (Const n) (at level 70) : source_scope.
69 Infix "+^" := Plus (left associativity, at level 79) : source_scope.
70
71 Infix "@" := App (left associativity, at level 77) : source_scope.
72 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
73 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope.
74
75 Bind Scope source_scope with exp.
76
77 Definition zero : Exp Nat := fun _ => ^0.
78 Definition one : Exp Nat := fun _ => ^1.
79 Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
80 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
81 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
82 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
83 \f, \x, #f @ #x.
84 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
85
86 Fixpoint typeDenote (t : type) : Set :=
87 match t with
88 | Nat => nat
89 | t1 --> t2 => typeDenote t1 -> typeDenote t2
90 end.
91
92 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
93 match e in (exp _ t) return (typeDenote t) with
94 | Var _ v => v
95
96 | Const n => n
97 | Plus e1 e2 => expDenote e1 + expDenote e2
98
99 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
100 | Abs _ _ e' => fun x => expDenote (e' x)
101 end.
102
103 Definition ExpDenote t (e : Exp t) := expDenote (e _).
104
105 Section exp_equiv.
106 Variables var1 var2 : type -> Type.
107
108 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop :=
109 | EqVar : forall G t (v1 : var1 t) v2,
110 In (existT _ t (v1, v2)) G
111 -> exp_equiv G (#v1) (#v2)
112
113 | EqConst : forall G n,
114 exp_equiv G (^n) (^n)
115 | EqPlus : forall G x1 y1 x2 y2,
116 exp_equiv G x1 x2
117 -> exp_equiv G y1 y2
118 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
119
120 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
121 exp_equiv G f1 f2
122 -> exp_equiv G x1 x2
123 -> exp_equiv G (f1 @ x1) (f2 @ x2)
124 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
125 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
126 -> exp_equiv G (Abs f1) (Abs f2).
127 End exp_equiv.
128
129 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
130 exp_equiv nil (E var1) (E var2).
131 End Source.
132
133 Section Closed.
134 Inductive type : Type :=
135 | TNat : type
136 | Arrow : type -> type -> type
137 | Code : type -> type -> type -> type
138 | Prod : type -> type -> type
139 | TUnit : type.
140
141 Notation "'Nat'" := TNat : cc_scope.
142 Notation "'Unit'" := TUnit : cc_scope.
143 Infix "-->" := Arrow (right associativity, at level 60) : cc_scope.
144 Infix "**" := Prod (right associativity, at level 59) : cc_scope.
145 Notation "env @@ dom ---> ran" := (Code env dom ran) (no associativity, at level 62, dom at next level) : cc_scope.
146
147 Bind Scope cc_scope with type.
148 Delimit Scope cc_scope with cc.
149
150 Open Local Scope cc_scope.
151
152 Section vars.
153 Variable var : type -> Set.
154
155 Inductive exp : type -> Type :=
156 | Var : forall t,
157 var t
158 -> exp t
159
160 | Const : nat -> exp Nat
161 | Plus : exp Nat -> exp Nat -> exp Nat
162
163 | App : forall dom ran,
164 exp (dom --> ran)
165 -> exp dom
166 -> exp ran
167
168 | Pack : forall env dom ran,
169 exp (env @@ dom ---> ran)
170 -> exp env
171 -> exp (dom --> ran)
172
173 | EUnit : exp Unit
174
175 | Pair : forall t1 t2,
176 exp t1
177 -> exp t2
178 -> exp (t1 ** t2)
179 | Fst : forall t1 t2,
180 exp (t1 ** t2)
181 -> exp t1
182 | Snd : forall t1 t2,
183 exp (t1 ** t2)
184 -> exp t2.
185
186 Section funcs.
187 Variable T : Type.
188
189 Inductive funcs : Type :=
190 | Main : T -> funcs
191 | Abs : forall env dom ran,
192 (var env -> var dom -> exp ran)
193 -> (var (env @@ dom ---> ran) -> funcs)
194 -> funcs.
195 End funcs.
196
197 Definition prog t := funcs (exp t).
198 End vars.
199
200 Implicit Arguments Var [var t].
201 Implicit Arguments Const [var].
202 Implicit Arguments EUnit [var].
203 Implicit Arguments Fst [var t1 t2].
204 Implicit Arguments Snd [var t1 t2].
205
206 Implicit Arguments Main [var T].
207 Implicit Arguments Abs [var T env dom ran].
208
209 Notation "# v" := (Var v) (at level 70) : cc_scope.
210
211 Notation "^ n" := (Const n) (at level 70) : cc_scope.
212 Infix "+^" := Plus (left associativity, at level 79) : cc_scope.
213
214 Infix "@@" := App (no associativity, at level 75) : cc_scope.
215 Infix "##" := Pack (no associativity, at level 71) : cc_scope.
216
217 Notation "()" := EUnit : cc_scope.
218
219 Notation "[ x1 , x2 ]" := (Pair x1 x2) (at level 73) : cc_scope.
220 Notation "#1 x" := (Fst x) (at level 72) : cc_scope.
221 Notation "#2 x" := (Snd x) (at level 72) : cc_scope.
222
223 Notation "f <= \\ x , y , e ; fs" :=
224 (Abs (fun x y => e) (fun f => fs))
225 (right associativity, at level 80, e at next level) : cc_scope.
226
227 Bind Scope cc_scope with exp funcs prog.
228
229 Fixpoint typeDenote (t : type) : Set :=
230 match t with
231 | Nat => nat
232 | Unit => unit
233 | dom --> ran => typeDenote dom -> typeDenote ran
234 | t1 ** t2 => typeDenote t1 * typeDenote t2
235 | env @@ dom ---> ran => typeDenote env -> typeDenote dom -> typeDenote ran
236 end%type.
237
238 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
239 match e in (exp _ t) return (typeDenote t) with
240 | Var _ v => v
241
242 | Const n => n
243 | Plus e1 e2 => expDenote e1 + expDenote e2
244
245 | App _ _ f x => (expDenote f) (expDenote x)
246 | Pack _ _ _ f env => (expDenote f) (expDenote env)
247
248 | EUnit => tt
249
250 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
251 | Fst _ _ e' => fst (expDenote e')
252 | Snd _ _ e' => snd (expDenote e')
253 end.
254
255 Fixpoint funcsDenote T (fs : funcs typeDenote T) : T :=
256 match fs with
257 | Main v => v
258 | Abs _ _ _ e fs =>
259 funcsDenote (fs (fun env arg => expDenote (e env arg)))
260 end.
261
262 Definition progDenote t (p : prog typeDenote t) : typeDenote t :=
263 expDenote (funcsDenote p).
264
265 Definition Exp t := forall var, exp var t.
266 Definition Prog t := forall var, prog var t.
267
268 Definition ExpDenote t (E : Exp t) := expDenote (E _).
269 Definition ProgDenote t (P : Prog t) := progDenote (P _).
270 End Closed.
271