1 | include "utilities/monad.ma". |
---|
2 | |
---|
3 | inductive bind_new |
---|
4 | (B : Type[0]) |
---|
5 | (E : Type[0]) |
---|
6 | : Type[0] ≝ |
---|
7 | | bret : E → bind_new B E |
---|
8 | | bnew : (B → bind_new B E) → bind_new B E. |
---|
9 | |
---|
10 | interpretation "new bind_new" 'new f = (bnew ?? f). |
---|
11 | |
---|
12 | notation > "ν list1 (ident x opt ( : ty)) sep , 'in' f" |
---|
13 | with precedence 48 for |
---|
14 | @{ ${ fold right @{$f} rec acc |
---|
15 | @{ ${default |
---|
16 | @{'new (λ${ident x} : $ty.$acc)} |
---|
17 | @{'new (λ${ident x}.$acc)} |
---|
18 | }} |
---|
19 | }}. |
---|
20 | |
---|
21 | notation < "hvbox(mstyle color #0000ff (ν) ident i : ty \nbsp 'in' \nbsp break p)" |
---|
22 | with precedence 48 for |
---|
23 | @{'new (λ${ident i} : $ty. $p) }. |
---|
24 | |
---|
25 | let rec bnews B E n (f : list B → bind_new B E) on n : bind_new B E ≝ |
---|
26 | match n with |
---|
27 | [ O ⇒ f [ ] |
---|
28 | | S x ⇒ νy in bnews … x (λl. f (y :: l)) |
---|
29 | ]. |
---|
30 | |
---|
31 | let rec bnews_strong B E n (f : ∀l:list B.|l| = n → bind_new B E) on n |
---|
32 | : bind_new B E ≝ |
---|
33 | match n return λx.x = n → bind_new B E with |
---|
34 | [ O ⇒ λprf.f [ ] ? |
---|
35 | | S n' ⇒ λprf.νx in bnews_strong … n' (λl',prf'. f (x :: l') ?) |
---|
36 | ] (refl …). normalize // qed. |
---|
37 | |
---|
38 | interpretation "iterated new" 'unews n f = (bnews ?? n f). |
---|
39 | interpretation "iterated new strong" 'sunews n f = (bnews_strong ?? n f). |
---|
40 | |
---|
41 | notation > "νν n 'as' ident l opt('with' ident EQ) 'in' f" with precedence 47 for |
---|
42 | ${default |
---|
43 | @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) } |
---|
44 | @{ 'unews $n (λ${ident l}.$f)} |
---|
45 | }. |
---|
46 | |
---|
47 | notation > "νν n 'as' ident l : ty opt('with' ident EQ) 'in' f" with precedence 47 for |
---|
48 | ${default |
---|
49 | @{ 'sunews $n (λ${ident l}:$ty.λ${ident EQ}.$f) } |
---|
50 | @{ 'unews $n (λ${ident l}:$ty.$f)} |
---|
51 | }. |
---|
52 | |
---|
53 | notation < "hvbox(νν n \nbsp 'as' ident l \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for |
---|
54 | @{ 'sunews $n (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }. |
---|
55 | notation < "hvbox(νν n \nbsp 'as' ident l \nbsp 'in' \nbsp break f)" with precedence 47 for |
---|
56 | @{ 'unews $n (λ${ident l} : $ty.$f) }. |
---|
57 | |
---|
58 | |
---|
59 | axiom bnew_proper : ∀B,E,f,g. (∀x. f x = g x) → bnew B E f = bnew B E g. |
---|
60 | |
---|
61 | let rec bbind A B C (l : bind_new A B) (f : B → bind_new A C) on l |
---|
62 | : bind_new A C ≝ |
---|
63 | match l with |
---|
64 | [ bret x ⇒ f x |
---|
65 | | bnew n ⇒ bnew … (λx. bbind … (n x) f) |
---|
66 | ]. |
---|
67 | |
---|
68 | definition BindNew ≝ |
---|
69 | λB.MakeMonadProps |
---|
70 | (* the monad *) |
---|
71 | (bind_new B) |
---|
72 | (* return *) |
---|
73 | (λX,x.bret … x) |
---|
74 | (* bind *) |
---|
75 | (bbind B) |
---|
76 | ????. |
---|
77 | [ (* ret_bind *) |
---|
78 | // |
---|
79 | |(* bind_ret *) |
---|
80 | #X#m elim m normalize [//] |
---|
81 | #l' #Hi @bnew_proper // |
---|
82 | |(* bind_bind *) |
---|
83 | #X#Y#Z#m#f#g elim m normalize |
---|
84 | [// |
---|
85 | |(* case bnew *) |
---|
86 | #l #Hi @bnew_proper // |
---|
87 | ] |
---|
88 | | #X#Y #m #f #g #H elim m normalize [ /2/ ] #k #IH @bnew_proper #x |
---|
89 | >IH % |
---|
90 | ] |
---|
91 | qed. |
---|
92 | |
---|
93 | unification hint 0 ≔ B, X; |
---|
94 | N ≟ BindNew B, M ≟ max_def N |
---|
95 | (*--------------------------------------------*) ⊢ |
---|
96 | bind_new B X ≡ monad M X. |
---|
97 | |
---|
98 | include "utilities/state.ma". |
---|
99 | |
---|
100 | let rec bcompile U R E |
---|
101 | (fresh : state_monad U R) |
---|
102 | (b : bind_new R E) on b : state_monad U E ≝ |
---|
103 | match b with |
---|
104 | [ bret x ⇒ return x |
---|
105 | | bnew f ⇒ |
---|
106 | ! r ← fresh ; |
---|
107 | bcompile … fresh (f r) |
---|
108 | ]. |
---|
109 | |
---|
110 | theorem bcompile_bbind : |
---|
111 | ∀U,R,E,F.∀fresh : state_monad U R.∀ b : bind_new R E.∀f : E → bind_new R F. |
---|
112 | bcompile … fresh (! x ← b ; |
---|
113 | f x) ≅ |
---|
114 | ! x ← bcompile … fresh b ; |
---|
115 | bcompile … fresh (f x). |
---|
116 | #U#R#E#F#fresh#b#f |
---|
117 | elim b normalize |
---|
118 | [ // |
---|
119 | | |
---|
120 | #bf #Hi #u0 |
---|
121 | @pair_elim normalize #u #r |
---|
122 | >(Hi r) -Hi // |
---|
123 | ] |
---|
124 | qed. |
---|