{-|
Module      : Idris.Prover
Description : Idris' theorem prover.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE PatternGuards #-}
module Idris.Prover (prover, showProof, showRunElab) where

-- Hack for GHC 7.10 and earlier compat without CPP or warnings
-- This exludes (<$>) as fmap, because wl-pprint uses it for newline
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
import Control.Monad.State.Strict
import System.Console.Haskeline
import System.Console.Haskeline.History
import System.IO (Handle, hPutStrLn, stdin, stdout)

-- | Launch the proof shell
prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()
prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()
prover ElabInfo
info Bool
mode Bool
lit Name
x =
           do Context
ctxt <- Idris Context
getContext
              IState
i <- Idris IState
getIState
              case Name -> Context -> [Term]
lookupTy Name
x Context
ctxt of
                  [Term
t] -> if Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> 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
-> Term
-> Idris ()
prove Bool
mode ElabInfo
info (IState -> Ctxt OptInfo
idris_optimisation IState
i) Context
ctxt Bool
lit Name
x Term
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]
++ String
" is not a hole"
                  [Term]
_ -> String -> Idris ()
forall a. String -> Idris a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No such hole"

showProof :: Bool -> Name -> [String] -> String
showProof :: Bool -> Name -> [String] -> String
showProof Bool
lit Name
n [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]
++ String
" = 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 (\String
x -> String
"  " 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]
++ String
"\n"
  where bird :: String
bird = if Bool
lit then String
"> " else String
""
        break :: String
break = String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bird

showRunElab :: Bool -> Name -> [String] -> String
showRunElab :: Bool -> Name -> [String] -> String
showRunElab Bool
lit Name
n [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 Float
1.0 Int
80 Doc Any
forall {a}. Doc a
doc) String
"")
  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 String
"=" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc a
forall a. String -> Doc a
text String
"%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 String
"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 -> 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 (StateT IState (ExceptT Err IO))
proverSettings ElabState EState
e = CompletionFunc (StateT IState (ExceptT Err IO))
-> Settings (StateT IState (ExceptT Err IO))
-> Settings (StateT IState (ExceptT Err IO))
forall (m :: * -> *). CompletionFunc m -> Settings m -> Settings m
setComplete ([String] -> CompletionFunc (StateT IState (ExceptT Err IO))
proverCompletion (ElabState EState -> [String]
assumptionNames ElabState EState
e)) Settings (StateT IState (ExceptT Err IO))
forall (m :: * -> *). MonadIO m => Settings m
defaultSettings

assumptionNames :: ElabState EState -> [String]
assumptionNames :: ElabState EState -> [String]
assumptionNames 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 -> [String]
forall {b} {c}. [(Name, b, c)] -> [String]
names Env
env
  where names :: [(Name, b, c)] -> [String]
names [] = []
        names ((MN Int
_ Text
_, b
_, c
_) : [(Name, b, c)]
bs) = [(Name, b, c)] -> [String]
names [(Name, b, c)]
bs
        names ((Name
n, b
_, c
_) : [(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
-> Term
-> Idris ()
prove Bool
mode ElabInfo
info Ctxt OptInfo
opt Context
ctxt Bool
lit Name
n Term
ty
    = do ProofState
ps <- (IState -> ProofState)
-> Idris IState -> StateT IState (ExceptT Err IO) ProofState
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\IState
ist -> Name
-> String -> Context -> Ctxt TypeInfo -> Int -> Term -> ProofState
initElaborator Name
n (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
ist) (IState -> Int
idris_name IState
ist) Term
ty) Idris IState
getIState
         String -> Name -> Idris ()
forall a. SExpable a => String -> a -> Idris ()
idemodePutSExp String
"start-proof-mode" Name
n
         (Term
tm, [String]
prf) <-
            if Bool
mode
              then ElabInfo
-> Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> [ElabShellHistory]
-> Maybe History
-> [(Name, Term, Term)]
-> StateT IState (ExceptT Err IO) (Term, [String])
elabloop ElabInfo
info Name
n Bool
True (String
"-" 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) String
"" 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
$ String
"Warning: this interactive prover is deprecated and will be removed " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                  String
"in a future release. Please see :elab for a similar feature that "String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                  String
"will replace it."
                      Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> Maybe History
-> StateT IState (ExceptT Err IO) (Term, [String])
ploop Name
n Bool
True (String
"-" 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) String
"" Maybe (ElabState EState)
forall a. Maybe a
Nothing) Maybe History
forall a. Maybe a
Nothing
         Int -> String -> Idris ()
logLvl Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Adding " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
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 Integer
_ Handle
_ -> String -> (Name, String) -> Idris ()
forall a. SExpable a => String -> a -> Idris ()
idemodePutSExp String
"end-proof-mode" (Name
n, Bool -> Name -> [String] -> String
shower Bool
lit Name
n [String]
prf)
           OutputMode
_            -> 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 = (n, (mode, prf)) : proofs })
         let tree :: ErasureInfo -> TC CaseDef
tree = Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(Term, Bool)]
-> [([Name], Term, Term)]
-> ErasureInfo
-> TC CaseDef
simpleCase Bool
False (Term -> SC
forall t. t -> SC' t
STerm Term
forall n. TT n
Erased) Bool
False Phase
CompileTime (String -> FC
fileFC String
"proof") [] [] [([], NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
ty, Term
tm)]
         Int -> String -> Idris ()
logLvl Int
3 ((ErasureInfo -> TC CaseDef) -> String
forall a. Show a => a -> String
show ErasureInfo -> TC CaseDef
tree)
         (Term
ptm, Term
pty) <- String
-> FC
-> (Err -> Err)
-> Env
-> Term
-> StateT IState (ExceptT Err IO) (Term, Term)
recheckC (ElabInfo -> String
constraintNS ElabInfo
info) (String -> FC
fileFC String
"proof") Err -> Err
forall a. a -> a
id [] Term
tm
         Int -> String -> Idris ()
logLvl Int
5 (String
"Proof type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
pty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                   String
"Expected type:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
ty)
         case Context -> Env -> Term -> Term -> TC ()
converts Context
ctxt [] Term
ty Term
pty of
              OK ()
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Error Err
e -> Err -> Idris ()
forall a. Err -> Idris a
ierror (Bool
-> (Term, Maybe Provenance)
-> (Term, Maybe Provenance)
-> Err
-> [(Name, Term)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
False (Term
ty, Maybe Provenance
forall a. Maybe a
Nothing) (Term
pty, Maybe Provenance
forall a. Maybe a
Nothing) Err
e [] Int
0)
         Term
ptm' <- Term -> Idris Term
forall term. Optimisable term => term -> Idris term
applyOpts Term
ptm
         ErasureInfo
ei <- IState -> ErasureInfo
getErasureInfo (IState -> ErasureInfo)
-> Idris IState -> StateT IState (ExceptT Err IO) ErasureInfo
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
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
-> [(Term, Bool)]
-> [Int]
-> [Either Term (Term, Term)]
-> [([Name], Term, Term)]
-> [([Name], Term, Term)]
-> Term
-> Context
-> TC Context
addCasedef Name
n ErasureInfo
ei (Bool -> Bool -> Bool -> CaseInfo
CaseInfo Bool
True Bool
True Bool
False) Bool
False (Term -> SC
forall t. t -> SC' t
STerm Term
forall n. TT n
Erased) Bool
True Bool
False
                                [] []  -- argtys, inaccArgs
                                [(Term, Term) -> Either Term (Term, Term)
forall a b. b -> Either a b
Right (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
ty, Term
ptm)]
                                [([], NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
ty, Term
ptm)]
                                [([], NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
ty, Term
ptm')] Term
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 Integer
n 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 String
"return" (String -> SExp
IdeMode.SymbolAtom String
"ok", String
"") Integer
n
           OutputMode
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep :: forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
st 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, Context
ctxt'), ES (ProofState
ps, est :: EState
est@EState{new_tyDecls :: EState -> [RDeclInstructions]
new_tyDecls = [RDeclInstructions]
declTodo}) String
x 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 a. a -> StateT IState (ExceptT Err IO) a
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 = []}) String
x Maybe (ElabState EState)
old)
        Error 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 Term
