{-|
Module      : Idris.PartialEval
Description : Implementation of a partial evaluator.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE FlexibleContexts, PatternGuards #-}

module Idris.PartialEval(
    partial_eval, getSpecApps, specType
  , mkPE_TyDecl, mkPE_TermDecl, PEArgType(..)
  , pe_app, pe_def, pe_clauses, pe_simple
  ) where

import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate

import Control.Monad.State

-- | Data type representing binding-time annotations for partial evaluation of arguments
data PEArgType = ImplicitS Name -- ^ Implicit static argument
               | ImplicitD Name -- ^ Implicit dynamic argument
               | ConstraintS    -- ^ Implementation constraint
               | ConstraintD    -- ^ Implementation constraint
               | ExplicitS      -- ^ Explicit static argument
               | ExplicitD      -- ^ Explicit dynamic argument
               | UnifiedD       -- ^ Erasable dynamic argument (found under unification)
  deriving (PEArgType -> PEArgType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PEArgType -> PEArgType -> Bool
$c/= :: PEArgType -> PEArgType -> Bool
== :: PEArgType -> PEArgType -> Bool
$c== :: PEArgType -> PEArgType -> Bool
Eq, Int -> PEArgType -> ShowS
[PEArgType] -> ShowS
PEArgType -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PEArgType] -> ShowS
$cshowList :: [PEArgType] -> ShowS
show :: PEArgType -> String
$cshow :: PEArgType -> String
showsPrec :: Int -> PEArgType -> ShowS
$cshowsPrec :: Int -> PEArgType -> ShowS
Show)

-- | A partially evaluated function. pe_app captures the lhs of the
-- new definition, pe_def captures the rhs, and pe_clauses is the
-- specialised implementation.
--
-- pe_simple is set if the result is always reducible, because in such
-- a case we'll also need to reduce the static argument
data PEDecl = PEDecl { PEDecl -> PTerm
pe_app :: PTerm, -- new application
                       PEDecl -> PTerm
pe_def :: PTerm, -- old application
                       PEDecl -> [(PTerm, PTerm)]
pe_clauses :: [(PTerm, PTerm)], -- clauses of new application
                       PEDecl -> Bool
pe_simple :: Bool -- if just one reducible clause
                     }

-- | Partially evaluates given terms under the given context.
-- It is an error if partial evaluation fails to make any progress.
-- Making progress is defined as: all of the names given with explicit
-- reduction limits (in practice, the function being specialised)
-- must have reduced at least once.
-- If we don't do this, we might end up making an infinite function after
-- applying the transformation.
partial_eval :: Context
            -> [(Name, Maybe Int)]
            -> [Either Term (Term, Term)]
            -> Maybe [Either Term (Term, Term)]
partial_eval :: Context
-> [(Name, Maybe Int)]
-> [Either Term (Term, Term)]
-> Maybe [Either Term (Term, Term)]
partial_eval Context
ctxt [(Name, Maybe Int)]
ns_in [Either Term (Term, Term)]
tms = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {a} {a}. Either a (a, Term) -> Maybe (Either a (a, Term))
peClause [Either Term (Term, Term)]
tms where
   ns :: [(Name, Maybe Int)]
ns = forall {a} {a}. (Eq a, Num a) => [(a, Maybe a)] -> [(a, Maybe a)]
squash [(Name, Maybe Int)]
ns_in
   squash :: [(a, Maybe a)] -> [(a, Maybe a)]
squash ((a
n, Just a
x) : [(a, Maybe a)]
ns)
       | Just (Just a
y) <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
n [(a, Maybe a)]
ns
                   = [(a, Maybe a)] -> [(a, Maybe a)]
squash ((a
n, forall a. a -> Maybe a
Just (a
x forall a. Num a => a -> a -> a
+ a
y)) forall a. a -> [a] -> [a]
: forall {t} {b}. Eq t => t -> [(t, b)] -> [(t, b)]
drop a
n [(a, Maybe a)]
ns)
       | Bool
otherwise = (a
n, forall a. a -> Maybe a
Just a
x) forall a. a -> [a] -> [a]
: [(a, Maybe a)] -> [(a, Maybe a)]
squash [(a, Maybe a)]
ns
   squash ((a, Maybe a)
n : [(a, Maybe a)]
ns) = (a, Maybe a)
n forall a. a -> [a] -> [a]
: [(a, Maybe a)] -> [(a, Maybe a)]
squash [(a, Maybe a)]
ns
   squash [] = []

   drop :: t -> [(t, b)] -> [(t, b)]
drop t
n ((t
m, b
_) : [(t, b)]
ns) | t
n forall a. Eq a => a -> a -> Bool
== t
m = [(t, b)]
ns
   drop t
n ((t, b)
x : [(t, b)]
ns) = (t, b)
x forall a. a -> [a] -> [a]
: t -> [(t, b)] -> [(t, b)]
drop t
n [(t, b)]
ns
   drop t
n [] = []

   -- If the term is not a clause, it is simply kept as is
   peClause :: Either a (a, Term) -> Maybe (Either a (a, Term))
