{-|
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.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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Name
x (forall a b. (a -> b) -> [a] -> [b]
map 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 forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Name
x forall a. [a] -> [a] -> [a]
++ String
" is not a hole"
                  [Term]
_ -> 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 forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" = proof" forall a. [a] -> [a] -> [a]
++ String
break forall a. [a] -> [a] -> [a]
++
             String -> [String] -> String
showSep String
break (forall a b. (a -> b) -> [a] -> [b]
map (\String
x -> String
"  " forall a. [a] -> [a] -> [a]
++ String
x) [String]
ps) forall a. [a] -> [a] -> [a]
++
                     String
break forall a. [a] -> [a] -> [a]
++ String
"\n"
  where bird :: String
bird = if Bool
lit then String
"> " else String
""
        break :: String
break = String
"\n" 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 (forall a. SimpleDoc a -> String -> String
displayS (forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
80 forall {a}. Doc a
doc) String
"")
  where doc :: Doc a
doc = forall a. String -> Doc a
text (forall a. Show a => a -> String
show Name
n) forall a. Doc a -> Doc a -> Doc a
<+> forall a. String -> Doc a
text String
"=" forall a. Doc a -> Doc a -> Doc a
<+> forall a. String -> Doc a
text String
"%runElab" forall a. Doc a -> Doc a -> Doc a
<+>
              forall a. Doc a -> Doc a -> Doc a -> Doc a
enclose forall {a}. Doc a
lparen forall {a}. Doc a
rparen
                (forall a. String -> Doc a
text String
"do" forall a. Doc a -> Doc a -> Doc a
<+> (forall a. Doc a -> Doc a
align forall a b. (a -> b) -> a -> b
$ forall a. [Doc a] -> Doc a
vsep (forall a b. (a -> b) -> [a] -> [b]
map forall a. String -> Doc a
text [String]
ps)))
        birdify :: String -> String
birdify = if Bool
lit
                     then forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String
"> " forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines
                     else forall a. a -> a
id

proverSettings :: ElabState EState -> Settings Idris
proverSettings :: ElabState EState -> Settings (StateT IState (ExceptT Err IO))
proverSettings ElabState EState
e = forall (m :: * -> *). CompletionFunc m -> Settings m -> Settings m
setComplete ([String] -> CompletionFunc (StateT IState (ExceptT Err IO))
proverCompletion (ElabState EState -> [String]
assumptionNames ElabState EState
e)) forall (m :: * -> *). MonadIO m => Settings m
defaultSettings

assumptionNames :: ElabState EState -> [String]
assumptionNames :: ElabState EState -> [String]
assumptionNames ElabState EState
e
  = case ProofState -> TC Env
envAtFocus (forall aux. ElabState aux -> ProofState
proof ElabState EState
e) of
         OK Env
env -> 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) = forall a. Show a => a -> String
show Name
n 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 <- 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
         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)]
-> Idris (Term, [String])
elabloop ElabInfo
info Name
n Bool
True (String
"-" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n) [] (forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
ps, EState
initEState) String
"" forall a. Maybe a
Nothing) [] forall a. Maybe a
Nothing []
              else do String -> Idris ()
iputStrLn forall a b. (a -> b) -> a -> b
$ String
"Warning: this interactive prover is deprecated and will be removed " forall a. [a] -> [a] -> [a]
++
                                  String
"in a future release. Please see :elab for a similar feature that "forall a. [a] -> [a] -> [a]
++
                                  String
"will replace it."
                      Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> Maybe History
-> Idris (Term, [String])
ploop Name
n Bool
True (String
"-" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n) [] (forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
ps, EState
initEState) String
"" forall a. Maybe a
Nothing) forall a. Maybe a
Nothing
         Int -> String -> Idris ()
logLvl Int
1 forall a b. (a -> b) -> a -> b
$ String
"Adding " forall a. [a] -> [a] -> [a]
++ 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
_ -> 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 forall a b. (a -> b) -> a -> b
$ Bool -> Name -> [String] -> String
shower Bool
lit Name
n [String]
prf
         let proofs :: [(Name, (Bool, [String]))]
