Mercurial > cpdt > repo
comparison src/Intensional.v @ 182:24b99e025fe8
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 |