adamc@170: (* Copyright (c) 2008, Adam Chlipala
adamc@170:  * 
adamc@170:  * This work is licensed under a
adamc@170:  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@170:  * Unported License.
adamc@170:  * The license text is available at:
adamc@170:  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@170:  *)
adamc@170: 
adamc@170: (* begin hide *)
adamc@170: Require Import String List.
adamc@170: 
adamc@170: Require Import Axioms Tactics.
adamc@170: 
adamc@170: Set Implicit Arguments.
adamc@170: (* end hide *)
adamc@170: 
adamc@170: 
adamc@170: (** %\chapter{Type-Theoretic Interpreters}% *)
adamc@170: 
adamc@170: (** TODO: Prose for this chapter *)
adamc@170: 
adamc@170: 
adamc@170: (** * Simply-Typed Lambda Calculus *)
adamc@170: 
adamc@170: Module STLC.
adamc@170:   Inductive type : Type :=
adamc@170:   | Nat : type
adamc@170:   | Arrow : type -> type -> type.
adamc@170: 
adamc@170:   Infix "-->" := Arrow (right associativity, at level 60).
adamc@170: 
adamc@170:   Section vars.
adamc@170:     Variable var : type -> Type.
adamc@170: 
adamc@170:     Inductive exp : type -> Type :=
adamc@170:     | Var : forall t,
adamc@170:       var t
adamc@170:       -> exp t
adamc@170: 
adamc@170:     | Const : nat -> exp Nat
adamc@170:     | Plus : exp Nat -> exp Nat -> exp Nat
adamc@170: 
adamc@170:     | App : forall t1 t2,
adamc@170:       exp (t1 --> t2)
adamc@170:       -> exp t1
adamc@170:       -> exp t2
adamc@170:     | Abs : forall t1 t2,
adamc@170:       (var t1 -> exp t2)
adamc@170:       -> exp (t1 --> t2).
adamc@170:   End vars.
adamc@170: 
adamc@170:   Definition Exp t := forall var, exp var t.
adamc@170: 
adamc@170:   Implicit Arguments Var [var t].
adamc@170:   Implicit Arguments Const [var].
adamc@170:   Implicit Arguments Plus [var].
adamc@170:   Implicit Arguments App [var t1 t2].
adamc@170:   Implicit Arguments Abs [var t1 t2].
adamc@170: 
adamc@170:   Notation "# v" := (Var v) (at level 70).
adamc@170: 
adamc@170:   Notation "^ n" := (Const n) (at level 70).
adamc@170:   Infix "++" := Plus.
adamc@170: 
adamc@170:   Infix "@" := App (left associativity, at level 77).
adamc@170:   Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@170:   Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@170: 
adamc@170:   Fixpoint typeDenote (t : type) : Set :=
adamc@170:     match t with
adamc@170:       | Nat => nat
adamc@170:       | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@170:     end.
adamc@170: 
adamc@170:   Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@170:     match e in (exp _ t) return (typeDenote t) with
adamc@170:       | Var _ v => v
adamc@170:         
adamc@170:       | Const n => n
adamc@170:       | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@170:         
adamc@170:       | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@170:       | Abs _ _ e' => fun x => expDenote (e' x)
adamc@170:     end.
adamc@170: 
adamc@170:   Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@170: 
adamc@170:   Section cfold.
adamc@170:     Variable var : type -> Type.
adamc@170: 
adamc@170:     Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
adamc@170:       match e in exp _ t return exp _ t with
adamc@170:         | Var _ v => #v
adamc@170: 
adamc@170:         | Const n => ^n
adamc@170:         | Plus e1 e2 =>
adamc@170:           let e1' := cfold e1 in
adamc@170:           let e2' := cfold e2 in
adamc@170:           match e1', e2' with
adamc@170:             | Const n1, Const n2 => ^(n1 + n2)
adamc@170:             | _, _ => e1' ++ e2'
adamc@170:           end
adamc@170: 
adamc@170:         | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@170:         | Abs _ _ e' => Abs (fun x => cfold (e' x))
adamc@170:       end.
adamc@170:   End cfold.
adamc@170: 
adamc@170:   Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@170: 
adamc@170:   Lemma cfold_correct : forall t (e : exp _ t),
adamc@170:     expDenote (cfold e) = expDenote e.
adamc@170:     induction e; crush; try (ext_eq; crush);
adamc@170:       repeat (match goal with
adamc@170:                 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@170:               end; crush).
adamc@170:   Qed.
adamc@170: 
adamc@170:   Theorem Cfold_correct : forall t (E : Exp t),
adamc@170:     ExpDenote (Cfold E) = ExpDenote E.
adamc@170:     unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@170:   Qed.
adamc@170: End STLC.