{-|
Module      : Idris.CaseSplit
Description : Module to provide case split functionality.

License     : BSD3
Maintainer  : The Idris Community.

Given a pattern clause and a variable 'n', elaborate the clause and find the
type of 'n'.

Make new pattern clauses by replacing 'n' with all the possibly constructors
applied to '_', and replacing all other variables with '_' in order to
resolve other dependencies.

Finally, merge the generated patterns with the original, by matching.
Always take the "more specific" argument when there is a discrepancy, i.e.
names over '_', patterns over names, etc.
-}

{-# LANGUAGE FlexibleContexts, PatternGuards #-}

module Idris.CaseSplit(
    splitOnLine, replaceSplits
  , getClause, getProofClause
  , mkWith
  , nameMissing
  , getUniq, nameRoot
  ) where

import Idris.AbsSyntax
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.Output
import Idris.Parser

import Control.Monad
import Control.Monad.State.Strict
import Data.Char
import Data.List (isPrefixOf, isSuffixOf)

-- | Given a variable to split, and a term application, return a list
-- of variable updates, paired with a flag to say whether the given
-- update typechecks (False = impossible) if the flag is 'False' the
-- splits should be output with the 'impossible' flag, otherwise they
-- should be output as normal
split :: Name -> PTerm -> Idris (Bool, [[(Name, PTerm)]])
split :: Name -> PTerm -> Idris (Bool, [[(Name, PTerm)]])
split Name
n PTerm
t'
   = do IState
ist <- Idris IState
getIState
        -- Make sure all the names in the term are accessible
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Name
n -> Name -> Accessibility -> StateT IState (ExceptT Err IO) ()
setAccessibility Name
n Accessibility
Public) (PTerm -> [Name]
allNamesIn PTerm
t')
        -- ETyDecl rather then ELHS because there'll be explicit type
        -- matching
        (Term
tm, Term
ty, [(Name, Term)]
pats) <- ElabInfo
-> ElabMode -> Bool -> PTerm -> Idris (Term, Term, [(Name, Term)])
elabValBind (FC -> ElabInfo
recinfo (String -> FC
fileFC String
"casesplit")) ElabMode
ETyDecl Bool
True (IState -> PTerm -> PTerm
addImplPat IState
ist PTerm
t')
        -- ASSUMPTION: tm is in normal form after elabValBind, so we don't
        -- need to do anything special to find out what family each argument
        -- is in
        Int -> String -> StateT IState (ExceptT Err IO) ()
logElab Int
4 (String
"Elaborated:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm forall a. [a] -> [a] -> [a]
++ String
" : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
ty forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, Term)]
pats)
--         iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
--         iputStrLn (show pats)
        let t :: PTerm
t = PTerm -> PTerm -> PTerm
mergeUserImpl (IState -> PTerm -> PTerm
addImplPat IState
ist PTerm
t') (IState -> Term -> PTerm
delabDirect IState
ist Term
tm)
        let ctxt :: Context
ctxt = IState -> Context
tt_ctxt IState
ist
        case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Term)]
pats of
             Maybe Term
Nothing -> forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" is not a pattern variable"
             Just Term
ty ->
                do let splits :: [PTerm]
splits = IState -> Term -> [PTerm]
findPats IState
ist Term
ty
                   Int -> String -> StateT IState (ExceptT Err IO) ()
logElab Int
1 (String
"New patterns " forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
", "
                         (forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
splits))
                   let newPats_in :: [PTerm]
newPats_in = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Context -> Name -> PTerm -> PTerm -> PTerm
replaceVar Context
ctxt Name
n) [PTerm]
splits (forall a. a -> [a]
repeat PTerm
t)
                   Int -> String -> StateT IState (ExceptT Err IO) ()
logElab Int
4 (String
"Working from " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
t)
                   Int -> String -> StateT IState (ExceptT Err IO) ()
logElab Int
4 (String
"Trying " forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n"
                               (forall a b. (a -> b) -> [a] -> [b]
map (PTerm -> String
showTmImpls) [PTerm]
newPats_in))
                   [(Bool, PTerm)]
newPats_in <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PTerm -> Idris (Bool, PTerm)
elabNewPat [PTerm]
newPats_in
                   case forall {a}. [a] -> [a] -> [(Bool, a)] -> Either [a] [a]
anyValid [] [] [(Bool, PTerm)]
newPats_in of
                        Left [PTerm]
fails -> do
                           let fails' :: [(PTerm, [(Name, PTerm)])]
fails' = IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
mergeAllPats IState
ist Name
n PTerm
t [PTerm]
fails
                           forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(PTerm, [(Name, PTerm)])]
fails'))
                        Right [PTerm]
newPats -> do
                           Int -> String -> StateT IState (ExceptT Err IO) ()
logElab Int
3 (String
"Original:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PTerm
t)
                           Int -> String -> StateT IState (ExceptT Err IO) ()
logElab Int
3 (String
"Split:\n" forall a. [a] -> [a] -> [a]
++
                                      (String -> [String] -> String
showSep String
"\n" (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [PTerm]
newPats)))
                           Int -> String -> StateT IState (ExceptT Err IO) ()
logElab Int
3 String
"----"
                           let newPats' :: [(PTerm, [(Name, PTerm)])]
newPats' = IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
mergeAllPats IState
ist Name
n PTerm
t [PTerm]
newPats
                           Int -> String -> StateT IState (ExceptT Err IO) ()
