Interps.v 10.4 KB
Newer Older
Adam Chlipala's avatar
Adam Chlipala committed
1
(* Copyright (c) 2008-2009, Adam Chlipala
Adam Chlipala's avatar
Adam Chlipala committed
2 3 4 5 6 7 8 9 10 11 12
 * 
 * This work is licensed under a
 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
 * Unported License.
 * The license text is available at:
 *   http://creativecommons.org/licenses/by-nc-nd/3.0/
 *)

(* begin hide *)
Require Import String List.

13
Require Import Axioms Tactics.
Adam Chlipala's avatar
Adam Chlipala committed
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63

Set Implicit Arguments.
(* end hide *)


(** %\chapter{Type-Theoretic Interpreters}% *)

(** TODO: Prose for this chapter *)


(** * Simply-Typed Lambda Calculus *)

Module STLC.
  Inductive type : Type :=
  | Nat : type
  | Arrow : type -> type -> type.

  Infix "-->" := Arrow (right associativity, at level 60).

  Section vars.
    Variable var : type -> Type.

    Inductive exp : type -> Type :=
    | Var : forall t,
      var t
      -> exp t

    | Const : nat -> exp Nat
    | Plus : exp Nat -> exp Nat -> exp Nat

    | App : forall t1 t2,
      exp (t1 --> t2)
      -> exp t1
      -> exp t2
    | Abs : forall t1 t2,
      (var t1 -> exp t2)
      -> exp (t1 --> t2).
  End vars.

  Definition Exp t := forall var, exp var t.

  Implicit Arguments Var [var t].
  Implicit Arguments Const [var].
  Implicit Arguments Plus [var].
  Implicit Arguments App [var t1 t2].
  Implicit Arguments Abs [var t1 t2].

  Notation "# v" := (Var v) (at level 70).

  Notation "^ n" := (Const n) (at level 70).
Adam Chlipala's avatar
Adam Chlipala committed
64
  Infix "+^" := Plus (left associativity, at level 79).
Adam Chlipala's avatar
Adam Chlipala committed
65 66 67 68 69

  Infix "@" := App (left associativity, at level 77).
  Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
  Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).

70 71 72 73 74 75 76 77 78
  Definition zero : Exp Nat := fun _ => ^0.
  Definition one : Exp Nat := fun _ => ^1.
  Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
  Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
  Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
  Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
    \f, \x, #f @ #x.
  Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.

Adam Chlipala's avatar
Adam Chlipala committed
79 80 81
  (* EX: Define an interpreter for [Exp]s. *)

(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
82 83 84 85 86 87
  Fixpoint typeDenote (t : type) : Set :=
    match t with
      | Nat => nat
      | t1 --> t2 => typeDenote t1 -> typeDenote t2
    end.

Adam Chlipala's avatar
Adam Chlipala committed
88 89
  Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
    match e with
Adam Chlipala's avatar
Adam Chlipala committed
90 91 92 93 94 95 96 97 98 99
      | Var _ v => v
        
      | Const n => n
      | Plus e1 e2 => expDenote e1 + expDenote e2
        
      | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
      | Abs _ _ e' => fun x => expDenote (e' x)
    end.

  Definition ExpDenote t (e : Exp t) := expDenote (e _).
Adam Chlipala's avatar
Adam Chlipala committed
100
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
101

102 103 104 105 106 107 108 109
  Eval compute in ExpDenote zero.
  Eval compute in ExpDenote one.
  Eval compute in ExpDenote zpo.
  Eval compute in ExpDenote ident.
  Eval compute in ExpDenote app_ident.
  Eval compute in ExpDenote app.
  Eval compute in ExpDenote app_ident'.

Adam Chlipala's avatar
Adam Chlipala committed
110 111 112
  (* EX: Define a constant-folding function for [Exp]s. *)

(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
113 114 115
  Section cfold.
    Variable var : type -> Type.

Adam Chlipala's avatar
Adam Chlipala committed
116 117
    Fixpoint cfold t (e : exp var t) : exp var t :=
      match e with
Adam Chlipala's avatar
Adam Chlipala committed
118 119 120 121 122 123
        | Var _ v => #v

        | Const n => ^n
        | Plus e1 e2 =>
          let e1' := cfold e1 in
          let e2' := cfold e2 in
124
          match e1', e2' return _ with
Adam Chlipala's avatar
Adam Chlipala committed
125
            | Const n1, Const n2 => ^(n1 + n2)
Adam Chlipala's avatar
Adam Chlipala committed
126
            | _, _ => e1' +^ e2'
Adam Chlipala's avatar
Adam Chlipala committed
127 128 129 130 131 132 133 134
          end

        | App _ _ e1 e2 => cfold e1 @ cfold e2
        | Abs _ _ e' => Abs (fun x => cfold (e' x))
      end.
  End cfold.

  Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
Adam Chlipala's avatar
Adam Chlipala committed
135 136 137
(* end thide *)

  (* EX: Prove the correctness of constant-folding. *)
Adam Chlipala's avatar
Adam Chlipala committed
138

