{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE TypeFamilies #-}

{- | Various utility functions dealing with the non-linear, higher-order
     patterns used for rewrite rules.
-}

module Agda.TypeChecking.Rewriting.NonLinPattern where

import Control.Monad.Reader

import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Defs

import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Lazy
import Agda.TypeChecking.Irrelevance (workOnTypes, isPropM)
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

import Agda.Utils.Functor
import Agda.Utils.Impossible
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Singleton
import Agda.Utils.Size

-- | Turn a term into a non-linear pattern, treating the
--   free variables as pattern variables.
--   The first argument indicates the relevance we are working under: if this
--   is Irrelevant, then we construct a pattern that never fails to match.
--   The second argument is the number of bound variables (from pattern lambdas).
--   The third argument is the type of the term.

class PatternFrom t a b where
  patternFrom :: Relevance -> Int -> t -> a -> TCM b

instance (PatternFrom t a b) => PatternFrom (Dom t) (Arg a) (Arg b) where
  patternFrom :: Relevance -> Int -> Dom t -> Arg a -> TCM (Arg b)
patternFrom Relevance
r Int
k Dom t
t Arg a
u = let r' :: Relevance
r' = Relevance
r Relevance -> Relevance -> Relevance
`composeRelevance` Arg a -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Arg a
u
                        in  (a -> TCMT IO b) -> Arg a -> TCM (Arg b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Relevance -> Int -> t -> a -> TCMT IO b
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r' Int
k (t -> a -> TCMT IO b) -> t -> a -> TCMT IO b
forall a b. (a -> b) -> a -> b
$ Dom t -> t
forall t e. Dom' t e -> e
unDom Dom t
t) Arg a
u

instance PatternFrom (Type, Term) Elims [Elim' NLPat] where
  patternFrom :: Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
patternFrom Relevance
r Int
k (Type
t,Term
hd) = \case
    [] -> [Elim' NLPat] -> TCM [Elim' NLPat]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    (Apply Arg Term
u : Elims
es) -> do
      ~(Pi Dom Type
a Abs Type
b) <- Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> TCMT IO Type -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
      Arg NLPat
p   <- Relevance -> Int -> Dom Type -> Arg Term -> TCM (Arg NLPat)
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k Dom Type
a Arg Term
u
      Type
t'  <- Type
t Type -> Arg Term -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m) =>
Type -> a -> m Type
`piApplyM` Arg Term
u
      let hd' :: Term
hd' = Term
hd Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ Arg Term
u ]
      [Elim' NLPat]
ps  <- Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k (Type
t',Term
hd') Elims
es
      [Elim' NLPat] -> TCM [Elim' NLPat]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Elim' NLPat] -> TCM [Elim' NLPat])
