source: src/utilities/bind_new.ma @ 2896

Last change on this file since 2896 was 1976, checked in by tranquil, 7 years ago
  • monads: just changed some defs, which had to be propagated in some files
  • ASM/CostProof.ma: linked cost as defined there to the one in StructuredTraces? that uses fold
  • added a library for permutations of lists (useful with fold AC ops on lists)
  • first draft of abstract_status implementation for joint languages (file joint/as_semantics.ma)
File size: 3.3 KB
Line 
1include "utilities/monad.ma".
2
3inductive 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 
10interpretation "new bind_new" 'new f = (bnew ?? f).
11
12notation > "ν 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
21notation < "hvbox(mstyle color #0000ff (ν) ident i : ty \nbsp 'in' \nbsp break p)"
22 with precedence 48 for
23  @{'new (λ${ident i} : $ty. $p) }.
24
25let 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 
31let 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 
38interpretation "iterated new" 'unews n f = (bnews ?? n f).
39interpretation "iterated new strong" 'sunews n f = (bnews_strong ?? n f).
40
41notation > "νν 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 
47notation > "νν 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 
53notation < "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) }.
55notation < "hvbox(νν n \nbsp 'as' ident l \nbsp 'in' \nbsp break f)" with precedence 47 for
56   @{ 'unews $n (λ${ident l} : $ty.$f) }.
57
58
59axiom bnew_proper : ∀B,E,f,g. (∀x. f x = g x) → bnew B E f = bnew B E g.
60
61let 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 
68definition 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]
91qed.
92
93unification hint 0 ≔ B, X;
94  N ≟ BindNew B, M ≟ max_def N
95(*--------------------------------------------*) ⊢
96  bind_new B X ≡ monad M X.
97
98include "utilities/state.ma".
99
100let 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 
110theorem 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   ]
124qed.
Note: See TracBrowser for help on using the repository browser.