Skip to content

Commit ff0e272

Browse files
gmalechagmalecha
committed
making MonadWriter polymorphic.
1 parent 4f715f0 commit ff0e272

File tree

5 files changed

+102
-69
lines changed

5 files changed

+102
-69
lines changed

‎examples/Printing.v‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
Require Import Coq.Strings.String.
22
Require Import ExtLib.Structures.MonadWriter.
3+
Require Import ExtLib.Data.PPair.
34
Require Import ExtLib.Data.Monads.WriterMonad.
45
Require Import ExtLib.Data.Monads.IdentityMonad.
56
Require Import ExtLib.Programming.Show.
@@ -16,11 +17,14 @@ Definition printString (str : string) : PrinterMonad unit :=
1617
(@show_exact str _ show_inj (@show_mon _ ShowScheme_string_compose)).
1718

1819
Definition runPrinter {T : Type} (c : PrinterMonad T) : T * string :=
19-
let '(val,str) := unIdent (runWriterT c) in
20+
let '(ppair val str) := unIdent (runWriterT c) in
2021
(val, str ""%string).
2122

2223

23-
Eval compute in runPrinter (Monad.bind (print 1) (fun _ => print 2)).
24+
Eval compute in
25+
runPrinter (Monad.bind (print 1) (fun _ => print 2)).
2426

25-
Eval compute in runPrinter (Monad.bind (print "hello "%string) (fun _ => print 2)).
26-
Eval compute in runPrinter (Monad.bind (printString "hello "%string) (fun _ => print 2)).
27+
Eval compute in
28+
runPrinter (Monad.bind (print "hello "%string) (fun _ => print 2)).
29+
Eval compute in
30+
runPrinter (Monad.bind (printString "hello "%string) (fun _ => print 2)).

‎theories/Data/Graph/GraphAdjList.v‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,14 @@
1-
Require Import ExtLib.Data.List.
2-
Require Import ExtLib.Data.Graph.Graph.
3-
Require Import ExtLib.Data.Graph.BuildGraph.
4-
Require Import ExtLib.Structures.Maps.
51
Require Import ExtLib.Core.RelDec.
62
Require Import ExtLib.Structures.Monads.
7-
Require Import ExtLib.Data.Monads.WriterMonad.
8-
Require Import ExtLib.Data.Monads.IdentityMonad.
93
Require Import ExtLib.Structures.Monoid.
104
Require Import ExtLib.Structures.Reducible.
5+
Require Import ExtLib.Structures.Maps.
6+
Require Import ExtLib.Data.List.
7+
Require Import ExtLib.Data.PPair.
8+
Require Import ExtLib.Data.Monads.WriterMonad.
9+
Require Import ExtLib.Data.Monads.IdentityMonad.
10+
Require Import ExtLib.Data.Graph.Graph.
11+
Require Import ExtLib.Data.Graph.BuildGraph.
1112

1213
Set Implicit Arguments.
1314
Set Strict Implicit.
@@ -22,10 +23,10 @@ Section GraphImpl.
2223
Definition adj_graph : Type := map.
2324

2425
Definition verts (g : adj_graph) : list V :=
25-
let c := foldM (m := writerT (Monoid_list_app) ident)
26+
let c := foldM (m := writerT (Monoid_list_app) ident)
2627
(fun k_v _ => let k := fst k_v in tell (k :: nil)) (ret tt) g
2728
in
28-
snd (unIdent (runWriterT c)).
29+
psnd (unIdent (runWriterT c)).
2930

3031
Definition succs (g : adj_graph) (v : V) : list V :=
3132
match lookup v g with
@@ -43,12 +44,12 @@ Section GraphImpl.
4344

4445
(** TODO: Move this **)
4546
Fixpoint list_in_dec v (ls : list V) : bool :=
46-
match ls with
47-
| nil => false
48-
| l :: ls =>
49-
if eq_dec l v then true
50-
else list_in_dec v ls
51-
end.
47+
match ls with
48+
| nil => false
49+
| l :: ls =>
50+
if eq_dec l v then true
51+
else list_in_dec v ls
52+
end.
5253

5354
Definition add_edge (f t : V) (g : adj_graph) : adj_graph :=
5455
match lookup f g with
@@ -66,4 +67,3 @@ Section GraphImpl.
6667
}.
6768

6869
End GraphImpl.
69-

‎theories/Data/Monads/WriterMonad.v‎