-> [Elim' NLPat] -> TCM [Elim' NLPat]
forall a b. (a -> b) -> a -> b
$ Arg NLPat -> Elim' NLPat
forall a. Arg a -> Elim' a
Apply Arg NLPat
p Elim' NLPat -> [Elim' NLPat] -> [Elim' NLPat]
forall a. a -> [a] -> [a]
: [Elim' NLPat]
ps
    (IApply Term
x Term
y Term
u : Elims
es) -> TypeError -> TCM [Elim' NLPat]
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM [Elim' NLPat]) -> TypeError -> TCM [Elim' NLPat]
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
      String
"Rewrite rules with cubical are not yet supported"
    (Proj ProjOrigin
o QName
f : Elims
es) -> do
      ~(Just (El Sort' Term
_ (Pi Dom Type
a Abs Type
b))) <- QName -> Type -> TCMT IO (Maybe Type)
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
QName -> Type -> m (Maybe Type)
getDefType QName
f (Type -> TCMT IO (Maybe Type))
-> TCMT IO Type -> TCMT IO (Maybe Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
      let t' :: Type
t' = Abs Type
b Abs Type -> Term -> Type
forall t a. Subst t a => Abs a -> t -> a
`absApp` Term
hd
      Term
hd' <- ProjOrigin -> QName -> Arg Term -> TCMT IO Term
forall (m :: * -> *).
HasConstInfo m =>
ProjOrigin -> QName -> Arg Term -> m Term
applyDef ProjOrigin
o QName
f (Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
a Arg Type -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Term
hd)
      [Elim' NLPat]
ps  <- Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k (Type
t',Term
hd') Elims
es
      [Elim' NLPat] -> TCM [Elim' NLPat]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Elim' NLPat] -> TCM [Elim' NLPat])
-> [Elim' NLPat] -> TCM [Elim' NLPat]
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> QName -> Elim' NLPat
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
f Elim' NLPat -> [Elim' NLPat] -> [Elim' NLPat]
forall a. a -> [a] -> [a]
: [Elim' NLPat]
ps

instance (PatternFrom t a b) => PatternFrom t (Dom a) (Dom b) where
  patternFrom :: Relevance -> Int -> t -> Dom a -> TCM (Dom b)
patternFrom Relevance
r Int
k t
t = (a -> TCMT IO b) -> Dom a -> TCM (Dom b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> TCMT IO b) -> Dom a -> TCM (Dom b))
-> (a -> TCMT IO b) -> Dom a -> TCM (Dom b)
forall a b. (a -> b) -> a -> b
$ Relevance -> Int -> t -> a -> TCMT IO b
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k t
t

instance PatternFrom () Type NLPType where
  patternFrom :: Relevance -> Int -> () -> Type -> TCM NLPType
patternFrom Relevance
r Int
k ()
_ Type
a = TCM NLPType -> TCM NLPType
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM NLPType -> TCM NLPType) -> TCM NLPType -> TCM NLPType
forall a b. (a -> b) -> a -> b
$
    NLPSort -> NLPat -> NLPType
NLPType (NLPSort -> NLPat -> NLPType)
-> TCMT IO NLPSort -> TCMT IO (NLPat -> NLPType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> () -> Sort' Term -> TCMT IO NLPSort
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k () (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
a)
            TCMT IO (NLPat -> NLPType) -> TCMT IO NLPat -> TCM NLPType
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Relevance -> Int -> Type -> Term -> TCMT IO NLPat
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k (Sort' Term -> Type
sort (Sort' Term -> Type) -> Sort' Term -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
a) (Type -> Term
forall t a. Type'' t a -> a
unEl Type
a)

instance PatternFrom () Sort NLPSort where
  patternFrom :: Relevance -> Int -> () -> Sort' Term -> TCMT IO NLPSort
patternFrom Relevance
r Int
k ()
_ Sort' Term
s = do
    Sort' Term
s <- Sort' Term -> TCMT IO (Sort' Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort' Term
s
    case Sort' Term
s of
      Type Level' Term
l   -> NLPat -> NLPSort
PType (NLPat -> NLPSort) -> TCMT IO NLPat -> TCMT IO NLPSort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> () -> Level' Term -> TCMT IO NLPat
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k () Level' Term
l
      Prop Level' Term
l   -> NLPat -> NLPSort
PProp (NLPat -> NLPSort) -> TCMT IO NLPat -> TCMT IO NLPSort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> () -> Level' Term -> TCMT IO NLPat
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k () Level' Term
l
      Sort' Term
Inf      -> NLPSort -> TCMT IO NLPSort
forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PInf
      Sort' Term
SizeUniv -> NLPSort -> TCMT IO NLPSort
forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PSizeUniv
      PiSort Dom Type
_ Abs (Sort' Term)
_ -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
      FunSort Sort' Term
_ Sort' Term
_ -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
      UnivSort Sort' Term
_ -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
      MetaS{}  -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
      DefS{}   -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
      DummyS String
s -> do
        String -> Int -> [String] -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
reportS String
"impossible" Int
10
          [ String
"patternFrom: hit dummy sort with content:"
          , String
s
          ]
        TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__

instance PatternFrom () Level NLPat where
  patternFrom :: Relevance -> Int -> () -> Level' Term -> TCMT IO NLPat
patternFrom Relevance
r Int
k ()
_ Level' Term
l = do
    Type
t <- TCMT IO Type
forall (m :: * -> *). HasBuiltins m => m Type
levelType
    Term
v <- Level' Term -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Level' Term -> m Term
reallyUnLevelView Level' Term
l
    Relevance -> Int -> Type -> Term -> TCMT IO NLPat
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k Type
t Term
v

instance PatternFrom Type Term NLPat where
  patternFrom :: Relevance -> Int -> Type -> Term -> TCMT IO NLPat
patternFrom Relevance
r0 Int
k Type
t Term
v = do
    Type
t <- Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
    Maybe (QName, Args)
etaRecord <- Type -> TCMT IO (Maybe (QName, Args))
forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, Args))
isEtaRecordType Type
t
    Bool
prop <- Type -> TCMT IO Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, MonadReduce m, MonadDebug m) =>
a -> m Bool
isPropM Type
t
    let r :: Relevance
r = if Bool
prop then Relevance
Irrelevant else Relevance
r0
    Term
v <- Term -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
    String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"rewriting.build" Int
60 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
      [ TCM Doc
"building a pattern from term v = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
      , TCM Doc
" of type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
      ]
    let done :: TCMT IO NLPat
done = NLPat -> TCMT IO NLPat
forall (m :: * -> *) a. Monad m => a -> m a
return (NLPat -> TCMT IO NLPat) -> NLPat -> TCMT IO NLPat
forall a b. (a -> b) -> a -> b
$ Term -> NLPat
PTerm Term
v
    case (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t , Term -> Term
stripDontCare Term
v) of
      (Pi Dom Type
a Abs Type
b , Term
_) -> do
        let body :: Term
body = Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise Int
1 Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
        NLPat
p <- Dom Type -> TCMT IO NLPat -> TCMT IO NLPat
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom Type
a (Relevance -> Int -> Type -> Term -> TCMT IO NLPat
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b) Term
body)
        NLPat -> TCMT IO NLPat
forall (m :: * -> *) a. Monad m => a -> m a
return (NLPat -> TCMT IO NLPat) -> NLPat -> TCMT IO NLPat
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs NLPat -> NLPat
PLam (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
a) (Abs NLPat -> NLPat) -> Abs NLPat -> NLPat
forall a b. (a -> b) -> a -> b
$ String -> NLPat -> Abs NLPat
forall a. String -> a -> Abs a
Abs (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) NLPat
p
      (Term
_ , Var Int
i Elims
es)
       | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k     -> do
           Type
t <- Int -> TCMT IO Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
           Int -> [Elim' NLPat] -> NLPat
PBoundVar Int
i ([Elim' NLPat] -> NLPat) -> TCM [Elim' NLPat] -> TCMT IO NLPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k (Type
t , Int -> Term
var Int
i) Elims
es
       -- The arguments of `var i` should be distinct bound variables
       -- in order to build a Miller pattern
       | Just Args
vs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
           TelV Tele (Dom Type)
tel Type
_ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type -> TCMT IO (TelV Type))
-> TCMT IO Type -> TCMT IO (TelV Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> TCMT IO Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
           Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Args -> Int
forall a. Sized a => a -> Int
size Args
vs) TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
           let ts :: [Type]
ts = Substitution' Term -> [Type] -> [Type]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst ([Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ [Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg Args
vs) ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Dom Type -> Type) -> [Dom Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Dom Type -> Type
forall t e. Dom' t e -> e
unDom ([Dom Type] -> [Type]) -> [Dom Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom Type]
forall a. Subst Term a => Tele (Dom a) -> [Dom a]
flattenTel Tele (Dom Type)
tel
           [Maybe (Arg Int)]
mbvs <- [(Type, Arg Term)]
-> ((Type, Arg Term) -> TCMT IO (Maybe (Arg Int)))
-> TCMT IO [Maybe (Arg Int)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Type] -> Args -> [(Type, Arg Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
ts Args
vs) (((Type, Arg Term) -> TCMT IO (Maybe (Arg Int)))
 -> TCMT IO [Maybe (Arg Int)])
-> ((Type, Arg Term) -> TCMT IO (Maybe (Arg Int)))
-> TCMT IO [Maybe (Arg Int)]
forall a b. (a -> b) -> a -> b
$ \(Type
t , Arg Term
v) -> do
             Term -> Type -> TCM (Maybe Int)
isEtaVar (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v) Type
t TCM (Maybe Int)
-> (Maybe Int -> TCMT IO (Maybe (Arg Int)))
-> TCMT IO (Maybe (Arg Int))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
               Just Int
j | Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k -> Maybe (Arg Int) -> TCMT IO (Maybe (Arg Int))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Arg Int) -> TCMT IO (Maybe (Arg Int)))
-> Maybe (Arg Int) -> TCMT IO (Maybe (Arg Int))
forall a b. (a -> b) -> a -> b
$ Arg Int -> Maybe (Arg Int)
forall a. a -> Maybe a
Just (Arg Int -> Maybe (Arg Int)) -> Arg Int -> Maybe (Arg Int)
forall a b. (a -> b) -> a -> b
$ Arg Term
v Arg Term -> Int -> Arg Int
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int
j
               Maybe Int
_              -> Maybe (Arg Int) -> TCMT IO (Maybe (Arg Int))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Arg Int)
forall a. Maybe a
Nothing
           case [Maybe (Arg Int)] -> Maybe [Arg Int]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Maybe (Arg Int)]
