map-only syntax and semantics

2 files changed, 70 insertions, 122 deletions

diff --git a/src/coq/Semantics.v b/src/coq/Semantics.v
index a60ae102..c3c8d908 100644
--- a/src/coq/Semantics.v
+++ b/src/coq/Semantics.v
@@ -25,21 +25,18 @@
  * POSSIBILITY OF SUCH DAMAGE.
  *)
 
-Require Import Arith List TheoryList.
-
 Require Import Axioms.
 Require Import Syntax.
 
 Set Implicit Arguments.
 
 
-Definition row (T : Type) := list (name * T).
+Definition row (A : Type) : Type := name -> option A.
 
-Fixpoint record (r : row Set) : Set :=
-  match r with
-    | nil => unit
-    | (_, T) :: r' => T * record r'
-  end%type.
+Definition record (r : row Set) := forall n, match r n with
+                                               | None => unit
+                                               | Some T => T
+                                             end.
 
 Fixpoint kDen (k : kind) : Type :=
   match k with
@@ -49,12 +46,6 @@ Fixpoint kDen (k : kind) : Type :=
     | KRecord k1 => row (kDen k1)
   end.
 
-Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') (r : row T) {struct r} : T' :=
-  match r with
-    | nil => i
-    | (n, v) :: r' => f n v (cfold f i r')
-  end.
-
 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
   match c in con _ k return kDen k with
     | CVar _ x => x
@@ -64,10 +55,16 @@ Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
     | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
     | Name n => n
     | TRecord c1 => record (cDen c1)
-    | CEmpty _ => nil
-    | CSingle _ c1 c2 => (cDen c1, cDen c2) :: nil
-    | CConcat _ c1 c2 => cDen c1 ++ cDen c2
-    | CFold k1 k2 => @cfold _ _
+    | CEmpty _ => fun _ => None
+    | CSingle _ c1 c2 => fun n => if name_eq_dec n (cDen c1) then Some (cDen c2) else None
+    | CConcat _ c1 c2 => fun n => match (cDen c1) n with
+                                    | None => (cDen c2) n
+                                    | v => v
+                                  end
+    | CMap k1 k2 => fun f r n => match r n with
+                                   | None => None
+                                   | Some T => Some (f T)
+                                 end
     | CGuarded _ _ _ _ c => cDen c
   end.
 
@@ -81,90 +78,51 @@ Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c
 Qed.
 
 Definition disjoint T (r1 r2 : row T) :=
-  AllS (fun p1 => AllS (fun p2 => fst p1 <> fst p2) r2) r1.
+  forall n, match r1 n, r2 n with
+              | Some _, Some _ => False
+              | _, _ => True
+            end.
 Definition dvar k (c1 c2 : con kDen (KRecord k)) :=
   disjoint (cDen c1) (cDen c2).
 