logElab Int
1 (String
"Name updates " forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n"
                                 (forall a b. (a -> b) -> [a] -> [b]
map (\ (PTerm
p, [(Name, PTerm)]
u) -> forall a. Show a => a -> String
show [(Name, PTerm)]
u forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PTerm
p) [(PTerm, [(Name, PTerm)])]
newPats'))
                           forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(PTerm, [(Name, PTerm)])]
newPats'))
   where
     anyValid :: [a] -> [a] -> [(Bool, a)] -> Either [a] [a]
anyValid [a]
ok [a]
bad [] = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
ok then forall a b. a -> Either a b
Left (forall a. [a] -> [a]
reverse [a]
bad)
                                     else forall a b. b -> Either a b
Right (forall a. [a] -> [a]
reverse [a]
ok)
     anyValid [a]
ok [a]
bad ((Bool
tc, a
p) : [(Bool, a)]
ps)
         | Bool
tc = [a] -> [a] -> [(Bool, a)] -> Either [a] [a]
anyValid (a
p forall a. a -> [a] -> [a]
: [a]
ok) [a]
bad [(Bool, a)]
ps
         | Bool
otherwise = [a] -> [a] -> [(Bool, a)] -> Either [a] [a]
anyValid [a]
ok (a
p forall a. a -> [a] -> [a]
: [a]
bad) [(Bool, a)]
ps

data MergeState = MS { MergeState -> [(Name, Name)]
namemap :: [(Name, Name)],
                       MergeState -> [(Name, Name)]
invented :: [(Name, Name)],
                       MergeState -> [Name]
explicit :: [Name],
                       MergeState -> [(Name, PTerm)]
updates :: [(Name, PTerm)] }

addUpdate :: Name -> PTerm -> State MergeState ()
addUpdate :: Name -> PTerm -> State MergeState ()
addUpdate Name
n PTerm
tm = do MergeState
ms <- forall s (m :: * -> *). MonadState s m => m s
get
                    forall s (m :: * -> *). MonadState s m => s -> m ()
put (MergeState
ms { updates :: [(Name, PTerm)]
updates = ((Name
n, PTerm -> PTerm
stripNS PTerm
tm) forall a. a -> [a] -> [a]
: MergeState -> [(Name, PTerm)]
updates MergeState
ms) } )

inventName :: IState -> Maybe Name -> Name -> State MergeState Name
inventName :: IState -> Maybe Name -> Name -> State MergeState Name
inventName IState
ist Maybe Name
ty Name
n =
    do MergeState
ms <- forall s (m :: * -> *). MonadState s m => m s
get
       let supp :: [Name]
supp = case Maybe Name
ty of
                       Maybe Name
Nothing -> []
                       Just Name
t -> IState -> Name -> [Name]
getNameHints IState
ist Name
t
       let nsupp :: [Name]
nsupp = case Name
n of
                        MN Int
i Text
n | Bool -> Bool
not (Text -> Bool
tnull Text
n) Bool -> Bool -> Bool
&& Text -> Char
thead Text
n forall a. Eq a => a -> a -> Bool
== Char
'_'
                               -> [Name] -> [Name]
mkSupply ([Name]
supp forall a. [a] -> [a] -> [a]
++ [Name]
varlist)
                        MN Int
i Text
n -> [Name] -> [Name]
mkSupply (Text -> Name
UN Text
n forall a. a -> [a] -> [a]
: [Name]
supp forall a. [a] -> [a] -> [a]
++ [Name]
varlist)
                        UN Text
n | Text -> Char
thead Text
n forall a. Eq a => a -> a -> Bool
== Char
'_'
                               -> [Name] -> [Name]
mkSupply ([Name]
supp forall a. [a] -> [a] -> [a]
++ [Name]
varlist)
                        Name
x -> [Name] -> [Name]
mkSupply (Name
x forall a. a -> [a] -> [a]
: [Name]
supp)
       let badnames :: [Name]
badnames = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (MergeState -> [(Name, Name)]
namemap MergeState
ms) forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (MergeState -> [(Name, Name)]
invented MergeState
ms) forall a. [a] -> [a] -> [a]
++
                      MergeState -> [Name]
explicit MergeState
ms
       case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (MergeState -> [(Name, Name)]
invented MergeState
ms) of
          Just Name
n' -> forall (m :: * -> *) a. Monad m => a -> m a
return Name
n'
          Maybe Name
Nothing ->
             do let n' :: Name
n' = [Name] -> [Name] -> Name
uniqueNameFrom [Name]
nsupp [Name]
badnames
                forall s (m :: * -> *). MonadState s m => s -> m ()
put (MergeState
ms { invented :: [(Name, Name)]
invented = (Name
n, Name
n') forall a. a -> [a] -> [a]
: MergeState -> [(Name, Name)]
invented MergeState
ms })
                forall (m :: * -> *) a. Monad m => a -> m a
return Name
n'

mkSupply :: [Name] -> [Name]
mkSupply :: [Name] -> [Name]
mkSupply [Name]
ns = [Name] -> [Name] -> [Name]
mkSupply' [Name]
ns (forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
nextName [Name]
ns)
  where mkSupply' :: [Name] -> [Name] -> [Name]
mkSupply' [Name]
xs [Name]
ns' = [Name]
xs forall a. [a] -> [a] -> [a]
++ [Name] -> [Name]
mkSupply [Name]
ns'

varlist :: [Name]
varlist :: [Name]
varlist = forall a b. (a -> b) -> [a] -> [b]
map (String -> Name
sUN forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[])) String
"xyzwstuv" -- EB's personal preference :)

stripNS :: PTerm -> PTerm
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

mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
mergeAllPats IState
ist Name
cv PTerm
t [] = []
mergeAllPats IState
ist Name
cv PTerm
t (PTerm
p : [PTerm]
ps)
    = let (PTerm
p', MS [(Name, Name)]
_ [(Name, Name)]
_ [Name]
_ [(Name, PTerm)]
u) = forall s a. State s a -> s -> (a, s)
runState (IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
mergePat IState
ist PTerm
t PTerm
p forall a. Maybe a
Nothing)
                                      ([(Name, Name)]
-> [(Name, Name)] -> [Name] -> [(Name, PTerm)] -> MergeState
MS [] [] (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/=Name
cv) (PTerm -> [Name]
patvars PTerm
t)) [])
          ps' :: [(PTerm, [(Name, PTerm)])]