mbvs of
             Just [Arg Int]
bvs | [Arg Int] -> Bool
forall a. Ord a => [a] -> Bool
fastDistinct [Arg Int]
bvs -> do
               let allBoundVars :: IntSet
allBoundVars = [Int] -> IntSet
IntSet.fromList (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
k)
                   ok :: Bool
ok = Bool -> Bool
not (Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r) Bool -> Bool -> Bool
||
                        [Int] -> IntSet
IntSet.fromList ((Arg Int -> Int) -> [Arg Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Arg Int -> Int
forall e. Arg e -> e
unArg [Arg Int]
bvs) IntSet -> IntSet -> Bool
forall a. Eq a => a -> a -> Bool
== IntSet
allBoundVars
               if Bool
ok then NLPat -> TCMT IO NLPat
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [Arg Int] -> NLPat
PVar Int
i [Arg Int]
bvs) else TCMT IO NLPat
done
             Maybe [Arg Int]
_ -> TCMT IO NLPat
done
       | Bool
otherwise -> TCMT IO NLPat
done
      (Term
_ , Term
_ ) | Just (QName
d, Args
pars) <- Maybe (QName, Args)
etaRecord -> do
        Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
        (Tele (Dom Type)
tel, ConHead
c, ConInfo
ci, Args
vs) <- QName
-> Args
-> Defn
-> Term
-> TCMT IO (Tele (Dom Type), ConHead, ConInfo, Args)
forall (m :: * -> *).
HasConstInfo m =>
QName
-> Args
-> Defn
-> Term
-> m (Tele (Dom Type), ConHead, ConInfo, Args)
etaExpandRecord_ QName
d Args
pars Defn
def Term
v
        TCMT IO (Maybe ((QName, Type, Args), Type))