tm <- Elab' EState Term
forall aux. Elab' aux Term
get_term
                                  Context
ctxt <- Elab' EState Context
forall aux. Elab' aux Context
get_context
                                  TC (Term, Term) -> StateT (ElabState EState) TC (Term, Term)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState EState) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term) -> StateT (ElabState EState) TC (Term, Term))
-> TC (Term, Term) -> StateT (ElabState EState) TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt [] (Term -> Raw
forget Term
tm)
                                  (a, Context) -> StateT (ElabState EState) TC (a, Context)
forall a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
res, Context
ctxt)
                         ((Term
_,Term
_,Bool
_,Env
_,Err
e,[FailContext]
_,FailAt
_):Fails
_) -> TC (a, Context) -> StateT (ElabState EState) TC (a, Context)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState EState) m a
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, Term, Term)] -> ProofState -> Idris ()
dumpState IState
ist Bool
inElab [(Name, Term, Term)]
menv ProofState
ps | [] <- ProofState -> [Name]
holes ProofState
ps =
  do let nm :: Name
nm = ProofState -> Name
thname ProofState
ps
     SimpleDoc OutputAnnotation
rendered <- OutputDoc -> Idris (SimpleDoc OutputAnnotation)
forall a. Doc a -> Idris (SimpleDoc a)
iRender (OutputDoc -> Idris (SimpleDoc OutputAnnotation))
-> OutputDoc -> Idris (SimpleDoc OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> [(Name, Bool)] -> Name -> OutputDoc
prettyName Bool
True Bool
False [] Name
nm OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<> OutputDoc
forall {a}. Doc a
colon OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> String -> OutputDoc
forall a. String -> Doc a
text String
"No more goals."
     SimpleDoc OutputAnnotation -> Idris ()
iputGoal SimpleDoc OutputAnnotation
rendered
dumpState IState
ist Bool
inElab [(Name, Term, Term)]
menv ProofState
ps | (Name
h : [Name]
hs) <- ProofState -> [Name]
holes ProofState
ps = do
  let OK Binder Term
ty  = ProofState -> TC (Binder Term)
goalAtFocus ProofState
ps
      OK Env
env = ProofState -> TC Env
envAtFocus ProofState
ps
      state :: OutputDoc
state = [Name] -> OutputDoc
prettyOtherGoals [Name]
hs OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<> OutputDoc
forall {a}. Doc a
line OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<>
              Bool -> Binder Term -> Env -> OutputDoc
prettyAssumptions Bool
inElab Binder Term
ty Env
env OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<> OutputDoc
forall {a}. Doc a
line OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<>
              [(Name, Term, Term)] -> OutputDoc
prettyMetaValues ([(Name, Term, Term)] -> [(Name, Term, Term)]
forall a. [a] -> [a]
reverse [(Name, Term, Term)]
menv) OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<>
              [(Name, Bool)] -> Binder Term -> OutputDoc
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 Term
ty
  SimpleDoc OutputAnnotation
rendered <- OutputDoc -> Idris (SimpleDoc OutputAnnotation)
forall a. Doc a -> Idris (SimpleDoc a)
iRender OutputDoc
state
  SimpleDoc OutputAnnotation -> Idris ()
iputGoal SimpleDoc OutputAnnotation
rendered

  where
    (Name
h : [Name]
_) = ProofState -> [Name]
holes ProofState
ps -- apparently the pattern guards don't give us this

    ppo :: PPOption
ppo = IState -> PPOption
ppOptionIst IState
ist

    tPretty :: [(Name, Bool)] -> Term -> OutputDoc
tPretty [(Name, Bool)]
bnd Term
t = OutputAnnotation -> OutputDoc -> OutputDoc
forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm [(Name, Bool)]
bnd Term
t) (OutputDoc -> OutputDoc)
-> (PTerm -> OutputDoc) -> PTerm -> OutputDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                    PPOption
-> [(Name, Bool)] -> [Name] -> [FixDecl] -> PTerm -> OutputDoc
pprintPTerm PPOption
ppo [(Name, Bool)]
bnd [] (IState -> [FixDecl]
idris_infixes IState
ist) (PTerm -> OutputDoc) -> PTerm -> OutputDoc
forall a b. (a -> b) -> a -> b
$
                    IState -> Term -> PTerm
delab IState
ist Term
t

    assumptionNames :: Env -> [Name]
    assumptionNames :: Env -> [Name]