proofs = IState -> [(Name, (Bool, [String]))]
proof_list IState
i
         IState -> Idris ()
putIState (IState
i { proof_list :: [(Name, (Bool, [String]))]
proof_list = (Name
n, (Bool
mode, [String]
prf)) forall a. a -> [a] -> [a]
: [(Name, (Bool, [String]))]
proofs })
         let tree :: ErasureInfo -> TC CaseDef
tree = Bool
-> SC
-> Bool
-> Phase
-> FC
-> [Int]
-> [(Term, Bool)]
-> [([Name], Term, Term)]
-> ErasureInfo
-> TC CaseDef
simpleCase Bool
False (forall t. t -> SC' t
STerm forall n. TT n
Erased) Bool
False Phase
CompileTime (String -> FC
fileFC String
"proof") [] [] [([], forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
ty, Term
tm)]
         Int -> String -> Idris ()
logLvl Int
3 (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") forall a. a -> a
id [] Term
tm
         Int -> String -> Idris ()
logLvl Int
5 (String
"Proof type: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
pty forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++
                   String
"Expected type:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
ty)
         case Context -> Env -> Term -> Term -> TC ()
converts Context
ctxt [] Term
ty Term
pty of
              OK ()
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Error Err
e -> forall a. Err -> Idris a
ierror (forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
False (Term
ty, forall a. Maybe a
Nothing) (Term
pty, forall a. Maybe a
Nothing) Err
e [] Int
0)
         Term
ptm' <- forall term. Optimisable term => term -> Idris term
applyOpts Term
ptm
         ErasureInfo
ei <- IState -> ErasureInfo
getErasureInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Idris IState
getIState
         Context
ctxt' <- do Context
ctxt <- Idris Context
getContext
                     forall a. TC a -> Idris a
tclift 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 (forall t. t -> SC' t
STerm forall n. TT n
Erased) Bool
True Bool
False
                                [] []  -- argtys, inaccArgs
                                [forall a b. b -> Either a b
Right (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
ty, Term
ptm)]
                                [([], forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
n Term
ty, Term
ptm)]
                                [([], 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 ->
             forall a. IO a -> Idris a
runIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$ forall a. SExpable a => String -> a -> Integer -> String
IdeMode.convSExp String
"return" (String -> SExp
IdeMode.SymbolAtom String
"ok", String
"") Integer
n
           OutputMode
_ -> 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 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
             forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
ps, EState
est {new_tyDecls :: [RDeclInstructions]
new_tyDecls = []}) String
x Maybe (ElabState EState)
old)
        Error Err
a -> forall a. Err -> Idris a
ierror Err
a
  where eCheck :: StateT (ElabState EState) TC (a, Context)
eCheck = do a
res <- ElabD a
e
                    forall aux. Bool -> Elab' aux ()
matchProblems Bool
True
                    forall aux. Elab' aux ()
unifyProblems
                    Fails
probs' <- forall aux. Elab' aux Fails
get_probs
                    case Fails
probs' of
                         [] -> do Term
tm <- forall aux. Elab' aux Term
get_term
                                  Context
ctxt <- forall aux. Elab' aux Context
get_context
                                  forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt [] (Term -> Raw
forget Term
tm)
                                  forall (m :: * -> *) a. Monad m => a -> m a
return (a
res, Context
ctxt)
                         ((Term
_,Term
_,Bool
_,Env
_,Err
e,[FailContext]
_,FailAt
_):Fails
_) -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 <- forall a. Doc a -> Idris (SimpleDoc a)
iRender forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> [(Name, Bool)] -> Name -> OutputDoc
prettyName Bool
True Bool
False [] Name
nm forall a. Doc a -> Doc a -> Doc a
<> forall {a}. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+> 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 forall a. Doc a -> Doc a -> Doc a
<> forall {a}. Doc a
line forall a. Doc a -> Doc a -> Doc a
<>
              Bool -> Binder Term -> Env -> OutputDoc
prettyAssumptions Bool
inElab Binder Term
ty Env
env forall a. Doc a -> Doc a -> Doc a
<> forall {a}. Doc a
line forall a. Doc a -> Doc a -> Doc a
<>
              [(Name, Term, Term)] -> OutputDoc
prettyMetaValues (forall a. [a] -> [a]
reverse [(Name, Term, Term)]
menv) forall a. Doc a -> Doc a -> Doc a
<>
              [(Name, Bool)] -> Binder Term -> OutputDoc
prettyGoal (forall a b. [a] -> [b] -> [(a, b)]
zip (Env -> [Name]
assumptionNames Env
env) (forall a. a -> [a]
repeat Bool
False)) Binder Term
ty
  SimpleDoc OutputAnnotation
rendered <- 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 = forall a. a -> Doc a -> Doc a
annotate ([(Name, Bool)] -> Term -> OutputAnnotation
AnnTerm [(Name, Bool)]
bnd Term
t) 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) forall a b. (a -> b) -> a -> b
$
                    IState -> Term -> PTerm
