{-# 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 <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
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" (([(Name, PTerm)] -> FilePath) -> [[(Name, PTerm)]] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map [(Name, PTerm)] -> FilePath
forall a. Show a => a -> FilePath
show [[(Name, PTerm)]]
res))
let ([FilePath]
before, (FilePath
ap : [FilePath]
later)) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall 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 = [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [FilePath]
res'
if Bool
updatefile
then do let fb :: FilePath
fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath
unlines [FilePath]
before FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
new FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
unlines [FilePath]
later)
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
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 = Name
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> Maybe (Maybe Name, Int, [Name], Bool, Bool)
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 <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSourceStrict FilePath
fn
let ([FilePath]
before, FilePath
tyline : [FilePath]
later) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (FilePath -> [FilePath]
lines FilePath
src)
let indent :: Int
indent = Int -> FilePath -> FilePath -> Int
forall {t}. Num t => t -> FilePath -> FilePath -> t
getIndent Int
0 (Name -> FilePath
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) = (FilePath -> Bool) -> [FilePath] -> ([FilePath], [FilePath])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not (Bool -> Bool) -> (FilePath -> Bool) -> FilePath -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> FilePath -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace) (FilePath
tylineFilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
:[FilePath]
later)
if Bool
updatefile
then do let fb :: FilePath
fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath
unlines ([FilePath]
before [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
nonblank) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
Int -> Char -> FilePath
forall a. Int -> a -> [a]
replicate Int
indent Char
' ' FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
cl FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
[FilePath] -> FilePath
unlines [FilePath]
rest)
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
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 | Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take Int
9 FilePath
xs FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
"implementation " = t
i
getIndent t
i FilePath
n FilePath
xs | Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take (FilePath -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
n) FilePath
xs FilePath -> FilePath -> Bool
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 t -> t -> t
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 <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSourceStrict FilePath
fn
let ([FilePath]
before, FilePath
tyline : [FilePath]
later) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (FilePath -> [FilePath]
lines FilePath
src)
let indent :: Int
indent = Int -> FilePath -> FilePath -> Int
forall {t} {a}. (Num t, Eq a) => t -> [a] -> [a] -> t
getIndent Int
0 (Name -> FilePath
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) = (FilePath -> Bool) -> [FilePath] -> ([FilePath], [FilePath])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not (Bool -> Bool) -> (FilePath -> Bool) -> FilePath -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> FilePath -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace) (FilePath
tylineFilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
:[FilePath]
later)
if Bool
updatefile
then do let fb :: FilePath
fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath
unlines ([FilePath]
before [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
nonblank) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
Int -> Char -> FilePath
forall a. Int -> a -> [a]
replicate Int
indent Char
' ' FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
cl FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
[FilePath] -> FilePath
unlines [FilePath]
rest)
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
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 | Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
n) [a]
xs [a] -> [a] -> Bool
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 t -> t -> t
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 <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSourceStrict FilePath
fn
let ([FilePath]
before, FilePath
tyline : [FilePath]
later) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall 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 Name
-> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
-> Maybe ([([(Name, Term)], Term, Term)], [PTerm])
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 -> FilePath -> Idris FilePath
forall a. a -> StateT IState (ExceptT Err IO) a
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
FilePath -> Integer -> Int -> [PTerm] -> Idris FilePath
forall {t}.
(Show t, Num t) =>
FilePath -> t -> Int -> [PTerm] -> Idris FilePath
showNew (Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"_rhs") Integer
1 Int
indent [PTerm]
tms'
let ([FilePath]
nonblank, [FilePath]
rest) = (FilePath -> Bool) -> [FilePath] -> ([FilePath], [FilePath])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not (Bool -> Bool) -> (FilePath -> Bool) -> FilePath -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> FilePath -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace) (FilePath
tylineFilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
:[FilePath]
later)
if Bool
updatefile
then do let fb :: FilePath
fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath
unlines ([FilePath]
before [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
nonblank)
FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
extras
FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (if FilePath -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
extras then FilePath
"" else FilePath
"\n")
FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
unlines [FilePath]
rest)
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ (FilePath -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
src Int -> IO () -> IO ()
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 = PTerm -> FilePath
forall a. Show a => a -> FilePath
show (PTerm -> FilePath) -> (PTerm -> PTerm) -> PTerm -> FilePath
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" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` FilePath
fn = Char
'>' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: Char
' ' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: Int -> Char -> FilePath
forall a. Int -> a -> [a]
replicate (Int
indInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
2) Char
' '
| Bool
otherwise = Int -> Char -> FilePath
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') <- FilePath -> t -> Idris (FilePath, t)
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
FilePath -> Idris FilePath
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> FilePath
makeIndent Int
ind FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
PTerm -> FilePath
showPat PTerm
tm FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" = ?" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
nm' FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
(if FilePath -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
rest then FilePath
"" else
FilePath
"\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
rest))
showNew FilePath
nm t
i Int
_ [] = FilePath -> Idris FilePath
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
""
getIndent :: FilePath -> Int
getIndent FilePath
s = FilePath -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Char -> Bool) -> FilePath -> FilePath
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 <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
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) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall 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) = (FilePath -> Bool) -> [FilePath] -> ([FilePath], [FilePath])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\FilePath
x -> Bool -> Bool
not ((Char -> Bool) -> FilePath -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace FilePath
x) Bool -> Bool -> Bool
&&
Bool -> Bool
not (Int
ind Int -> Int -> Bool
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 FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath
unlines ([FilePath]
before [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
nonblank) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
with FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
unlines [FilePath]
rest)
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
copyFile FilePath
fb FilePath
fn
else FilePath -> Idris ()
iPrintResult (FilePath
with FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n")
where getIndent :: FilePath -> Int
getIndent FilePath
s = FilePath -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Char -> Bool) -> FilePath -> FilePath
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 <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSourceStrict FilePath
fn
let ([FilePath]
before, FilePath
tyline : [FilePath]
later) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (FilePath -> [FilePath]
lines FilePath
src)
let newcase :: [FilePath]
newcase = FilePath -> FilePath -> [FilePath]
addCaseSkel (Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n) FilePath
tyline
if Bool
updatefile then
do let fb :: FilePath
fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath
unlines ([FilePath]
before [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
newcase [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
later))
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
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 FilePath -> FilePath -> FilePath
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 FilePath -> FilePath -> Maybe (FilePath, Int, FilePath)
forall {a} {t}. (Eq a, Num t) => [a] -> [a] -> Maybe ([a], t, [a])
findSubstr (Char
'?'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
n) FilePath
line of
Just (FilePath
before, Int
pos, FilePath
after) ->
[FilePath
before FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (if Bool
b then FilePath
"(" else FilePath
"") FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"case _ of",
Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take (Int
pos Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (if Bool
b then Int
6 else Int
5)) (Char -> FilePath
forall a. a -> [a]
repeat Char
' ') FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
"case_val => ?" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (if Bool
b then FilePath
")" else FilePath
"")
FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
after]
Maybe (FilePath, Int, FilePath)
Nothing -> FilePath -> [FilePath]
forall a. FilePath -> [a]
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail FilePath
"No such metavariable"
brackets :: Bool -> FilePath -> Bool
brackets Bool
eq FilePath
line | FilePath
line FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'?' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: Name -> FilePath
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 = [a] -> t -> [a] -> [a] -> Maybe ([a], t, [a])
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 | Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
n) [a]
xs [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
== [a]
n
= ([a], t, [a]) -> Maybe ([a], t, [a])
forall a. a -> Maybe a
Just ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
acc, t
i, Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
n) [a]
xs)
findSubstr' [a]
acc t
i [a]
n [] = Maybe ([a], t, [a])
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 a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
acc) (t
i t -> t -> t
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 (Int -> Maybe Int
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 <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSourceStrict FilePath
fn
let ([FilePath]
before, FilePath
tyline : [FilePath]
later) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall 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] -> Name -> StateT IState (ExceptT Err IO) Name
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
[] -> Name -> StateT IState (ExceptT Err IO) Name
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n
[Name]
ns -> Err -> StateT IState (ExceptT Err IO) Name
forall a. Err -> Idris a
ierror ([Name] -> Err
forall t. [Name] -> Err' t
CantResolveAlts [Name]
ns)
IState
i <- Idris IState
getIState
let (Maybe Name
top, Int
envlen, [Name]
psnames)
= case Name
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> Maybe (Maybe Name, Int, [Name], Bool, Bool)
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)
_ -> (Maybe Name
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 [PTactic -> PTactic -> PTactic
forall t. PTactic' t -> PTactic' t -> PTactic' t
Try (PTactic -> PTactic -> PTactic
forall t. PTactic' t -> PTactic' t -> PTactic' t
TSeq PTactic
forall t. PTactic' t
Intros (Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic
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))
(Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic
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 = FC
-> Name
-> PTerm
-> [PTerm]
-> PTerm
-> [PDecl' PTerm]
-> PClause' PTerm
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 <- Idris FilePath -> (Err -> Idris FilePath) -> Idris FilePath
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch
(do ElabWhat -> ElabInfo -> PDecl' PTerm -> Idris ()
elabDecl' ElabWhat
EAll (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC FilePath
"proofsearch")) (FC -> FnOpts -> Name -> [PClause' PTerm] -> PDecl' PTerm
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
FilePath -> Idris FilePath
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> Idris FilePath)
-> (Doc OutputAnnotation -> FilePath)
-> Doc OutputAnnotation
-> Idris FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleDoc OutputAnnotation -> FilePath -> FilePath)
-> FilePath -> SimpleDoc OutputAnnotation -> FilePath
forall a b c. (a -> b -> c) -> b -> a -> c
flip SimpleDoc OutputAnnotation -> FilePath -> FilePath
forall a. SimpleDoc a -> FilePath -> FilePath
displayS FilePath
"" (SimpleDoc OutputAnnotation -> FilePath)
-> (Doc OutputAnnotation -> SimpleDoc OutputAnnotation)
-> Doc OutputAnnotation
-> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Float -> Int -> Doc OutputAnnotation -> SimpleDoc OutputAnnotation
forall a. Float -> Int -> Doc a -> SimpleDoc a
renderPretty Float
1.0 Int
80 (Doc OutputAnnotation -> Idris FilePath)
-> Doc OutputAnnotation -> Idris FilePath
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
(Int -> PTerm -> PTerm
forall {t}. (Eq t, Num t) => t -> PTerm -> PTerm
dropCtxt Int
envlen
(IState -> Term -> PTerm
delab IState
i ((Term, [(Name, Int)]) -> Term
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 -> FilePath -> Idris FilePath
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath
"?" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n))
let newmv :: FilePath
newmv = Bool -> FilePath -> FilePath -> FilePath -> FilePath
guessBrackets Bool
False FilePath
tyline (Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n) FilePath
newmv_pre
if Bool
updatefile then
do let fb :: FilePath
fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeSource FilePath
fb ([FilePath] -> FilePath
unlines [FilePath]
before FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath -> FilePath -> FilePath -> FilePath
updateMeta FilePath
tyline (Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n) FilePath
newmv FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n"
FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
unlines [FilePath]
later)
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
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 t -> t -> t
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 t -> t -> t
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 t -> t -> t
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 -> FilePath -> FilePath
updateMeta (Char
'?':FilePath
cs) FilePath
n FilePath
new
| FilePath -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
cs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= FilePath -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
n
= case Int -> FilePath -> (FilePath, FilePath)
forall a. Int -> [a] -> ([a], [a])
splitAt (FilePath -> Int
forall a. [a] -> Int
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 Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'}') Bool -> Bool -> Bool
&& FilePath
mv FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
n)
then FilePath
new FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Char
c Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
cs)
else Char
'?' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
mv FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Char
c Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath -> FilePath -> FilePath -> FilePath
updateMeta FilePath
cs FilePath
n FilePath
new
(FilePath
mv, []) -> if (FilePath
mv FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
n) then FilePath
new else Char
'?' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
mv
updateMeta (Char
'=':Char
'>':FilePath
cs) FilePath
n FilePath
new = Char
'='Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:Char
'>'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath -> FilePath -> FilePath -> FilePath
updateMeta FilePath
cs FilePath
n FilePath
new
updateMeta (Char
'=':FilePath
cs) FilePath
n FilePath
new = Char
'='Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath -> FilePath -> FilePath -> FilePath
updateMeta FilePath
cs FilePath
n FilePath
new
updateMeta (Char
c:FilePath
cs) FilePath
n FilePath
new
= Char
c Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath -> FilePath -> FilePath -> FilePath
updateMeta FilePath
cs FilePath
n FilePath
new
updateMeta [] FilePath
n FilePath
new = FilePath
""
guessBrackets :: Bool -> FilePath -> FilePath -> FilePath -> FilePath
guessBrackets Bool
brack (Char
'?':FilePath
cs) FilePath
n FilePath
new
| FilePath -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
cs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= FilePath -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
n
= case Int -> FilePath -> (FilePath, FilePath)
forall a. Int -> [a] -> ([a], [a])
splitAt (FilePath -> Int
forall a. [a] -> Int
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 Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'}') Bool -> Bool -> Bool
&& FilePath
mv FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
n)
then Bool -> FilePath -> FilePath
addBracket Bool
brack FilePath
new
else Bool -> FilePath -> FilePath -> FilePath -> FilePath
guessBrackets Bool
True FilePath
cs FilePath
n FilePath
new
(FilePath
mv, []) -> if (FilePath
mv FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
n) then Bool -> FilePath -> FilePath
addBracket Bool
brack FilePath
new else Char
'?' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
mv
guessBrackets Bool
brack (Char
'=':Char
'>':FilePath
cs) FilePath
n FilePath
new = Bool -> FilePath -> FilePath -> FilePath -> FilePath
guessBrackets Bool
False FilePath
cs FilePath
n FilePath
new
guessBrackets Bool
brack (Char
'-':Char
'>':FilePath
cs) FilePath
n FilePath
new = Bool -> FilePath -> FilePath -> FilePath -> FilePath
guessBrackets Bool
False FilePath
cs FilePath
n FilePath
new
guessBrackets Bool
brack (Char
'=':FilePath
cs) FilePath
n FilePath
new = Bool -> FilePath -> FilePath -> FilePath -> FilePath
guessBrackets Bool
False FilePath
cs FilePath
n FilePath
new
guessBrackets Bool
brack (Char
c:FilePath
cs) FilePath
n FilePath
new
= Bool -> FilePath -> FilePath -> FilePath -> FilePath
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 | Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take (FilePath -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
n) FilePath
cs FilePath -> FilePath -> Bool
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 -> FilePath -> FilePath
addBracket Bool
False FilePath
new = FilePath
new
addBracket Bool
True new :: FilePath
new@(Char
'(':FilePath
xs) | FilePath -> Char
forall a. HasCallStack => [a] -> a
last FilePath
xs Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')' = FilePath
new
addBracket Bool
True FilePath
new | (Char -> Bool) -> FilePath -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace FilePath
new = Char
'(' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
new FilePath -> FilePath -> FilePath
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 <- IO FilePath -> Idris FilePath
forall a. IO a -> Idris a
runIO (IO FilePath -> Idris FilePath) -> IO FilePath -> Idris FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readSourceStrict FilePath
fn
let ([FilePath]
before, FilePath
tyline : [FilePath]
later) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (FilePath -> [FilePath]
lines FilePath
src)
let isProv :: Bool
isProv = FilePath -> FilePath -> Bool
checkProv FilePath
tyline (Name -> FilePath
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] -> (Name, Term) -> StateT IState (ExceptT Err IO) (Name, Term)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name, Term)
t
[] -> Err -> StateT IState (ExceptT Err IO) (Name, Term)
forall a. Err -> Idris a
ierror (Name -> Err
forall t. Name -> Err' t
NoSuchVariable Name
n)
[(Name, Term)]
ns -> Err -> StateT IState (ExceptT Err IO) (Name, Term)
forall a. Err -> Idris a
ierror ([Name] -> Err
forall t. [Name] -> Err' t
CantResolveAlts (((Name, Term) -> Name) -> [(Name, Term)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Term) -> Name
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 Name
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
-> Maybe (Maybe Name, Int, [Name], Bool, Bool)
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
_) -> Int -> Idris Int
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
arity
Maybe (Maybe Name, Int, [Name], Bool, Bool)
_ -> Int -> Idris Int
forall a. a -> StateT IState (ExceptT Err IO) a
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 = [Name] -> Int -> PTerm -> PTerm
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 = Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" : " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
IState -> [Name] -> Term -> FilePath
constraints IState
i [Name]
interfaces Term
mty FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
PPOption -> PTerm -> FilePath
showTmOpts (PPOption
defaultPPOption { ppopt_pinames = True })
PTerm
impty
let lem_app :: FilePath
lem_app = Bool -> FilePath -> FilePath -> FilePath -> FilePath
guessBrackets Bool
False FilePath
tyline (Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n) (Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Name] -> Int -> Term -> FilePath
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 FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
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)
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
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 -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
lem FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n" FilePath -> FilePath -> FilePath
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 IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (FilePath -> IO ()) -> FilePath -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> SExp -> Integer -> FilePath
forall a. SExpable a => FilePath -> a -> Integer -> FilePath
convSExp FilePath
"return" SExp
good Integer
n
else do
let lem_app :: FilePath
lem_app = Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Name] -> Integer -> Term -> FilePath
forall {t} {t :: * -> *}.
(Eq t, Num t, Foldable t) =>
t Name -> t -> Term -> FilePath
appArgs [] (-Integer
1) Term
mty FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
" = ?" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"_rhs"
if Bool
updatefile then
do let fb :: FilePath
fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
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)
IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
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 IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> (FilePath -> IO ()) -> FilePath -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> FilePath -> IO ()
hPutStrLn Handle
h (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> SExp -> Integer -> FilePath
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 Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'_' Bool -> Bool -> Bool
&& Name
n Name -> t Name -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t Name
skip)
= FilePath
" " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ t Name -> t -> Term -> FilePath
appArgs t Name
skip (t
i t -> t -> t
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 t -> t -> t
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 t -> t -> Bool
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 Name -> t Name -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t Name
skip Bool -> Bool -> Bool
||
Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take Int
4 (Text -> FilePath
str Text
c) FilePath -> FilePath -> Bool
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 t -> t -> t
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 t -> t -> t
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) ((PArg -> PArg) -> [PArg] -> [PArg]
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 = Placeholder }
placeholderImp PArg
tm = PArg
tm { getTm = stripImp (getTm 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
", " (IState -> [Name] -> Term -> [FilePath]
forall {t :: * -> *}.
Foldable t =>
IState -> t Name -> Term -> [FilePath]
showConstraints IState
i [Name
n] Term
ty) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" => "
constraints IState
i [Name]
ns Term
ty = FilePath
"(" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> [FilePath] -> FilePath
showSep FilePath
", " (IState -> [Name] -> Term -> [FilePath]
forall {t :: * -> *}.
Foldable t =>
IState -> t Name -> Term -> [FilePath]
showConstraints IState
i [Name]
ns Term
ty) FilePath -> FilePath -> FilePath
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 Name -> t Name -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
ns = PTerm -> FilePath
forall a. Show a => a -> FilePath
show (IState -> Term -> PTerm
delab IState
i Term
ty) FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
:
IState -> t Name -> Term -> [FilePath]
showConstraints IState
i t Name
ns (Term -> Term -> Term
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
forall n. TT n
Erased) Term
sc)
| Bool
otherwise = IState -> t Name -> Term -> [FilePath]
showConstraints IState
i t Name
ns (Term -> Term -> Term
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
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 Name -> [Name] -> [Name]
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 (Term -> Term -> Term
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
forall n. TT n
Erased) Term
sc)
= Name
n Name -> [Name] -> [Name]
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 Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: IState -> Context -> Term -> [Name]
guessImps IState
ist Context
ctxt Term
sc
| Term -> Bool
forall {n}. TT n -> Bool
paramty Term
ty = Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: IState -> Context -> Term -> [Name]
guessImps IState
ist Context
ctxt Term
sc
| Name -> Bool
forall {a}. Show a => a -> Bool
ignoreName Name
n = Name
n Name -> [Name] -> [Name]
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 a -> FilePath
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
&& (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Name
x -> Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Name
x [Name]
usednames)
([Name] -> Term -> [Name]
forall {a} {n}. [a] -> TT n -> [a]
paramNames [Name]
binders Term
ty)
= Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: IState -> Context -> [Name] -> [Name] -> Term -> [Name]
guessInterfaces IState
ist Context
ctxt (Name
n Name -> [Name] -> [Name]
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 Name -> [Name] -> [Name]
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) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
ty
= [TT n] -> [a]
forall {n}. [TT n] -> [a]
vnames [TT n]
args
where vnames :: [TT n] -> [a]
vnames [] = []
vnames (V Int
i : [TT n]
xs) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
bs = [a]
bs [a] -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!! Int
i a -> [a] -> [a]
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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
t
= case Name -> Ctxt InterfaceInfo -> Maybe InterfaceInfo
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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
t
= case Name -> Ctxt InterfaceInfo -> Maybe InterfaceInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
Just InterfaceInfo
_ -> (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Term -> Bool
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 Name -> Name -> Bool
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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ap,
Name -> Context -> Bool
isConName Name
f Context
ctxt = (Term -> Bool) -> [Term] -> Bool
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 = (Char -> Bool) -> FilePath -> Bool
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 (FilePath -> Bool) -> [FilePath] -> ([FilePath], [FilePath])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not (Bool -> Bool) -> (FilePath -> Bool) -> FilePath -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Bool
blank) ([FilePath] -> [FilePath]
forall a. [a] -> [a]
reverse [FilePath]
before) of
([FilePath]
bef, []) -> ([FilePath]
bef, [FilePath
""])
([FilePath], [FilePath])
x -> ([FilePath], [FilePath])
x
mvline :: FilePath
mvline = FilePath -> FilePath -> FilePath -> FilePath
updateMeta FilePath
tyline (Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n) FilePath
lem_app in
[FilePath] -> FilePath
unlines ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> [FilePath]
forall a. [a] -> [a]
reverse [FilePath]
bef_start [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++
[FilePath
blankline, FilePath
lem, FilePath
blankline] [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++
[FilePath] -> [FilePath]
forall a. [a] -> [a]
reverse [FilePath]
bef_end [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ FilePath
mvline FilePath -> [FilePath] -> [FilePath]
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 (FilePath -> Bool) -> [FilePath] -> ([FilePath], [FilePath])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not (Bool -> Bool) -> (FilePath -> Bool) -> FilePath -> Bool
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 ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath]
before [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ FilePath
tyline FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
:
([FilePath]
later_bef [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath
blankline, FilePath
lem_app, FilePath
blankline] [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++
[FilePath]
later_end)