1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 12:42:02 +03:00
Idris2/tests/idris2/interactive034/timeout.idr
Edwin Brady 4ef29da87e Fix expression search on already solved holes
If it's solved by unification, expression search should just print the
unified value. In fact it almost did this, but wasn't reducing the holes
so the result was being rendered incorrectly.
2021-06-23 00:59:26 +01:00

57 lines
1.9 KiB
Idris

import Data.List
import Data.List.Elem
%search_timeout 1000
||| A Place has an ID and a number of tokens
data Place : Type where
MkPlace : (i : Nat) -> (nTokens : Nat) -> Place
||| A transition has a name
data Transition : Type where
MkTransition : String -> Transition
||| An Input links a Place and a Transition...
data Input : Type where
MkInput : (from : Place) -> (to : Transition) -> Input
-- Accessor functions for proof
0 inputFrom : Input -> Place
inputFrom (MkInput p t) = p
0 inputTo : Input -> Transition
inputTo (MkInput p t) = t
data SoundInputFrom : Input -> List Place -> Type where
MkSoundInputFrom : (i : Input)
-> (ps : List Place)
-> (prf : Elem (inputFrom i) ps)
-> SoundInputFrom i ps
data SoundInputTo : Input -> List Transition -> Type where
MkSoundInputTo : (i : Input)
-> (ts : List Transition)
-> (prf : Elem (inputTo i) ts)
-> SoundInputTo i ts
data SoundInput : Input -> List Place -> List Transition -> Type where
MkSoundInput : (i : Input)
-> (ps : List Place)
-> (ts : List Transition)
-> (fromOK : SoundInputFrom i ps)
-> (toOK : SoundInputTo i ts)
-> SoundInput i ps ts
data AllInputsSound : List Input -> List Place -> List Transition -> Type where
NilInputsIsSound : AllInputsSound [] _ _
ConsIsSound : (headIsSound : SoundInput i ps ts)
-> (tailIsSound : AllInputsSound is ps ts)
-> AllInputsSound (i :: is) ps ts
-- Searching here finds the right answer immediately, but then if we don't
-- have a timeout, it takes ages to explore more non-solutions! So we cut off
-- after a second
tailIsNotSound : (contra : (AllInputsSound is ps ts -> Void))
-> AllInputsSound (i :: is) ps ts
-> Void