making MonadWriter polymorphic.

examples/Printing.v

@@ -1,5 +1,6 @@
 Require Import Coq.Strings.String.
 Require Import ExtLib.Structures.MonadWriter.
+Require Import ExtLib.Data.PPair.
 Require Import ExtLib.Data.Monads.WriterMonad.
 Require Import ExtLib.Data.Monads.IdentityMonad.
 Require Import ExtLib.Programming.Show.
@@ -16,11 +17,14 @@ Definition printString (str : string) : PrinterMonad unit :=
                     (@show_exact str _ show_inj (@show_mon _ ShowScheme_string_compose)).
 
 Definition runPrinter {T : Type} (c : PrinterMonad T) : T * string :=
-  let '(val,str) := unIdent (runWriterT c) in
+  let '(ppair val str) := unIdent (runWriterT c) in
   (val, str ""%string).
 
 
-Eval compute in runPrinter (Monad.bind (print 1) (fun _ => print 2)).
+Eval compute in
+    runPrinter (Monad.bind (print 1) (fun _ => print 2)).
 
-Eval compute in runPrinter (Monad.bind (print "hello "%string) (fun _ => print 2)).
-Eval compute in runPrinter (Monad.bind (printString "hello "%string) (fun _ => print 2)).
+Eval compute in
+    runPrinter (Monad.bind (print "hello "%string) (fun _ => print 2)).
+Eval compute in
+    runPrinter (Monad.bind (printString "hello "%string) (fun _ => print 2)).

theories/Data/Graph/GraphAdjList.v

@@ -1,13 +1,14 @@
-Require Import ExtLib.Data.List.
-Require Import ExtLib.Data.Graph.Graph.
-Require Import ExtLib.Data.Graph.BuildGraph.
-Require Import ExtLib.Structures.Maps.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Structures.Monads.
-Require Import ExtLib.Data.Monads.WriterMonad.
-Require Import ExtLib.Data.Monads.IdentityMonad.
 Require Import ExtLib.Structures.Monoid.
 Require Import ExtLib.Structures.Reducible.
+Require Import ExtLib.Structures.Maps.
+Require Import ExtLib.Data.List.
+Require Import ExtLib.Data.PPair.
+Require Import ExtLib.Data.Monads.WriterMonad.
+Require Import ExtLib.Data.Monads.IdentityMonad.
+Require Import ExtLib.Data.Graph.Graph.
+Require Import ExtLib.Data.Graph.BuildGraph.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -22,10 +23,10 @@ Section GraphImpl.
   Definition adj_graph : Type := map.
 
   Definition verts (g : adj_graph) : list V :=
-    let c := foldM (m := writerT (Monoid_list_app) ident) 
+    let c := foldM (m := writerT (Monoid_list_app) ident)
       (fun k_v _ => let k := fst k_v in tell (k :: nil)) (ret tt) g
     in
-    snd (unIdent (runWriterT c)).
+    psnd (unIdent (runWriterT c)).
 
   Definition succs (g : adj_graph) (v : V) : list V :=
     match lookup v g with
@@ -43,12 +44,12 @@ Section GraphImpl.
 
   (** TODO: Move this **)
   Fixpoint list_in_dec v (ls : list V) : bool :=
-      match ls with
-        | nil => false
-        | l :: ls =>
-          if eq_dec l v then true
-          else list_in_dec v ls
-      end.
+    match ls with
+    | nil => false
+    | l :: ls =>
+      if eq_dec l v then true
+      else list_in_dec v ls
+    end.
 
   Definition add_edge (f t : V) (g : adj_graph) : adj_graph :=
     match lookup f g with
@@ -66,4 +67,3 @@ Section GraphImpl.
   }.
 
 End GraphImpl.
-

theories/Data/Monads/WriterMonad.v

@@ -1,38 +1,47 @@
 Require Import ExtLib.Structures.Monads.
 Require Import ExtLib.Structures.Monoid.
+Require Import ExtLib.Data.PPair.
 
 Set Implicit Arguments.
 Set Maximal Implicit Insertion.
