summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-21 14:10:06 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-21 14:10:06 -0500
commit9f20d9299eab7caab6421860b6a54f831af73921 (patch)
tree9e2dcb53a357f93751c3f1e1237a3d0900d02b2d
parentfe5ac0fba7f973b2557c7ae7a6bb9248024ffacd (diff)
Finish semantics for Featherweight Ur
-rw-r--r--src/coq/Name.v71
-rw-r--r--src/coq/Semantics.v81
-rw-r--r--src/coq/Syntax.v16
3 files changed, 154 insertions, 14 deletions
diff --git a/src/coq/Name.v b/src/coq/Name.v
new file mode 100644
index 00000000..bc6df1c1
--- /dev/null
+++ b/src/coq/Name.v
@@ -0,0 +1,71 @@
+(* Copyright (c) 2009, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ * this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ * this list of conditions and the following disclaimer in the documentation
+ * and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ * derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+Set Implicit Arguments.
+
+
+Fixpoint name' (n : nat) : Type :=
+ match n with
+ | O => Empty_set
+ | S n' => option (name' n')
+ end.
+
+Definition name'_eq_dec : forall n (x y : name' n), {x = y} + {x <> y}.
+ Hint Extern 1 (_ = _ -> False) => congruence.
+
+ induction n; simpl; intuition;
+ repeat match goal with
+ | [ x : Empty_set |- _ ] => destruct x
+ | [ x : option _ |- _ ] => destruct x
+ end; intuition;
+ match goal with
+ | [ IH : _, n1 : name' _, n2 : name' _ |- _ ] =>
+ destruct (IHn n1 n0); subst; intuition
+ end.
+Qed.
+
+Definition badName' n (P : name' n -> bool) :
+ {nm : _ | P nm = false} + {forall nm, P nm = true}.
+ Hint Constructors sig.
+ Hint Extern 1 (_ = true) =>
+ match goal with
+ | [ nm : option _ |- _ ] => destruct nm
+ end; auto.
+
+ induction n; simpl; intuition;
+ match goal with
+ | [ IH : forall P : _ -> _,_ |- _ ] =>
+ case_eq (P None);
+ destruct (IH (fun nm => P (Some nm))); firstorder eauto
+ end.
+Qed.
+
+Parameter numNames : nat.
+Definition name := name' (S numNames).
+Definition name_eq_dec : forall (x y : name), {x = y} + {x <> y} := @name'_eq_dec _.
+Definition badName : forall P : name -> bool, {nm : _ | P nm = false} + {forall nm, P nm = true} := @badName' _.
+Definition defaultName : name := None.
diff --git a/src/coq/Semantics.v b/src/coq/Semantics.v
index 19c67a05..2a12df72 100644
--- a/src/coq/Semantics.v
+++ b/src/coq/Semantics.v
@@ -48,6 +48,14 @@ Fixpoint kDen (k : kind) : Type :=
| KRecord k1 => row (kDen k1)
end.
+Fixpoint kDefault (k : kind) : kDen k :=
+ match k return kDen k with
+ | KType => unit
+ | KName => defaultName
+ | KArrow _ k2 => fun _ => kDefault k2
+ | KRecord _ => fun _ => None
+ end.
+
Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
match c in con _ k return kDen k with
| CVar _ x => x
@@ -67,7 +75,13 @@ Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
| None => None
| Some T => Some (f T)
end
- | CGuarded _ _ _ _ c => cDen c
+ | CGuarded _ _ c1 c2 c =>
+ if badName (fun n => match (cDen c1) n, (cDen c2) n with
+ | Some _, Some _ => false
+ | _, _ => true
+ end)
+ then kDefault _
+ else cDen c
end.
Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2',
@@ -87,11 +101,33 @@ Definition disjoint T (r1 r2 : row T) :=
Definition dvar k (c1 c2 : con kDen (KRecord k)) :=
disjoint (cDen c1) (cDen c2).
+Theorem known_badName : forall T (r1 r2 : row T) T' (v1 v2 : T'),
+ disjoint r1 r2
+ -> (if badName (fun n => match r1 n, r2 n with
+ | Some _, Some _ => false
+ | _, _ => true
+ end)
+ then v1
+ else v2) = v2.
+ intros; match goal with
+ | [ |- context[if ?E then _ else _] ] => destruct E
+ end; firstorder;
+ match goal with
+ | [ H : disjoint _ _, x : name |- _ ] =>
+ generalize (H x);
+ repeat match goal with
+ | [ |- context[match ?E with None => _ | Some _ => _ end] ] => destruct E
+ end; tauto || congruence
+ end.
+Qed.
+
+Hint Rewrite known_badName using solve [ auto ] : Semantics.
+
Scheme deq_mut := Minimality for deq Sort Prop
with disj_mut := Minimality for disj Sort Prop.
Ltac deq_disj_correct scm :=
- let t := repeat progress (simpl; intuition; subst) in
+ let t := repeat progress (simpl; intuition; subst; autorewrite with Semantics) in
let rec use_disjoint' notDone E :=
match goal with
@@ -113,7 +149,7 @@ Ltac deq_disj_correct scm :=
disjoint (cDen c1) (cDen c2))); t;
repeat ((unfold row; apply ext_eq)
|| (match goal with
- | [ H : _ |- _ ] => rewrite H
+ | [ H : _ |- _ ] => rewrite H; []
| [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H)
end); t);
unfold disjoint; t;
@@ -124,8 +160,33 @@ Ltac deq_disj_correct scm :=
use_disjoint N1; use_disjoint N2; destruct (name_eq_dec N1 N2)
| [ _ : context[match cDen ?C ?E with Some _ => _ | None => _ end] |- _ ] =>
use_disjoint E; destruct (cDen C E)
+ | [ |- context[if ?E then _ else _] ] => destruct E
end; t).
+Lemma bool_disjoint : forall T (r1 r2 : row T),
+ (forall nm : name,
+ match r1 nm with
+ | Some _ => match r2 nm with
+ | Some _ => false
+ | None => true
+ end
+ | None => true
+ end = true)
+ -> disjoint r1 r2.
+ intros; intro;
+ match goal with
+ | [ H : _, n : name |- _ ] => generalize (H n)
+ end;
+ repeat match goal with
+ | [ |- context[match ?E with Some _ => _ | None => _ end] ] => destruct E
+ end; tauto || discriminate.
+Qed.
+
+Implicit Arguments bool_disjoint [T r1 r2].
+
+Hint Resolve bool_disjoint.
+Hint Unfold dvar.
+
Theorem deq_correct : forall k (c1 c2 : con kDen k),
deq dvar c1 c2
-> cDen c1 = cDen c2.
@@ -138,8 +199,6 @@ Theorem disj_correct : forall k (c1 c2 : con kDen (KRecord k)),
deq_disj_correct disj_mut.
Qed.
-Axiom cheat : forall T, T.
-
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).
@@ -166,6 +225,8 @@ Qed.
Implicit Arguments cut_disjoint [v r].
+Set Printing All.
+
Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t :=
match e in exp _ _ t return tDen t with
| Var _ x => x
@@ -225,5 +286,13 @@ Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t :=
| _ => fun x => x
end ((eDen e1) n)
- | _ => cheat _
+ | Guarded _ c1 c2 _ e1 =>
+ match badName (fun n => match (cDen c1) n, (cDen c2) n with
+ | Some _, Some _ => false
+ | _, _ => true
+ end)
+ as BN return (if BN return Set then _ else _) with
+ | inleft _ => tt
+ | inright pf => eDen (e1 (bool_disjoint pf))
+ end
end.
diff --git a/src/coq/Syntax.v b/src/coq/Syntax.v
index b19a790e..2378037e 100644
--- a/src/coq/Syntax.v
+++ b/src/coq/Syntax.v
@@ -25,15 +25,12 @@
* POSSIBILITY OF SUCH DAMAGE.
*)
-Require Import String.
+Require Import Name.
+Export Name.
Set Implicit Arguments.
-Definition name : Type := string.
-Definition name_eq_dec : forall (x y : name), {x = y} + {x <> y} := string_dec.
-
-
(** Syntax of Featherweight Ur *)
Inductive kind : Type :=
@@ -160,9 +157,12 @@ Section vars.
-> deq (CApp (CApp (CMap k1 k2) f) (CConcat (CSingle c1 c2) c3))
(CConcat (CSingle c1 (CApp f c2)) (CApp (CApp (CMap k1 k2) f) c3))
- | Eq_Guarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2),
- (*disj c1 c2
- ->*) deq (CGuarded c1 c2 c) c
+ | Eq_Guarded_Remove : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2),
+ disj c1 c2
+ -> deq (CGuarded c1 c2 c) c
+ | Eq_Guarded_Cong : forall k1 k2 (c1 c2 : con (KRecord k1)) (c c' : con k2),
+ (dvar c1 c2 -> deq c c')
+ -> deq (CGuarded c1 c2 c) (CGuarded c1 c2 c')
| Eq_Map_Ident : forall k c,
deq (CApp (CApp (CMap k k) (CAbs (fun x => CVar x))) c) c