Last change
on this file since 2919 was
1882,
checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size:
895 bytes

Line  

1  include "utilities/monad.ma". 

2  include "basics/types.ma". 

3  include "basics/lists/list.ma". 

4  definition 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  ] 

22  qed. 

23  

24  include "hints_declaration.ma". 

25  unification hint 0 ≔ X, T; 

26  M ≟ Trace T 

27  (**) ⊢ 

28  X × (list T) ≡ monad M X 

29  . 

30  

31  definition trace_emit : ∀T. T → monad (Trace T) unit ≝ 

32  λT,t.〈it, [t]〉. 

33  

34  definition 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.