{-|
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
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
(PEArgType -> PEArgType -> Bool)
-> (PEArgType -> PEArgType -> Bool) -> Eq PEArgType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PEArgType -> PEArgType -> Bool
== :: PEArgType -> PEArgType -> Bool
$c/= :: PEArgType -> PEArgType -> Bool
/= :: PEArgType -> PEArgType -> Bool
Eq, Int -> PEArgType -> ShowS
[PEArgType] -> ShowS
PEArgType -> String
(Int -> PEArgType -> ShowS)
-> (PEArgType -> String)
-> ([PEArgType] -> ShowS)
-> Show PEArgType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PEArgType -> ShowS
showsPrec :: Int -> PEArgType -> ShowS
$cshow :: PEArgType -> String
show :: PEArgType -> String
$cshowList :: [PEArgType] -> ShowS
showList :: [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 = (Either Term (Term, Term) -> Maybe (Either Term (Term, Term)))
-> [Either Term (Term, Term)] -> Maybe [Either Term (Term, Term)]
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 Either Term (Term, Term) -> Maybe (Either Term (Term, Term))
forall {a} {a}. Either a (a, Term) -> Maybe (Either a (a, Term))
peClause [Either Term (Term, Term)]
tms where
   ns :: [(Name, Maybe Int)]
ns = [(Name, Maybe Int)] -> [(Name, Maybe Int)]
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) <- a -> [(a, Maybe a)] -> Maybe (Maybe a)
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, a -> Maybe a
forall a. a -> Maybe a
Just (a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
y)) (a, Maybe a) -> [(a, Maybe a)] -> [(a, Maybe a)]
forall a. a -> [a] -> [a]
: a -> [(a, Maybe a)] -> [(a, Maybe a)]
forall {t} {b}. Eq t => t -> [(t, b)] -> [(t, b)]
drop a
n [(a, Maybe a)]
ns)
       | Bool
otherwise = (a
n, a -> Maybe a
forall a. a -> Maybe a
Just a
x) (a, Maybe a) -> [(a, Maybe a)] -> [(a, Maybe a)]
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 (a, Maybe a) -> [(a, Maybe a)] -> [(a, Maybe a)]
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 t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
m = [(t, b)]
ns
   drop t
n ((t, b)
x : [(t, b)]
ns) = (t, b)
x (t, b) -> [(t, b)] -> [(t, b)]
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) = Either a (a, Term) -> Maybe (Either a (a, Term))
forall a. a -> Maybe a
Just (Either a (a, Term) -> Maybe (Either a (a, Term)))
-> Either a (a, Term) -> Maybe (Either a (a, Term))
forall a b. (a -> b) -> a -> b
$ a -> Either a (a, Term)
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 [] (((Name, Maybe Int) -> (Name, Int))
-> [(Name, Maybe Int)] -> [(Name, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Maybe Int) -> (Name, Int)
forall {b}. Num b => (Name, Maybe b) -> (Name, b)
toLimit [(Name, Maybe Int)]
ns) Term
rhs in
             do Bool -> Maybe () -> Maybe ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Either Term (Term, Term)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Term (Term, Term)]
tms Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) (Maybe () -> Maybe ()) -> Maybe () -> Maybe ()
forall a b. (a -> b) -> a -> b
$ [(Name, Maybe Int)] -> [(Name, Int)] -> Maybe ()
forall {a} {a}.
(Ord a, Num a, Eq a) =>
[(a, Maybe a)] -> [(a, a)] -> Maybe ()
checkProgress [(Name, Maybe Int)]
ns [(Name, Int)]
reductions
                Either a (a, Term) -> Maybe (Either a (a, Term))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, Term) -> Either a (a, Term)
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 [] = () -> Maybe ()
forall a. a -> Maybe a
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) <- a -> [(a, Maybe a)] -> Maybe (Maybe a)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
n [(a, Maybe a)]
ns
             = if a
