{-|
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
(PEArgType -> PEArgType -> Bool)
-> (PEArgType -> PEArgType -> Bool) -> Eq PEArgType
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
(Int -> PEArgType -> ShowS)
-> (PEArgType -> String)
-> ([PEArgType] -> ShowS)
-> Show PEArgType
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 ctxt :: Context
ctxt ns_in :: [(Name, Maybe Int)]
ns_in tms :: [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)
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 ((n :: a
n, Just x :: a
x) : ns :: [(a, Maybe a)]
ns)
       | Just (Just y :: 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 (n :: (a, Maybe a)
n : ns :: [(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 n :: t
n ((m :: t
m, _) : ns :: [(t, b)]
ns) | t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
m = [(t, b)]
ns
   drop n :: t
n (x :: (t, b)
x : ns :: [(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 n :: 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 t :: 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 (lhs :: a
lhs, rhs :: Term
rhs))
       = let (rhs' :: Term
rhs', reductions :: [(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 (t :: * -> *) a. Foldable t => t a -> Int
length [Either Term (Term, Term)]
tms Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 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 (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 (n :: Name
n, Nothing) | Name -> Context -> Bool
isTCDict Name
n Context
ctxt = (Name
n, 2)
   toLimit (n :: Name
n, Nothing) = (Name
n, 65536) -- somewhat arbitrary reduction limit
   toLimit (n :: Name
n, Just l :: b
l) = (Name
n, b
l)

   checkProgress :: [(a, Maybe a)] -> [(a, a)] -> Maybe ()
checkProgress ns :: [(a, Maybe a)]
ns [] = () -> Maybe ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
   checkProgress ns :: [(a, Maybe a)]
ns ((n :: a
n, r :: a
r) : rs :: [(a, a)]
rs)
      | Just (Just start :: 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
<= 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 args :: [(PEArgType, Term)]
args ty :: Term
ty = let (t :: Term
t, args' :: [((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 :: * -> *).
(MonadState [((PEArgType, TT n), Name)] m, Eq n) =>
[(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 ((ExplicitS, v :: TT n
v) : xs :: [(PEArgType, TT n)]
xs) (Bind n :: n
n (Pi rc :: RigCount
rc _ t :: TT n
t _) sc :: 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 _, v :: TT n
v) : xs :: [(PEArgType, TT n)]
xs) (Bind n :: n
n (Pi rc :: RigCount
rc _ t :: TT n
t _) sc :: 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 ((ConstraintS, v :: TT n
v) : xs :: [(PEArgType, TT n)]
xs) (Bind n :: n
n (Pi rc :: RigCount
rc _ t :: TT n
t _) sc :: 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 ((UnifiedD, _) : xs :: [(PEArgType, TT n)]
xs) (Bind n :: n
n (Pi _ _ t :: TT n
t _) sc :: TT n
sc)
         = [(PEArgType, TT n)] -> TT n -> TT n
st [(PEArgType, TT n)]
xs TT n
sc
    -- Keep types as is
    st (_ : xs :: [(PEArgType, TT n)]
xs) (Bind n :: n
n (Pi rig :: RigCount
rig i :: Maybe ImplicitInfo
i t :: TT n
t k :: TT n
k) sc :: 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 _ t :: 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 _, v :: TT n
v) : xs :: [(PEArgType, TT n)]
xs) (Bind n :: Name
n (Pi rig :: RigCount
rig i :: Maybe ImplicitInfo
i t :: Term
t k :: Term
k) sc :: 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 n' :: 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 (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
                   _ -> 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 (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 (x :: (PEArgType, TT n)
x : xs :: [(PEArgType, TT n)]
xs) (Bind n :: Name
n (Pi rig :: RigCount
rig i :: Maybe ImplicitInfo
i t :: Term
t k :: Term
k) sc :: 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 (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 xs :: [(PEArgType, TT n)]
xs t :: 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 "_"))))
                      Term -> m Term
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 ist :: IState
ist args :: [(PEArgType, Term)]
args ty :: 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 ((ExplicitD, v :: b
v) : xs :: [(PEArgType, b)]
xs) (Bind n :: Name
n (Pi rig :: RigCount
rig _ t :: Term
t k :: Term
k) sc :: 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 ((ConstraintD, v :: b
v) : xs :: [(PEArgType, b)]
xs) (Bind n :: Name
n (Pi rig :: RigCount
rig _ t :: Term
t k :: Term
k) sc :: 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 _, v :: b
v) : xs :: [(PEArgType, b)]
xs) (Bind n :: Name
n (Pi rig :: RigCount
rig _ t :: Term
t k :: Term
k) sc :: 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 (_ : xs :: [(PEArgType, b)]
xs) t :: Term
t
       = [(PEArgType, b)] -> Term -> PTerm
mkty [(PEArgType, b)]
xs Term
t
    mkty [] t :: Term
t = IState -> Term -> PTerm
delab IState
ist Term
t

    generaliseIn :: Term -> Term
generaliseIn tm :: 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) 0

    gen :: Term -> m Term
gen tm :: Term
tm | (P _ fn :: Name
fn _, args :: [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
+ 1)
             Term -> m Term
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 "spec") Term
forall n. TT n
Erased)
    gen (App s :: AppStatus Name
s f :: Term
f a :: 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
gen Term
a
    gen tm :: Term
tm = Term -> m Term
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 ist :: IState
ist v :: Term
v
    | (P _ c :: Name
c _, args :: [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
                                          [_] -> Bool
True
                                          _ -> 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 ist :: IState
ist v :: Term
v
    | Bool -> Bool
not (IState -> Term -> Bool
interfaceConstraint IState
ist Term
v) = Bool
False
    | (P _ c :: Name
c _, args :: [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 _) = Bool
True
        concrete tm :: Term
tm | (P _ n :: Name
n _, args :: [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 -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
concrete [Term]
args
                                 _ -> 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 ist :: IState
ist d :: [(Term, Term)]
d ns :: [(PEArgType, Term)]
ns newname :: Name
newname sname :: Name
sname lhs :: PTerm
lhs rhs :: 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 ap :: TT n
ap = case TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
ap of
                         (_, args :: [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 _ [] = Bool
True -- can definitely reduce from here
        -- if Static, doesn't matter what the argument is
        dynArgs ((ImplicitS _, _) : ns :: [(PEArgType, b)]
ns) (a :: TT n
a : as :: [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
        dynArgs ((ConstraintS, _) : ns :: [(PEArgType, b)]
ns) (a :: TT n
a : as :: [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
        dynArgs ((ExplicitS, _) : ns :: [(PEArgType, b)]
ns) (a :: TT n
a : as :: [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 (_ : ns :: [(PEArgType, b)]
ns) (V _     : as :: [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
        dynArgs (_ : ns :: [(PEArgType, b)]
ns) (P _ _ _ : as :: [TT n]
as) = [(PEArgType, b)] -> [TT n] -> Bool
dynArgs [(PEArgType, b)]
ns [TT n]
as
        dynArgs _ _ = Bool
False -- and now we'll get stuck

mkNewPats ist :: IState
ist d :: [(Term, Term)]
d ns :: [(PEArgType, Term)]
ns newname :: Name
newname sname :: Name
sname lhs :: PTerm
lhs rhs :: 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 (oldlhs :: Term
oldlhs, oldrhs :: Term
oldrhs)
         = let (_, as :: [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 _ [] _ = []
    -- dynamics don't appear on the LHS if they're implicit
    mkLHSargs sub :: [(Name, Term)]
sub ((ExplicitD, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: Term
a : as :: [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 sub :: [(Name, Term)]
sub ((ImplicitD n :: Name
n, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: Term
a : as :: [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 sub :: [(Name, Term)]
sub ((ConstraintD, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: Term
a : as :: [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 sub :: [(Name, Term)]
sub ((UnifiedD, _) : ns :: [(PEArgType, Term)]
ns) (a :: Term
a : as :: [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 sub :: [(Name, Term)]
sub ((ImplicitS _, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: Term
a : as :: [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 sub :: [(Name, Term)]
sub ((ExplicitS, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: Term
a : as :: [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 sub :: [(Name, Term)]
sub ((ConstraintS, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: Term
a : as :: [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 sub :: [(Name, Term)]
sub _ [] = [] -- no more LHS

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

    --- 'as' are the LHS arguments
    mkRHSargs :: [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs ((ExplicitS, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) as :: [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 ((ExplicitD, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: PArg' PTerm
a : as :: [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 n :: Name
n, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: PArg' PTerm
a : as :: [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 n :: Name
n, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) as :: [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 ((ConstraintD, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) (a :: PArg' PTerm
a : as :: [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 ((ConstraintS, t :: Term
t) : ns :: [(PEArgType, Term)]
ns) as :: [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 (_ : ns :: [(PEArgType, Term)]
ns) as :: [PArg' PTerm]
as = [(PEArgType, Term)] -> [PArg' PTerm] -> [PArg' PTerm]
mkRHSargs [(PEArgType, Term)]
ns [PArg' PTerm]
as
    mkRHSargs _ _ = []

-- | 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 ist :: IState
ist newname :: Name
newname sname :: Name
sname specty :: PTerm
specty ns :: [(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
                         Nothing -> PTerm -> PTerm -> [(PTerm, PTerm)] -> Bool -> PEDecl
PEDecl PTerm
lhs PTerm
rhs [(PTerm
lhs, PTerm
rhs)] Bool
True
                         Just d :: ([([(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 (ps :: [(a, a, b)]
ps, _) = ((a, a, b) -> (a, b)) -> [(a, a, b)] -> [(a, b)]
forall a b. (a -> b) -> [a] -> [b]
map (\(_, lhs :: a
lhs, rhs :: b
rhs) -> (a
lhs, b
rhs)) [(a, a, b)]
ps

  eraseRet :: PTerm -> PTerm
eraseRet (PPi p :: Plicity
p n :: Name
n fc :: FC
fc ty :: PTerm
ty sc :: PTerm
sc) = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc PTerm
ty (PTerm -> PTerm
eraseRet PTerm
sc)
  eraseRet _ = 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 _ n :: Name
n _ _ sc :: PTerm
sc)
        | Name
n Name -> [Name] -> 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 tm :: PTerm
tm = []

  mkp :: [(PEArgType, Term)] -> [PArg' PTerm]
mkp [] = []
  mkp ((ExplicitD, tm :: Term
tm) : tms :: [(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 n :: Name
n, tm :: Term
tm) : tms :: [(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 (_ : tms :: [(PEArgType, Term)]
tms) = [(PEArgType, Term)] -> [PArg' PTerm]
mkp [(PEArgType, Term)]
tms

  eraseDeps :: t Name -> PTerm -> PTerm
eraseDeps ns :: t Name
ns tm :: 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 ns :: t Name
ns (PApp fc :: FC
fc t :: PTerm
t as :: [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 ns :: t Name
ns t :: PTerm
t = PTerm
t

  deImpArg :: t Name -> PArg' PTerm -> PArg' PTerm
deImpArg ns :: t Name
ns a :: PArg' PTerm
a | PArg' PTerm -> Name
forall t. PArg' t -> Name
pname PArg' PTerm
a Name -> t Name -> Bool
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 ist :: IState
ist env :: [Name]
env tm :: 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 env :: p
env True imp :: PArg' t
imp tm :: Term
tm n :: a
n
         | Just n :: 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 env :: p
env False imp :: PArg' t
imp tm :: Term
tm n :: a
n
         | Just nm :: 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]
++ "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]
++ "arg")) Term
forall n. TT n
Erased))

    imparg :: PArg' t -> Maybe Name
imparg (PExp _ _ _ _) = Maybe Name
forall a. Maybe a
Nothing
    imparg (PConstraint _ _ _ _) = Maybe Name
forall a. Maybe a
Nothing
    imparg arg :: 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 _ _ _ _) = Bool
True
    constrarg arg :: PArg' t
arg = Bool
False

    buildApp :: p -> [Bool] -> [PArg' t] -> [Term] -> [a] -> [(PEArgType, Term)]
buildApp env :: p
env [] [] _ _ = []
    buildApp env :: p
env (s :: Bool
s:ss :: [Bool]
ss) (i :: PArg' t
i:is :: [PArg' t]
is) (a :: Term
a:as :: [Term]
as) (n :: a
n:ns :: [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 env :: [Name]
env tm :: Term
tm@(App _ f :: Term
f a :: Term
a) | (P _ n :: Name
n _, args :: [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 statics :: [Bool]
statics, Just imps :: [PArg' PTerm]
imps) ->
                   if ([Bool] -> 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 (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 [0..] of
                           args :: [(PEArgType, Term)]
args -> [(Name
n, [(PEArgType, Term)]
args)]
--                            _ -> []
                      else []
               _ -> []
    ga env :: [Name]
env (Bind n :: Name
n (Let rc :: RigCount
rc t :: Term
t v :: Term
v) sc :: 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 env :: [Name]
env (Bind n :: Name
n t :: Binder Term
t sc :: Term
sc) = [Name] -> Term -> [(Name, [(PEArgType, Term)])]
ga (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
    ga env :: [Name]
env t :: 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 ctxt :: Context
ctxt n :: Name
n = case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
                                Just (CaseOp _ _ _ _ _ cds :: CaseDefs
cds) ->
                                     SC -> Bool
noOverlap (([Name], SC) -> SC
forall a b. (a, b) -> b
snd (CaseDefs -> ([Name], SC)
cases_compiletime CaseDefs
cds))
                                _ -> Bool
False

    noOverlap :: SC -> Bool
    noOverlap :: SC -> Bool
noOverlap (Case _ _ [DefaultCase sc :: SC
sc]) = SC -> Bool
noOverlap SC
sc
    noOverlap (Case _ _ alts :: [CaseAlt' Term]
alts) = [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
alts
    noOverlap _ = 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 _ _ _ sc :: SC
sc : rest :: [CaseAlt' Term]
rest)
        = [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest Bool -> Bool -> Bool
&& SC -> Bool
noOverlap SC
sc
    noOverlapAlts (FnCase _ _ sc :: SC
sc : rest :: [CaseAlt' Term]
rest) = [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest
    noOverlapAlts (ConstCase _ sc :: SC
sc : rest :: [CaseAlt' Term]
rest)
        = [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest Bool -> Bool -> Bool
&& SC -> Bool
noOverlap SC
sc
    noOverlapAlts (SucCase _ sc :: SC
sc : rest :: [CaseAlt' Term]
rest)
        = [CaseAlt' Term] -> Bool
noOverlapAlts [CaseAlt' Term]
rest Bool -> Bool -> Bool
&& SC -> Bool
noOverlap SC
sc
    noOverlapAlts (DefaultCase _ : _) = Bool
False
    noOverlapAlts _ = Bool
True