mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-10 15:16:54 +03:00
e1c79ef07d
Instead of guessing the error for the thing that's closest to working, better to say that no alternative works. (This makes the bizarre 'score' heuristic for error messages obsolete, so that'll be removed soon too.)
38 lines
884 B
Idris
38 lines
884 B
Idris
import IOu
|
|
|
|
import Data.Vect
|
|
|
|
data Result : (a : AnyType) -> (a -> AnyType) -> AnyType where
|
|
Res : {k : a -> AnyType} -> (val : a) -> (h : k val) -> Result a k
|
|
|
|
|
|
|
|
|
|
|
|
------
|
|
data DoorState = OPEN | CLOSED
|
|
|
|
data DoorH : DoorState -> UniqueType where
|
|
MkDH : DoorH s
|
|
|
|
data DoorCmd : AnyType -> AnyType where
|
|
Open : DoorH CLOSED -> DoorCmd (DoorH OPEN)
|
|
Knock : DoorH CLOSED -> DoorCmd (DoorH CLOSED)
|
|
Close : DoorH OPEN -> DoorCmd (DoorH CLOSED)
|
|
|
|
data DoorLang : AnyType -> AnyType where
|
|
Return : {a : AnyType} -> a -> DoorLang a
|
|
Action : DoorCmd a -> DoorLang a
|
|
(>>=) : DoorLang a -> (a -> DoorLang b) -> DoorLang b
|
|
|
|
implicit
|
|
action : DoorCmd a -> DoorLang a
|
|
action = Action
|
|
|
|
testProg : DoorH CLOSED -> DoorLang ()
|
|
testProg h = with Main, Show do -- h <- Knock h
|
|
h <- Open h
|
|
-- h <- Close h
|
|
Return ()
|
|
|