+Set Universe Polymorphism.
+
+Set Printing Universes.
 
 Section WriterType.
-  Variable S : Type.
+  Polymorphic Universe s d c.
+  Variable S : Type@{s}.
 
-  Record writerT (Monoid_S : Monoid S) (m : Type -> Type) (t : Type) : Type := mkWriterT
-  { runWriterT : m (t * S)%type }.
+  Record writerT (Monoid_S : Monoid@{s} S) (m : Type@{d} -> Type@{c}) (t : Type@{d}) : Type := mkWriterT
+  { runWriterT : m (pprod t S)%type }.
 
   Variable Monoid_S : Monoid S.
-  Variable m : Type -> Type.
+  Variable m : Type@{d} -> Type@{c}.
   Context {M : Monad m}.
 
-  Definition execWriterT {T} (c : writerT Monoid_S m T) : m S := 
-    bind (runWriterT c) (fun (x : T * S) => ret (snd x)).
+  Definition execWriterT {T} (c : writerT Monoid_S m T) : m S :=
+    bind (runWriterT c) (fun (x : pprod T S) => ret (psnd x)).
+
+  Definition evalWriterT {T} (c : writerT Monoid_S m T) : m T :=
+    bind (runWriterT c) (fun (x : pprod T S) => ret (pfst x)).
 