delab IState
ist Term
t

    assumptionNames :: Env -> [Name]
    assumptionNames :: Env -> [Name]
assumptionNames = forall a b. (a -> b) -> [a] -> [b]
map 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 [] = 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 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)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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Env -> [Name]
freeEnvNames Env
bs Bool -> Bool -> Bool
|| Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` 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) =
      forall {a}. Doc a
line forall a. Doc a -> Doc a -> Doc a
<> Name -> Bool -> OutputDoc
bindingOf Name
n Bool
False forall a. Doc a -> Doc a -> Doc a
<+> forall a. String -> Doc a
text String
"=" forall a. Doc a -> Doc a -> Doc a
<+> [(Name, Bool)] -> Term -> OutputDoc
tPretty [(Name, Bool)]
bnd Term
v forall a. Doc a -> Doc a -> Doc a
<+> forall {a}. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+>
        forall a. Doc a -> Doc a
align ([(Name, Bool)] -> Term -> OutputDoc
tPretty [(Name, Bool)]
bnd Term
t) 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)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) =
      forall {a}. Doc a
line forall a. Doc a -> Doc a -> Doc a
<> Name -> Bool -> OutputDoc
bindingOf Name
n Bool
False forall a. Doc a -> Doc a -> Doc a
<+> forall {a}. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+>
      forall a. Doc a -> Doc a
align ([(Name, Bool)] -> Term -> OutputDoc
tPretty [(Name, Bool)]
bnd (forall b. Binder b -> b
binderTy Binder Term
b)) 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)forall a. a -> [a] -> [a]
:[(Name, Bool)]
bnd) Env
bs

    prettyMetaValues :: [(Name, Term, Term)] -> OutputDoc
prettyMetaValues [] = forall {a}. Doc a
empty
    prettyMetaValues [(Name, Term, Term)]
mvs =
      forall a. String -> Doc a
text String
"----------              Meta-values:               ----------" forall a. Doc a -> Doc a -> Doc a
<$$>
      [(Name, Bool)] -> [(Name, Term, Term)] -> OutputDoc
prettyMetaValues' [] [(Name, Term, Term)]
mvs forall a. Doc a -> Doc a -> Doc a
<> forall {a}. Doc a
line forall a. Doc a -> Doc a -> Doc a
<> forall {a}. Doc a
line
    prettyMetaValues' :: [(Name, Bool)] -> [(Name, Term, Term)] -> OutputDoc
prettyMetaValues' [(Name, Bool)]
_   [] = 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 forall a. Doc a -> Doc a -> Doc a
<$>
      [(Name, Bool)] -> [(Name, Term, Term)] -> OutputDoc
prettyMetaValues' ((Name
n, Bool
False)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" forall a. Doc a -> Doc a -> Doc a
<+> Name -> Bool -> OutputDoc
bindingOf Name
n Bool
False forall a. Doc a -> Doc a -> Doc a
<+> forall {a}. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+>
                           [(Name, Bool)] -> Term -> OutputDoc
tPretty [(Name, Bool)]
bnd Term
ty forall a. Doc a -> Doc a -> Doc a
<+> forall a. String -> Doc a
text String
"=" forall a. Doc a -> Doc a -> Doc a
<+> [(Name, Bool)] -> Term -> OutputDoc
tPretty [(Name, Bool)]
bnd Term
tm

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

    goalNames :: Binder (TT a) -> [a]
goalNames (Guess TT a
t TT a
v) = forall n. Eq n => TT n -> [n]
freeNames TT a
t forall a. [a] -> [a] -> [a]
++ forall n. Eq n => TT n -> [n]
freeNames TT a
v
    goalNames Binder (TT a)
b = forall n. Eq n => TT n -> [n]
freeNames (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 forall a. Doc a -> Doc a -> Doc a
<+> forall a. String -> Doc a
text String
"=?=" 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 forall a b. (a -> b) -> a -> b
$ forall b. Binder b -> b
binderTy Binder Term
b

    prettyGoal :: [(Name, Bool)] -> Binder Term -> OutputDoc
prettyGoal [(Name, Bool)]
bnd Binder Term
ty =
      forall a. String -> Doc a
text String
"----------                 Goal:                  ----------" forall a. Doc a -> Doc a -> Doc a
<$$>
      Name -> Bool -> OutputDoc
bindingOf Name
h Bool
False forall a. Doc a -> Doc a -> Doc a
<+> forall {a}. Doc a
colon forall a. Doc a -> Doc a -> Doc a
<+> 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 forall (t :: * -> *) a. Foldable t => t a -> Bool
null Env
env then forall {a}. Doc a
empty
      else
        forall a. String -> Doc a
text String
"----------              Assumptions:              ----------" forall a. Doc a -> Doc a -> Doc a
<>
        forall a. Int -> Doc a -> Doc a
nest Int
nestingSize (Bool -> Binder Term -> [(Name, Bool)] -> Env -> OutputDoc
prettyPs Bool
inElab Binder Term
g [] forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse Env
env)

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

    freeEnvNames :: Env -> [Name]
    freeEnvNames :: Env -> [Name]
freeEnvNames = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Name
n, RigCount
_, Binder Term
b) -> forall n. Eq n => TT n -> [n]
freeNames (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Term
b 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
_) <- forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
st ElabD a
e
                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 forall a. Eq a => a -> a -> Bool
== Handle
stdout then Handle
stdin else Handle
h
     Either Err Int
len' <- forall a. IO a -> Idris a
runIO 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 -> forall a. Err -> Idris a
ierror Err
err
       Right Int
n  -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
     String
l <- forall a. IO a -> Idris a
runIO 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 -> forall a. Err -> Idris a
ierror Err
err
                     Right (SExp
sexp, Integer
id) -> forall (m :: * -> *) a. Monad m => a -> m a
return (SExp
sexp, Integer
id)
     IState -> Idris ()
putIState forall a b. (a -> b) -> a -> b
$ IState
i { idris_outputmode :: OutputMode
idris_outputmode = Integer -> Handle -> OutputMode
IdeMode Integer
id Handle
h }
     case SExp -> Maybe IdeModeCommand
IdeMode.sexpToCommand SExp
sexp of
       Just (IdeMode.REPLCompletions String
prefix) ->
         do (String
unused, [Completion]
compls) <- [String] -> CompletionFunc (StateT IState (ExceptT Err IO))
proverCompletion (ElabState EState -> [String]
assumptionNames ElabState EState
e) (forall a. [a] -> [a]
reverse String
prefix, String
"")
            let good :: SExp
good = [SExp] -> SExp
IdeMode.SexpList [String -> SExp
IdeMode.SymbolAtom String
"ok", forall a. SExpable a => a -> SExp
IdeMode.toSExp (forall a b. (a -> b) -> [a] -> [b]
map Completion -> String
replacement [Completion]
compls, forall a. [a] -> [a]
reverse String
unused)]
            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) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just String
cmd)
       Just (IdeMode.TypeOf String
str) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (String
":t " forall a. [a] -> [a] -> [a]
++ String
str))
       Just (IdeMode.DocsFor String
str WhatDocs
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (String
":doc " forall a. [a] -> [a] -> [a]
++ String
str))
       Maybe IdeModeCommand
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return 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') <- forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
st forall aux. Elab' aux ()
loadState
                                  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> [a]
init [String]
prf, [(Name, Term, Term)]
env, ElabState EState
st')
undoStep [String]
prf [(Name, Term, Term)]
env ElabState EState
st ElabShellHistory
LetStep = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> [a]
init [String]
prf, forall a. [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') <- forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
st forall aux. Elab' aux ()
loadState
                                  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> [a]
init [String]
prf, forall a. [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 [] = 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
                                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 <- 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) forall a b. (a -> b) -> a -> b
$
                   forall (m :: * -> *) a. MonadMask m => m a -> m a -> m a
handleInterrupt (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) forall a b. (a -> b) -> a -> b
$
                   forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
InputT m a -> InputT m a
withInterrupt (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Idris a
mTry forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 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)]
-> Idris (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
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
d forall a b. (a -> b) -> a -> b
$ IState -> Bool -> [(Name, Term, Term)] -> ProofState -> Idris ()
dumpState IState
ist Bool
True [(Name, Term, Term)]
env (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
_ ->
             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) forall a b. (a -> b) -> a -> b
$
               do case Maybe History
h of
                    Just History
history -> forall (m :: * -> *). MonadIO m => History -> InputT m ()
putHistory History
history
                    Maybe History
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  Maybe String
l <- forall (m :: * -> *) a. MonadMask m => m a -> m a -> m a
handleInterrupt (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just String
"") forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
InputT m a -> InputT m a
withInterrupt forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadIO m, MonadMask m) =>
String -> InputT m (Maybe String)
getInputLine (String
prompt forall a. [a] -> [a] -> [a]
++ String
"> ")
                  History
h' <- forall (m :: * -> *). MonadIO m => InputT m History
getHistory
                  forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
l, 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
                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
"" ; forall a. String -> Idris a
ifail String
"Abandoned"
                        Just String
input -> 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
""; forall a. String -> Idris a
ifail String
"Abandoned"
         Either ParseError (Either ElabShellCmd PDo)
_ -> 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) <-
         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 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) (forall w. Message w => w -> Idris OutputDoc
formatMessage ParseError
err)
                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 <- forall a. ElabState EState -> ElabD a -> Idris a
lifte ElabState EState
e forall aux. Elab' aux [Name]
get_holes
                             forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
hs) forall a b. (a -> b) -> a -> b
$ forall a. String -> Idris a
ifail String
"Incomplete proof"
                             String -> Idris ()
iputStrLn String
"Proof completed!"
                             forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [ElabShellHistory]
prev, ElabState EState
e, Bool
True, [String]
prf, [(Name, Term, Term)]
env, forall a b. b -> Either a b
Right 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
                              forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [ElabShellHistory]
prev', ElabState EState
st', Bool
False, [String]
prf', [(Name, Term, Term)]
env', forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String -> Idris ()
iPrintResult String
"")
                  ElabShellCmd
EAbandon ->
                    forall a. HasCallStack => String -> a
error String
"the impossible happened - should have been matched on outer scope"
                  ElabShellCmd
EProofState -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf, [(Name, Term, Term)]
env, forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String -> Idris ()
iPrintResult String
"")
                  ElabShellCmd
EProofTerm ->
                    do Term
tm <- forall a. ElabState EState -> ElabD a -> Idris a
lifte ElabState EState
e forall aux. Elab' aux Term
get_term
                       forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf, [(Name, Term, Term)]
env, forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ OutputDoc -> Idris ()
iRenderResult (forall a. String -> Doc a
text String
"TT:" 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
                                 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
                       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
                                  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) <- 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
                                   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
                                  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  {} -> forall a. String -> Idris a
ifail String
"Pattern-matching let not supported here"
                  DoRewrite  {} -> forall a. String -> Idris a
ifail String
"Pattern-matching do-rewrite not supported here"
                  DoBindP {} -> 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
                       forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabShellHistory
LetStepforall a. a -> [a] -> [a]
:[ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf forall a. [a] -> [a] -> [a]
++ [String
step], (Name
i, Term
ty', Term
tm' ) forall a. a -> [a] -> [a]
: [(Name, Term, Term)]
env, 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"))
                                                [ forall {t}. t -> PArg' t
pexp (IState -> [(Name, Term, Term)] -> PTerm -> PTerm
inLets IState
ist [(Name, Term, Term)]
env PTerm
ty)
                                                , 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
                       forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabShellHistory
LetStepforall a. a -> [a] -> [a]
:[ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf forall a. [a] -> [a] -> [a]
++ [String
step], (Name
i, Term
ty', Term
tm' ) forall a. a -> [a] -> [a]
: [(Name, Term, Term)]
env, 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') <- forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e forall aux. Elab' aux ()
saveState -- enable :undo
                       (Term
res, ElabState EState
e'') <- forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e' forall a b. (a -> b) -> a -> b
$
                                       ElabInfo -> IState -> FC -> Env -> Term -> [String] -> ElabD Term
runElabAction ElabInfo
info IState
ist FC
NoFC [] Term
tm [String
"Shell"]
                       Context
ctxt <- Idris Context
getContext
                       (Term
v, Term
vty) <- forall a. TC a -> Idris a
tclift 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
                       forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabShellHistory
BothStepforall a. a -> [a] -> [a]
:[ElabShellHistory]
prev, ElabState EState
e'', Bool
False, [String]
prf forall a. [a] -> [a] -> [a]
++ [String
step], (Name
i, Term
vty', Term
v') forall a. a -> [a] -> [a]
: [(Name, Term, Term)]
env, 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') <- forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e forall aux. Elab' aux ()
saveState -- enable :undo
                       (Term
_, ElabState EState
e'') <- forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e' forall a b. (a -> b) -> a -> b
$
                                     ElabInfo -> IState -> FC -> Env -> Term -> [String] -> ElabD Term
runElabAction ElabInfo
info IState
ist FC
NoFC [] Term
tm [String
"Shell"]
                       forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabShellHistory
ElabStepforall a. a -> [a] -> [a]
:[ElabShellHistory]
prev, ElabState EState
e'', Bool
False, [String]
prf forall a. [a] -> [a] -> [a]
++ [String
step], [(Name, Term, Term)]
env, forall a b. b -> Either a b
Right (String -> Idris ()
iPrintResult String
"")))
           (\Err
err -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [ElabShellHistory]
prev, ElabState EState
e, Bool
False, [String]
prf, [(Name, Term, Term)]
env, forall a b. a -> Either a b
Left Err
err))
       forall a. SExpable a => String -> a -> Idris ()
idemodePutSExp String
"write-proof-state" ([String]
prf', 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 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)]
-> Idris (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
_) <- forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
st forall aux. Elab' aux Term
get_term
                           forall (m :: * -> *) a. Monad m => a -> m a
return (Term
tm, [String]
prf')
                   else 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)]
-> Idris (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)]
-> Idris (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 = 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 (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
-> Idris (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)
         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
d forall a b. (a -> b) -> a -> b
$ IState -> Bool -> [(Name, Term, Term)] -> ProofState -> Idris ()
dumpState IState
i Bool
False [] (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
_ ->
               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) 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 -> forall (m :: * -> *). MonadIO m => History -> InputT m ()
putHistory History
history
                      Maybe History
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
                    Maybe String
l <- forall (m :: * -> *) a. MonadMask m => m a -> m a -> m a
handleInterrupt (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just String
"") forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
InputT m a -> InputT m a
withInterrupt forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadIO m, MonadMask m) =>
String -> InputT m (Maybe String)
getInputLine (String
prompt forall a. [a] -> [a] -> [a]
++ String
"> ")
                    History
h' <- forall (m :: * -> *). MonadIO m => InputT m History
getHistory
                    forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String
l, 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
                  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
""; forall a. String -> Idris a
ifail String
"Abandoned"
            Just String
input -> 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
""; forall a. String -> Idris a
ifail String
"Abandoned"
            Either ParseError PTactic
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
         (Bool
d, ElabState EState
st, Bool
done, [String]
prf', Either Err (Idris ())
res) <- forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
           (case Either ParseError PTactic
cmd of
              Left ParseError
err -> do
                Either Err (Idris ())
msg <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) (forall w. Message w => w -> Idris OutputDoc
formatMessage ParseError
err)
                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) <- forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e forall aux. Elab' aux ()
loadState
                               forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabState EState
st, Bool
False, forall a. [a] -> [a]
init [String]
prf, forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String -> Idris ()
iPrintResult String
"")
              Right PTactic
ProofState -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabState EState
e, Bool
False, [String]
prf, forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String -> Idris ()
iPrintResult String
"")
              Right PTactic
ProofTerm -> do Term
tm <- forall a. ElabState EState -> ElabD a -> Idris a
lifte ElabState EState
e forall aux. Elab' aux Term
get_term
                                    String -> Idris ()
iputStrLn forall a b. (a -> b) -> a -> b
$ String
"TT: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm forall a. [a] -> [a] -> [a]
++ String
"\n"
                                    forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf, forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String -> Idris ()
iPrintResult String
"")
              Right PTactic
Qed -> do [Name]
hs <- forall a. ElabState EState -> ElabD a -> Idris a
lifte ElabState EState
e forall aux. Elab' aux [Name]
get_holes
                              forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
hs) forall a b. (a -> b) -> a -> b
$ forall a. String -> Idris a
ifail String
"Incomplete proof"
                              String -> Idris ()
iputStrLn String
"Proof completed!"
                              forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
True, [String]
prf, forall a b. b -> Either a b
Right 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) -> 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) <- forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e forall aux. Elab' aux ()
saveState
                   (()
_, ElabState EState
st) <- forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e (Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD ()
runTac Bool
autoSolve IState
i (forall a. a -> Maybe a
Just FC
proverFC) Name
fn PTactic
tac)
                   forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, ElabState EState
st, Bool
False, [String]
prf forall a. [a] -> [a] -> [a]
++ [String
step], forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String -> Idris ()
iPrintResult String
""))
           (\Err
err -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf, forall a b. a -> Either a b
Left Err
err))
         forall a. SExpable a => String -> a -> Idris ()
idemodePutSExp String
"write-proof-state" ([String]
prf', 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 forall a b. (a -> b) -> a -> b
$ IState -> Err -> OutputDoc
pprintErr IState
ist Err
err
                          Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> Maybe History
-> Idris (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
_) <- forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
st forall aux. Elab' aux Term
get_term
                             forall (m :: * -> *) a. Monad m => a -> m a
return (Term
tm, [String]
prf')
                     else forall a b.
ElabState EState -> Idris a -> Idris b -> Idris b -> Idris b
runWithInterrupt ElabState EState
e Idris ()
ok
                             (Name
-> Bool
-> String
-> [String]
-> ElabState EState
-> Maybe History
-> Idris (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
-> Idris (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 = 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 (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
    forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do
        let OK Env
env = ProofState -> TC Env
envAtFocus (forall aux. ElabState aux -> ProofState
proof ElabState EState
e)
            ctxt' :: Context
ctxt'  = forall {t :: * -> *} {b}.
Foldable t =>
t (Name, b, Binder Term) -> Context -> Context
envCtxt Env
env Context
ctxt
            bnd :: [(Name, Bool)]
bnd    = forall a b. (a -> b) -> [a] -> [b]
map (\(Name, RigCount, Binder Term)
x -> (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 :: Context
tt_ctxt = Context
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 forall a b. (a -> b) -> a -> b
$ String
"No such variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n
                       [Name]
ts -> [(Name, Bool)] -> Name -> [(Name, OutputDoc)] -> Idris ()
iPrintFunTypes [(Name, Bool)]
bnd Name
n (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
        forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf, forall a b. b -> Either a b
Right Idris ()
action))
      (\Err
err -> do IState -> Idris ()
putIState IState
ist ; 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
    forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do
        let OK Env
env = ProofState -> TC Env
envAtFocus (forall aux. ElabState aux -> ProofState
proof ElabState EState
e)
            ctxt' :: Context
ctxt'  = forall {t :: * -> *} {b}.
Foldable t =>
t (Name, b, Binder Term) -> Context -> Context
envCtxt Env
env Context
ctxt
        IState -> Idris ()
putIState IState
ist { tt_ctxt :: Context
tt_ctxt = Context
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 = forall a b. (a -> b) -> [a] -> [b]
map (\(Name, RigCount, Binder Term)
x -> (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
        forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf, forall a b. b -> Either a b
Right Idris ()
action))
      (\Err
err -> do IState -> Idris ()
putIState IState
ist { tt_ctxt :: Context
tt_ctxt = Context
ctxt } ; 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 = forall a. Idris a -> Idris a
withErrorReflection forall a b. (a -> b) -> a -> b
$
    do Context
ctxt <- Idris Context
getContext
       IState
ist <- Idris IState
getIState
       forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do
         let OK Env
env = ProofState -> TC Env
envAtFocus (forall aux. ElabState aux -> ProofState
proof ElabState EState
e)
             ctxt' :: Context
ctxt'  = forall {t :: * -> *} {b}.
Foldable t =>
t (Name, b, Binder Term) -> Context -> Context
envCtxt Env
env Context
ctxt
             ist' :: IState
ist'   = IState
ist { tt_ctxt :: Context
tt_ctxt = Context
ctxt' }
             bnd :: [(Name, Bool)]
bnd    = forall a b. (a -> b) -> [a] -> [b]
map (\(Name, RigCount, Binder Term)
x -> (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'     = forall a. NFData a => a -> a
force (Context -> Env -> Term -> Term
normaliseAll Context
ctxt' Env
env Term
tm)
             ty' :: Term
ty'     = 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
         forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf, forall a b. b -> Either a b
Right Idris ()
action))
        (\Err
err -> do IState -> Idris ()
putIState IState
ist ; 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
                           forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (case forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
ist) of
                                         [] -> forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf,
                                                       forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ String
"No documentation for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n)
                                         [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ns -> do [OutputDoc]
toShow <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall {b}. IState -> (Name, b) -> Idris OutputDoc
showDoc IState
ist) [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
ns
                                                  forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False,  ElabState EState
e, Bool
False, [String]
prf,
                                                          forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ OutputDoc -> Idris ()
iRenderResult (forall a. [Doc a] -> Doc a
vsep [OutputDoc]
toShow)))
                                      (\Err
err -> do IState -> Idris ()
putIState IState
ist ; forall a. Err -> Idris a
ierror Err
err)
         where showDoc :: IState -> (Name, b) -> Idris OutputDoc
showDoc IState
ist (Name
n, b
d) = do Docs
doc <- Name -> HowMuchDocs -> Idris Docs
getDocs Name
n HowMuchDocs
FullDocs
                                       forall (m :: * -> *) a. Monad m => a -> m a
return 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
                            forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, ElabState EState
e, Bool
False, [String]
prf, forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputDoc -> Idris ()
iRenderResult 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 = forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, b
e, Bool
False, d
prf, forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ [PkgName] -> PTerm -> Idris ()
searchByType [] PTerm
t)