start a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
1 Bool -> Bool -> Bool
|| a
r a -> a -> Bool
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 Maybe ()
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') = State [((PEArgType, Term), Name)] Term
-> [((PEArgType, Term), Name)]
-> (Term, [((PEArgType, Term), Name)])
forall s a. State s a -> s -> (a, s)
runState ([(PEArgType, Term)]
-> Term -> State [((PEArgType, Term), Name)] Term
forall {n} {m :: * -> *}.
(Eq n, MonadState [((PEArgType, TT n), Name)] m) =>
[(PEArgType, TT n)] -> Term -> m Term
unifyEq [(PEArgType, Term)]
args Term
ty) [] in
                       ([(PEArgType, Term)] -> Term -> Term
forall {n}. [(PEArgType, TT n)] -> TT n -> TT n
st ((((PEArgType, Term), Name) -> (PEArgType, Term))
-> [((PEArgType, Term), Name)] -> [(PEArgType, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((PEArgType, Term), Name) -> (PEArgType, Term)
forall a b. (a, b) -> a
fst [((PEArgType, Term), Name)]
args') Term
t, (((PEArgType, Term), Name) -> (PEArgType, Term))
-> [((PEArgType, Term), Name)] -> [(PEArgType, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((PEArgType, Term), Name) -> (PEArgType, Term)
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)
         = n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> TT n -> TT n -> Binder (TT 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)
         = n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> TT n -> TT n -> Binder (TT 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)
         = n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> TT n -> TT n -> Binder (TT 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)
         = n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> Maybe ImplicitInfo -> TT n -> TT n -> Binder (TT 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 <- m [((PEArgType, TT n), Name)]
forall s (m :: * -> *). MonadState s m => m s
get
              case (PEArgType, TT n) -> [((PEArgType, TT n), Name)] -> Maybe Name
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 [((PEArgType, TT n), Name)] -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([((PEArgType, TT n), Name)]
amap [((PEArgType, TT n), Name)]
-> [((PEArgType, TT n), Name)] -> [((PEArgType, TT n), Name)]
forall a. [a] -> [a] -> [a]
++ [((PEArgType
UnifiedD, TT n
forall n. TT n
Erased), Name
n)])
                           Term
sc' <- [(PEArgType, TT n)] -> Term -> m Term
unifyEq [(PEArgType, TT n)]
xs (Name -> Term -> Term -> Term
forall n. Eq n => n -> TT n -> TT n -> TT n
subst Name
n (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n' Term
forall n. TT n
Erased) Term
sc)
                           Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
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 [((PEArgType, TT n), Name)] -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([((PEArgType, TT n), Name)]
amap [((PEArgType, TT n), Name)]
-> [((PEArgType, TT n), Name)] -> [((PEArgType, TT n), Name)]
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
                           Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
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 <- m [((PEArgType, TT n), Name)]
forall s (m :: * -> *). MonadState s m => m s
get
              [((PEArgType, TT n), Name)] -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([((PEArgType, TT n), Name)]
args [((PEArgType, TT n), Name)]
-> [((PEArgType, TT n), Name)] -> [((PEArgType, TT n), Name)]
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
              Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
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 <- m [((PEArgType, TT n), Name)]
forall s (m :: * -> *). MonadState s m => m s
get
                      [((PEArgType, TT n), Name)] -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([((PEArgType, TT n), Name)]
args [((PEArgType, TT n), Name)]
-> [((PEArgType, TT n), Name)] -> [((PEArgType, TT n), Name)]
forall a. [a] -> [a] -> [a]
++ ([(PEArgType, TT n)] -> [Name] -> [((PEArgType, TT n), Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(PEArgType, TT n)]
xs (Name -> [Name]
forall a. a -> [a]
repeat (String -> Name
sUN String
"_"))))
                      Term -> m Term
forall a. a -> m a
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 = [(PEArgType, Term)] -> Term -> PTerm
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 = State Int Term -> Int -> Term
forall s a. State s a -> s -> a
evalState (Term -> State Int Term
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) <- Term -> (Term, [Term])
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 <- m Int
forall s (m :: * -> *). MonadState s m => m s
get
             Int -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
nm Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
             Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound (Int -> String -> Name
sMN Int
nm String
"spec") Term
forall n. TT n
Erased)
    gen (App AppStatus Name
s Term
f Term
a) = AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s (Term -> Term -> Term) -> m Term -> m (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
gen Term
f m (Term -> Term) -> m Term -> m Term
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
gen Term
a
    gen Term
tm = Term -> m Term
forall a. a -> m a
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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
v = case Name -> Ctxt InterfaceInfo -> [InterfaceInfo]
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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
v = (Term -> Bool) -> [Term] -> Bool
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) <- Term -> (Term, [Term])
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
_] -> (Term -> Bool) -> [Term] -> Bool
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 | (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
forall {n}. TT n -> Bool
dynVar (((Term, Term) -> Term) -> [(Term, Term)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term, Term) -> Term
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 TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
ap of
                         (TT n
_, [TT n]
args) -> [(PEArgType, Term)] -> [TT n] -> Bool
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 (((Term, Term) -> (PTerm, PTerm))
-> [(Term, Term)] -> [(PTerm, PTerm)]
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) = Term -> (Term, [Term])
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)
         = PTerm -> PArg' PTerm
forall {t}. t -> PArg' t
pexp (IState -> Term -> PTerm
delab IState
ist ([(Name, Term)] -> Term -> Term
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, Term)]
sub Term
a)) PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
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)
         = Name -> PTerm -> Bool -> PArg' PTerm
forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n (IState -> Term -> PTerm
delab IState
ist ([(Name, Term)] -> Term -> Term
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, Term)]
sub Term
a)) Bool
True PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
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)
         = PTerm -> PArg' PTerm
forall {t}. t -> PArg' t
pconst (IState -> Term -> PTerm
delab IState
ist ([(Name, Term)] -> Term -> Term
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, Term)]
sub Term
a)) PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
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 (Term -> Term -> [(Name, Term)] -> [(Name, Term)]
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 (Term -> Term -> [(Name, Term)] -> [(Name, Term)]
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 (Term -> Term -> [(Name, Term)] -> [(Name, Term)]
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) (a, b) -> [(a, b)] -> [(a, b)]
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 = PTerm -> PArg' PTerm
forall {t}. t -> PArg' t
pexp (IState -> Term -> PTerm
delab IState
ist Term
t) PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
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 PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
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 PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
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
          = Name -> PTerm -> Bool -> PArg' PTerm
forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n (IState -> Term -> PTerm
delab IState
ist Term
t) Bool
True PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
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 PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
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
          = PTerm -> PArg' PTerm
forall {t}. t -> PArg' t
pconst (IState -> Term -> PTerm
delab IState
ist Term
t) PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
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 = [Name] -> PTerm -> PTerm
forall {t :: * -> *}. Foldable t => t Name -> PTerm -> PTerm
eraseDeps [Name]
deps (PTerm -> PTerm) -> PTerm -> PTerm
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 = [Name] -> PTerm -> PTerm
forall {t :: * -> *}. Foldable t => t Name -> PTerm -> PTerm
eraseDeps [Name]
deps (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
                  IState -> Term -> PTerm
delab IState
ist (Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
sname Term
forall n. TT n
Erased) (((PEArgType, Term) -> Term) -> [(PEArgType, Term)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (PEArgType, Term) -> Term
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) $
                   Name
-> Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
-> Maybe ([([(Name, Term)], Term, Term)], [PTerm])
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 (([([(Name, Term)], Term, Term)], [PTerm]) -> [(Term, Term)]
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
_) = ((a, a, b) -> (a, b)) -> [(a, a, b)] -> [(a, 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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` PTerm -> [Name]
allNamesIn PTerm
sc = Name
n Name -> [Name] -> [Name]
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) = PTerm -> PArg' PTerm
forall {t}. t -> PArg' t
pexp (IState -> Term -> PTerm
delab IState
ist Term
tm) PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
forall a. a -> [a] -> [a]
: [(PEArgType, Term)] -> [PArg' PTerm]
mkp [(PEArgType, Term)]
tms
  mkp ((ImplicitD Name
n, Term
tm) : [(PEArgType, Term)]
tms) = Name -> PTerm -> Bool -> PArg' PTerm
forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
n (IState -> Term -> PTerm
delab IState
ist Term
tm) Bool
True PArg' PTerm -> [PArg' PTerm] -> [PArg' PTerm]
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 (t Name -> PTerm -> PTerm
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 ((PArg' PTerm -> PArg' PTerm) -> [PArg' PTerm] -> [PArg' PTerm]
forall a b. (a -> b) -> [a] -> [b]
map (t Name -> PArg' PTerm -> PArg' PTerm
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 | PArg' PTerm -> Name
forall t. PArg' t -> Name
pname PArg' PTerm
a Name -> t Name -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
ns = PArg' PTerm
a { getTm = 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 (Term -> Term
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 <- PArg' t -> Maybe Name
forall {t}. PArg' t -> Maybe Name
imparg PArg' t
imp = (Name -> PEArgType
ImplicitS Name
n, Term
tm)
         | PArg' t -> Bool
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 <- PArg' t -> Maybe Name
forall {t}. PArg' t -> Maybe Name
imparg PArg' t
imp = (Name -> PEArgType
ImplicitD Name
nm, (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN (a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"arg")) Term
forall n. TT n
Erased))
         | PArg' t -> Bool
forall {t}. PArg' t -> Bool
constrarg PArg' t
imp = (PEArgType
ConstraintD, Term
tm)
         | Bool
otherwise = (PEArgType
ExplicitD, (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN (a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"arg")) Term
forall n. TT n
Erased))

    imparg :: PArg' t -> Maybe Name
imparg (PExp Int
_ [ArgOpt]
_ Name
_ t
_) = Maybe Name
forall a. Maybe a
Nothing
    imparg (PConstraint Int
_ [ArgOpt]
_ Name
_ t
_) = Maybe Name
forall a. Maybe a
Nothing
    imparg PArg' t
arg = Name -> Maybe Name
forall a. a -> Maybe a
Just (PArg' t -> Name
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' = p -> Bool -> PArg' t -> Term -> a -> (PEArgType, Term)
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' (PEArgType, Term) -> [(PEArgType, Term)] -> [(PEArgType, Term)]
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) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm,
                          Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` ((Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name)
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name
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 [(Name, [(PEArgType, Term)])]
-> [(Name, [(PEArgType, Term)])] -> [(Name, [(PEArgType, Term)])]
forall a. [a] -> [a] -> [a]
++ [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga [Name]
env Term
a [(Name, [(PEArgType, Term)])]
-> [(Name, [(PEArgType, Term)])] -> [(Name, [(PEArgType, Term)])]
forall a. [a] -> [a] -> [a]
++
          case (Name -> Ctxt [Bool] -> Maybe [Bool]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [Bool]
idris_statics IState
ist),
                  Name -> Ctxt [PArg' PTerm] -> Maybe [PArg' PTerm]
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 ([Bool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
statics Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Bool -> Bool -> 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 [Name]
-> [Bool]
-> [PArg' PTerm]
-> [Term]
-> [Integer]
-> [(PEArgType, Term)]
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 [(Name, [(PEArgType, Term)])]
-> [(Name, [(PEArgType, Term)])] -> [(Name, [(PEArgType, Term)])]
forall a. [a] -> [a] -> [a]
++ [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga (Name
n Name -> [Name] -> [Name]
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 Name -> [Name] -> [Name]
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 (([Name], SC) -> SC
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