mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-26 13:11:30 +03:00
a972778eab
They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
83 lines
2.0 KiB
Idris
83 lines
2.0 KiB
Idris
module Door
|
|
|
|
public export
|
|
data Usage = Once | Many
|
|
|
|
public export
|
|
data Lin : (Type -> Type) -> Usage -> Type -> Type where
|
|
Pure : (1 x : a) -> Lin m u a
|
|
Lift : (1 x : m a) -> Lin m Many a
|
|
BindOnce : (1 act : Lin m Once a) ->
|
|
(1 k : (1 x : a) -> Lin m t b) -> Lin m t b
|
|
BindMany : (1 act : Lin m Many a) ->
|
|
(1 k : (x : a) -> Lin m t b) -> Lin m t b
|
|
|
|
public export
|
|
data Unrestricted : Type -> Type where
|
|
MkUn : (x : a) -> Unrestricted a
|
|
|
|
export
|
|
pure : (1 x : a) -> Lin m u a
|
|
pure = Pure
|
|
|
|
export
|
|
lift : (1 x : m a) -> Lin m Many a
|
|
lift = Lift
|
|
|
|
public export
|
|
contType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type
|
|
contType m Once q a b = (1 x : a) -> Lin m q b
|
|
contType m Many q a b = (x : a) -> Lin m q b
|
|
|
|
public export
|
|
(>>=) : {p : _}
|
|
-> (1 f : Lin m p a)
|
|
-> (1 k : contType m p q a b)
|
|
-> Lin m q b
|
|
(>>=) {p=Once} = BindOnce
|
|
(>>=) {p=Many} = BindMany
|
|
|
|
export
|
|
run : Monad m => Lin m u t -> m t
|
|
run (Pure x) = pure x
|
|
run (Lift p) = p
|
|
run (BindOnce act k)
|
|
= do act' <- run act
|
|
run (k act')
|
|
run (BindMany act k)
|
|
= do act' <- run act
|
|
run (k act')
|
|
|
|
public export
|
|
One : (Type -> Type) -> Type -> Type
|
|
One m = Lin m Once
|
|
|
|
public export
|
|
Any : (Type -> Type) -> Type -> Type
|
|
Any m = Lin m Many
|
|
|
|
infix 2 @@
|
|
|
|
public export
|
|
data Res : (a : Type) -> (a -> Type) -> Type where
|
|
(@@) : (val : a) -> (1 resource : r val) -> Res a r
|
|
|
|
data DoorState = Closed | Open
|
|
|
|
-- changes start here
|
|
|
|
openWhen : Bool -> DoorState
|
|
openWhen ok = if ok then Open else Closed
|
|
|
|
data Door : DoorState -> Type where
|
|
MkDoor : (isOpen : Bool) -> Door (if isOpen then Open else Closed)
|
|
|
|
-- Testing that 'if' works okay in an interface
|
|
interface Doored (m : Type -> Type) where
|
|
newDoor : One m (Door Closed)
|
|
knock : (1 d : Door t) -> One m (Door t)
|
|
openDoor : (1 d : Door Closed)
|
|
-> One m (Res Bool (\ok => Door (if ok then Open else Closed)))
|
|
closeDoor : (1 d : Door Open) -> One m (Door Closed)
|
|
deleteDoor : (1 d : Door Closed) -> Any m ()
|