Lines changed: 33 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,38 +1,47 @@
11
Require Import ExtLib.Structures.Monads.
22
Require Import ExtLib.Structures.Monoid.
3+
Require Import ExtLib.Data.PPair.
34

45
Set Implicit Arguments.
56
Set Maximal Implicit Insertion.
7+
Set Universe Polymorphism.
8+
9+
Set Printing Universes.
610

711
Section WriterType.
8-
Variable S : Type.
12+
Polymorphic Universe s d c.
13+
Variable S : Type@{s}.
914

10-
Record writerT (Monoid_S : Monoid S) (m : Type -> Type) (t : Type) : Type := mkWriterT
11-
{ runWriterT : m (t * S)%type }.
15+
Record writerT (Monoid_S : Monoid@{s} S) (m : Type@{d} -> Type@{c}) (t : Type@{d}) : Type := mkWriterT
16+
{ runWriterT : m (pprod t S)%type }.
1217

1318
Variable Monoid_S : Monoid S.
14-
Variable m : Type -> Type.
19+
Variable m : Type@{d} -> Type@{c}.
1520
Context {M : Monad m}.
1621

17-
Definition execWriterT {T} (c : writerT Monoid_S m T) : m S :=
18-
bind (runWriterT c) (fun (x : T * S) => ret (snd x)).
22+
Definition execWriterT {T} (c : writerT Monoid_S m T) : m S :=
23+
bind (runWriterT c) (fun (x : pprod T S) => ret (psnd x)).
24+
25+
Definition evalWriterT {T} (c : writerT Monoid_S m T) : m T :=
26+
bind (runWriterT c) (fun (x : pprod T S) => ret (pfst x)).
1927

20-
Definition evalWriterT {T} (c : writerT Monoid_S m T) : m T :=
21-
bind (runWriterT c) (fun (x : T * S) => ret (fst x)).
28+
Local Notation "( x , y )" := (ppair x y).
2229

2330
Global Instance Monad_writerT : Monad (writerT Monoid_S m) :=
2431
{ ret := fun _ x => mkWriterT _ _ _ (@ret _ M _ (x, monoid_unit Monoid_S))
2532
; bind := fun _ _ c1 c2 =>
2633
mkWriterT _ _ _ (
2734
@bind _ M _ _ (runWriterT c1) (fun v =>
28-
bind (runWriterT (c2 (fst v))) (fun v' =>
29-
ret (fst v', monoid_plus Monoid_S (snd v) (snd v')))))
35+
bind (runWriterT (c2 (pfst v))) (fun v' =>
36+
ret (pfst v', monoid_plus Monoid_S (psnd v) (psnd v')))))
3037
}.
3138

