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 «?, ?» = ?
File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.