Mercurial > cpdt > repo

annotate src/Interps.v @ 171:b00b6a9b6b58

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PSLC
author Adam Chlipala <adamc@hcoop.net>
date Sun, 09 Nov 2008 13:59:51 -0500
parents f8353e2a21d6
children 653c03f6061e
rev   line source
adamc@170 1 (* Copyright (c) 2008, Adam Chlipala
adamc@170 2 *
adamc@170 3 * This work is licensed under a
adamc@170 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@170 5 * Unported License.
adamc@170 6 * The license text is available at:
adamc@170 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@170 8 *)
adamc@170 9
adamc@170 10 (* begin hide *)
adamc@170 11 Require Import String List.
adamc@170 12
adamc@170 13 Require Import Axioms Tactics.
adamc@170 14
adamc@170 15 Set Implicit Arguments.
adamc@170 16 (* end hide *)
adamc@170 17
adamc@170 18
adamc@170 19 (** %\chapter{Type-Theoretic Interpreters}% *)
adamc@170 20
adamc@170 21 (** TODO: Prose for this chapter *)
adamc@170 22
adamc@170 23
adamc@170 24 (** * Simply-Typed Lambda Calculus *)
adamc@170 25
adamc@170 26 Module STLC.
adamc@170 27 Inductive type : Type :=
adamc@170 28 | Nat : type
adamc@170 29 | Arrow : type -> type -> type.
adamc@170 30
adamc@170 31 Infix "-->" := Arrow (right associativity, at level 60).
adamc@170 32
adamc@170 33 Section vars.
adamc@170 34 Variable var : type -> Type.
adamc@170 35
adamc@170 36 Inductive exp : type -> Type :=
adamc@170 37 | Var : forall t,
adamc@170 38 var t
adamc@170 39 -> exp t
adamc@170 40
adamc@170 41 | Const : nat -> exp Nat
adamc@170 42 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@170 43
adamc@170 44 | App : forall t1 t2,
adamc@170 45 exp (t1 --> t2)
adamc@170 46 -> exp t1
adamc@170 47 -> exp t2
adamc@170 48 | Abs : forall t1 t2,
adamc@170 49 (var t1 -> exp t2)
adamc@170 50 -> exp (t1 --> t2).
adamc@170 51 End vars.
adamc@170 52
adamc@170 53 Definition Exp t := forall var, exp var t.
adamc@170 54
adamc@170 55 Implicit Arguments Var [var t].
adamc@170 56 Implicit Arguments Const [var].
adamc@170 57 Implicit Arguments Plus [var].
adamc@170 58 Implicit Arguments App [var t1 t2].
adamc@170 59 Implicit Arguments Abs [var t1 t2].
adamc@170 60
adamc@170 61 Notation "# v" := (Var v) (at level 70).
adamc@170 62
adamc@170 63 Notation "^ n" := (Const n) (at level 70).
adamc@171 64 Infix "+^" := Plus (left associativity, at level 79).
adamc@170 65
adamc@170 66 Infix "@" := App (left associativity, at level 77).
adamc@170 67 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@170 68 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@170 69
adamc@170 70 Fixpoint typeDenote (t : type) : Set :=
adamc@170 71 match t with
adamc@170 72 | Nat => nat
adamc@170 73 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@170 74 end.
adamc@170 75
adamc@170 76 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@170 77 match e in (exp _ t) return (typeDenote t) with
adamc@170 78 | Var _ v => v
adamc@170 79
adamc@170 80 | Const n => n
adamc@170 81 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@170 82
adamc@170 83 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@170 84 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@170 85 end.
adamc@170 86
adamc@170 87 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@170 88
adamc@170 89 Section cfold.
adamc@170 90 Variable var : type -> Type.
adamc@170 91
adamc@170 92 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
adamc@170 93 match e in exp _ t return exp _ t with
adamc@170 94 | Var _ v => #v
adamc@170 95
adamc@170 96 | Const n => ^n
adamc@170 97 | Plus e1 e2 =>
adamc@170 98 let e1' := cfold e1 in
adamc@170 99 let e2' := cfold e2 in
adamc@170 100 match e1', e2' with
adamc@170 101 | Const n1, Const n2 => ^(n1 + n2)
adamc@171 102 | _, _ => e1' +^ e2'
adamc@170 103 end
adamc@170 104
adamc@170 105 | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@170 106 | Abs _ _ e' => Abs (fun x => cfold (e' x))
adamc@170 107 end.
adamc@170 108 End cfold.
adamc@170 109
adamc@170 110 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@170 111
adamc@170 112 Lemma cfold_correct : forall t (e : exp _ t),
adamc@170 113 expDenote (cfold e) = expDenote e.
adamc@170 114 induction e; crush; try (ext_eq; crush);
adamc@170 115 repeat (match goal with
adamc@170 116 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@170 117 end; crush).
adamc@170 118 Qed.
adamc@170 119
adamc@170 120 Theorem Cfold_correct : forall t (E : Exp t),
adamc@170 121 ExpDenote (Cfold E) = ExpDenote E.
adamc@170 122 unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@170 123 Qed.
adamc@170 124 End STLC.
adamc@171 125
adamc@171 126
adamc@171 127 (** * Adding Products and Sums *)
adamc@171 128
adamc@171 129 Module PSLC.
adamc@171 130 Inductive type : Type :=
adamc@171 131 | Nat : type
adamc@171 132 | Arrow : type -> type -> type
adamc@171 133 | Prod : type -> type -> type
adamc@171 134 | Sum : type -> type -> type.
adamc@171 135
adamc@171 136 Infix "-->" := Arrow (right associativity, at level 62).
adamc@171 137 Infix "**" := Prod (right associativity, at level 61).
adamc@171 138 Infix "++" := Sum (right associativity, at level 60).
adamc@171 139
adamc@171 140 Section vars.
adamc@171 141 Variable var : type -> Type.
adamc@171 142
adamc@171 143 Inductive exp : type -> Type :=
adamc@171 144 | Var : forall t,
adamc@171 145 var t
adamc@171 146 -> exp t
adamc@171 147
adamc@171 148 | Const : nat -> exp Nat
adamc@171 149 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@171 150
adamc@171 151 | App : forall t1 t2,
adamc@171 152 exp (t1 --> t2)
adamc@171 153 -> exp t1
adamc@171 154 -> exp t2
adamc@171 155 | Abs : forall t1 t2,
adamc@171 156 (var t1 -> exp t2)
adamc@171 157 -> exp (t1 --> t2)
adamc@171 158
adamc@171 159 | Pair : forall t1 t2,
adamc@171 160 exp t1
adamc@171 161 -> exp t2
adamc@171 162 -> exp (t1 ** t2)
adamc@171 163 | Fst : forall t1 t2,
adamc@171 164 exp (t1 ** t2)
adamc@171 165 -> exp t1
adamc@171 166 | Snd : forall t1 t2,
adamc@171 167 exp (t1 ** t2)
adamc@171 168 -> exp t2
adamc@171 169
adamc@171 170 | Inl : forall t1 t2,
adamc@171 171 exp t1
adamc@171 172 -> exp (t1 ++ t2)
adamc@171 173 | Inr : forall t1 t2,
adamc@171 174 exp t2
adamc@171 175 -> exp (t1 ++ t2)
adamc@171 176 | SumCase : forall t1 t2 t,
adamc@171 177 exp (t1 ++ t2)
adamc@171 178 -> (var t1 -> exp t)
adamc@171 179 -> (var t2 -> exp t)
adamc@171 180 -> exp t.
adamc@171 181 End vars.
adamc@171 182
adamc@171 183 Definition Exp t := forall var, exp var t.
adamc@171 184
adamc@171 185 Implicit Arguments Var [var t].
adamc@171 186 Implicit Arguments Const [var].
adamc@171 187 Implicit Arguments Abs [var t1 t2].
adamc@171 188 Implicit Arguments Inl [var t1 t2].
adamc@171 189 Implicit Arguments Inr [var t1 t2].
adamc@171 190
adamc@171 191 Notation "# v" := (Var v) (at level 70).
adamc@171 192
adamc@171 193 Notation "^ n" := (Const n) (at level 70).
adamc@171 194 Infix "+^" := Plus (left associativity, at level 79).
adamc@171 195
adamc@171 196 Infix "@" := App (left associativity, at level 77).
adamc@171 197 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@171 198 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@171 199
adamc@171 200 Notation "[ e1 , e2 ]" := (Pair e1 e2).
adamc@171 201 Notation "#1 e" := (Fst e) (at level 75).
adamc@171 202 Notation "#2 e" := (Snd e) (at level 75).
adamc@171 203
adamc@171 204 Notation "'case' e 'of' x => e1 | y => e2" := (SumCase e (fun x => e1) (fun y => e2))
adamc@171 205 (at level 79).
adamc@171 206
adamc@171 207 Fixpoint typeDenote (t : type) : Set :=
adamc@171 208 match t with
adamc@171 209 | Nat => nat
adamc@171 210 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@171 211 | t1 ** t2 => typeDenote t1 * typeDenote t2
adamc@171 212 | t1 ++ t2 => typeDenote t1 + typeDenote t2
adamc@171 213 end%type.
adamc@171 214
adamc@171 215 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@171 216 match e in (exp _ t) return (typeDenote t) with
adamc@171 217 | Var _ v => v
adamc@171 218
adamc@171 219 | Const n => n
adamc@171 220 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@171 221
adamc@171 222 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@171 223 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@171 224
adamc@171 225 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@171 226 | Fst _ _ e' => fst (expDenote e')
adamc@171 227 | Snd _ _ e' => snd (expDenote e')
adamc@171 228
adamc@171 229 | Inl _ _ e' => inl _ (expDenote e')
adamc@171 230 | Inr _ _ e' => inr _ (expDenote e')
adamc@171 231 | SumCase _ _ _ e' e1 e2 =>
adamc@171 232 match expDenote e' with
adamc@171 233 | inl v => expDenote (e1 v)
adamc@171 234 | inr v => expDenote (e2 v)
adamc@171 235 end
adamc@171 236 end.
adamc@171 237
adamc@171 238 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@171 239
adamc@171 240 Section cfold.
adamc@171 241 Variable var : type -> Type.
adamc@171 242
adamc@171 243 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
adamc@171 244 match e in exp _ t return exp _ t with
adamc@171 245 | Var _ v => #v
adamc@171 246
adamc@171 247 | Const n => ^n
adamc@171 248 | Plus e1 e2 =>
adamc@171 249 let e1' := cfold e1 in
adamc@171 250 let e2' := cfold e2 in
adamc@171 251 match e1', e2' with
adamc@171 252 | Const n1, Const n2 => ^(n1 + n2)
adamc@171 253 | _, _ => e1' +^ e2'
adamc@171 254 end
adamc@171 255
adamc@171 256 | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@171 257 | Abs _ _ e' => Abs (fun x => cfold (e' x))
adamc@171 258
adamc@171 259 | Pair _ _ e1 e2 => [cfold e1, cfold e2]
adamc@171 260 | Fst _ _ e' => #1 (cfold e')
adamc@171 261 | Snd _ _ e' => #2 (cfold e')
adamc@171 262
adamc@171 263 | Inl _ _ e' => Inl (cfold e')
adamc@171 264 | Inr _ _ e' => Inr (cfold e')
adamc@171 265 | SumCase _ _ _ e' e1 e2 =>
adamc@171 266 case cfold e' of
adamc@171 267 x => cfold (e1 x)
adamc@171 268 | y => cfold (e2 y)
adamc@171 269 end.
adamc@171 270 End cfold.
adamc@171 271
adamc@171 272 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@171 273
adamc@171 274 Lemma cfold_correct : forall t (e : exp _ t),
adamc@171 275 expDenote (cfold e) = expDenote e.
adamc@171 276 induction e; crush; try (ext_eq; crush);
adamc@171 277 repeat (match goal with
adamc@171 278 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@171 279 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E
adamc@171 280 end; crush).
adamc@171 281 Qed.
adamc@171 282
adamc@171 283 Theorem Cfold_correct : forall t (E : Exp t),
adamc@171 284 ExpDenote (Cfold E) = ExpDenote E.
adamc@171 285 unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@171 286 Qed.
adamc@171 287 End PSLC.