Finish semantics for Featherweight Ur

1 files changed, 75 insertions, 6 deletions

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.