source: src/utilities/bindLists.ma @ 1651

Last change on this file since 1651 was 1647, checked in by tranquil, 8 years ago
  • corrected some notation problems
  • adapted Cligth with slight modifications to new monad framework
File size: 6.9 KB
Line 
1include "utilities/monad.ma".
2include "basics/lists/list.ma".
3
4inductive bind_list
5  (B : Type[0])
6  (T : Type[0])
7  (E : Type[0])
8  : Type[0] ≝
9  | bnil : bind_list B T E
10  | bcons : E → bind_list B T E → bind_list B T E
11  | bnew : T → (B → bind_list B T E) → bind_list B T E.
12 
13interpretation "new blist" 'new t f = (bnew ??? t f).
14interpretation "cons blist" 'cons hd tl = (bcons ??? hd tl).
15interpretation "nil blist" 'nil = (bnil ???).
16
17notation > "ν list1 ident x sep , opt('of' t) 'in' f"
18  with precedence 48 for
19  ${ default
20    @{ ${ fold right @{$f} rec acc @{'new $t (λ${ident x}.$acc)} } }
21    @{ ${ fold right @{$f} rec acc @{'new 'it (λ${ident x}.$acc)} } }
22  }.
23
24notation < "hvbox(ν ident i \nbsp 'of' \nbsp t \nbsp 'in' \nbsp break p)"
25 with precedence 48 for
26  @{'new $t (λ${ident i} : $ty. $p) }.
27
28interpretation "unit it" 'it = it.
29
30notation < "hvbox(ν ident i \nbsp 'in' \nbsp break p)"
31 with precedence 48 for
32    @{'new 'it (λ${ident i} : $ty. $p) }.
33   
34let rec bnews B T E (tys : list T) (f : list B → bind_list B T E) on tys : bind_list B T E ≝
35  match tys with
36  [ nil ⇒ f [ ]
37  | cons ty tys ⇒ νx of ty in bnews … tys (λl. f (x :: l))
38  ].
39 
40let rec bnews_strong B T E (tys : list T) (f : ∀l : list B.|l| = |tys| → bind_list B T E) on tys : bind_list B T E ≝
41  match tys return λx.x = tys → bind_list B T E with
42  [ nil ⇒ λprf.f [ ] ?
43  | cons ty tys' ⇒ λprf.νx of ty in bnews_strong … tys' (λl',prf'. f (x :: l') ?)
44  ] (refl …). destruct normalize // qed.
45 
46let rec bnews_n B E n (f : list B → bind_list B unit E) on n : bind_list B unit E ≝
47  match n with
48  [ O ⇒ f [ ]
49  | S n ⇒ νx in bnews_n … n (λl. f (x :: l))
50  ].
51 
52let rec bnews_n_strong B E n (f : ∀l:list B.|l| = n → bind_list B unit E) on n : bind_list B unit E ≝
53  match n return λx.x = n → bind_list B unit E with
54  [ O ⇒ λprf.f [ ] ?
55  | S n' ⇒ λprf.νx in bnews_n_strong … n' (λl',prf'. f (x :: l') ?)
56  ] (refl …). normalize // qed.
57 
58interpretation "iterated typed new" 'tnews ts f = (bnews ??? ts f).
59interpretation "iterated untyped new" 'unews n f = (bnews_n ?? n f).
60interpretation "iterated typed new strong" 'stnews ts f = (bnews_strong ??? ts f).
61interpretation "iterated untyped new strong" 'sunews n f = (bnews_n_strong ?? n f).
62
63notation > "νν ident l 'of' ts opt('with' ident EQ) 'in' f" with precedence 47 for
64 ${default
65   @{ 'stnews $ts (λ${ident l}.λ${ident EQ}.$f) }
66   @{ 'tnews $ts (λ${ident l}.$f)}
67 }.
68 
69notation > "νν ident l : ty 'of' ts opt('with' ident EQ) 'in' f" with precedence 47 for
70 ${default
71   @{ 'stnews $ts (λ${ident l}:$ty.λ${ident EQ}.$f) }
72   @{ 'tnews $ts (λ${ident l}:$ty.$f)}
73 }.
74 
75notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
76   @{ 'stnews $ts (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
77notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'in'  break f)" with precedence 47 for
78   @{ 'tnews $ts (λ${ident l} : $ty.$f) }.
79
80notation > "νν ident l ^ n opt('with' ident EQ) 'in' f" with precedence 47 for
81 ${default
82   @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) }
83   @{ 'unews $n (λ${ident l}.$f)}
84 }.
85 
86notation > "νν ident l : ty ^ n opt('with' ident EQ) 'in' f" with precedence 47 for
87 ${default
88   @{ 'sunews $n (λ${ident l}:$ty.λ${ident EQ}.$f) }
89   @{ 'unews $n (λ${ident l}:$ty.$f)}
90 }.
91 
92notation < "hvbox(νν \nbsp ident l : ty ^ n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
93   @{ 'sunews $n (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
94notation < "hvbox(νν_ n \nbsp ident l : ty ^ n \nbsp 'in' \nbsp break f)" with precedence 47 for
95   @{ 'unews $n (λ${ident l} : $ty.$f) }.
96
97
98axiom bnew_proper : ∀B,T,E. bnew B T E ⊨ eq ? ++> (eq ? ++> eq ?) ++> eq ?.
99(* the following is equivalent to the above *)
100theorem bnew_proper' : ∀X,Y,Z.Y (* non-empty *) →
101  ∀f,g : X → bind_list X Y Z.  (∀x. f x = g x) → f = g.
102#X#Y#Z#y#f#g#eqf
103cut ('new y f = 'new y g) /2 by bnew_proper/
104#eq destruct //
105qed.
106
107definition blist_of_list : ∀B,T,E. list E →
108  bind_list B T E ≝
109  λB,T,E,l.
110  let f ≝ λe.λbl. e :: bl in
111  foldr … f [] l.
112 
113 
114coercion blist_from_list :
115  ∀B,T,E. ∀l:list E. bind_list B T E ≝ blist_of_list on _l : list ? to bind_list ???.
116
117let rec bappend A B C (l1 : bind_list A B C) l2 on l1 : bind_list A B C ≝
118match l1 with
119[ bnil ⇒ l2
120| bcons x l1' ⇒ x :: (bappend … l1' l2)
121| bnew t l1' ⇒ νx of t in bappend … (l1' x) l2
122].
123
124interpretation "append blist" 'append l1 l2 = (bappend ??? l1 l2).
125
126let rec bbind A B C D (l : bind_list A B C) (f : C → bind_list A B D) on l
127  : bind_list A B D ≝
128  match l with
129  [ bnil ⇒ bnil …
130  | bcons x l1' ⇒ bappend … (f x) (bbind … l1' f)
131  | bnew t l1' ⇒ bnew … t (λx. bbind … (l1' x) f)
132  ].
133 
134interpretation "bind_list bind" 'm_bind m f = (bbind ? ? ? ? m f).
135
136include "utilities/proper.ma".
137
138lemma bappend_assoc : ∀A,B,C.∀l1,l2,l3:bind_list A B C.
139  ((l1@l2)@l3) = (l1 @ l2 @ l3).
140#A#B#C#l1 elim l1 normalize
141[
142(* case bnil *)
143  #l2#l3 //
144| #x#l'#Hi#l2#l3 >Hi //
145| #t#l'#Hi#l2#l3 @bnew_proper //
146qed.
147
148lemma bbind_bappend : ∀A,B,C,D.∀l1,l2:bind_list A B C.∀f:C→bind_list A B D.
149  ((l1 @ l2) »= f) = ((l1 »= f) @ (l2 »= f)).
150#A#B#C#D#l1 elim l1 normalize /2 by bnew_proper/ qed.
151
152lemma bappend_bnil : ∀A,B,C.∀l : bind_list A B C.( l@[ ]) = l.
153#A#B#C#l elim l normalize /2 by bnew_proper/ qed.
154 
155definition BindList ≝
156  λB,T.MakeMonadProps
157  (* the monad *)
158  (λX.bind_list B T X)
159  (* return *)
160  (λE,x.[x])
161  (* bind *)
162  (bbind B T)
163  ???.
164[(* ret_bind *)
165  #X#Y#x#f normalize @bappend_bnil
166|(* bind_ret *)
167 #X#m elim m normalize /2 by /
168 #t #l' #Hi @bnew_proper // normalize #s#t#eq destruct @Hi
169|(* bind_bind *)
170 #X#Y#Z#m#f#g elim m normalize
171 [//
172 |(* case bcons *)
173  #x #l1' #Hi <Hi @bbind_bappend
174 |(* case bnew *)
175  #t #l #Hi @bnew_proper //
176  #x#y #x_eq_y destruct(x_eq_y) @Hi
177 ]
178]
179qed.
180
181unification hint 0 ≔ B, T, X;
182  N ≟ BindList B T, M ≟ max_def N, O ≟ m_def M
183(*--------------------------------------------*) ⊢
184  bind_list B T X ≡ monad O X.
185
186include "utilities/state.ma".
187
188let rec bcompile R T E U
189  (fresh : T → state_monad U R)
190  (blist : bind_list R T E) on blist : state_monad U (list E) ≝
191  match blist with
192  [ bnil ⇒ return [ ]
193  | bcons x l ⇒
194    ! res ← bcompile … fresh l ;
195    return (x :: res)
196  | bnew t f ⇒
197    ! r ← fresh t ;
198    bcompile … fresh (f r)
199  ].
200 
201theorem bcompile_append :
202  ∀E, R, T, U, fresh, bl1, bl2.
203  (bcompile E R T U fresh (bl1 @ bl2)) ≅
204  (
205  ! l1 ← bcompile … fresh bl1 ;
206  ! l2 ← bcompile … fresh bl2 ;
207  return (l1 @ l2)
208  ).
209  #E#R#T#U#fresh#bl1#bl2
210  elim bl1 normalize
211   [
212     #u @pair_elim //
213   |
214    #x#bl1' #Hi #u0 >Hi -Hi
215    elim (bcompile E R T U fresh bl1' u0) #u1 #l1
216    normalize
217    elim (bcompile E R T U fresh bl2 u1) #u2 #l2
218    normalize //
219   |
220    #t #blf #Hi #u0
221    @pair_elim normalize #u #r
222    >(Hi r) -Hi //
223qed.
Note: See TracBrowser for help on using the repository browser.