{-# LANGUAGE NondecreasingIndentation #-}

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

module Agda.TypeChecking.Rewriting.NonLinPattern where

import Control.Monad        ( (>=>), forM )
import Control.Monad.Reader ( asks )

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.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Primitive.Cubical

import Agda.Utils.Either
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, HasBuiltins 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
i : Elims
es) -> do
      ~(PathType Sort
s QName
q Arg Term
l Arg Term
b Arg Term
u Arg Term
v) <- Type -> TCMT IO PathView
forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView (Type -> TCMT IO PathView) -> TCMT IO Type -> TCMT IO PathView
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' = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
b Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` [ Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
i ]
      let hd' :: Term
hd' = Term
hd Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [Term -> Term -> Term -> Elim' Term
forall a. a -> a -> a -> Elim' a
IApply Term
x Term
y Term
i]
      Type
interval <- TCMT IO Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
      NLPat
p   <- Relevance -> Int -> Type -> Term -> TCM NLPat
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k Type
interval Term
i
      [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
$ NLPat -> NLPat -> NLPat -> Elim' NLPat
forall a. a -> a -> a -> Elim' a
IApply (Term -> NLPat
PTerm Term
x) (Term -> NLPat
PTerm Term
y) NLPat
p Elim' NLPat -> [Elim' NLPat] -> [Elim' NLPat]
forall a. a -> [a] -> [a]
: [Elim' NLPat]
ps
    (Proj ProjOrigin
o QName
f : Elims
es) -> do
      ~(Just (El Sort
_ (Pi Dom Type
a Abs Type
b))) <- QName -> Type -> TCMT IO (Maybe Type)
forall (m :: * -> *). PureTCM 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 -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
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 -> TCMT IO NLPSort
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k () (Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
a)
            TCMT IO (NLPat -> NLPType) -> TCM NLPat -> TCM NLPType
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Relevance -> Int -> Type -> Term -> TCM NLPat
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k (Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
a) (Type -> Term
forall t a. Type'' t a -> a
unEl Type
a)

instance PatternFrom () Sort NLPSort where
  patternFrom :: Relevance -> Int -> () -> Sort -> TCMT IO NLPSort
patternFrom Relevance
r Int
k ()
_ Sort
s = do
    Sort
s <- Sort -> TCMT IO Sort
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Sort
s
    case Sort
s of
      Type Level' Term
l   -> NLPat -> NLPSort
PType (NLPat -> NLPSort) -> TCM NLPat -> TCMT IO NLPSort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> () -> Level' Term -> TCM 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) -> TCM NLPat -> TCMT IO NLPSort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> () -> Level' Term -> TCM NLPat
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k () Level' Term
l
      Inf IsFibrant
f Integer
n  -> NLPSort -> TCMT IO NLPSort
forall (m :: * -> *) a. Monad m => a -> m a
return (NLPSort -> TCMT IO NLPSort) -> NLPSort -> TCMT IO NLPSort
forall a b. (a -> b) -> a -> b
$ IsFibrant -> Integer -> NLPSort
PInf IsFibrant
f Integer
n
      SSet Level' Term
l   -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
      Sort
SizeUniv -> NLPSort -> TCMT IO NLPSort
forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PSizeUniv
      Sort
LockUniv -> NLPSort -> TCMT IO NLPSort
forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PLockUniv
      PiSort Dom' Term Term
_ Sort
_ Abs Sort
_ -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
      FunSort Sort
_ Sort
_ -> TCMT IO NLPSort
forall a. HasCallStack => a
__IMPOSSIBLE__
      UnivSort Sort
_ -> 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 -> TCM 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 -> TCM 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 -> TCM 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 <- (Blocker -> Bool) -> Either Blocker Bool -> Bool
forall a b. (a -> b) -> Either a b -> b
fromRight Blocker -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__ (Either Blocker Bool -> Bool)
-> (BlockT (TCMT IO) Bool -> TCMT IO (Either Blocker Bool))
-> BlockT (TCMT IO) Bool
-> TCMT IO Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> BlockT (TCMT IO) Bool -> TCMT IO (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (BlockT (TCMT IO) Bool -> TCMT IO Bool)
-> BlockT (TCMT IO) Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Type -> BlockT (TCMT IO) Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 :: TCM NLPat
done = NLPat -> TCM NLPat
forall (m :: * -> *) a. Monad m => a -> m a
return (NLPat -> TCM NLPat) -> NLPat -> TCM 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 a. Subst 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 -> TCM NLPat -> TCM NLPat
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom Type
a (Relevance -> Int -> Type -> Term -> TCM 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 a. Subst a => Abs a -> a
absBody Abs Type
b) Term
body)
        NLPat -> TCM NLPat
forall (m :: * -> *) a. Monad m => a -> m a
return (NLPat -> TCM NLPat) -> NLPat -> TCM 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] -> TCM 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' (SubstArg [Type]) -> [Type] -> [Type]
forall a. Subst a => Substitution' (SubstArg a) -> 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. TermSubst 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 -> TCMT IO (Maybe Int)
forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
isEtaVar (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v) Type
t TCMT IO (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 -> TCM NLPat
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [Arg Int] -> NLPat
PVar Int
i [Arg Int]
bvs) else TCM NLPat
done
             Maybe [Arg Int]
_ -> TCM NLPat
done
       | Bool
otherwise -> TCM 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))
-> TCM NLPat
-> (((QName, Type, Args), Type) -> TCM NLPat)
-> TCM 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 :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t) TCM NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__ ((((QName, Type, Args), Type) -> TCM NLPat) -> TCM NLPat)
-> (((QName, Type, Args), Type) -> TCM NLPat) -> TCM 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] -> TCM 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) -> TCM NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , Lit{})   -> TCM NLPat
done
      (Term
_ , Def QName
f Elims
es) | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r -> TCM 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 -> TCM NLPat
done
          [Elim' Term
x , Elim' Term
y] | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
lmax -> TCM 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] -> TCM 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 -> TCM NLPat
done
      (Term
_ , Con ConHead
c ConInfo
ci Elims
vs) ->
        TCMT IO (Maybe ((QName, Type, Args), Type))
-> TCM NLPat
-> (((QName, Type, Args), Type) -> TCM NLPat)
-> TCM 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 :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t) TCM NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__ ((((QName, Type, Args), Type) -> TCM NLPat) -> TCM NLPat)
-> (((QName, Type, Args), Type) -> TCM NLPat) -> TCM 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] -> TCM 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 -> TCM 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 a. Subst a => Abs a -> a
absBody Abs Type
b)
        NLPat -> TCM NLPat
forall (m :: * -> *) a. Monad m => a -> m a
return (NLPat -> TCM NLPat) -> NLPat -> TCM 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
s)     -> NLPSort -> NLPat
PSort (NLPSort -> NLPat) -> TCMT IO NLPSort -> TCM NLPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Relevance -> Int -> () -> Sort -> TCMT IO NLPSort
forall t a b.
PatternFrom t a b =>
Relevance -> Int -> t -> a -> TCM b
patternFrom Relevance
r Int
k () Sort
s
      (Term
_ , Level Level' Term
l)    -> TCM NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , DontCare{}) -> TCM NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , MetaV{})    -> TCM NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , Dummy String
s Elims
_)  -> String -> TCM 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 :: PureTCM m => p -> m a

  default nlPatToTerm ::
    ( NLPatToTerm p' a', Traversable f, p ~ f p', a ~ f a'
    , PureTCM 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, PureTCM 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, PureTCM 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, PureTCM 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, PureTCM 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, PureTCM 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, PureTCM 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, PureTCM m) => p -> m a
nlPatToTerm Abs NLPType
b
    PSort NLPSort
s        -> Sort -> Term
Sort  (Sort -> Term) -> m Sort -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NLPSort -> m Sort
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM 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, PureTCM 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, PureTCM 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 :: * -> *). PureTCM m => Term -> m (Level' Term)
levelView

instance NLPatToTerm NLPType Type where
  nlPatToTerm :: NLPType -> m Type
nlPatToTerm (NLPType NLPSort
s NLPat
a) = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Sort -> Term -> Type) -> m Sort -> m (Term -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NLPSort -> m Sort
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM 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, PureTCM m) => p -> m a
nlPatToTerm NLPat
a

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

-- | 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
    PInf IsFibrant
f Integer
n  -> IntSet
forall a. Null a => a
empty
    NLPSort
PSizeUniv -> IntSet
forall a. Null a => a
empty
    NLPSort
PLockUniv -> 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
    PInf IsFibrant
f Integer
n  -> [QName]
forall a. Null a => a
empty
    NLPSort
PSizeUniv -> [QName]
forall a. Null a => a
empty
    NLPSort
PLockUniv -> [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 ((FreeEnv' a IgnoreSorts c -> Bool)
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((IgnoreSorts
IgnoreNot IgnoreSorts -> IgnoreSorts -> Bool
forall a. Eq a => a -> a -> Bool
==) (IgnoreSorts -> Bool)
-> (FreeEnv' a IgnoreSorts c -> IgnoreSorts)
-> FreeEnv' a IgnoreSorts c
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
    PInf IsFibrant
f Integer
n  -> FreeM a c
forall a. Monoid a => a
mempty
    NLPSort
PSizeUniv -> FreeM a c
forall a. Monoid a => a
mempty
    NLPSort
PLockUniv -> FreeM a c
forall a. Monoid a => a
mempty