Mercurial > cpdt > repo

annotate src/Interps.v @ 170:f8353e2a21d6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
STLC example in Interps
author Adam Chlipala <adamc@hcoop.net>
date Sun, 09 Nov 2008 13:44:31 -0500
parents
children b00b6a9b6b58
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@170 64 Infix "++" := Plus.
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@170 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.