{-# 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 n :: Name
n t' :: 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_ (\n :: Name
n -> Name -> Accessibility -> StateT IState (ExceptT Err IO) ()
setAccessibility Name
n Accessibility
Public) (PTerm -> [Name]
allNamesIn PTerm
t')
(tm :: Term
tm, ty :: Term
ty, pats :: [(Name, Term)]
pats) <- ElabInfo
-> ElabMode -> Bool -> PTerm -> Idris (Term, Term, [(Name, Term)])
elabValBind (FC -> ElabInfo
recinfo (String -> FC
fileFC "casesplit")) ElabMode
ETyDecl Bool
True (IState -> PTerm -> PTerm
addImplPat IState
ist PTerm
t')
Int -> String -> StateT IState (ExceptT Err IO) ()
logElab 4 ("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
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\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
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]
++ " is not a pattern variable"
Just ty :: Term
ty ->
do let splits :: [PTerm]
splits = IState -> Term -> [PTerm]
findPats IState
ist Term
ty
Int -> String -> StateT IState (ExceptT Err IO) ()
logElab 1 ("New patterns " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep ", "
((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 4 ("Working from " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
t)
Int -> String -> StateT IState (ExceptT Err IO) ()
logElab 4 ("Trying " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep "\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)
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 fails :: [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 (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 newPats :: [PTerm]
newPats -> do
Int -> String -> StateT IState (ExceptT Err IO) ()
logElab 3 ("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 3 ("Split:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
(String -> [String] -> String
showSep "\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 3 "----"
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 1 ("Name updates " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
showSep "\n"
(((PTerm, [(Name, PTerm)]) -> String)
-> [(PTerm, [(Name, PTerm)])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: PTerm
p, u :: [(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
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 (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 ok :: [a]
ok bad :: [a]
bad [] = if [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 ok :: [a]
ok bad :: [a]
bad ((tc :: Bool
tc, p :: a
p) : ps :: [(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 n :: Name
n tm :: 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 :: [(Name, PTerm)]
updates = ((Name
n, PTerm -> PTerm
stripNS PTerm
tm) (Name, PTerm) -> [(Name, PTerm)] -> [(Name, PTerm)]
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 ist :: IState
ist ty :: Maybe Name
ty n :: 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
Nothing -> []
Just t :: Name
t -> IState -> Name -> [Name]
getNameHints IState
ist Name
t
let nsupp :: [Name]
nsupp = case Name
n of
MN i :: Int
i n :: 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
== '_'
-> [Name] -> [Name]
mkSupply ([Name]
supp [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
varlist)
MN i :: Int
i n :: 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 n :: Text
n | Text -> Char
thead Text
n Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '_'
-> [Name] -> [Name]
mkSupply ([Name]
supp [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
varlist)
x :: 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 n' :: Name
n' -> Name -> State MergeState Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n'
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 :: [(Name, Name)]
invented = (Name
n, Name
n') (Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
: MergeState -> [(Name, Name)]
invented MergeState
ms })
Name -> State MergeState Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n'
mkSupply :: [Name] -> [Name]
mkSupply :: [Name] -> [Name]
mkSupply ns :: [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' xs :: [Name]
xs ns' :: [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]
:[])) "xyzwstuv"
stripNS :: PTerm -> PTerm
stripNS :: PTerm -> PTerm
stripNS tm :: PTerm
tm = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
dens PTerm
tm where
dens :: PTerm -> PTerm
dens (PRef fc :: FC
fc hls :: [FC]
hls n :: Name
n) = FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
hls (Name -> Name
nsroot Name
n)
dens t :: PTerm
t = PTerm
t
mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
mergeAllPats ist :: IState
ist cv :: Name
cv t :: PTerm
t [] = []
mergeAllPats ist :: IState
ist cv :: Name
cv t :: PTerm
t (p :: PTerm
p : ps :: [PTerm]
ps)
= let (p' :: PTerm
p', MS _ _ _ u :: [(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 _ _ n :: Name
n) = [Name
n]
patvars (PApp _ _ as :: [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 _ n :: Name
n) = [Name
n]
patvars _ = []
mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
mergePat ist :: IState
ist orig :: PTerm
orig new :: PTerm
new t :: Maybe Name
t =
do
case IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause IState
ist PTerm
orig PTerm
new of
Left _ -> () -> State MergeState ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Right ns :: [(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 (n :: Name
n, PRef fc :: FC
fc _ n' :: 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 :: [(Name, Name)]
namemap = ((Name
n', Name
n) (Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
: MergeState -> [(Name, Name)]
namemap MergeState
ms) })
addNameMap _ = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
mergePat' :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm
mergePat' ist :: IState
ist (PPatvar fc :: FC
fc n :: Name
n) new :: PTerm
new t :: 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' ist :: IState
ist old :: PTerm
old (PPatvar fc :: FC
fc n :: Name
n) t :: 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' ist :: IState
ist orig :: PTerm
orig@(PRef fc :: FC
fc _ n :: Name
n) new :: PTerm
new@(PRef _ _ n' :: Name
n') t :: 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 (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 x :: Name
x -> do Name -> PTerm -> State MergeState ()
addUpdate Name
n (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
x)
PTerm -> State MergeState PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
x)
Nothing -> do MergeState -> State MergeState ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (MergeState
ms { namemap :: [(Name, Name)]
namemap = ((Name
n', Name
n) (Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
: MergeState -> [(Name, Name)]
namemap MergeState
ms) })
PTerm -> State MergeState PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n)
mergePat' ist :: IState
ist (PApp _ _ args :: [PArg]
args) (PApp fc :: FC
fc f :: PTerm
f args' :: [PArg]
args') t :: 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 (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 x :: PArg
x (y :: PArg
y, t :: 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 _ _ _ _ _) ->
PArg -> StateT MergeState Identity PArg
forall (m :: * -> *) a. Monad m => a -> m a
return (PArg
y { machine_inf :: Bool
machine_inf = PArg -> Bool
forall t. PArg' t -> Bool
machine_inf PArg
x,
getTm :: PTerm
getTm = PTerm
tm' })
_ -> PArg -> StateT MergeState Identity PArg
forall (m :: * -> *) a. Monad m => a -> m a
return (PArg
y { getTm :: PTerm
getTm = PTerm
tm' })
mergePat' ist :: IState
ist (PRef fc :: FC
fc _ n :: Name
n) tm :: PTerm
tm ty :: 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 (m :: * -> *) a. Monad m => a -> m a
return PTerm
tm
mergePat' ist :: IState
ist x :: PTerm
x y :: PTerm
y t :: Maybe Name
t = PTerm -> State MergeState PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
y
mergeUserImpl :: PTerm -> PTerm -> PTerm
mergeUserImpl :: PTerm -> PTerm -> PTerm
mergeUserImpl x :: PTerm
x y :: PTerm
y = PTerm
x
argTys :: IState -> PTerm -> [Maybe Name]
argTys :: IState -> PTerm -> [Maybe Name]
argTys ist :: IState
ist (PRef fc :: FC
fc hls :: [FC]
hls n :: Name
n)
= case Name -> Context -> [Term]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
[ty :: 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
_ -> Maybe Name -> [Maybe Name]
forall a. a -> [a]
repeat Maybe Name
forall a. Maybe a
Nothing
where tyName :: Term -> Maybe Name
tyName (Bind _ (Pi _ _ _ _) _) = Name -> Maybe Name
forall a. a -> Maybe a
Just (String -> Name
sUN "->")
tyName t :: Term
t | (P _ d :: Name
d _, [_, ty :: 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 "Delayed" = Term -> Maybe Name
tyName Term
ty
| (P _ n :: Name
n _, _) <- 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 _ _ = 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 ist :: IState
ist orig :: PTerm
orig@(PRef fc :: FC
fc hls :: [FC]
hls n :: Name
n) ty :: 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 x :: Name
x -> PTerm -> State MergeState PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
x)
Nothing -> case Name
n of
(UN _) -> PTerm -> State MergeState PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
orig
_ -> do Name
n' <- IState -> Maybe Name -> Name -> State MergeState Name
inventName IState
ist Maybe Name
ty Name
n
PTerm -> State MergeState PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n')
tidy ist :: IState
ist (PApp fc :: FC
fc f :: PTerm
f args :: [PArg]
args) ty :: 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 (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 x :: PArg
x ty' :: 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 (m :: * -> *) a. Monad m => a -> m a
return (PArg
x { getTm :: PTerm
getTm = PTerm
tm' })
tidy ist :: IState
ist tm :: PTerm
tm ty :: Maybe Name
ty = PTerm -> State MergeState PTerm
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 t :: 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 (tm :: Term
tm, ty :: Term
ty) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabVal (FC -> ElabInfo
recinfo (String -> FC
fileFC "casesplit")) ElabMode
ELHS PTerm
t
IState
i <- Idris IState
getIState
(Bool, PTerm) -> StateT IState (ExceptT Err IO) (Bool, PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, IState -> Term -> PTerm
delabDirect IState
i Term
tm))
(\e :: Err
e -> do IState
i <- Idris IState
getIState
Int -> String -> StateT IState (ExceptT Err IO) ()
logElab 5 (String -> StateT IState (ExceptT Err IO) ())
-> String -> StateT IState (ExceptT Err IO) ()
forall a b. (a -> b) -> a -> b
$ "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]
++ "\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 (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, PTerm
t))
findPats :: IState -> Type -> [PTerm]
findPats :: IState -> Term -> [PTerm]
findPats ist :: IState
ist t :: Term
t | (P _ n :: Name
n _, _) <- 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
[ti :: TypeInfo
ti] -> (Name -> PTerm) -> [Name] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map Name -> PTerm
genPat (TypeInfo -> [Name]
con_names TypeInfo
ti)
_ -> [PTerm
Placeholder]
where genPat :: Name -> PTerm
genPat n :: Name
n = case Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [PArg]
idris_implicits IState
ist) of
[args :: [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)
_ -> String -> PTerm
forall a. HasCallStack => String -> a
error (String -> PTerm) -> String -> PTerm
forall a b. (a -> b) -> a -> b
$ "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 tm :: PArg
tm = PArg
tm { getTm :: PTerm
getTm = PTerm
Placeholder }
findPats ist :: IState
ist t :: Term
t = [PTerm
Placeholder]
replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
replaceVar ctxt :: Context
ctxt n :: Name
n t :: PTerm
t (PApp fc :: FC
fc f :: PTerm
f pats :: [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 _ v :: 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 _ _ v :: 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 _ _ _) = PTerm
Placeholder
subst (PApp fc :: FC
fc (PRef _ _ t :: Name
t) pats :: [PArg]
pats)
| Name -> Context -> Bool
isTConName Name
t Context
ctxt = PTerm
Placeholder
subst (PApp fc :: FC
fc f :: PTerm
f pats :: [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 x :: PTerm
x = PTerm
x
substArg :: PArg -> PArg
substArg arg :: PArg
arg = PArg
arg { getTm :: PTerm
getTm = PTerm -> PTerm
subst (PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
arg) }
replaceVar ctxt :: Context
ctxt n :: Name
n t :: PTerm
t pat :: PTerm
pat = PTerm
pat
splitOnLine :: Int
-> Name
-> FilePath
-> Idris (Bool, [[(Name, PTerm)]])
splitOnLine :: Int -> Name -> String -> Idris (Bool, [[(Name, PTerm)]])
splitOnLine l :: Int
l n :: Name
n fn :: String
fn = do
PTerm
cl <- String -> Int -> Idris PTerm
getInternalApp String
fn Int
l
Int -> String -> StateT IState (ExceptT Err IO) ()
logElab 3 ("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 (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 l :: String
l ups :: [[(Name, PTerm)]]
ups impossible :: Bool
impossible
= do IState
ist <- Idris IState
getIState
Integer -> [String] -> Idris [String]
forall b. (Show b, Num b) => b -> [String] -> Idris [String]
updateRHSs 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 ist :: IState
ist str :: String
str [] = String
str String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
rep ist :: IState
ist str :: String
str ((n :: a
n, tm :: PTerm
tm) : ups :: [(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 i :: b
i [] = [String] -> Idris [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
updateRHSs i :: b
i (x :: String
x : xs :: [String]
xs)
| Bool
impossible = do [String]
xs' <- b -> [String] -> Idris [String]
updateRHSs b
i [String]
xs
[String] -> Idris [String]
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 (x' :: String
x', i' :: 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 (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 (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 last :: Bool
last i :: b
i ('?':'=':xs :: String
xs) = do (xs' :: String
xs', i' :: 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 (m :: * -> *) a. Monad m => a -> m a
return ("?=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
xs', b
i')
updateRHS last :: Bool
last i :: b
i ('?':xs :: String
xs)
= do let (nm :: String
nm, rest_in :: 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
. (\x :: Char
x -> Char -> Bool
isSpace Char
x Bool -> Bool -> Bool
|| Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== ')'
Bool -> Bool -> Bool
|| Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '(')) 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
=='\n')) String
rest_in of
(_, restnl :: String
restnl) -> String
restnl
(nm' :: String
nm', i' :: 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 (m :: * -> *) a. Monad m => a -> m a
return ('?'Char -> String -> String
forall a. a -> [a] -> [a]
:String
nm' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rest, b
i')
updateRHS last :: Bool
last i :: b
i (x :: Char
x : xs :: String
xs) = do (xs' :: String
xs', i' :: 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 (m :: * -> *) a. Monad m => a -> m a
return (Char
x Char -> String -> String
forall a. a -> [a] -> [a]
: String
xs', b
i')
updateRHS last :: Bool
last i :: b
i [] = (String, b) -> StateT IState (ExceptT Err IO) (String, b)
forall (m :: * -> *) a. Monad m => a -> m a
return ("", b
i)
setImpossible :: Bool -> String -> String
setImpossible brace :: Bool
brace ('}':xs :: String
xs) = '}' Char -> String -> String
forall a. a -> [a] -> [a]
: Bool -> String -> String
setImpossible Bool
False String
xs
setImpossible brace :: Bool
brace ('{':xs :: String
xs) = '{' Char -> String -> String
forall a. a -> [a] -> [a]
: Bool -> String -> String
setImpossible Bool
True String
xs
setImpossible False ('=':xs :: String
xs) = "impossible\n"
setImpossible brace :: Bool
brace (x :: Char
x : xs :: String
xs) = Char
x Char -> String -> String
forall a. a -> [a] -> [a]
: Bool -> String -> String
setImpossible Bool
brace String
xs
setImpossible brace :: Bool
brace [] = ""
nshow :: PTerm -> String
nshow (PRef _ _ (UN z :: Text
z)) | Text
z Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Z" = "Z"
nshow (PApp _ (PRef _ _ (UN s :: Text
s)) [x :: PArg
x]) | Text
s Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "S" =
"(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]
++ ")"
nshow t :: PTerm
t = PTerm -> String
forall a. Show a => a -> String
show PTerm
t
expandBraces :: String -> String
expandBraces ('{' : '-' : xs :: String
xs) = '{' Char -> String -> String
forall a. a -> [a] -> [a]
: '-' Char -> String -> String
forall a. a -> [a] -> [a]
: String
xs
expandBraces ('{' : xs :: String
xs)
= let (brace :: String
brace, (_:rest :: 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
/= '}') String
xs in
if (Bool -> Bool
not ('=' Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
brace))
then ('{' Char -> String -> String
forall a. a -> [a] -> [a]
: String
brace String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
brace String -> String -> String
forall a. [a] -> [a] -> [a]
++ "}") String -> String -> String
forall a. [a] -> [a] -> [a]
++
String -> String
expandBraces String
rest
else ('{' Char -> String -> String
forall a. a -> [a] -> [a]
: String
brace String -> String -> String
forall a. [a] -> [a] -> [a]
++ "}") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
expandBraces String
rest
expandBraces (x :: Char
x : xs :: 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 start :: Bool
start n :: String
n tm :: String
tm [] = []
updatePat start :: Bool
start n :: String
n tm :: String
tm ('{':rest :: String
rest) =
let (space :: String
space, rest' :: String
rest') = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isSpace String
rest in
'{' 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 start :: Bool
start n :: String
n tm :: String
tm done :: String
done@('?':rest :: String
rest) = String
done
updatePat True n :: String
n tm :: String
tm xs :: String
xs@(c :: Char
c:rest :: String
rest) | String -> 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 (t :: * -> *) a. Foldable t => t a -> Int
length String
n
= let (before :: String
before, after :: String
after@(next :: Char
next:_)) = Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt (String -> 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 start :: Bool
start n :: String
n tm :: String
tm (c :: Char
c:rest :: 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
== '_')) String
n String
tm String
rest
addBrackets :: String -> String
addBrackets tm :: String
tm | ' ' Char -> String -> 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
tm Bool -> Bool -> Bool
&& String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf ")" String
tm)
= "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tm String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
| Bool
otherwise = String
tm
getUniq :: (Show t, Num t) => [Char] -> t -> Idris ([Char], t)
getUniq :: String -> t -> Idris (String, t)
getUniq nm :: String
nm i :: 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
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 (m :: * -> *) a. Monad m => a -> m a
return (String
n, t
it -> t -> t
forall a. Num a => a -> a -> a
+1)
_ -> 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
+1)
nameRoot :: [String] -> String -> String
nameRoot acc :: [String]
acc nm :: 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]
acc
nameRoot acc :: [String]
acc nm :: 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
/='_') String
nm of
(before :: String
before, ('_' : after :: String
after)) -> [String] -> String -> String
nameRoot ([String]
acc [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
before]) String
after
_ -> String -> [String] -> String
showSep "_" ([String]
acc [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
nm])
showLHSName :: Name -> String
showLHSName :: Name -> String
showLHSName n :: 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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
opChars) String
fn
then "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fn String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
else String
fn
showRHSName :: Name -> String
showRHSName :: Name -> String
showRHSName n :: 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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
opChars) String
fn
then "op"
else String
fn
getClause :: Int
-> Name
-> Name
-> FilePath
-> Idris String
getClause :: Int -> Name -> Name -> String -> Idris String
getClause l :: Int
l _ un :: Name
un fp :: 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
[c :: InterfaceInfo
c] -> String -> Idris String
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))
_ -> do PTerm
ty_in <- String -> Int -> Idris PTerm
getInternalApp String
fp Int
l
let ty :: PTerm
ty = case PTerm
ty_in of
PTyped _ t :: PTerm
t -> PTerm
t
x :: 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 (m :: * -> *) a. Monad m => a -> m a
return (Name -> String
showLHSName Name
un String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
app String -> String -> String
forall a. [a] -> [a] -> [a]
++ "= ?"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
showRHSName Name
un String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_rhs")
where mkApp :: IState -> PTerm -> [Name] -> String
mkApp :: IState -> PTerm -> [Name] -> String
mkApp i :: IState
i (PPi (Exp _ _ False _) (MN _ _) _ ty :: PTerm
ty sc :: PTerm
sc) used :: [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
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 i :: IState
i (PPi (Exp _ _ False _) (UN n :: Text
n) _ ty :: PTerm
ty sc :: PTerm
sc) used :: [Name]
used
| Text -> Char
thead Text
n Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '_'
= 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
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 i :: IState
i (PPi (Exp _ _ False _) n :: Name
n _ _ sc :: PTerm
sc) used :: [Name]
used
= Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " 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 i :: IState
i (PPi _ _ _ _ sc :: PTerm
sc) used :: [Name]
used = IState -> PTerm -> [Name] -> String
mkApp IState
i PTerm
sc [Name]
used
mkApp i :: IState
i _ _ = ""
getNameFrom :: IState -> [Name] -> PTerm -> Name
getNameFrom i :: IState
i used :: [Name]
used (PPi _ _ _ _ _)
= [Name] -> [Name] -> Name
uniqueNameFrom ([Name] -> [Name]
mkSupply [String -> Name
sUN "f", String -> Name
sUN "g"]) [Name]
used
getNameFrom i :: IState
i used :: [Name]
used (PApp fc :: FC
fc f :: PTerm
f as :: [PArg]
as) = IState -> [Name] -> PTerm -> Name
getNameFrom IState
i [Name]
used PTerm
f
getNameFrom i :: IState
i used :: [Name]
used (PRef fc :: FC
fc _ f :: Name
f)
= case IState -> Name -> [Name]
getNameHints IState
i Name
f of
[] -> [Name] -> [Name] -> Name
uniqueNameFrom ([Name] -> [Name]
mkSupply [String -> Name
sUN "x", String -> Name
sUN "y",
String -> Name
sUN "z"]) [Name]
used
ns :: [Name]
ns -> [Name] -> [Name] -> Name
uniqueNameFrom ([Name] -> [Name]
mkSupply [Name]
ns) [Name]
used
getNameFrom i :: IState
i used :: [Name]
used _ = [Name] -> [Name] -> Name
uniqueNameFrom ([Name] -> [Name]
mkSupply [String -> Name
sUN "x", String -> Name
sUN "y",
String -> Name
sUN "z"]) [Name]
used
mkInterfaceBodies :: Int -> IState -> [(Name, (Bool, FnOpts, PTerm))] -> String
mkInterfaceBodies :: Int -> IState -> [(Name, (Bool, FnOpts, PTerm))] -> String
mkInterfaceBodies indent :: Int
indent i :: IState
i ns :: [(Name, (Bool, FnOpts, PTerm))]
ns
= String -> [String] -> String
showSep "\n"
(((Name, (Bool, FnOpts, PTerm)) -> Integer -> String)
-> [(Name, (Bool, FnOpts, PTerm))] -> [Integer] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(n :: Name
n, (_, _, ty :: PTerm
ty)) m :: Integer
m -> Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
indent ' ' 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
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
forall a. [a] -> [a] -> [a]
++ Name -> String
showRHSName Name
un String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_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 [1..])
def :: String -> String
def n :: String
n@(x :: Char
x:xs :: String
xs) | Bool -> Bool
not (Char -> Bool
isAlphaNum Char
x) = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
def n :: String
n = String
n
getProofClause :: Int
-> Name
-> FilePath
-> Idris String
getProofClause :: Int -> Name -> String -> Idris String
getProofClause l :: Int
l fn :: Name
fn fp :: 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 n :: PTerm
n t :: PTerm
t -> PTerm
t
x :: PTerm
x -> PTerm
x
String -> Idris String
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
forall a. [a] -> [a] -> [a]
++ Name -> String
showRHSName Name
fn String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_rhs")
where mkApp :: PTerm -> String
mkApp (PPi _ _ _ _ sc :: PTerm
sc) = PTerm -> String
mkApp PTerm
sc
mkApp rt :: PTerm
rt = "(" 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
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 str :: String
str n :: Name
n indent :: Int
indent = let str' :: String
str' = String -> String -> String
replaceRHS String
str "with (_)"
in String
str' String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
newpat String
str
where replaceRHS :: String -> String -> String
replaceRHS [] str :: String
str = String
str
replaceRHS ('?':'=': rest :: String
rest) str :: String
str = String
str
replaceRHS ('=': rest :: String
rest) str :: String
str
| Bool -> Bool
not ('=' Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
rest) = String
str
replaceRHS (x :: Char
x : rest :: String
rest) str :: String
str = Char
x Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String -> String
replaceRHS String
rest String
str
newpat :: String -> String
newpat ('>':patstr :: String
patstr) = '>'Char -> String -> String
forall a. a -> [a] -> [a]
:String -> String
newpat String
patstr
newpat patstr :: String
patstr = Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
indent ' ' String -> String -> String
forall a. [a] -> [a] -> [a]
++
String -> String -> String
replaceRHS String
patstr "| with_pat = ?" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
showRHSName Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_rhs"
nameMissing :: [PTerm] -> Idris [PTerm]
nameMissing :: [PTerm] -> Idris [PTerm]
nameMissing ps :: [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)
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 "_") (PTerm -> PTerm
base ([PTerm] -> PTerm
forall a. [a] -> a
head [PTerm]
ps))
[PTerm]
newPats
[PTerm] -> Idris [PTerm]
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
fc f :: PTerm
f args :: [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 (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 "_")))) [PArg]
args)
base t :: PTerm
t = PTerm
t
nm :: PTerm -> Idris PTerm
nm ptm :: PTerm
ptm = do (Bool, PTerm)
mptm <- PTerm -> StateT IState (ExceptT Err IO) (Bool, PTerm)
elabNewPat PTerm
ptm
case (Bool, PTerm)
mptm of
(False, _) -> PTerm -> Idris PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
ptm
(True, ptm' :: PTerm
ptm') -> PTerm -> Idris PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
ptm'