peClause (Left a
t) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left a
t
   -- If the term is a clause, specialise the right hand side
   peClause (Right (a
lhs, Term
rhs))
       = let (Term
rhs', [(Name, Int)]
reductions) = Context -> Env -> [(Name, Int)] -> Term -> (Term, [(Name, Int)])
specialise Context
ctxt [] (forall a b. (a -> b) -> [a] -> [b]
map forall {b}. Num b => (Name, Maybe b) -> (Name, b)
toLimit [(Name, Maybe Int)]
ns) Term
rhs in
             do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Term (Term, Term)]
tms forall a. Eq a => a -> a -> Bool
== Int
1) forall a b. (a -> b) -> a -> b
$ forall {a} {a}.
(Ord a, Num a, Eq a) =>
[(a, Maybe a)] -> [(a, a)] -> Maybe ()
checkProgress [(Name, Maybe Int)]
ns [(Name, Int)]
reductions
                forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (a
lhs, Term
rhs'))

   -- TMP HACK until I do PE by WHNF rather than using main evaluator
   toLimit :: (Name, Maybe b) -> (Name, b)
toLimit (Name
n, Maybe b
Nothing) | Name -> Context -> Bool
isTCDict Name
n Context
ctxt = (Name
n, b
2)
   toLimit (Name
n, Maybe b
Nothing) = (Name
n, b
65536) -- somewhat arbitrary reduction limit
   toLimit (Name
n, Just b
l) = (Name
n, b
l)

   checkProgress :: [(a, Maybe a)] -> [(a, a)] -> Maybe ()
checkProgress [(a, Maybe a)]
ns [] = forall (m :: * -> *) a. Monad m => a -> m a
return ()
   checkProgress [(a, Maybe a)]
ns ((a
n, a
r) : [(a, a)]
rs)
      | Just (Just a
start) <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
n [(a, Maybe a)]
ns
             = if a
start forall a. Ord a => a -> a -> Bool
<= a
1 Bool -> Bool -> Bool
|| a
r forall a. Ord a => a -> a -> Bool
< a
start then [(a, Maybe a)] -> [(a, a)] -> Maybe ()
checkProgress [(a, Maybe a)]
ns [(a, a)]
rs else forall a. Maybe a
Nothing
      | Bool
otherwise = [(a, Maybe a)] -> [(a, a)] -> Maybe ()
checkProgress [(a, Maybe a)]
ns [(a, a)]
rs

-- | Specialises the type of a partially evaluated TT function returning
-- a pair of the specialised type and the types of expected arguments.
specType :: [(PEArgType, Term)] -> Type -> (Type, [(PEArgType, Term)])
specType :: [(PEArgType, Term)] -> Term -> (Term, [(PEArgType, Term)])
specType [(PEArgType, Term)]
args Term
ty = let (Term
t, [((PEArgType, Term), Name)]
args') = forall s a. State s a -> s -> (a, s)
runState (forall {n} {m :: * -> *}.
(MonadState [((PEArgType, TT n), Name)] m, Eq n) =>
[(PEArgType, TT n)] -> Term -> m Term
unifyEq [(PEArgType, Term)]
args Term
ty) [] in
                       (forall {n}. [(PEArgType, TT n)] -> TT n -> TT n
st (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [((PEArgType, Term), Name)]
args') Term
t, forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [((PEArgType, Term), Name)]
args')
  where
    -- Specialise static argument in type by let-binding provided value instead
    -- of expecting it as a function argument
    st :: [(PEArgType, TT n)] -> TT n -> TT n
st ((PEArgType
ExplicitS, TT n
v) : [(PEArgType, TT n)]
xs) (Bind n
n (Pi RigCount
rc Maybe ImplicitInfo
_ TT n
t TT n
_) TT n
sc)
         = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (forall b. RigCount -> b -> b -> Binder b
Let RigCount
rc TT n
t TT n
v) ([(PEArgType, TT n)] -> TT n -> TT n
st [(PEArgType, TT n)]
xs TT n
sc)
    st ((ImplicitS Name
_, TT n
v) : [(PEArgType, TT n)]
xs) (Bind n
n (Pi RigCount
rc Maybe ImplicitInfo
_ TT n
t TT n
_) TT n
sc)
         = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (forall b. RigCount -> b -> b -> Binder b
Let RigCount
rc TT n
t TT n
v) ([(PEArgType, TT n)] -> TT n -> TT n
st [(PEArgType, TT n)]
xs TT n
sc)
    st ((PEArgType
ConstraintS, TT n
v) : [(PEArgType, TT n)]
xs) (Bind n
n (Pi RigCount
rc Maybe ImplicitInfo
_ TT n
t TT n
_) TT n
sc)
         = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (forall b. RigCount -> b -> b -> Binder b
Let RigCount
rc TT n
t TT n
v) ([(PEArgType, TT n)] -> TT n -> TT n
st [(PEArgType, TT n)]
xs TT n
sc)
    -- Erase argument from function type
    st ((PEArgType
UnifiedD, TT n
_) : [(PEArgType, TT n)]
xs) (Bind n
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT n
t TT n
_) TT n
sc)
         = [(PEArgType, TT n)] -> TT n -> TT n
st [(PEArgType, TT n)]
xs TT n
sc
    -- Keep types as is
    st ((PEArgType, TT n)
_ : [(PEArgType, TT n)]
xs) (Bind n
n (Pi RigCount
rig Maybe ImplicitInfo
i TT n
t TT n
k) TT n
sc)
         = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i TT n
t TT n
k) ([(PEArgType, TT n)] -> TT n -> TT n
st [(PEArgType, TT n)]
xs TT n
sc)
    st [(PEArgType, TT n)]
_ TT n
t = TT n
t

    -- Erase implicit dynamic argument if existing argument shares it value,
    -- by substituting the value of previous argument
    unifyEq :: [(PEArgType, TT n)] -> Term -> m Term
unifyEq (imp :: (PEArgType, TT n)
imp@(ImplicitD Name
_, TT n
v) : [(PEArgType, TT n)]
xs) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
i Term
t Term
k) Term
sc)
         = do [((PEArgType, TT n), Name)]
