source: src/utilities/trace.ma @ 1635

Last change on this file since 1635 was 1635, checked in by tranquil, 8 years ago
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File size: 903 bytes
Line 
1include "utilities/monad.ma".
2include "basics/types.ma".
3include "basics/lists/list.ma".
4definition Trace ≝ λT : Type[0].MakeMonad (mk_MonadDefinition
5  (* the monad *)
6  (λX.X × (list T))
7  (* return *)
8  (λX,x.〈x, [ ]〉)
9  (* bind *)
10  (λX,Y,m,f. let 〈x, ts〉 ≝ m in let 〈y,ts'〉 ≝ f x in 〈y, ts @ ts'〉)
11  ???).
12[(* bind_bind *)
13 #X#Y#Z*#x#t1#f#g
14 normalize elim (f x)
15 #y#t2 normalize elim (g y)
16 #z#t3 normalize >associative_append //
17|(* bind_ret *)
18 #X*#x#t normalize >append_nil //
19|(* ret_bind *)
20  #X#Y#x#f normalize elim (f x) #y #t' normalize //
21]
22qed.
23
24include "hints_declaration.ma".
25unification hint 0 ≔ X, T;
26M ≟ Trace T
27(*---------------*) ⊢
28X × (list T) ≡ monad (m_def M) X
29.
30
31definition trace_emit : ∀T. T → monad (Trace T) unit ≝
32  λT,t.〈it, [t]〉.
33
34definition trace_emits : ∀T. list T → monad (Trace T) unit ≝
35  λT,ts.〈it, ts〉.
36
Note: See TracBrowser for help on using the repository browser.