{-# 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 fn :: FilePath
fn updatefile :: Bool
updatefile l :: Int
l n :: 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
(ok :: Bool
ok, res :: [[(Name, PTerm)]]
res) <- Int -> Name -> FilePath -> Idris (Bool, [[(Name, PTerm)]])
splitOnLine Int
l Name
n FilePath
fn
Int -> FilePath -> Idris ()
logLvl 1 (FilePath -> [FilePath] -> FilePath
showSep "\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 (before :: [FilePath]
before, (ap :: FilePath
ap : later :: [FilePath]
later)) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-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]
++ "~"
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 fn :: FilePath
fn updatefile :: Bool
updatefile l :: Int
l n :: 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
Nothing -> FilePath -> Bool -> Int -> Name -> Idris ()
addMissing FilePath
fn Bool
updatefile Int
l Name
n
Just _ -> 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 (before :: [FilePath]
before, tyline :: FilePath
tyline : later :: [FilePath]
later) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) (FilePath -> [FilePath]
lines FilePath
src)
let indent :: Int
indent = Int -> FilePath -> FilePath -> Int
forall t. Num t => t -> FilePath -> FilePath -> t
getIndent 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 (nonblank :: [FilePath]
nonblank, rest :: [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]
++ "~"
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 ' ' FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
cl FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\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 i :: t
i n :: FilePath
n [] = 0
getIndent i :: t
i n :: FilePath
n xs :: FilePath
xs | Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take 9 FilePath
xs FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== "implementation " = t
i
getIndent i :: t
i n :: FilePath
n xs :: FilePath
xs | Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take (FilePath -> 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 i :: t
i n :: FilePath
n (x :: Char
x : xs :: FilePath
xs) = t -> FilePath -> FilePath -> t
getIndent (t
i t -> t -> t
forall a. Num a => a -> a -> a
+ 1) FilePath
n FilePath
xs
getAppName :: PTerm -> Name
getAppName (PApp _ r :: PTerm
r _) = PTerm -> Name
getAppName PTerm
r
getAppName (PRef _ _ r :: Name
r) = Name
r
getAppName (PTyped n :: PTerm
n _) = PTerm -> Name
getAppName PTerm
n
getAppName _ = Name
n
addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
addProofClauseFrom fn :: FilePath
fn updatefile :: Bool
updatefile l :: Int
l n :: 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 (before :: [FilePath]
before, tyline :: FilePath
tyline : later :: [FilePath]
later) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-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 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 (nonblank :: [FilePath]
nonblank, rest :: [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]
++ "~"
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 ' ' FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
cl FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\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 i :: t
i n :: [a]
n [] = 0
getIndent i :: t
i n :: [a]
n xs :: [a]
xs | Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take ([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 i :: t
i n :: [a]
n (x :: a
x : xs :: [a]
xs) = t -> [a] -> [a] -> t
getIndent (t
i t -> t -> t
forall a. Num a => a -> a -> a
+ 1) [a]
n [a]
xs
addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()
addMissing fn :: FilePath
fn updatefile :: Bool
updatefile l :: Int
l n :: 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 (before :: [FilePath]
before, tyline :: FilePath
tyline : later :: [FilePath]
later) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-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
Nothing -> FilePath -> Idris FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return ""
Just (_, tms :: [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]
++ "_rhs") 1 Int
indent [PTerm]
tms'
let (nonblank :: [FilePath]
nonblank, rest :: [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]
++ "~"
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 (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
extras then "" else "\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 (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 tm :: PTerm
tm = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
dens PTerm
tm where
dens :: PTerm -> PTerm
dens (PRef fc :: FC
fc hls :: [FC]
hls n :: Name
n) = FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
hls (Name -> Name
nsroot Name
n)
dens t :: PTerm
t = PTerm
t
nsroot :: Name -> Name
nsroot (NS n :: Name
n _) = Name -> Name
nsroot Name
n
nsroot (SN (WhereN _ _ n :: Name
n)) = Name -> Name
nsroot Name
n
nsroot n :: Name
n = Name
n
getAppName :: PTerm -> Name
getAppName (PApp _ r :: PTerm
r _) = PTerm -> Name
getAppName PTerm
r
getAppName (PRef _ _ r :: Name
r) = Name
r
getAppName (PTyped n :: PTerm
n _) = PTerm -> Name
getAppName PTerm
n
getAppName _ = Name
n
makeIndent :: Int -> FilePath
makeIndent ind :: Int
ind | ".lidr" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` FilePath
fn = '>' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: ' ' 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
-2) ' '
| Bool
otherwise = Int -> Char -> FilePath
forall a. Int -> a -> [a]
replicate Int
ind ' '
showNew :: FilePath -> t -> Int -> [PTerm] -> Idris FilePath
showNew nm :: FilePath
nm i :: t
i ind :: Int
ind (tm :: PTerm
tm : tms :: [PTerm]
tms)
= do (nm' :: FilePath
nm', i' :: 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 (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
forall a. [a] -> [a] -> [a]
++ FilePath
nm' FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
(if FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
rest then "" else
"\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
rest))
showNew nm :: FilePath
nm i :: t
i _ [] = FilePath -> Idris FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return ""
getIndent :: FilePath -> Int
getIndent s :: FilePath
s = FilePath -> 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 fn :: FilePath
fn updatefile :: Bool
updatefile l :: Int
l n :: 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 (before :: [FilePath]
before, tyline :: FilePath
tyline : later :: [FilePath]
later) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-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 (nonblank :: [FilePath]
nonblank, rest :: [FilePath]
rest) = (FilePath -> Bool) -> [FilePath] -> ([FilePath], [FilePath])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\x :: 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]
++ "~"
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]
++ "\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]
++ "\n")
where getIndent :: FilePath -> Int
getIndent s :: FilePath
s = FilePath -> 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 fn :: FilePath
fn updatefile :: Bool
updatefile l :: Int
l n :: 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 (before :: [FilePath]
before, tyline :: FilePath
tyline : later :: [FilePath]
later) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-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]
++ "~"
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 "\n" [FilePath]
newcase FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++"\n")
where addCaseSkel :: FilePath -> FilePath -> [FilePath]
addCaseSkel n :: FilePath
n line :: 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 -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
n) FilePath
line of
Just (before :: FilePath
before, pos :: Int
pos, after :: FilePath
after) ->
[FilePath
before FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (if Bool
b then "(" else "") FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "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 6 else 5)) (Char -> FilePath
forall a. a -> [a]
repeat ' ') FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"case_val => ?" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (if Bool
b then ")" else "")
FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
after]
Nothing -> FilePath -> [FilePath]
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail "No such metavariable"
brackets :: Bool -> FilePath -> Bool
brackets eq :: Bool
eq line :: FilePath
line | FilePath
line FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== '?' 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 eq :: Bool
eq ('=':ls :: FilePath
ls) = Bool -> FilePath -> Bool
brackets Bool
True FilePath
ls
brackets eq :: Bool
eq (' ':ls :: FilePath
ls) = Bool -> FilePath -> Bool
brackets Bool
eq FilePath
ls
brackets eq :: Bool
eq (l :: Char
l : ls :: FilePath
ls) = Bool -> FilePath -> Bool
brackets Bool
False FilePath
ls
brackets eq :: Bool
eq [] = Bool
True
findSubstr :: [a] -> [a] -> Maybe ([a], t, [a])
findSubstr n :: [a]
n xs :: [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' [] 0 [a]
n [a]
xs
findSubstr' :: [a] -> t -> [a] -> [a] -> Maybe ([a], t, [a])
findSubstr' acc :: [a]
acc i :: t
i n :: [a]
n xs :: [a]
xs | Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take ([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 (t :: * -> *) a. Foldable t => t a -> Int
length [a]
n) [a]
xs)
findSubstr' acc :: [a]
acc i :: t
i n :: [a]
n [] = Maybe ([a], t, [a])
forall a. Maybe a
Nothing
findSubstr' acc :: [a]
acc i :: t
i n :: [a]
n (x :: a
x : xs :: [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
+ 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 fn :: FilePath
fn updatefile :: Bool
updatefile rec :: Bool
rec l :: Int
l n :: Name
n hints :: [Name]
hints 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 20)
doProofSearch fn :: FilePath
fn updatefile :: Bool
updatefile rec :: Bool
rec l :: Int
l n :: Name
n hints :: [Name]
hints (Just depth :: 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 (before :: [FilePath]
before, tyline :: FilePath
tyline : later :: [FilePath]
later) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) (FilePath -> [FilePath]
lines FilePath
src)
Context
ctxt <- Idris Context
getContext
Name
mn <- case Name -> Context -> [Name]
lookupNames Name
n Context
ctxt of
[x :: Name
x] -> Name -> StateT IState (ExceptT Err IO) Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
[] -> Name -> StateT IState (ExceptT Err IO) Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n
ns :: [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 (top :: Maybe Name
top, envlen :: Int
envlen, psnames :: [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 (t :: Maybe Name
t, e :: Int
e, ns :: [Name]
ns, False, d :: Bool
d) -> (Maybe Name
t, Int
e, [Name]
ns)
_ -> (Maybe Name
forall a. Maybe a
Nothing, 0, [])
let fc :: FC
fc = FilePath -> FC
fileFC FilePath
fn
let body :: Maybe Name -> PTerm
body t :: 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 "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])
(tm :: Term
tm, ty :: Term
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabVal (FC -> ElabInfo
recinfo (FilePath -> FC
fileFC "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 (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 "" (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 1.0 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 a. (Eq a, Num a) => a -> 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, 1)] Term
tm))))))
(\e :: Err
e -> FilePath -> Idris FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return ("?" 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]
++ "~"
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]
++ "\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 :: a -> PTerm -> PTerm
dropCtxt 0 sc :: PTerm
sc = PTerm
sc
dropCtxt i :: a
i (PPi _ _ _ _ sc :: PTerm
sc) = a -> PTerm -> PTerm
dropCtxt (a
i a -> a -> a
forall a. Num a => a -> a -> a
- 1) PTerm
sc
dropCtxt i :: a
i (PLet _ _ _ _ _ _ sc :: PTerm
sc) = a -> PTerm -> PTerm
dropCtxt (a
i a -> a -> a
forall a. Num a => a -> a -> a
- 1) PTerm
sc
dropCtxt i :: a
i (PLam _ _ _ _ sc :: PTerm
sc) = a -> PTerm -> PTerm
dropCtxt (a
i a -> a -> a
forall a. Num a => a -> a -> a
- 1) PTerm
sc
dropCtxt _ t :: PTerm
t = PTerm
t
stripNS :: PTerm -> PTerm
stripNS tm :: PTerm
tm = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
dens PTerm
tm where
dens :: PTerm -> PTerm
dens (PRef fc :: FC
fc hls :: [FC]
hls n :: Name
n) = FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
hls (Name -> Name
nsroot Name
n)
dens t :: PTerm
t = PTerm
t
nsroot :: Name -> Name
nsroot (NS n :: Name
n _) = Name -> Name
nsroot Name
n
nsroot (SN (WhereN _ _ n :: Name
n)) = Name -> Name
nsroot Name
n
nsroot n :: Name
n = Name
n
updateMeta :: FilePath -> FilePath -> FilePath -> FilePath
updateMeta ('?':cs :: FilePath
cs) n :: FilePath
n new :: FilePath
new
| FilePath -> 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 (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 (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
n) FilePath
cs of
(mv :: FilePath
mv, c :: Char
c:cs :: FilePath
cs) ->
if ((Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== ')' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '}') 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 -> 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
(mv :: FilePath
mv, []) -> if (FilePath
mv FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
n) then FilePath
new else '?' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
mv
updateMeta ('=':'>':cs :: FilePath
cs) n :: FilePath
n new :: FilePath
new = '='Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:'>'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath -> FilePath -> FilePath -> FilePath
updateMeta FilePath
cs FilePath
n FilePath
new
updateMeta ('=':cs :: FilePath
cs) n :: FilePath
n new :: FilePath
new = '='Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath -> FilePath -> FilePath -> FilePath
updateMeta FilePath
cs FilePath
n FilePath
new
updateMeta (c :: Char
c:cs :: FilePath
cs) n :: FilePath
n new :: FilePath
new
= Char
c Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath -> FilePath -> FilePath -> FilePath
updateMeta FilePath
cs FilePath
n FilePath
new
updateMeta [] n :: FilePath
n new :: FilePath
new = ""
guessBrackets :: Bool -> FilePath -> FilePath -> FilePath -> FilePath
guessBrackets brack :: Bool
brack ('?':cs :: FilePath
cs) n :: FilePath
n new :: FilePath
new
| FilePath -> 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 (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 (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
n) FilePath
cs of
(mv :: FilePath
mv, c :: Char
c:cs :: FilePath
cs) ->
if ((Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== ')' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '}') 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
(mv :: 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 -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
mv
guessBrackets brack :: Bool
brack ('=':'>':cs :: FilePath
cs) n :: FilePath
n new :: FilePath
new = Bool -> FilePath -> FilePath -> FilePath -> FilePath
guessBrackets Bool
False FilePath
cs FilePath
n FilePath
new
guessBrackets brack :: Bool
brack ('-':'>':cs :: FilePath
cs) n :: FilePath
n new :: FilePath
new = Bool -> FilePath -> FilePath -> FilePath -> FilePath
guessBrackets Bool
False FilePath
cs FilePath
n FilePath
new
guessBrackets brack :: Bool
brack ('=':cs :: FilePath
cs) n :: FilePath
n new :: FilePath
new = Bool -> FilePath -> FilePath -> FilePath -> FilePath
guessBrackets Bool
False FilePath
cs FilePath
n FilePath
new
guessBrackets brack :: Bool
brack (c :: Char
c:cs :: FilePath
cs) n :: FilePath
n new :: 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 brack :: Bool
brack [] n :: FilePath
n new :: FilePath
new = ""
checkProv :: FilePath -> FilePath -> Bool
checkProv line :: FilePath
line n :: FilePath
n = Bool -> FilePath -> FilePath -> Bool
isProv' Bool
False FilePath
line FilePath
n
where
isProv' :: Bool -> FilePath -> FilePath -> Bool
isProv' p :: Bool
p cs :: FilePath
cs n :: FilePath
n | Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take (FilePath -> 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' _ ('?':cs :: FilePath
cs) n :: FilePath
n = Bool -> FilePath -> FilePath -> Bool
isProv' Bool
False FilePath
cs FilePath
n
isProv' _ ('{':cs :: FilePath
cs) n :: FilePath
n = Bool -> FilePath -> FilePath -> Bool
isProv' Bool
True FilePath
cs FilePath
n
isProv' _ ('}':cs :: FilePath
cs) n :: FilePath
n = Bool -> FilePath -> FilePath -> Bool
isProv' Bool
True FilePath
cs FilePath
n
isProv' p :: Bool
p (_:cs :: FilePath
cs) n :: FilePath
n = Bool -> FilePath -> FilePath -> Bool
isProv' Bool
p FilePath
cs FilePath
n
isProv' _ [] n :: FilePath
n = Bool
False
addBracket :: Bool -> FilePath -> FilePath
addBracket False new :: FilePath
new = FilePath
new
addBracket True new :: FilePath
new@('(':xs :: FilePath
xs) | FilePath -> Char
forall a. [a] -> a
last FilePath
xs Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== ')' = FilePath
new
addBracket True new :: FilePath
new | (Char -> Bool) -> FilePath -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isSpace FilePath
new = '(' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
new FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ")"
| Bool
otherwise = FilePath
new
makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()
makeLemma fn :: FilePath
fn updatefile :: Bool
updatefile l :: Int
l n :: 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 (before :: [FilePath]
before, tyline :: FilePath
tyline : later :: [FilePath]
later) = Int -> [FilePath] -> ([FilePath], [FilePath])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-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
(fname :: Name
fname, mty_full :: Term
mty_full) <- case Name -> Context -> [(Name, Term)]
lookupTyName Name
n Context
ctxt of
[t :: (Name, Term)
t] -> (Name, Term) -> StateT IState (ExceptT Err IO) (Name, Term)
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)
ns :: [(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 (_, arity :: Int
arity, _, _, _) -> Int -> Idris Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
arity
_ -> Int -> Idris Int
forall (m :: * -> *) a. Monad m => a -> m a
return (-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 a (t :: * -> *).
(Ord a, Num a, Foldable t) =>
t Name -> a -> 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
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 :: Bool
ppopt_pinames = Bool
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 a (t :: * -> *).
(Eq a, Num a, Foldable t) =>
t Name -> a -> 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]
++ "~"
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 _ -> FilePath -> Idris ()
iPrintResult (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath
lem FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
lem_app
IdeMode n :: Integer
n h :: Handle
h ->
let good :: SExp
good = [SExp] -> SExp
SexpList [FilePath -> SExp
SymbolAtom "ok",
[SExp] -> SExp
SexpList [FilePath -> SExp
SymbolAtom "metavariable-lemma",
[SExp] -> SExp
SexpList [FilePath -> SExp
SymbolAtom "replace-metavariable",
FilePath -> SExp
StringAtom FilePath
lem_app],
[SExp] -> SExp
SexpList [FilePath -> SExp
SymbolAtom "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 "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 a (t :: * -> *).
(Eq a, Num a, Foldable t) =>
t Name -> a -> Term -> FilePath
appArgs [] (-1) Term
mty FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
" = ?" 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]
++ "_rhs"
if Bool
updatefile then
do let fb :: FilePath
fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "~"
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 _ -> FilePath -> Idris ()
iPrintResult FilePath
lem_app
IdeMode n :: Integer
n h :: Handle
h ->
let good :: SExp
good = [SExp] -> SExp
SexpList [FilePath -> SExp
SymbolAtom "ok",
[SExp] -> SExp
SexpList [FilePath -> SExp
SymbolAtom "provisional-definition-lemma",
[SExp] -> SExp
SexpList [FilePath -> SExp
SymbolAtom "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 "return" SExp
good Integer
n
where appArgs :: t Name -> a -> Term -> FilePath
appArgs skip :: t Name
skip 0 _ = ""
appArgs skip :: t Name
skip i :: a
i (Bind n :: Name
n@(UN c :: Text
c) (Pi _ _ _ _) sc :: Term
sc)
| (Text -> Char
thead Text
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '_' 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
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 -> a -> Term -> FilePath
appArgs t Name
skip (a
i a -> a -> a
forall a. Num a => a -> a -> a
- 1) Term
sc
appArgs skip :: t Name
skip i :: a
i (Bind _ (Pi _ _ _ _) sc :: Term
sc) = t Name -> a -> Term -> FilePath
appArgs t Name
skip (a
i a -> a -> a
forall a. Num a => a -> a -> a
- 1) Term
sc
appArgs skip :: t Name
skip i :: a
i _ = ""
stripMNBind :: t Name -> a -> PTerm -> PTerm
stripMNBind _ args :: a
args t :: PTerm
t | a
args a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 = PTerm -> PTerm
stripImp PTerm
t
stripMNBind skip :: t Name
skip args :: a
args (PPi b :: Plicity
b n :: Name
n@(UN c :: Text
c) _ ty :: PTerm
ty sc :: 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 4 (Text -> FilePath
str Text
c) FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== "__pi"
= Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
b Name
n FC
NoFC (PTerm -> PTerm
stripImp PTerm
ty) (t Name -> a -> PTerm -> PTerm
stripMNBind t Name
skip (a
args a -> a -> a
forall a. Num a => a -> a -> a
- 1) PTerm
sc)
stripMNBind skip :: t Name
skip args :: a
args (PPi b :: Plicity
b _ _ ty :: PTerm
ty sc :: PTerm
sc) = t Name -> a -> PTerm -> PTerm
stripMNBind t Name
skip (a
args a -> a -> a
forall a. Num a => a -> a -> a
- 1) PTerm
sc
stripMNBind skip :: t Name
skip args :: a
args t :: PTerm
t = PTerm -> PTerm
stripImp PTerm
t
stripImp :: PTerm -> PTerm
stripImp (PApp fc :: FC
fc f :: PTerm
f as :: [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 _ _ _ _ _) = PArg
tm { getTm :: PTerm
getTm = PTerm
Placeholder }
placeholderImp tm :: PArg
tm = PArg
tm { getTm :: PTerm
getTm = PTerm -> PTerm
stripImp (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
tm) }
stripImp (PPi b :: Plicity
b n :: Name
n f :: FC
f ty :: PTerm
ty sc :: 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 t :: PTerm
t = PTerm
t
constraints :: IState -> [Name] -> Type -> String
constraints :: IState -> [Name] -> Term -> FilePath
constraints i :: IState
i [] ty :: Term
ty = ""
constraints i :: IState
i [n :: Name
n] ty :: Term
ty = FilePath -> [FilePath] -> FilePath
showSep ", " (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]
++ " => "
constraints i :: IState
i ns :: [Name]
ns ty :: Term
ty = "(" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> [FilePath] -> FilePath
showSep ", " (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]
++ ") => "
showConstraints :: IState -> t Name -> Term -> [FilePath]
showConstraints i :: IState
i ns :: t Name
ns (Bind n :: Name
n (Pi _ _ ty :: Term
ty _) sc :: Term
sc)
| Name
n Name -> t Name -> 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 _ _ _ = []
guessImps :: IState -> Context -> Term -> [Name]
guessImps :: IState -> Context -> Term -> [Name]
guessImps ist :: IState
ist ctxt :: Context
ctxt (Bind n :: Name
n@(MN _ _) (Pi _ _ ty :: Term
ty _) sc :: Term
sc)
= Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: IState -> Context -> Term -> [Name]
guessImps IState
ist Context
ctxt Term
sc
guessImps ist :: IState
ist ctxt :: Context
ctxt (Bind n :: Name
n (Pi _ _ ty :: Term
ty _) sc :: 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 ist :: IState
ist ctxt :: Context
ctxt _ = []
paramty :: TT n -> Bool
paramty (TType _) = Bool
True
paramty (Bind _ (Pi _ _ (TType _) _) sc :: TT n
sc) = TT n -> Bool
paramty TT n
sc
paramty _ = Bool
False
ignoreName :: a -> Bool
ignoreName n :: a
n = case a -> FilePath
forall a. Show a => a -> FilePath
show a
n of
"_aX" -> Bool
True
_ -> Bool
False
guessInterfaces :: IState -> Context -> [Name] -> [Name] -> Term -> [Name]
guessInterfaces :: IState -> Context -> [Name] -> [Name] -> Term -> [Name]
guessInterfaces ist :: IState
ist ctxt :: Context
ctxt binders :: [Name]
binders usednames :: [Name]
usednames (Bind n :: Name
n (Pi _ _ ty :: Term
ty _) sc :: 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 (\x :: Name
x -> Name -> [Name] -> 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 ist :: IState
ist ctxt :: Context
ctxt _ _ _ = []
paramNames :: [a] -> TT n -> [a]
paramNames bs :: [a]
bs ty :: TT n
ty | (P _ _ _, args :: [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 i :: Int
i : xs :: [TT n]
xs) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
bs = [a]
bs [a] -> Int -> a
forall a. [a] -> Int -> a
!! Int
i a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [TT n] -> [a]
vnames [TT n]
xs
vnames (_ : xs :: [TT n]
xs) = [TT n] -> [a]
vnames [TT n]
xs
isInterface :: IState -> Term -> Bool
isInterface ist :: IState
ist t :: Term
t
| (P _ n :: Name
n _, args :: [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 _ -> Bool
True
_ -> Bool
False
| Bool
otherwise = Bool
False
isParamInterface :: IState -> Term -> Bool
isParamInterface ist :: IState
ist t :: Term
t
| (P _ n :: Name
n _, args :: [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 _ -> (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
_ -> Bool
False
| Bool
otherwise = Bool
False
where isV :: TT n -> Bool
isV (V _) = Bool
True
isV _ = Bool
False
guarded :: Context -> Name -> Term -> Bool
guarded ctxt :: Context
ctxt n :: Name
n (P _ n' :: Name
n' _) | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' = Bool
True
guarded ctxt :: Context
ctxt n :: Name
n ap :: Term
ap@(App _ _ _)
| (P _ f :: Name
f _, args :: [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 ctxt :: Context
ctxt n :: Name
n (Bind _ (Pi _ _ t :: Term
t _) sc :: 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 ctxt :: Context
ctxt n :: Name
n _ = 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 before :: [FilePath]
before tyline :: FilePath
tyline lem :: FilePath
lem lem_app :: FilePath
lem_app later :: [FilePath]
later
= let (bef_end :: [FilePath]
bef_end, blankline :: FilePath
blankline : bef_start :: [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
(bef :: [FilePath]
bef, []) -> ([FilePath]
bef, [""])
x :: ([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 before :: [FilePath]
before tyline :: FilePath
tyline lem_app :: FilePath
lem_app later :: [FilePath]
later
= let (later_bef :: [FilePath]
later_bef, blankline :: FilePath
blankline : later_end :: [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
(bef :: [FilePath]
bef, []) -> ([FilePath]
bef, [""])
x :: ([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)