{-# LANGUAGE PatternGuards #-}
module Idris.Prover (prover, showProof, showRunElab) where
import Prelude (Bool(..), Either(..), Eq(..), Maybe(..), Show(..), String,
concatMap, elem, error, foldl, foldr, fst, id, init, length,
lines, map, not, null, repeat, reverse, tail, zip, ($), (&&),
(++), (.), (||))
import Idris.AbsSyntax
import Idris.Completion
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.DataOpts
import Idris.Delaborate
import Idris.Docs (getDocs, pprintConstDocs, pprintDocs)
import Idris.Elab.Term
import Idris.Elab.Utils
import Idris.Elab.Value
import Idris.ElabDecls
import Idris.Error
import qualified Idris.IdeMode as IdeMode
import Idris.Options
import Idris.Output
import Idris.Parser hiding (params)
import Idris.TypeSearch (searchByType)
import Util.Pretty
import Control.DeepSeq
import Control.Monad.State.Strict
import System.Console.Haskeline
import System.Console.Haskeline.History
import System.IO (Handle, hPutStrLn, stdin, stdout)
prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()
prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()
prover info :: ElabInfo
info mode :: Bool
mode lit :: Bool
lit x :: Name
x =
do Context
ctxt <- Idris Context
getContext
IState
i <- Idris IState
getIState
case Name -> Context -> [Type]
lookupTy Name
x Context
ctxt of
[t :: Type
t] -> if Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Name
x (((Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name)
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name
forall a b. (a, b) -> a
fst (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
i))
then Bool
-> ElabInfo
-> Ctxt OptInfo
-> Context
-> Bool
-> Name
-> Type
-> Idris ()
prove Bool
mode ElabInfo
info (IState -> Ctxt OptInfo
idris_optimisation IState
i) Context
ctxt Bool
lit Name
x Type
t
else String -> Idris ()
forall a. String -> Idris a
ifail (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is not a hole"
_ -> String -> Idris ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "No such hole"
showProof :: Bool -> Name -> [String] -> String
showProof :: Bool -> Name -> [String] -> String
showProof lit :: Bool
lit n :: Name
n ps :: [String]
ps
= String
bird String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = proof" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
break String -> String -> String
forall a. [a] -> [a] -> [a]
++
String -> [String] -> String
showSep String
break ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: String
x -> " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x) [String]
ps) String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
break String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
where bird :: String
bird = if Bool
lit then "> " else ""
break :: String
break = "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bird
showRunElab :: Bool -> Name -> [String] -> String
showRunElab :: Bool -> Name -> [String] -> String
showRunElab lit :: Bool
lit n :: Name
n ps :: [String]
ps = String -> String
birdify (SimpleDoc Any -> String -> String
forall a. SimpleDoc a -> String -> String
displayS (Float -> Int -> Doc Any -> SimpleDoc Any
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty 1.0 80 Doc Any
forall a. Doc a
doc) "")
where doc :: Doc a
doc = String -> Doc a
forall a. String -> Doc a
text (Name -> String
forall a. Show a => a -> String
show Name
n) Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc a
forall a. String -> Doc a
text "=" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc a
forall a. String -> Doc a
text "%runElab" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+>
Doc a -> Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a -> Doc a
enclose Doc a
forall a. Doc a
lparen Doc a
forall a. Doc a
rparen
(String -> Doc a
forall a. String -> Doc a
text "do" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> (Doc a -> Doc a
forall a. Doc a -> Doc a
align (Doc a -> Doc a) -> Doc a -> Doc a
forall a b. (a -> b) -> a -> b
$ [Doc a] -> Doc a
forall a. [Doc a] -> Doc a
vsep ((String -> Doc a) -> [String] -> [Doc a]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc a
forall a. String -> Doc a
text [String]
ps)))
birdify :: String -> String
birdify = if Bool
lit
then (String -> String) -> [String] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ("> " String -> String -> String
forall a. [a] -> [a] -> [a]
++) ([String] -> String) -> (String -> [String]) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines
else String -> String
forall a. a -> a
id
proverSettings :: ElabState EState -> Settings Idris
proverSettings :: ElabState EState -> Settings Idris
proverSettings e :: ElabState EState
e = CompletionFunc Idris -> Settings Idris -> Settings Idris
forall (m :: * -> *). CompletionFunc m -> Settings m -> Settings m
setComplete ([String] -> CompletionFunc Idris
proverCompletion (ElabState EState -> [String]
assumptionNames ElabState EState
e)) Settings Idris
forall (m :: * -> *). MonadIO m => Settings m
defaultSettings
assumptionNames :: ElabState EState -> [String]
assumptionNames :: ElabState EState -> [String]
assumptionNames e :: ElabState EState
e
= case ProofState -> TC Env
envAtFocus (ElabState EState -> ProofState
forall aux. ElabState aux -> ProofState
proof ElabState EState
e) of
OK env :: Env
env -> Env -> [String]
forall b c. [(Name, b, c)] -> [String]
names Env
env
where names :: [(Name, b, c)] -> [String]
names [] = []
names ((MN _ _, _, _) : bs :: [(Name, b, c)]
bs) = [(Name, b, c)] -> [String]
names [(Name, b, c)]
bs
names ((n :: Name
n, _, _) : bs :: [(Name, b, c)]
bs) = Name -> String
forall a. Show a => a -> String
show Name
n String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [(Name, b, c)] -> [String]
names [(Name, b, c)]
bs
prove :: Bool -> ElabInfo -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()
prove :: Bool
-> ElabInfo
-> Ctxt OptInfo
-> Context
-> Bool
-> Name
-> Type
-> Idris ()
prove mode :: Bool
mode info :: ElabInfo
info opt :: Ctxt OptInfo
opt ctxt :: Context
ctxt lit :: Bool
lit n :: Name
n ty :: Type
ty
= do ProofState
ps <- (IState -> ProofState)
-> Idris IState -> StateT IState (ExceptT Err IO) ProofState
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ist :: IState
ist -> Name
-> String -> Context -> Ctxt TypeInfo -> Int -> Type -> ProofState
initElaborator Name
n (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
ist) (IState -> Int
idris_name IState
ist) Type
ty) Idris IState
getIState
String -> Name -> Idris ()
forall a. SExpable a => String -> a -> Idris ()
idemodePutSExp "start-proof-mode" Name
n
(tm :: Type
tm, prf :: [String]
prf) <-
if Bool
mode
then ElabInfo
-> Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> [ElabShellHistory]
-> Maybe History
-> [(Name, Type, Type)]
-> Idris (Type, [String])
elabloop ElabInfo
info Name
n Bool
True ("-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n) [] ((ProofState, EState)
-> String -> Maybe (ElabState EState) -> ElabState EState
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
ps, EState
initEState) "" Maybe (ElabState EState)
forall a. Maybe a
Nothing) [] Maybe History
forall a. Maybe a
Nothing []
else do String -> Idris ()
iputStrLn (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Warning: this interactive prover is deprecated and will be removed " String -> String -> String
forall a. [a] -> [a] -> [a]
++
"in a future release. Please see :elab for a similar feature that "String -> String -> String
forall a. [a] -> [a] -> [a]
++
"will replace it."
Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> Maybe History
-> Idris (Type, [String])
ploop Name
n Bool
True ("-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n) [] ((ProofState, EState)
-> String -> Maybe (ElabState EState) -> ElabState EState
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
ps, EState
initEState) "" Maybe (ElabState EState)
forall a. Maybe a
Nothing) Maybe History
forall a. Maybe a
Nothing
Int -> String -> Idris ()
logLvl 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Adding " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
tm
IState
i <- Idris IState
getIState
let shower :: Bool -> Name -> [String] -> String
shower = if Bool
mode
then Bool -> Name -> [String] -> String
showRunElab
else Bool -> Name -> [String] -> String
showProof
case IState -> OutputMode
idris_outputmode IState
i of
IdeMode _ _ -> String -> (Name, String) -> Idris ()
forall a. SExpable a => String -> a -> Idris ()
idemodePutSExp "end-proof-mode" (Name
n, Bool -> Name -> [String] -> String
shower Bool
lit Name
n [String]
prf)
_ -> String -> Idris ()
iputStrLn (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ Bool -> Name -> [String] -> String
shower Bool
lit Name
n [String]
prf
let proofs :: [(Name, (Bool, [String]))]
proofs = IState -> [(Name, (Bool, [String]))]
proof_list IState
i
IState -> Idris ()
putIState (IState
i { proof_list :: [(Name, (Bool, [String]))]
proof_list = (Name
n, (Bool
mode, [String]
prf)) (Name, (Bool, [String]))
-> [(Name, (Bool, [String]))] -> [(Name, (Bool, [String]))]
forall a. a -> [a] -> [a]
: [(Name, (Bool, [String]))]
proofs })
let tree :: ErasureInfo -> TC CaseDef
tree = Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(Type, Bool)]
-> [([Name], Type, Type)]
-> ErasureInfo
-> TC CaseDef
simpleCase Bool
False (Type -> SC
forall t. t -> SC' t
STerm Type
forall n. TT n
Erased) Bool
False Phase
CompileTime (String -> FC
fileFC "proof") [] [] [([], NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Type
ty, Type
tm)]
Int -> String -> Idris ()
logLvl 3 ((ErasureInfo -> TC CaseDef) -> String
forall a. Show a => a -> String
show ErasureInfo -> TC CaseDef
tree)
(ptm :: Type
ptm, pty :: Type
pty) <- String
-> FC
-> (Err -> Err)
-> Env
-> Type
-> StateT IState (ExceptT Err IO) (Type, Type)
recheckC (ElabInfo -> String
constraintNS ElabInfo
info) (String -> FC
fileFC "proof") Err -> Err
forall a. a -> a
id [] Type
tm
Int -> String -> Idris ()
logLvl 5 ("Proof type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
pty String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
"Expected type:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty)
case Context -> Env -> Type -> Type -> TC ()
converts Context
ctxt [] Type
ty Type
pty of
OK _ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Error e :: Err
e -> Err -> Idris ()
forall a. Err -> Idris a
ierror (Bool
-> (Type, Maybe Provenance)
-> (Type, Maybe Provenance)
-> Err
-> [(Name, Type)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
False (Type
ty, Maybe Provenance
forall a. Maybe a
Nothing) (Type
pty, Maybe Provenance
forall a. Maybe a
Nothing) Err
e [] 0)
Type
ptm' <- Type -> Idris Type
forall term. Optimisable term => term -> Idris term
applyOpts Type
ptm
ErasureInfo
ei <- IState -> ErasureInfo
getErasureInfo (IState -> ErasureInfo)
-> Idris IState -> StateT IState (ExceptT Err IO) ErasureInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Idris IState
getIState
Context
ctxt' <- do Context
ctxt <- Idris Context
getContext
TC Context -> Idris Context
forall a. TC a -> Idris a
tclift (TC Context -> Idris Context) -> TC Context -> Idris Context
forall a b. (a -> b) -> a -> b
$ Name
-> ErasureInfo
-> CaseInfo
-> Bool
-> SC
-> Bool
-> Bool
-> [(Type, Bool)]
-> [Int]
-> [Either Type (Type, Type)]
-> [([Name], Type, Type)]
-> [([Name], Type, Type)]
-> Type
-> Context
-> TC Context
addCasedef Name
n ErasureInfo
ei (Bool -> Bool -> Bool -> CaseInfo
CaseInfo Bool
True Bool
True Bool
False) Bool
False (Type -> SC
forall t. t -> SC' t
STerm Type
forall n. TT n
Erased) Bool
True Bool
False
[] []
[(Type, Type) -> Either Type (Type, Type)
forall a b. b -> Either a b
Right (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Type
ty, Type
ptm)]
[([], NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Type
ty, Type
ptm)]
[([], NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Type
ty, Type
ptm')] Type
ty
Context
ctxt
Context -> Idris ()
setContext Context
ctxt'
FC -> Name -> Idris ()
solveDeferred FC
emptyFC Name
n
case IState -> OutputMode
idris_outputmode IState
i of
IdeMode n :: Integer
n h :: Handle
h ->
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (String -> IO ()) -> String -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> (SExp, String) -> Integer -> String
forall a. SExpable a => String -> a -> Integer -> String
IdeMode.convSExp "return" (String -> SExp
IdeMode.SymbolAtom "ok", "") Integer
n
_ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep st :: ElabState EState
st e :: ElabD a
e =
case StateT (ElabState EState) TC (a, Context)
-> ElabState EState -> TC ((a, Context), ElabState EState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT (ElabState EState) TC (a, Context)
eCheck ElabState EState
st of
OK ((a :: a
a, ctxt' :: Context
ctxt'), ES (ps :: ProofState
ps, est :: EState
est@EState{new_tyDecls :: EState -> [RDeclInstructions]
new_tyDecls = [RDeclInstructions]
declTodo}) x :: String
x old :: Maybe (ElabState EState)
old) ->
do Context -> Idris ()
setContext Context
ctxt'
ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
toplevel [RDeclInstructions]
declTodo
(a, ElabState EState) -> Idris (a, ElabState EState)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, (ProofState, EState)
-> String -> Maybe (ElabState EState) -> ElabState EState
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
ps, EState
est {new_tyDecls :: [RDeclInstructions]
new_tyDecls = []}) String
x Maybe (ElabState EState)
old)
Error a :: Err
a -> Err -> Idris (a, ElabState EState)
forall a. Err -> Idris a
ierror Err
a
where eCheck :: StateT (ElabState EState) TC (a, Context)
eCheck = do a
res <- ElabD a
e
Bool -> Elab' EState ()
forall aux. Bool -> Elab' aux ()
matchProblems Bool
True
Elab' EState ()
forall aux. Elab' aux ()
unifyProblems
Fails
probs' <- Elab' EState Fails
forall aux. Elab' aux Fails
get_probs
case Fails
probs' of
[] -> do Type
tm <- Elab' EState Type
forall aux. Elab' aux Type
get_term
Context
ctxt <- Elab' EState Context
forall aux. Elab' aux Context
get_context
TC (Type, Type) -> StateT (ElabState EState) TC (Type, Type)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Type, Type) -> StateT (ElabState EState) TC (Type, Type))
-> TC (Type, Type) -> StateT (ElabState EState) TC (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt [] (Type -> Raw
forget Type
tm)
(a, Context) -> StateT (ElabState EState) TC (a, Context)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
res, Context
ctxt)
((_,_,_,_,e :: Err
e,_,_):_) -> TC (a, Context) -> StateT (ElabState EState) TC (a, Context)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (a, Context) -> StateT (ElabState EState) TC (a, Context))
-> TC (a, Context) -> StateT (ElabState EState) TC (a, Context)
forall a b. (a -> b) -> a -> b
$ Err -> TC (a, Context)
forall a. Err -> TC a
Error Err
e
dumpState :: IState -> Bool -> [(Name, Type, Term)] -> ProofState -> Idris ()
dumpState :: IState -> Bool -> [(Name, Type, Type)] -> ProofState -> Idris ()
dumpState ist :: IState
ist inElab :: Bool
inElab menv :: [(Name, Type, Type)]
menv ps :: ProofState
ps | [] <- ProofState -> [Name]
holes ProofState
ps =
do let nm :: Name
nm = ProofState -> Name
thname ProofState
ps
SimpleDoc OutputAnnotation
rendered <- Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation)
forall a. Doc a -> Idris (SimpleDoc a)
iRender (Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation))
-> Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
prettyName Bool
True Bool
False [] Name
nm Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text "No more goals."
SimpleDoc OutputAnnotation -> Idris ()
iputGoal SimpleDoc OutputAnnotation
rendered
dumpState ist :: IState
ist inElab :: Bool
inElab menv :: [(Name, Type, Type)]
menv ps :: ProofState
ps | (h :: Name
h : hs :: [Name]
hs) <- ProofState -> [Name]
holes ProofState
ps = do
let OK ty :: Binder Type
ty = ProofState -> TC (Binder Type)
goalAtFocus ProofState
ps
OK env :: Env
env = ProofState -> TC Env
envAtFocus ProofState
ps
state :: Doc OutputAnnotation
state = [Name] -> Doc OutputAnnotation
prettyOtherGoals [Name]
hs Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Bool -> Binder Type -> Env -> Doc OutputAnnotation
prettyAssumptions Bool
inElab Binder Type
ty Env
env Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
[(Name, Type, Type)] -> Doc OutputAnnotation
prettyMetaValues ([(Name, Type, Type)] -> [(Name, Type, Type)]
forall a. [a] -> [a]
reverse [(Name, Type, Type)]
menv) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
[(Name, Bool)] -> Binder Type -> Doc OutputAnnotation
prettyGoal ([Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Env -> [Name]
assumptionNames Env
env) (Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)) Binder Type
ty
SimpleDoc OutputAnnotation
rendered <- Doc OutputAnnotation -> Idris (SimpleDoc OutputAnnotation)
forall a. Doc a -> Idris (SimpleDoc a)
iRender Doc OutputAnnotation
state
SimpleDoc OutputAnnotation -> Idris ()
iputGoal SimpleDoc OutputAnnotation
rendered
where
(h :: Name
h : _) = ProofState -> [Name]
holes ProofState
ps
ppo :: PPOption
ppo = IState -> PPOption
ppOptionIst IState
ist
tPretty :: [(Name, Bool)] -> Type -> Doc OutputAnnotation
tPretty bnd :: [(Name, Bool)]
bnd t :: Type
t = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Type -> OutputAnnotation
AnnTerm [(Name, Bool)]
bnd Type
t) (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (PTerm -> Doc OutputAnnotation) -> PTerm -> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppo [(Name, Bool)]
bnd [] (IState -> [FixDecl]
idris_infixes IState
ist) (PTerm -> Doc OutputAnnotation) -> PTerm -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$
IState -> Type -> PTerm
delab IState
ist Type
t
assumptionNames :: Env -> [Name]
assumptionNames :: Env -> [Name]
assumptionNames = ((Name, RigCount, Binder Type) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Type) -> Name
forall a b c. (a, b, c) -> a
fstEnv
prettyPs :: Bool -> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
prettyPs :: Bool
-> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
prettyPs all :: Bool
all g :: Binder Type
g bnd :: [(Name, Bool)]
bnd [] = Doc OutputAnnotation
forall a. Doc a
empty
prettyPs all :: Bool
all g :: Binder Type
g bnd :: [(Name, Bool)]
bnd ((n :: Name
n@(MN _ r :: Text
r), _, _) : bs :: Env
bs)
| Bool -> Bool
not Bool
all Bool -> Bool -> Bool
&& Text
r Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "rewrite_rule" = Bool
-> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
prettyPs Bool
all Binder Type
g ((Name
n, Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) Env
bs
prettyPs all :: Bool
all g :: Binder Type
g bnd :: [(Name, Bool)]
bnd ((n :: Name
n@(MN _ _), _, _) : bs :: Env
bs)
| Bool -> Bool
not (Bool
all Bool -> Bool -> Bool
|| Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Env -> [Name]
freeEnvNames Env
bs Bool -> Bool -> Bool
|| Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Binder Type -> [Name]
forall n. Eq n => Binder (TT n) -> [n]
goalNames Binder Type
g) = Bool
-> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
prettyPs Bool
all Binder Type
g [(Name, Bool)]
bnd Env
bs
prettyPs all :: Bool
all g :: Binder Type
g bnd :: [(Name, Bool)]
bnd ((n :: Name
n, _, Let rig :: RigCount
rig t :: Type
t v :: Type
v) : bs :: Env
bs) =
Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Name -> Bool -> Doc OutputAnnotation
bindingOf Name
n Bool
False Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text "=" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [(Name, Bool)] -> Type -> Doc OutputAnnotation
tPretty [(Name, Bool)]
bnd Type
v Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([(Name, Bool)] -> Type -> Doc OutputAnnotation
tPretty [(Name, Bool)]
bnd Type
t) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Bool
-> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
prettyPs Bool
all Binder Type
g ((Name
n, Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) Env
bs
prettyPs all :: Bool
all g :: Binder Type
g bnd :: [(Name, Bool)]
bnd ((n :: Name
n, _, b :: Binder Type
b) : bs :: Env
bs) =
Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Name -> Bool -> Doc OutputAnnotation
bindingOf Name
n Bool
False Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([(Name, Bool)] -> Type -> Doc OutputAnnotation
tPretty [(Name, Bool)]
bnd (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b)) Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Bool
-> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
prettyPs Bool
all Binder Type
g ((Name
n, Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) Env
bs
prettyMetaValues :: [(Name, Type, Type)] -> Doc OutputAnnotation
prettyMetaValues [] = Doc OutputAnnotation
forall a. Doc a
empty
prettyMetaValues mvs :: [(Name, Type, Type)]
mvs =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text "---------- Meta-values: ----------" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$$>
[(Name, Bool)] -> [(Name, Type, Type)] -> Doc OutputAnnotation
prettyMetaValues' [] [(Name, Type, Type)]
mvs Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<> Doc OutputAnnotation
forall a. Doc a
line
prettyMetaValues' :: [(Name, Bool)] -> [(Name, Type, Type)] -> Doc OutputAnnotation
prettyMetaValues' _ [] = Doc OutputAnnotation
forall a. Doc a
empty
prettyMetaValues' bnd :: [(Name, Bool)]
bnd [mv :: (Name, Type, Type)
mv] = [(Name, Bool)] -> (Name, Type, Type) -> Doc OutputAnnotation
ppMv [(Name, Bool)]
bnd (Name, Type, Type)
mv
prettyMetaValues' bnd :: [(Name, Bool)]
bnd ((mv :: (Name, Type, Type)
mv@(n :: Name
n, ty :: Type
ty, tm :: Type
tm)) : mvs :: [(Name, Type, Type)]
mvs) =
[(Name, Bool)] -> (Name, Type, Type) -> Doc OutputAnnotation
ppMv [(Name, Bool)]
bnd (Name, Type, Type)
mv Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$>
[(Name, Bool)] -> [(Name, Type, Type)] -> Doc OutputAnnotation
prettyMetaValues' ((Name
n, Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) [(Name, Type, Type)]
mvs
ppMv :: [(Name, Bool)] -> (Name, Type, Type) -> Doc OutputAnnotation
ppMv bnd :: [(Name, Bool)]
bnd (n :: Name
n, ty :: Type
ty, tm :: Type
tm) = String -> Doc OutputAnnotation
kwd "let" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Bool -> Doc OutputAnnotation
bindingOf Name
n Bool
False Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+>
[(Name, Bool)] -> Type -> Doc OutputAnnotation
tPretty [(Name, Bool)]
bnd Type
ty Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text "=" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [(Name, Bool)] -> Type -> Doc OutputAnnotation
tPretty [(Name, Bool)]
bnd Type
tm
kwd :: String -> Doc OutputAnnotation
kwd = OutputAnnotation -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. a -> Doc a -> Doc a
annotate OutputAnnotation
AnnKeyword (Doc OutputAnnotation -> Doc OutputAnnotation)
-> (String -> Doc OutputAnnotation)
-> String
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc OutputAnnotation
forall a. String -> Doc a
text
goalNames :: Binder (TT n) -> [n]
goalNames (Guess t :: TT n
t v :: TT n
v) = TT n -> [n]
forall n. Eq n => TT n -> [n]
freeNames TT n
t [n] -> [n] -> [n]
forall a. [a] -> [a] -> [a]
++ TT n -> [n]
forall n. Eq n => TT n -> [n]
freeNames TT n
v
goalNames b :: Binder (TT n)
b = TT n -> [n]
forall n. Eq n => TT n -> [n]
freeNames (Binder (TT n) -> TT n
forall b. Binder b -> b
binderTy Binder (TT n)
b)
prettyG :: [(Name, Bool)] -> Binder Type -> Doc OutputAnnotation
prettyG bnd :: [(Name, Bool)]
bnd (Guess t :: Type
t v :: Type
v) = [(Name, Bool)] -> Type -> Doc OutputAnnotation
tPretty [(Name, Bool)]
bnd Type
t Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc OutputAnnotation
forall a. String -> Doc a
text "=?=" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [(Name, Bool)] -> Type -> Doc OutputAnnotation
tPretty [(Name, Bool)]
bnd Type
v
prettyG bnd :: [(Name, Bool)]
bnd b :: Binder Type
b = [(Name, Bool)] -> Type -> Doc OutputAnnotation
tPretty [(Name, Bool)]
bnd (Type -> Doc OutputAnnotation) -> Type -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b
prettyGoal :: [(Name, Bool)] -> Binder Type -> Doc OutputAnnotation
prettyGoal bnd :: [(Name, Bool)]
bnd ty :: Binder Type
ty =
String -> Doc OutputAnnotation
forall a. String -> Doc a
text "---------- Goal: ----------" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$$>
Name -> Bool -> Doc OutputAnnotation
bindingOf Name
h Bool
False Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation
forall a. Doc a
colon Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align ([(Name, Bool)] -> Binder Type -> Doc OutputAnnotation
prettyG [(Name, Bool)]
bnd Binder Type
ty)
prettyAssumptions :: Bool -> Binder Type -> Env -> Doc OutputAnnotation
prettyAssumptions inElab :: Bool
inElab g :: Binder Type
g env :: Env
env =
if Env -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Env
env then Doc OutputAnnotation
forall a. Doc a
empty
else
String -> Doc OutputAnnotation
forall a. String -> Doc a
text "---------- Assumptions: ----------" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<>
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (Bool
-> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
prettyPs Bool
inElab Binder Type
g [] (Env -> Doc OutputAnnotation) -> Env -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ Env -> Env
forall a. [a] -> [a]
reverse Env
env)
prettyOtherGoals :: [Name] -> Doc OutputAnnotation
prettyOtherGoals hs :: [Name]
hs =
if [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
hs then Doc OutputAnnotation
forall a. Doc a
empty
else
String -> Doc OutputAnnotation
forall a. String -> Doc a
text "---------- Other goals: ----------" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<$$>
Int -> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a
align (Doc OutputAnnotation -> Doc OutputAnnotation)
-> ([Name] -> Doc OutputAnnotation)
-> [Name]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
cat ([Doc OutputAnnotation] -> Doc OutputAnnotation)
-> ([Name] -> [Doc OutputAnnotation])
-> [Name]
-> Doc OutputAnnotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc OutputAnnotation
-> [Doc OutputAnnotation] -> [Doc OutputAnnotation]
forall a. Doc a -> [Doc a] -> [Doc a]
punctuate (String -> Doc OutputAnnotation
forall a. String -> Doc a
text ",") ([Doc OutputAnnotation] -> [Doc OutputAnnotation])
-> ([Name] -> [Doc OutputAnnotation])
-> [Name]
-> [Doc OutputAnnotation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Doc OutputAnnotation) -> [Name] -> [Doc OutputAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Bool -> Doc OutputAnnotation
`bindingOf` Bool
False) ([Name] -> Doc OutputAnnotation) -> [Name] -> Doc OutputAnnotation
forall a b. (a -> b) -> a -> b
$ [Name]
hs)
freeEnvNames :: Env -> [Name]
freeEnvNames :: Env -> [Name]
freeEnvNames = ((Name, RigCount, Binder Type) -> [Name]) -> Env -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(n :: Name
n, _, b :: Binder Type
b) -> Type -> [Name]
forall n. Eq n => TT n -> [n]
freeNames (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Type
b Type
forall n. TT n
Erased))
lifte :: ElabState EState -> ElabD a -> Idris a
lifte :: ElabState EState -> ElabD a -> Idris a
lifte st :: ElabState EState
st e :: ElabD a
e = do (v :: a
v, _) <- ElabState EState -> ElabD a -> Idris (a, ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
st ElabD a
e
a -> Idris a
forall (m :: * -> *) a. Monad m => a -> m a
return a
v
receiveInput :: Handle -> ElabState EState -> Idris (Maybe String)
receiveInput :: Handle -> ElabState EState -> Idris (Maybe String)
receiveInput h :: Handle
h e :: ElabState EState
e =
do IState
i <- Idris IState
getIState
let inh :: Handle
inh = if Handle
h Handle -> Handle -> Bool
forall a. Eq a => a -> a -> Bool
== Handle
stdout then Handle
stdin else Handle
h
Either Err Int
len' <- IO (Either Err Int) -> Idris (Either Err Int)
forall a. IO a -> Idris a
runIO (IO (Either Err Int) -> Idris (Either Err Int))
-> IO (Either Err Int) -> Idris (Either Err Int)
forall a b. (a -> b) -> a -> b
$ Handle -> IO (Either Err Int)
IdeMode.getLen Handle
inh
Int
len <- case Either Err Int
len' of
Left err :: Err
err -> Err -> Idris Int
forall a. Err -> Idris a
ierror Err
err
Right n :: Int
n -> Int -> Idris Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
String
l <- IO String -> Idris String
forall a. IO a -> Idris a
runIO (IO String -> Idris String) -> IO String -> Idris String
forall a b. (a -> b) -> a -> b
$ Handle -> Int -> String -> IO String
IdeMode.getNChar Handle
inh Int
len ""
(sexp :: SExp
sexp, id :: Integer
id) <- case String -> Either Err (SExp, Integer)
IdeMode.parseMessage String
l of
Left err :: Err
err -> Err -> Idris (SExp, Integer)
forall a. Err -> Idris a
ierror Err
err
Right (sexp :: SExp
sexp, id :: Integer
id) -> (SExp, Integer) -> Idris (SExp, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (SExp
sexp, Integer
id)
IState -> Idris ()
putIState (IState -> Idris ()) -> IState -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState
i { idris_outputmode :: OutputMode
idris_outputmode = Integer -> Handle -> OutputMode
IdeMode Integer
id Handle
h }
case SExp -> Maybe IdeModeCommand
IdeMode.sexpToCommand SExp
sexp of
Just (IdeMode.REPLCompletions prefix :: String
prefix) ->
do (unused :: String
unused, compls :: [Completion]
compls) <- [String] -> CompletionFunc Idris
proverCompletion (ElabState EState -> [String]
assumptionNames ElabState EState
e) (String -> String
forall a. [a] -> [a]
reverse String
prefix, "")
let good :: SExp
good = [SExp] -> SExp
IdeMode.SexpList [String -> SExp
IdeMode.SymbolAtom "ok", ([String], String) -> SExp
forall a. SExpable a => a -> SExp
IdeMode.toSExp ((Completion -> String) -> [Completion] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Completion -> String
replacement [Completion]
compls, String -> String
forall a. [a] -> [a]
reverse String
unused)]
String -> SExp -> Idris ()
forall a. SExpable a => String -> a -> Idris ()
idemodePutSExp "return" SExp
good
Handle -> ElabState EState -> Idris (Maybe String)
receiveInput Handle
h ElabState EState
e
Just (IdeMode.Interpret cmd :: String
cmd) -> Maybe String -> Idris (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just String
cmd)
Just (IdeMode.TypeOf str :: String
str) -> Maybe String -> Idris (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just (":t " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str))
Just (IdeMode.DocsFor str :: String
str _) -> Maybe String -> Idris (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just (":doc " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str))
_ -> Maybe String -> Idris (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing
data ElabShellHistory = ElabStep | LetStep | BothStep
undoStep :: [String] -> [(Name, Type, Term)] -> ElabState EState -> ElabShellHistory -> Idris ([String], [(Name, Type, Term)], ElabState EState)
undoStep :: [String]
-> [(Name, Type, Type)]
-> ElabState EState
-> ElabShellHistory
-> Idris ([String], [(Name, Type, Type)], ElabState EState)
undoStep prf :: [String]
prf env :: [(Name, Type, Type)]
env st :: ElabState EState
st ElabStep = do (_, st' :: ElabState EState
st') <- ElabState EState -> Elab' EState () -> Idris ((), ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
st Elab' EState ()
forall aux. Elab' aux ()
loadState
([String], [(Name, Type, Type)], ElabState EState)
-> Idris ([String], [(Name, Type, Type)], ElabState EState)
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> [String]
forall a. [a] -> [a]
init [String]
prf, [(Name, Type, Type)]
env, ElabState EState
st')
undoStep prf :: [String]
prf env :: [(Name, Type, Type)]
env st :: ElabState EState
st LetStep = ([String], [(Name, Type, Type)], ElabState EState)
-> Idris ([String], [(Name, Type, Type)], ElabState EState)
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> [String]
forall a. [a] -> [a]
init [String]
prf, [(Name, Type, Type)] -> [(Name, Type, Type)]
forall a. [a] -> [a]
tail [(Name, Type, Type)]
env, ElabState EState
st)
undoStep prf :: [String]
prf env :: [(Name, Type, Type)]
env st :: ElabState EState
st BothStep = do (_, st' :: ElabState EState
st') <- ElabState EState -> Elab' EState () -> Idris ((), ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
st Elab' EState ()
forall aux. Elab' aux ()
loadState
([String], [(Name, Type, Type)], ElabState EState)
-> Idris ([String], [(Name, Type, Type)], ElabState EState)
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> [String]
forall a. [a] -> [a]
init [String]
prf, [(Name, Type, Type)] -> [(Name, Type, Type)]
forall a. [a] -> [a]
tail [(Name, Type, Type)]
env, ElabState EState
st')
undoElab :: [String] -> [(Name, Type, Term)] -> ElabState EState -> [ElabShellHistory] -> Idris ([String], [(Name, Type, Term)], ElabState EState, [ElabShellHistory])
undoElab :: [String]
-> [(Name, Type, Type)]
-> ElabState EState
-> [ElabShellHistory]
-> Idris
([String], [(Name, Type, Type)], ElabState EState,
[ElabShellHistory])
undoElab prf :: [String]
prf env :: [(Name, Type, Type)]
env st :: ElabState EState
st [] = String
-> Idris
([String], [(Name, Type, Type)], ElabState EState,
[ElabShellHistory])
forall a. String -> Idris a
ifail "Nothing to undo"
undoElab prf :: [String]
prf env :: [(Name, Type, Type)]
env st :: ElabState EState
st (h :: ElabShellHistory
h:hs :: [ElabShellHistory]
hs) = do (prf' :: [String]
prf', env' :: [(Name, Type, Type)]
env', st' :: ElabState EState
st') <- [String]
-> [(Name, Type, Type)]
-> ElabState EState
-> ElabShellHistory
-> Idris ([String], [(Name, Type, Type)], ElabState EState)
undoStep [String]
prf [(Name, Type, Type)]
env ElabState EState
st ElabShellHistory
h
([String], [(Name, Type, Type)], ElabState EState,
[ElabShellHistory])
-> Idris
([String], [(Name, Type, Type)], ElabState EState,
[ElabShellHistory])
forall (m :: * -> *) a. Monad m => a -> m a
return ([String]
prf', [(Name, Type, Type)]
env', ElabState EState
st', [ElabShellHistory]
hs)
proverfc :: FC
proverfc = String -> FC
fileFC "prover"
runWithInterrupt
:: ElabState EState
-> Idris a
-> Idris b
-> Idris b
-> Idris b
runWithInterrupt :: ElabState EState -> Idris a -> Idris b -> Idris b -> Idris b
runWithInterrupt elabState :: ElabState EState
elabState mTry :: Idris a
mTry mSuccess :: Idris b
mSuccess mFailure :: Idris b
mFailure = do
IState
ist <- Idris IState
getIState
case IState -> OutputMode
idris_outputmode IState
ist of
RawOutput _ -> do
Bool
success <- Settings Idris -> InputT Idris Bool -> Idris Bool
forall (m :: * -> *) a.
MonadException m =>
Settings m -> InputT m a -> m a
runInputT (ElabState EState -> Settings Idris
proverSettings ElabState EState
elabState) (InputT Idris Bool -> Idris Bool)
-> InputT Idris Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$
InputT Idris Bool -> InputT Idris Bool -> InputT Idris Bool
forall (m :: * -> *) a. MonadException m => m a -> m a -> m a
handleInterrupt (Bool -> InputT Idris Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) (InputT Idris Bool -> InputT Idris Bool)
-> InputT Idris Bool -> InputT Idris Bool
forall a b. (a -> b) -> a -> b
$
InputT Idris Bool -> InputT Idris Bool
forall (m :: * -> *) a.
MonadException m =>
InputT m a -> InputT m a
withInterrupt (Idris a -> InputT Idris a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Idris a
mTry InputT Idris a -> InputT Idris Bool -> InputT Idris Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> InputT Idris Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
if Bool
success then Idris b
mSuccess else Idris b
mFailure
IdeMode _ _ -> Idris a
mTry Idris a -> Idris b -> Idris b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Idris b
mSuccess
elabloop :: ElabInfo -> Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
elabloop :: ElabInfo
-> Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> [ElabShellHistory]
-> Maybe History
-> [(Name, Type, Type)]
-> Idris (Type, [String])
elabloop info :: ElabInfo
info fn :: Name
fn d :: Bool
d prompt :: String
prompt prf :: [String]
prf e :: ElabState EState
e prev :: [ElabShellHistory]
prev h :: Maybe History
h env :: [(Name, Type, Type)]
env
= do IState
ist <- Idris IState
getIState
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
d (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState -> Bool -> [(Name, Type, Type)] -> ProofState -> Idris ()
dumpState IState
ist Bool
True [(Name, Type, Type)]
env (ElabState EState -> ProofState
forall aux. ElabState aux -> ProofState
proof ElabState EState
e)
(x :: Maybe String
x, h' :: Maybe History
h') <-
case IState -> OutputMode
idris_outputmode IState
ist of
RawOutput _ ->
Settings Idris
-> InputT Idris (Maybe String, Maybe History)
-> Idris (Maybe String, Maybe History)
forall (m :: * -> *) a.
MonadException m =>
Settings m -> InputT m a -> m a
runInputT (ElabState EState -> Settings Idris
proverSettings ElabState EState
e) (InputT Idris (Maybe String, Maybe History)
-> Idris (Maybe String, Maybe History))
-> InputT Idris (Maybe String, Maybe History)
-> Idris (Maybe String, Maybe History)
forall a b. (a -> b) -> a -> b
$
do case Maybe History
h of
Just history :: History
history -> History -> InputT Idris ()
forall (m :: * -> *). MonadIO m => History -> InputT m ()
putHistory History
history
Nothing -> () -> InputT Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe String
l <- InputT Idris (Maybe String)
-> InputT Idris (Maybe String) -> InputT Idris (Maybe String)
forall (m :: * -> *) a. MonadException m => m a -> m a -> m a
handleInterrupt (Maybe String -> InputT Idris (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> InputT Idris (Maybe String))
-> Maybe String -> InputT Idris (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just "") (InputT Idris (Maybe String) -> InputT Idris (Maybe String))
-> InputT Idris (Maybe String) -> InputT Idris (Maybe String)
forall a b. (a -> b) -> a -> b
$ InputT Idris (Maybe String) -> InputT Idris (Maybe String)
forall (m :: * -> *) a.
MonadException m =>
InputT m a -> InputT m a
withInterrupt (InputT Idris (Maybe String) -> InputT Idris (Maybe String))
-> InputT Idris (Maybe String) -> InputT Idris (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> InputT Idris (Maybe String)
forall (m :: * -> *).
MonadException m =>
String -> InputT m (Maybe String)
getInputLine (String
prompt String -> String -> String
forall a. [a] -> [a] -> [a]
++ "> ")
History
h' <- InputT Idris History
forall (m :: * -> *). MonadIO m => InputT m History
getHistory
(Maybe String, Maybe History)
-> InputT Idris (Maybe String, Maybe History)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
l, History -> Maybe History
forall a. a -> Maybe a
Just History
h')
IdeMode _ handle :: Handle
handle ->
do String -> Idris ()
isetPrompt String
prompt
Maybe String
i <- Handle -> ElabState EState -> Idris (Maybe String)
receiveInput Handle
handle ElabState EState
e
(Maybe String, Maybe History)
-> Idris (Maybe String, Maybe History)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
i, Maybe History
h)
(cmd :: Either ParseError (Either ElabShellCmd PDo)
cmd, step :: String
step) <- case Maybe String
x of
Nothing -> do String -> Idris ()
iPrintError "" ; String
-> Idris (Either ParseError (Either ElabShellCmd PDo), String)
forall a. String -> Idris a
ifail "Abandoned"
Just input :: String
input -> (Either ParseError (Either ElabShellCmd PDo), String)
-> Idris (Either ParseError (Either ElabShellCmd PDo), String)
forall (m :: * -> *) a. Monad m => a -> m a
return (IState -> String -> Either ParseError (Either ElabShellCmd PDo)
parseElabShellStep IState
ist String
input, String
input)
case Either ParseError (Either ElabShellCmd PDo)
cmd of
Right (Left EAbandon) -> do String -> Idris ()
iPrintError ""; String -> Idris ()
forall a. String -> Idris a
ifail "Abandoned"
_ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(d :: Bool
d, prev' :: [ElabShellHistory]
prev', st :: ElabState EState
st, done :: Bool
done, prf' :: [String]
prf', env' :: [(Name, Type, Type)]
env', res :: Either Err (Idris ())
res) <-
Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> (Err
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ())))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
(case Either ParseError (Either ElabShellCmd PDo)
cmd of
Left err :: ParseError
err -> do
Either Err (Idris ())
msg <- (Doc OutputAnnotation -> Either Err (Idris ()))
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
-> StateT IState (ExceptT Err IO) (Either Err (Idris ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Err -> Either Err (Idris ())
forall a b. a -> Either a b
Left (Err -> Either Err (Idris ()))
-> (Doc OutputAnnotation -> Err)
-> Doc OutputAnnotation
-> Either Err (Idris ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Err)
-> (Doc OutputAnnotation -> String) -> Doc OutputAnnotation -> Err
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc OutputAnnotation -> String
forall a. Show a => a -> String
show) (ParseError -> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
forall w.
Message w =>
w -> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
formatMessage ParseError
err)
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf, [(Name, Type, Type)]
env, Either Err (Idris ())
msg)
Right (Left cmd' :: ElabShellCmd
cmd') ->
case ElabShellCmd
cmd' of
EQED -> do [Name]
hs <- ElabState EState -> ElabD [Name] -> Idris [Name]
forall a. ElabState EState -> ElabD a -> Idris a
lifte ElabState EState
e ElabD [Name]
forall aux. Elab' aux [Name]
get_holes
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
hs) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> Idris ()
forall a. String -> Idris a
ifail "Incomplete proof"
String -> Idris ()
iputStrLn "Proof completed!"
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [ElabShellHistory]
prev, ElabState EState
e, Bool
True, [String]
prf, [(Name, Type, Type)]
env, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (Idris () -> Either Err (Idris ()))
-> Idris () -> Either Err (Idris ())
forall a b. (a -> b) -> a -> b
$ String -> Idris ()
iPrintResult "")
EUndo -> do (prf' :: [String]
prf', env' :: [(Name, Type, Type)]
env', st' :: ElabState EState
st', prev' :: [ElabShellHistory]
prev') <- [String]
-> [(Name, Type, Type)]
-> ElabState EState
-> [ElabShellHistory]
-> Idris
([String], [(Name, Type, Type)], ElabState EState,
[ElabShellHistory])
undoElab [String]
prf [(Name, Type, Type)]
env ElabState EState
e [ElabShellHistory]
prev
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [ElabShellHistory]
prev', ElabState EState
st', Bool
False, [String]
prf', [(Name, Type, Type)]
env', Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (Idris () -> Either Err (Idris ()))
-> Idris () -> Either Err (Idris ())
forall a b. (a -> b) -> a -> b
$ String -> Idris ()
iPrintResult "")
EAbandon ->
String
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall a. HasCallStack => String -> a
error "the impossible happened - should have been matched on outer scope"
EProofState -> (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf, [(Name, Type, Type)]
env, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (Idris () -> Either Err (Idris ()))
-> Idris () -> Either Err (Idris ())
forall a b. (a -> b) -> a -> b
$ String -> Idris ()
iPrintResult "")
EProofTerm ->
do Type
tm <- ElabState EState -> Elab' EState Type -> Idris Type
forall a. ElabState EState -> ElabD a -> Idris a
lifte ElabState EState
e Elab' EState Type
forall aux. Elab' aux Type
get_term
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf, [(Name, Type, Type)]
env, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (Idris () -> Either Err (Idris ()))
-> Idris () -> Either Err (Idris ())
forall a b. (a -> b) -> a -> b
$ Doc OutputAnnotation -> Idris ()
iRenderResult (String -> Doc OutputAnnotation
forall a. String -> Doc a
text "TT:" Doc OutputAnnotation
-> Doc OutputAnnotation -> Doc OutputAnnotation
forall a. Doc a -> Doc a -> Doc a
<+> [Name] -> Type -> Doc OutputAnnotation
pprintTT [] Type
tm))
EEval tm :: PTerm
tm -> do (d' :: Bool
d', st' :: ElabState EState
st', done :: Bool
done, prf' :: [String]
prf', go :: Either Err (Idris ())
go) <- ElabState EState
-> [String]
-> PTerm
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
evalTerm ElabState EState
e [String]
prf PTerm
tm
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
d', [ElabShellHistory]
prev, ElabState EState
st', Bool
done, [String]
prf', [(Name, Type, Type)]
env, Either Err (Idris ())
go)
ECheck (PRef _ _ n :: Name
n) ->
do (d' :: Bool
d', st' :: ElabState EState
st', done :: Bool
done, prf' :: [String]
prf', go :: Either Err (Idris ())
go) <- ElabState EState
-> [String]
-> Name
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
checkNameType ElabState EState
e [String]
prf Name
n
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
d', [ElabShellHistory]
prev, ElabState EState
st', Bool
done, [String]
prf', [(Name, Type, Type)]
env, Either Err (Idris ())
go)
ECheck tm :: PTerm
tm -> do (d' :: Bool
d', st' :: ElabState EState
st', done :: Bool
done, prf' :: [String]
prf', go :: Either Err (Idris ())
go) <- ElabState EState
-> [String]
-> PTerm
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
checkType ElabState EState
e [String]
prf PTerm
tm
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
d', [ElabShellHistory]
prev, ElabState EState
st', Bool
done, [String]
prf', [(Name, Type, Type)]
env, Either Err (Idris ())
go)
ESearch ty :: PTerm
ty -> do (d' :: Bool
d', st' :: ElabState EState
st', done :: Bool
done, prf' :: [String]
prf', go :: Either Err (Idris ())
go) <- ElabState EState
-> [String]
-> PTerm
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) b d a.
Monad m =>
b -> d -> PTerm -> m (Bool, b, Bool, d, Either a (Idris ()))
search ElabState EState
e [String]
prf PTerm
ty
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
d', [ElabShellHistory]
prev, ElabState EState
st', Bool
done, [String]
prf', [(Name, Type, Type)]
env, Either Err (Idris ())
go)
EDocStr d :: Either Name Const
d -> do (d' :: Bool
d', st' :: ElabState EState
st', done :: Bool
done, prf' :: [String]
prf', go :: Either Err (Idris ())
go) <- ElabState EState
-> [String]
-> Either Name Const
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
docStr ElabState EState
e [String]
prf Either Name Const
d
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
d', [ElabShellHistory]
prev, ElabState EState
st', Bool
done, [String]
prf', [(Name, Type, Type)]
env, Either Err (Idris ())
go)
Right (Right cmd' :: PDo
cmd') ->
case PDo
cmd' of
DoLetP {} -> String
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall a. String -> Idris a
ifail "Pattern-matching let not supported here"
DoRewrite {} -> String
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall a. String -> Idris a
ifail "Pattern-matching do-rewrite not supported here"
DoBindP {} -> String
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall a. String -> Idris a
ifail "Pattern-matching <- not supported here"
DoLet fc :: FC
fc rig :: RigCount
rig i :: Name
i ifc :: FC
ifc Placeholder expr :: PTerm
expr ->
do (tm :: Type
tm, ty :: Type
ty) <- ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Type, Type)
elabVal (FC -> ElabInfo
recinfo FC
proverfc) ElabMode
ERHS (IState -> [(Name, Type, Type)] -> PTerm -> PTerm
inLets IState
ist [(Name, Type, Type)]
env PTerm
expr)
Context
ctxt <- Idris Context
getContext
let tm' :: Type
tm' = Context -> Env -> Type -> Type
normaliseAll Context
ctxt [] Type
tm
ty' :: Type
ty' = Context -> Env -> Type -> Type
normaliseAll Context
ctxt [] Type
ty
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabShellHistory
LetStepElabShellHistory -> [ElabShellHistory] -> [ElabShellHistory]
forall a. a -> [a] -> [a]
:[ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
step], (Name
i, Type
ty', Type
tm' ) (Name, Type, Type) -> [(Name, Type, Type)] -> [(Name, Type, Type)]
forall a. a -> [a] -> [a]
: [(Name, Type, Type)]
env, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (String -> Idris ()
iPrintResult ""))
DoLet fc :: FC
fc rig :: RigCount
rig i :: Name
i ifc :: FC
ifc ty :: PTerm
ty expr :: PTerm
expr ->
do (tm :: Type
tm, ty :: Type
ty) <- ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Type, Type)
elabVal (FC -> ElabInfo
recinfo FC
proverfc) ElabMode
ERHS
(FC -> PTerm -> [PArg] -> PTerm
PApp FC
NoFC (FC -> [FC] -> Name -> PTerm
PRef FC
NoFC [] (String -> Name
sUN "the"))
[ PTerm -> PArg
forall t. t -> PArg' t
pexp (IState -> [(Name, Type, Type)] -> PTerm -> PTerm
inLets IState
ist [(Name, Type, Type)]
env PTerm
ty)
, PTerm -> PArg
forall t. t -> PArg' t
pexp (IState -> [(Name, Type, Type)] -> PTerm -> PTerm
inLets IState
ist [(Name, Type, Type)]
env PTerm
expr)
])
Context
ctxt <- Idris Context
getContext
let tm' :: Type
tm' = Context -> Env -> Type -> Type
normaliseAll Context
ctxt [] Type
tm
ty' :: Type
ty' = Context -> Env -> Type -> Type
normaliseAll Context
ctxt [] Type
ty
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabShellHistory
LetStepElabShellHistory -> [ElabShellHistory] -> [ElabShellHistory]
forall a. a -> [a] -> [a]
:[ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
step], (Name
i, Type
ty', Type
tm' ) (Name, Type, Type) -> [(Name, Type, Type)] -> [(Name, Type, Type)]
forall a. a -> [a] -> [a]
: [(Name, Type, Type)]
env, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (String -> Idris ()
iPrintResult ""))
DoBind fc :: FC
fc i :: Name
i ifc :: FC
ifc expr :: PTerm
expr ->
do (tm :: Type
tm, ty :: Type
ty) <- ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Type, Type)
elabVal (FC -> ElabInfo
recinfo FC
proverfc) ElabMode
ERHS (IState -> [(Name, Type, Type)] -> PTerm -> PTerm
inLets IState
ist [(Name, Type, Type)]
env PTerm
expr)
(_, e' :: ElabState EState
e') <- ElabState EState -> Elab' EState () -> Idris ((), ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e Elab' EState ()
forall aux. Elab' aux ()
saveState
(res :: Type
res, e'' :: ElabState EState
e'') <- ElabState EState
-> Elab' EState Type -> Idris (Type, ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e' (Elab' EState Type -> Idris (Type, ElabState EState))
-> Elab' EState Type -> Idris (Type, ElabState EState)
forall a b. (a -> b) -> a -> b
$
ElabInfo
-> IState -> FC -> Env -> Type -> [String] -> Elab' EState Type
runElabAction ElabInfo
info IState
ist FC
NoFC [] Type
tm ["Shell"]
Context
ctxt <- Idris Context
getContext
(v :: Type
v, vty :: Type
vty) <- TC (Type, Type) -> StateT IState (ExceptT Err IO) (Type, Type)
forall a. TC a -> Idris a
tclift (TC (Type, Type) -> StateT IState (ExceptT Err IO) (Type, Type))
-> TC (Type, Type) -> StateT IState (ExceptT Err IO) (Type, Type)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt [] (Type -> Raw
forget Type
res)
let v' :: Type
v' = Context -> Env -> Type -> Type
normaliseAll Context
ctxt [] Type
v
vty' :: Type
vty' = Context -> Env -> Type -> Type
normaliseAll Context
ctxt [] Type
vty
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabShellHistory
BothStepElabShellHistory -> [ElabShellHistory] -> [ElabShellHistory]
forall a. a -> [a] -> [a]
:[ElabShellHistory]
prev, ElabState EState
e'', Bool
False, [String]
prf [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
step], (Name
i, Type
vty', Type
v') (Name, Type, Type) -> [(Name, Type, Type)] -> [(Name, Type, Type)]
forall a. a -> [a] -> [a]
: [(Name, Type, Type)]
env, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (String -> Idris ()
iPrintResult ""))
DoExp fc :: FC
fc expr :: PTerm
expr ->
do (tm :: Type
tm, ty :: Type
ty) <- ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Type, Type)
elabVal (FC -> ElabInfo
recinfo FC
proverfc) ElabMode
ERHS (IState -> [(Name, Type, Type)] -> PTerm -> PTerm
inLets IState
ist [(Name, Type, Type)]
env PTerm
expr)
(_, e' :: ElabState EState
e') <- ElabState EState -> Elab' EState () -> Idris ((), ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e Elab' EState ()
forall aux. Elab' aux ()
saveState
(_, e'' :: ElabState EState
e'') <- ElabState EState
-> Elab' EState Type -> Idris (Type, ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e' (Elab' EState Type -> Idris (Type, ElabState EState))
-> Elab' EState Type -> Idris (Type, ElabState EState)
forall a b. (a -> b) -> a -> b
$
ElabInfo
-> IState -> FC -> Env -> Type -> [String] -> Elab' EState Type
runElabAction ElabInfo
info IState
ist FC
NoFC [] Type
tm ["Shell"]
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabShellHistory
ElabStepElabShellHistory -> [ElabShellHistory] -> [ElabShellHistory]
forall a. a -> [a] -> [a]
:[ElabShellHistory]
prev, ElabState EState
e'', Bool
False, [String]
prf [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
step], [(Name, Type, Type)]
env, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (String -> Idris ()
iPrintResult "")))
(\err :: Err
err -> (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
-> Idris
(Bool, [ElabShellHistory], ElabState EState, Bool, [String],
[(Name, Type, Type)], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf, [(Name, Type, Type)]
env, Err -> Either Err (Idris ())
forall a b. a -> Either a b
Left Err
err))
String -> ([String], Int) -> Idris ()
forall a. SExpable a => String -> a -> Idris ()
idemodePutSExp "write-proof-state" ([String]
prf', [String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
prf')
case Either Err (Idris ())
res of
Left err :: Err
err -> do IState
ist <- Idris IState
getIState
Doc OutputAnnotation -> Idris ()
iRenderError (Doc OutputAnnotation -> Idris ())
-> Doc OutputAnnotation -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState -> Err -> Doc OutputAnnotation
pprintErr IState
ist Err
err
ElabInfo
-> Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> [ElabShellHistory]
-> Maybe History
-> [(Name, Type, Type)]
-> Idris (Type, [String])
elabloop ElabInfo
info Name
fn Bool
d String
prompt [String]
prf' ElabState EState
st [ElabShellHistory]
prev' Maybe History
h' [(Name, Type, Type)]
env'
Right ok :: Idris ()
ok ->
if Bool
done then do (tm :: Type
tm, _) <- ElabState EState
-> Elab' EState Type -> Idris (Type, ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
st Elab' EState Type
forall aux. Elab' aux Type
get_term
(Type, [String]) -> Idris (Type, [String])
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
tm, [String]
prf')
else ElabState EState
-> Idris ()
-> Idris (Type, [String])
-> Idris (Type, [String])
-> Idris (Type, [String])
forall a b.
ElabState EState -> Idris a -> Idris b -> Idris b -> Idris b
runWithInterrupt ElabState EState
e Idris ()
ok
(ElabInfo
-> Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> [ElabShellHistory]
-> Maybe History
-> [(Name, Type, Type)]
-> Idris (Type, [String])
elabloop ElabInfo
info Name
fn Bool
d String
prompt [String]
prf' ElabState EState
st [ElabShellHistory]
prev' Maybe History
h' [(Name, Type, Type)]
env')
(ElabInfo
-> Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> [ElabShellHistory]
-> Maybe History
-> [(Name, Type, Type)]
-> Idris (Type, [String])
elabloop ElabInfo
info Name
fn Bool
d String
prompt [String]
prf ElabState EState
e [ElabShellHistory]
prev Maybe History
h' [(Name, Type, Type)]
env)
where
inLets :: IState -> [(Name, Type, Term)] -> PTerm -> PTerm
inLets :: IState -> [(Name, Type, Type)] -> PTerm -> PTerm
inLets ist :: IState
ist lets :: [(Name, Type, Type)]
lets tm :: PTerm
tm = ((Name, Type, Type) -> PTerm -> PTerm)
-> PTerm -> [(Name, Type, Type)] -> PTerm
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(n :: Name
n, ty :: Type
ty, v :: Type
v) b :: PTerm
b -> FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
NoFC RigCount
RigW Name
n FC
NoFC (IState -> Type -> PTerm
delab IState
ist Type
ty) (IState -> Type -> PTerm
delab IState
ist Type
v) PTerm
b) PTerm
tm ([(Name, Type, Type)] -> [(Name, Type, Type)]
forall a. [a] -> [a]
reverse [(Name, Type, Type)]
lets)
ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])
ploop :: Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> Maybe History
-> Idris (Type, [String])
ploop fn :: Name
fn d :: Bool
d prompt :: String
prompt prf :: [String]
prf e :: ElabState EState
e h :: Maybe History
h
= do IState
i <- Idris IState
getIState
let autoSolve :: Bool
autoSolve = IOption -> Bool
opt_autoSolve (IState -> IOption
idris_options IState
i)
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
d (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState -> Bool -> [(Name, Type, Type)] -> ProofState -> Idris ()
dumpState IState
i Bool
False [] (ElabState EState -> ProofState
forall aux. ElabState aux -> ProofState
proof ElabState EState
e)
(x :: Maybe String
x, h' :: Maybe History
h') <-
case IState -> OutputMode
idris_outputmode IState
i of
RawOutput _ ->
Settings Idris
-> InputT Idris (Maybe String, Maybe History)
-> Idris (Maybe String, Maybe History)
forall (m :: * -> *) a.
MonadException m =>
Settings m -> InputT m a -> m a
runInputT (ElabState EState -> Settings Idris
proverSettings ElabState EState
e) (InputT Idris (Maybe String, Maybe History)
-> Idris (Maybe String, Maybe History))
-> InputT Idris (Maybe String, Maybe History)
-> Idris (Maybe String, Maybe History)
forall a b. (a -> b) -> a -> b
$
do case Maybe History
h of
Just history :: History
history -> History -> InputT Idris ()
forall (m :: * -> *). MonadIO m => History -> InputT m ()
putHistory History
history
Nothing -> () -> InputT Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe String
l <- InputT Idris (Maybe String)
-> InputT Idris (Maybe String) -> InputT Idris (Maybe String)
forall (m :: * -> *) a. MonadException m => m a -> m a -> m a
handleInterrupt (Maybe String -> InputT Idris (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> InputT Idris (Maybe String))
-> Maybe String -> InputT Idris (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just "") (InputT Idris (Maybe String) -> InputT Idris (Maybe String))
-> InputT Idris (Maybe String) -> InputT Idris (Maybe String)
forall a b. (a -> b) -> a -> b
$ InputT Idris (Maybe String) -> InputT Idris (Maybe String)
forall (m :: * -> *) a.
MonadException m =>
InputT m a -> InputT m a
withInterrupt (InputT Idris (Maybe String) -> InputT Idris (Maybe String))
-> InputT Idris (Maybe String) -> InputT Idris (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> InputT Idris (Maybe String)
forall (m :: * -> *).
MonadException m =>
String -> InputT m (Maybe String)
getInputLine (String
prompt String -> String -> String
forall a. [a] -> [a] -> [a]
++ "> ")
History
h' <- InputT Idris History
forall (m :: * -> *). MonadIO m => InputT m History
getHistory
(Maybe String, Maybe History)
-> InputT Idris (Maybe String, Maybe History)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
l, History -> Maybe History
forall a. a -> Maybe a
Just History
h')
IdeMode _ handle :: Handle
handle ->
do String -> Idris ()
isetPrompt String
prompt
Maybe String
i <- Handle -> ElabState EState -> Idris (Maybe String)
receiveInput Handle
handle ElabState EState
e
(Maybe String, Maybe History)
-> Idris (Maybe String, Maybe History)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
i, Maybe History
h)
(cmd :: Either ParseError PTactic
cmd, step :: String
step) <- case Maybe String
x of
Nothing -> do String -> Idris ()
iPrintError ""; String -> Idris (Either ParseError PTactic, String)
forall a. String -> Idris a
ifail "Abandoned"
Just input :: String
input -> (Either ParseError PTactic, String)
-> Idris (Either ParseError PTactic, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (IState -> String -> Either ParseError PTactic
parseTactic IState
i String
input, String
input)
case Either ParseError PTactic
cmd of
Right Abandon -> do String -> Idris ()
iPrintError ""; String -> Idris ()
forall a. String -> Idris a
ifail "Abandoned"
_ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(d :: Bool
d, st :: ElabState EState
st, done :: Bool
done, prf' :: [String]
prf', res :: Either Err (Idris ())
res) <- Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> (Err
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ())))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
(case Either ParseError PTactic
cmd of
Left err :: ParseError
err -> do
Either Err (Idris ())
msg <- (Doc OutputAnnotation -> Either Err (Idris ()))
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
-> StateT IState (ExceptT Err IO) (Either Err (Idris ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Err -> Either Err (Idris ())
forall a b. a -> Either a b
Left (Err -> Either Err (Idris ()))
-> (Doc OutputAnnotation -> Err)
-> Doc OutputAnnotation
-> Either Err (Idris ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Err)
-> (Doc OutputAnnotation -> String) -> Doc OutputAnnotation -> Err
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc OutputAnnotation -> String
forall a. Show a => a -> String
show) (ParseError -> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
forall w.
Message w =>
w -> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
formatMessage ParseError
err)
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf, Either Err (Idris ())
msg)
Right Undo -> do (_, st :: ElabState EState
st) <- ElabState EState -> Elab' EState () -> Idris ((), ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e Elab' EState ()
forall aux. Elab' aux ()
loadState
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabState EState
st, Bool
False, [String] -> [String]
forall a. [a] -> [a]
init [String]
prf, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (Idris () -> Either Err (Idris ()))
-> Idris () -> Either Err (Idris ())
forall a b. (a -> b) -> a -> b
$ String -> Idris ()
iPrintResult "")
Right ProofState -> (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabState EState
e, Bool
False, [String]
prf, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (Idris () -> Either Err (Idris ()))
-> Idris () -> Either Err (Idris ())
forall a b. (a -> b) -> a -> b
$ String -> Idris ()
iPrintResult "")
Right ProofTerm -> do Type
tm <- ElabState EState -> Elab' EState Type -> Idris Type
forall a. ElabState EState -> ElabD a -> Idris a
lifte ElabState EState
e Elab' EState Type
forall aux. Elab' aux Type
get_term
String -> Idris ()
iputStrLn (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "TT: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
tm String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (Idris () -> Either Err (Idris ()))
-> Idris () -> Either Err (Idris ())
forall a b. (a -> b) -> a -> b
$ String -> Idris ()
iPrintResult "")
Right Qed -> do [Name]
hs <- ElabState EState -> ElabD [Name] -> Idris [Name]
forall a. ElabState EState -> ElabD a -> Idris a
lifte ElabState EState
e ElabD [Name]
forall aux. Elab' aux [Name]
get_holes
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
hs) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> Idris ()
forall a. String -> Idris a
ifail "Incomplete proof"
String -> Idris ()
iputStrLn "Proof completed!"
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
True, [String]
prf, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (Idris () -> Either Err (Idris ()))
-> Idris () -> Either Err (Idris ())
forall a b. (a -> b) -> a -> b
$ String -> Idris ()
iPrintResult "")
Right (TCheck (PRef _ _ n :: Name
n)) -> ElabState EState
-> [String]
-> Name
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
checkNameType ElabState EState
e [String]
prf Name
n
Right (TCheck t :: PTerm
t) -> ElabState EState
-> [String]
-> PTerm
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
checkType ElabState EState
e [String]
prf PTerm
t
Right (TEval t :: PTerm
t) -> ElabState EState
-> [String]
-> PTerm
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
evalTerm ElabState EState
e [String]
prf PTerm
t
Right (TDocStr x :: Either Name Const
x) -> ElabState EState
-> [String]
-> Either Name Const
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
docStr ElabState EState
e [String]
prf Either Name Const
x
Right (TSearch t :: PTerm
t) -> ElabState EState
-> [String]
-> PTerm
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) b d a.
Monad m =>
b -> d -> PTerm -> m (Bool, b, Bool, d, Either a (Idris ()))
search ElabState EState
e [String]
prf PTerm
t
Right tac :: PTactic
tac ->
do (_, e :: ElabState EState
e) <- ElabState EState -> Elab' EState () -> Idris ((), ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e Elab' EState ()
forall aux. Elab' aux ()
saveState
(_, st :: ElabState EState
st) <- ElabState EState -> Elab' EState () -> Idris ((), ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e (Bool -> IState -> Maybe FC -> Name -> PTactic -> Elab' EState ()
runTac Bool
autoSolve IState
i (FC -> Maybe FC
forall a. a -> Maybe a
Just FC
proverFC) Name
fn PTactic
tac)
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabState EState
st, Bool
False, [String]
prf [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
step], Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (Idris () -> Either Err (Idris ()))
-> Idris () -> Either Err (Idris ())
forall a b. (a -> b) -> a -> b
$ String -> Idris ()
iPrintResult ""))
(\err :: Err
err -> (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf, Err -> Either Err (Idris ())
forall a b. a -> Either a b
Left Err
err))
String -> ([String], Int) -> Idris ()
forall a. SExpable a => String -> a -> Idris ()
idemodePutSExp "write-proof-state" ([String]
prf', [String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
prf')
case Either Err (Idris ())
res of
Left err :: Err
err -> do IState
ist <- Idris IState
getIState
Doc OutputAnnotation -> Idris ()
iRenderError (Doc OutputAnnotation -> Idris ())
-> Doc OutputAnnotation -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState -> Err -> Doc OutputAnnotation
pprintErr IState
ist Err
err
Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> Maybe History
-> Idris (Type, [String])
ploop Name
fn Bool
d String
prompt [String]
prf' ElabState EState
st Maybe History
h'
Right ok :: Idris ()
ok ->
if Bool
done then do (tm :: Type
tm, _) <- ElabState EState
-> Elab' EState Type -> Idris (Type, ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
st Elab' EState Type
forall aux. Elab' aux Type
get_term
(Type, [String]) -> Idris (Type, [String])
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
tm, [String]
prf')
else ElabState EState
-> Idris ()
-> Idris (Type, [String])
-> Idris (Type, [String])
-> Idris (Type, [String])
forall a b.
ElabState EState -> Idris a -> Idris b -> Idris b -> Idris b
runWithInterrupt ElabState EState
e Idris ()
ok
(Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> Maybe History
-> Idris (Type, [String])
ploop Name
fn Bool
d String
prompt [String]
prf' ElabState EState
st Maybe History
h')
(Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> Maybe History
-> Idris (Type, [String])
ploop Name
fn Bool
d String
prompt [String]
prf ElabState EState
e Maybe History
h')
envCtxt :: t (Name, b, Binder Type) -> Context -> Context
envCtxt env :: t (Name, b, Binder Type)
env ctxt :: Context
ctxt = (Context -> (Name, b, Binder Type) -> Context)
-> Context -> t (Name, b, Binder Type) -> Context
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\c :: Context
c (n :: Name
n, _, b :: Binder Type
b) -> Name -> NameType -> Type -> Context -> Context
addTyDecl Name
n NameType
Bound (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b) Context
c) Context
ctxt t (Name, b, Binder Type)
env
checkNameType :: ElabState EState -> [String] -> Name -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
checkNameType :: ElabState EState
-> [String]
-> Name
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
checkNameType e :: ElabState EState
e prf :: [String]
prf n :: Name
n = do
Context
ctxt <- Idris Context
getContext
IState
ist <- Idris IState
getIState
Bool
imp <- Idris Bool
impShow
Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> (Err
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ())))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do
let OK env :: Env
env = ProofState -> TC Env
envAtFocus (ElabState EState -> ProofState
forall aux. ElabState aux -> ProofState
proof ElabState EState
e)
ctxt' :: Context
ctxt' = Env -> Context -> Context
forall (t :: * -> *) b.
Foldable t =>
t (Name, b, Binder Type) -> Context -> Context
envCtxt Env
env Context
ctxt
bnd :: [(Name, Bool)]
bnd = ((Name, RigCount, Binder Type) -> (Name, Bool))
-> Env -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: (Name, RigCount, Binder Type)
x -> ((Name, RigCount, Binder Type) -> Name
forall a b c. (a, b, c) -> a
fstEnv (Name, RigCount, Binder Type)
x, Bool
False)) Env
env
ist' :: IState
ist' = IState
ist { tt_ctxt :: Context
tt_ctxt = Context
ctxt' }
IState -> Idris ()
putIState IState
ist'
let action :: Idris ()
action = case Name -> Context -> [Name]
lookupNames Name
n Context
ctxt' of
[] -> String -> Idris ()
iPrintError (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "No such variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
ts :: [Name]
ts -> [(Name, Bool)]
-> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()
iPrintFunTypes [(Name, Bool)]
bnd Name
n ((Name -> (Name, Doc OutputAnnotation))
-> [Name] -> [(Name, Doc OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (\n :: Name
n -> (Name
n, IState -> Name -> Doc OutputAnnotation
pprintDelabTy IState
ist' Name
n)) [Name]
ts)
IState -> Idris ()
putIState IState
ist
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right Idris ()
action))
(\err :: Err
err -> do IState -> Idris ()
putIState IState
ist ; Err
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. Err -> Idris a
ierror Err
err)
checkType :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
checkType :: ElabState EState
-> [String]
-> PTerm
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
checkType e :: ElabState EState
e prf :: [String]
prf t :: PTerm
t = do
IState
ist <- Idris IState
getIState
Context
ctxt <- Idris Context
getContext
Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> (Err
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ())))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do
let OK env :: Env
env = ProofState -> TC Env
envAtFocus (ElabState EState -> ProofState
forall aux. ElabState aux -> ProofState
proof ElabState EState
e)
ctxt' :: Context
ctxt' = Env -> Context -> Context
forall (t :: * -> *) b.
Foldable t =>
t (Name, b, Binder Type) -> Context -> Context
envCtxt Env
env Context
ctxt
IState -> Idris ()
putIState IState
ist { tt_ctxt :: Context
tt_ctxt = Context
ctxt' }
(tm :: Type
tm, ty :: Type
ty) <- ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Type, Type)
elabVal (FC -> ElabInfo
recinfo FC
proverfc) ElabMode
ERHS PTerm
t
let ppo :: PPOption
ppo = IState -> PPOption
ppOptionIst IState
ist
infixes :: [FixDecl]
infixes = IState -> [FixDecl]
idris_infixes IState
ist
action :: Idris ()
action = case Type
tm of
TType _ ->
Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
iPrintTermWithType (PPOption -> PTerm -> Doc OutputAnnotation
prettyImp PPOption
ppo (FC -> PTerm
PType FC
emptyFC)) Doc OutputAnnotation
type1Doc
_ -> let bnd :: [(Name, Bool)]
bnd = ((Name, RigCount, Binder Type) -> (Name, Bool))
-> Env -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: (Name, RigCount, Binder Type)
x -> ((Name, RigCount, Binder Type) -> Name
forall a b c. (a, b, c) -> a
fstEnv (Name, RigCount, Binder Type)
x, Bool
False)) Env
env in
Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
iPrintTermWithType (PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppo [(Name, Bool)]
bnd [] [FixDecl]
infixes (IState -> Type -> PTerm
delab IState
ist Type
tm))
(PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppo [(Name, Bool)]
bnd [] [FixDecl]
infixes (IState -> Type -> PTerm
delab IState
ist Type
ty))
IState -> Idris ()
putIState IState
ist
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right Idris ()
action))
(\err :: Err
err -> do IState -> Idris ()
putIState IState
ist { tt_ctxt :: Context
tt_ctxt = Context
ctxt } ; Err
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. Err -> Idris a
ierror Err
err)
proverFC :: FC
proverFC = String -> (Int, Int) -> (Int, Int) -> FC
FC "(prover shell)" (0, 0) (0, 0)
evalTerm :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
evalTerm :: ElabState EState
-> [String]
-> PTerm
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
evalTerm e :: ElabState EState
e prf :: [String]
prf t :: PTerm
t = Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. Idris a -> Idris a
withErrorReflection (Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ())))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a b. (a -> b) -> a -> b
$
do Context
ctxt <- Idris Context
getContext
IState
ist <- Idris IState
getIState
Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> (Err
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ())))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do
let OK env :: Env
env = ProofState -> TC Env
envAtFocus (ElabState EState -> ProofState
forall aux. ElabState aux -> ProofState
proof ElabState EState
e)
ctxt' :: Context
ctxt' = Env -> Context -> Context
forall (t :: * -> *) b.
Foldable t =>
t (Name, b, Binder Type) -> Context -> Context
envCtxt Env
env Context
ctxt
ist' :: IState
ist' = IState
ist { tt_ctxt :: Context
tt_ctxt = Context
ctxt' }
bnd :: [(Name, Bool)]
bnd = ((Name, RigCount, Binder Type) -> (Name, Bool))
-> Env -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: (Name, RigCount, Binder Type)
x -> ((Name, RigCount, Binder Type) -> Name
forall a b c. (a, b, c) -> a
fstEnv (Name, RigCount, Binder Type)
x, Bool
False)) Env
env
IState -> Idris ()
putIState IState
ist'
(tm :: Type
tm, ty :: Type
ty) <- ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Type, Type)
elabVal (FC -> ElabInfo
recinfo FC
proverfc) ElabMode
ERHS PTerm
t
let tm' :: Type
tm' = Type -> Type
forall a. NFData a => a -> a
force (Context -> Env -> Type -> Type
normaliseAll Context
ctxt' Env
env Type
tm)
ty' :: Type
ty' = Type -> Type
forall a. NFData a => a -> a
force (Context -> Env -> Type -> Type
normaliseAll Context
ctxt' Env
env Type
ty)
ppo :: PPOption
ppo = IOption -> PPOption
ppOption (IState -> IOption
idris_options IState
ist')
infixes :: [FixDecl]
infixes = IState -> [FixDecl]
idris_infixes IState
ist
tmDoc :: Doc OutputAnnotation
tmDoc = PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppo [(Name, Bool)]
bnd [] [FixDecl]
infixes (IState -> Type -> PTerm
delab IState
ist' Type
tm')
tyDoc :: Doc OutputAnnotation
tyDoc = PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
ppo [(Name, Bool)]
bnd [] [FixDecl]
infixes (IState -> Type -> PTerm
delab IState
ist' Type
ty')
action :: Idris ()
action = Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
iPrintTermWithType Doc OutputAnnotation
tmDoc Doc OutputAnnotation
tyDoc
IState -> Idris ()
putIState IState
ist
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right Idris ()
action))
(\err :: Err
err -> do IState -> Idris ()
putIState IState
ist ; Err
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. Err -> Idris a
ierror Err
err)
docStr :: ElabState EState -> [String] -> Either Name Const -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
docStr :: ElabState EState
-> [String]
-> Either Name Const
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
docStr e :: ElabState EState
e prf :: [String]
prf (Left n :: Name
n) = do IState
ist <- Idris IState
getIState
Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> (Err
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ())))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (case Name
-> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
ist) of
[] -> (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf,
Err -> Either Err (Idris ())
forall a b. a -> Either a b
Left (Err -> Either Err (Idris ()))
-> (String -> Err) -> String -> Either Err (Idris ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Either Err (Idris ()))
-> String -> Either Err (Idris ())
forall a b. (a -> b) -> a -> b
$ "No documentation for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n)
ns :: [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ns -> do [Doc OutputAnnotation]
toShow <- ((Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation))
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> StateT IState (ExceptT Err IO) [Doc OutputAnnotation]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (IState
-> (Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
forall b.
IState
-> (Name, b)
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
showDoc IState
ist) [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ns
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf,
Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (Idris () -> Either Err (Idris ()))
-> Idris () -> Either Err (Idris ())
forall a b. (a -> b) -> a -> b
$ Doc OutputAnnotation -> Idris ()
iRenderResult ([Doc OutputAnnotation] -> Doc OutputAnnotation
forall a. [Doc a] -> Doc a
vsep [Doc OutputAnnotation]
toShow)))
(\err :: Err
err -> do IState -> Idris ()
putIState IState
ist ; Err
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. Err -> Idris a
ierror Err
err)
where showDoc :: IState
-> (Name, b)
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
showDoc ist :: IState
ist (n :: Name
n, d :: b
d) = do Docs
doc <- Name -> HowMuchDocs -> Idris Docs
getDocs Name
n HowMuchDocs
FullDocs
Doc OutputAnnotation
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc OutputAnnotation
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation))
-> Doc OutputAnnotation
-> StateT IState (ExceptT Err IO) (Doc OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ IState -> Docs -> Doc OutputAnnotation
pprintDocs IState
ist Docs
doc
docStr e :: ElabState EState
e prf :: [String]
prf (Right c :: Const
c) = do IState
ist <- Idris IState
getIState
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
(Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (Idris () -> Either Err (Idris ()))
-> (Doc OutputAnnotation -> Idris ())
-> Doc OutputAnnotation
-> Either Err (Idris ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc OutputAnnotation -> Idris ()
iRenderResult (Doc OutputAnnotation -> Either Err (Idris ()))
-> Doc OutputAnnotation -> Either Err (Idris ())
forall a b. (a -> b) -> a -> b
$ IState -> Const -> String -> Doc OutputAnnotation
pprintConstDocs IState
ist Const
c (Const -> String
constDocs Const
c))
search :: b -> d -> PTerm -> m (Bool, b, Bool, d, Either a (Idris ()))
search e :: b
e prf :: d
prf t :: PTerm
t = (Bool, b, Bool, d, Either a (Idris ()))
-> m (Bool, b, Bool, d, Either a (Idris ()))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, b
e, Bool
False, d
prf, Idris () -> Either a (Idris ())
forall a b. b -> Either a b
Right (Idris () -> Either a (Idris ()))
-> Idris () -> Either a (Idris ())
forall a b. (a -> b) -> a -> b
$ [PkgName] -> PTerm -> Idris ()
searchByType [] PTerm
t)