Changeset 1976 for src/common/IOMonad.ma


Ignore:
Timestamp:
May 21, 2012, 7:04:21 PM (8 years ago)
Author:
tranquil
Message:
  • 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IOMonad.ma

    r1949 r1976  
    165165
    166166definition IOPred ≝ λO,I,Perr.
    167   mk_MonadPred (IOMonad O I)
    168     (λA.pred_io O I A Perr)
     167  mk_InjMonadPred (IOMonad O I)
     168    (mk_MonadPred ? (λA.pred_io O I A Perr) ???)
    169169    (λA,P,a_sig.match a_sig with [ mk_Sig a prf ⇒ pred_io_inject O I A Perr P a prf ])
    170     ????.
    171 [//
    172 |#X #Y #relin #relout #m elim m
     170    ?. //
     171[ #X #P #Q #H #m elim m
     172  [#o #f #IH #H #i @IH @H
     173  | #v @H
     174  | #e //
     175  ]
     176| #X #Y #relin #relout #m elim m
    173177  [ #o #f #IH whd in ⊢ (%→?); #H
    174178    #f #G whd #i
     
    177181  | #e //
    178182  ]
    179 | #X #P #Q #H #m elim m
    180   [#o #f #IH #H #i @IH @H
    181   | #v @H
    182   | #e //
    183   ]
    184 |#X #P * #m elim m
     183| #X #P * #m elim m
    185184  [ #o #f #IH whd in ⊢ (%→?); #H
    186185    change with (Interact ?????) in ⊢ (???%);
     
    200199coercion err_to_io : ∀O,I,A.∀c:res A.IO O I A ≝ err_to_io on _c:res ? to IO ???.
    201200
     201(*
    202202lemma res_io_pred : ∀O,I,A,Perr,P.∀m : res A.pred_res … Perr P m → pred_io O I ? Perr P m.
    203203#O #I #A #Perr #P * /2/ qed.
     
    205205lemma io_res_pred : ∀O,I,A,Perr,P.∀m : res A.pred_io O I ? Perr P m → pred_res ? Perr P m.
    206206#O #I #A #Perr #P * /2/ qed.
    207 
     207*)
    208208definition err_to_io_sig : ∀O,I,T.∀P:T → Prop. res (Sig T P) → IO O I (Sig T P) ≝
    209209λO,I,T,P,v. match v with [ OK v' ⇒ Value O I (Sig T P) v' | Error m ⇒ Wrong O I (Sig T P) m ].
Note: See TracChangeset for help on using the changeset viewer.