amap <- forall s (m :: * -> *). MonadState s m => m s
get
              case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (PEArgType, TT n)
imp [((PEArgType, TT n), Name)]
amap of
                   Just Name
n' ->
                        do forall s (m :: * -> *). MonadState s m => s -> m ()
put ([((PEArgType, TT n), Name)]
amap forall a. [a] -> [a] -> [a]
++ [((PEArgType
UnifiedD, forall n. TT n
Erased), Name
n)])
                           Term
sc' <- [(PEArgType, TT n)] -> Term -> m Term
unifyEq [(PEArgType, TT n)]
xs (forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
n (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n' forall n. TT n
Erased) Term
sc)
                           forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i Term
t Term
k) Term
sc') -- erase later
                   Maybe Name
_ -> do forall s (m :: * -> *). MonadState s m => s -> m ()
put ([((PEArgType, TT n), Name)]
amap forall a. [a] -> [a] -> [a]
++ [((PEArgType, TT n)
imp, Name
n)])
                           Term
sc' <- [(PEArgType, TT n)] -> Term -> m Term
unifyEq [(PEArgType, TT n)]
xs Term
sc
                           forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i Term
t Term
k) Term
sc')
    unifyEq ((PEArgType, TT n)
x : [(PEArgType, TT n)]
xs) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
i Term
t Term
k) Term
sc)
         = do [((PEArgType, TT n), Name)]
args <- forall s (m :: * -> *). MonadState s m => m s
get
              forall s (m :: * -> *). MonadState s m => s -> m ()
put ([((PEArgType, TT n), Name)]
args forall a. [a] -> [a] -> [a]
++ [((PEArgType, TT n)
x, Name
n)])
              Term
sc' <- [(PEArgType, TT n)] -> Term -> m Term
unifyEq [(PEArgType, TT n)]
xs Term
sc
              forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i Term
t Term
k) Term
sc')
    unifyEq [(PEArgType, TT n)]
xs Term
t = do [((PEArgType, TT n), Name)]
args <- forall s (m :: * -> *). MonadState s m => m s
get
                      forall s (m :: * -> *). MonadState s m => s -> m ()
put ([((PEArgType, TT n), Name)]
args forall a. [a] -> [a] -> [a]
++ (forall a b. [a] -> [b] -> [(a, b)]
zip [(PEArgType, TT n)]
xs (forall a. a -> [a]
repeat (String -> Name
sUN String
"_"))))
                      forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

-- | Creates an Idris type declaration given current state and a
-- specialised TT function application type.
-- Can be used in combination with the output of 'specType'.
--
-- This should: specialise any static argument position, then generalise
-- over any function applications in the result.
mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm
mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Term -> PTerm
mkPE_TyDecl IState
ist [(PEArgType, Term)]
args Term
ty = forall {b}. [(PEArgType, b)] -> Term -> PTerm
mkty [(PEArgType, Term)]
args Term
ty
  where
    mkty :: [(PEArgType, b)] -> Term -> PTerm
mkty ((PEArgType
ExplicitD, b
v) : [(PEArgType, b)]
xs) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
t Term
k) Term
sc)
       = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
expl Name
n FC
NoFC (IState -> Term -> PTerm
delab IState
ist (Term -> Term
generaliseIn Term
t)) ([(PEArgType, b)] -> Term -> PTerm
mkty [(PEArgType, b)]
xs Term
sc)
    mkty ((PEArgType
ConstraintD, b
v) : [(PEArgType, b)]
xs) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
t Term
k) Term
sc)
         | IState -> Term -> Bool
concreteInterface IState
ist Term
t = [(PEArgType, b)] -> Term -> PTerm
mkty [(PEArgType, b)]
xs Term
sc
         | IState -> Term -> Bool
interfaceConstraint IState
ist Term
t
             = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
constraint Name
n FC
NoFC (IState -> Term -> PTerm
delab IState
ist (Term -> Term
generaliseIn Term
t)) ([(PEArgType, b)] -> Term -> PTerm
mkty [(PEArgType, b)]
xs Term
sc)
    mkty ((ImplicitD Name
_, b
v) : [(PEArgType, b)]
xs) (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
_ Term
t Term
k) Term
sc)
         = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
