[Agda] heres a nice example of copattern matching

[Carter Schonwald]

Hey all,
I wrote a toy model of the CPU MESI cacheline protocol in agda using
copatterns/coinduction, it turned out super nice! figured y'all  would
enjoy it

i've included it inline below, and a github gist here
https://gist.github.com/cartazio/5b1d3d8dd12b9279866d

module MesiModel where

open import Data.Vec
open import Data.Fin
open import Data.Nat
open import Data.Product


data MesiState : Set where
  Invalid   : MesiState
  Modified   : MesiState
  Exclusive : MesiState
  Shared    : MesiState
open MesiState



record MesiCommandI  : Set where
      coinductive
      field
        LocalReadI   : MesiState  ×  MesiCommandI
        LocalWriteI  :  MesiState  ×  MesiCommandI
        RemoteReadI  :  MesiState  ×  MesiCommandI
        RemoteWriteI :  MesiState  ×  MesiCommandI


open MesiCommandI

denoteMCI : MesiState -> MesiCommandI
LocalReadI (denoteMCI Invalid)  = Exclusive  , denoteMCI Exclusive
LocalReadI (denoteMCI Modified)  = Modified  , denoteMCI Modified
LocalReadI (denoteMCI Exclusive) = Exclusive , denoteMCI Exclusive
LocalReadI (denoteMCI Shared) = Shared , denoteMCI Shared  -- MesiState  ×
 MesiCommandI

LocalWriteI (denoteMCI Invalid)  = Modified , denoteMCI Modified
LocalWriteI (denoteMCI Modified) = Modified , denoteMCI Modified
LocalWriteI (denoteMCI Exclusive)= Modified , denoteMCI Modified
LocalWriteI (denoteMCI Shared) =   Modified , denoteMCI Modified   -- :
 MesiState  ×  MesiCommandI

RemoteReadI (denoteMCI Invalid)  = Invalid , denoteMCI Invalid -- check
RemoteReadI (denoteMCI Modified) = Invalid , denoteMCI Invalid
RemoteReadI (denoteMCI Exclusive) = Shared , denoteMCI Shared
RemoteReadI (denoteMCI Shared)    = Shared , denoteMCI Shared  -- :
 MesiState  ×  MesiCommandI

RemoteWriteI (denoteMCI Invalid) =  Invalid , denoteMCI Invalid -- check
RemoteWriteI (denoteMCI Modified) = Invalid , denoteMCI Invalid
RemoteWriteI (denoteMCI Exclusive)= Invalid , denoteMCI Invalid
RemoteWriteI (denoteMCI Shared) =   Invalid , denoteMCI Invalid -- :
 MesiState  ×  MesiCommandI
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160313/3a8abc76/attachment.html