summaryrefslogtreecommitdiff
path: root/src/coq
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-21 11:23:24 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-21 11:23:24 -0500
commit06c8fa2f35ba45081eca93d4ff6666eb83d16037 (patch)
tree95cdf86ddabc3237e5b5fb28160fbf03c4b73148 /src/coq
parent2bfa859812bcf33fa05372d668ac363d17bc8892 (diff)
map-only syntax and semantics
Diffstat (limited to 'src/coq')
-rw-r--r--src/coq/Semantics.v136
-rw-r--r--src/coq/Syntax.v56
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.