impl Name
n FC
NoFC (IState -> Term -> PTerm
delab IState
ist (Term -> Term
generaliseIn Term
t)) ([(PEArgType, b)] -> Term -> PTerm
mkty [(PEArgType, b)]
xs Term
sc)

    mkty ((PEArgType, b)
_ : [(PEArgType, b)]
xs) Term
t
       = [(PEArgType, b)] -> Term -> PTerm
mkty [(PEArgType, b)]
xs Term
t
    mkty [] Term
t = IState -> Term -> PTerm
delab IState
ist Term
t

    generaliseIn :: Term -> Term
generaliseIn Term
tm = forall s a. State s a -> s -> a
evalState (forall {m :: * -> *}. MonadState Int m => Term -> m Term
gen Term
tm) Int
0

    gen :: Term -> m Term
gen Term
tm | (P NameType
_ Name
fn Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
tm,
             Name -> Context -> Bool
isFnName Name
fn (IState -> Context
tt_ctxt IState
ist)
        = do Int
nm <- forall s (m :: * -> *). MonadState s m => m s
get
             forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nm forall a. Num a => a -> a -> a
+ Int
1)
             forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound (Int -> String -> Name
sMN Int
nm String
"spec") forall n. TT n
Erased)
    gen (App AppStatus Name
s Term
f Term
a) = forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
gen Term
f forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
gen Term
a
    gen Term
tm = forall (m :: * -> *) a. Monad m => a -> m a
return Term
tm

