summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-11-30 15:28:56 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2011-11-30 15:28:56 -0500
commitd35896d2f29d23c3cd4c180f9249e44ebf7ed208 (patch)
tree46bd1fc7feee6dad73467084bb05bff6b03b69c4
parentb0da719acd2e225d83e064e9336e1097b87df6d8 (diff)
Update Coq semantics for 8.3pl2
-rw-r--r--.hgignore3
-rw-r--r--src/coq/Makefile14
-rw-r--r--src/coq/README2
-rw-r--r--src/coq/Semantics.v22
4 files changed, 28 insertions, 13 deletions
diff --git a/.hgignore b/.hgignore
index 401353b3..b5ed224a 100644
--- a/.hgignore
+++ b/.hgignore
@@ -47,6 +47,8 @@ doc/*.html
.depend
Makefile.coq
*.vo
+*.v.d
+*.glob
xml/parse
xml/entities.sml
@@ -55,7 +57,6 @@ syntax: regexp
^Makefile$
^src/c/Makefile$
-^src/coq/Makefile$
^libtool$
^config.h$
^stamp-h1$
diff --git a/src/coq/Makefile b/src/coq/Makefile
new file mode 100644
index 00000000..fc488d68
--- /dev/null
+++ b/src/coq/Makefile
@@ -0,0 +1,14 @@
+MODULES := Axioms Name Syntax Semantics
+VS := $(MODULES:%=%.v)
+
+.PHONY: coq clean
+
+coq: Makefile.coq
+ make -f Makefile.coq
+
+Makefile.coq: Makefile $(VS)
+ coq_makefile -impredicative-set $(VS) -o Makefile.coq
+
+clean:: Makefile.coq
+ make -f Makefile.coq clean
+ rm -f Makefile.coq
diff --git a/src/coq/README b/src/coq/README
index 963a7d16..10cb01e5 100644
--- a/src/coq/README
+++ b/src/coq/README
@@ -1,3 +1,3 @@
This is a Coq formalization of a simplified version of the Ur programming language.
-It has only been tested with Coq version 8.1pl3.
+It has only been tested with Coq version 8.3pl2.
diff --git a/src/coq/Semantics.v b/src/coq/Semantics.v
index 39fb534a..c334a89b 100644
--- a/src/coq/Semantics.v
+++ b/src/coq/Semantics.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2009, Adam Chlipala
+(* Copyright (c) 2009, 2011, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
@@ -25,7 +25,7 @@
* POSSIBILITY OF SUCH DAMAGE.
*)
-Require Import Eqdep.
+Require Import Eqdep_dec.
Require Import Axioms.
Require Import Syntax.
@@ -54,8 +54,8 @@ Definition disjoint T (r1 r2 : row T) :=
| _, _ => True
end.
-Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
- match c in con _ k return kDen k with
+Fixpoint cDen k (c : con kDen k) : kDen k :=
+ match c with
| CVar _ x => x
| Arrow c1 c2 => cDen c1 -> cDen c2
| Poly _ c1 => forall x, cDen (c1 x)
@@ -147,7 +147,7 @@ Definition tDen (t : con kDen KType) : Set := cDen t.
Theorem name_eq_dec_refl : forall n, name_eq_dec n n = left _ (refl_equal n).
intros; destruct (name_eq_dec n n); intuition; [
match goal with
- | [ e : _ = _ |- _ ] => rewrite (UIP_refl _ _ e); reflexivity
+ | [ e : _ = _ |- _ ] => rewrite (UIP_dec name_eq_dec e (refl_equal _)); reflexivity
end
| elimtype False; tauto
].
@@ -168,7 +168,7 @@ Qed.
Implicit Arguments cut_disjoint [v r].
-Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t :=
+Fixpoint eDen t (e : exp dvar tDen t) : tDen t :=
match e in exp _ _ t return tDen t with
| Var _ x => x
| App _ _ e1 e2 => (eDen e1) (eDen e2)
@@ -181,21 +181,21 @@ Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t :=
| refl_equal => eDen e1
end
| Empty => fun _ => tt
- | Single c _ e1 => fun n => if name_eq_dec n (cDen c) as B
- return (match (match (if B then _ else _) with Some _ => if B then _ else _ | None => _ end)
+ | Single c c' e1 => fun n => if name_eq_dec n (cDen c) as B
+ return (match (match (if B then _ else _) with Some _ => _ | None => _ end)
with Some _ => _ | None => unit end)
then eDen e1 else tt
| Proj c _ _ e1 =>
match name_eq_dec_refl (cDen c) in _ = B
return (match (match (if B then _ else _) with
- | Some _ => if B then _ else _
+ | Some _ => _
| None => _ end)
return Set
with Some _ => _ | None => _ end) with
| refl_equal => (eDen e1) (cDen c)
end
| Cut c _ c' Hdisj e1 => fun n =>
- match name_eq_dec n (cDen c) as B return (match (match (if B then Some _ else None) with Some _ => if B then _ else _ | None => (cDen c') n end)
+ match name_eq_dec n (cDen c) as B return (match (match (if B then Some _ else None) with Some _ => _ | None => (cDen c') n end)
with Some T => T | None => unit end
-> match (cDen c') n with
| None => unit
@@ -218,7 +218,7 @@ Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t :=
end
-> match (match D with
| None => (cDen c2) n
- | v => v
+ | Some v => Some v
end) with
| None => unit
| Some T => T