ps' = IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
mergeAllPats IState
ist Name
cv PTerm
t [PTerm]
ps in
          ((PTerm
p', [(Name, PTerm)]
u) forall a. a -> [a] -> [a]
: [(PTerm, [(Name, PTerm)])]
ps')
  where patvars :: PTerm -> [Name]
patvars (PRef FC
_ [FC]
_ Name
n) = [Name
n]
        patvars (PApp FC
_ PTerm
_ [PArg]
as) = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (PTerm -> [Name]
patvars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. PArg' t -> t
getTm) [PArg]
as
        patvars (PPatvar FC
_ Name
n) = [Name
n]
        patvars PTerm
_ = []

mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
mergePat IState
ist PTerm
orig PTerm
new Maybe Name
t =
    do -- collect user names for name map, by matching user pattern against
       -- the generated pattern
       case IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause IState
ist PTerm
orig PTerm
new of
            Left (PTerm, PTerm)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Right [(Name, PTerm)]
ns -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {m :: * -> *}.
MonadState MergeState m =>
(Name, PTerm) -> m ()
addNameMap [(Name, PTerm)]
ns
       IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
mergePat' IState
ist PTerm
orig PTerm
new Maybe Name
t
  where
    addNameMap :: (Name, PTerm) -> m ()
addNameMap (Name
n, PRef FC
fc [FC]
_ Name
n') = do MergeState
ms <- forall s (m :: * -> *). MonadState s m => m s
get
                                      forall s (m :: * -> *). MonadState s m => s -> m ()
put (MergeState
ms { namemap :: [(Name, Name)]
namemap = ((Name
n', Name
n) forall a. a -> [a] -> [a]
: MergeState -> [(Name, Name)]
namemap MergeState
ms) })
    addNameMap (Name, PTerm)
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | If any names are unified, make sure they stay unified. Always
-- prefer user provided name (first pattern)
mergePat' :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
mergePat' IState
ist (PPatvar FC
fc Name
n) PTerm
new Maybe Name
t
  = IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
mergePat' IState
ist (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) PTerm
new Maybe Name
t
mergePat' IState
ist PTerm
old (PPatvar FC
fc Name
n) Maybe Name
t
  = IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
mergePat' IState
ist PTerm
old (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) Maybe Name
t
mergePat' IState
ist orig :: PTerm
orig@(PRef FC
fc [FC]
_ Name
n) new :: PTerm
new@(PRef FC
_ [FC]
_ Name
n') Maybe Name
t
  | Name -> Context -> Bool
isDConName Name
n' (IState -> Context
tt_ctxt IState
ist) = do Name -> PTerm -> State MergeState ()
addUpdate Name
n PTerm
new
                                     forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
new
  | Bool
otherwise
    = do MergeState
ms <- forall s (m :: * -> *). MonadState s m => m s
get
         case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n' (MergeState -> [(Name, Name)]
namemap MergeState
ms) of
              Just Name
x -> do Name -> PTerm -> State MergeState ()
addUpdate Name
n (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
x)
                           forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
x)
              Maybe Name
Nothing -> do forall s (m :: * -> *). MonadState s m => s -> m ()
put (MergeState
ms { namemap :: [(Name, Name)]
namemap = ((Name
n', Name
n) forall a. a -> [a] -> [a]
: MergeState -> [(Name, Name)]
namemap MergeState
ms) })
                            forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n)
mergePat' IState
ist (PApp FC
_ PTerm
_ [PArg]
args) (PApp FC
fc PTerm
f [PArg]
args') Maybe Name
t
      = do [PArg]
newArgs <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM PArg -> (PArg, Maybe Name) -> StateT MergeState Identity PArg
mergeArg [PArg]
args (forall a b. [a] -> [b] -> [(a, b)]
zip [PArg]
args' (IState -> PTerm -> [Maybe Name]
argTys IState
ist PTerm
f))
           forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f [PArg]
newArgs)
   where mergeArg :: PArg -> (PArg, Maybe Name) -> StateT MergeState Identity PArg
mergeArg PArg
x (PArg
y, Maybe Name
t)
              = do PTerm
tm' <- IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
mergePat' IState
ist (forall t. PArg' t -> t
getTm PArg
x) (forall t. PArg' t -> t
getTm PArg
y) Maybe Name
t
                   case PArg
x of
                        (PImp Int
_ Bool
_ [ArgOpt]
_ Name
_ PTerm
_) ->
                             forall (m :: * -> *) a. Monad m => a -> m a
