Changeset 1647 for src/common/Errors.ma


Ignore:
Timestamp:
Jan 17, 2012, 1:13:08 PM (8 years ago)
Author:
tranquil
Message:
  • corrected some notation problems
  • adapted Cligth with slight modifications to new monad framework
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r1640 r1647  
    4949(*Implicit Arguments Error [A].*)
    5050
    51 definition Res : Monad ≝ MakeMonad (mk_MonadDefinition
     51definition Res ≝ MakeMonadProps
    5252  (* the monad *)
    5353  res
     
    5656  (* bind *)
    5757  (λX,Y,m,f. match m with [ OK x ⇒ f x | Error msg ⇒ Error ? msg])
    58   ???).
     58  ???.
    5959//
    60 [(* bind_bind *)
     60[(* bind_ret *)
     61 #X*normalize //
     62|(* bind_bind *)
    6163 #X#Y#Z*normalize //
    62 |(* bind_ret *)
    63  #X*normalize //
    6464]
    6565qed.
     
    6767include "hints_declaration.ma".
    6868unification hint 0 ≔ X;
    69 M ≟ m_def Res
     69N ≟ max_def Res, M ≟ m_def N
    7070(*---------------*) ⊢
    7171res X ≡ monad M X
     
    9696interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).*)
    9797
    98 lemma res_bind_inversion:
     98lemma bind_inversion:
    9999  ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B.
    100100  (f »= g = return y) →
     
    250250  ] (refl ? f).
    251251
    252 notation > "vbox('!' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
     252notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 48 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
    253253
    254254definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C.
     
    258258  ] (refl ? f).
    259259
    260 notation > "vbox('!' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 40 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.
     260notation > "vbox('do' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 48 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.
    261261
    262262definition res_to_opt : ∀A:Type[0]. res A → option A ≝
    263263 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
    264264
     265(* aliases for backward compatibility *)
     266definition bind ≝ m_bind Res.
     267definition bind2 ≝ m_bind2 Res.
     268definition bind3 ≝ m_bind3 Res.
     269definition mmap ≝ m_mmap Res.
     270definition mmap_sigma ≝ m_mmap_sigma Res.
Note: See TracChangeset for help on using the changeset viewer.