Advertisement
Guest User

Untitled

a guest
Dec 8th, 2016
66
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 0.92 KB | None | 0 0
  1. module Main
  2.  
  3. data DoorState = DoorClosed | DoorOpen
  4.  
  5. data DoorResult = OK | Jammed
  6.  
  7. data DoorCmd : (ty : Type) -> DoorState -> (ty -> DoorState) -> Type where
  8. Open : DoorCmd DoorResult DoorClosed (\res => case res of
  9. OK => DoorOpen
  10. Jammed => DoorClosed)
  11. Close : DoorCmd () DoorOpen (const DoorClosed)
  12. RingBell : DoorCmd () DoorClosed (const DoorClosed)
  13. Display : String -> DoorCmd () state (const state)
  14.  
  15. Pure : (res : ty) -> DoorCmd ty (state_fn res) state_fn
  16. (>>=) : DoorCmd a state1 state2_fn ->
  17. ((res : a) -> DoorCmd b (state2_fn res) state3_fn) ->
  18. DoorCmd b state1 state3_fn
  19.  
  20. doorProg : DoorCmd () DoorClosed (const DoorClosed)
  21. doorProg = do RingBell
  22. OK <- Open | Jammed => Display "Door Jammed"
  23. Display "Glad to be of service"
  24. Close
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement