Mercurial > cpdt > repo

comparison src/Hoas.v @ 222:13620dfd5f97

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port Hoas
author Adam Chlipala <adamc@hcoop.net>
date Mon, 16 Nov 2009 12:08:18 -0500
parents 8905f28ffeef
children 3c4ed57c9907
comparison
equal deleted inserted replaced
221:54e8ecb5ec88 222:13620dfd5f97
1 (* Copyright (c) 2008, Adam Chlipala 1 (* Copyright (c) 2008-2009, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
71 Definition app_ident' := App (App app ident) one_again. 71 Definition app_ident' := App (App app ident) one_again.
72 72
73 (* EX: Define a function to count the number of variable occurrences in an [Exp]. *) 73 (* EX: Define a function to count the number of variable occurrences in an [Exp]. *)
74 74
75 (* begin thide *) 75 (* begin thide *)
76 Fixpoint countVars t (e : exp (fun _ => unit) t) {struct e} : nat := 76 Fixpoint countVars t (e : exp (fun _ => unit) t) : nat :=
77 match e with 77 match e with
78 | Const' _ => 0 78 | Const' _ => 0
79 | Plus' e1 e2 => countVars e1 + countVars e2 79 | Plus' e1 e2 => countVars e1 + countVars e2
80 | Var _ _ => 1 80 | Var _ _ => 1
81 | App' _ _ e1 e2 => countVars e1 + countVars e2 81 | App' _ _ e1 e2 => countVars e1 + countVars e2
94 Eval compute in CountVars app_ident'. 94 Eval compute in CountVars app_ident'.
95 95
96 (* EX: Define a function to count the number of occurrences of a single distinguished variable. *) 96 (* EX: Define a function to count the number of occurrences of a single distinguished variable. *)
97 97
98 (* begin thide *) 98 (* begin thide *)
99 Fixpoint countOne t (e : exp (fun _ => bool) t) {struct e} : nat := 99 Fixpoint countOne t (e : exp (fun _ => bool) t) : nat :=
100 match e with 100 match e with
101 | Const' _ => 0 101 | Const' _ => 0
102 | Plus' e1 e2 => countOne e1 + countOne e2 102 | Plus' e1 e2 => countOne e1 + countOne e2
103 | Var _ true => 1 103 | Var _ true => 1
104 | Var _ false => 0 104 | Var _ false => 0
130 match n with 130 match n with
131 | O => "O" 131 | O => "O"
132 | S n' => "S(" ++ natToString n' ++ ")" 132 | S n' => "S(" ++ natToString n' ++ ")"
133 end. 133 end.
134 134
135 Fixpoint toString t (e : exp (fun _ => string) t) (cur : string) {struct e} : string * string := 135 Fixpoint toString t (e : exp (fun _ => string) t) (cur : string) : string * string :=
136 match e with 136 match e with
137 | Const' n => (cur, natToString n) 137 | Const' n => (cur, natToString n)
138 | Plus' e1 e2 => 138 | Plus' e1 e2 =>
139 let (cur', s1) := toString e1 cur in 139 let (cur', s1) := toString e1 cur in
140 let (cur'', s2) := toString e2 cur' in 140 let (cur'', s2) := toString e2 cur' in
165 165
166 (* begin thide *) 166 (* begin thide *)
167 Section flatten. 167 Section flatten.
168 Variable var : type -> Type. 168 Variable var : type -> Type.
169 169
170 Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t := 170 Fixpoint flatten t (e : exp (exp var) t) : exp var t :=
171 match e in exp _ t return exp _ t with 171 match e with
172 | Const' n => Const' n 172 | Const' n => Const' n
173 | Plus' e1 e2 => Plus' (flatten e1) (flatten e2) 173 | Plus' e1 e2 => Plus' (flatten e1) (flatten e2)
174 | Var _ e' => e' 174 | Var _ e' => e'
175 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2) 175 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2)
176 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x))) 176 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x)))
210 | IsApp2 : forall dom ran (F : Exp (dom --> ran)), Val F -> isCtx (AppCong2 F) 210 | IsApp2 : forall dom ran (F : Exp (dom --> ran)), Val F -> isCtx (AppCong2 F)
211 | IsPlus1 : forall E2, isCtx (PlusCong1 E2) 211 | IsPlus1 : forall E2, isCtx (PlusCong1 E2)
212 | IsPlus2 : forall E1, Val E1 -> isCtx (PlusCong2 E1). 212 | IsPlus2 : forall E1, Val E1 -> isCtx (PlusCong2 E1).
213 213
214 Definition plug t1 t2 (C : Ctx t1 t2) : Exp t1 -> Exp t2 := 214 Definition plug t1 t2 (C : Ctx t1 t2) : Exp t1 -> Exp t2 :=
215 match C in Ctx t1 t2 return Exp t1 -> Exp t2 with 215 match C with
216 | AppCong1 _ _ X => fun F => App F X 216 | AppCong1 _ _ X => fun F => App F X
217 | AppCong2 _ _ F => fun X => App F X 217 | AppCong2 _ _ F => fun X => App F X
218 | PlusCong1 E2 => fun E1 => Plus E1 E2 218 | PlusCong1 E2 => fun E1 => Plus E1 E2
219 | PlusCong2 E1 => fun E2 => Plus E1 E2 219 | PlusCong2 E1 => fun E2 => Plus E1 E2
220 end. 220 end.
388 Ltac equate_conj F G := 388 Ltac equate_conj F G :=
389 match constr:(F, G) with 389 match constr:(F, G) with
390 | (_ ?x1, _ ?x2) => constr:(x1 = x2) 390 | (_ ?x1, _ ?x2) => constr:(x1 = x2)
391 | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2) 391 | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2)
392 | (_ ?x1 ?y1 ?z1, _ ?x2 ?y2 ?z2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2) 392 | (_ ?x1 ?y1 ?z1, _ ?x2 ?y2 ?z2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2)
393 | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2) 393 | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) =>
394 | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2) 394 constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2)
395 | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) =>
396 constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2)
395 end. 397 end.
396 398
397 Ltac my_crush := 399 Ltac my_crush :=
398 my_crush'; 400 my_crush';
399 repeat (match goal with 401 repeat (match goal with