{-|
Module      : Idris.Interactive
Description : Bits and pieces for editing source files interactively, called from the REPL

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# 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 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, res) <- splitOnLine l n fn
        logLvl 1 (showSep "\n" (map show res))
        let (before, (ap : later)) = splitAt (l-1) (lines src)
        res' <- replaceSplits ap res (not ok)
        let new = [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [FilePath]
res'
        if updatefile
          then do let fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~" -- make a backup!
                  runIO $ writeSource fb (unlines before ++ new ++ unlines later)
                  runIO $ copyFile fb fn
          else -- do iputStrLn (show res)
            iPrintResult new

addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()
addClauseFrom FilePath
fn Bool
updatefile Int
l Name
n = do
    -- if a definition already exists, add missing cases rather than
    -- adding a new definition.
    ist <- Idris IState
getIState
    cl <- getInternalApp fn l
    let fulln = PTerm -> Name
getAppName PTerm
cl
    let 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 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
        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, tyline : later) = splitAt (l-1) (lines src)
        let 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
        cl <- getClause l fulln n fn
        -- add clause before first blank line in 'later'
        let (nonblank, rest) = span (not . all isSpace) (tyline:later)
        if updatefile
          then do let fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
                  runIO $ writeSource fb (unlines (before ++ nonblank) ++
                                        replicate indent ' ' ++
                                        cl ++ "\n" ++
                                        unlines rest)
                  runIO $ copyFile fb fn
          else iPrintResult 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 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, tyline : later) = splitAt (l-1) (lines src)
        let 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
        cl <- getProofClause l n fn
        -- add clause before first blank line in 'later'
        let (nonblank, rest) = span (not . all isSpace) (tyline:later)
        if updatefile
          then do let fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
                  runIO $ writeSource fb (unlines (before ++ nonblank) ++
                                        replicate indent ' ' ++
                                        cl ++ "\n" ++
                                        unlines rest)
                  runIO $ copyFile fb fn
          else iPrintResult 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 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, tyline : later) = splitAt (l-1) (lines src)
        let indent = FilePath -> Int
getIndent FilePath
tyline
        i <- getIState
        cl <- getInternalApp fn l
        let n' = PTerm -> Name
getAppName PTerm
cl

        extras <- case lookupCtxtExact n' (idris_patdefs 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 tms' <- [PTerm] -> Idris [PTerm]
nameMissing [PTerm]
tms
                                           showNew (show n ++ "_rhs") 1 indent tms'
        let (nonblank, rest) = span (not . all isSpace) (tyline:later)
        if updatefile
          then do let fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
                  runIO $ writeSource fb (unlines (before ++ nonblank)
                                        ++ extras
                                        ++ (if null extras then "" else "\n")
                                        ++ unlines rest)
                  runIO $ (length src `seq` copyFile fb fn)
          else iPrintResult 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 (nm', i') <- FilePath -> t -> Idris (FilePath, t)
forall t. (Show t, Num t) => FilePath -> t -> Idris (FilePath, t)
getUniq FilePath
nm t
i
                             rest <- showNew nm i' ind tms
                             return (makeIndent ind ++
                                     showPat tm ++ " = ?" ++ nm' ++
                                     (if null rest then "" else
                                         "\n" ++ 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
  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
  i <- getIState
  indentWith <- getIndentWith
  let (before, tyline : later) = splitAt (l-1) (lines src)
  let ind = FilePath -> Int
getIndent FilePath
tyline
--  runIO . traceIO $ "indentWith = " ++ show indentWith
  let with = FilePath -> Name -> Int -> FilePath
mkWith FilePath
tyline Name
n Int
indentWith
  -- add clause before first blank line in 'later',
  -- or (TODO) before first line with same indentation as tyline
  let (nonblank, rest) = 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)) later
  if updatefile
    then do
      let fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
      runIO $ writeSource fb (unlines (before ++ nonblank) ++
                              with ++ "\n" ++ unlines rest)
      runIO $ copyFile fb fn
    else iPrintResult (with ++ "\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)

-- Replace the given metavariable on the given line with a 'case'
-- block, using a _ for the scrutinee
makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
makeCase :: FilePath -> Bool -> Int -> Name -> Idris ()
makeCase FilePath
fn Bool
updatefile Int
l Name
n
   = do 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, tyline : later) = splitAt (l-1) (lines src)
        let newcase = FilePath -> FilePath -> [FilePath]
addCaseSkel (Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n) FilePath
tyline

        if updatefile then
           do let fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
              runIO $ writeSource fb (unlines (before ++ newcase ++ later))
              runIO $ copyFile fb fn
           else iPrintResult (showSep "\n" newcase ++"\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"

        -- Assume case needs to be bracketed unless the metavariable is
        -- on its own after an =
        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 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, tyline : later) = splitAt (l-1) (lines src)
         ctxt <- getContext
         mn <- case lookupNames n 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)
         i <- getIState
         let (top, envlen, psnames)
              = case lookup mn (idris_metavars 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 = FilePath -> FC
fileFC FilePath
fn
         let 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 = 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) []
         newmv_pre <- idrisCatch
             (do elabDecl' EAll (recinfo (fileFC "proofsearch")) (PClauses fc [] mn [def])
                 (tm, ty) <- elabVal (recinfo (fileFC "proofsearch")) ERHS (PRef fc [] mn)
                 ctxt <- getContext
                 i <- getIState
                 return . flip displayS "" . renderPretty 1.0 80 $
                   pprintPTerm defaultPPOption [] [] (idris_infixes i)
                     (stripNS
                        (dropCtxt envlen
                           (delab i (fst (specialise ctxt [] [(mn, 1)] 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 = 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 updatefile then
            do let fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
               runIO $ writeSource fb (unlines before ++
                                     updateMeta tyline (show n) newmv ++ "\n"
                                       ++ unlines later)
               runIO $ copyFile fb fn
            else iPrintResult 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 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, tyline : later) = splitAt (l-1) (lines src)

        -- if the name is in braces, rather than preceded by a ?, treat it
        -- as a lemma in a provisional definition

        let isProv = FilePath -> FilePath -> Bool
checkProv FilePath
tyline (Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n)

        ctxt <- getContext
        (fname, mty_full) <- case lookupTyName n 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))

        i <- getIState
        let mty = IState -> Term -> Term
errReverse IState
i Term
mty_full

        margs <- case lookup fname (idris_metavars 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 (not isProv) then do
            let skip = IState -> Context -> Term -> [Name]
guessImps IState
i (IState -> Context
tt_ctxt IState
i) Term
mty
            let 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 = IState -> Context -> [Name] -> [Name] -> Term -> [Name]
guessInterfaces IState
i (IState -> Context
tt_ctxt IState
i) [] (PTerm -> [Name]
allNamesIn PTerm
impty) Term
mty

            let 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 = 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 updatefile then
               do let fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
                  runIO $ writeSource fb (addLem before tyline lem lem_app later)
                  runIO $ copyFile fb fn
               else case idris_outputmode 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 -- provisional definition
            let 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 updatefile then
               do let fb = FilePath
fn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"~"
                  runIO $ writeSource fb (addProv before tyline lem_app later)
                  runIO $ copyFile fb fn
               else case idris_outputmode 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" -- keep in type, but not in app
                = 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
_ = []

        -- Guess which binders should be implicits in the generated lemma.
        -- Make them implicit if they appear guarded by a top level constructor,
        -- or at the top level themselves.
        -- Also, make interface implementations implicit
        guessImps :: IState -> Context -> Term -> [Name]
        -- machine names aren't lifted
        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

        -- TMP HACK unusable name so don't lift
        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 ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows
--             | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc
        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)