-
Notifications
You must be signed in to change notification settings - Fork 11
/
trace_lib.v
148 lines (122 loc) · 4.31 KB
/
trace_lib.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
(* monae: Monadic equational reasoning in Coq *)
(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later *)
Ltac typeof X := type of X.
Require Import ZArith.
From mathcomp Require Import all_ssreflect.
From infotheo Require Import ssrZ.
Require Import hierarchy monad_lib.
(******************************************************************************)
(* Example using the trace monad *)
(******************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope monae_scope.
Definition marks T {M : traceMonad T} (l : seq T) : M (seq unit) :=
sequence (map mark l).
Local Open Scope zarith_ext_scope.
Section statetrace_program_equivalence_example.
Local Open Scope do_notation.
Variable M : stateTraceMonad Z nat.
Let st_none1 : M Z :=
do _ <- st_mark '|0|;
do n <- st_get;
do _ <- st_put (n + 1)%Z;
do _ <- st_mark '|n|;
Ret n.
Let st_none2 : M Z :=
do n <- st_get;
do _ <- st_mark '|0|;
do _ <- st_mark '|n|;
do _ <- st_put (n + 1)%Z;
Ret n.
Goal st_none1 = st_none2.
Proof.
rewrite /st_none1 /st_none2 st_getmark bindA.
bind_ext; case.
bind_ext => n.
by rewrite -bindA st_putmark bindA.
Qed.
End statetrace_program_equivalence_example.
Section statetrace_example.
Local Open Scope do_notation.
Variables (T : UU0) (M : stateTraceMonad Z T).
Variables (log0 log1 : T).
Definition monadtrace_example (m0 m1 m2 : M nat) : M nat :=
do x <- m0;
st_put (Z_of_nat x) >>
do y <- st_get;
st_mark log0 >>
do z <- m2;
st_mark log1 >>
Ret (x + Z.abs_nat y + z).
End statetrace_example.
Definition assoc {A B C : Type} : (A * B) * C -> A * (B * C) :=
fun x => (x.1.1, (x.1.2, x.2)).
Definition assoc_inv {A B C : Type} : A * (B * C) -> (A * B) * C :=
fun x => ((x.1, x.2.1), x.2.2).
Definition assoc_opt
{A B C : Type} (x : option (A * B) * C) : option (A * (B * C)) :=
match x with
| (None, _) => None
| (Some (a, b), c) => Some (a, (b, c))
end.
Section relation_statetrace_state_trace.
Variables (S T : UU0) (MN : stateTraceReifyMonad S T).
Lemma st_get_get (M : stateReifyMonad S) s :
reify (st_get : MN _) s = assoc_opt (reify (get : M _) s.1, s.2).
Proof. by case: s => s1 s2; rewrite reifyget reifystget. Qed.
Lemma st_put_put (M : stateReifyMonad S) s s' :
reify (st_put s' : MN _) s = assoc_opt (reify (put s' : M _) s.1, s.2).
Proof. by case: s => s1 s2; rewrite reifyput reifystput. Qed.
Fail Lemma stMark_Mark (M : traceReifyMonad T) s t :
Reify (stMark t : MN _) s =
let x := Reify (Mark t : M _) s.2 in
match x with
| None => None
| Some x => Some (x.1, (s.1, x.2))
end.
(*Proof. by rewrite reifytmark reifystmark. Qed.*)
End relation_statetrace_state_trace.
(* wip *)
Module MonadTrans.
Structure t (m : monad) (u : monad) : Type := Pack {
lift : forall A, m A -> u A ;
drop : forall A, u A -> m A
}.
End MonadTrans.
Arguments MonadTrans.lift {m} {u} _ {_}.
Arguments MonadTrans.drop {m} {u} _ {_}.
Local Notation "'Lift'" := MonadTrans.lift.
Local Notation "'Drop'" := MonadTrans.drop.
(* TODO: hb *)
Module Tracer.
Record class m (v : traceMonad unit) (mv : MonadTrans.t m v) : Type := Class {
(* NB: see also monad_transformer.v *)
lift_ret : forall (A : UU0) (a : A), Lift mv (Ret a) = Ret a :> v A ;
lift_bind : forall A B (m0 : m A) (f : A -> m B),
Lift mv (m0 >>= f) = Lift mv m0 >>= (@MonadTrans.lift _ _ mv _ \o f) :> v B ;
drop_ret : forall (A : UU0) (a : A), Drop mv (Ret a) = Ret a :> m A ;
drop_bind : forall A B (m0 : v B) (f : B -> v A),
Drop mv (m0 >>= f) = Drop mv m0 >>= (@MonadTrans.drop _ _ mv _ \o f) :> m A ;
drop_mark : Drop mv (mark tt) = Ret tt
}.
(* the monad v is a tracer of the monad m *)
Structure t := Pack { m : monad ;
v : traceMonad unit ;
mv : MonadTrans.t m v ;
class_of : class mv }.
End Tracer.
Coercion Tracer.mv : Tracer.t >-> MonadTrans.t.
Section tracer_example.
Local Open Scope do_notation.
Variable (M : Tracer.t).
Let v : traceMonad unit := Tracer.v M.
Let m : monad := Tracer.m M.
Definition tracer_example (m0 m1 m2 : m nat) : v _ :=
do x <- Lift M m0;
do y <- Lift M m1;
mark tt >>
do z <- Lift M m2;
Ret (x + y + z).
End tracer_example.