Adam Chlipala's avatar
Adam Chlipala committed
139
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
140 141 142 143 144 145 146 147 148 149 150 151
  Lemma cfold_correct : forall t (e : exp _ t),
    expDenote (cfold e) = expDenote e.
    induction e; crush; try (ext_eq; crush);
      repeat (match goal with
                | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
              end; crush).
  Qed.

  Theorem Cfold_correct : forall t (E : Exp t),
    ExpDenote (Cfold E) = ExpDenote E.
    unfold ExpDenote, Cfold; intros; apply cfold_correct.
  Qed.
Adam Chlipala's avatar
Adam Chlipala committed
152
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
153
End STLC.
Adam Chlipala's avatar
Adam Chlipala committed
154 155 156 157 158


(** * Adding Products and Sums *)

Module PSLC.
Adam Chlipala's avatar
Adam Chlipala committed
159 160 161
  (* EX: Extend the development with products and sums. *)

(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
162 163 164 165 166
  Inductive type : Type :=
  | Nat : type
  | Arrow : type -> type -> type
  | Prod : type -> type -> type
  | Sum : type -> type -> type.
Adam Chlipala's avatar
Adam Chlipala committed
167
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
168 169 170 171 172

  Infix "-->" := Arrow (right associativity, at level 62).
  Infix "**" := Prod (right associativity, at level 61).
  Infix "++" := Sum (right associativity, at level 60).

Adam Chlipala's avatar
Adam Chlipala committed
173
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
  Section vars.
    Variable var : type -> Type.

    Inductive exp : type -> Type :=
    | Var : forall t,
      var t
      -> exp t

    | Const : nat -> exp Nat
    | Plus : exp Nat -> exp Nat -> exp Nat

    | App : forall t1 t2,
      exp (t1 --> t2)
      -> exp t1
      -> exp t2
    | Abs : forall t1 t2,
      (var t1 -> exp t2)
      -> exp (t1 --> t2)

    | Pair : forall t1 t2,
      exp t1
      -> exp t2
      -> exp (t1 ** t2)
    | Fst : forall t1 t2,
      exp (t1 ** t2)
      -> exp t1
    | Snd : forall t1 t2,
      exp (t1 ** t2)
      -> exp t2

    | Inl : forall t1 t2,
      exp t1
      -> exp (t1 ++ t2)
    | Inr : forall t1 t2,
      exp t2
      -> exp (t1 ++ t2)
    | SumCase : forall t1 t2 t,
      exp (t1 ++ t2)
      -> (var t1 -> exp t)
      -> (var t2 -> exp t)
      -> exp t.
  End vars.

  Definition Exp t := forall var, exp var t.
Adam Chlipala's avatar
Adam Chlipala committed
218
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
219 220 221 222 223 224 225 226 227 228

  Implicit Arguments Var [var t].
  Implicit Arguments Const [var].
  Implicit Arguments Abs [var t1 t2].
  Implicit Arguments Inl [var t1 t2].
  Implicit Arguments Inr [var t1 t2].

  Notation "# v" := (Var v) (at level 70).

  Notation "^ n" := (Const n) (at level 70).
229
  Infix "+^" := Plus (left associativity, at level 78).
Adam Chlipala's avatar
Adam Chlipala committed
230 231 232 233 234 235 236 237 238 239 240 241

  Infix "@" := App (left associativity, at level 77).
  Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
  Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).

  Notation "[ e1 , e2 ]" := (Pair e1 e2).
  Notation "#1 e" := (Fst e) (at level 75).
  Notation "#2 e" := (Snd e) (at level 75).

  Notation "'case' e 'of' x => e1 | y => e2" := (SumCase e (fun x => e1) (fun y => e2))
    (at level 79).

242 243 244 245 246 247 248 249 250 251 252 253
  Definition swap : Exp (Nat ** Nat --> Nat ** Nat) := fun _ =>
    \p, [#2 #p, #1 #p].
  Definition zo : Exp (Nat ** Nat) := fun _ => [^0, ^1].
  Definition swap_zo : Exp (Nat ** Nat) := fun _ => swap _ @ zo _.

  Definition natOut : Exp (Nat ++ Nat --> Nat) := fun _ =>
    \s, case #s of x => #x | y => #y +^ #y.
  Definition ns1 : Exp (Nat ++ Nat) := fun _ => Inl (^3).
  Definition ns2 : Exp (Nat ++ Nat) := fun _ => Inr (^5).
  Definition natOut_ns1 : Exp Nat := fun _ => natOut _ @ ns1 _.
  Definition natOut_ns2 : Exp Nat := fun _ => natOut _ @ ns2 _.

Adam Chlipala's avatar
Adam Chlipala committed
254
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
255 256 257 258 259 260 261 262
  Fixpoint typeDenote (t : type) : Set :=
    match t with
      | Nat => nat
      | t1 --> t2 => typeDenote t1 -> typeDenote t2
      | t1 ** t2 => typeDenote t1 * typeDenote t2
      | t1 ++ t2 => typeDenote t1 + typeDenote t2
    end%type.

Adam Chlipala's avatar
Adam Chlipala committed
263 264
  Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
    match e with
Adam Chlipala's avatar
Adam Chlipala committed
265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286
      | Var _ v => v
        
      | Const n => n
      | Plus e1 e2 => expDenote e1 + expDenote e2
        
      | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
      | Abs _ _ e' => fun x => expDenote (e' x)

      | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
      | Fst _ _ e' => fst (expDenote e')
      | Snd _ _ e' => snd (expDenote e')

      | Inl _ _ e' => inl _ (expDenote e')
      | Inr _ _ e' => inr _ (expDenote e')
      | SumCase _ _ _ e' e1 e2 =>
        match expDenote e' with
          | inl v => expDenote (e1 v)
          | inr v => expDenote (e2 v)
        end
    end.

  Definition ExpDenote t (e : Exp t) := expDenote (e _).