return (PArg
y { machine_inf :: Bool
machine_inf = forall t. PArg' t -> Bool
machine_inf PArg
x,
                                         getTm :: PTerm
getTm = PTerm
tm' })
                        PArg
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (PArg
y { getTm :: PTerm
getTm = PTerm
tm' })
mergePat' IState
ist (PRef FC
fc [FC]
_ Name
n) PTerm
tm Maybe Name
ty = do PTerm
tm <- IState -> PTerm -> Maybe Name -> State MergeState PTerm
tidy IState
ist PTerm
tm Maybe Name
ty
                                       Name -> PTerm -> State MergeState ()
addUpdate Name
n PTerm
tm
                                       forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
tm
mergePat' IState
ist PTerm
x PTerm
y Maybe Name
t = forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
y

mergeUserImpl :: PTerm -> PTerm -> PTerm
mergeUserImpl :: PTerm -> PTerm -> PTerm
mergeUserImpl PTerm
x PTerm
y = PTerm
x

argTys :: IState -> PTerm -> [Maybe Name]
argTys :: IState -> PTerm -> [Maybe Name]
argTys IState
ist (PRef FC
fc [FC]
hls Name
n)
    = case Name -> Context -> [Term]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
           [Term
ty] -> let ty' :: Term
ty' = Context -> Env -> Term -> Term
normalise (IState -> Context
tt_ctxt IState
ist) [] Term
ty in
                       forall a b. (a -> b) -> [a] -> [b]
map (Term -> Maybe Name
tyName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall n. TT n -> [(n, TT n)]
getArgTys Term
ty') forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat forall a. Maybe a
Nothing
           [Term]
_ -> forall a. a -> [a]
repeat forall a. Maybe a
Nothing
  where tyName :: Term -> Maybe Name
tyName (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ Term
_ Term
_) Term
_) = forall a. a -> Maybe a
Just (String -> Name
sUN String
"->")
        tyName Term
t | (P NameType
_ Name
d Term
_, [Term
_, Term
ty]) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t,
                   Name
d forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"Delayed" = Term -> Maybe Name
tyName Term
ty
                 | (P NameType
_ Name
n Term
_, [Term]
_) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t = forall a. a -> Maybe a
Just Name
n
                 | Bool
otherwise = forall a. Maybe a
Nothing
argTys IState
_ PTerm
_ = forall a. a -> [a]
repeat forall a. Maybe a
Nothing

tidy :: IState -> PTerm -> Maybe Name -> State MergeState PTerm
tidy :: IState -> PTerm -> Maybe Name -> State MergeState PTerm
tidy IState
ist orig :: PTerm
orig@(PRef FC
fc [FC]
hls Name
n) Maybe Name
ty
     = do MergeState
ms <- forall s (m :: * -> *). MonadState s m => m s
get
          case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (MergeState -> [(Name, Name)]
namemap MergeState
ms) of
               Just Name
x -> forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
x)
               Maybe Name
Nothing -> case Name
n of
                               (UN Text
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
orig
                               Name
_ -> do Name
n' <- IState -> Maybe Name -> Name -> State MergeState Name
inventName IState
ist Maybe Name
ty Name
n
                                       forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n')
tidy IState
ist (PApp FC
fc PTerm
f [PArg]
args) Maybe Name
ty
     = do [PArg]
args' <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM PArg -> Maybe Name -> StateT MergeState Identity PArg
tidyArg [PArg]
args (IState -> PTerm -> [Maybe Name]
argTys IState
ist PTerm
f)
          forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f [PArg]
args')
    where tidyArg :: PArg -> Maybe Name -> StateT MergeState Identity PArg
tidyArg PArg
x Maybe Name
ty' = do PTerm
tm' <- IState -> PTerm -> Maybe Name -> State MergeState PTerm
tidy IState
ist (forall t. PArg' t -> t
getTm PArg
x) Maybe Name
ty'
                             forall (m :: * -> *) a. Monad m => a -> m a
return (PArg
x { getTm :: PTerm
getTm = PTerm
tm' })
tidy IState
ist PTerm
tm Maybe Name
ty = forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
tm


-- mapPT tidyVar tm
--   where tidyVar (PRef _ _) = Placeholder
--         tidyVar t = t

elabNewPat :: PTerm -> Idris (Bool, PTerm)
elabNewPat :: PTerm -> Idris (Bool, PTerm)
elabNewPat PTerm
t = forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do (Term
tm, Term
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabVal (FC -> ElabInfo
recinfo (String -> FC
fileFC String
"casesplit")) ElabMode
ELHS PTerm
t
                              IState
i <- Idris IState
getIState
                              forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, IState -> Term -> PTerm
delabDirect IState
i Term
tm))
                          (\Err
e -> do IState
i <- Idris IState
getIState
                                    Int -> String -> StateT IState (ExceptT Err IO) ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Not a valid split:\n" forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
t forall a. [a] -> [a] -> [a]
++ String
"\n"
                                                     forall a. [a] -> [a] -> [a]
++ IState -> Err -> String
pshow IState
i Err
e
                                    forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, PTerm
t))

findPats :: IState -> Type -> [PTerm]
findPats :: IState -> Term -> [PTerm]
findPats IState
ist Term
t | (P NameType
_ Name
n Term
_, [Term]
_) <- forall n. TT n -> (TT n, [TT n])
unApply Term
t
    = case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
ist) of
           [TypeInfo
ti] -> forall a b. (a -> b) -> [a] -> [b]
map Name -> PTerm
genPat (TypeInfo -> [Name]
con_names TypeInfo
ti)
           [TypeInfo]
_ -> [PTerm
Placeholder]
    where genPat :: Name -> PTerm
genPat Name
n = case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [PArg]
idris_implicits IState
ist) of
                        [[PArg]
args] -> FC -> PTerm -> [PArg] -> PTerm
PApp FC
emptyFC (FC -> [FC] -> Name -> PTerm
PRef FC
emptyFC [] Name
n)
                                         (forall a b. (a -> b) -> [a] -> [b]
map PArg -> PArg
toPlaceholder [PArg]
args)
                        [[PArg]]
_ -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Can't happen (genPat) " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n
          toPlaceholder :: PArg -> PArg
toPlaceholder PArg
tm = PArg
tm { getTm :: PTerm
getTm = PTerm
Placeholder }
findPats IState
ist Term
t = [PTerm
Placeholder]

replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
replaceVar Context
ctxt Name
n PTerm
t (PApp FC
fc PTerm
f [PArg]
pats) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f (forall a b. (a -> b) -> [a] -> [b]
map PArg -> PArg
substArg [PArg]
pats)
  where subst :: PTerm -> PTerm
        subst :: PTerm -> PTerm
subst orig :: PTerm
orig@(PPatvar FC
_ Name
v) | Name
v forall a. Eq a => a -> a -> Bool
== Name
n = PTerm
t
                                 | Bool
otherwise = PTerm
Placeholder
        subst orig :: PTerm
orig@(PRef FC
_ [FC]
_ Name
v) | Name
v forall a. Eq a => a -> a -> Bool
== Name
n = PTerm
t
                                | Name -> Context -> Bool
isDConName Name
v Context
ctxt = PTerm
orig
        subst (PRef FC
_ [FC]
_ Name
_) = PTerm
Placeholder
        subst (PApp FC
fc (PRef FC
_ [FC]
_ Name
t) [PArg]
pats)
            | Name -> Context -> Bool
isTConName Name
t Context
ctxt = PTerm
Placeholder -- infer types
        subst (PApp FC
fc PTerm
f [PArg]
pats) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f (forall a b. (a -> b) -> [a] -> [b]
map PArg -> PArg
substArg [PArg]
pats)
        subst PTerm
x = PTerm
x

        substArg :: PArg -> PArg
substArg PArg
arg = PArg
arg { getTm :: PTerm
getTm = PTerm -> PTerm
subst (forall t. PArg' t -> t
getTm PArg
arg) }

replaceVar Context
ctxt Name
n PTerm
t PTerm
pat = PTerm
pat

splitOnLine :: Int         -- ^ line number
            -> Name        -- ^ variable
            -> FilePath    -- ^ name of file
            -> Idris (Bool, [[(Name, PTerm)]])
splitOnLine :: Int -> Name -> String -> Idris (Bool, [[(Name, PTerm)]])
splitOnLine Int
l Name
n String
fn = do
    PTerm
cl <- String -> Int -> Idris PTerm
getInternalApp String
fn Int
l
    Int -> String -> StateT IState (ExceptT Err IO) ()
logElab Int
3 (String
"Working with " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
cl)
    (Bool, [[(Name, PTerm)]])
tms <- Name -> PTerm -> Idris (Bool, [[(Name, PTerm)]])
split Name
n PTerm
cl
    forall (m :: * -> *) a. Monad m => a -> m a
return (Bool, [[(Name, PTerm)]])
tms

replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]
replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]
replaceSplits String
l [[(Name, PTerm)]]
ups Bool
impossible
    = do IState