-- | Checks if a given argument is an interface constraint argument
interfaceConstraint :: Idris.AbsSyntax.IState -> TT Name -> Bool
interfaceConstraint :: IState -> Term -> Bool
interfaceConstraint IState
ist Term
v
    | (P NameType
_ Name
c Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
v = case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
c (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
                                          [InterfaceInfo
_] -> Bool
True
                                          [InterfaceInfo]
_ -> Bool
False
    | Bool
otherwise = Bool
False

-- | Checks if the given arguments of an interface constraint are all either constants
-- or references (i.e. that it doesn't contain any complex terms).
concreteInterface :: IState -> TT Name -> Bool
concreteInterface :: IState -> Term -> Bool
concreteInterface IState
ist Term
v
    | Bool -> Bool
not (IState -> Term -> Bool
interfaceConstraint IState
ist Term
v) = Bool
False
    | (P NameType
_ Name
c Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
v = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
concrete [Term]
args
    | Bool
otherwise = Bool
False
  where concrete :: Term -> Bool
concrete (Constant Const
_) = Bool
True
        concrete Term
tm | (P NameType
_ Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
tm
                         = case Name -> Context -> [Term]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
                                 [Term
_] -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
concrete [Term]
args
                                 [Term]
_ -> Bool
False
                    | Bool
otherwise = Bool
False

mkNewPats :: IState
          -> [(Term, Term)]      -- ^ definition to specialise
          -> [(PEArgType, Term)] -- ^ arguments to specialise with
          -> Name                -- ^ New name
          -> Name                -- ^ Specialised function name
          -> PTerm               -- ^ Default lhs
          -> PTerm               -- ^ Default rhs
          -> PEDecl
-- If all of the dynamic positions on the lhs are variables (rather than
-- patterns or constants) then we can just make a simple definition
-- directly applying the specialised function, since we know the
-- definition isn't going to block on any of the dynamic arguments
-- in this case
mkNewPats :: IState
-> [(Term, Term)]
-> [(PEArgType, Term)]
-> Name
-> Name
-> PTerm
-> PTerm
-> PEDecl
mkNewPats IState
ist [(Term, Term)]
d [(PEArgType, Term)]
ns Name
newname Name
sname PTerm
lhs PTerm
rhs | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall {n}. TT n -> Bool
dynVar (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Term, Term)]
d)
     = PTerm -> PTerm -> [(PTerm, PTerm)] -> Bool -> PEDecl
PEDecl PTerm
lhs PTerm
rhs [(PTerm
lhs, PTerm
rhs)] Bool
True
  where dynVar :: TT n -> Bool
dynVar TT n
ap = case forall n. TT n -> (TT n, [TT n])
unApply TT n
ap of
                         (TT n
_, [TT n]
args) -> forall {b} {n}. [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, Term)]
ns [TT n]
args
        dynArgs :: [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
_ [] = Bool
True -- can definitely reduce from here
        -- if Static, doesn't matter what the argument is
        dynArgs ((ImplicitS Name
_, b
_) : [(PEArgType, b)]
ns) (TT n
a : [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
        dynArgs ((PEArgType
ConstraintS, b
_) : [(PEArgType, b)]
ns) (TT n
a : [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
        dynArgs ((PEArgType
ExplicitS, b
_) : [(PEArgType, b)]
ns) (TT n
a : [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
        -- if Dynamic, it had better be a variable or we'll need to
        -- do some more work
        dynArgs ((PEArgType, b)
_ : [(PEArgType, b)]
ns) (V Int
_     : [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
        dynArgs ((PEArgType, b)
_ : [(PEArgType, b)]
ns) (P NameType
_ n
_ TT n
_ : [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
        dynArgs [(PEArgType, b)]
_ [TT n]
_ = Bool
False -- and now we'll get stuck

mkNewPats IState
ist [(Term, Term)]
d [(PEArgType, Term)]
ns Name
newname Name
sname PTerm
lhs PTerm
rhs =
           PTerm -> PTerm -> [(PTerm, PTerm)] -> Bool -> PEDecl
PEDecl PTerm
lhs PTerm
rhs (forall a b. (a -> b) -> [a] -> [b]
map (Term, Term) -> (PTerm, PTerm)
mkClause [(Term, Term)]
d) Bool
False
  where
    mkClause :: (Term, Term) -> (PTerm, PTerm)
    mkClause :: (Term, Term) -> (PTerm, PTerm)
mkClause (Term
oldlhs, Term
oldrhs)
         = let (Term
_, [Term]
as) = forall n. TT n -> (TT n, [TT n])
unApply Term
oldlhs
               lhsargs :: [PArg' PTerm]
lhsargs = [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs [] [(PEArgType, Term)]
ns [Term]
as
               lhs :: PTerm
lhs = FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
emptyFC (FC -> [FC] -> Name -> PTerm
PRef FC
emptyFC [] Name
newname) [PArg' PTerm]
lhsargs
               rhs :: PTerm
rhs = FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
emptyFC (FC -> [FC] -> Name -> PTerm
PRef FC
emptyFC [] Name
sname)
                                  ([(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
lhsargs) in
                     (PTerm
lhs, PTerm
rhs)

    mkLHSargs :: [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs [(Name, Term)]
_ [] [Term]
_ = []
    -- dynamics don't appear on the LHS if they're implicit
    mkLHSargs [(Name, Term)]
sub ((PEArgType
ExplicitD, Term
t) : [(PEArgType, Term)]
ns) (Term
a : [Term]
as)
         = forall {t}. t -> PArg' t
pexp (IState -> Term -> PTerm
delab IState
ist (forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, Term)]
sub Term
a)) forall a. a -> [a] -> [a]
: [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs [(Name, Term)]
sub [(PEArgType, Term)]
ns [Term]
as
    mkLHSargs [(Name, Term)]
sub ((ImplicitD Name
n, Term
t) : [(PEArgType, Term)]
ns) (Term
a : [Term]
as)
         = forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n (IState -> Term -> PTerm
delab IState
ist (forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, Term)]
sub Term
a)) Bool
True forall a. a -> [a] -> [a]
: [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs [(Name, Term)]
sub [(PEArgType, Term)]
ns [Term]
as
    mkLHSargs [(Name, Term)]
sub ((PEArgType
ConstraintD, Term
t) : [(PEArgType, Term)]
ns) (Term
a : [Term]
as)
         = forall {t}. t -> PArg' t
pconst (IState -> Term -> PTerm
delab IState
ist (forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, Term)]
sub Term
a)) forall a. a -> [a] -> [a]
: [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs [(Name, Term)]
sub [(PEArgType, Term)]
ns [Term]
as
    mkLHSargs [(Name, Term)]
sub ((PEArgType
UnifiedD, Term
_) : [(PEArgType, Term)]
ns) (Term
a : [Term]
as)
         = [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs [(Name, Term)]
sub [(PEArgType, Term)]
ns [Term]
as
    -- statics get dropped in any case
    mkLHSargs [(Name, Term)]
sub ((ImplicitS Name
_, Term
t) : [(PEArgType, Term)]
ns) (Term
a : [Term]
as)
         = [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs (forall {a} {b}. TT a -> b -> [(a, b)] -> [(a, b)]
extend Term
a Term
t [(Name, Term)]
sub) [(PEArgType, Term)]
ns [Term]
as
    mkLHSargs [(Name, Term)]
sub ((PEArgType
ExplicitS, Term
t) : [(PEArgType, Term)]
ns) (Term
a : [Term]
as)
         = [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs (forall {a} {b}. TT a -> b -> [(a, b)] -> [(a, b)]
extend Term
a Term
t [(Name, Term)]
sub) [(PEArgType, Term)]
ns [Term]
as
    mkLHSargs [(Name, Term)]
sub ((PEArgType
ConstraintS, Term
t) : [(PEArgType, Term)]
ns) (Term
a : [Term]
as)
         = [(Name, Term)] -> [(PEArgType, Term)] -> [Term] -> [PArg' PTerm]
mkLHSargs (forall {a} {b}. TT a -> b -> [(a, b)] -> [(a, b)]
extend Term
a Term
t [(Name, Term)]
sub) [(PEArgType, Term)]
ns [Term]
as
    mkLHSargs [(Name, Term)]
sub [(PEArgType, Term)]
_ [] = [] -- no more LHS

    extend :: TT a -> b -> [(a, b)] -> [(a, b)]
extend (P NameType
_ a
n TT a
_) b
t [(a, b)]
sub = (a
n, b
t) forall a. a -> [a] -> [a]
: [(a, b)]
sub
    extend TT a
_ b
_ [(a, b)]
sub = [(a, b)]
sub

    --- 'as' are the LHS arguments
    mkRHSargs :: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs ((PEArgType
ExplicitS, Term
t) : [(PEArgType, Term)]
ns) [PArg' PTerm]
as = forall {t}. t -> PArg' t
pexp (IState -> Term -> PTerm
delab IState
ist Term
t) forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
    mkRHSargs ((PEArgType
ExplicitD, Term
t) : [(PEArgType, Term)]
ns) (PArg' PTerm
a : [PArg' PTerm]
as) = PArg' PTerm
a forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
    -- Keep the implicits on the RHS, in case they got matched on
    mkRHSargs ((ImplicitD Name
n, Term
t) : [(PEArgType, Term)]
ns) (PArg' PTerm
a : [PArg' PTerm]
as) = PArg' PTerm
a forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
    mkRHSargs ((ImplicitS Name
n, Term
t) : [(PEArgType, Term)]
ns) [PArg' PTerm]
as -- Dropped from LHS
          = forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n (IState -> Term -> PTerm
delab IState
ist Term
t) Bool
True forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
    mkRHSargs ((PEArgType
ConstraintD, Term
t) : [(PEArgType, Term)]
ns) (PArg' PTerm
a : [PArg' PTerm]
as) = PArg' PTerm
a forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
    mkRHSargs ((PEArgType
ConstraintS, Term
t) : [(PEArgType, Term)]
ns) [PArg' PTerm]
as -- Dropped from LHS
          = forall {t}. t -> PArg' t
pconst (IState -> Term -> PTerm
delab IState
ist Term
t) forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
    mkRHSargs ((PEArgType, Term)
_ : [(PEArgType, Term)]
ns) [PArg' PTerm]
as = [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
    mkRHSargs [(PEArgType, Term)]
_ [PArg' PTerm]
_ = []

-- | Creates a new declaration for a specialised function application.
-- Simple version at the moment: just create a version which is a direct
-- application of the function to be specialised.
-- More complex version to do: specialise the definition clause by clause
mkPE_TermDecl :: IState
              -> Name
              -> Name
              -> PTerm -- ^ Type of specialised function
              -> [(PEArgType, Term)]
              -> PEDecl
mkPE_TermDecl :: IState -> Name -> Name -> PTerm -> [(PEArgType, Term)] -> PEDecl
mkPE_TermDecl IState
ist Name
newname Name
sname PTerm
specty [(PEArgType, Term)]
ns
      {- We need to erase the *dynamic* arguments
         where their *name* appears in the *type* of a later argument
         in specty.
         i.e. if a later dynamic argument depends on an earlier dynamic
         argument, we should infer the earlier one.
         Then we need to erase names from the LHS which no longer appear
         on the RHS.
         -}
    = let deps :: [Name]
deps = PTerm -> [Name]
getDepNames (PTerm -> PTerm
eraseRet PTerm
specty)
          lhs :: PTerm
lhs = forall {t :: * -> *}. Foldable t => t Name -> PTerm -> PTerm
eraseDeps [Name]
deps forall a b. (a -> b) -> a -> b
$
                  FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
emptyFC (FC -> [FC] -> Name -> PTerm
PRef FC
emptyFC [] Name
newname) ([(PEArgType, Term)] -> [PArg' PTerm]
mkp [(PEArgType, Term)]
ns)
          rhs :: PTerm
rhs = forall {t :: * -> *}. Foldable t => t Name -> PTerm -> PTerm
eraseDeps [Name]
deps forall a b. (a -> b) -> a -> b
$
                  IState -> Term -> PTerm
delab IState
ist (forall n. TT n -> [TT n] -> TT n
mkApp (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
sname forall n. TT n
Erased) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(PEArgType, Term)]
ns))
          patdef :: Maybe ([([(Name, Term)], Term, Term)], [PTerm])
patdef = -- trace (showTmImpls specty ++ "\n" ++ showTmImpls lhs ++ "\n"
                   --      ++ showTmImpls rhs) $
                   forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
sname (IState -> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
idris_patdefs IState
ist)
          newpats :: PEDecl
newpats = case Maybe ([([(Name, Term)], Term, Term)], [PTerm])
patdef of
                         Maybe ([([(Name, Term)], Term, Term)], [PTerm])
Nothing -> PTerm -> PTerm -> [(PTerm, PTerm)] -> Bool -> PEDecl
PEDecl PTerm
lhs PTerm
rhs [(PTerm
lhs, PTerm
rhs)] Bool
True
                         Just ([([(Name, Term)], Term, Term)], [PTerm])
d -> IState
-> [(Term, Term)]
-> [(PEArgType, Term)]
-> Name
-> Name
-> PTerm
-> PTerm
-> PEDecl
mkNewPats IState
ist (forall {a} {a} {b} {b}. ([(a, a, b)], b) -> [(a, b)]
getPats ([([(Name, Term)], Term, Term)], [PTerm])
d) [(PEArgType, Term)]
ns
                                             Name
newname Name
sname PTerm
lhs PTerm
rhs in
          PEDecl
newpats where

  getPats :: ([(a, a, b)], b) -> [(a, b)]
getPats ([(a, a, b)]
ps, b
_) = forall a b. (a -> b) -> [a] -> [b]
map (\(a
_, a
lhs, b
rhs) -> (a
lhs, b
rhs)) [(a, a, b)]
ps

  eraseRet :: PTerm -> PTerm
eraseRet (PPi Plicity
p Name
n FC
fc PTerm
ty PTerm
sc) = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc PTerm
ty (PTerm -> PTerm
eraseRet PTerm
sc)
  eraseRet PTerm
_ = PTerm
Placeholder

  -- Get names used in later arguments; assume we've called eraseRet so there's
  -- no names going to appear in return type
  getDepNames :: PTerm -> [Name]
getDepNames (PPi Plicity
_ Name
n FC
_ PTerm
_ PTerm
sc)
        | Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` PTerm -> [Name]
allNamesIn PTerm
sc = Name
n forall a. a -> [a] -> [a]
: PTerm -> [Name]
getDepNames PTerm
sc
        | Bool
otherwise = PTerm -> [Name]
getDepNames PTerm
sc
  getDepNames PTerm
tm = []

  mkp :: [(PEArgType, Term)] -> [PArg' PTerm]
mkp [] = []
  mkp ((PEArgType
ExplicitD, Term
tm) : [(PEArgType, Term)]
tms) = forall {t}. t -> PArg' t
pexp (IState -> Term -> PTerm
delab IState
ist Term
tm) forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm]
mkp [(PEArgType, Term)]
tms
  mkp ((ImplicitD Name
n, Term
tm) : [(PEArgType, Term)]
tms) = forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n (IState -> Term -> PTerm
delab IState
ist Term
tm) Bool
True forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm]
mkp [(PEArgType, Term)]
tms
  mkp ((PEArgType, Term)
_ : [(PEArgType, Term)]
tms) = [(PEArgType, Term)] -> [PArg' PTerm]
mkp [(PEArgType, Term)]
tms

  eraseDeps :: t Name -> PTerm -> PTerm
eraseDeps t Name
ns PTerm
tm = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT (forall {t :: * -> *}. Foldable t => t Name -> PTerm -> PTerm
deImp t Name
ns) PTerm
tm

  deImp :: t Name -> PTerm -> PTerm
deImp t Name
ns (PApp FC
fc PTerm
t [PArg' PTerm]
as) = FC -> PTerm -> [PArg' PTerm] -> PTerm
PApp FC
fc PTerm
t (forall a b. (a -> b) -> [a] -> [b]
map (forall {t :: * -> *}.
Foldable t =>
t Name -> PArg' PTerm -> PArg' PTerm
deImpArg t Name
ns) [PArg' PTerm]
as)
  deImp t Name
ns PTerm
t = PTerm
t

  deImpArg :: t Name -> PArg' PTerm -> PArg' PTerm
deImpArg t Name
ns PArg' PTerm
a | forall t. PArg' t -> Name
pname PArg' PTerm
a forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
ns = PArg' PTerm
a { getTm :: PTerm
getTm = PTerm
Placeholder }
                | Bool
otherwise = PArg' PTerm
a

-- | Get specialised applications for a given function
getSpecApps :: IState
            -> [Name]
            -> Term
            -> [(Name, [(PEArgType, Term)])]
getSpecApps :: IState -> [Name] -> Term -> [(Name, [(PEArgType, Term)])]
getSpecApps IState
ist [Name]
env Term
tm = [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga [Name]
env (forall n. TT n -> TT n
explicitNames Term
tm) where

--     staticArg env True _ tm@(P _ n _) _ | n `elem` env = Just (True, tm)
--     staticArg env True _ tm@(App f a) _ | (P _ n _, args) <- unApply tm,
--                                            n `elem` env = Just (True, tm)
    staticArg :: p -> Bool -> PArg' t -> Term -> a -> (PEArgType, Term)
staticArg p
env Bool
True PArg' t
imp Term
tm a
n
         | Just Name
n <- forall {t}. PArg' t -> Maybe Name
imparg PArg' t
imp = (Name -> PEArgType
ImplicitS Name
n, Term
tm)
         | forall {t}. PArg' t -> Bool
constrarg PArg' t
imp = (PEArgType
ConstraintS, Term
tm)
         | Bool
otherwise = (PEArgType
ExplicitS, Term
tm)

    staticArg p
env Bool
False PArg' t
imp Term
tm a
n
         | Just Name
nm <- forall {t}. PArg' t -> Maybe Name
imparg PArg' t
imp = (Name -> PEArgType
ImplicitD Name
nm, (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN (forall a. Show a => a -> String
show a
n forall a. [a] -> [a] -> [a]
++ String
"arg")) forall n. TT n
Erased))
         | forall {t}. PArg' t -> Bool
constrarg PArg' t
imp = (PEArgType
ConstraintD, Term
tm)
         | Bool
otherwise = (PEArgType
ExplicitD, (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN (forall a. Show a => a -> String
show a
n forall a. [a] -> [a] -> [a]
++ String
"arg")) forall n. TT n
Erased))

    imparg :: PArg' t -> Maybe Name
imparg (PExp Int
_ [ArgOpt]
_ Name
_ t
_) = forall a. Maybe a
Nothing
    imparg (PConstraint Int
_ [ArgOpt]
_ Name
_ t
_) = forall a. Maybe a
Nothing
    imparg PArg' t
arg = forall a. a -> Maybe a
Just (forall t. PArg' t -> Name
pname PArg' t
arg)

    constrarg :: PArg' t -> Bool
constrarg (PConstraint Int
_ [ArgOpt]
_ Name
_ t
_) = Bool
True
    constrarg PArg' t
arg = Bool
False

    buildApp :: p -> [Bool] -> [PArg' t] -> [Term] -> [a] -> [(PEArgType, Term)]
buildApp p
env [] [] [Term]
_ [a]
_ = []
    buildApp p
env (Bool
s:[Bool]
ss) (PArg' t
i:[PArg' t]
is) (Term
a:[Term]
as) (a
n:[a]
ns)
        = let s' :: (PEArgType, Term)
s' = forall {a} {p} {t}.
Show a =>
p -> Bool -> PArg' t -> Term -> a -> (PEArgType, Term)
staticArg p
env Bool
s PArg' t
i Term
a a
n
              ss' :: [(PEArgType, Term)]
ss' = p -> [Bool] -> [PArg' t] -> [Term] -> [a] -> [(PEArgType, Term)]
buildApp p
env [Bool]
ss [PArg' t]
is [Term]
as [a]
ns in
              ((PEArgType, Term)
s' forall a. a -> [a] -> [a]
: [(PEArgType, Term)]
ss')

    -- if we have a *defined* function that has static arguments,
    -- it will become a specialised application
    ga :: [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga [Name]
env tm :: Term
tm@(App AppStatus Name
_ Term
f Term
a) | (P NameType
_ Name
n Term
_, [Term]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Term
tm,
                          Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist) =
        [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga [Name]
env Term
f forall a. [a] -> [a] -> [a]
++ [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga [Name]
env Term
a forall a. [a] -> [a] -> [a]
++
          case (forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [Bool]
idris_statics IState
ist),
                  forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [PArg' PTerm]
idris_implicits IState
ist)) of
               (Just [Bool]
statics, Just [PArg' PTerm]
imps) ->
                   if (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
statics forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
statics
                          Bool -> Bool -> Bool
&& Context -> Name -> Bool
specialisable (IState -> Context
tt_ctxt IState
ist) Name
n) then
                      case forall {a} {p} {t}.
Show a =>
p -> [Bool] -> [PArg' t] -> [Term] -> [a] -> [(PEArgType, Term)]
buildApp [Name]
env [Bool]
statics [PArg' PTerm]
imps [Term]
args [Integer
0..] of
                           [(PEArgType, Term)]
args -> [(Name
n, [(PEArgType, Term)]
args)]
--                            _ -> []
                      else []
               (Maybe [Bool], Maybe [PArg' PTerm])
_ -> []
    ga [Name]
env (Bind Name
n (Let RigCount
rc Term
t Term
v) Term
sc) = [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga [Name]
env Term
v forall a. [a] -> [a] -> [a]
++ [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga (Name
n forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
    ga [Name]
env (Bind Name
n Binder Term
t Term
sc) = [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga (Name
n forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
    ga [Name]
env Term
t = []

    -- A function is only specialisable if there are no overlapping
    -- cases in the case tree (otherwise the partial evaluation could
    -- easily get stuck)
    specialisable :: Context -> Name -> Bool
    specialisable :: Context -> Name -> Bool
specialisable Context
ctxt Name
n = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
                                Just (CaseOp CaseInfo
_ Term
_ [(Term, Bool)]
_ [Either Term (Term, Term)]
_ [([Name], Term, Term)]
_ CaseDefs
cds) ->
                                     SC -> Bool
noOverlap (forall a b. (a, b) -> b
snd (CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cds))
                                Maybe Def
_ -> Bool
False

    noOverlap :: SC -> Bool
    noOverlap :: SC -> Bool
noOverlap (Case CaseType
_ Name
_ [DefaultCase SC
sc]) = SC -> Bool
noOverlap SC
sc
    noOverlap (Case CaseType
_ Name
_ [CaseAlt' Term]
alts) = [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
alts
    noOverlap SC
_ = Bool
True

    -- There's an overlap if the case tree has a default case along with
    -- some other cases. It's fine if there's a default case on its own.
    noOverlapAlts :: [CaseAlt' Term] -> Bool
noOverlapAlts (ConCase Name
_ Int
_ [Name]
_ SC
sc : [CaseAlt' Term]
rest)
        = [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest Bool -> Bool -> Bool
&& SC -> Bool
noOverlap SC
sc
    noOverlapAlts (FnCase Name
_ [Name]
_ SC
sc : [CaseAlt' Term]
rest) = [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest
    noOverlapAlts (ConstCase Const
_ SC
sc : [CaseAlt' Term]
rest)
        = [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest Bool -> Bool -> Bool
&& SC -> Bool
noOverlap SC
sc
    noOverlapAlts (SucCase Name
_ SC
sc : [CaseAlt' Term]
rest)
        = [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest Bool -> Bool -> Bool
&& SC -> Bool
noOverlap SC
sc
    noOverlapAlts (DefaultCase SC
_ : [CaseAlt' Term]
_) = Bool
False
    noOverlapAlts [CaseAlt' Term]
_ = Bool
True