-> TCMT IO NLPat
-> (((QName, Type, Args), Type) -> TCMT IO NLPat)
-> TCMT IO NLPat
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ConHead -> Type -> TCMT IO (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t) TCMT IO NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__ ((((QName, Type, Args), Type) -> TCMT IO NLPat) -> TCMT IO NLPat)
-> (((QName, Type, Args), Type) -> TCMT IO NLPat) -> TCMT IO NLPat
forall a b. (a -> b) -> a -> b
$ \ ((QName, Type, Args)
_ , Type
ct) -> do
        QName -> [Elim' NLPat] -> NLPat
PDef (ConHead -> QName
conName ConHead
c) ([Elim' NLPat] -> NLPat) -> TCM [Elim' NLPat] -> TCMT IO NLPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k (Type
ct , ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci []) ((Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
vs)
      (Term
_ , Lam ArgInfo
i Abs Term
t) -> TCMT IO NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , Lit{})   -> TCMT IO NLPat
done
      (Term
_ , Def QName
f Elims
es) | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r -> TCMT IO NLPat
done
      (Term
_ , Def QName
f Elims
es) -> do
        Def QName
lsuc [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc
        Def QName
lmax [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax
        case Elims
es of
          [Elim' Term
x]     | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
lsuc -> TCMT IO NLPat
done
          [Elim' Term
x , Elim' Term
y] | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
lmax -> TCMT IO NLPat
done
          Elims
_                   -> do
            Type
ft <- Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
            QName -> [Elim' NLPat] -> NLPat
PDef QName
f ([Elim' NLPat] -> NLPat) -> TCM [Elim' NLPat] -> TCMT IO NLPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k (Type
ft , QName -> Elims -> Term
Def QName
f []) Elims
es
      (Term
_ , Con ConHead
c ConInfo
ci Elims
vs) | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r -> TCMT IO NLPat
done
      (Term
_ , Con ConHead
c ConInfo
ci Elims
vs) ->
        TCMT IO (Maybe ((QName, Type, Args), Type))
-> TCMT IO NLPat
-> (((QName, Type, Args), Type) -> TCMT IO NLPat)
-> TCMT IO NLPat
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ConHead -> Type -> TCMT IO (Maybe ((QName, Type, Args), Type))
forall (m :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug m) =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t) TCMT IO NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__ ((((QName, Type, Args), Type) -> TCMT IO NLPat) -> TCMT IO NLPat)
-> (((QName, Type, Args), Type) -> TCMT IO NLPat) -> TCMT IO NLPat
forall a b. (a -> b) -> a -> b
$ \ ((QName, Type, Args)
_ , Type
ct) -> do
        QName -> [Elim' NLPat] -> NLPat
PDef (ConHead -> QName
conName ConHead
c) ([Elim' NLPat] -> NLPat) -> TCM [Elim' NLPat] -> TCMT IO NLPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k (Type
ct , ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci []) Elims
vs
      (Term
_ , Pi Dom Type
a Abs Type
b) | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r -> TCMT IO NLPat
done
      (Term
_ , Pi Dom Type
a Abs Type
b) -> do
        Dom NLPType
pa <- Relevance -> Int -> () -> Dom Type -> TCM (Dom NLPType)
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k () Dom Type
a
        NLPType
pb <- Dom Type -> TCM NLPType -> TCM NLPType
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom Type
a (Relevance -> Int -> () -> Type -> TCM NLPType
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) () (Type -> TCM NLPType) -> Type -> TCM NLPType
forall a b. (a -> b) -> a -> b
$ Abs Type -> Type
forall t a. Subst t a => Abs a -> a
absBody Abs Type
b)
        NLPat -> TCMT IO NLPat
forall (m :: * -> *) a. Monad m => a -> m a
return (NLPat -> TCMT IO NLPat) -> NLPat -> TCMT IO NLPat
forall a b. (a -> b) -> a -> b
$ Dom NLPType -> Abs NLPType -> NLPat
PPi Dom NLPType
pa (String -> NLPType -> Abs NLPType
forall a. String -> a -> Abs a
Abs (Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b) NLPType
pb)
      (Term
_ , Sort Sort' Term
s)     -> NLPSort -> NLPat
PSort (NLPSort -> NLPat) -> TCMT IO NLPSort -> TCMT IO NLPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> () -> Sort' Term -> TCMT IO NLPSort
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k () Sort' Term
s
      (Term
_ , Level Level' Term
l)    -> TCMT IO NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , DontCare{}) -> TCMT IO NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , MetaV{})    -> TCMT IO NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , Dummy String
s Elims
_)  -> String -> TCMT IO NLPat
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
s

-- | Convert from a non-linear pattern to a term.

class NLPatToTerm p a where
  nlPatToTerm
    :: (MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug m)
    => p -> m a

  default nlPatToTerm ::
    ( NLPatToTerm p' a', Traversable f, p ~ f p', a ~ f a'
    , MonadReduce m, HasBuiltins m, HasConstInfo m, MonadDebug m
    ) => p -> m a
  nlPatToTerm = (p' -> m a') -> f p' -> m (f a')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse p' -> m a'
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm

instance NLPatToTerm p a => NLPatToTerm [p] [a] where
instance NLPatToTerm p a => NLPatToTerm (Arg p) (Arg a) where
instance NLPatToTerm p a => NLPatToTerm (Dom p) (Dom a) where
instance NLPatToTerm p a => NLPatToTerm (Elim' p) (Elim' a) where
instance NLPatToTerm p a => NLPatToTerm (Abs p) (Abs a) where

instance NLPatToTerm Nat Term where
  nlPatToTerm :: Int -> m Term
nlPatToTerm = Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> (Int -> Term) -> Int -> m Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var

instance NLPatToTerm NLPat Term where
  nlPatToTerm :: NLPat -> m Term
nlPatToTerm = \case
    PVar Int
i [Arg Int]
xs      -> Int -> Elims -> Term
Var Int
i (Elims -> Term) -> (Args -> Elims) -> Args -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Term) -> m Args -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Int] -> m Args
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm [Arg Int]
xs
    PTerm Term