-Lemma AllS_app : forall T P (ls2 : list T),
-  AllS P ls2
-  -> forall ls1, AllS P ls1
-    -> AllS P (ls1 ++ ls2).
-  induction 2; simpl; intuition.
-Qed.
-
-Lemma AllS_weaken : forall T (P P' : T -> Prop),
-  (forall x, P x -> P' x)
-  -> forall ls,
-    AllS P ls
-    -> AllS P' ls.
-  induction 2; simpl; intuition.
-Qed.
-
-Theorem disjoint_symm : forall T (r1 r2 : row T),
-  disjoint r1 r2
-  -> disjoint r2 r1.
-  Hint Constructors AllS.
-  Hint Resolve AllS_weaken.
-  
-  unfold disjoint; induction r2; simpl; intuition.
-  constructor.
-  eapply AllS_weaken; eauto.
-  intuition.
-  inversion H0; auto.
-
-  apply IHr2.
-  eapply AllS_weaken; eauto.
-  intuition.
-  inversion H0; auto.
-Qed.  
-
-Lemma map_id : forall k (r : row k),
-  cfold (fun x x0 (x1 : row _) => (x, x0) :: x1) nil r = r.
-  induction r; simpl; intuition;
-    match goal with
-      | [ H : _ |- _ ] => rewrite H
-    end; intuition.
-Qed.
-
-Lemma map_dist : forall T1 T2 (f : T1 -> T2) (r2 r1 : row T1),
-  cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil (r1 ++ r2)
-  = cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil r1
-  ++ cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil r2.
-  induction r1; simpl; intuition;
-    match goal with
-      | [ H : _ |- _ ] => rewrite H
-    end; intuition.
-Qed.
-
-Lemma fold_fuse : forall T1 T2 T3 (f : name -> T1 -> T2 -> T2) (i : T2) (f' : T3 -> T1) (c : row T3),
-  cfold f i (cfold (fun x x0 (x1 : row _) => (x, f' x0) :: x1) nil c)
-  = cfold (fun x x0 => f x (f' x0)) i c.
-  induction c; simpl; intuition;
-    match goal with
-      | [ H : _ |- _ ] => rewrite <- H
-    end; intuition.
-Qed.
-
 Scheme deq_mut := Minimality for deq Sort Prop
 with disj_mut := Minimality for disj Sort Prop.
 
 Theorem deq_correct : forall k (c1 c2 : con kDen k),
   deq dvar c1 c2
   -> cDen c1 = cDen c2.
-  Hint Resolve map_id map_dist fold_fuse AllS_app disjoint_symm.
-  Hint Extern 1 (_ = _) => unfold row; symmetry; apply app_ass.
+  Ltac t := repeat progress (simpl; intuition; subst).
+
+  Ltac use_disjoint' notDone E :=
+    match goal with
+      | [ H : disjoint _ _ |- _ ] =>
+        notDone H; generalize (H E); use_disjoint'
+          ltac:(fun H' =>
+            match H' with
+              | H => fail 1
+              | _ => notDone H'
+            end) E
+      | _ => idtac
+    end.
+  Ltac use_disjoint := use_disjoint' ltac:(fun _ => idtac).
 
   apply (deq_mut (dvar := dvar)
     (fun k (c1 c2 : con kDen k) =>
       cDen c1 = cDen c2)
     (fun k (c1 c2 : con kDen (KRecord k)) =>
-      disjoint (cDen c1) (cDen c2)));
-  simpl; intuition;
+      disjoint (cDen c1) (cDen c2))); t;
+  repeat ((unfold row; apply ext_eq)
+    || (match goal with
+          | [ H : _ |- _ ] => rewrite H
+          | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H)
+        end); t);
+  unfold disjoint; t;
     repeat (match goal with
-              | [ H : _ |- _ ] => rewrite H
-              | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H)
-            end; simpl; intuition); try congruence; unfold disjoint in *; intuition;
-    fold kDen in *; repeat match goal with
-                             | [ H : AllS _ (_ :: _) |- _ ] => inversion H; clear H; subst; simpl in *
-                           end; auto.
+              | [ |- context[match cDen ?C ?E with Some _ => _ | None => _ end] ] =>
+                use_disjoint E; destruct (cDen C E)
+              | [ |- context[if name_eq_dec ?N1 ?N2 then _ else _] ] =>
+                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)
+            end; t).
 Qed.
diff --git a/src/coq/Syntax.v b/src/coq/Syntax.v
index d73f5361..7fc085b4 100644
--- a/src/coq/Syntax.v
+++ b/src/coq/Syntax.v
@@ -25,10 +25,13 @@
  * POSSIBILITY OF SUCH DAMAGE.
  *)
 
+Require Import String.
+
 Set Implicit Arguments.
 
 
-Definition name := nat.
+Definition name : Type := string.
+Definition name_eq_dec : forall (x y : name), {x = y} + {x <> y} := string_dec.
 
 
 (** Syntax of Featherweight Ur *)
@@ -53,8 +56,7 @@ Section vars.
   | CEmpty : forall k, con (KRecord k)
   | CSingle : forall k, con KName -> con k -> con (KRecord k)
   | CConcat : forall k, con (KRecord k) -> con (KRecord k) -> con (KRecord k)
-  | CFold : forall k1 k2, con (KArrow (KArrow KName (KArrow k1 (KArrow k2 k2)))
-    (KArrow k2 (KArrow (KRecord k1) k2)))
+  | CMap : forall k1 k2, con (KArrow (KArrow k1 k2) (KArrow (KRecord k1) (KRecord k2)))
   | CGuarded : forall k1 k2, con (KRecord k1) -> con (KRecord k1) -> con k2 -> con k2.
 
   Variable dvar : forall k, con (KRecord k) -> con (KRecord k) -> Type.
@@ -121,7 +123,7 @@ Section vars.
 
   | DEq : forall k (c1 c2 c1' : con (KRecord k)),
     disj c1 c2
-    -> deq c1 c1'
+    -> deq c1' c1
     -> disj c1' c2
 
   with deq : forall k, con k -> con k -> Prop :=
@@ -145,42 +147,30 @@ Section vars.
 
   | Eq_Concat_Empty : forall k c,
     deq (CConcat (CEmpty k) c) c
+  | Eq_Concat_Comm : forall k (c1 c2 c3 : con (KRecord k)),
+    disj c1 c2
+    -> deq (CConcat c1 c2) (CConcat c2 c1)
   | Eq_Concat_Assoc : forall k (c1 c2 c3 : con (KRecord k)),
     deq (CConcat c1 (CConcat c2 c3)) (CConcat (CConcat c1 c2) c3)
 
-  | Eq_Fold_Empty : forall k1 k2 f i,
-    deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CEmpty _)) i
-  | Eq_Fold_Cons : forall k1 k2 f i c1 c2 c3,
+  | Eq_Map_Empty : forall k1 k2 f,
+    deq (CApp (CApp (CMap k1 k2) f) (CEmpty _)) (CEmpty _)
+  | Eq_Map_Cons : forall k1 k2 f c1 c2 c3,
     disj (CSingle c1 c2) c3