assumptionNames = ((Name, RigCount, Binder Term) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv

    prettyPs :: Bool -> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
    prettyPs :: Bool -> Binder Term -> [(Name, Bool)] -> Env -> OutputDoc
prettyPs Bool
all Binder Term
g [(Name, Bool)]
bnd [] = OutputDoc
forall {a}. Doc a
empty
    prettyPs Bool
all Binder Term
g [(Name, Bool)]
bnd ((n :: Name
n@(MN Int
_ Text
r), RigCount
_, Binder Term
_) : 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 String
"rewrite_rule" = Bool -> Binder Term -> [(Name, Bool)] -> Env -> OutputDoc
prettyPs Bool
all Binder Term
g ((Name
n, Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) Env
bs
    prettyPs Bool
all Binder Term
g [(Name, Bool)]
bnd ((n :: Name
n@(MN Int
_ Text
_), RigCount
_, Binder Term
_) : Env
bs)
        | Bool -> Bool
not (Bool
all Bool -> Bool -> Bool
|| Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> 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 a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Binder Term -> [Name]
forall {a}. Eq a => Binder (TT a) -> [a]
goalNames Binder Term
g) = Bool -> Binder Term -> [(Name, Bool)] -> Env -> OutputDoc
prettyPs Bool
all Binder Term
g [(Name, Bool)]
bnd Env
bs
    prettyPs Bool
all Binder Term
g [(Name, Bool)]
bnd ((Name
n, RigCount
_, Let RigCount
rig Term
t Term
v) : Env
bs) =
      OutputDoc
forall {a}. Doc a
line OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<> Name -> Bool -> OutputDoc
bindingOf Name
n Bool
False OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> String -> OutputDoc
forall a. String -> Doc a
text String
"=" OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> [(Name, Bool)] -> Term -> OutputDoc
tPretty [(Name, Bool)]
bnd Term
v OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> OutputDoc
forall {a}. Doc a
colon OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+>
        OutputDoc -> OutputDoc
forall a. Doc a -> Doc a
align ([(Name, Bool)] -> Term -> OutputDoc
tPretty [(Name, Bool)]
bnd Term
t) OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<> Bool -> Binder Term -> [(Name, Bool)] -> Env -> OutputDoc
prettyPs Bool
all Binder Term
g ((Name
n, Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) Env
bs
    prettyPs Bool
all Binder Term
g [(Name, Bool)]
bnd ((Name
n, RigCount
_, Binder Term
b) : Env
bs) =
      OutputDoc
forall {a}. Doc a
line OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<> Name -> Bool -> OutputDoc
bindingOf Name
n Bool
False OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> OutputDoc
forall {a}. Doc a
colon OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+>
      OutputDoc -> OutputDoc
forall a. Doc a -> Doc a
align ([(Name, Bool)] -> Term -> OutputDoc
tPretty [(Name, Bool)]
bnd (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b)) OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<> Bool -> Binder Term -> [(Name, Bool)] -> Env -> OutputDoc
prettyPs Bool
all Binder Term
g ((Name
n, Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) Env
bs

    prettyMetaValues :: [(Name, Term, Term)] -> OutputDoc
prettyMetaValues [] = OutputDoc
forall {a}. Doc a
empty
    prettyMetaValues [(Name, Term, Term)]
mvs =
      String -> OutputDoc
forall a. String -> Doc a
text String
"----------              Meta-values:               ----------" OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<$$>
      [(Name, Bool)] -> [(Name, Term, Term)] -> OutputDoc
prettyMetaValues' [] [(Name, Term, Term)]
mvs OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<> OutputDoc
forall {a}. Doc a
line OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<> OutputDoc
forall {a}. Doc a
line
    prettyMetaValues' :: [(Name, Bool)] -> [(Name, Term, Term)] -> OutputDoc
prettyMetaValues' [(Name, Bool)]
_   [] = OutputDoc
forall {a}. Doc a
empty
    prettyMetaValues' [(Name, Bool)]
bnd [(Name, Term, Term)
mv] = [(Name, Bool)] -> (Name, Term, Term) -> OutputDoc
ppMv [(Name, Bool)]
bnd (Name, Term, Term)
mv
    prettyMetaValues' [(Name, Bool)]
bnd ((mv :: (Name, Term, Term)
mv@(Name
n, Term
ty, Term
tm)) : [(Name, Term, Term)]
mvs) =
      [(Name, Bool)] -> (Name, Term, Term) -> OutputDoc
ppMv [(Name, Bool)]
bnd (Name, Term, Term)
mv OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<$>
      [(Name, Bool)] -> [(Name, Term, Term)] -> OutputDoc
prettyMetaValues' ((Name
n, Bool
False)(Name, Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) [(Name, Term, Term)]
mvs

    ppMv :: [(Name, Bool)] -> (Name, Term, Term) -> OutputDoc
ppMv [(Name, Bool)]
bnd (Name
n, Term
ty, Term
tm) = String -> OutputDoc
kwd String
"let" OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> Name -> Bool -> OutputDoc
bindingOf Name
n Bool
False OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> OutputDoc
forall {a}. Doc a
colon OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+>
                           [(Name, Bool)] -> Term -> OutputDoc
tPretty [(Name, Bool)]
bnd Term
ty OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> String -> OutputDoc
forall a. String -> Doc a
text String
"=" OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> [(Name, Bool)] -> Term -> OutputDoc
tPretty [(Name, Bool)]
bnd Term
tm

    kwd :: String -> OutputDoc
kwd = OutputAnnotation -> OutputDoc -> OutputDoc
forall a. a -> Doc a -> Doc a
annotate OutputAnnotation
AnnKeyword (OutputDoc -> OutputDoc)
-> (String -> OutputDoc) -> String -> OutputDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> OutputDoc
forall a. String -> Doc a
text

    goalNames :: Binder (TT a) -> [a]
goalNames (Guess TT a
t TT a
v) = TT a -> [a]
forall n. Eq n => TT n -> [n]
freeNames TT a
t [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ TT a -> [a]
forall n. Eq n => TT n -> [n]
freeNames TT a
v
    goalNames Binder (TT a)
b = TT a -> [a]
forall n. Eq n => TT n -> [n]
freeNames (Binder (TT a) -> TT a
forall b. Binder b -> b
binderTy Binder (TT a)
b)

    prettyG :: [(Name, Bool)] -> Binder Term -> OutputDoc
prettyG [(Name, Bool)]
bnd (Guess Term
t Term
v) = [(Name, Bool)] -> Term -> OutputDoc
tPretty [(Name, Bool)]
bnd Term
t OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> String -> OutputDoc
forall a. String -> Doc a
text String
"=?=" OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> [(Name, Bool)] -> Term -> OutputDoc
tPretty [(Name, Bool)]
bnd Term
v
    prettyG [(Name, Bool)]
bnd Binder Term
b = [(Name, Bool)] -> Term -> OutputDoc
tPretty [(Name, Bool)]
bnd (Term -> OutputDoc) -> Term -> OutputDoc
forall a b. (a -> b) -> a -> b
$ Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b

    prettyGoal :: [(Name, Bool)] -> Binder Term -> OutputDoc
prettyGoal [(Name, Bool)]
bnd Binder Term
ty =
      String -> OutputDoc
forall a. String -> Doc a
text String
"----------                 Goal:                  ----------" OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<$$>
      Name -> Bool -> OutputDoc
bindingOf Name
h Bool
False OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> OutputDoc
forall {a}. Doc a
colon OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a
align ([(Name, Bool)] -> Binder Term -> OutputDoc
prettyG [(Name, Bool)]
bnd Binder Term
ty)

    prettyAssumptions :: Bool -> Binder Term -> Env -> OutputDoc
prettyAssumptions Bool
inElab Binder Term
g Env
env =
      if Env -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Env
env then OutputDoc
forall {a}. Doc a
empty
      else
        String -> OutputDoc
forall a. String -> Doc a
text String
"----------              Assumptions:              ----------" OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<>
        Int -> OutputDoc -> OutputDoc
forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (Bool -> Binder Term -> [(Name, Bool)] -> Env -> OutputDoc
prettyPs Bool
inElab Binder Term
g [] (Env -> OutputDoc) -> Env -> OutputDoc
forall a b. (a -> b) -> a -> b
$ Env -> Env
forall a. [a] -> [a]
reverse Env
env)

    prettyOtherGoals :: [Name] -> OutputDoc
prettyOtherGoals [Name]
hs =
      if [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
hs then OutputDoc
forall {a}. Doc a
empty
      else
        String -> OutputDoc
forall a. String -> Doc a
text String
"----------              Other goals:              ----------" OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<$$>
        Int -> OutputDoc -> OutputDoc
forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (OutputDoc -> OutputDoc
forall a. Doc a -> Doc a
align (OutputDoc -> OutputDoc)
-> ([Name] -> OutputDoc) -> [Name] -> OutputDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OutputDoc] -> OutputDoc
forall a. [Doc a] -> Doc a
cat ([OutputDoc] -> OutputDoc)
-> ([Name] -> [OutputDoc]) -> [Name] -> OutputDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputDoc -> [OutputDoc] -> [OutputDoc]
forall a. Doc a -> [Doc a] -> [Doc a]
punctuate (String -> OutputDoc
forall a. String -> Doc a
text String
",") ([OutputDoc] -> [OutputDoc])
-> ([Name] -> [OutputDoc]) -> [Name] -> [OutputDoc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> OutputDoc) -> [Name] -> [OutputDoc]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Bool -> OutputDoc
`bindingOf` Bool
False) ([Name] -> OutputDoc) -> [Name] -> OutputDoc
forall a b. (a -> b) -> a -> b
$ [Name]
hs)

    freeEnvNames :: Env -> [Name]
    freeEnvNames :: Env -> [Name]
freeEnvNames = ((Name, RigCount, Binder Term) -> [Name]) -> Env -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Name
n, RigCount
_, Binder Term
b) -> Term -> [Name]
forall n. Eq n => TT n -> [n]
freeNames (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Term
b Term
forall n. TT n
Erased))

lifte :: ElabState EState -> ElabD a -> Idris a
lifte :: forall a. ElabState EState -> ElabD a -> Idris a
lifte ElabState EState
st ElabD a
e = do (a
v, ElabState EState
_) <- 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 a. a -> StateT IState (ExceptT Err IO) 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 Handle
h 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 -> StateT IState (ExceptT Err IO) Int
forall a. Err -> Idris a
ierror Err
err
       Right Int
n  -> Int -> StateT IState (ExceptT Err IO) Int
forall a. a -> StateT IState (ExceptT Err IO) a
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 String
""
     (SExp
sexp, Integer
id) <- case String -> Either Err (SExp, Integer)
IdeMode.parseMessage String
l of
                     Left Err
err -> Err -> StateT IState (ExceptT Err IO) (SExp, Integer)
forall a. Err -> Idris a
ierror Err
err
                     Right (SExp
sexp, Integer
id) -> (SExp, Integer) -> StateT IState (ExceptT Err IO) (SExp, Integer)
forall a. a -> StateT IState (ExceptT Err IO) a
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 = IdeMode id h }
     case SExp -> Maybe IdeModeCommand
IdeMode.sexpToCommand SExp
sexp of
       Just (IdeMode.REPLCompletions String
prefix) ->
         do (String
unused, [Completion]
compls) <- [String] -> CompletionFunc (StateT IState (ExceptT Err IO))
proverCompletion (ElabState EState -> [String]
assumptionNames ElabState EState
e) (String -> String
forall a. [a] -> [a]
reverse String
prefix, String
"")
            let good :: SExp
good = [SExp] -> SExp
IdeMode.SexpList [String -> SExp
IdeMode.SymbolAtom String
"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 String
"return" SExp
good
            Handle -> ElabState EState -> Idris (Maybe String)
receiveInput Handle
h ElabState EState
e
       Just (IdeMode.Interpret String
cmd) -> Maybe String -> Idris (Maybe String)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just String
cmd)
       Just (IdeMode.TypeOf String
str) -> Maybe String -> Idris (Maybe String)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just (String
":t " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str))
       Just (IdeMode.DocsFor String
str WhatDocs
_) -> Maybe String -> Idris (Maybe String)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe String
forall a. a -> Maybe a
Just (String
":doc " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str))
       Maybe IdeModeCommand
