{-# LANGUAGE PatternGuards #-}
module Idris.Prover (prover, showProof, showRunElab) where
import Prelude (Bool(..), Either(..), Eq(..), Maybe(..), Show(..), String,
concatMap, elem, error, foldl, foldr, fst, id, init, length,
lines, map, not, null, repeat, reverse, tail, zip, ($), (&&),
(++), (.), (||))
import Idris.AbsSyntax
import Idris.Completion
import Idris.Core.CaseTree
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.DataOpts
import Idris.Delaborate
import Idris.Docs (getDocs, pprintConstDocs, pprintDocs)
import Idris.Elab.Term
import Idris.Elab.Utils
import Idris.Elab.Value
import Idris.ElabDecls
import Idris.Error
import qualified Idris.IdeMode as IdeMode
import Idris.Options
import Idris.Output
import Idris.Parser hiding (params)
import Idris.TypeSearch (searchByType)
import Util.Pretty
import Control.DeepSeq
import Control.Monad.State.Strict
import System.Console.Haskeline
import System.Console.Haskeline.History
import System.IO (Handle, hPutStrLn, stdin, stdout)
prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()
prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()
prover 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
[] []
[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
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
-> Idris b
-> Idris b
-> 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)
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
(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)
(()
_, ElabState EState
e') <- forall a.
ElabState EState -> ElabD a -> Idris (a, ElabState EState)
elabStep ElabState EState
e forall aux. Elab' aux ()
saveState
(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
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
$
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'
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)