Mercurial > cpdt > repo
comparison src/Hoas.v @ 169:8905f28ffeef
Templatize Hoas
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 05 Nov 2008 09:39:00 -0500 |
parents | 0c5a41e9e508 |
children | 13620dfd5f97 |
comparison
equal
deleted
inserted
replaced
168:0c5a41e9e508 | 169:8905f28ffeef |
---|---|
44 Implicit Arguments Const' [var]. | 44 Implicit Arguments Const' [var]. |
45 Implicit Arguments Var [var t]. | 45 Implicit Arguments Var [var t]. |
46 Implicit Arguments Abs' [var dom ran]. | 46 Implicit Arguments Abs' [var dom ran]. |
47 | 47 |
48 Definition Exp t := forall var, exp var t. | 48 Definition Exp t := forall var, exp var t. |
49 (* begin thide *) | |
49 Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2. | 50 Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2. |
50 | 51 |
51 Definition Const (n : nat) : Exp Nat := | 52 Definition Const (n : nat) : Exp Nat := |
52 fun _ => Const' n. | 53 fun _ => Const' n. |
53 Definition Plus (E1 E2 : Exp Nat) : Exp Nat := | 54 Definition Plus (E1 E2 : Exp Nat) : Exp Nat := |
54 fun _ => Plus' (E1 _) (E2 _). | 55 fun _ => Plus' (E1 _) (E2 _). |
55 Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran := | 56 Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran := |
56 fun _ => App' (F _) (X _). | 57 fun _ => App' (F _) (X _). |
57 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) := | 58 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) := |
58 fun _ => Abs' (B _). | 59 fun _ => Abs' (B _). |
60 (* end thide *) | |
61 | |
62 (* EX: Define appropriate shorthands, so that these definitions type-check. *) | |
59 | 63 |
60 Definition zero := Const 0. | 64 Definition zero := Const 0. |
61 Definition one := Const 1. | 65 Definition one := Const 1. |
62 Definition one_again := Plus zero one. | 66 Definition one_again := Plus zero one. |
63 Definition ident : Exp (Nat --> Nat) := Abs (fun _ X => Var X). | 67 Definition ident : Exp (Nat --> Nat) := Abs (fun _ X => Var X). |
64 Definition app_ident := App ident one_again. | 68 Definition app_ident := App ident one_again. |
65 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => | 69 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => |
66 Abs' (fun f => Abs' (fun x => App' (Var f) (Var x))). | 70 Abs' (fun f => Abs' (fun x => App' (Var f) (Var x))). |
67 Definition app_ident' := App (App app ident) one_again. | 71 Definition app_ident' := App (App app ident) one_again. |
68 | 72 |
73 (* EX: Define a function to count the number of variable occurrences in an [Exp]. *) | |
74 | |
75 (* begin thide *) | |
69 Fixpoint countVars t (e : exp (fun _ => unit) t) {struct e} : nat := | 76 Fixpoint countVars t (e : exp (fun _ => unit) t) {struct e} : nat := |
70 match e with | 77 match e with |
71 | Const' _ => 0 | 78 | Const' _ => 0 |
72 | Plus' e1 e2 => countVars e1 + countVars e2 | 79 | Plus' e1 e2 => countVars e1 + countVars e2 |
73 | Var _ _ => 1 | 80 | Var _ _ => 1 |
74 | App' _ _ e1 e2 => countVars e1 + countVars e2 | 81 | App' _ _ e1 e2 => countVars e1 + countVars e2 |
75 | Abs' _ _ e' => countVars (e' tt) | 82 | Abs' _ _ e' => countVars (e' tt) |
76 end. | 83 end. |
77 | 84 |
78 Definition CountVars t (E : Exp t) : nat := countVars (E _). | 85 Definition CountVars t (E : Exp t) : nat := countVars (E _). |
86 (* end thide *) | |
79 | 87 |
80 Eval compute in CountVars zero. | 88 Eval compute in CountVars zero. |
81 Eval compute in CountVars one. | 89 Eval compute in CountVars one. |
82 Eval compute in CountVars one_again. | 90 Eval compute in CountVars one_again. |
83 Eval compute in CountVars ident. | 91 Eval compute in CountVars ident. |
84 Eval compute in CountVars app_ident. | 92 Eval compute in CountVars app_ident. |
85 Eval compute in CountVars app. | 93 Eval compute in CountVars app. |
86 Eval compute in CountVars app_ident'. | 94 Eval compute in CountVars app_ident'. |
87 | 95 |
96 (* EX: Define a function to count the number of occurrences of a single distinguished variable. *) | |
97 | |
98 (* begin thide *) | |
88 Fixpoint countOne t (e : exp (fun _ => bool) t) {struct e} : nat := | 99 Fixpoint countOne t (e : exp (fun _ => bool) t) {struct e} : nat := |
89 match e with | 100 match e with |
90 | Const' _ => 0 | 101 | Const' _ => 0 |
91 | Plus' e1 e2 => countOne e1 + countOne e2 | 102 | Plus' e1 e2 => countOne e1 + countOne e2 |
92 | Var _ true => 1 | 103 | Var _ true => 1 |
95 | Abs' _ _ e' => countOne (e' false) | 106 | Abs' _ _ e' => countOne (e' false) |
96 end. | 107 end. |
97 | 108 |
98 Definition CountOne t1 t2 (E : Exp1 t1 t2) : nat := | 109 Definition CountOne t1 t2 (E : Exp1 t1 t2) : nat := |
99 countOne (E _ true). | 110 countOne (E _ true). |
111 (* end thide *) | |
100 | 112 |
101 Definition ident1 : Exp1 Nat Nat := fun _ X => Var X. | 113 Definition ident1 : Exp1 Nat Nat := fun _ X => Var X. |
102 Definition add_self : Exp1 Nat Nat := fun _ X => Plus' (Var X) (Var X). | 114 Definition add_self : Exp1 Nat Nat := fun _ X => Plus' (Var X) (Var X). |
103 Definition app_zero : Exp1 (Nat --> Nat) Nat := fun _ X => App' (Var X) (Const' 0). | 115 Definition app_zero : Exp1 (Nat --> Nat) Nat := fun _ X => App' (Var X) (Const' 0). |
104 Definition app_ident1 : Exp1 Nat Nat := fun _ X => App' (Abs' (fun Y => Var Y)) (Var X). | 116 Definition app_ident1 : Exp1 Nat Nat := fun _ X => App' (Abs' (fun Y => Var Y)) (Var X). |
106 Eval compute in CountOne ident1. | 118 Eval compute in CountOne ident1. |
107 Eval compute in CountOne add_self. | 119 Eval compute in CountOne add_self. |
108 Eval compute in CountOne app_zero. | 120 Eval compute in CountOne app_zero. |
109 Eval compute in CountOne app_ident1. | 121 Eval compute in CountOne app_ident1. |
110 | 122 |
123 (* EX: Define a function to pretty-print [Exp]s as strings. *) | |
124 | |
125 (* begin thide *) | |
111 Section ToString. | 126 Section ToString. |
112 Open Scope string_scope. | 127 Open Scope string_scope. |
113 | 128 |
114 Fixpoint natToString (n : nat) : string := | 129 Fixpoint natToString (n : nat) : string := |
115 match n with | 130 match n with |
134 (cur', "(\" ++ cur ++ ", " ++ s ++ ")") | 149 (cur', "(\" ++ cur ++ ", " ++ s ++ ")") |
135 end. | 150 end. |
136 | 151 |
137 Definition ToString t (E : Exp t) : string := snd (toString (E _) "x"). | 152 Definition ToString t (E : Exp t) : string := snd (toString (E _) "x"). |
138 End ToString. | 153 End ToString. |
154 (* end thide *) | |
139 | 155 |
140 Eval compute in ToString zero. | 156 Eval compute in ToString zero. |
141 Eval compute in ToString one. | 157 Eval compute in ToString one. |
142 Eval compute in ToString one_again. | 158 Eval compute in ToString one_again. |
143 Eval compute in ToString ident. | 159 Eval compute in ToString ident. |
144 Eval compute in ToString app_ident. | 160 Eval compute in ToString app_ident. |
145 Eval compute in ToString app. | 161 Eval compute in ToString app. |
146 Eval compute in ToString app_ident'. | 162 Eval compute in ToString app_ident'. |
147 | 163 |
164 (* EX: Define a substitution function. *) | |
165 | |
166 (* begin thide *) | |
148 Section flatten. | 167 Section flatten. |
149 Variable var : type -> Type. | 168 Variable var : type -> Type. |
150 | 169 |
151 Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t := | 170 Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t := |
152 match e in exp _ t return exp _ t with | 171 match e in exp _ t return exp _ t with |
158 end. | 177 end. |
159 End flatten. | 178 End flatten. |
160 | 179 |
161 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ => | 180 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ => |
162 flatten (E2 _ (E1 _)). | 181 flatten (E2 _ (E1 _)). |
182 (* end thide *) | |
163 | 183 |
164 Eval compute in Subst one ident1. | 184 Eval compute in Subst one ident1. |
165 Eval compute in Subst one add_self. | 185 Eval compute in Subst one add_self. |
166 Eval compute in Subst ident app_zero. | 186 Eval compute in Subst ident app_zero. |
167 Eval compute in Subst one app_ident1. | 187 Eval compute in Subst one app_ident1. |
215 | 235 |
216 where "E1 ==> E2" := (Step E1 E2). | 236 where "E1 ==> E2" := (Step E1 E2). |
217 | 237 |
218 Hint Constructors isCtx Step. | 238 Hint Constructors isCtx Step. |
219 | 239 |
240 (* EX: Prove type soundness. *) | |
241 | |
242 (* begin thide *) | |
220 Inductive Closed : forall t, Exp t -> Prop := | 243 Inductive Closed : forall t, Exp t -> Prop := |
221 | CConst : forall n, | 244 | CConst : forall n, |
222 Closed (Const n) | 245 Closed (Const n) |
223 | CPlus : forall E1 E2, | 246 | CPlus : forall E1 E2, |
224 Closed E1 | 247 Closed E1 |
252 | 275 |
253 Theorem progress : forall t (E : Exp t), | 276 Theorem progress : forall t (E : Exp t), |
254 Val E \/ exists E', E ==> E'. | 277 Val E \/ exists E', E ==> E'. |
255 intros; apply progress'; apply closed. | 278 intros; apply progress'; apply closed. |
256 Qed. | 279 Qed. |
280 (* end thide *) | |
257 | 281 |
258 | 282 |
259 (** * Big-Step Semantics *) | 283 (** * Big-Step Semantics *) |
260 | 284 |
261 Reserved Notation "E1 ===> E2" (no associativity, at level 90). | 285 Reserved Notation "E1 ===> E2" (no associativity, at level 90). |
278 | 302 |
279 where "E1 ===> E2" := (BigStep E1 E2). | 303 where "E1 ===> E2" := (BigStep E1 E2). |
280 | 304 |
281 Hint Constructors BigStep. | 305 Hint Constructors BigStep. |
282 | 306 |
307 (* EX: Prove the equivalence of the small- and big-step semantics. *) | |
308 | |
309 (* begin thide *) | |
283 Reserved Notation "E1 ==>* E2" (no associativity, at level 90). | 310 Reserved Notation "E1 ==>* E2" (no associativity, at level 90). |
284 | 311 |
285 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop := | 312 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop := |
286 | Done : forall t (E : Exp t), E ==>* E | 313 | Done : forall t (E : Exp t), E ==>* E |
287 | OneStep : forall t (E E' E'' : Exp t), | 314 | OneStep : forall t (E E' E'' : Exp t), |
415 E ==>* V | 442 E ==>* V |
416 -> Val V | 443 -> Val V |
417 -> E ===> V. | 444 -> E ===> V. |
418 induction 1; crush; eauto. | 445 induction 1; crush; eauto. |
419 Qed. | 446 Qed. |
447 (* end thide *) |