u        -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
    PDef QName
f [Elim' NLPat]
es      -> (Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f) m Defn -> (Defn -> m Term) -> m Term
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Constructor{ conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c } -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ConOSystem (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Elim' NLPat] -> m Elims
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm [Elim' NLPat]
es
      Defn
_                            -> QName -> Elims -> Term
Def QName
f (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Elim' NLPat] -> m Elims
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm [Elim' NLPat]
es
    PLam ArgInfo
i Abs NLPat
u       -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
i (Abs Term -> Term) -> m (Abs Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs NLPat -> m (Abs Term)
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm Abs NLPat
u
    PPi Dom NLPType
a Abs NLPType
b        -> Dom Type -> Abs Type -> Term
Pi    (Dom Type -> Abs Type -> Term)
-> m (Dom Type) -> m (Abs Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom NLPType -> m (Dom Type)
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm Dom NLPType
a m (Abs Type -> Term) -> m (Abs Type) -> m Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs NLPType -> m (Abs Type)
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm Abs NLPType
b
    PSort NLPSort
s        -> Sort' Term -> Term
Sort  (Sort' Term -> Term) -> m (Sort' Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NLPSort -> m (Sort' Term)
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm NLPSort
s
    PBoundVar Int
i [Elim' NLPat]
es -> Int -> Elims -> Term
Var Int
i (Elims -> Term) -> m Elims -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Elim' NLPat] -> m Elims
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm [Elim' NLPat]
es

instance NLPatToTerm NLPat Level where
  nlPatToTerm :: NLPat -> m (Level' Term)
nlPatToTerm = NLPat -> m Term
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm (NLPat -> m Term)
-> (Term -> m (Level' Term)) -> NLPat -> m (Level' Term)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term -> m (Level' Term)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m, MonadDebug m) =>
Term -> m (Level' Term)
levelView

instance NLPatToTerm NLPType Type where
  nlPatToTerm :: NLPType -> m Type
nlPatToTerm (NLPType NLPSort
s NLPat
a) = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort' Term -> Term -> Type) -> m (Sort' Term) -> m (Term -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NLPSort -> m (Sort' Term)
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm NLPSort
s m (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NLPat -> m Term
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm NLPat
a

instance NLPatToTerm NLPSort Sort where
  nlPatToTerm :: NLPSort -> m (Sort' Term)
nlPatToTerm (PType NLPat
l) = Level' Term -> Sort' Term
forall t. Level' t -> Sort' t
Type (Level' Term -> Sort' Term) -> m (Level' Term) -> m (Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NLPat -> m (Level' Term)
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm NLPat
l
  nlPatToTerm (PProp NLPat
l) = Level' Term -> Sort' Term
forall t. Level' t -> Sort' t
Prop (Level' Term -> Sort' Term) -> m (Level' Term) -> m (Sort' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NLPat -> m (Level' Term)
forall p a (m :: * -> *).
(NLPatToTerm p a, MonadReduce m, HasBuiltins m, HasConstInfo m,
 MonadDebug m) =>
p -> m a
nlPatToTerm NLPat
l
  nlPatToTerm NLPSort
PInf      = Sort' Term -> m (Sort' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
forall t. Sort' t
Inf
  nlPatToTerm NLPSort
PSizeUniv = Sort' Term -> m (Sort' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
forall t. Sort' t
SizeUniv

-- | Gather the set of pattern variables of a non-linear pattern
class NLPatVars a where
  nlPatVarsUnder :: Int -> a -> IntSet

  nlPatVars :: a -> IntSet
  nlPatVars = Int -> a -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
0

instance {-# OVERLAPPABLE #-} (Foldable f, NLPatVars a) => NLPatVars (f a) where
  nlPatVarsUnder :: Int -> f a -> IntSet
nlPatVarsUnder Int
k = (a -> IntSet) -> f a -> IntSet
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((a -> IntSet) -> f a -> IntSet) -> (a -> IntSet) -> f a -> IntSet
forall a b. (a -> b) -> a -> b
$ Int -> a -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k

instance NLPatVars NLPType where
  nlPatVarsUnder :: Int -> NLPType -> IntSet
nlPatVarsUnder Int
k (NLPType NLPSort
l NLPat
a) = Int -> (NLPSort, NLPat) -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k (NLPSort
l, NLPat
a)

instance NLPatVars NLPSort where
  nlPatVarsUnder :: Int -> NLPSort -> IntSet
nlPatVarsUnder Int
k = \case
    PType NLPat
l   -> Int -> NLPat -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k NLPat
l
    PProp NLPat
l   -> Int -> NLPat -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k NLPat
l
    NLPSort
PInf      -> IntSet
forall a. Null a => a
empty
    NLPSort
PSizeUniv -> IntSet
forall a. Null a => a
empty

instance NLPatVars NLPat where
  nlPatVarsUnder :: Int -> NLPat -> IntSet
nlPatVarsUnder Int
k = \case
      PVar Int
i [Arg Int]
_  -> Int -> IntSet
forall el coll. Singleton el coll => el -> coll
singleton (Int -> IntSet) -> Int -> IntSet
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k
      PDef QName
_ [Elim' NLPat]
es -> Int -> [Elim' NLPat] -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k [Elim' NLPat]
es
      PLam ArgInfo
_ Abs NLPat
p  -> Int -> Abs NLPat -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k Abs NLPat
p
      PPi Dom NLPType
a Abs NLPType
b   -> Int -> (Dom NLPType, Abs NLPType) -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k (Dom NLPType
a, Abs NLPType
b)
      PSort NLPSort
s   -> Int -> NLPSort -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k NLPSort
s
      PBoundVar Int
_ [Elim' NLPat]
es -> Int -> [Elim' NLPat] -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k [Elim' NLPat]
es
      PTerm{}   -> IntSet
forall a. Null a => a
empty

instance (NLPatVars a, NLPatVars b) => NLPatVars (a,b) where
  nlPatVarsUnder :: Int -> (a, b) -> IntSet
nlPatVarsUnder Int
k (a
a,b
b) = Int -> a -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k a
a IntSet -> IntSet -> IntSet
forall a. Monoid a => a -> a -> a
`mappend` Int -> b -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k b
b

instance NLPatVars a => NLPatVars (Abs a) where
  nlPatVarsUnder :: Int -> Abs a -> IntSet
nlPatVarsUnder Int
k = \case
    Abs   String
_ a
v -> Int -> a -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) a
v
    NoAbs String
_ a
v -> Int -> a -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k a
v

-- | Get all symbols that a non-linear pattern matches against
class GetMatchables a where
  getMatchables :: a -> [QName]

  default getMatchables :: (Foldable f, GetMatchables a', a ~ f a') => a -> [QName]
  getMatchables = (a' -> [QName]) -> f a' -> [QName]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a' -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables

instance GetMatchables a => GetMatchables [a] where
instance GetMatchables a => GetMatchables (Arg a) where
instance GetMatchables a => GetMatchables (Dom a) where
instance GetMatchables a => GetMatchables (Elim' a) where
instance GetMatchables a => GetMatchables (Abs a) where

instance (GetMatchables a, GetMatchables b) => GetMatchables (a,b) where
  getMatchables :: (a, b) -> [QName]
getMatchables (a
x,b
y) = a -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables a
x [QName] -> [QName] -> [QName]
forall a. [a] -> [a] -> [a]
++ b -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables b
y

instance GetMatchables NLPat where
  getMatchables :: NLPat -> [QName]
getMatchables NLPat
p =
    case NLPat
p of
      PVar Int
_ [Arg Int]
_       -> [QName]
forall a. Null a => a
empty
      PDef QName
f [Elim' NLPat]
_       -> QName -> [QName]
forall el coll. Singleton el coll => el -> coll
singleton QName
f
      PLam ArgInfo
_ Abs NLPat
x       -> Abs NLPat -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables Abs NLPat
x
      PPi Dom NLPType
a Abs NLPType
b        -> (Dom NLPType, Abs NLPType) -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables (Dom NLPType
a,Abs NLPType
b)
      PSort NLPSort
s        -> NLPSort -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables NLPSort
s
      PBoundVar Int
i [Elim' NLPat]
es -> [Elim' NLPat] -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables [Elim' NLPat]
es
      PTerm Term
u        -> Term -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables Term
u

instance GetMatchables NLPType where
  getMatchables :: NLPType -> [QName]
getMatchables = NLPat -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables (NLPat -> [QName]) -> (NLPType -> NLPat) -> NLPType -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NLPType -> NLPat
nlpTypeUnEl

instance GetMatchables NLPSort where
  getMatchables :: NLPSort -> [QName]
getMatchables = \case
    PType NLPat
l   -> NLPat -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables NLPat
l
    PProp NLPat
l   -> NLPat -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables NLPat
l
    NLPSort
PInf      -> [QName]
forall a. Null a => a
empty
    NLPSort
PSizeUniv -> [QName]
forall a. Null a => a
empty

instance GetMatchables Term where
  getMatchables :: Term -> [QName]
getMatchables = (MetaId -> Maybe Term) -> (QName -> [QName]) -> Term -> [QName]
forall a b.
(GetDefs a, Monoid b) =>
(MetaId -> Maybe Term) -> (QName -> b) -> a -> b
getDefs' MetaId -> Maybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ QName -> [QName]
forall el coll. Singleton el coll => el -> coll
singleton

instance GetMatchables RewriteRule where
  getMatchables :: RewriteRule -> [QName]
getMatchables = [Elim' NLPat] -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables ([Elim' NLPat] -> [QName])
-> (RewriteRule -> [Elim' NLPat]) -> RewriteRule -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> [Elim' NLPat]
rewPats

-- | Only computes free variables that are not bound (see 'nlPatVars'),
--   i.e., those in a 'PTerm'.

instance Free NLPat where
  freeVars' :: NLPat -> FreeM a c
freeVars' = \case
    PVar Int
_ [Arg Int]
_       -> FreeM a c
forall a. Monoid a => a
mempty
    PDef QName
_ [Elim' NLPat]
es      -> [Elim' NLPat] -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' [Elim' NLPat]
es
    PLam ArgInfo
_ Abs NLPat
u       -> Abs NLPat -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Abs NLPat
u
    PPi Dom NLPType
a Abs NLPType
b        -> (Dom NLPType, Abs NLPType) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (Dom NLPType
a,Abs NLPType
b)
    PSort NLPSort
s        -> NLPSort -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' NLPSort
s
    PBoundVar Int
_ [Elim' NLPat]
es -> [Elim' NLPat] -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' [Elim' NLPat]
es
    PTerm Term
t        -> Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' Term
t

instance Free NLPType where
  freeVars' :: NLPType -> FreeM a c
freeVars' (NLPType NLPSort
s NLPat
a) =
    ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
-> FreeM a c -> FreeM a c -> FreeM a c
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((IgnoreSorts
IgnoreNot IgnoreSorts -> IgnoreSorts -> Bool
forall a. Eq a => a -> a -> Bool
==) (IgnoreSorts -> Bool)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity IgnoreSorts
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FreeEnv' a IgnoreSorts c -> IgnoreSorts)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity IgnoreSorts
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks FreeEnv' a IgnoreSorts c -> IgnoreSorts
forall a c. FreeEnv' a IgnoreSorts c -> IgnoreSorts
feIgnoreSorts)
      {- then -} ((NLPSort, NLPat) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' (NLPSort
s, NLPat
a))
      {- else -} (NLPat -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' NLPat
a)

instance Free NLPSort where
  freeVars' :: NLPSort -> FreeM a c
freeVars' = \case
    PType NLPat
l   -> NLPat -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' NLPat
l
    PProp NLPat
l   -> NLPat -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' NLPat
l
    NLPSort
PInf      -> FreeM a c
forall a. Monoid a => a
mempty
    NLPSort
PSizeUniv -> FreeM a c
forall a. Monoid a => a
mempty