{-# 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
(Name -> StateT IState (ExceptT Err IO) ())
-> [Name] -> StateT IState (ExceptT Err IO) ()
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" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, Term)] -> String
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 Name -> [(Name, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Term)]
pats of
Maybe Term
Nothing -> String -> Idris (Bool, [[(Name, PTerm)]])
forall a. String -> Idris a
ifail (String -> Idris (Bool, [[(Name, PTerm)]]))
-> String -> Idris (Bool, [[(Name, PTerm)]])
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
", "
((PTerm -> String) -> [PTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
showTmImpls [PTerm]
splits))
let newPats_in :: [PTerm]
newPats_in = (PTerm -> PTerm -> PTerm) -> [PTerm] -> [PTerm] -> [PTerm]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Context -> Name -> PTerm -> PTerm -> PTerm
replaceVar Context
ctxt Name
n) [PTerm]
splits (PTerm -> [PTerm]
forall a. a -> [a]
repeat PTerm
t)
Int -> String -> StateT IState (ExceptT Err IO) ()
logElab Int
4 (String
"Working from " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
t)
Int -> String -> StateT IState (ExceptT Err IO) ()
logElab Int
4 (String
"Trying " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n"
((PTerm -> String) -> [PTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm -> String
showTmImpls) [PTerm]
newPats_in))
[(Bool, PTerm)]
newPats_in <- (PTerm -> StateT IState (ExceptT Err IO) (Bool, PTerm))
-> [PTerm] -> StateT IState (ExceptT Err IO) [(Bool, PTerm)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM PTerm -> StateT IState (ExceptT Err IO) (Bool, PTerm)
elabNewPat [PTerm]
newPats_in
case [PTerm] -> [PTerm] -> [(Bool, PTerm)] -> Either [PTerm] [PTerm]
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
(Bool, [[(Name, PTerm)]]) -> Idris (Bool, [[(Name, PTerm)]])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, (((PTerm, [(Name, PTerm)]) -> [(Name, PTerm)])
-> [(PTerm, [(Name, PTerm)])] -> [[(Name, PTerm)]]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm, [(Name, PTerm)]) -> [(Name, PTerm)]
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" String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
forall a. Show a => a -> String
show PTerm
t)
Int -> String -> StateT IState (ExceptT Err IO) ()
logElab Int
3 (String
"Split:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
(String -> [String] -> String
showSep String
"\n" ((PTerm -> String) -> [PTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> String
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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep String
"\n"
(((PTerm, [(Name, PTerm)]) -> String)
-> [(PTerm, [(Name, PTerm)])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (PTerm
p, [(Name, PTerm)]
u) -> [(Name, PTerm)] -> String
forall a. Show a => a -> String
show [(Name, PTerm)]
u String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
forall a. Show a => a -> String
show PTerm
p) [(PTerm, [(Name, PTerm)])]
newPats'))
(Bool, [[(Name, PTerm)]]) -> Idris (Bool, [[(Name, PTerm)]])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, (((PTerm, [(Name, PTerm)]) -> [(Name, PTerm)])
-> [(PTerm, [(Name, PTerm)])] -> [[(Name, PTerm)]]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm, [(Name, PTerm)]) -> [(Name, PTerm)]
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 [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
ok then [a] -> Either [a] [a]
forall a b. a -> Either a b
Left ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
bad)
else [a] -> Either [a] [a]
forall a b. b -> Either a b
Right ([a] -> [a]
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 a -> [a] -> [a]
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 a -> [a] -> [a]
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 <- StateT MergeState Identity MergeState
forall s (m :: * -> *). MonadState s m => m s
get
MergeState -> State MergeState ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (MergeState
ms { updates = ((n, stripNS tm) : updates 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 <- StateT MergeState Identity MergeState
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 Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'
-> [Name] -> [Name]
mkSupply ([Name]
supp [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
varlist)
MN Int
i Text
n -> [Name] -> [Name]
mkSupply (Text -> Name
UN Text
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
supp [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
varlist)
UN Text
n | Text -> Char
thead Text
n Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'
-> [Name] -> [Name]
mkSupply ([Name]
supp [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
varlist)
Name
x -> [Name] -> [Name]
mkSupply (Name
x Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
supp)
let badnames :: [Name]
badnames = ((Name, Name) -> Name) -> [(Name, Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Name) -> Name
forall a b. (a, b) -> b
snd (MergeState -> [(Name, Name)]
namemap MergeState
ms) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ ((Name, Name) -> Name) -> [(Name, Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Name) -> Name
forall a b. (a, b) -> b
snd (MergeState -> [(Name, Name)]
invented MergeState
ms) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
MergeState -> [Name]
explicit MergeState
ms
case Name -> [(Name, Name)] -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (MergeState -> [(Name, Name)]
invented MergeState
ms) of
Just Name
n' -> Name -> State MergeState Name
forall a. a -> StateT MergeState Identity a
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
MergeState -> State MergeState ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (MergeState
ms { invented = (n, n') : invented ms })
Name -> State MergeState Name
forall a. a -> StateT MergeState Identity a
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 ((Name -> Name) -> [Name] -> [Name]
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 [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name] -> [Name]
mkSupply [Name]
ns'
varlist :: [Name]
varlist :: [Name]
varlist = (Char -> Name) -> String -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Name
sUN (String -> Name) -> (Char -> String) -> Char -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> String -> String
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) = State MergeState PTerm -> MergeState -> (PTerm, MergeState)
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 Maybe Name
forall a. Maybe a
Nothing)
([(Name, Name)]
-> [(Name, Name)] -> [Name] -> [(Name, PTerm)] -> MergeState
MS [] [] ((Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> Name -> Bool
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) (PTerm, [(Name, PTerm)])
-> [(PTerm, [(Name, PTerm)])] -> [(PTerm, [(Name, PTerm)])]
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) = (PArg -> [Name]) -> [PArg] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (PTerm -> [Name]
patvars (PTerm -> [Name]) -> (PArg -> PTerm) -> PArg -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PArg -> PTerm
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)
_ -> () -> State MergeState ()
forall a. a -> StateT MergeState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Right [(Name, PTerm)]
ns -> ((Name, PTerm) -> State MergeState ())
-> [(Name, PTerm)] -> State MergeState ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Name, PTerm) -> State MergeState ()
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 <- m MergeState
forall s (m :: * -> *). MonadState s m => m s
get
MergeState -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (MergeState
ms { namemap = ((n', n) : namemap ms) })
addNameMap (Name, PTerm)
_ = () -> m ()
forall a. a -> m a
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
PTerm -> State MergeState PTerm
forall a. a -> StateT MergeState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
new
| Bool
otherwise
= do MergeState
ms <- StateT MergeState Identity MergeState
forall s (m :: * -> *). MonadState s m => m s
get
case Name -> [(Name, Name)] -> Maybe Name
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)
PTerm -> State MergeState PTerm
forall a. a -> StateT MergeState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
x)
Maybe Name
Nothing -> do MergeState -> State MergeState ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (MergeState
ms { namemap = ((n', n) : namemap ms) })
PTerm -> State MergeState PTerm
forall a. a -> StateT MergeState Identity a
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 <- (PArg -> (PArg, Maybe Name) -> StateT MergeState Identity PArg)
-> [PArg]
-> [(PArg, Maybe Name)]
-> StateT MergeState Identity [PArg]
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 ([PArg] -> [Maybe Name] -> [(PArg, Maybe Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [PArg]
args' (IState -> PTerm -> [Maybe Name]
argTys IState
ist PTerm
f))
PTerm -> State MergeState PTerm
forall a. a -> StateT MergeState Identity a
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 (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
x) (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
y) Maybe Name
t
case PArg
x of
(PImp Int
_ Bool
_ [ArgOpt]
_ Name
_ PTerm
_) ->
PArg -> StateT MergeState Identity PArg
forall a. a -> StateT MergeState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (PArg
y { machine_inf = machine_inf x,
getTm = tm' })
PArg
_ -> PArg -> StateT MergeState Identity PArg
forall a. a -> StateT MergeState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (PArg
y { getTm = 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
PTerm -> State MergeState PTerm
forall a. a -> StateT MergeState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
tm
mergePat' IState
ist PTerm
x PTerm
y Maybe Name
t = PTerm -> State MergeState PTerm
forall a. a -> StateT MergeState Identity a
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
((Name, Term) -> Maybe Name) -> [(Name, Term)] -> [Maybe Name]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Maybe Name
tyName (Term -> Maybe Name)
-> ((Name, Term) -> Term) -> (Name, Term) -> Maybe Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Term) -> Term
forall a b. (a, b) -> b
snd) (Term -> [(Name, Term)]
forall n. TT n -> [(n, TT n)]
getArgTys Term
ty') [Maybe Name] -> [Maybe Name] -> [Maybe Name]
forall a. [a] -> [a] -> [a]
++ Maybe Name -> [Maybe Name]
forall a. a -> [a]
repeat Maybe Name
forall a. Maybe a
Nothing
[Term]
_ -> Maybe Name -> [Maybe Name]
forall a. a -> [a]
repeat Maybe Name
forall a. Maybe a
Nothing
where tyName :: Term -> Maybe Name
tyName (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ Term
_ Term
_) Term
_) = Name -> Maybe Name
forall a. a -> Maybe a
Just (String -> Name
sUN String
"->")
tyName Term
t | (P NameType
_ Name
d Term
_, [Term
_, Term
ty]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
t,
Name
d Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"Delayed" = Term -> Maybe Name
tyName Term
ty
| (P NameType
_ Name
n Term
_, [Term]
_) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
t = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
| Bool
otherwise = Maybe Name
forall a. Maybe a
Nothing
argTys IState
_ PTerm
_ = Maybe Name -> [Maybe Name]
forall a. a -> [a]
repeat Maybe Name
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 <- StateT MergeState Identity MergeState
forall s (m :: * -> *). MonadState s m => m s
get
case Name -> [(Name, Name)] -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (MergeState -> [(Name, Name)]
namemap MergeState
ms) of
Just Name
x -> PTerm -> State MergeState PTerm
forall a. a -> StateT MergeState Identity a
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
_) -> PTerm -> State MergeState PTerm
forall a. a -> StateT MergeState Identity a
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
PTerm -> State MergeState PTerm
forall a. a -> StateT MergeState Identity a
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' <- (PArg -> Maybe Name -> StateT MergeState Identity PArg)
-> [PArg] -> [Maybe Name] -> StateT MergeState Identity [PArg]
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)
PTerm -> State MergeState PTerm
forall a. a -> StateT MergeState Identity a
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 (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
x) Maybe Name
ty'
PArg -> StateT MergeState Identity PArg
forall a. a -> StateT MergeState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (PArg
x { getTm = tm' })
tidy IState
ist PTerm
tm Maybe Name
ty = PTerm -> State MergeState PTerm
forall a. a -> StateT MergeState Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
tm
elabNewPat :: PTerm -> Idris (Bool, PTerm)
elabNewPat :: PTerm -> StateT IState (ExceptT Err IO) (Bool, PTerm)
elabNewPat PTerm
t = StateT IState (ExceptT Err IO) (Bool, PTerm)
-> (Err -> StateT IState (ExceptT Err IO) (Bool, PTerm))
-> StateT IState (ExceptT Err IO) (Bool, PTerm)
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
(Bool, PTerm) -> StateT IState (ExceptT Err IO) (Bool, PTerm)
forall a. a -> StateT IState (ExceptT Err IO) a
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 (String -> StateT IState (ExceptT Err IO) ())
-> String -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ String
"Not a valid split:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ IState -> Err -> String
pshow IState
i Err
e
(Bool, PTerm) -> StateT IState (ExceptT Err IO) (Bool, PTerm)
forall a. a -> StateT IState (ExceptT Err IO) a
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]
_) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
t
= case Name -> Ctxt TypeInfo -> [TypeInfo]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
ist) of
[TypeInfo
ti] -> (Name -> PTerm) -> [Name] -> [PTerm]
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 Name -> Ctxt [PArg] -> [[PArg]]
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)
((PArg -> PArg) -> [PArg] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> PArg
toPlaceholder [PArg]
args)
[[PArg]]
_ -> String -> PTerm
forall a. HasCallStack => String -> a
error (String -> PTerm) -> String -> PTerm
forall a b. (a -> b) -> a -> b
$ String
"Can't happen (genPat) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
toPlaceholder :: PArg -> PArg
toPlaceholder PArg
tm = PArg
tm { getTm = 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 ((PArg -> PArg) -> [PArg] -> [PArg]
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 Name -> Name -> Bool
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 Name -> Name -> Bool
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 ((PArg -> PArg) -> [PArg] -> [PArg]
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 = subst (getTm 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 " String -> String -> String
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
(Bool, [[(Name, PTerm)]]) -> Idris (Bool, [[(Name, PTerm)]])
forall a. a -> StateT IState (ExceptT Err IO) a
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
Integer -> [String] -> Idris [String]
forall {b}. (Show b, Num b) => b -> [String] -> Idris [String]
updateRHSs Integer
1 (([(Name, PTerm)] -> String) -> [[(Name, PTerm)]] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (IState -> String -> [(Name, PTerm)] -> String
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 String -> String -> String
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 (a -> String
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 [] = [String] -> Idris [String]
forall a. a -> StateT IState (ExceptT Err IO) a
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
[String] -> Idris [String]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> String -> String
setImpossible Bool
False String
x String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
xs')
| Bool
otherwise = do (String
x', b
i') <- Bool -> b -> String -> StateT IState (ExceptT Err IO) (String, b)
forall {b}.
(Show b, Num b) =>
Bool -> b -> String -> StateT IState (ExceptT Err IO) (String, b)
updateRHS ([String] -> Bool
forall a. [a] -> Bool
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
[String] -> Idris [String]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
x' String -> [String] -> [String]
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
(String, b) -> StateT IState (ExceptT Err IO) (String, b)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
"?=" String -> String -> 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) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\Char
x -> Char -> Bool
isSpace Char
x Bool -> Bool -> Bool
|| Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
')'
Bool -> Bool -> Bool
|| Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'(')) String
xs
let rest :: String
rest = if Bool
last then String
rest_in else
case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==Char
'\n')) String
rest_in of
(String
_, String
restnl) -> String
restnl
(String
nm', b
i') <- String -> b -> StateT IState (ExceptT Err IO) (String, b)
forall t. (Show t, Num t) => String -> t -> Idris (String, t)
getUniq String
nm b
i
(String, b) -> StateT IState (ExceptT Err IO) (String, b)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
'?'Char -> String -> String
forall a. a -> [a] -> [a]
:String
nm' String -> String -> String
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
(String, b) -> StateT IState (ExceptT Err IO) (String, b)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
x Char -> String -> String
forall a. a -> [a] -> [a]
: String
xs', b
i')
updateRHS Bool
last b
i [] = (String, b) -> StateT IState (ExceptT Err IO) (String, b)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
"", b
i)
setImpossible :: Bool -> String -> String
setImpossible Bool
brace (Char
'}':String
xs) = Char
'}' Char -> String -> String
forall a. a -> [a] -> [a]
: Bool -> String -> String
setImpossible Bool
False String
xs
setImpossible Bool
brace (Char
'{':String
xs) = Char
'{' Char -> String -> String
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 Char -> String -> String
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 Text -> Text -> Bool
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 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"S" =
String
"(S " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
addBrackets (PTerm -> String
nshow (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
x)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
nshow PTerm
t = PTerm -> String
forall a. Show a => a -> String
show PTerm
t
expandBraces :: String -> String
expandBraces (Char
'{' : Char
'-' : String
xs) = Char
'{' Char -> String -> String
forall a. a -> [a] -> [a]
: Char
'-' Char -> String -> String
forall a. a -> [a] -> [a]
: String
xs
expandBraces (Char
'{' : String
xs)
= let (String
brace, (Char
_:String
rest)) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'}') String
xs in
if (Bool -> Bool
not (Char
'=' Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
brace))
then (Char
'{' Char -> String -> String
forall a. a -> [a] -> [a]
: String
brace String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
brace String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}") String -> String -> String
forall a. [a] -> [a] -> [a]
++
String -> String
expandBraces String
rest
else (Char
'{' Char -> String -> String
forall a. a -> [a] -> [a]
: String
brace String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
expandBraces String
rest
expandBraces (Char
x : String
xs) = Char
x Char -> String -> String
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') = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isSpace String
rest in
Char
'{' Char -> String -> String
forall a. a -> [a] -> [a]
: String
space String -> String -> String
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) | String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
n
= let (String
before, after :: String
after@(Char
next:String
_)) = Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
n) String
xs in
if (String
before String -> String -> Bool
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 String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> String -> String -> String -> String
updatePat Bool
False String
n String
tm String
after
else Char
c Char -> String -> String
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 Char -> String -> String
forall a. a -> [a] -> [a]
: Bool -> String -> String -> String -> String
updatePat (Bool -> Bool
not ((Char -> Bool
isAlphaNum Char
c) Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_')) String
n String
tm String
rest
addBrackets :: String -> String
addBrackets String
tm | Char
' ' Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
tm
, Bool -> Bool
not (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
"(" String
tm Bool -> Bool -> Bool
&& String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf String
")" String
tm)
= String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tm String -> String -> String
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 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ t -> String
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
[] -> (String, t) -> Idris (String, t)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
n, t
it -> t -> t
forall a. Num a => a -> a -> a
+t
1)
[Term]
_ -> String -> t -> Idris (String, t)
forall t. (Show t, Num t) => String -> t -> Idris (String, t)
getUniq String
nm (t
it -> t -> t
forall a. Num a => a -> a -> a
+t
1)
nameRoot :: [String] -> String -> String
nameRoot [String]
acc String
nm | (Char -> Bool) -> String -> Bool
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 (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/=Char
'_') String
nm of
(String
before, (Char
'_' : String
after)) -> [String] -> String -> String
nameRoot ([String]
acc [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
before]) String
after
(String, String)
_ -> String -> [String] -> String
showSep String
"_" ([String]
acc [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
nm])
showLHSName :: Name -> String
showLHSName :: Name -> String
showLHSName Name
n = let fn :: String
fn = Name -> String
forall a. Show a => a -> String
show Name
n in
if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Char -> String -> Bool) -> String -> Char -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
opChars) String
fn
then String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fn String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
else String
fn
showRHSName :: Name -> String
showRHSName :: Name -> String
showRHSName Name
n = let fn :: String
fn = Name -> String
forall a. Show a => a -> String
show Name
n in
if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Char -> String -> Bool) -> String -> Char -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
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 Name -> Ctxt InterfaceInfo -> [InterfaceInfo]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
un (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i) of
[InterfaceInfo
c] -> String -> Idris String
forall a. a -> StateT IState (ExceptT Err IO) a
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 <- Idris IState
forall s (m :: * -> *). MonadState s m => m s
get
let app :: String
app = IState -> PTerm -> [Name] -> String
mkApp IState
ist PTerm
ty []
String -> Idris String
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> String
showLHSName Name
un String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
app String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"= ?"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
showRHSName Name
un String -> String -> String
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
Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IState -> PTerm -> [Name] -> String
mkApp IState
i PTerm
sc (Name
n Name -> [Name] -> [Name]
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 Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'
= let n :: Name
n = IState -> [Name] -> PTerm -> Name
getNameFrom IState
i [Name]
used PTerm
ty in
Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IState -> PTerm -> [Name] -> String
mkApp IState
i PTerm
sc (Name
n Name -> [Name] -> [Name]
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
= Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IState -> PTerm -> [Name] -> String
mkApp IState
i PTerm
sc (Name
n Name -> [Name] -> [Name]
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"
(((Name, (Bool, FnOpts, PTerm)) -> Integer -> String)
-> [(Name, (Bool, FnOpts, PTerm))] -> [Integer] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Name
n, (Bool
_, FnOpts
_, PTerm
ty)) Integer
m -> Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
indent Char
' ' String -> String -> String
forall a. [a] -> [a] -> [a]
++
String -> String
def (Name -> String
forall a. Show a => a -> String
show (Name -> Name
nsroot Name
n)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ IState -> PTerm -> [Name] -> String
mkApp IState
i PTerm
ty []
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"= ?"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
showRHSName Name
un String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_rhs_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
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
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n String -> String -> String
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
String -> Idris String
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> String
mkApp PTerm
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = ?" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
showRHSName Name
fn String -> String -> String
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
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
forall a. Show a => a -> String
show PTerm
rt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") <== " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
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' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
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
'=' Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
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 Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String -> String
replaceRHS String
rest String
str
newpat :: String -> String
newpat (Char
'>':String
patstr) = Char
'>'Char -> String -> String
forall a. a -> [a] -> [a]
:String -> String
newpat String
patstr
newpat String
patstr = Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
indent Char
' ' String -> String -> String
forall a. [a] -> [a] -> [a]
++
String -> String -> String
replaceRHS String
patstr String
"| with_pat = ?" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
showRHSName Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_rhs"
nameMissing :: [PTerm] -> Idris [PTerm]
nameMissing :: [PTerm] -> Idris [PTerm]
nameMissing [PTerm]
ps = do IState
ist <- Idris IState
forall s (m :: * -> *). MonadState s m => m s
get
[PTerm]
newPats <- (PTerm -> Idris PTerm) -> [PTerm] -> Idris [PTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 ([PTerm] -> PTerm
forall a. HasCallStack => [a] -> a
head [PTerm]
ps))
[PTerm]
newPats
[PTerm] -> Idris [PTerm]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (((PTerm, [(Name, PTerm)]) -> PTerm)
-> [(PTerm, [(Name, PTerm)])] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm, [(Name, PTerm)]) -> PTerm
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 ((PArg -> PArg) -> [PArg] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PArg -> PArg
forall a b. (a -> b) -> PArg' a -> PArg' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PTerm -> PTerm -> PTerm
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 -> StateT IState (ExceptT Err IO) (Bool, PTerm)
elabNewPat PTerm
ptm
case (Bool, PTerm)
mptm of
(Bool
False, PTerm
_) -> PTerm -> Idris PTerm
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
ptm
(Bool
True, PTerm
ptm') -> PTerm -> Idris PTerm
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
ptm'