Adam Chlipala's avatar
Adam Chlipala committed
287
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
288

289 290 291 292 293 294 295 296 297 298
  Eval compute in ExpDenote swap.
  Eval compute in ExpDenote zo.
  Eval compute in ExpDenote swap_zo.

  Eval compute in ExpDenote natOut.
  Eval compute in ExpDenote ns1.
  Eval compute in ExpDenote ns2.
  Eval compute in ExpDenote natOut_ns1.
  Eval compute in ExpDenote natOut_ns2.

Adam Chlipala's avatar
Adam Chlipala committed
299
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
300 301 302
  Section cfold.
    Variable var : type -> Type.

303
    Definition pairOutType t :=
304
      match t return Type with
305 306 307 308 309 310 311 312 313 314
        | t1 ** t2 => option (exp var t1 * exp var t2)
        | _ => unit
      end.

    Definition pairOutDefault (t : type) : pairOutType t :=
      match t return pairOutType t with
        | _ ** _ => None
        | _ => tt
      end.

Adam Chlipala's avatar
Adam Chlipala committed
315 316
    Definition pairOut t1 t2 (e : exp var (t1 ** t2))
      : option (exp var t1 * exp var t2) :=
317 318 319 320 321
      match e in exp _ t return pairOutType t with
        | Pair _ _ e1 e2 => Some (e1, e2)
        | _ => pairOutDefault _
      end.

Adam Chlipala's avatar
Adam Chlipala committed
322 323
    Fixpoint cfold t (e : exp var t) : exp var t :=
      match e with
Adam Chlipala's avatar
Adam Chlipala committed
324 325 326 327 328 329
        | Var _ v => #v

        | Const n => ^n
        | Plus e1 e2 =>
          let e1' := cfold e1 in
          let e2' := cfold e2 in
330
          match e1', e2' return _ with
Adam Chlipala's avatar
Adam Chlipala committed
331 332 333 334 335 336 337 338
            | Const n1, Const n2 => ^(n1 + n2)
            | _, _ => e1' +^ e2'
          end

        | App _ _ e1 e2 => cfold e1 @ cfold e2
        | Abs _ _ e' => Abs (fun x => cfold (e' x))

        | Pair _ _ e1 e2 => [cfold e1, cfold e2]
339 340 341 342 343 344 345 346 347 348 349 350
        | Fst t1 _ e' =>
          let e'' := cfold e' in
            match pairOut e'' with
              | None => #1 e''
              | Some (e1, _) => e1
            end
        | Snd _ _ e' =>
          let e'' := cfold e' in
            match pairOut e'' with
              | None => #2 e''
              | Some (_, e2) => e2
            end
Adam Chlipala's avatar
Adam Chlipala committed
351 352 353 354 355 356 357 358 359 360 361 362

        | Inl _ _ e' => Inl (cfold e')
        | Inr _ _ e' => Inr (cfold e')
        | SumCase _ _ _ e' e1 e2 =>
          case cfold e' of
            x => cfold (e1 x)
          | y => cfold (e2 y)
      end.
  End cfold.

  Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).

363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380
  Section pairs.
    Variables A B : Type.

    Variable v1 : A.
    Variable v2 : B.
    Variable v : A * B.

    Theorem pair_eta1 : (v1, v2) = v -> v1 = fst v.
      destruct v; crush.
    Qed.

    Theorem pair_eta2 : (v1, v2) = v -> v2 = snd v.
      destruct v; crush.
    Qed.
  End pairs.

  Hint Resolve pair_eta1 pair_eta2.

Adam Chlipala's avatar
Adam Chlipala committed
381 382 383 384 385 386
  Lemma cfold_correct : forall t (e : exp _ t),
    expDenote (cfold e) = expDenote e.
    induction e; crush; try (ext_eq; crush);
      repeat (match goal with
                | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
                | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E
387
              end; crush); eauto.
Adam Chlipala's avatar
Adam Chlipala committed
388 389 390 391 392 393
  Qed.

  Theorem Cfold_correct : forall t (E : Exp t),
    ExpDenote (Cfold E) = ExpDenote E.
    unfold ExpDenote, Cfold; intros; apply cfold_correct.
  Qed.
Adam Chlipala's avatar
Adam Chlipala committed
394
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
395
End PSLC.