{-# LANGUAGE PatternGuards #-}
module Idris.Interactive(
caseSplitAt, addClauseFrom, addProofClauseFrom
, addMissing, makeWith, makeCase, doProofSearch
, makeLemma
) where
import Idris.AbsSyntax
import Idris.CaseSplit
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate
import Idris.Elab.Term
import Idris.Elab.Value
import Idris.ElabDecls
import Idris.Error
import Idris.ErrReverse
import Idris.IdeMode hiding (IdeModeCommand(..))
import Idris.Output
import Util.Pretty
import Util.System
import Data.Char
import Data.List (isSuffixOf)
import System.Directory
import System.IO
caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()
caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()
caseSplitAt FilePath
fn Bool
updatefile Int
l Name
n
= do FilePath
src <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSourceStrict FilePath
fn
(Bool
ok, [[(Name, PTerm)]]
res) <- Int -> Name -> FilePath -> Idris (Bool, [[(Name, PTerm)]])
splitOnLine Int
l Name
n FilePath
fn
Int -> FilePath -> Idris ()
logLvl Int
1 (FilePath -> [FilePath] -> FilePath
showSep FilePath
"\n" (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> FilePath
show [[(Name, PTerm)]]
res))
let ([FilePath]
before, (FilePath
ap : [FilePath]
later)) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lforall a. Num a => a -> a -> a
-Int
1) (FilePath -> [FilePath]
lines FilePath
src)
[FilePath]
res' <- FilePath -> [[(Name, PTerm)]] -> Bool -> Idris [FilePath]
replaceSplits FilePath
ap [[(Name, PTerm)]]
res (Bool -> Bool
not Bool
ok)
let new :: FilePath
new = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [FilePath]
res'
if Bool
updatefile
then do let fb :: FilePath
fb = FilePath
fn forall a. [a] -> [a] -> [a]
++ FilePath
"~"
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath
unlines [FilePath]
before forall a. [a] -> [a] -> [a]
++ FilePath
new forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
unlines [FilePath]
later)
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
copyFile FilePath
fb FilePath
fn
else
FilePath -> Idris ()
iPrintResult FilePath
new
addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
addClauseFrom FilePath
fn Bool
updatefile Int
l Name
n = do
IState
ist <- Idris IState
getIState
PTerm
cl <- FilePath -> Int -> Idris PTerm
getInternalApp FilePath
fn Int
l
let fulln :: Name
fulln = PTerm -> Name
getAppName PTerm
cl
let metavars :: Maybe (Maybe Name, Int, [Name], Bool, Bool)
metavars = forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
fulln (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist)
case Maybe (Maybe Name, Int, [Name], Bool, Bool)
metavars of
Maybe (Maybe Name, Int, [Name], Bool, Bool)
Nothing -> FilePath -> Bool -> Int -> Name -> Idris ()
addMissing FilePath
fn Bool
updatefile Int
l Name
n
Just (Maybe Name, Int, [Name], Bool, Bool)
_ -> do
FilePath
src <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSourceStrict FilePath
fn
let ([FilePath]
before, FilePath
tyline : [FilePath]
later) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lforall a. Num a => a -> a -> a
-Int
1) (FilePath -> [FilePath]
lines FilePath
src)
let indent :: Int
indent = forall {t}. Num t => t -> FilePath -> FilePath -> t
getIndent Int
0 (forall a. Show a => a -> FilePath
show Name
n) FilePath
tyline
FilePath
cl <- Int -> Name -> Name -> FilePath -> Idris FilePath
getClause Int
l Name
fulln Name
n FilePath
fn
let ([FilePath]
nonblank, [FilePath]
rest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace) (FilePath
tylineforall a. a -> [a] -> [a]
:[FilePath]
later)
if Bool
updatefile
then do let fb :: FilePath
fb = FilePath
fn forall a. [a] -> [a] -> [a]
++ FilePath
"~"
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath
unlines ([FilePath]
before forall a. [a] -> [a] -> [a]
++ [FilePath]
nonblank) forall a. [a] -> [a] -> [a]
++
forall a. Int -> a -> [a]
replicate Int
indent Char
' ' forall a. [a] -> [a] -> [a]
++
FilePath
cl forall a. [a] -> [a] -> [a]
++ FilePath
"\n" forall a. [a] -> [a] -> [a]
++
[FilePath] -> FilePath
unlines [FilePath]
rest)
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
copyFile FilePath
fb FilePath
fn
else FilePath -> Idris ()
iPrintResult FilePath
cl
where
getIndent :: t -> FilePath -> FilePath -> t
getIndent t
i FilePath
n [] = t
0
getIndent t
i FilePath
n FilePath
xs | forall a. Int -> [a] -> [a]
take Int
9 FilePath
xs forall a. Eq a => a -> a -> Bool
== FilePath
"implementation " = t
i
getIndent t
i FilePath
n FilePath
xs | forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
n) FilePath
xs forall a. Eq a => a -> a -> Bool
== FilePath
n = t
i
getIndent t
i FilePath
n (Char
x : FilePath
xs) = t -> FilePath -> FilePath -> t
getIndent (t
i forall a. Num a => a -> a -> a
+ t
1) FilePath
n FilePath
xs
getAppName :: PTerm -> Name
getAppName (PApp FC
_ PTerm
r [PArg]
_) = PTerm -> Name
getAppName PTerm
r
getAppName (PRef FC
_ [FC]
_ Name
r) = Name
r
getAppName (PTyped PTerm
n PTerm
_) = PTerm -> Name
getAppName PTerm
n
getAppName PTerm
_ = Name
n
addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
addProofClauseFrom FilePath
fn Bool
updatefile Int
l Name
n
= do FilePath
src <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSourceStrict FilePath
fn
let ([FilePath]
before, FilePath
tyline : [FilePath]
later) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lforall a. Num a => a -> a -> a
-Int
1) (FilePath -> [FilePath]
lines FilePath
src)
let indent :: Int
indent = forall {t} {a}. (Num t, Eq a) => t -> [a] -> [a] -> t
getIndent Int
0 (forall a. Show a => a -> FilePath
show Name
n) FilePath
tyline
FilePath
cl <- Int -> Name -> FilePath -> Idris FilePath
getProofClause Int
l Name
n FilePath
fn
let ([FilePath]
nonblank, [FilePath]
rest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace) (FilePath
tylineforall a. a -> [a] -> [a]
:[FilePath]
later)
if Bool
updatefile
then do let fb :: FilePath
fb = FilePath
fn forall a. [a] -> [a] -> [a]
++ FilePath
"~"
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath
unlines ([FilePath]
before forall a. [a] -> [a] -> [a]
++ [FilePath]
nonblank) forall a. [a] -> [a] -> [a]
++
forall a. Int -> a -> [a]
replicate Int
indent Char
' ' forall a. [a] -> [a] -> [a]
++
FilePath
cl forall a. [a] -> [a] -> [a]
++ FilePath
"\n" forall a. [a] -> [a] -> [a]
++
[FilePath] -> FilePath
unlines [FilePath]
rest)
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
copyFile FilePath
fb FilePath
fn
else FilePath -> Idris ()
iPrintResult FilePath
cl
where
getIndent :: t -> [a] -> [a] -> t
getIndent t
i [a]
n [] = t
0
getIndent t
i [a]
n [a]
xs | forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
n) [a]
xs forall a. Eq a => a -> a -> Bool
== [a]
n = t
i
getIndent t
i [a]
n (a
x : [a]
xs) = t -> [a] -> [a] -> t
getIndent (t
i forall a. Num a => a -> a -> a
+ t
1) [a]
n [a]
xs
addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
addMissing FilePath
fn Bool
updatefile Int
l Name
n
= do FilePath
src <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSourceStrict FilePath
fn
let ([FilePath]
before, FilePath
tyline : [FilePath]
later) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lforall a. Num a => a -> a -> a
-Int
1) (FilePath -> [FilePath]
lines FilePath
src)
let indent :: Int
indent = FilePath -> Int
getIndent FilePath
tyline
IState
i <- Idris IState
getIState
PTerm
cl <- FilePath -> Int -> Idris PTerm
getInternalApp FilePath
fn Int
l
let n' :: Name
n' = PTerm -> Name
getAppName PTerm
cl
FilePath
extras <- case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n' (IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs IState
i) of
Maybe ([([(Name, Term)], Term, Term)], [PTerm])
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
""
Just ([([(Name, Term)], Term, Term)]
_, [PTerm]
tms) -> do [PTerm]
tms' <- [PTerm] -> Idris [PTerm]
nameMissing [PTerm]
tms
forall {t}.
(Show t, Num t) =>
FilePath -> t -> Int -> [PTerm] -> Idris FilePath
showNew (forall a. Show a => a -> FilePath
show Name
n forall a. [a] -> [a] -> [a]
++ FilePath
"_rhs") Integer
1 Int
indent [PTerm]
tms'
let ([FilePath]
nonblank, [FilePath]
rest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace) (FilePath
tylineforall a. a -> [a] -> [a]
:[FilePath]
later)
if Bool
updatefile
then do let fb :: FilePath
fb = FilePath
fn forall a. [a] -> [a] -> [a]
++ FilePath
"~"
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath
unlines ([FilePath]
before forall a. [a] -> [a] -> [a]
++ [FilePath]
nonblank)
forall a. [a] -> [a] -> [a]
++ FilePath
extras
forall a. [a] -> [a] -> [a]
++ (if forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
extras then FilePath
"" else FilePath
"\n")
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
unlines [FilePath]
rest)
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ (forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
src seq :: forall a b. a -> b -> b
`seq` FilePath -> FilePath -> IO ()
copyFile FilePath
fb FilePath
fn)
else FilePath -> Idris ()
iPrintResult FilePath
extras
where showPat :: PTerm -> FilePath
showPat = forall a. Show a => a -> FilePath
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. PTerm -> PTerm
stripNS
stripNS :: PTerm -> PTerm
stripNS PTerm
tm = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
dens PTerm
tm where
dens :: PTerm -> PTerm
dens (PRef FC
fc [FC]
hls Name
n) = FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
hls (Name -> Name
nsroot Name
n)
dens PTerm
t = PTerm
t
nsroot :: Name -> Name
nsroot (NS Name
n [Text]
_) = Name -> Name
nsroot Name
n
nsroot (SN (WhereN Int
_ Name
_ Name
n)) = Name -> Name
nsroot Name
n
nsroot Name
n = Name
n
getAppName :: PTerm -> Name
getAppName (PApp FC
_ PTerm
r [PArg]
_) = PTerm -> Name
getAppName PTerm
r
getAppName (PRef FC
_ [FC]
_ Name
r) = Name
r
getAppName (PTyped PTerm
n PTerm
_) = PTerm -> Name
getAppName PTerm
n
getAppName PTerm
_ = Name
n
makeIndent :: Int -> FilePath
makeIndent Int
ind | FilePath
".lidr" forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` FilePath
fn = Char
'>' forall a. a -> [a] -> [a]
: Char
' ' forall a. a -> [a] -> [a]
: forall a. Int -> a -> [a]
replicate (Int
indforall a. Num a => a -> a -> a
-Int
2) Char
' '
| Bool
otherwise = forall a. Int -> a -> [a]
replicate Int
ind Char
' '
showNew :: FilePath -> t -> Int -> [PTerm] -> Idris FilePath
showNew FilePath
nm t
i Int
ind (PTerm
tm : [PTerm]
tms)
= do (FilePath
nm', t
i') <- forall t. (Show t, Num t) => FilePath -> t -> Idris (FilePath, t)
getUniq FilePath
nm t
i
FilePath
rest <- FilePath -> t -> Int -> [PTerm] -> Idris FilePath
showNew FilePath
nm t
i' Int
ind [PTerm]
tms
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> FilePath
makeIndent Int
ind forall a. [a] -> [a] -> [a]
++
PTerm -> FilePath
showPat PTerm
tm forall a. [a] -> [a] -> [a]
++ FilePath
" = ?" forall a. [a] -> [a] -> [a]
++ FilePath
nm' forall a. [a] -> [a] -> [a]
++
(if forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
rest then FilePath
"" else
FilePath
"\n" forall a. [a] -> [a] -> [a]
++ FilePath
rest))
showNew FilePath
nm t
i Int
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
""
getIndent :: FilePath -> Int
getIndent FilePath
s = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isSpace FilePath
s)
makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()
makeWith FilePath
fn Bool
updatefile Int
l Name
n = do
FilePath
src <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSourceStrict FilePath
fn
IState
i <- Idris IState
getIState
Int
indentWith <- Idris Int
getIndentWith
let ([FilePath]
before, FilePath
tyline : [FilePath]
later) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lforall a. Num a => a -> a -> a
-Int
1) (FilePath -> [FilePath]
lines FilePath
src)
let ind :: Int
ind = FilePath -> Int
getIndent FilePath
tyline
let with :: FilePath
with = FilePath -> Name -> Int -> FilePath
mkWith FilePath
tyline Name
n Int
indentWith
let ([FilePath]
nonblank, [FilePath]
rest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\FilePath
x -> Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace FilePath
x) Bool -> Bool -> Bool
&&
Bool -> Bool
not (Int
ind forall a. Eq a => a -> a -> Bool
== FilePath -> Int
getIndent FilePath
x)) [FilePath]
later
if Bool
updatefile
then do
let fb :: FilePath
fb = FilePath
fn forall a. [a] -> [a] -> [a]
++ FilePath
"~"
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath
unlines ([FilePath]
before forall a. [a] -> [a] -> [a]
++ [FilePath]
nonblank) forall a. [a] -> [a] -> [a]
++
FilePath
with forall a. [a] -> [a] -> [a]
++ FilePath
"\n" forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
unlines [FilePath]
rest)
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
copyFile FilePath
fb FilePath
fn
else FilePath -> Idris ()
iPrintResult (FilePath
with forall a. [a] -> [a] -> [a]
++ FilePath
"\n")
where getIndent :: FilePath -> Int
getIndent FilePath
s = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isSpace FilePath
s)
makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
makeCase FilePath
fn Bool
updatefile Int
l Name
n
= do FilePath
src <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSourceStrict FilePath
fn
let ([FilePath]
before, FilePath
tyline : [FilePath]
later) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lforall a. Num a => a -> a -> a
-Int
1) (FilePath -> [FilePath]
lines FilePath
src)
let newcase :: [FilePath]
newcase = FilePath -> FilePath -> [FilePath]
addCaseSkel (forall a. Show a => a -> FilePath
show Name
n) FilePath
tyline
if Bool
updatefile then
do let fb :: FilePath
fb = FilePath
fn forall a. [a] -> [a] -> [a]
++ FilePath
"~"
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath
unlines ([FilePath]
before forall a. [a] -> [a] -> [a]
++ [FilePath]
newcase forall a. [a] -> [a] -> [a]
++ [FilePath]
later))
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
copyFile FilePath
fb FilePath
fn
else FilePath -> Idris ()
iPrintResult (FilePath -> [FilePath] -> FilePath
showSep FilePath
"\n" [FilePath]
newcase forall a. [a] -> [a] -> [a]
++FilePath
"\n")
where addCaseSkel :: FilePath -> FilePath -> [FilePath]
addCaseSkel FilePath
n FilePath
line =
let b :: Bool
b = Bool -> FilePath -> Bool
brackets Bool
False FilePath
line in
case forall {a} {t}. (Eq a, Num t) => [a] -> [a] -> Maybe ([a], t, [a])
findSubstr (Char
'?'forall a. a -> [a] -> [a]
:FilePath
n) FilePath
line of
Just (FilePath
before, Int
pos, FilePath
after) ->
[FilePath
before forall a. [a] -> [a] -> [a]
++ (if Bool
b then FilePath
"(" else FilePath
"") forall a. [a] -> [a] -> [a]
++ FilePath
"case _ of",
forall a. Int -> [a] -> [a]
take (Int
pos forall a. Num a => a -> a -> a
+ (if Bool
b then Int
6 else Int
5)) (forall a. a -> [a]
repeat Char
' ') forall a. [a] -> [a] -> [a]
++
FilePath
"case_val => ?" forall a. [a] -> [a] -> [a]
++ FilePath
n forall a. [a] -> [a] -> [a]
++ (if Bool
b then FilePath
")" else FilePath
"")
forall a. [a] -> [a] -> [a]
++ FilePath
after]
Maybe (FilePath, Int, FilePath)
Nothing -> forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail FilePath
"No such metavariable"
brackets :: Bool -> FilePath -> Bool
brackets Bool
eq FilePath
line | FilePath
line forall a. Eq a => a -> a -> Bool
== Char
'?' forall a. a -> [a] -> [a]
: forall a. Show a => a -> FilePath
show Name
n = Bool -> Bool
not Bool
eq
brackets Bool
eq (Char
'=':FilePath
ls) = Bool -> FilePath -> Bool
brackets Bool
True FilePath
ls
brackets Bool
eq (Char
' ':FilePath
ls) = Bool -> FilePath -> Bool
brackets Bool
eq FilePath
ls
brackets Bool
eq (Char
l : FilePath
ls) = Bool -> FilePath -> Bool
brackets Bool
False FilePath
ls
brackets Bool
eq [] = Bool
True
findSubstr :: [a] -> [a] -> Maybe ([a], t, [a])
findSubstr [a]
n [a]
xs = forall {a} {t}.
(Eq a, Num t) =>
[a] -> t -> [a] -> [a] -> Maybe ([a], t, [a])
findSubstr' [] t
0 [a]
n [a]
xs
findSubstr' :: [a] -> t -> [a] -> [a] -> Maybe ([a], t, [a])
findSubstr' [a]
acc t
i [a]
n [a]
xs | forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
n) [a]
xs forall a. Eq a => a -> a -> Bool
== [a]
n
= forall a. a -> Maybe a
Just (forall a. [a] -> [a]
reverse [a]
acc, t
i, forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
n) [a]
xs)
findSubstr' [a]
acc t
i [a]
n [] = forall a. Maybe a
Nothing
findSubstr' [a]
acc t
i [a]
n (a
x : [a]
xs) = [a] -> t -> [a] -> [a] -> Maybe ([a], t, [a])
findSubstr' (a
x forall a. a -> [a] -> [a]
: [a]
acc) (t
i forall a. Num a => a -> a -> a
+ t
1) [a]
n [a]
xs
doProofSearch :: FilePath -> Bool -> Bool ->
Int -> Name -> [Name] -> Maybe Int -> Idris ()
doProofSearch :: FilePath
-> Bool -> Bool -> Int -> Name -> [Name] -> Maybe Int -> Idris ()
doProofSearch FilePath
fn Bool
updatefile Bool
rec Int
l Name
n [Name]
hints Maybe Int
Nothing
= FilePath
-> Bool -> Bool -> Int -> Name -> [Name] -> Maybe Int -> Idris ()
doProofSearch FilePath
fn Bool
updatefile Bool
rec Int
l Name
n [Name]
hints (forall a. a -> Maybe a
Just Int
20)
doProofSearch FilePath
fn Bool
updatefile Bool
rec Int
l Name
n [Name]
hints (Just Int
depth)
= do FilePath
src <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSourceStrict FilePath
fn
let ([FilePath]
before, FilePath
tyline : [FilePath]
later) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lforall a. Num a => a -> a -> a
-Int
1) (FilePath -> [FilePath]
lines FilePath
src)
Context
ctxt <- Idris Context
getContext
Name
mn <- case Name -> Context -> [Name]
lookupNames Name
n Context
ctxt of
[Name
x] -> forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return Name
n
[Name]
ns -> forall a. Err -> Idris a
ierror (forall t. [Name] -> Err' t
CantResolveAlts [Name]
ns)
IState
i <- Idris IState
getIState
let (Maybe Name
top, Int
envlen, [Name]
psnames)
= case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
mn (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
i) of
Just (Maybe Name
t, Int
e, [Name]
ns, Bool
False, Bool
d) -> (Maybe Name
t, Int
e, [Name]
ns)
Maybe (Maybe Name, Int, [Name], Bool, Bool)
_ -> (forall a. Maybe a
Nothing, Int
0, [])
let fc :: FC
fc = FilePath -> FC
fileFC FilePath
fn
let body :: Maybe Name -> PTerm
body Maybe Name
t = [PTactic] -> PTerm
PProof [forall t. PTactic' t -> PTactic' t -> PTactic' t
Try (forall t. PTactic' t -> PTactic' t -> PTactic' t
TSeq forall t. PTactic' t
Intros (forall t.
Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic' t
ProofSearch Bool
rec Bool
False Int
depth Maybe Name
t [Name]
psnames [Name]
hints))
(forall t.
Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic' t
ProofSearch Bool
rec Bool
False Int
depth Maybe Name
t [Name]
psnames [Name]
hints)]
let def :: PClause' PTerm
def = forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
mn (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
mn) [] (Maybe Name -> PTerm
body Maybe Name
top) []
FilePath
newmv_pre <- forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
(do ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
EAll (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"proofsearch")) (forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc [] Name
mn [PClause' PTerm
def])
(Term
tm, Term
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"proofsearch")) ElabMode
ERHS (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
mn)
Context
ctxt <- Idris Context
getContext
IState
i <- Idris IState
getIState
forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. SimpleDoc a -> ShowS
displayS FilePath
"" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
80 forall a b. (a -> b) -> a -> b
$
PPOption
-> [(Name, Bool)]
-> [Name]
-> [FixDecl]
-> PTerm
-> Doc OutputAnnotation
pprintPTerm PPOption
defaultPPOption [] [] (IState -> [FixDecl]
idris_infixes IState
i)
(PTerm -> PTerm
stripNS
(forall {t}. (Eq t, Num t) => t -> PTerm -> PTerm
dropCtxt Int
envlen
(IState -> Term -> PTerm
delab IState
i (forall a b. (a, b) -> a
fst (Context -> Env -> [(Name, Int)] -> Term -> (Term, [(Name, Int)])
specialise Context
ctxt [] [(Name
mn, Int
1)] Term
tm))))))
(\Err
e -> forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath
"?" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show Name
n))
let newmv :: FilePath
newmv = Bool -> FilePath -> FilePath -> ShowS
guessBrackets Bool
False FilePath
tyline (forall a. Show a => a -> FilePath
show Name
n) FilePath
newmv_pre
if Bool
updatefile then
do let fb :: FilePath
fb = FilePath
fn forall a. [a] -> [a] -> [a]
++ FilePath
"~"
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath
unlines [FilePath]
before forall a. [a] -> [a] -> [a]
++
FilePath -> FilePath -> ShowS
updateMeta FilePath
tyline (forall a. Show a => a -> FilePath
show Name
n) FilePath
newmv forall a. [a] -> [a] -> [a]
++ FilePath
"\n"
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
unlines [FilePath]
later)
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
copyFile FilePath
fb FilePath
fn
else FilePath -> Idris ()
iPrintResult FilePath
newmv
where dropCtxt :: t -> PTerm -> PTerm
dropCtxt t
0 PTerm
sc = PTerm
sc
dropCtxt t
i (PPi Plicity
_ Name
_ FC
_ PTerm
_ PTerm
sc) = t -> PTerm -> PTerm
dropCtxt (t
i forall a. Num a => a -> a -> a
- t
1) PTerm
sc
dropCtxt t
i (PLet FC
_ RigCount
_ Name
_ FC
_ PTerm
_ PTerm
_ PTerm
sc) = t -> PTerm -> PTerm
dropCtxt (t
i forall a. Num a => a -> a -> a
- t
1) PTerm
sc
dropCtxt t
i (PLam FC
_ Name
_ FC
_ PTerm
_ PTerm
sc) = t -> PTerm -> PTerm
dropCtxt (t
i forall a. Num a => a -> a -> a
- t
1) PTerm
sc
dropCtxt t
_ PTerm
t = PTerm
t
stripNS :: PTerm -> PTerm
stripNS PTerm
tm = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
dens PTerm
tm where
dens :: PTerm -> PTerm
dens (PRef FC
fc [FC]
hls Name
n) = FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
hls (Name -> Name
nsroot Name
n)
dens PTerm
t = PTerm
t
nsroot :: Name -> Name
nsroot (NS Name
n [Text]
_) = Name -> Name
nsroot Name
n
nsroot (SN (WhereN Int
_ Name
_ Name
n)) = Name -> Name
nsroot Name
n
nsroot Name
n = Name
n
updateMeta :: FilePath -> FilePath -> ShowS
updateMeta (Char
'?':FilePath
cs) FilePath
n FilePath
new
| forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
cs forall a. Ord a => a -> a -> Bool
>= forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
n
= case forall a. Int -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
n) FilePath
cs of
(FilePath
mv, Char
c:FilePath
cs) ->
if ((Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
|| Char
c forall a. Eq a => a -> a -> Bool
== Char
')' Bool -> Bool -> Bool
|| Char
c forall a. Eq a => a -> a -> Bool
== Char
'}') Bool -> Bool -> Bool
&& FilePath
mv forall a. Eq a => a -> a -> Bool
== FilePath
n)
then FilePath
new forall a. [a] -> [a] -> [a]
++ (Char
c forall a. a -> [a] -> [a]
: FilePath
cs)
else Char
'?' forall a. a -> [a] -> [a]
: FilePath
mv forall a. [a] -> [a] -> [a]
++ Char
c forall a. a -> [a] -> [a]
: FilePath -> FilePath -> ShowS
updateMeta FilePath
cs FilePath
n FilePath
new
(FilePath
mv, []) -> if (FilePath
mv forall a. Eq a => a -> a -> Bool
== FilePath
n) then FilePath
new else Char
'?' forall a. a -> [a] -> [a]
: FilePath
mv
updateMeta (Char
'=':Char
'>':FilePath
cs) FilePath
n FilePath
new = Char
'='forall a. a -> [a] -> [a]
:Char
'>'forall a. a -> [a] -> [a]
:FilePath -> FilePath -> ShowS
updateMeta FilePath
cs FilePath
n FilePath
new
updateMeta (Char
'=':FilePath
cs) FilePath
n FilePath
new = Char
'='forall a. a -> [a] -> [a]
:FilePath -> FilePath -> ShowS
updateMeta FilePath
cs FilePath
n FilePath
new
updateMeta (Char
c:FilePath
cs) FilePath
n FilePath
new
= Char
c forall a. a -> [a] -> [a]
: FilePath -> FilePath -> ShowS
updateMeta FilePath
cs FilePath
n FilePath
new
updateMeta [] FilePath
n FilePath
new = FilePath
""
guessBrackets :: Bool -> FilePath -> FilePath -> ShowS
guessBrackets Bool
brack (Char
'?':FilePath
cs) FilePath
n FilePath
new
| forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
cs forall a. Ord a => a -> a -> Bool
>= forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
n
= case forall a. Int -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
n) FilePath
cs of
(FilePath
mv, Char
c:FilePath
cs) ->
if ((Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
|| Char
c forall a. Eq a => a -> a -> Bool
== Char
')' Bool -> Bool -> Bool
|| Char
c forall a. Eq a => a -> a -> Bool
== Char
'}') Bool -> Bool -> Bool
&& FilePath
mv forall a. Eq a => a -> a -> Bool
== FilePath
n)
then Bool -> ShowS
addBracket Bool
brack FilePath
new
else Bool -> FilePath -> FilePath -> ShowS
guessBrackets Bool
True FilePath
cs FilePath
n FilePath
new
(FilePath
mv, []) -> if (FilePath
mv forall a. Eq a => a -> a -> Bool
== FilePath
n) then Bool -> ShowS
addBracket Bool
brack FilePath
new else Char
'?' forall a. a -> [a] -> [a]
: FilePath
mv
guessBrackets Bool
brack (Char
'=':Char
'>':FilePath
cs) FilePath
n FilePath
new = Bool -> FilePath -> FilePath -> ShowS
guessBrackets Bool
False FilePath
cs FilePath
n FilePath
new
guessBrackets Bool
brack (Char
'-':Char
'>':FilePath
cs) FilePath
n FilePath
new = Bool -> FilePath -> FilePath -> ShowS
guessBrackets Bool
False FilePath
cs FilePath
n FilePath
new
guessBrackets Bool
brack (Char
'=':FilePath
cs) FilePath
n FilePath
new = Bool -> FilePath -> FilePath -> ShowS
guessBrackets Bool
False FilePath
cs FilePath
n FilePath
new
guessBrackets Bool
brack (Char
c:FilePath
cs) FilePath
n FilePath
new
= Bool -> FilePath -> FilePath -> ShowS
guessBrackets (Bool
brack Bool -> Bool -> Bool
|| Bool -> Bool
not (Char -> Bool
isSpace Char
c)) FilePath
cs FilePath
n FilePath
new
guessBrackets Bool
brack [] FilePath
n FilePath
new = FilePath
""
checkProv :: FilePath -> FilePath -> Bool
checkProv FilePath
line FilePath
n = Bool -> FilePath -> FilePath -> Bool
isProv' Bool
False FilePath
line FilePath
n
where
isProv' :: Bool -> FilePath -> FilePath -> Bool
isProv' Bool
p FilePath
cs FilePath
n | forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
n) FilePath
cs forall a. Eq a => a -> a -> Bool
== FilePath
n = Bool
p
isProv' Bool
_ (Char
'?':FilePath
cs) FilePath
n = Bool -> FilePath -> FilePath -> Bool
isProv' Bool
False FilePath
cs FilePath
n
isProv' Bool
_ (Char
'{':FilePath
cs) FilePath
n = Bool -> FilePath -> FilePath -> Bool
isProv' Bool
True FilePath
cs FilePath
n
isProv' Bool
_ (Char
'}':FilePath
cs) FilePath
n = Bool -> FilePath -> FilePath -> Bool
isProv' Bool
True FilePath
cs FilePath
n
isProv' Bool
p (Char
_:FilePath
cs) FilePath
n = Bool -> FilePath -> FilePath -> Bool
isProv' Bool
p FilePath
cs FilePath
n
isProv' Bool
_ [] FilePath
n = Bool
False
addBracket :: Bool -> ShowS
addBracket Bool
False FilePath
new = FilePath
new
addBracket Bool
True new :: FilePath
new@(Char
'(':FilePath
xs) | forall a. [a] -> a
last FilePath
xs forall a. Eq a => a -> a -> Bool
== Char
')' = FilePath
new
addBracket Bool
True FilePath
new | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace FilePath
new = Char
'(' forall a. a -> [a] -> [a]
: FilePath
new forall a. [a] -> [a] -> [a]
++ FilePath
")"
| Bool
otherwise = FilePath
new
makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
makeLemma FilePath
fn Bool
updatefile Int
l Name
n
= do FilePath
src <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSourceStrict FilePath
fn
let ([FilePath]
before, FilePath
tyline : [FilePath]
later) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lforall a. Num a => a -> a -> a
-Int
1) (FilePath -> [FilePath]
lines FilePath
src)
let isProv :: Bool
isProv = FilePath -> FilePath -> Bool
checkProv FilePath
tyline (forall a. Show a => a -> FilePath
show Name
n)
Context
ctxt <- Idris Context
getContext
(Name
fname, Term
mty_full) <- case Name -> Context -> [(Name, Term)]
lookupTyName Name
n Context
ctxt of
[(Name, Term)
t] -> forall (m :: * -> *) a. Monad m => a -> m a
return (Name, Term)
t
[] -> forall a. Err -> Idris a
ierror (forall t. Name -> Err' t
NoSuchVariable Name
n)
[(Name, Term)]
ns -> forall a. Err -> Idris a
ierror (forall t. [Name] -> Err' t
CantResolveAlts (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Term)]
ns))
IState
i <- Idris IState
getIState
let mty :: Term
mty = IState -> Term -> Term
errReverse IState
i Term
mty_full
Int
margs <- case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
fname (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
i) of
Just (Maybe Name
_, Int
arity, [Name]
_, Bool
_, Bool
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
arity
Maybe (Maybe Name, Int, [Name], Bool, Bool)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (-Int
1)
if (Bool -> Bool
not Bool
isProv) then do
let skip :: [Name]
skip = IState -> Context -> Term -> [Name]
guessImps IState
i (IState -> Context
tt_ctxt IState
i) Term
mty
let impty :: PTerm
impty = forall {t} {t :: * -> *}.
(Ord t, Num t, Foldable t) =>
t Name -> t -> PTerm -> PTerm
stripMNBind [Name]
skip Int
margs (IState -> Term -> PTerm
delab IState
i Term
mty)
let interfaces :: [Name]
interfaces = IState -> Context -> [Name] -> [Name] -> Term -> [Name]
guessInterfaces IState
i (IState -> Context
tt_ctxt IState
i) [] (PTerm -> [Name]
allNamesIn PTerm
impty) Term
mty
let lem :: FilePath
lem = forall a. Show a => a -> FilePath
show Name
n forall a. [a] -> [a] -> [a]
++ FilePath
" : " forall a. [a] -> [a] -> [a]
++
IState -> [Name] -> Term -> FilePath
constraints IState
i [Name]
interfaces Term
mty forall a. [a] -> [a] -> [a]
++
PPOption -> PTerm -> FilePath
showTmOpts (PPOption
defaultPPOption { ppopt_pinames :: Bool
ppopt_pinames = Bool
True })
PTerm
impty
let lem_app :: FilePath
lem_app = Bool -> FilePath -> FilePath -> ShowS
guessBrackets Bool
False FilePath
tyline (forall a. Show a => a -> FilePath
show Name
n) (forall a. Show a => a -> FilePath
show Name
n forall a. [a] -> [a] -> [a]
++ forall {t} {t :: * -> *}.
(Eq t, Num t, Foldable t) =>
t Name -> t -> Term -> FilePath
appArgs [Name]
skip Int
margs Term
mty)
if Bool
updatefile then
do let fb :: FilePath
fb = FilePath
fn forall a. [a] -> [a] -> [a]
++ FilePath
"~"
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath]
-> FilePath -> FilePath -> FilePath -> [FilePath] -> FilePath
addLem [FilePath]
before FilePath
tyline FilePath
lem FilePath
lem_app [FilePath]
later)
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
copyFile FilePath
fb FilePath
fn
else case IState -> OutputMode
idris_outputmode IState
i of
RawOutput Handle
_ -> FilePath -> Idris ()
iPrintResult forall a b. (a -> b) -> a -> b
$ FilePath
lem forall a. [a] -> [a] -> [a]
++ FilePath
"\n" forall a. [a] -> [a] -> [a]
++ FilePath
lem_app
IdeMode Integer
n Handle
h ->
let good :: SExp
good = [SExp] -> SExp
SexpList [FilePath -> SExp
SymbolAtom FilePath
"ok",
[SExp] -> SExp
SexpList [FilePath -> SExp
SymbolAtom FilePath
"metavariable-lemma",
[SExp] -> SExp
SexpList [FilePath -> SExp
SymbolAtom FilePath
"replace-metavariable",
FilePath -> SExp
StringAtom FilePath
lem_app],
[SExp] -> SExp
SexpList [FilePath -> SExp
SymbolAtom FilePath
"definition-type",
FilePath -> SExp
StringAtom FilePath
lem]]]
in forall a. IO a -> Idris a
runIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$ forall a. SExpable a => FilePath -> a -> Integer -> FilePath
convSExp FilePath
"return" SExp
good Integer
n
else do
let lem_app :: FilePath
lem_app = forall a. Show a => a -> FilePath
show Name
n forall a. [a] -> [a] -> [a]
++ forall {t} {t :: * -> *}.
(Eq t, Num t, Foldable t) =>
t Name -> t -> Term -> FilePath
appArgs [] (-Integer
1) Term
mty forall a. [a] -> [a] -> [a]
++
FilePath
" = ?" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show Name
n forall a. [a] -> [a] -> [a]
++ FilePath
"_rhs"
if Bool
updatefile then
do let fb :: FilePath
fb = FilePath
fn forall a. [a] -> [a] -> [a]
++ FilePath
"~"
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath -> FilePath -> [FilePath] -> FilePath
addProv [FilePath]
before FilePath
tyline FilePath
lem_app [FilePath]
later)
forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
copyFile FilePath
fb FilePath
fn
else case IState -> OutputMode
idris_outputmode IState
i of
RawOutput Handle
_ -> FilePath -> Idris ()
iPrintResult FilePath
lem_app
IdeMode Integer
n Handle
h ->
let good :: SExp
good = [SExp] -> SExp
SexpList [FilePath -> SExp
SymbolAtom FilePath
"ok",
[SExp] -> SExp
SexpList [FilePath -> SExp
SymbolAtom FilePath
"provisional-definition-lemma",
[SExp] -> SExp
SexpList [FilePath -> SExp
SymbolAtom FilePath
"definition-clause",
FilePath -> SExp
StringAtom FilePath
lem_app]]]
in forall a. IO a -> Idris a
runIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$ forall a. SExpable a => FilePath -> a -> Integer -> FilePath
convSExp FilePath
"return" SExp
good Integer
n
where appArgs :: t Name -> t -> Term -> FilePath
appArgs t Name
skip t
0 Term
_ = FilePath
""
appArgs t Name
skip t
i (Bind n :: Name
n@(UN Text
c) (Pi RigCount
_ Maybe ImplicitInfo
_ Term
_ Term
_) Term
sc)
| (Text -> Char
thead Text
c forall a. Eq a => a -> a -> Bool
/= Char
'_' Bool -> Bool -> Bool
&& Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t Name
skip)
= FilePath
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show Name
n forall a. [a] -> [a] -> [a]
++ t Name -> t -> Term -> FilePath
appArgs t Name
skip (t
i forall a. Num a => a -> a -> a
- t
1) Term
sc
appArgs t Name
skip t
i (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ Term
_ Term
_) Term
sc) = t Name -> t -> Term -> FilePath
appArgs t Name
skip (t
i forall a. Num a => a -> a -> a
- t
1) Term
sc
appArgs t Name
skip t
i Term
_ = FilePath
""
stripMNBind :: t Name -> t -> PTerm -> PTerm
stripMNBind t Name
_ t
args PTerm
t | t
args forall a. Ord a => a -> a -> Bool
<= t
0 = PTerm -> PTerm
stripImp PTerm
t
stripMNBind t Name
skip t
args (PPi Plicity
b n :: Name
n@(UN Text
c) FC
_ PTerm
ty PTerm
sc)
| Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t Name
skip Bool -> Bool -> Bool
||
forall a. Int -> [a] -> [a]
take Int
4 (Text -> FilePath
str Text
c) forall a. Eq a => a -> a -> Bool
== FilePath
"__pi"
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
b Name
n FC
NoFC (PTerm -> PTerm
stripImp PTerm
ty) (t Name -> t -> PTerm -> PTerm
stripMNBind t Name
skip (t
args forall a. Num a => a -> a -> a
- t
1) PTerm
sc)
stripMNBind t Name
skip t
args (PPi Plicity
b Name
_ FC
_ PTerm
ty PTerm
sc) = t Name -> t -> PTerm -> PTerm
stripMNBind t Name
skip (t
args forall a. Num a => a -> a -> a
- t
1) PTerm
sc
stripMNBind t Name
skip t
args PTerm
t = PTerm -> PTerm
stripImp PTerm
t
stripImp :: PTerm -> PTerm
stripImp (PApp FC
fc PTerm
f [PArg]
as) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (PTerm -> PTerm
stripImp PTerm
f) (forall a b. (a -> b) -> [a] -> [b]
map PArg -> PArg
placeholderImp [PArg]
as)
where
placeholderImp :: PArg -> PArg
placeholderImp tm :: PArg
tm@(PImp Int
_ Bool
_ [ArgOpt]
_ Name
_ PTerm
_) = PArg
tm { getTm :: PTerm
getTm = PTerm
Placeholder }
placeholderImp PArg
tm = PArg
tm { getTm :: PTerm
getTm = PTerm -> PTerm
stripImp (forall t. PArg' t -> t
getTm PArg
tm) }
stripImp (PPi Plicity
b Name
n FC
f PTerm
ty PTerm
sc) = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
b Name
n FC
f (PTerm -> PTerm
stripImp PTerm
ty) (PTerm -> PTerm
stripImp PTerm
sc)
stripImp PTerm
t = PTerm
t
constraints :: IState -> [Name] -> Type -> String
constraints :: IState -> [Name] -> Term -> FilePath
constraints IState
i [] Term
ty = FilePath
""
constraints IState
i [Name
n] Term
ty = FilePath -> [FilePath] -> FilePath
showSep FilePath
", " (forall {t :: * -> *}.
Foldable t =>
IState -> t Name -> Term -> [FilePath]
showConstraints IState
i [Name
n] Term
ty) forall a. [a] -> [a] -> [a]
++ FilePath
" => "
constraints IState
i [Name]
ns Term
ty = FilePath
"(" forall a. [a] -> [a] -> [a]
++ FilePath -> [FilePath] -> FilePath
showSep FilePath
", " (forall {t :: * -> *}.
Foldable t =>
IState -> t Name -> Term -> [FilePath]
showConstraints IState
i [Name]
ns Term
ty) forall a. [a] -> [a] -> [a]
++ FilePath
") => "
showConstraints :: IState -> t Name -> Term -> [FilePath]
showConstraints IState
i t Name
ns (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc)
| Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
ns = forall a. Show a => a -> FilePath
show (IState -> Term -> PTerm
delab IState
i Term
ty) forall a. a -> [a] -> [a]
:
IState -> t Name -> Term -> [FilePath]
showConstraints IState
i t Name
ns (forall n. TT n -> TT n -> TT n
substV (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n forall n. TT n
Erased) Term
sc)
| Bool
otherwise = IState -> t Name -> Term -> [FilePath]
showConstraints IState
i t Name
ns (forall n. TT n -> TT n -> TT n
substV (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n forall n. TT n
Erased) Term
sc)
showConstraints IState
_ t Name
_ Term
_ = []
guessImps :: IState -> Context -> Term -> [Name]
guessImps :: IState -> Context -> Term -> [Name]
guessImps IState
ist Context
ctxt (Bind n :: Name
n@(MN Int
_ Text
_) (Pi RigCount
_ Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc)
= Name
n forall a. a -> [a] -> [a]
: IState -> Context -> Term -> [Name]
guessImps IState
ist Context
ctxt Term
sc
guessImps IState
ist Context
ctxt (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc)
| Context -> Name -> Term -> Bool
guarded Context
ctxt Name
n (forall n. TT n -> TT n -> TT n
substV (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n forall n. TT n
Erased) Term
sc)
= Name
n forall a. a -> [a] -> [a]
: IState -> Context -> Term -> [Name]
guessImps IState
ist Context
ctxt Term
sc
| IState -> Term -> Bool
isInterface IState
ist Term
ty
= Name
n forall a. a -> [a] -> [a]
: IState -> Context -> Term -> [Name]
guessImps IState
ist Context
ctxt Term
sc
| forall {n}. TT n -> Bool
paramty Term
ty = Name
n forall a. a -> [a] -> [a]
: IState -> Context -> Term -> [Name]
guessImps IState
ist Context
ctxt Term
sc
| forall {a}. Show a => a -> Bool
ignoreName Name
n = Name
n forall a. a -> [a] -> [a]
: IState -> Context -> Term -> [Name]
guessImps IState
ist Context
ctxt Term
sc
| Bool
otherwise = IState -> Context -> Term -> [Name]
guessImps IState
ist Context
ctxt Term
sc
guessImps IState
ist Context
ctxt Term
_ = []
paramty :: TT n -> Bool
paramty (TType UExp
_) = Bool
True
paramty (Bind n
_ (Pi RigCount
_ Maybe ImplicitInfo
_ (TType UExp
_) TT n
_) TT n
sc) = TT n -> Bool
paramty TT n
sc
paramty TT n
_ = Bool
False
ignoreName :: a -> Bool
ignoreName a
n = case forall a. Show a => a -> FilePath
show a
n of
FilePath
"_aX" -> Bool
True
FilePath
_ -> Bool
False
guessInterfaces :: IState -> Context -> [Name] -> [Name] -> Term -> [Name]
guessInterfaces :: IState -> Context -> [Name] -> [Name] -> Term -> [Name]
guessInterfaces IState
ist Context
ctxt [Name]
binders [Name]
usednames (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Term
ty Term
_) Term
sc)
| IState -> Term -> Bool
isParamInterface IState
ist Term
ty Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Name
x -> forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Name
x [Name]
usednames)
(forall {a} {n}. [a] -> TT n -> [a]
paramNames [Name]
binders Term
ty)
= Name
n forall a. a -> [a] -> [a]
: IState -> Context -> [Name] -> [Name] -> Term -> [Name]
guessInterfaces IState
ist Context
ctxt (Name
n forall a. a -> [a] -> [a]
: [Name]
binders) [Name]
usednames Term
sc
| Bool
otherwise = IState -> Context -> [Name] -> [Name] -> Term -> [Name]
guessInterfaces IState
ist Context
ctxt (Name
n forall a. a -> [a] -> [a]
: [Name]
binders) [Name]
usednames Term
sc
guessInterfaces IState
ist Context
ctxt [Name]
_ [Name]
_ Term
_ = []
paramNames :: [a] -> TT n -> [a]
paramNames [a]
bs TT n
ty | (P NameType
_ n
_ TT n
_, [TT n]
args) <- forall n. TT n -> (TT n, [TT n])
unApply TT n
ty
= forall {n}. [TT n] -> [a]
vnames [TT n]
args
where vnames :: [TT n] -> [a]
vnames [] = []
vnames (V Int
i : [TT n]
xs) | Int
i forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
bs = [a]
bs forall a. [a] -> Int -> a
!! Int
i forall a. a -> [a] -> [a]
: [TT n] -> [a]
vnames [TT n]
xs
vnames (TT n
_ : [TT n]
xs) = [TT n] -> [a]
vnames [TT n]
xs
isInterface :: IState -> Term -> Bool
isInterface IState
ist Term
t
| (P NameType
_ Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t
= case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
Just InterfaceInfo
_ -> Bool
True
Maybe InterfaceInfo
_ -> Bool
False
| Bool
otherwise = Bool
False
isParamInterface :: IState -> Term -> Bool
isParamInterface IState
ist Term
t
| (P NameType
_ Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t
= case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
Just InterfaceInfo
_ -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall {n}. TT n -> Bool
isV [Term]
args
Maybe InterfaceInfo
_ -> Bool
False
| Bool
otherwise = Bool
False
where isV :: TT n -> Bool
isV (V Int
_) = Bool
True
isV TT n
_ = Bool
False
guarded :: Context -> Name -> Term -> Bool
guarded Context
ctxt Name
n (P NameType
_ Name
n' Term
_) | Name
n forall a. Eq a => a -> a -> Bool
== Name
n' = Bool
True
guarded Context
ctxt Name
n ap :: Term
ap@(App AppStatus Name
_ Term
_ Term
_)
| (P NameType
_ Name
f Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
Name -> Context -> Bool
isConName Name
f Context
ctxt = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Context -> Name -> Term -> Bool
guarded Context
ctxt Name
n) [Term]
args
guarded Context
ctxt Name
n (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ Term
t Term
_) Term
sc)
= Context -> Name -> Term -> Bool
guarded Context
ctxt Name
n Term
t Bool -> Bool -> Bool
|| Context -> Name -> Term -> Bool
guarded Context
ctxt Name
n Term
sc
guarded Context
ctxt Name
n Term
_ = Bool
False
blank :: FilePath -> Bool
blank = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace
addLem :: [FilePath]
-> FilePath -> FilePath -> FilePath -> [FilePath] -> FilePath
addLem [FilePath]
before FilePath
tyline FilePath
lem FilePath
lem_app [FilePath]
later
= let ([FilePath]
bef_end, FilePath
blankline : [FilePath]
bef_start)
= case forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Bool
blank) (forall a. [a] -> [a]
reverse [FilePath]
before) of
([FilePath]
bef, []) -> ([FilePath]
bef, [FilePath
""])
([FilePath], [FilePath])
x -> ([FilePath], [FilePath])
x
mvline :: FilePath
mvline = FilePath -> FilePath -> ShowS
updateMeta FilePath
tyline (forall a. Show a => a -> FilePath
show Name
n) FilePath
lem_app in
[FilePath] -> FilePath
unlines forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [FilePath]
bef_start forall a. [a] -> [a] -> [a]
++
[FilePath
blankline, FilePath
lem, FilePath
blankline] forall a. [a] -> [a] -> [a]
++
forall a. [a] -> [a]
reverse [FilePath]
bef_end forall a. [a] -> [a] -> [a]
++ FilePath
mvline forall a. a -> [a] -> [a]
: [FilePath]
later
addProv :: [FilePath] -> FilePath -> FilePath -> [FilePath] -> FilePath
addProv [FilePath]
before FilePath
tyline FilePath
lem_app [FilePath]
later
= let ([FilePath]
later_bef, FilePath
blankline : [FilePath]
later_end)
= case forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Bool
blank) [FilePath]
later of
([FilePath]
bef, []) -> ([FilePath]
bef, [FilePath
""])
([FilePath], [FilePath])
x -> ([FilePath], [FilePath])
x in
[FilePath] -> FilePath
unlines forall a b. (a -> b) -> a -> b
$ [FilePath]
before forall a. [a] -> [a] -> [a]
++ FilePath
tyline forall a. a -> [a] -> [a]
:
([FilePath]
later_bef forall a. [a] -> [a] -> [a]
++ [FilePath
blankline, FilePath
lem_app, FilePath
blankline] forall a. [a] -> [a] -> [a]
++
[FilePath]
later_end)