Changeset 1647 for src/common


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
Location:
src/common
Files:
2 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.
  • src/common/IOMonad.ma

    r1640 r1647  
    2424
    2525definition IOMonad ≝ λO,I.
    26   MakeMonad (mk_MonadDefinition
     26  MakeMonadProps
    2727  (* the monad *)
    2828  (IO O I)
     
    3131  (* bind *)
    3232  (bindIO O I)
    33   ???). / by /
    34 [(* bind_bind *)
     33  ???. / by /
     34[(* bind_ret *)
     35 #X#m elim m normalize // #o#f#Hi @interact_proper //
     36|(* bind_bind *)
    3537 #X#Y#Z#m#f#g elim m normalize [2,3://]
    3638 (* Interact *)
    3739  #o#f #Hi @interact_proper //
    38 |(* bind_ret *)
    39  #X#m elim m normalize // #o#f#Hi @interact_proper //
    4040]
    4141qed.
     
    4646
    4747unification hint 0 ≔ O, I, T;
    48   N ≟ IOMonad O I, M ≟ m_def N
     48  N ≟ IOMonad O I, M ≟ max_def N, M' ≟ m_def M
    4949(*******************************************) ⊢
    50   IO O I T ≡ monad M T
     50  IO O I T ≡ monad M' T
    5151.
    5252
     
    177177  P_io O I ? P (bindIO O I A B e f).
    178178#I #O #A #B #P' #P #e elim e;
    179 [ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2/;
     179[ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2 by /;
    180180| #v #f #He #H @H @He
    181181| //;
     
    187187  P_io O I ? P (bindIO2 O I A B C e f).
    188188#I #O #A #B #C #P' #P #e elim e;
    189 [ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2/;
     189[ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2 by /;
    190190| #v cases v; #v1 #v2 #f #He #H @H @He
    191191| //;
     
    213213#I #O #A #B #C #P #e #Q #R cases e; #e' cases e'; normalize;
    214214[ *;
    215 | #e'' cases e''; #a #b #Pab #H normalize; /2/;
     215| #e'' cases e''; #a #b #Pab #H normalize; /2 by _/;
    216216] qed.
    217217*)
Note: See TracChangeset for help on using the changeset viewer.