Mercurial > cpdt > repo

comparison src/Hoas.v @ 169:8905f28ffeef

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 *)