-  Definition evalWriterT {T} (c : writerT Monoid_S m T) : m T := 
-    bind (runWriterT c) (fun (x : T * S) => ret (fst x)).
+  Local Notation "( x , y )" := (ppair x y).
 
   Global Instance Monad_writerT : Monad (writerT Monoid_S m) :=
   { ret := fun _ x => mkWriterT _ _ _ (@ret _ M _ (x, monoid_unit Monoid_S))
   ; bind := fun _ _ c1 c2 =>
     mkWriterT _ _ _ (
       @bind _ M _ _ (runWriterT c1) (fun v =>
-        bind (runWriterT (c2 (fst v))) (fun v' =>
-        ret (fst v', monoid_plus Monoid_S (snd v) (snd v')))))
+        bind (runWriterT (c2 (pfst v))) (fun v' =>
+        ret (pfst v', monoid_plus Monoid_S (psnd v) (psnd v')))))
   }.
 
   Global Instance Writer_writerT : MonadWriter Monoid_S (writerT Monoid_S m) :=
   { tell   := fun x => mkWriterT _ _ _ (ret (tt, x))
-  ; listen := fun _ c => mkWriterT _ _ _ (bind (runWriterT c) (fun x => ret (fst x, snd x, snd x)))
-  ; pass   := fun _ c => mkWriterT _ _ _ (bind (runWriterT c) (fun x => ret (let '(x,ss,s) := x in (x, ss s))))
+  ; listen := fun _ c => mkWriterT _ _ _ (bind (runWriterT c)
+                                               (fun x => ret (pair (pfst x) (psnd x), psnd x)))
+  ; pass   := fun _ c => mkWriterT _ _ _ (bind (runWriterT c)
+                                               (fun x => ret (let '(ppair (pair x ss) s) := x in (x, ss s))))
   }.
 
   Global Instance MonadT_writerT : MonadT (writerT Monoid_S m) m :=
@@ -58,14 +67,22 @@ Section WriterType.
   ; catch := fun _ c h => mkWriterT _ _ _ (catch (runWriterT c) (fun x => runWriterT (h x)))
   }.
 
-  Global Instance Writer_writerT_pass {T} {MonT : Monoid T} {_ : Monad m} {_ : MonadWriter MonT m} : MonadWriter MonT (writerT Monoid_S m) :=
-  { tell   := fun x => mkWriterT _ m _ (bind (tell x) (fun x => ret (x, monoid_unit Monoid_S)))
-  ; listen := fun _ c => mkWriterT _ m _ (bind (listen (runWriterT c)) (fun x => let '(a,t,s) := x in ret (a,s,t)))
-  ; pass   := fun _ c => mkWriterT _ m _ (pass (bind (runWriterT c) (fun x => let '(a,t,s) := x in ret (a,s,t))))
+  Global Instance Writer_writerT_pass {T} {MonT : Monoid T} {M : Monad m} {MW : MonadWriter MonT m}
+  : MonadWriter MonT (writerT Monoid_S m) :=
+  { tell   := fun x => mkWriterT _ m _ (bind (tell x)
+                                             (fun x => ret (x, monoid_unit Monoid_S)))
+  ; listen := fun _ c => mkWriterT _ m _ (bind (m:=m) (@listen _ _ _ MW  _ (runWriterT c))
+                                               (fun x => let '(pair (ppair a t) s) := x in
+                                                         ret (m:=m) (pair a s,t)))
+  ; pass   := fun _ c => mkWriterT _ m _ (@pass _ _ _ MW _
+                                            (bind (m:=m) (runWriterT c)
+                                                  (fun x => let '(ppair (pair a t) s) := x in
+                                                            ret (m:=m) (pair (ppair a s) t))))
   }.
 
 End WriterType.
 
+Arguments mkWriterT {_} _ {_ _} _.
 Arguments runWriterT {S} {Monoid_S} {m} {t} _.
 Arguments evalWriterT {S} {Monoid_S} {m} {M} {T} _.
 Arguments execWriterT {S} {Monoid_S} {m} {M} {T} _.

theories/Data/PList.v

@@ -4,10 +4,12 @@ Require Import ExtLib.Data.POption.
 Require Import ExtLib.Data.PPair.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Tactics.Consider.
+Require Import ExtLib.Tactics.Injection.
 
 Require Import Coq.Bool.Bool.
 
 Set Universe Polymorphism.
+Set Primitive Projections.
 
 Section plist.
   Polymorphic Universe i.
@@ -118,36 +120,36 @@ Arguments nth_error {_} _ _.
 
 
 Section plistFun.
-  Polymorphic Fixpoint split {A B : Type} (lst : plist (ppair A B)) :=
+  Polymorphic Fixpoint split {A B : Type} (lst : plist (pprod A B)) :=
     match lst with
     | pnil => (pnil, pnil)
-    | pcons (pprod x y) tl => let (left, right) := split tl in (pcons x left, pcons y right)
+    | pcons (ppair x y) tl => let (left, right) := split tl in (pcons x left, pcons y right)
     end.
 
-  Lemma pIn_split_l {A B : Type} (lst : plist (ppair A B)) (p : ppair A B) (H : pIn p lst) : 
+  Lemma pIn_split_l {A B : Type} (lst : plist (pprod A B)) (p : pprod A B) (H : pIn p lst) :
     (pIn (pfst p) (fst (split lst))).
   Proof.
     destruct p; simpl.
     induction lst; simpl in *.
     + destruct H.
     + destruct t; simpl.
       destruct (split lst); simpl.
-      destruct H as [H | H]; [
-          inversion H; left; reflexivity |
-          right; apply IHlst; apply H].
-  Qed.      
+      destruct H as [H | H].
+      { inv_all. tauto. }
+      { tauto. }
+  Qed.
 
-  Lemma pIn_split_r {A B : Type} (lst : plist (ppair A B)) (p : ppair A B) (H : pIn p lst) : 
+  Lemma pIn_split_r {A B : Type} (lst : plist (pprod A B)) (p : pprod A B) (H : pIn p lst) :
     (pIn (psnd p) (snd (split lst))).
   Proof.
     destruct p; simpl.
     induction lst; simpl in *.
     + destruct H.
     + destruct t; simpl.
       destruct (split lst); simpl.
-      destruct H as [H | H]; [
-          inversion H; left; reflexivity |
-          right; apply IHlst; apply H].
+      destruct H.
+      { inv_all; tauto. }
+      { tauto. }
   Qed.
 
   Lemma pIn_app_iff (A : Type) (l l' : plist A) (a : A) :
@@ -170,7 +172,7 @@ Section plistOk.
     + left; reflexivity.
     + right; apply IHlst; assumption.
   Qed.
-  
+
   Lemma inb_complete (x : A) (lst : plist A) (H : pIn x lst) : inb x lst = true.
   Proof.
     induction lst; simpl in *; try intuition congruence.
@@ -187,7 +189,7 @@ Section plistOk.
       * intro H. apply inb_complete in H. intuition congruence.
       * apply IHlst; assumption.
   Qed.
-  
+
   Lemma nodup_complete (lst : plist A) (H : pNoDup lst) : nodup lst = true.
   Proof.
     induction lst.
@@ -196,7 +198,7 @@ Section plistOk.
       * apply eq_true_not_negb. intros H; apply H2. apply inb_sound; assumption.
       * apply IHlst; assumption.
   Qed.
-  
+
 End plistOk.
 
 Section pmap.
@@ -269,4 +271,3 @@ Section PListEq.
   Qed.
 
 End PListEq.
-

theories/Data/PPair.v

@@ -1,32 +1,40 @@
 Require Import ExtLib.Core.RelDec.
+Require Import ExtLib.Tactics.Injection.
 
 Set Printing Universes.
 Set Primitive Projections.
 Set Universe Polymorphism.
+
 Section pair.
   Polymorphic Universes i j.
   Variable (T : Type@{i}) (U : Type@{j}).
 
-  Polymorphic Inductive ppair : Type@{max (i, j)} :=
-  | pprod : T -> U -> ppair.
-
-  Polymorphic Definition pfst (p : ppair) :=
-    match p with
-    | pprod t _ => t
-    end.
-
-  Polymorphic Definition psnd (p : ppair) :=
-    match p with
-    | pprod _ u => u
-    end.
+  Polymorphic Record pprod : Type@{max (i, j)} := ppair
+  { pfst : T
+  ; psnd : U }.
 
 End pair.
 
-Arguments ppair _ _.
-Arguments pprod {_ _} _ _.
+Arguments pprod _ _.
+Arguments ppair {_ _} _ _.
 Arguments pfst {_ _} _.
 Arguments psnd {_ _} _.
 
+Section Injective.
+  Polymorphic Universes i j.
+  Context {T : Type@{i}} {U : Type@{j}}.
+
+  Global Instance Injective_pprod (a : T) (b : U) c d
+  : Injective (ppair a b = ppair c d) :=
+  { result := a = c /\ b = d }.
+  Proof.
+    intros.
+    change a with (pfst@{i j} {| pfst := a ; psnd := b |}).
+    change b with (psnd@{i j} {| pfst := a ; psnd := b |}) at 2.
+    rewrite H. split; reflexivity.
+  Defined.
+End Injective.
+
 Section PProdEq.
   Polymorphic Universes i j.
   Context {T : Type@{i}} {U : Type@{j}}.
@@ -35,20 +43,23 @@ Section PProdEq.
   Context {EDCT : RelDec_Correct EDT}.
   Context {EDCU : RelDec_Correct EDU}.
 
-  Polymorphic Definition ppair_eqb (p1 p2 : ppair T U) : bool :=
+  Polymorphic Definition ppair_eqb (p1 p2 : pprod T U) : bool :=
     pfst p1 ?[ eq ] pfst p2 && psnd p1 ?[ eq ] psnd p2.
 
   (** Specialization for equality **)
-  Global Polymorphic Instance RelDec_eq_ppair : RelDec (@eq (@ppair T U)) :=
+  Global Polymorphic Instance RelDec_eq_ppair : RelDec (@eq (@pprod T U)) :=
   { rel_dec := ppair_eqb }.
 
-  Global Polymorphic Instance RelDec_Correct_eq_ppair : RelDec_Correct RelDec_eq_ppair.
+  Global Polymorphic Instance RelDec_Correct_eq_ppair
+  : RelDec_Correct RelDec_eq_ppair.
   Proof.
     constructor. intros p1 p2. destruct p1, p2. simpl.
     unfold ppair_eqb. simpl.
     rewrite Bool.andb_true_iff.
     repeat rewrite rel_dec_correct.
-    split; intuition congruence.
+    split.
+    { destruct 1. f_equal; assumption. }
+    { intros. inv_all. tauto. }
   Qed.
 
-End PProdEq.
+End PProdEq.