ist <- Idris IState
getIState
         forall {b}. (Show b, Num b) => b -> [String] -> Idris [String]
updateRHSs Integer
1 (forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. Show a => IState -> String -> [(a, PTerm)] -> String
rep IState
ist (String -> String
expandBraces String
l)) [[(Name, PTerm)]]
ups)
  where
    rep :: IState -> String -> [(a, PTerm)] -> String
rep IState
ist String
str [] = String
str forall a. [a] -> [a] -> [a]
++ String
"\n"
    rep IState
ist String
str ((a
n, PTerm
tm) : [(a, PTerm)]
ups)
        = IState -> String -> [(a, PTerm)] -> String
rep IState
ist (Bool -> String -> String -> String -> String
updatePat Bool
False (forall a. Show a => a -> String
show a
n) (PTerm -> String
nshow (IState -> PTerm -> PTerm
resugar IState
ist PTerm
tm)) String
str) [(a, PTerm)]
ups

    updateRHSs :: b -> [String] -> Idris [String]
updateRHSs b
i [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
    updateRHSs b
i (String
x : [String]
xs)
       | Bool
impossible = do [String]
xs' <- b -> [String] -> Idris [String]
updateRHSs b
i [String]
xs
                         forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> String -> String
setImpossible Bool
False String
x forall a. a -> [a] -> [a]
: [String]
xs')
       | Bool
otherwise = do (String
x', b
i') <- forall {b}.
(Show b, Num b) =>
Bool -> b -> String -> StateT IState (ExceptT Err IO) (String, b)
updateRHS (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
xs) b
i String
x
                        [String]
xs' <- b -> [String] -> Idris [String]
updateRHSs b
i' [String]
xs
                        forall (m :: * -> *) a. Monad m => a -> m a
return (String
x' forall a. a -> [a] -> [a]
: [String]
xs')

    updateRHS :: Bool -> b -> String -> StateT IState (ExceptT Err IO) (String, b)
updateRHS Bool
last b
i (Char
'?':Char
'=':String
xs) = do (String
xs', b
i') <- Bool -> b -> String -> StateT IState (ExceptT Err IO) (String, b)
updateRHS Bool
last b
i String
xs
                                       forall (m :: * -> *) a. Monad m => a -> m a
return (String
"?=" forall a. [a] -> [a] -> [a]
++ String
xs', b
i')
    updateRHS Bool
last b
i (Char
'?':String
xs)
        = do let (String
nm, String
rest_in) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\Char
x -> Char -> Bool
isSpace Char
x Bool -> Bool -> Bool
|| Char
x forall a. Eq a => a -> a -> Bool
== Char
')'
                                                              Bool -> Bool -> Bool
|| Char
x forall a. Eq a => a -> a -> Bool
== Char
'(')) String
xs
             let rest :: String
rest = if Bool
last then String
rest_in else
                           case forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Eq a => a -> a -> Bool
==Char
'\n')) String
rest_in of
                                (String
_, String
restnl) -> String
restnl
             (String
nm', b
i') <- forall t. (Show t, Num t) => String -> t -> Idris (String, t)
getUniq String
nm b
i
             forall (m :: * -> *) a. Monad m => a -> m a
return (Char
'?'forall a. a -> [a] -> [a]
:String
nm' forall a. [a] -> [a] -> [a]
++ String
rest, b
i')
    updateRHS Bool
last b
i (Char
x : String
xs) = do (String
xs', b
i') <- Bool -> b -> String -> StateT IState (ExceptT Err IO) (String, b)
updateRHS Bool
last b
i String
xs
                                   forall (m :: * -> *) a. Monad m => a -> m a
return (Char
x forall a. a -> [a] -> [a]
: String
xs', b
i')
    updateRHS Bool
last b
i [] = forall (m :: * -> *) a. Monad m => a -> m a
return (String
"", b
i)

    setImpossible :: Bool -> String -> String
setImpossible Bool
brace (Char
'}':String
xs) = Char
'}' forall a. a -> [a] -> [a]
: Bool -> String -> String
setImpossible Bool
False String
xs
    setImpossible Bool
brace (Char
'{':String
xs) = Char
'{' forall a. a -> [a] -> [a]
: Bool -> String -> String
setImpossible Bool
True String
xs
    setImpossible Bool
False (Char
'=':String
xs) = String
"impossible\n"
    setImpossible Bool
brace (Char
x : String
xs) = Char
x forall a. a -> [a] -> [a]
: Bool -> String -> String
setImpossible Bool
brace String
xs
    setImpossible Bool
brace [] = String
""

    -- TMP HACK: If there are Nats, we don't want to show as numerals since
    -- this isn't supported in a pattern, so special case here
    nshow :: PTerm -> String
nshow (PRef FC
_ [FC]
_ (UN Text
z)) | Text
z forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Z" = String
"Z"
    nshow (PApp FC
_ (PRef FC
_ [FC]
_ (UN Text
s)) [PArg
x]) | Text
s forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"S" =
               String
"(S " forall a. [a] -> [a] -> [a]
++ String -> String
addBrackets (PTerm -> String
nshow (forall t. PArg' t -> t
getTm PArg
x)) forall a. [a] -> [a] -> [a]
++ String
")"
    nshow PTerm
t = forall a. Show a => a -> String
show PTerm
t

    -- if there's any {n} replace with {n=n}
    -- but don't replace it in comments
    expandBraces :: String -> String
expandBraces (Char
'{' : Char
'-' : String
xs) = Char
'{' forall a. a -> [a] -> [a]
: Char
'-' forall a. a -> [a] -> [a]
: String
xs
    expandBraces (Char
'{' : String
xs)
        = let (String
brace, (Char
_:String
rest)) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span (forall a. Eq a => a -> a -> Bool
/= Char
'}') String
xs in
              if (Bool -> Bool
not (Char
'=' forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
brace))
                 then (Char
'{' forall a. a -> [a] -> [a]
: String
brace forall a. [a] -> [a] -> [a]
++ String
" = " forall a. [a] -> [a] -> [a]
++ String
brace forall a. [a] -> [a] -> [a]
++ String
"}") forall a. [a] -> [a] -> [a]
++
                         String -> String
expandBraces String
rest
                 else (Char
'{' forall a. a -> [a] -> [a]
: String
brace forall a. [a] -> [a] -> [a]
++ String
"}") forall a. [a] -> [a] -> [a]
++ String -> String
expandBraces String
rest
    expandBraces (Char
x : String
xs) = Char
x forall a. a -> [a] -> [a]
: String -> String
expandBraces String
xs
    expandBraces [] = []

    updatePat :: Bool -> String -> String -> String -> String
updatePat Bool
start String
n String
tm [] = []
    updatePat Bool
start String
n String
tm (Char
'{':String
rest) =
        let (String
space, String
rest') = forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isSpace String
rest in
            Char
'{' forall a. a -> [a] -> [a]
: String
space forall a. [a] -> [a] -> [a]
++ Bool -> String -> String -> String -> String
updatePat Bool
False String
n String
tm String
rest'
    updatePat Bool
start String
n String
tm done :: String
done@(Char
'?':String
rest) = String
done
    updatePat Bool
True String
n String
tm xs :: String
xs@(Char
c:String
rest) | forall (t :: * -> *) a. Foldable t => t a -> Int
length String
xs forall a. Ord a => a -> a -> Bool
> forall (t :: * -> *) a. Foldable t => t a -> Int
length String
n
        = let (String
before, after :: String
after@(Char
next:String
_)) = forall a. Int -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> Int
length String
n) String
xs in
              if (String
before forall a. Eq a => a -> a -> Bool
== String
n Bool -> Bool -> Bool
&& Bool -> Bool
not (Char -> Bool
isAlphaNum Char
next))
                 then String -> String
addBrackets String
tm forall a. [a] -> [a] -> [a]
++ Bool -> String -> String -> String -> String
updatePat Bool
False String
n String
tm String
after
                 else Char
c forall a. a -> [a] -> [a]
: Bool -> String -> String -> String -> String
updatePat (Bool -> Bool
not (Char -> Bool
isAlphaNum Char
c)) String
n String
tm String
rest
    updatePat Bool
start String
n String
tm (Char
c:String
rest) = Char
c forall a. a -> [a] -> [a]
: Bool -> String -> String -> String -> String
updatePat (Bool -> Bool
not ((Char -> Bool
isAlphaNum Char
c) Bool -> Bool -> Bool
|| Char
c forall a. Eq a => a -> a -> Bool
== Char
'_')) String
n String
tm String
rest

    addBrackets :: String -> String
addBrackets String
tm | Char
' ' forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
tm
                   , Bool -> Bool
not (forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
"(" String
tm Bool -> Bool -> Bool
&& forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf String
")" String
tm)
                       = String
"(" forall a. [a] -> [a] -> [a]
++ String
tm forall a. [a] -> [a] -> [a]
++ String
")"
                   | Bool
otherwise = String
tm


getUniq :: (Show t, Num t) => [Char] -> t -> Idris ([Char], t)
getUniq :: forall t. (Show t, Num t) => String -> t -> Idris (String, t)
getUniq String
nm t
i
       = do IState
ist <- Idris IState
getIState
            let n :: String
n = [String] -> String -> String
nameRoot [] String
nm forall a. [a] -> [a] -> [a]
++ String
"_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
i
            case Name -> Context -> [Term]
lookupTy (String -> Name
sUN String
n) (IState -> Context
tt_ctxt IState
ist) of
                 [] -> forall (m :: * -> *) a. Monad m => a -> m a
return (String
n, t
iforall a. Num a => a -> a -> a
+t
1)
                 [Term]
_ -> forall t. (Show t, Num t) => String -> t -> Idris (String, t)
getUniq String
nm (t
iforall a. Num a => a -> a -> a
+t
1)

nameRoot :: [String] -> String -> String
nameRoot [String]
acc String
nm | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
nm = String -> [String] -> String
showSep String
"_" [String]
acc
nameRoot [String]
acc String
nm =
        case forall a. (a -> Bool) -> [a] -> ([a], [a])
span (forall a. Eq a => a -> a -> Bool
/=Char
'_') String
nm of
             (String
before, (Char
'_' : String
after)) -> [String] -> String -> String
nameRoot ([String]
acc forall a. [a] -> [a] -> [a]
++ [String
before]) String
after
             (String, String)
_ -> String -> [String] -> String
showSep String
"_" ([String]
acc forall a. [a] -> [a] -> [a]
++ [String
nm])

-- Show a name for use in pattern definitions on the lhs
showLHSName :: Name -> String
showLHSName :: Name -> String
showLHSName Name
n = let fn :: String
fn = forall a. Show a => a -> String
show Name
n in
                    if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
opChars) String
fn
                       then String
"(" forall a. [a] -> [a] -> [a]
++ String
fn forall a. [a] -> [a] -> [a]
++ String
")"
                       else String
fn

-- Show a name for the purpose of generating a metavariable name on the rhs
showRHSName :: Name -> String
showRHSName :: Name -> String
showRHSName Name
n = let fn :: String
fn = forall a. Show a => a -> String
show Name
n in
                    if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
opChars) String
fn
                       then String
"op"
                       else String
fn

getClause :: Int      -- ^ line number that the type is declared on
          -> Name     -- ^ Function name
          -> Name     -- ^ User given name
          -> FilePath -- ^ Source file name
          -> Idris String
getClause :: Int -> Name -> Name -> String -> Idris String
getClause Int
l Name
_ Name
un String
fp
    = do IState
i <- Idris IState
getIState
         Int
indentClause <- Idris Int
getIndentClause
--         runIO . traceIO $ "indentClause = " ++ show indentClause
         case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
un (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i) of
              [InterfaceInfo
c] -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IState -> [(Name, (Bool, FnOpts, PTerm))] -> String
mkInterfaceBodies Int
indentClause IState
i (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
c))
              [InterfaceInfo]
_ -> do PTerm
ty_in <- String -> Int -> Idris PTerm
getInternalApp String
fp Int
l
                      let ty :: PTerm
ty = case PTerm
ty_in of
                                    PTyped PTerm
_ PTerm
t -> PTerm
t
                                    PTerm
x -> PTerm
x
                      IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                      let app :: String
app = IState -> PTerm -> [Name] -> String
mkApp IState
ist PTerm
ty []
                      forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> String
showLHSName Name
un forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
app forall a. [a] -> [a] -> [a]
++ String
"= ?"
                                      forall a. [a] -> [a] -> [a]
++ Name -> String
showRHSName Name
un forall a. [a] -> [a] -> [a]
++ String
"_rhs")
   where mkApp :: IState -> PTerm -> [Name] -> String
         mkApp :: IState -> PTerm -> [Name] -> String
mkApp IState
i (PPi (Exp [ArgOpt]
_ Static
_ Bool
False RigCount
_) (MN Int
_ Text
_) FC
_ PTerm
ty PTerm
sc) [Name]
used
               = let n :: Name
n = IState -> [Name] -> PTerm -> Name
getNameFrom IState
i [Name]
used PTerm
ty in
                     forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ IState -> PTerm -> [Name] -> String
mkApp IState
i PTerm
sc (Name
n forall a. a -> [a] -> [a]
: [Name]
used)
         mkApp IState
i (PPi (Exp [ArgOpt]
_ Static
_ Bool
False RigCount
_) (UN Text
n) FC
_ PTerm
ty PTerm
sc) [Name]
used
            | Text -> Char
thead Text
n forall a. Eq a => a -> a -> Bool
== Char
'_'
               = let n :: Name
n = IState -> [Name] -> PTerm -> Name
getNameFrom IState
i [Name]
used PTerm
ty in
                     forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ IState -> PTerm -> [Name] -> String
mkApp IState
i PTerm
sc (Name
n forall a. a -> [a] -> [a]
: [Name]
used)
         mkApp IState
i (PPi (Exp [ArgOpt]
_ Static
_ Bool
False RigCount
_) Name
n FC
_ PTerm
_ PTerm
sc) [Name]
used
               = forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ IState -> PTerm -> [Name] -> String
mkApp IState
i PTerm
sc (Name
n forall a. a -> [a] -> [a]
: [Name]
used)
         mkApp IState
i (PPi Plicity
_ Name
_ FC
_ PTerm
_ PTerm
sc) [Name]
used = IState -> PTerm -> [Name] -> String
mkApp IState
i PTerm
sc [Name]
used
         mkApp IState
i PTerm
_ [Name]
_ = String
""

         getNameFrom :: IState -> [Name] -> PTerm -> Name
getNameFrom IState
i [Name]
used (PPi Plicity
_ Name
_ FC
_ PTerm
_ PTerm
_)
              = [Name] -> [Name] -> Name
uniqueNameFrom ([Name] -> [Name]
mkSupply [String -> Name
sUN String
"f", String -> Name
sUN String
"g"]) [Name]
used
         getNameFrom IState
i [Name]
used (PApp FC
fc PTerm
f [PArg]
as) = IState -> [Name] -> PTerm -> Name
getNameFrom IState
i [Name]
used PTerm
f
         getNameFrom IState
i [Name]
used (PRef FC
fc [FC]
_ Name
f)
            = case IState -> Name -> [Name]
getNameHints IState
i Name
f of
                   [] -> [Name] -> [Name] -> Name
uniqueNameFrom ([Name] -> [Name]
mkSupply [String -> Name
sUN String
"x", String -> Name
sUN String
"y",
                                                   String -> Name
sUN String
"z"]) [Name]
used
                   [Name]
ns -> [Name] -> [Name] -> Name
uniqueNameFrom ([Name] -> [Name]
mkSupply [Name]
ns) [Name]
used
         getNameFrom IState
i [Name]
used PTerm
_ = [Name] -> [Name] -> Name
uniqueNameFrom ([Name] -> [Name]
mkSupply [String -> Name
sUN String
"x", String -> Name
sUN String
"y",
                                                          String -> Name
sUN String
"z"]) [Name]
used

         -- write method declarations, indent with `indent` spaces.
         mkInterfaceBodies :: Int -> IState -> [(Name, (Bool, FnOpts, PTerm))] -> String
         mkInterfaceBodies :: Int -> IState -> [(Name, (Bool, FnOpts, PTerm))] -> String
mkInterfaceBodies Int
indent IState
i [(Name, (Bool, FnOpts, PTerm))]
ns
             = String -> [String] -> String
showSep String
"\n"
                  (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Name
n, (Bool
_, FnOpts
_, PTerm
ty)) Integer
m -> forall a. Int -> a -> [a]
replicate Int
indent Char
' ' forall a. [a] -> [a] -> [a]
++
                            String -> String
def (forall a. Show a => a -> String
show (Name -> Name
nsroot Name
n)) forall a. [a] -> [a] -> [a]
++ String
" "
                                 forall a. [a] -> [a] -> [a]
++ IState -> PTerm -> [Name] -> String
mkApp IState
i PTerm
ty []
                                 forall a. [a] -> [a] -> [a]
++ String
"= ?"
                                 forall a. [a] -> [a] -> [a]
++ Name -> String
showRHSName Name
un forall a. [a] -> [a] -> [a]
++ String
"_rhs_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
m) [(Name, (Bool, FnOpts, PTerm))]
ns [Integer
1..])

         def :: String -> String
def n :: String
n@(Char
x:String
xs) | Bool -> Bool
not (Char -> Bool
isAlphaNum Char
x) = String
"(" forall a. [a] -> [a] -> [a]
++ String
n forall a. [a] -> [a] -> [a]
++ String
")"
         def String
n = String
n

getProofClause :: Int      -- ^ line number that the type is declared
               -> Name     -- ^ Function name
               -> FilePath -- ^ Source file name
               -> Idris String
getProofClause :: Int -> Name -> String -> Idris String
getProofClause Int
l Name
fn String
fp
                  = do PTerm
ty_in <- String -> Int -> Idris PTerm
getInternalApp String
fp Int
l
                       let ty :: PTerm
ty = case PTerm
ty_in of
                                     PTyped PTerm
n PTerm
t -> PTerm
t
                                     PTerm
x -> PTerm
x
                       forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> String
mkApp PTerm
ty forall a. [a] -> [a] -> [a]
++ String
" = ?" forall a. [a] -> [a] -> [a]
++ Name -> String
showRHSName Name
fn forall a. [a] -> [a] -> [a]
++ String
"_rhs")
   where mkApp :: PTerm -> String
mkApp (PPi Plicity
_ Name
_ FC
_ PTerm
_ PTerm
sc) = PTerm -> String
mkApp PTerm
sc
         mkApp PTerm
rt = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PTerm
rt forall a. [a] -> [a] -> [a]
++ String
") <== " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
fn

-- Purely syntactic - turn a pattern match clause into a with and a new
-- match clause

mkWith :: String -> Name -> Int -> String
mkWith :: String -> Name -> Int -> String
mkWith String
str Name
n Int
indent = let str' :: String
str' = String -> String -> String
replaceRHS String
str String
"with (_)"
                      in String
str' forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ String -> String
newpat String
str

   where replaceRHS :: String -> String -> String
replaceRHS [] String
str = String
str
         replaceRHS (Char
'?':Char
'=': String
rest) String
str = String
str
         replaceRHS (Char
'=': String
rest) String
str
              | Bool -> Bool
not (Char
'=' forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
rest) = String
str
         replaceRHS (Char
x : String
rest) String
str = Char
x forall a. a -> [a] -> [a]
: String -> String -> String
replaceRHS String
rest String
str

         newpat :: String -> String
newpat (Char
'>':String
patstr) = Char
'>'forall a. a -> [a] -> [a]
:String -> String
newpat String
patstr
         newpat String
patstr = forall a. Int -> a -> [a]
replicate Int
indent Char
' ' forall a. [a] -> [a] -> [a]
++
           String -> String -> String
replaceRHS String
patstr String
"| with_pat = ?" forall a. [a] -> [a] -> [a]
++ Name -> String
showRHSName Name
n forall a. [a] -> [a] -> [a]
++ String
"_rhs"

-- Replace _ with names in missing clauses

nameMissing :: [PTerm] -> Idris [PTerm]
nameMissing :: [PTerm] -> Idris [PTerm]
nameMissing [PTerm]
ps = do IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                    [PTerm]
newPats <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PTerm -> Idris PTerm
nm [PTerm]
ps
                    let newPats' :: [(PTerm, [(Name, PTerm)])]
newPats' = IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
mergeAllPats IState
ist (String -> Name
sUN String
"_") (PTerm -> PTerm
base (forall a. [a] -> a
head [PTerm]
ps))
                                                [PTerm]
newPats
                    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(PTerm, [(Name, PTerm)])]
newPats')
  where
    base :: PTerm -> PTerm
base (PApp FC
fc PTerm
f [PArg]
args) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN String
"_")))) [PArg]
args)
    base PTerm
t = PTerm
t

    nm :: PTerm -> Idris PTerm
nm PTerm
ptm = do (Bool, PTerm)
mptm <- PTerm -> Idris (Bool, PTerm)
elabNewPat PTerm
ptm
                case (Bool, PTerm)
mptm of
                     (Bool
False, PTerm
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
ptm
                     (Bool
True, PTerm
ptm') -> forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
ptm'