3239
Global Instance Writer_writerT : MonadWriter Monoid_S (writerT Monoid_S m) :=
3340
{ tell := fun x => mkWriterT _ _ _ (ret (tt, x))
34-
; listen := fun _ c => mkWriterT _ _ _ (bind (runWriterT c) (fun x => ret (fst x, snd x, snd x)))
35-
; pass := fun _ c => mkWriterT _ _ _ (bind (runWriterT c) (fun x => ret (let '(x,ss,s) := x in (x, ss s))))
41+
; listen := fun _ c => mkWriterT _ _ _ (bind (runWriterT c)
42+
(fun x => ret (pair (pfst x) (psnd x), psnd x)))
43+
; pass := fun _ c => mkWriterT _ _ _ (bind (runWriterT c)
44+
(fun x => ret (let '(ppair (pair x ss) s) := x in (x, ss s))))
3645
}.
3746

3847
Global Instance MonadT_writerT : MonadT (writerT Monoid_S m) m :=
@@ -58,14 +67,22 @@ Section WriterType.
5867
; catch := fun _ c h => mkWriterT _ _ _ (catch (runWriterT c) (fun x => runWriterT (h x)))
5968
}.
6069

61-
Global Instance Writer_writerT_pass {T} {MonT : Monoid T} {_ : Monad m} {_ : MonadWriter MonT m} : MonadWriter MonT (writerT Monoid_S m) :=
62-
{ tell := fun x => mkWriterT _ m _ (bind (tell x) (fun x => ret (x, monoid_unit Monoid_S)))
63-
; listen := fun _ c => mkWriterT _ m _ (bind (listen (runWriterT c)) (fun x => let '(a,t,s) := x in ret (a,s,t)))
64-
; pass := fun _ c => mkWriterT _ m _ (pass (bind (runWriterT c) (fun x => let '(a,t,s) := x in ret (a,s,t))))
70+
Global Instance Writer_writerT_pass {T} {MonT : Monoid T} {M : Monad m} {MW : MonadWriter MonT m}
71+
: MonadWriter MonT (writerT Monoid_S m) :=
72+
{ tell := fun x => mkWriterT _ m _ (bind (tell x)
73+
(fun x => ret (x, monoid_unit Monoid_S)))
74+
; listen := fun _ c => mkWriterT _ m _ (bind (m:=m) (@listen _ _ _ MW _ (runWriterT c))
75+
(fun x => let '(pair (ppair a t) s) := x in
76+
ret (m:=m) (pair a s,t)))
77+
; pass := fun _ c => mkWriterT _ m _ (@pass _ _ _ MW _
78+
(bind (m:=m) (runWriterT c)
79+
(fun x => let '(ppair (pair a t) s) := x in
80+
ret (m:=m) (pair (ppair a s) t))))
6581
}.
6682

6783
End WriterType.
6884

85+
Arguments mkWriterT {_} _ {_ _} _.
6986
Arguments runWriterT {S} {Monoid_S} {m} {t} _.
7087
Arguments evalWriterT {S} {Monoid_S} {m} {M} {T} _.
7188
Arguments execWriterT {S} {Monoid_S} {m} {M} {T} _.

‎theories/Data/PList.v‎

Lines changed: 16 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,12 @@ Require Import ExtLib.Data.POption.
44
Require Import ExtLib.Data.PPair.
55
Require Import ExtLib.Core.RelDec.
66
Require Import ExtLib.Tactics.Consider.
7+
Require Import ExtLib.Tactics.Injection.
78

89
Require Import Coq.Bool.Bool.
910

1011
Set Universe Polymorphism.
12+
Set Primitive Projections.
1113

1214
Section plist.
1315
Polymorphic Universe i.
@@ -118,36 +120,36 @@ Arguments nth_error {_} _ _.
118120

119121

120122
Section plistFun.
121-
Polymorphic Fixpoint split {A B : Type} (lst : plist (ppair A B)) :=
123+
Polymorphic Fixpoint split {A B : Type} (lst : plist (pprod A B)) :=
122124
match lst with
123125
| pnil => (pnil, pnil)
124-
| pcons (pprod x y) tl => let (left, right) := split tl in (pcons x left, pcons y right)
126+
| pcons (ppair x y) tl => let (left, right) := split tl in (pcons x left, pcons y right)
125127
end.
126128

127-
Lemma pIn_split_l {A B : Type} (lst : plist (ppair A B)) (p : ppair A B) (H : pIn p lst) :
129+
Lemma pIn_split_l {A B : Type} (lst : plist (pprod A B)) (p : pprod A B) (H : pIn p lst) :
128130
(pIn (pfst p) (fst (split lst))).
129131
Proof.
130132
destruct p; simpl.
131133
induction lst; simpl in *.
132134
+ destruct H.
133135
+ destruct t; simpl.
134136
destruct (split lst); simpl.
135-
destruct H as [H | H]; [
136-
inversion H; left; reflexivity |
137-
right; apply IHlst; apply H].
138-
Qed.
137+
destruct H as [H | H].
138+
{ inv_all. tauto. }
139+
{ tauto. }
140+
Qed.
139141

140-
Lemma pIn_split_r {A B : Type} (lst : plist (ppair A B)) (p : ppair A B) (H : pIn p lst) :
142+
Lemma pIn_split_r {A B : Type} (lst : plist (pprod A B)) (p : pprod A B) (H : pIn p lst) :
141143
(pIn (psnd p) (snd (split lst))).
142144
Proof.
143145
destruct p; simpl.
144146
induction lst; simpl in *.
145147
+ destruct H.
146148
+ destruct t; simpl.
147149
destruct (split lst); simpl.
148-
destruct H as [H | H]; [
149-
inversion H; left; reflexivity |
150-
right; apply IHlst; apply H].
150+
destruct H.
151+
{ inv_all; tauto. }
152+
{ tauto. }
151153
Qed.
152154

153155
Lemma pIn_app_iff (A : Type) (l l' : plist A) (a : A) :
@@ -170,7 +172,7 @@ Section plistOk.
170172
+ left; reflexivity.
171173
+ right; apply IHlst; assumption.
172174
Qed.
173-
175+
174176
Lemma inb_complete (x : A) (lst : plist A) (H : pIn x lst) : inb x lst = true.
175177
Proof.
176178
induction lst; simpl in *; try intuition congruence.
@@ -187,7 +189,7 @@ Section plistOk.
187189
* intro H. apply inb_complete in H. intuition congruence.
188190
* apply IHlst; assumption.
189191
Qed.
190-
192+
191193
Lemma nodup_complete (lst : plist A) (H : pNoDup lst) : nodup lst = true.
192194
Proof.
193195
induction lst.
@@ -196,7 +198,7 @@ Section plistOk.
196198
* apply eq_true_not_negb. intros H; apply H2. apply inb_sound; assumption.
197199
* apply IHlst; assumption.
198200
Qed.
199-
201+
200202
End plistOk.
201203

202204
Section pmap.
@@ -269,4 +271,3 @@ Section PListEq.
269271
Qed.
270272

271273
End PListEq.
272-

‎theories/Data/PPair.v‎

Lines changed: 30 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,32 +1,40 @@
11
Require Import ExtLib.Core.RelDec.
2+
Require Import ExtLib.Tactics.Injection.
23

34
Set Printing Universes.
45
Set Primitive Projections.
56
Set Universe Polymorphism.
7+
68
Section pair.
79
Polymorphic Universes i j.
810
Variable (T : Type@{i}) (U : Type@{j}).
911

10-
Polymorphic Inductive ppair : Type@{max (i, j)} :=
11-
| pprod : T -> U -> ppair.
12-
13-
Polymorphic Definition pfst (p : ppair) :=
14-
match p with
15-
| pprod t _ => t
16-
end.
17-
18-
Polymorphic Definition psnd (p : ppair) :=
19-
match p with
20-
| pprod _ u => u
21-
end.
12+
Polymorphic Record pprod : Type@{max (i, j)} := ppair
13+
{ pfst : T
14+
; psnd : U }.
2215

2316
End pair.
2417

25-
Arguments ppair _ _.
26-
Arguments pprod {_ _} _ _.
18+
Arguments pprod _ _.
19+
Arguments ppair {_ _} _ _.
2720
Arguments pfst {_ _} _.
2821
Arguments psnd {_ _} _.
2922

23+
Section Injective.
24+
Polymorphic Universes i j.
25+
Context {T : Type@{i}} {U : Type@{j}}.
26+
27+
Global Instance Injective_pprod (a : T) (b : U) c d
28+
: Injective (ppair a b = ppair c d) :=
29+
{ result := a = c /\ b = d }.
30+
Proof.
31+
intros.
32+
change a with (pfst@{i j} {| pfst := a ; psnd := b |}).
33+
change b with (psnd@{i j} {| pfst := a ; psnd := b |}) at 2.
34+
rewrite H. split; reflexivity.
35+
Defined.
36+
End Injective.
37+
3038
Section PProdEq.
3139
Polymorphic Universes i j.
3240
Context {T : Type@{i}} {U : Type@{j}}.
@@ -35,20 +43,23 @@ Section PProdEq.
3543
Context {EDCT : RelDec_Correct EDT}.
3644
Context {EDCU : RelDec_Correct EDU}.
3745

38-
Polymorphic Definition ppair_eqb (p1 p2 : ppair T U) : bool :=
46+
Polymorphic Definition ppair_eqb (p1 p2 : pprod T U) : bool :=
3947
pfst p1 ?[ eq ] pfst p2 && psnd p1 ?[ eq ] psnd p2.
4048

4149
(** Specialization for equality **)
42-
Global Polymorphic Instance RelDec_eq_ppair : RelDec (@eq (@ppair T U)) :=
50+
Global Polymorphic Instance RelDec_eq_ppair : RelDec (@eq (@pprod T U)) :=
4351
{ rel_dec := ppair_eqb }.
4452

45-
Global Polymorphic Instance RelDec_Correct_eq_ppair : RelDec_Correct RelDec_eq_ppair.
53+
Global Polymorphic Instance RelDec_Correct_eq_ppair
54+
: RelDec_Correct RelDec_eq_ppair.
4655
Proof.
4756
constructor. intros p1 p2. destruct p1, p2. simpl.
4857
unfold ppair_eqb. simpl.
4958
rewrite Bool.andb_true_iff.
5059
repeat rewrite rel_dec_correct.
51-
split; intuition congruence.
60+
split.
61+
{ destruct 1. f_equal; assumption. }
62+
{ intros. inv_all. tauto. }
5263
Qed.
5364

54-
End PProdEq.
65+
End PProdEq.

0 commit comments

Comments
 (0)