-    -> deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CConcat (CSingle c1 c2) c3))
-    (CApp (CApp (CApp f c1) c2) (CApp (CApp (CApp (CFold k1 k2) f) i) c3))
+    -> 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
+    (*disj c1 c2
+    ->*) deq (CGuarded c1 c2 c) c
 
   | Eq_Map_Ident : forall k c,
-    deq (CApp (CApp (CApp (CFold k (KRecord k))
-      (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CVar x2)) (CVar x3))))))
-    (CEmpty _)) c) c
+    deq (CApp (CApp (CMap k k) (CAbs (fun x => CVar x))) c) c
   | Eq_Map_Dist : forall k1 k2 f c1 c2,
-    deq (CApp (CApp (CApp (CFold k1 (KRecord k2))
-      (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f (CVar x2))) (CVar x3))))))
-    (CEmpty _)) (CConcat c1 c2))
-    (CConcat
-      (CApp (CApp (CApp (CFold k1 (KRecord k2))
-        (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f (CVar x2))) (CVar x3))))))
-      (CEmpty _)) c1)
-      (CApp (CApp (CApp (CFold k1 (KRecord k2))
-        (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f (CVar x2))) (CVar x3))))))
-      (CEmpty _)) c2))
-
-  | Eq_Fold_Fuse : forall k1 k2 k3 f i f' c,
-    deq (CApp (CApp (CApp (CFold k1 k2) f) i)
-      (CApp (CApp (CApp (CFold k3 (KRecord k1))
-        (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f' (CVar x2))) (CVar x3))))))
-      (CEmpty _)) c))
-    (CApp (CApp (CApp (CFold k3 k2)
-      (CAbs (fun x1 => CAbs (fun x2 => CApp (CApp f (CVar x1)) (CApp f' (CVar x2))))))
-      i) c).
+    deq (CApp (CApp (CMap k1 k2) f) (CConcat c1 c2))
+    (CConcat (CApp (CApp (CMap k1 k2) f) c1) (CApp (CApp (CMap k1 k2) f) c2))
+  | Eq_Map_Fuse : forall k1 k2 k3 f f' c,
+    deq (CApp (CApp (CMap k2 k3) f')
+      (CApp (CApp (CMap k1 k2) f) c))
+    (CApp (CApp (CMap k1 k3) (CAbs (fun x => CApp f' (CApp f (CVar x))))) c).
 End vars.