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