Advertisement
Guest User

Untitled

a guest
Dec 8th, 2016
73
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 1.64 KB | None | 0 0
  1. module Main
  2.  
  3. data DoorState = DoorClosed | DoorOpen
  4.  
  5. data DoorResult = OK | Jammed
  6.  
  7. doorResult : DoorResult -> DoorState
  8. doorResult = \res => case res of
  9. OK => DoorOpen
  10. Jammed => DoorClosed
  11.  
  12. data DoorCmd : (ty : Type) -> DoorState -> (ty -> DoorState) -> Type where
  13. Open : DoorCmd DoorResult DoorClosed doorResult
  14. Close : DoorCmd () DoorOpen (const DoorClosed)
  15. RingBell : DoorCmd () DoorClosed (const DoorClosed)
  16. Display : String -> DoorCmd () state (const state)
  17.  
  18. Pure : (res : ty) -> DoorCmd ty (state_fn res) state_fn
  19. (>>=) : DoorCmd a state1 state2_fn ->
  20. ((res : a) -> DoorCmd b (state2_fn res) state3_fn) ->
  21. DoorCmd b state1 state3_fn
  22.  
  23. doorProg : DoorCmd () DoorClosed (const DoorClosed)
  24. doorProg = do RingBell
  25. OK <- Open | Jammed => Display "Door Jammed"
  26. Display "Glad to be of service"
  27. Close
  28.  
  29. {-
  30. - + Errors (1)
  31. `-- Chap14.idr line 27 col 14:
  32. When checking right hand side of Main.case block in doorProg at Chap14.idr:25:21 with expected type
  33. DoorCmd () (state2_fn OK) (\value => DoorClosed)
  34.  
  35. When checking an application of constructor Main.>>=:
  36. Type mismatch between
  37. DoorCmd () DoorOpen (const DoorClosed) (Type of Close)
  38. and
  39. DoorCmd ()
  40. (const (state2_fn OK) _)
  41. (\value => DoorClosed) (Expected type)
  42.  
  43. Specifically:
  44. Type mismatch between
  45. DoorOpen
  46. and
  47. state2_fn OK
  48. -}
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement