{-# 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)
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
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')
(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')
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)
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"
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
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 ()
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
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
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
-> Name
-> FilePath
-> 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
""
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
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])
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
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
-> Name
-> Name
-> FilePath
-> 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
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
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
-> Name
-> FilePath
-> 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
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"
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'