Mercurial > cpdt > repo

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