Mercurial > cpdt > repo

comparison 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
comparison
equal deleted inserted replaced
169:8905f28ffeef 170:f8353e2a21d6
1 (* Copyright (c) 2008, Adam Chlipala
2 *
3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License.
6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *)
9
10 (* begin hide *)
11 Require Import String List.
12
13 Require Import Axioms Tactics.
14
15 Set Implicit Arguments.
16 (* end hide *)
17
18
19 (** %\chapter{Type-Theoretic Interpreters}% *)
20
21 (** TODO: Prose for this chapter *)
22
23
24 (** * Simply-Typed Lambda Calculus *)
25
26 Module STLC.
27 Inductive type : Type :=
28 | Nat : type
29 | Arrow : type -> type -> type.
30
31 Infix "-->" := Arrow (right associativity, at level 60).
32
33 Section vars.
34 Variable var : type -> Type.
35
36 Inductive exp : type -> Type :=
37 | Var : forall t,
38 var t
39 -> exp t
40
41 | Const : nat -> exp Nat
42 | Plus : exp Nat -> exp Nat -> exp Nat
43
44 | App : forall t1 t2,
45 exp (t1 --> t2)
46 -> exp t1
47 -> exp t2
48 | Abs : forall t1 t2,
49 (var t1 -> exp t2)
50 -> exp (t1 --> t2).
51 End vars.
52
53 Definition Exp t := forall var, exp var t.
54
55 Implicit Arguments Var [var t].
56 Implicit Arguments Const [var].
57 Implicit Arguments Plus [var].
58 Implicit Arguments App [var t1 t2].
59 Implicit Arguments Abs [var t1 t2].
60
61 Notation "# v" := (Var v) (at level 70).
62
63 Notation "^ n" := (Const n) (at level 70).
64 Infix "++" := Plus.
65
66 Infix "@" := App (left associativity, at level 77).
67 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
68 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
69
70 Fixpoint typeDenote (t : type) : Set :=
71 match t with
72 | Nat => nat
73 | t1 --> t2 => typeDenote t1 -> typeDenote t2
74 end.
75
76 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
77 match e in (exp _ t) return (typeDenote t) with
78 | Var _ v => v
79
80 | Const n => n
81 | Plus e1 e2 => expDenote e1 + expDenote e2
82
83 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
84 | Abs _ _ e' => fun x => expDenote (e' x)
85 end.
86
87 Definition ExpDenote t (e : Exp t) := expDenote (e _).
88
89 Section cfold.
90 Variable var : type -> Type.
91
92 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
93 match e in exp _ t return exp _ t with
94 | Var _ v => #v
95
96 | Const n => ^n
97 | Plus e1 e2 =>
98 let e1' := cfold e1 in
99 let e2' := cfold e2 in
100 match e1', e2' with
101 | Const n1, Const n2 => ^(n1 + n2)
102 | _, _ => e1' ++ e2'
103 end
104
105 | App _ _ e1 e2 => cfold e1 @ cfold e2
106 | Abs _ _ e' => Abs (fun x => cfold (e' x))
107 end.
108 End cfold.
109
110 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
111
112 Lemma cfold_correct : forall t (e : exp _ t),
113 expDenote (cfold e) = expDenote e.
114 induction e; crush; try (ext_eq; crush);
115 repeat (match goal with
116 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
117 end; crush).
118 Qed.
119
120 Theorem Cfold_correct : forall t (E : Exp t),
121 ExpDenote (Cfold E) = ExpDenote E.
122 unfold ExpDenote, Cfold; intros; apply cfold_correct.
123 Qed.
124 End STLC.