_ -> Maybe String -> Idris (Maybe String)
forall a. a -> StateT IState (ExceptT Err IO) a
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, Term, Term)]
-> ElabState EState
-> ElabShellHistory
-> Idris ([String], [(Name, Term, Term)], ElabState EState)
undoStep [String]
prf [(Name, Term, Term)]
env ElabState EState
st ElabShellHistory
ElabStep = do (()
_, 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, Term, Term)], ElabState EState)
-> Idris ([String], [(Name, Term, Term)], ElabState EState)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> [String]
forall a. HasCallStack => [a] -> [a]
init [String]
prf, [(Name, Term, Term)]
env, ElabState EState
st')
undoStep [String]
prf [(Name, Term, Term)]
env ElabState EState
st ElabShellHistory
LetStep = ([String], [(Name, Term, Term)], ElabState EState)
-> Idris ([String], [(Name, Term, Term)], ElabState EState)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> [String]
forall a. HasCallStack => [a] -> [a]
init [String]
prf, [(Name, Term, Term)] -> [(Name, Term, Term)]
forall a. HasCallStack => [a] -> [a]
tail [(Name, Term, Term)]
env, ElabState EState
st)
undoStep [String]
prf [(Name, Term, Term)]
env ElabState EState
st ElabShellHistory
BothStep = do (()
_, 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, Term, Term)], ElabState EState)
-> Idris ([String], [(Name, Term, Term)], ElabState EState)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> [String]
forall a. HasCallStack => [a] -> [a]
init [String]
prf, [(Name, Term, Term)] -> [(Name, Term, Term)]
forall a. HasCallStack => [a] -> [a]
tail [(Name, Term, Term)]
env, ElabState EState
st')

undoElab :: [String] -> [(Name, Type, Term)] -> ElabState EState -> [ElabShellHistory] -> Idris ([String], [(Name, Type, Term)], ElabState EState, [ElabShellHistory])
undoElab :: [String]
-> [(Name, Term, Term)]
-> ElabState EState
-> [ElabShellHistory]
-> Idris
     ([String], [(Name, Term, Term)], ElabState EState,
      [ElabShellHistory])
undoElab [String]
prf [(Name, Term, Term)]
env ElabState EState
st [] = String
-> Idris
     ([String], [(Name, Term, Term)], ElabState EState,
      [ElabShellHistory])
