Changeset 2453


Ignore:
Timestamp:
Nov 12, 2012, 4:30:03 PM (7 years ago)
Author:
tranquil
Message:

come changes in monad notation to

  • avoid pretty printed monsters
  • avoid "»=" notation for bind that breaks stuff like «?, ?» = ?
Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r2439 r2453  
    8989lemma bind_inversion:
    9090  ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B.
    91   (f »= g = return y) →
     91  (! x ← f ; g x = return y) →
    9292  ∃x. (f = return x) ∧ (g x = return y).
    9393#A #B #f #g #y cases f normalize
  • src/common/IOMonad.ma

    r2444 r2453  
    369369lemma bind_res_value : ∀O,I,A,B,e,f,v. ∀P:B → Type[0].
    370370  (∀a. e = OK A a → f a = OK B v → P v) →
    371   (match e »= f with [ OK v ⇒ Value … v | Error m ⇒ Wrong … m ] = Value O I B v → P v).
     371  (match m_bind … e f with [ OK v ⇒ Value … v | Error m ⇒ Wrong … m ] = Value O I B v → P v).
    372372#O #I #A #B *
    373373[ #a #f #v #P #H #E @H [ @a | @refl | normalize in E; cases (f a) in E ⊢ %;
     
    403403lemma bindIO_inversion: ∀O,I.
    404404  ∀A,B: Type[0]. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
    405   (f »= g = return y) →
     405  (m_bind … f g = return y) →
    406406  ∃x. (f = return x) ∧ (g x = return y).
    407407#O #I #A #B #f #g #y cases f normalize
  • src/common/PositiveMap.ma

    r2439 r2453  
    425425match b with
    426426[ pm_leaf ⇒ pm_leaf ?
    427 | pm_node a l r ⇒ pm_node ? (a »= f)
     427| pm_node a l r ⇒ pm_node ? (!x ← a ; f x)
    428428    (map_opt ?? f l)
    429429    (map_opt ?? f r)
  • src/utilities/monad.ma

    r2179 r2453  
    2828}.
    2929
    30 notation "m »= f" with precedence 49
    31   for @{'m_bind $m $f }.
     30(* notation "m »= f" with precedence 49
     31  for @{'m_bind $m $f }. *)
    3232
    3333notation > "!_ e; e'"
     
    3737notation > "! ident v : ty ← e; e'"
    3838  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
    39 notation < "vbox(! \nbsp ident v ← e ; break e')"
    40   with precedence 48 for @{'m_bind ${e} (λ${ident v}.${e'})}.
    4139notation > "! ident v ← e : ty ; e'"
    4240  with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}.
    43 notation < "vbox(! \nbsp ident v : ty \nbsp ←  \nbsp e ; break e')"
     41notation < "vbox(! \nbsp hvbox( ident v : ty \nbsp break ← \nbsp e ;) break e')"
    4442  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
    4543notation > "! ident v : ty ← e : ty' ; e'"
     
    5149notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'"
    5250  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
    53 notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e ; break e')"
    54   with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
    55 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉  \nbsp ←  \nbsp e ; break e')"
     51notation < "vbox(! \nbsp hvbox( 〈ident v1 : ty1, break ident v2 : ty2〉 \nbsp break ← \nbsp e ; ) break e')"
    5652  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
    5753notation > "! 〈ident v1, ident v2, ident v3〉 ← e ; e'"
     
    6157notation > "! 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'"
    6258  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
    63 notation < "vbox(! \nbsp 〈ident v1, ident v2, ident v3〉 \nbsp ← \nbsp e ; break e')"
    64   with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
    65 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 \nbsp ← e \nbsp ; break e')"
     59notation < "vbox(! \nbsp hvbox( 〈ident v1 : ty1, break ident v2 : ty2, break ident v3 : ty3〉 \nbsp break ← e \nbsp ; ) break e')"
    6660  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
    6761
     
    7165  @{'m_bind ${e} (λ${fresh p_sig}.
    7266    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
    73 notation < "vbox(! \nbsp «ident v1, ident v2» \nbsp ← \nbsp e ; break e')"
     67notation < "vbox(! \nbsp hvbox( «ident v1, break ident v2» \nbsp break ← \nbsp e ; ) break e')"
    7468  with precedence 48 for
    7569  @{'m_bind ${e} (λ${fresh p_sig}.
     
    7973  with precedence 48 for
    8074  @{'m_sigbind2 ${e} (λ${ident v1},${ident v2},${ident H}. ${e'})}.
    81 notation < "vbox(! \nbsp «ident v1, ident v2, ident H» \nbsp ← \nbsp e ; e')"
     75notation < "vbox(! \nbsp hvbox( «ident v1, break ident v2, break ident H» \nbsp break ← \nbsp e ; ) e')"
    8276  with precedence 48 for
    8377  @{'m_sigbind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.
     
    144138  ; sm_eq_sym : ∀X.symmetric ? (sm_eq X)
    145139  ; sm_return_proper : ∀X,x.sm_eq X (return x) (return x)
    146   ; sm_bind_proper : ∀X,Y,x,y,f,g.sm_eq X x y → (∀x.sm_eq Y (f x) (g x)) → sm_eq Y (x »= f) (y »= g)
     140  ; sm_bind_proper : ∀X,Y,x,y,f,g.sm_eq X x y → (∀x.sm_eq Y (f x) (g x)) → sm_eq Y (m_bind … x f) (m_bind … y g)
    147141  ; sm_return_bind : ∀X,Y.∀x : X.∀f : X → smax_def Y.
    148142      sm_eq Y (! y ← return x ; f y) (f x)
Note: See TracChangeset for help on using the changeset viewer.