### changeset 222:13620dfd5f97

Port Hoas
author Adam Chlipala Mon, 16 Nov 2009 12:08:18 -0500 54e8ecb5ec88 2a34c4dc6a10 src/Firstorder.v src/Hoas.v 2 files changed, 12 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
```--- a/src/Firstorder.v	Mon Nov 16 11:09:47 2009 -0500
+++ b/src/Firstorder.v	Mon Nov 16 12:08:18 2009 -0500
@@ -1,4 +1,4 @@
*
* Creative Commons Attribution-Noncommercial-No Derivative Works 3.0```
```--- a/src/Hoas.v	Mon Nov 16 11:09:47 2009 -0500
+++ b/src/Hoas.v	Mon Nov 16 12:08:18 2009 -0500
@@ -1,4 +1,4 @@
*
* Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -73,7 +73,7 @@
(* EX: Define a function to count the number of variable occurrences in an [Exp]. *)

(* begin thide *)
-Fixpoint countVars t (e : exp (fun _ => unit) t) {struct e} : nat :=
+Fixpoint countVars t (e : exp (fun _ => unit) t) : nat :=
match e with
| Const' _ => 0
| Plus' e1 e2 => countVars e1 + countVars e2
@@ -96,7 +96,7 @@
(* EX: Define a function to count the number of occurrences of a single distinguished variable. *)

(* begin thide *)
-Fixpoint countOne t (e : exp (fun _ => bool) t) {struct e} : nat :=
+Fixpoint countOne t (e : exp (fun _ => bool) t) : nat :=
match e with
| Const' _ => 0
| Plus' e1 e2 => countOne e1 + countOne e2
@@ -132,7 +132,7 @@
| S n' => "S(" ++ natToString n' ++ ")"
end.

-  Fixpoint toString t (e : exp (fun _ => string) t) (cur : string) {struct e} : string * string :=
+  Fixpoint toString t (e : exp (fun _ => string) t) (cur : string) : string * string :=
match e with
| Const' n => (cur, natToString n)
| Plus' e1 e2 =>
@@ -167,8 +167,8 @@
Section flatten.
Variable var : type -> Type.

-  Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t :=
-    match e in exp _ t return exp _ t with
+  Fixpoint flatten t (e : exp (exp var) t) : exp var t :=
+    match e with
| Const' n => Const' n
| Plus' e1 e2 => Plus' (flatten e1) (flatten e2)
| Var _ e' => e'
@@ -212,7 +212,7 @@
| IsPlus2 : forall E1, Val E1 -> isCtx (PlusCong2 E1).

Definition plug t1 t2 (C : Ctx t1 t2) : Exp t1 -> Exp t2 :=
-  match C in Ctx t1 t2 return Exp t1 -> Exp t2 with
+  match C with
| AppCong1 _ _ X => fun F => App F X
| AppCong2 _ _ F => fun X => App F X
| PlusCong1 E2 => fun E1 => Plus E1 E2
@@ -390,8 +390,10 @@
| (_ ?x1, _ ?x2) => constr:(x1 = x2)
| (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2)
| (_ ?x1 ?y1 ?z1, _ ?x2 ?y2 ?z2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2)
-    | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2)
-    | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2)
+    | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) =>
+      constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2)
+    | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) =>
+      constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2)
end.

Ltac my_crush :=```