forall a. String -> Idris a
ifail String
"Nothing to undo"
undoElab [String]
prf [(Name, Term, Term)]
env ElabState EState
st (ElabShellHistory
h:[ElabShellHistory]
hs) = do ([String]
prf', [(Name, Term, Term)]
env', ElabState EState
st') <- [String]
-> [(Name, Term, Term)]
-> ElabState EState
-> ElabShellHistory
-> Idris ([String], [(Name, Term, Term)], ElabState EState)
undoStep [String]
prf [(Name, Term, Term)]
env ElabState EState
st ElabShellHistory
h
                                ([String], [(Name, Term, Term)], ElabState EState,
 [ElabShellHistory])
-> Idris
     ([String], [(Name, Term, Term)], ElabState EState,
      [ElabShellHistory])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([String]
prf', [(Name, Term, Term)]
env', ElabState EState
st', [ElabShellHistory]
hs)

proverfc :: FC
proverfc = String -> FC
fileFC String
"prover"

runWithInterrupt
  :: ElabState EState
  -> Idris a -- ^ run with SIGINT handler
  -> Idris b -- ^ run if mTry finished
  -> Idris b -- ^ run if mTry was interrupted
  -> Idris b
runWithInterrupt :: forall a b.
ElabState EState -> Idris a -> Idris b -> Idris b -> Idris b
runWithInterrupt ElabState EState
elabState Idris a
mTry Idris b
mSuccess Idris b
mFailure = do
  IState
ist <- Idris IState
getIState
  case IState -> OutputMode
idris_outputmode IState
ist of
    RawOutput Handle
_ -> do
      Bool
success <- Settings (StateT IState (ExceptT Err IO))
-> InputT (StateT IState (ExceptT Err IO)) Bool
-> StateT IState (ExceptT Err IO) Bool
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
Settings m -> InputT m a -> m a
runInputT (ElabState EState -> Settings (StateT IState (ExceptT Err IO))
proverSettings ElabState EState
elabState) (InputT (StateT IState (ExceptT Err IO)) Bool
 -> StateT IState (ExceptT Err IO) Bool)
-> InputT (StateT IState (ExceptT Err IO)) Bool
-> StateT IState (ExceptT Err IO) Bool
forall a b. (a -> b) -> a -> b
$
                   InputT (StateT IState (ExceptT Err IO)) Bool
-> InputT (StateT IState (ExceptT Err IO)) Bool
-> InputT (StateT IState (ExceptT Err IO)) Bool
forall (m :: * -> *) a. MonadMask m => m a -> m a -> m a
handleInterrupt (Bool -> InputT (StateT IState (ExceptT Err IO)) Bool
forall a. a -> InputT (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) (InputT (StateT IState (ExceptT Err IO)) Bool
 -> InputT (StateT IState (ExceptT Err IO)) Bool)
-> InputT (StateT IState (ExceptT Err IO)) Bool
-> InputT (StateT IState (ExceptT Err IO)) Bool
forall a b. (a -> b) -> a -> b
$
                   InputT (StateT IState (ExceptT Err IO)) Bool
-> InputT (StateT IState (ExceptT Err IO)) Bool
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
InputT m a -> InputT m a
withInterrupt (Idris a -> InputT (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => m a -> InputT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Idris a
mTry InputT (StateT IState (ExceptT Err IO)) a
-> InputT (StateT IState (ExceptT Err IO)) Bool
-> InputT (StateT IState (ExceptT Err IO)) Bool
forall a b.
InputT (StateT IState (ExceptT Err IO)) a
-> InputT (StateT IState (ExceptT Err IO)) b
-> InputT (StateT IState (ExceptT Err IO)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> InputT (StateT IState (ExceptT Err IO)) Bool
forall a. a -> InputT (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
      if Bool
success then Idris b
mSuccess else Idris b
mFailure
    IdeMode Integer
_ Handle
_ -> Idris a
mTry Idris a -> Idris b -> Idris b
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) 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, Term, Term)]
-> StateT IState (ExceptT Err IO) (Term, [String])
elabloop ElabInfo
info Name
fn Bool
d String
prompt [String]
prf ElabState EState
e [ElabShellHistory]
prev Maybe History
h [(Name, Term, Term)]
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, Term, Term)] -> ProofState -> Idris ()
dumpState IState
ist Bool
True [(Name, Term, Term)]
env (ElabState EState -> ProofState
forall aux. ElabState aux -> ProofState
proof ElabState EState
e)
       (Maybe String
x, Maybe History
h') <-
         case IState -> OutputMode
idris_outputmode IState
ist of
           RawOutput Handle
_ ->
             Settings (StateT IState (ExceptT Err IO))
-> InputT
     (StateT IState (ExceptT Err IO)) (Maybe String, Maybe History)
-> StateT IState (ExceptT Err IO) (Maybe String, Maybe History)
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
Settings m -> InputT m a -> m a
runInputT (ElabState EState -> Settings (StateT IState (ExceptT Err IO))
proverSettings ElabState EState
e) (InputT
   (StateT IState (ExceptT Err IO)) (Maybe String, Maybe History)
 -> StateT IState (ExceptT Err IO) (Maybe String, Maybe History))
-> InputT
     (StateT IState (ExceptT Err IO)) (Maybe String, Maybe History)
-> StateT IState (ExceptT Err IO) (Maybe String, Maybe History)
forall a b. (a -> b) -> a -> b
$
               do case Maybe History
h of
                    Just History
history -> History -> InputT (StateT IState (ExceptT Err IO)) ()
forall (m :: * -> *). MonadIO m => History -> InputT m ()
putHistory History
history
                    Maybe History
Nothing -> () -> InputT (StateT IState (ExceptT Err IO)) ()
forall a. a -> InputT (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  Maybe String
l <- InputT (StateT IState (ExceptT Err IO)) (Maybe String)
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
forall (m :: * -> *) a. MonadMask m => m a -> m a -> m a
handleInterrupt (Maybe String
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
forall a. a -> InputT (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
 -> InputT (StateT IState (ExceptT Err IO)) (Maybe String))
-> Maybe String
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"") (InputT (StateT IState (ExceptT Err IO)) (Maybe String)
 -> InputT (StateT IState (ExceptT Err IO)) (Maybe String))
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
forall a b. (a -> b) -> a -> b
$ InputT (StateT IState (ExceptT Err IO)) (Maybe String)
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
InputT m a -> InputT m a
withInterrupt (InputT (StateT IState (ExceptT Err IO)) (Maybe String)
 -> InputT (StateT IState (ExceptT Err IO)) (Maybe String))
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
forall (m :: * -> *).
(MonadIO m, MonadMask m) =>
String -> InputT m (Maybe String)
getInputLine (String
prompt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"> ")
                  History
h' <- InputT (StateT IState (ExceptT Err IO)) History
forall (m :: * -> *). MonadIO m => InputT m History
getHistory
                  (Maybe String, Maybe History)
-> InputT
     (StateT IState (ExceptT Err IO)) (Maybe String, Maybe History)
forall a. a -> InputT (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
l, History -> Maybe History
forall a. a -> Maybe a
Just History
h')
           IdeMode Integer
_ 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)
-> StateT IState (ExceptT Err IO) (Maybe String, Maybe History)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
i, Maybe History
h)
       (Either ParseError (Either ElabShellCmd PDo)
cmd, String
step) <- case Maybe String
x of
                        Maybe String
Nothing -> do String -> Idris ()
iPrintError String
"" ; String
-> StateT
     IState
     (ExceptT Err IO)
     (Either ParseError (Either ElabShellCmd PDo), String)
forall a. String -> Idris a
ifail String
"Abandoned"
                        Just String
input -> (Either ParseError (Either ElabShellCmd PDo), String)
-> StateT
     IState
     (ExceptT Err IO)
     (Either ParseError (Either ElabShellCmd PDo), String)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (IState -> String -> Either ParseError (Either ElabShellCmd PDo)
parseElabShellStep IState
ist String
input, String
input)

       -- if we're abandoning, it has to be outside the scope of the catch
       case Either ParseError (Either ElabShellCmd PDo)
cmd of
         Right (Left ElabShellCmd
EAbandon) -> do String -> Idris ()
iPrintError String
""; String -> Idris ()
forall a. String -> Idris a
ifail String
"Abandoned"
         Either ParseError (Either ElabShellCmd PDo)
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

       (Bool
d, [ElabShellHistory]
prev', ElabState EState
st, Bool
done, [String]
prf', [(Name, Term, Term)]
env', Either Err (Idris ())
res) <-
         Idris
  (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
   [(Name, Term, Term)], Either Err (Idris ()))
-> (Err
    -> Idris
         (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
          [(Name, Term, Term)], Either Err (Idris ())))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
           (case Either ParseError (Either ElabShellCmd PDo)
cmd of
              Left ParseError
err -> do
                Either Err (Idris ())
msg <- (OutputDoc -> Either Err (Idris ()))
-> StateT IState (ExceptT Err IO) OutputDoc
-> StateT IState (ExceptT Err IO) (Either Err (Idris ()))
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
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 ()))
-> (OutputDoc -> Err) -> OutputDoc -> Either Err (Idris ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Err) -> (OutputDoc -> String) -> OutputDoc -> Err
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputDoc -> String
forall a. Show a => a -> String
show) (ParseError -> StateT IState (ExceptT Err IO) OutputDoc
forall w.
Message w =>
w -> StateT IState (ExceptT Err IO) OutputDoc
formatMessage ParseError
err)
                (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
 [(Name, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf, [(Name, Term, Term)]
env, Either Err (Idris ())
msg)
              Right (Left ElabShellCmd
cmd') ->
                case ElabShellCmd
cmd' of
                  ElabShellCmd
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 a. [a] -> 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 String
"Incomplete proof"
                             String -> Idris ()
iputStrLn String
"Proof completed!"
                             (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
 [(Name, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [ElabShellHistory]
prev, ElabState EState
e, Bool
True, [String]
prf, [(Name, Term, Term)]
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 String
"")
                  ElabShellCmd
EUndo -> do ([String]
prf', [(Name, Term, Term)]
env', ElabState EState
st', [ElabShellHistory]
prev') <- [String]
-> [(Name, Term, Term)]
-> ElabState EState
-> [ElabShellHistory]
-> Idris
     ([String], [(Name, Term, Term)], ElabState EState,
      [ElabShellHistory])
undoElab [String]
prf [(Name, Term, Term)]
env ElabState EState
e [ElabShellHistory]
prev
                              (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
 [(Name, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [ElabShellHistory]
prev', ElabState EState
st', Bool
False, [String]
prf', [(Name, Term, Term)]
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 String
"")
                  ElabShellCmd
EAbandon ->
                    String
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. HasCallStack => String -> a
error String
"the impossible happened - should have been matched on outer scope"
                  ElabShellCmd
EProofState -> (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
 [(Name, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf, [(Name, Term, Term)]
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 String
"")
                  ElabShellCmd
EProofTerm ->
                    do Term
tm <- ElabState EState -> Elab' EState Term -> Idris Term
forall a. ElabState EState -> ElabD a -> Idris a
lifte ElabState EState
e Elab' EState Term
forall aux. Elab' aux Term
get_term
                       (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
 [(Name, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf, [(Name, Term, Term)]
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
$ OutputDoc -> Idris ()
iRenderResult (String -> OutputDoc
forall a. String -> Doc a
text String
"TT:" OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> [Name] -> Term -> OutputDoc
pprintTT [] Term
tm))
                  EEval PTerm
tm -> do (Bool
d', ElabState EState
st', Bool
done, [String]
prf', 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, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
d', [ElabShellHistory]
prev, ElabState EState
st', Bool
done, [String]
prf', [(Name, Term, Term)]
env, Either Err (Idris ())
go)
                  ECheck (PRef FC
_ [FC]
_ Name
n) ->
                    do (Bool
d', ElabState EState
st', Bool
done, [String]
prf', 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, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
d', [ElabShellHistory]
prev, ElabState EState
st', Bool
done, [String]
prf', [(Name, Term, Term)]
env, Either Err (Idris ())
go)
                  ECheck PTerm
tm -> do (Bool
d', ElabState EState
st', Bool
done, [String]
prf', 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, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
d', [ElabShellHistory]
prev, ElabState EState
st', Bool
done, [String]
prf', [(Name, Term, Term)]
env, Either Err (Idris ())
go)
                  ESearch PTerm
ty -> do (Bool
d', ElabState EState
st', Bool
done, [String]
prf', 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, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
d', [ElabShellHistory]
prev, ElabState EState
st', Bool
done, [String]
prf', [(Name, Term, Term)]
env, Either Err (Idris ())
go)
                  EDocStr Either Name Const
d -> do (Bool
d', ElabState EState
st', Bool
done, [String]
prf', 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, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
d', [ElabShellHistory]
prev, ElabState EState
st', Bool
done, [String]
prf', [(Name, Term, Term)]
env, Either Err (Idris ())
go)
              Right (Right PDo
cmd') ->
                case PDo
cmd' of
                  DoLetP  {} -> String
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. String -> Idris a
ifail String
"Pattern-matching let not supported here"
                  DoRewrite  {} -> String
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. String -> Idris a
ifail String
"Pattern-matching do-rewrite not supported here"
                  DoBindP {} -> String
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. String -> Idris a
ifail String
"Pattern-matching <- not supported here"
                  DoLet FC
fc RigCount
rig Name
i FC
ifc PTerm
Placeholder PTerm
expr ->
                    do (Term
tm, Term
ty) <- ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal (FC -> ElabInfo
recinfo FC
proverfc) ElabMode
ERHS (IState -> [(Name, Term, Term)] -> PTerm -> PTerm
inLets IState
ist [(Name, Term, Term)]
env PTerm
expr)
                       Context
ctxt <- Idris Context
getContext
                       let tm' :: Term
tm' = Context -> Env -> Term -> Term
normaliseAll Context
ctxt [] Term
tm
                           ty' :: Term
ty' = Context -> Env -> Term -> Term
normaliseAll Context
ctxt [] Term
ty
                       (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
 [(Name, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
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, Term
ty', Term
tm' ) (Name, Term, Term) -> [(Name, Term, Term)] -> [(Name, Term, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term, Term)]
env, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (String -> Idris ()
iPrintResult String
""))
                  DoLet FC
fc RigCount
rig Name
i FC
ifc PTerm
ty PTerm
expr ->
                    do (Term
tm, Term
ty) <- ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
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 String
"the"))
                                                [ PTerm -> PArg
forall {t}. t -> PArg' t
pexp (IState -> [(Name, Term, Term)] -> PTerm -> PTerm
inLets IState
ist [(Name, Term, Term)]
env PTerm
ty)
                                                , PTerm -> PArg
forall {t}. t -> PArg' t
pexp (IState -> [(Name, Term, Term)] -> PTerm -> PTerm
inLets IState
ist [(Name, Term, Term)]
env PTerm
expr)
                                                ])
                       Context
ctxt <- Idris Context
getContext
                       let tm' :: Term
tm' = Context -> Env -> Term -> Term
normaliseAll Context
ctxt [] Term
tm
                           ty' :: Term
ty' = Context -> Env -> Term -> Term
normaliseAll Context
ctxt [] Term
ty
                       (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
 [(Name, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
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, Term
ty', Term
tm' ) (Name, Term, Term) -> [(Name, Term, Term)] -> [(Name, Term, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term, Term)]
env, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (String -> Idris ()
iPrintResult String
""))
                  DoBind FC
fc Name
i FC
ifc PTerm
expr ->
                    do (Term
tm, Term
ty) <- ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal (FC -> ElabInfo
recinfo FC
proverfc) ElabMode
ERHS (IState -> [(Name, Term, Term)] -> PTerm -> PTerm
inLets IState
ist [(Name, Term, Term)]
env PTerm
expr)
                       (()
_, 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 -- enable :undo
                       (Term
res, ElabState EState
e'') <- ElabState EState
-> Elab' EState Term -> Idris (Term, ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e' (Elab' EState Term -> Idris (Term, ElabState EState))
-> Elab' EState Term -> Idris (Term, ElabState EState)
forall a b. (a -> b) -> a -> b
$
                                       ElabInfo
-> IState -> FC -> Env -> Term -> [String] -> Elab' EState Term
runElabAction ElabInfo
info IState
ist FC
NoFC [] Term
tm [String
"Shell"]
                       Context
ctxt <- Idris Context
getContext
                       (Term
v, Term
vty) <- TC (Term, Term) -> StateT IState (ExceptT Err IO) (Term, Term)
forall a. TC a -> Idris a
tclift (TC (Term, Term) -> StateT IState (ExceptT Err IO) (Term, Term))
-> TC (Term, Term) -> StateT IState (ExceptT Err IO) (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt [] (Term -> Raw
forget Term
res)
                       let v' :: Term
v'   = Context -> Env -> Term -> Term
normaliseAll Context
ctxt [] Term
v
                           vty' :: Term
vty' = Context -> Env -> Term -> Term
normaliseAll Context
ctxt [] Term
vty
                       (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
 [(Name, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
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, Term
vty', Term
v') (Name, Term, Term) -> [(Name, Term, Term)] -> [(Name, Term, Term)]
forall a. a -> [a] -> [a]
: [(Name, Term, Term)]
env, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (String -> Idris ()
iPrintResult String
""))
                  DoExp FC
fc PTerm
expr ->
                    do (Term
tm, Term
ty) <- ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal (FC -> ElabInfo
recinfo FC
proverfc) ElabMode
ERHS (IState -> [(Name, Term, Term)] -> PTerm -> PTerm
inLets IState
ist [(Name, Term, Term)]
env PTerm
expr)
                       -- TODO: call elaborator with Elab () as goal here
                       (()
_, 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 -- enable :undo
                       (Term
_, ElabState EState
e'') <- ElabState EState
-> Elab' EState Term -> Idris (Term, ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e' (Elab' EState Term -> Idris (Term, ElabState EState))
-> Elab' EState Term -> Idris (Term, ElabState EState)
forall a b. (a -> b) -> a -> b
$
                                     ElabInfo
-> IState -> FC -> Env -> Term -> [String] -> Elab' EState Term
runElabAction ElabInfo
info IState
ist FC
NoFC [] Term
tm [String
"Shell"]
                       (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
 [(Name, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
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, Term, Term)]
env, Idris () -> Either Err (Idris ())
forall a b. b -> Either a b
Right (String -> Idris ()
iPrintResult String
"")))
           (\Err
err -> (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
 [(Name, Term, Term)], Either Err (Idris ()))
-> Idris
     (Bool, [ElabShellHistory], ElabState EState, Bool, [String],
      [(Name, Term, Term)], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf, [(Name, Term, Term)]
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 String
"write-proof-state" ([String]
prf', [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
prf')
       case Either Err (Idris ())
res of
         Left Err
err -> do IState
ist <- Idris IState
getIState
                        OutputDoc -> Idris ()
iRenderError (OutputDoc -> Idris ()) -> OutputDoc -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState -> Err -> OutputDoc
pprintErr IState
ist Err
err
                        ElabInfo
-> Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> [ElabShellHistory]
-> Maybe History
-> [(Name, Term, Term)]
-> StateT IState (ExceptT Err IO) (Term, [String])
elabloop ElabInfo
info Name
fn Bool
d String
prompt [String]
prf' ElabState EState
st [ElabShellHistory]
prev' Maybe History
h' [(Name, Term, Term)]
env'
         Right Idris ()
ok ->
           if Bool
done then do (Term
tm, ElabState EState
_) <- ElabState EState
-> Elab' EState Term -> Idris (Term, ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
st Elab' EState Term
forall aux. Elab' aux Term
get_term
                           (Term, [String]) -> StateT IState (ExceptT Err IO) (Term, [String])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
tm, [String]
prf')
                   else ElabState EState
-> Idris ()
-> StateT IState (ExceptT Err IO) (Term, [String])
-> StateT IState (ExceptT Err IO) (Term, [String])
-> StateT IState (ExceptT Err IO) (Term, [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, Term, Term)]
-> StateT IState (ExceptT Err IO) (Term, [String])
elabloop ElabInfo
info Name
fn Bool
d String
prompt [String]
prf' ElabState EState
st [ElabShellHistory]
prev' Maybe History
h' [(Name, Term, Term)]
env')
                           (ElabInfo
-> Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> [ElabShellHistory]
-> Maybe History
-> [(Name, Term, Term)]
-> StateT IState (ExceptT Err IO) (Term, [String])
elabloop ElabInfo
info Name
fn Bool
d String
prompt [String]
prf ElabState EState
e [ElabShellHistory]
prev Maybe History
h' [(Name, Term, Term)]
env)

  where
    -- A bit of a hack: wrap the value up in a let binding, which will
    -- normalise away. It would be better to figure out how to call
    -- the elaborator with a custom environment here to avoid the
    -- delab step.
    inLets :: IState -> [(Name, Type, Term)] -> PTerm -> PTerm
    inLets :: IState -> [(Name, Term, Term)] -> PTerm -> PTerm
inLets IState
ist [(Name, Term, Term)]
lets PTerm
tm = ((Name, Term, Term) -> PTerm -> PTerm)
-> PTerm -> [(Name, Term, Term)] -> PTerm
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Name
n, Term
ty, Term
v) PTerm
b -> FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
NoFC RigCount
RigW Name
n FC
NoFC (IState -> Term -> PTerm
delab IState
ist Term
ty) (IState -> Term -> PTerm
delab IState
ist Term
v) PTerm
b) PTerm
tm ([(Name, Term, Term)] -> [(Name, Term, Term)]
forall a. [a] -> [a]
reverse [(Name, Term, Term)]
lets)



ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])
ploop :: Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> Maybe History
-> StateT IState (ExceptT Err IO) (Term, [String])
ploop Name
fn Bool
d String
prompt [String]
prf ElabState EState
e 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, Term, Term)] -> ProofState -> Idris ()
dumpState IState
i Bool
False [] (ElabState EState -> ProofState
forall aux. ElabState aux -> ProofState
proof ElabState EState
e)
         (Maybe String
x, Maybe History
h') <-
           case IState -> OutputMode
idris_outputmode IState
i of
             RawOutput Handle
_ ->
               Settings (StateT IState (ExceptT Err IO))
-> InputT
     (StateT IState (ExceptT Err IO)) (Maybe String, Maybe History)
-> StateT IState (ExceptT Err IO) (Maybe String, Maybe History)
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
Settings m -> InputT m a -> m a
runInputT (ElabState EState -> Settings (StateT IState (ExceptT Err IO))
proverSettings ElabState EState
e) (InputT
   (StateT IState (ExceptT Err IO)) (Maybe String, Maybe History)
 -> StateT IState (ExceptT Err IO) (Maybe String, Maybe History))
-> InputT
     (StateT IState (ExceptT Err IO)) (Maybe String, Maybe History)
-> StateT IState (ExceptT Err IO) (Maybe String, Maybe History)
forall a b. (a -> b) -> a -> b
$
                 -- Manually track the history so that we can use the proof state
                 do case Maybe History
h of
                      Just History
history -> History -> InputT (StateT IState (ExceptT Err IO)) ()
forall (m :: * -> *). MonadIO m => History -> InputT m ()
putHistory History
history
                      Maybe History
Nothing -> () -> InputT (StateT IState (ExceptT Err IO)) ()
forall a. a -> InputT (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                    Maybe String
l <- InputT (StateT IState (ExceptT Err IO)) (Maybe String)
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
forall (m :: * -> *) a. MonadMask m => m a -> m a -> m a
handleInterrupt (Maybe String
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
forall a. a -> InputT (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
 -> InputT (StateT IState (ExceptT Err IO)) (Maybe String))
-> Maybe String
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"") (InputT (StateT IState (ExceptT Err IO)) (Maybe String)
 -> InputT (StateT IState (ExceptT Err IO)) (Maybe String))
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
forall a b. (a -> b) -> a -> b
$ InputT (StateT IState (ExceptT Err IO)) (Maybe String)
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
InputT m a -> InputT m a
withInterrupt (InputT (StateT IState (ExceptT Err IO)) (Maybe String)
 -> InputT (StateT IState (ExceptT Err IO)) (Maybe String))
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
-> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> InputT (StateT IState (ExceptT Err IO)) (Maybe String)
forall (m :: * -> *).
(MonadIO m, MonadMask m) =>
String -> InputT m (Maybe String)
getInputLine (String
prompt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"> ")
                    History
h' <- InputT (StateT IState (ExceptT Err IO)) History
forall (m :: * -> *). MonadIO m => InputT m History
getHistory
                    (Maybe String, Maybe History)
-> InputT
     (StateT IState (ExceptT Err IO)) (Maybe String, Maybe History)
forall a. a -> InputT (StateT IState (ExceptT Err IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
l, History -> Maybe History
forall a. a -> Maybe a
Just History
h')
             IdeMode Integer
_ 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)
-> StateT IState (ExceptT Err IO) (Maybe String, Maybe History)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
i, Maybe History
h)
         (Either ParseError PTactic
cmd, String
step) <- case Maybe String
x of
            Maybe String
Nothing -> do String -> Idris ()
iPrintError String
""; String
-> StateT
     IState (ExceptT Err IO) (Either ParseError PTactic, String)
forall a. String -> Idris a
ifail String
"Abandoned"
            Just String
input -> (Either ParseError PTactic, String)
-> StateT
     IState (ExceptT Err IO) (Either ParseError PTactic, String)
forall a. a -> StateT IState (ExceptT Err IO) a
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 PTactic
Abandon -> do String -> Idris ()
iPrintError String
""; String -> Idris ()
forall a. String -> Idris a
ifail String
"Abandoned"
            Either ParseError PTactic
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         (Bool
d, ElabState EState
st, Bool
done, [String]
prf', 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 ParseError
err -> do
                Either Err (Idris ())
msg <- (OutputDoc -> Either Err (Idris ()))
-> StateT IState (ExceptT Err IO) OutputDoc
-> StateT IState (ExceptT Err IO) (Either Err (Idris ()))
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
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 ()))
-> (OutputDoc -> Err) -> OutputDoc -> Either Err (Idris ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Err) -> (OutputDoc -> String) -> OutputDoc -> Err
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputDoc -> String
forall a. Show a => a -> String
show) (ParseError -> StateT IState (ExceptT Err IO) OutputDoc
forall w.
Message w =>
w -> StateT IState (ExceptT Err IO) OutputDoc
formatMessage ParseError
err)
                (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
     (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf, Either Err (Idris ())
msg)
              Right PTactic
Undo -> do (()
_, 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 a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabState EState
st, Bool
False, [String] -> [String]
forall a. HasCallStack => [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 String
"")
              Right PTactic
ProofState -> (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
     (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
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 String
"")
              Right PTactic
ProofTerm -> do Term
tm <- ElabState EState -> Elab' EState Term -> Idris Term
forall a. ElabState EState -> ElabD a -> Idris a
lifte ElabState EState
e Elab' EState Term
forall aux. Elab' aux Term
get_term
                                    String -> Idris ()
iputStrLn (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"TT: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
                                    (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
     (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
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 String
"")
              Right PTactic
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 a. [a] -> 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 String
"Incomplete proof"
                              String -> Idris ()
iputStrLn String
"Proof completed!"
                              (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
     (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
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 String
"")
              Right (TCheck (PRef FC
_ [FC]
_ 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 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 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 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 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 PTactic
tac ->
                do (()
_, 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
                   (()
_, 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 a. a -> StateT IState (ExceptT Err IO) a
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 String
""))
           (\Err
err -> (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
     (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
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 String
"write-proof-state" ([String]
prf', [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
prf')
         case Either Err (Idris ())
res of
           Left Err
err -> do IState
ist <- Idris IState
getIState
                          OutputDoc -> Idris ()
iRenderError (OutputDoc -> Idris ()) -> OutputDoc -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState -> Err -> OutputDoc
pprintErr IState
ist Err
err
                          Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> Maybe History
-> StateT IState (ExceptT Err IO) (Term, [String])
ploop Name
fn Bool
d String
prompt [String]
prf' ElabState EState
st Maybe History
h'
           Right Idris ()
ok ->
             if Bool
done then do (Term
tm, ElabState EState
_) <- ElabState EState
-> Elab' EState Term -> Idris (Term, ElabState EState)
forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
st Elab' EState Term
forall aux. Elab' aux Term
get_term
                             (Term, [String]) -> StateT IState (ExceptT Err IO) (Term, [String])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
tm, [String]
prf')
                     else ElabState EState
-> Idris ()
-> StateT IState (ExceptT Err IO) (Term, [String])
-> StateT IState (ExceptT Err IO) (Term, [String])
-> StateT IState (ExceptT Err IO) (Term, [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
-> StateT IState (ExceptT Err IO) (Term, [String])
ploop Name
fn Bool
d String
prompt [String]
prf' ElabState EState
st Maybe History
h')
                             (Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> Maybe History
-> StateT IState (ExceptT Err IO) (Term, [String])
ploop Name
fn Bool
d String
prompt [String]
prf ElabState EState
e Maybe History
h')


envCtxt :: t (Name, b, Binder Term) -> Context -> Context
envCtxt t (Name, b, Binder Term)
env Context
ctxt = (Context -> (Name, b, Binder Term) -> Context)
-> Context -> t (Name, b, Binder Term) -> Context
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Context
c (Name
n, b
_, Binder Term
b) -> Name -> NameType -> Term -> Context -> Context
addTyDecl Name
n NameType
Bound (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b) Context
c) Context
ctxt t (Name, b, Binder Term)
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 ElabState EState
e [String]
prf Name
n = do
    Context
ctxt <- Idris Context
getContext
    IState
ist <- Idris IState
getIState
    Bool
imp <- StateT IState (ExceptT Err IO) 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 = 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 Term) -> Context -> Context
envCtxt Env
env Context
ctxt
            bnd :: [(Name, Bool)]
bnd    = ((Name, RigCount, Binder Term) -> (Name, Bool))
-> Env -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name, RigCount, Binder Term)
x -> ((Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv (Name, RigCount, Binder Term)
x, Bool
False)) Env
env
            ist' :: IState
ist'   = IState
ist { tt_ctxt = ctxt' }
        IState -> Idris ()
putIState IState
ist'
        -- Unlike the REPL, metavars have no special treatment, to
        -- make it easier to see how to prove with them.
        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
$ String
"No such variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
                       [Name]
ts -> [(Name, Bool)] -> Name -> [(Name, OutputDoc)] -> Idris ()
iPrintFunTypes [(Name, Bool)]
bnd Name
n ((Name -> (Name, OutputDoc)) -> [Name] -> [(Name, OutputDoc)]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, IState -> Name -> OutputDoc
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 a. a -> StateT IState (ExceptT Err IO) a
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 -> 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 ElabState EState
e [String]
prf 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 = 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 Term) -> Context -> Context
envCtxt Env
env Context
ctxt
        IState -> Idris ()
putIState IState
ist { tt_ctxt = ctxt' }
        (Term
tm, Term
ty) <- ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
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 Term
tm of
              TType UExp
_ ->
                OutputDoc -> OutputDoc -> Idris ()
iPrintTermWithType (PPOption -> PTerm -> OutputDoc
prettyImp PPOption
ppo (FC -> PTerm
PType FC
emptyFC)) OutputDoc
type1Doc
              Term
_ -> let bnd :: [(Name, Bool)]
bnd = ((Name, RigCount, Binder Term) -> (Name, Bool))
-> Env -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name, RigCount, Binder Term)
x -> ((Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv (Name, RigCount, Binder Term)
x, Bool
False)) Env
env in
                   OutputDoc -> OutputDoc -> Idris ()
iPrintTermWithType (PPOption
-> [(Name, Bool)] -> [Name] -> [FixDecl] -> PTerm -> OutputDoc
pprintPTerm PPOption
ppo [(Name, Bool)]
bnd [] [FixDecl]
infixes (IState -> Term -> PTerm
delab IState
ist Term
tm))
                                       (PPOption
-> [(Name, Bool)] -> [Name] -> [FixDecl] -> PTerm -> OutputDoc
pprintPTerm PPOption
ppo [(Name, Bool)]
bnd [] [FixDecl]
infixes (IState -> Term -> PTerm
delab IState
ist Term
ty))
        IState -> Idris ()
putIState IState
ist
        (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
     (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
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 -> do IState -> Idris ()
putIState IState
ist { tt_ctxt = 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 String
"(prover shell)" (Int
0, Int
0) (Int
0, Int
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 ElabState EState
e [String]
prf 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 = 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 Term) -> Context -> Context
envCtxt Env
env Context
ctxt
             ist' :: IState
ist'   = IState
ist { tt_ctxt = ctxt' }
             bnd :: [(Name, Bool)]
bnd    = ((Name, RigCount, Binder Term) -> (Name, Bool))
-> Env -> [(Name, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name, RigCount, Binder Term)
x -> ((Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv (Name, RigCount, Binder Term)
x, Bool
False)) Env
env
         IState -> Idris ()
putIState IState
ist'
         (Term
tm, Term
ty) <- ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal (FC -> ElabInfo
recinfo FC
proverfc) ElabMode
ERHS PTerm
t
         let tm' :: Term
tm'     = Term -> Term
forall a. NFData a => a -> a
force (Context -> Env -> Term -> Term
normaliseAll Context
ctxt' Env
env Term
tm)
             ty' :: Term
ty'     = Term -> Term
forall a. NFData a => a -> a
force (Context -> Env -> Term -> Term
normaliseAll Context
ctxt' Env
env Term
ty)
             ppo :: PPOption
ppo     = IOption -> PPOption
ppOption (IState -> IOption
idris_options IState
ist')
             infixes :: [FixDecl]
infixes = IState -> [FixDecl]
idris_infixes IState
ist
             tmDoc :: OutputDoc
tmDoc   = PPOption
-> [(Name, Bool)] -> [Name] -> [FixDecl] -> PTerm -> OutputDoc
pprintPTerm PPOption
ppo [(Name, Bool)]
bnd [] [FixDecl]
infixes (IState -> Term -> PTerm
delab IState
ist' Term
tm')
             tyDoc :: OutputDoc
tyDoc   = PPOption
-> [(Name, Bool)] -> [Name] -> [FixDecl] -> PTerm -> OutputDoc
pprintPTerm PPOption
ppo [(Name, Bool)]
bnd [] [FixDecl]
infixes (IState -> Term -> PTerm
delab IState
ist' Term
ty')
             action :: Idris ()
action  = OutputDoc -> OutputDoc -> Idris ()
iPrintTermWithType OutputDoc
tmDoc OutputDoc
tyDoc
         IState -> Idris ()
putIState IState
ist
         (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
-> Idris
     (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
forall a. a -> StateT IState (ExceptT Err IO) a
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 -> 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 ElabState EState
e [String]
prf (Left 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 a. a -> StateT IState (ExceptT Err IO) a
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
$ String
"No documentation for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n)
                                         [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ns -> do [OutputDoc]
toShow <- ((Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))
 -> StateT IState (ExceptT Err IO) OutputDoc)
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> StateT IState (ExceptT Err IO) [OutputDoc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (IState
-> (Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))
-> StateT IState (ExceptT Err IO) OutputDoc
forall {b}.
IState -> (Name, b) -> StateT IState (ExceptT Err IO) OutputDoc
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 a. a -> StateT IState (ExceptT Err IO) a
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
$ OutputDoc -> Idris ()
iRenderResult ([OutputDoc] -> OutputDoc
forall a. [Doc a] -> Doc a
vsep [OutputDoc]
toShow)))
                                      (\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) OutputDoc
showDoc IState
ist (Name
n, b
d) = do Docs
doc <- Name -> HowMuchDocs -> Idris Docs
getDocs Name
n HowMuchDocs
FullDocs
                                       OutputDoc -> StateT IState (ExceptT Err IO) OutputDoc
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (OutputDoc -> StateT IState (ExceptT Err IO) OutputDoc)
-> OutputDoc -> StateT IState (ExceptT Err IO) OutputDoc
forall a b. (a -> b) -> a -> b
$ IState -> Docs -> OutputDoc
pprintDocs IState
ist Docs
doc
docStr ElabState EState
e [String]
prf (Right 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 a. a -> StateT IState (ExceptT Err IO) a
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 ()))
-> (OutputDoc -> Idris ()) -> OutputDoc -> Either Err (Idris ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputDoc -> Idris ()
iRenderResult (OutputDoc -> Either Err (Idris ()))
-> OutputDoc -> Either Err (Idris ())
forall a b. (a -> b) -> a -> b
$ IState -> Const -> String -> OutputDoc
pprintConstDocs IState
ist Const
c (Const -> String
constDocs Const
c))
search :: b -> d -> PTerm -> m (Bool, b, Bool, d, Either a (Idris ()))
search b
e d
prf PTerm
t = (Bool, b, Bool, d, Either a (Idris ()))
-> m (Bool, b, Bool, d, Either a (Idris ()))
forall a. a -> m a
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)