include "utilities/monad.ma".
include "basics/types.ma".
include "basics/lists/list.ma".
definition Trace ≝ λT : Type[0].MakeMonad (mk_MonadDefinition
  (* the monad *)
  (λX.X × (list T))
  (* return *)
  (λX,x.〈x, [ ]〉)
  (* bind *)
  (λX,Y,m,f. let 〈x, ts〉 ≝ m in let 〈y,ts'〉 ≝ f x in 〈y, ts @ ts'〉)
  ???).
[(* bind_bind *)
 #X#Y#Z*#x#t1#f#g
 normalize elim (f x)
 #y#t2 normalize elim (g y)
 #z#t3 normalize >associative_append //
|(* bind_ret *)
 #X*#x#t normalize >append_nil //
|(* ret_bind *)
  #X#Y#x#f normalize elim (f x) #y #t' normalize //
]
qed.

include "hints_declaration.ma".
unification hint 0 ≔ X, T;
M ≟ Trace T
(*---------------*) ⊢
X × (list T) ≡ monad M X
.

definition trace_emit : ∀T. T → monad (Trace T) unit ≝
  λT,t.〈it, [t]〉.

definition trace_emits : ∀T. list T → monad (Trace T) unit ≝
  λT,ts.〈it, ts〉.