{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

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

module Agda.TypeChecking.Rewriting.NonLinPattern where

import Prelude hiding ( null )

import Control.Monad.Reader ( asks )

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Defs
import Agda.Syntax.Internal.MetaVars ( AllMetas, unblockOnAllMetasIn )

import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Lazy
import Agda.TypeChecking.Irrelevance ( isDefSing )
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.Base

import Agda.Utils.Functor
import Agda.Utils.Impossible
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Singleton
import Agda.Utils.Size
import qualified Agda.Utils.VarSet as VarSet
import Agda.Utils.VarSet (VarSet)
import Data.Foldable (Foldable(fold))

-- | Turn a term into a non-linear pattern, treating the
--   free variables as pattern variables.
--   The first two arguments indicate whether the pattern we are under is
--   definitionally singular. Specifically, the first tracks the definitional
--   singularity of the last |PDef|/|PBoundVar| match, while the second tracks
--   the current definitional singularity.
--   The third argument is the number of bound variables (from pattern lambdas).
--   The fourth argument is the type of the term.

class PatternFrom a b where
  patternFrom :: DefSing -> DefSing -> Int -> TypeOf a -> a -> TCM b

instance (PatternFrom a b) => PatternFrom (Arg a) (Arg b) where
  patternFrom :: DefSing -> DefSing -> Int -> TypeOf (Arg a) -> Arg a -> TCM (Arg b)
patternFrom DefSing
r0 DefSing
r1 Int
k TypeOf (Arg a)
t Arg a
u
    = let r1' :: DefSing
r1' = DefSing
r1 DefSing -> DefSing -> DefSing
`maxDefSing` Relevance -> DefSing
relToDefSing (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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse (DefSing -> DefSing -> Int -> TypeOf a -> a -> TCMT IO b
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1' Int
k (TypeOf a -> a -> TCMT IO b) -> TypeOf a -> a -> TCMT IO b
forall a b. (a -> b) -> a -> b
$ Dom' Term (TypeOf a) -> TypeOf a
forall t e. Dom' t e -> e
unDom TypeOf (Arg a)
Dom' Term (TypeOf a)
t) Arg a
u

instance PatternFrom Elims PElims where
  patternFrom :: DefSing -> DefSing -> Int -> TypeOf Elims -> Elims -> TCM PElims
patternFrom DefSing
r0 DefSing
r1 Int
k (Type
t,Elims -> Term
hd) = \case
    [] -> PElims -> TCM PElims
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    (Apply Arg Term
u : Elims
es) -> do
      (a, b) <- Type -> TCM (Dom Type, Abs Type)
assertPi Type
t
      p   <- patternFrom r0 r1 k a u
      let t'  = Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u)
      let hd' = Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Arg Term
uElim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:)
      ps  <- patternFrom r0 r1 k (t',hd') es
      return $ Apply p : ps
    (IApply Term
x Term
y Term
i : Elims
es) -> do
      (s, q, l, b, u, v) <- Type -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
assertPath Type
t
      let 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' = Elims -> Term
hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Term -> Term -> Elim' Term
forall a. a -> a -> a -> Elim' a
IApply Term
x Term
y Term
iElim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
:)
      interval <- primIntervalType
      p   <- patternFrom r0 r1 k interval i
      ps  <- patternFrom r0 r1 k (t',hd') es
      return $ IApply (PTerm x) (PTerm y) p : ps
    (Proj ProjOrigin
o QName
f : Elims
es) -> do
      (a,b) <- QName -> Type -> TCM (Dom Type, Abs Type)
assertProjOf QName
f Type
t
      let u = Elims -> Term
hd []
          t' = Abs Type
b Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
u
      hd' <- applyDef o f (argFromDom a $> u)
      ps  <- patternFrom r0 r1 k (t',applyE hd') es
      return $ Proj o f : ps

instance (PatternFrom a b) => PatternFrom (Dom a) (Dom b) where
  patternFrom :: DefSing -> DefSing -> Int -> TypeOf (Dom a) -> Dom a -> TCM (Dom b)
patternFrom DefSing
r0 DefSing
r1 Int
k TypeOf (Dom a)
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' Term a -> f (Dom' Term 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
$ DefSing -> DefSing -> Int -> TypeOf a -> a -> TCMT IO b
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 Int
k TypeOf a
TypeOf (Dom a)
t

instance PatternFrom Type NLPType where
  patternFrom :: DefSing -> DefSing -> Int -> TypeOf Type -> Type -> TCM NLPType
patternFrom DefSing
r0 DefSing
r1 Int
k TypeOf Type
_ 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
<$> DefSing -> DefSing -> Int -> TypeOf Sort -> Sort -> TCMT IO NLPSort
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 Int
k () (Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
a)
            TCMT IO (NLPat -> NLPType) -> TCM NLPat -> TCM NLPType
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DefSing -> DefSing -> Int -> TypeOf Term -> Term -> TCM NLPat
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 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 :: DefSing -> DefSing -> Int -> TypeOf Sort -> Sort -> TCMT IO NLPSort
patternFrom DefSing
r0 DefSing
r1 Int
k TypeOf Sort
_ Sort
s = do
    s <- Sort -> TCMT IO Sort
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Sort
s
    case s of
      Univ Univ
u Level' Term
l -> Univ -> NLPat -> NLPSort
PUniv Univ
u (NLPat -> NLPSort) -> TCM NLPat -> TCMT IO NLPSort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DefSing
-> DefSing
-> Int
-> TypeOf (Level' Term)
-> Level' Term
-> TCM NLPat
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 Int
k () Level' Term
l
      Inf Univ
u Integer
n  -> NLPSort -> TCMT IO NLPSort
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NLPSort -> TCMT IO NLPSort) -> NLPSort -> TCMT IO NLPSort
forall a b. (a -> b) -> a -> b
$ Univ -> Integer -> NLPSort
PInf Univ
u Integer
n
      Sort
SizeUniv -> NLPSort -> TCMT IO NLPSort
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PSizeUniv
      Sort
LockUniv -> NLPSort -> TCMT IO NLPSort
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PLockUniv
      Sort
LevelUniv -> NLPSort -> TCMT IO NLPSort
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PLevelUniv
      Sort
IntervalUniv -> NLPSort -> TCMT IO NLPSort
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return NLPSort
PIntervalUniv
      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 ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> [String] -> 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 :: DefSing
-> DefSing
-> Int
-> TypeOf (Level' Term)
-> Level' Term
-> TCM NLPat
patternFrom DefSing
r0 DefSing
r1 Int
k TypeOf (Level' Term)
_ Level' Term
l = do
    t <- TCMT IO Type
forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
levelType
    v <- reallyUnLevelView l
    patternFrom r0 r1 k t v

instance PatternFrom Term NLPat where
  patternFrom :: DefSing -> DefSing -> Int -> TypeOf Term -> Term -> TCM NLPat
patternFrom DefSing
r0 DefSing
r1 Int
k TypeOf Term
t Term
v = do
    t <- Type -> TCMT IO Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked TypeOf Term
Type
t
    etaRecord <- isEtaRecordType t
    r1 <- maxDefSing r1 <$> isDefSing t
    v <- unLevel =<< abortIfBlocked v
    reportSDoc "rewriting.build" 60 $ sep
      [ "building a pattern from term v = " <+> prettyTCM v
      , " of type " <+> prettyTCM t
      ]
    pview <- pathViewAsPi'whnf
    let done = Term -> TCMT IO ()
forall (m :: * -> *) t. (MonadBlock m, AllMetas t) => t -> m ()
blockOnMetasIn Term
v TCMT IO () -> TCM NLPat -> TCM NLPat
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> NLPat -> TCM NLPat
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> NLPat
PTerm Term
v)
    case (unEl t , stripDontCare 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 ]
        p <- Dom Type -> TCM NLPat -> TCM NLPat
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Dom Type -> m a -> m a
addContext Dom Type
a (DefSing -> DefSing -> Int -> TypeOf Term -> Term -> TCM NLPat
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 (Int
k Int -> 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)
        return $ PLam (domInfo a) $ Abs (absName b) p
      (Term, Term)
_ | Left ((Dom Type
a,Abs Type
b),(Term
x,Term
y)) <- Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
pview Type
t -> do
        let body :: Term
body = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 Term
v Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ Term -> Term -> Term -> Elim' Term
forall a. a -> a -> a -> Elim' a
IApply (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term
x) (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term
y) (Term -> Elim' Term) -> Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0 ]
        p <- Dom Type -> TCM NLPat -> TCM NLPat
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Dom Type -> m a -> m a
addContext Dom Type
a (DefSing -> DefSing -> Int -> TypeOf Term -> Term -> TCM NLPat
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 (Int
k Int -> 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)
        return $ PLam (domInfo a) $ Abs (absName b) p
      (Term
_ , Var Int
i Elims
es)
       | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k     -> do
           t <- Int -> TCMT IO Type
forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Type
typeOfBV Int
i
           PBoundVar i <$> patternFrom r1 r1 k (t , Var i) 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 tel rest <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath (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 :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Type
typeOfBV Int
i
           unless (natSize tel >= natSize vs) $ blockOnMetasIn rest >> addContext tel (errNotPi rest)
           let ts = Substitution' (SubstArg [Type]) -> [Type] -> [Type]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst ([SubstArg [Type]] -> Substitution' (SubstArg [Type])
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([SubstArg [Type]] -> Substitution' (SubstArg [Type]))
-> [SubstArg [Type]] -> Substitution' (SubstArg [Type])
forall a b. (a -> b) -> a -> b
$ [SubstArg [Type]] -> [SubstArg [Type]]
forall a. [a] -> [a]
reverse ([SubstArg [Type]] -> [SubstArg [Type]])
-> [SubstArg [Type]] -> [SubstArg [Type]]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> SubstArg [Type]) -> Args -> [SubstArg [Type]]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
Arg Term -> SubstArg [Type]
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
           mbvs <- forM (zip ts vs) $ \(Type
t , Arg Term
v) -> do
             (Arg Term, Type) -> TCMT IO ()
forall (m :: * -> *) t. (MonadBlock m, AllMetas t) => t -> m ()
blockOnMetasIn (Arg Term
v,Type
t)
             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 a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
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 a. a -> TCMT IO a
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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Arg Int)
forall a. Maybe a
Nothing
           case sequence mbvs of
             Just [Arg Int]
bvs | [Arg Int] -> Bool
forall a. Ord a => [a] -> Bool
fastDistinct [Arg Int]
bvs -> do
               let allBoundVars :: VarSet
allBoundVars = Int -> VarSet
VarSet.full Int
k
                   ok :: Bool
ok = Bool -> Bool
not (DefSing -> Bool
isAlwaysSing DefSing
r1) Bool -> Bool -> Bool
||
                        [Int] -> VarSet
VarSet.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) VarSet -> VarSet -> Bool
forall a. Eq a => a -> a -> Bool
== VarSet
allBoundVars
               if Bool
ok then NLPat -> TCM NLPat
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DefSing -> Int -> [Arg Int] -> NLPat
PVar DefSing
r0 Int
i [Arg Int]
bvs) else TCM NLPat
done
                 -- Important: Definitional singularity at |PVar|s should be
                 -- that of the surrounding pattern (|r| rather than |r'|).
                 -- If only the variable itself might be definitionally singular
                 -- that is not a problem.
             Maybe [Arg Int]
_ -> TCM NLPat
done
       | Bool
otherwise -> TCM NLPat
done
      (Term
_ , Term
_ ) | Just (QName
d, Args
pars) <- Maybe (QName, Args)
etaRecord -> do
        RecordDefn 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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
        (tel, c, ci, vs) <- etaExpandRecord_ d pars def v
        ct <- assertConOf c t
        PDef (conName c) <$> patternFrom r1 r1 k (ct , Con c ci) (map Apply vs)
      (Term
_ , Lam{})   -> Type -> TCM NLPat
forall a. Type -> TCM a
errNotPi Type
t
      (Term
_ , Lit{})   -> TCM NLPat
done
      (Term
_ , Def QName
f Elims
es) | DefSing -> Bool
isAlwaysSing DefSing
r1 -> TCM NLPat
done
      (Term
_ , Def QName
f Elims
es) -> do
        Def lsuc [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc
        Def lmax [] <- primLevelMax
        case 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
            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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
            PDef f <$> patternFrom r1 r1 k (ft , Def f) es
      (Term
_ , Con ConHead
c ConInfo
ci Elims
vs) | DefSing -> Bool
isAlwaysSing DefSing
r1 -> TCM NLPat
done
      (Term
_ , Con ConHead
c ConInfo
ci Elims
vs) -> do
        ct <- ConHead -> Type -> TCMT IO Type
assertConOf ConHead
c Type
t
        PDef (conName c) <$> patternFrom r1 r1 k (ct , Con c ci) vs
      (Term
_ , Pi Dom Type
a Abs Type
b) | DefSing -> Bool
isAlwaysSing DefSing
r1 -> TCM NLPat
done
      (Term
_ , Pi Dom Type
a Abs Type
b) -> do
        pa <- DefSing
-> DefSing
-> Int
-> TypeOf (Dom Type)
-> Dom Type
-> TCM (Dom NLPType)
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 Int
k () Dom Type
a
        pb <- addContext a (patternFrom r0 r1 (k + 1) () $ absBody b)
        return $ PPi pa (Abs (absName b) 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
<$> DefSing -> DefSing -> Int -> TypeOf Sort -> Sort -> TCMT IO NLPSort
forall a b.
PatternFrom a b =>
DefSing -> DefSing -> Int -> TypeOf a -> a -> TCM b
patternFrom DefSing
r0 DefSing
r1 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 MetaId
m Elims
_)  -> TCM NLPat
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Term
_ , Dummy DummyTermKind
s Elims
_)  -> String -> TCM NLPat
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ (DummyTermKind -> String
forall a. Show a => a -> String
show DummyTermKind
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse p' -> m a'
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). 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 :: forall (m :: * -> *). PureTCM m => Int -> m Term
nlPatToTerm = Term -> m Term
forall a. a -> m a
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 :: forall (m :: * -> *). PureTCM m => NLPat -> m Term
nlPatToTerm = \case
    PVar DefSing
s 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
forall (m :: * -> *). PureTCM m => [Arg Int] -> m Args
nlPatToTerm [Arg Int]
xs
    PTerm Term
u        -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
    PDef QName
f PElims
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, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f) m Defn -> (Defn -> m Term) -> m Term
forall a b. m a -> (a -> m b) -> m b
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
<$> PElims -> m Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => PElims -> m Elims
nlPatToTerm PElims
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
<$> PElims -> m Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => PElims -> m Elims
nlPatToTerm PElims
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
forall (m :: * -> *). PureTCM m => Abs NLPat -> m (Abs Term)
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
forall (m :: * -> *). PureTCM m => Dom NLPType -> m (Dom Type)
nlPatToTerm Dom NLPType
a m (Abs Type -> Term) -> m (Abs Type) -> m Term
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Abs NLPType -> m (Abs Type)
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => Abs NLPType -> m (Abs Type)
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
forall (m :: * -> *). PureTCM m => NLPSort -> m Sort
nlPatToTerm NLPSort
s
    PBoundVar Int
i PElims
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
<$> PElims -> m Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => PElims -> m Elims
nlPatToTerm PElims
es

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

instance NLPatToTerm NLPSort Sort where
  nlPatToTerm :: forall (m :: * -> *). PureTCM m => NLPSort -> m Sort
nlPatToTerm (PUniv Univ
u NLPat
l) = Univ -> Level' Term -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (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
forall (m :: * -> *). PureTCM m => NLPat -> m (Level' Term)
nlPatToTerm NLPat
l
  nlPatToTerm (PInf Univ
u Integer
n) = Sort -> m Sort
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> m Sort) -> Sort -> m Sort
forall a b. (a -> b) -> a -> b
$ Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
n
  nlPatToTerm NLPSort
PSizeUniv = Sort -> m Sort
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
forall t. Sort' t
SizeUniv
  nlPatToTerm NLPSort
PLockUniv = Sort -> m Sort
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
forall t. Sort' t
LockUniv
  nlPatToTerm NLPSort
PLevelUniv = Sort -> m Sort
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
forall t. Sort' t
LevelUniv
  nlPatToTerm NLPSort
PIntervalUniv = Sort -> m Sort
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
forall t. Sort' t
IntervalUniv

data PatVars = PatVars
  { PatVars -> VarSet
neverSingPatVars :: VarSet
      -- ^ Variables bound in never definitionally singular contexts
  , PatVars -> VarSet
maybeSingPatVars :: VarSet
      -- ^ Variables bound in possibly definitionally singular contexts
  }
  deriving (PatVars -> PatVars -> Bool
(PatVars -> PatVars -> Bool)
-> (PatVars -> PatVars -> Bool) -> Eq PatVars
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PatVars -> PatVars -> Bool
== :: PatVars -> PatVars -> Bool
$c/= :: PatVars -> PatVars -> Bool
/= :: PatVars -> PatVars -> Bool
Eq)

instance Null PatVars where
  empty :: PatVars
empty = VarSet -> VarSet -> PatVars
PatVars VarSet
forall a. Null a => a
empty VarSet
forall a. Null a => a
empty
  null :: PatVars -> Bool
null (PatVars VarSet
ps VarSet
ps') = VarSet -> Bool
forall a. Null a => a -> Bool
null VarSet
ps Bool -> Bool -> Bool
&& VarSet -> Bool
forall a. Null a => a -> Bool
null VarSet
ps'

instance Semigroup PatVars where
  PatVars VarSet
ps VarSet
ps' <> :: PatVars -> PatVars -> PatVars
<> PatVars VarSet
qs VarSet
qs' = VarSet -> VarSet -> PatVars
PatVars (VarSet
ps VarSet -> VarSet -> VarSet
forall a. Semigroup a => a -> a -> a
<> VarSet
qs) (VarSet
ps' VarSet -> VarSet -> VarSet
forall a. Semigroup a => a -> a -> a
<> VarSet
qs')

instance Monoid PatVars where
  mempty :: PatVars
mempty = VarSet -> VarSet -> PatVars
PatVars VarSet
forall a. Monoid a => a
mempty VarSet
forall a. Monoid a => a
mempty

instance Singleton (DefSing, Int) PatVars where
  singleton :: (DefSing, Int) -> PatVars
singleton (DefSing
NeverSing,  Int
x) = VarSet -> VarSet -> PatVars
PatVars (Int -> VarSet
forall el coll. Singleton el coll => el -> coll
singleton Int
x) VarSet
forall a. Null a => a
empty
  singleton (DefSing
MaybeSing,  Int
x) = VarSet -> VarSet -> PatVars
PatVars VarSet
forall a. Null a => a
empty (Int -> VarSet
forall el coll. Singleton el coll => el -> coll
singleton Int
x)
  singleton (DefSing
AlwaysSing, Int
x) = PatVars
forall a. HasCallStack => a
__IMPOSSIBLE__

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

  default nlPatVarsUnder ::
    ( NLPatVars p, Foldable f, Functor f, a ~ f p
    ) => Int -> a -> PatVars
  nlPatVarsUnder Int
k a
x = f PatVars -> PatVars
forall m. Monoid m => f m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (f PatVars -> PatVars) -> f PatVars -> PatVars
forall a b. (a -> b) -> a -> b
$ Int -> p -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k (p -> PatVars) -> f p -> f PatVars
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a
f p
x

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

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

instance NLPatVars NLPSort where
  nlPatVarsUnder :: Int -> NLPSort -> PatVars
nlPatVarsUnder Int
k = \case
    PUniv Univ
_ NLPat
l   -> Int -> NLPat -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k NLPat
l
    PInf Univ
f Integer
n  -> PatVars
forall a. Null a => a
empty
    NLPSort
PSizeUniv -> PatVars
forall a. Null a => a
empty
    NLPSort
PLockUniv -> PatVars
forall a. Null a => a
empty
    NLPSort
PLevelUniv -> PatVars
forall a. Null a => a
empty
    NLPSort
PIntervalUniv -> PatVars
forall a. Null a => a
empty

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

instance (NLPatVars a, NLPatVars b) => NLPatVars (a,b) where
  nlPatVarsUnder :: Int -> (a, b) -> PatVars
nlPatVarsUnder Int
k (a
a,b
b) = Int -> a -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k a
a PatVars -> PatVars -> PatVars
forall a. Semigroup a => a -> a -> a
<> Int -> b -> PatVars
forall a. NLPatVars a => Int -> a -> PatVars
nlPatVarsUnder Int
k b
b

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

instance NLPatVars a => NLPatVars (Arg a) where
instance NLPatVars a => NLPatVars (Dom a) where
instance NLPatVars a => NLPatVars (Elim' a) where
instance NLPatVars PElims where

-- | 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 m a. Monoid m => (a -> m) -> f a -> m
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{}         -> [QName]
forall a. Null a => a
empty
      PDef QName
f PElims
es      -> QName -> [QName]
forall el coll. Singleton el coll => el -> coll
singleton QName
f [QName] -> [QName] -> [QName]
forall a. [a] -> [a] -> [a]
++ PElims -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables PElims
es
      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 PElims
es -> PElims -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables PElims
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
    PUniv Univ
_ NLPat
l -> NLPat -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables NLPat
l
    PInf Univ
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
    NLPSort
PLevelUniv -> [QName]
forall a. Null a => a
empty
    NLPSort
PIntervalUniv -> [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 = PElims -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables (PElims -> [QName])
-> (RewriteRule -> PElims) -> RewriteRule -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> PElims
rewPats

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

instance Free NLPat where
  freeVars' :: forall a c. IsVarSet a c => NLPat -> FreeM a c
freeVars' = \case
    PVar{}         -> FreeM a c
forall a. Monoid a => a
mempty
    PDef QName
_ PElims
es      -> PElims -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => PElims -> FreeM a c
freeVars' PElims
es
    PLam ArgInfo
_ Abs NLPat
u       -> Abs NLPat -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Abs NLPat -> 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
forall a c. IsVarSet a c => (Dom NLPType, Abs NLPType) -> 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
forall a c. IsVarSet a c => NLPSort -> FreeM a c
freeVars' NLPSort
s
    PBoundVar Int
_ PElims
es -> PElims -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => PElims -> FreeM a c
freeVars' PElims
es
    PTerm Term
t        -> Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Term -> FreeM a c
freeVars' Term
t

instance Free NLPType where
  freeVars' :: forall a c. IsVarSet a c => NLPType -> FreeM a c
freeVars' (NLPType NLPSort
s NLPat
a) =
    ReaderT (FreeEnv' a IgnoreSorts c) Identity Bool
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
-> ReaderT (FreeEnv' a IgnoreSorts c) Identity 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) -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (NLPSort, NLPat) -> FreeM a c
freeVars' (NLPSort
s, NLPat
a))
      {- else -} (NLPat -> ReaderT (FreeEnv' a IgnoreSorts c) Identity c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => NLPat -> FreeM a c
freeVars' NLPat
a)

instance Free NLPSort where
  freeVars' :: forall a c. IsVarSet a c => NLPSort -> FreeM a c
freeVars' = \case
    PUniv Univ
_ NLPat
l -> NLPat -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => NLPat -> FreeM a c
freeVars' NLPat
l
    PInf Univ
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
    NLPSort
PLevelUniv -> FreeM a c
forall a. Monoid a => a
mempty
    NLPSort
PIntervalUniv -> FreeM a c
forall a. Monoid a => a
mempty

-- Throws a pattern violation if the given term contains any
-- metavariables.
blockOnMetasIn :: (MonadBlock m, AllMetas t) => t -> m ()
blockOnMetasIn :: forall (m :: * -> *) t. (MonadBlock m, AllMetas t) => t -> m ()
blockOnMetasIn t
t = case t -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAllMetasIn t
t of
  UnblockOnAll Set Blocker
ms | Set Blocker -> Bool
forall a. Null a => a -> Bool
null Set Blocker
ms -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  Blocker
b -> Blocker -> m ()
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
b

-- Helper functions


assertPi :: Type -> TCM (Dom Type, Abs Type)
assertPi :: Type -> TCM (Dom Type, Abs Type)
assertPi Type
t = Type -> TCMT IO Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t TCMT IO Type
-> (Type -> TCM (Dom Type, Abs Type)) -> TCM (Dom Type, Abs Type)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  El Sort
_ (Pi Dom Type
a Abs Type
b) -> (Dom Type, Abs Type) -> TCM (Dom Type, Abs Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom Type
a,Abs Type
b)
  Type
t             -> Type -> TCM (Dom Type, Abs Type)
forall a. Type -> TCM a
errNotPi Type
t

errNotPi :: Type -> TCM a
errNotPi :: forall a. Type -> TCM a
errNotPi Type
t = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
IlltypedRewriteRule (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
    , TCMT IO Doc
"should be a function type, but it isn't."
    , TCMT IO Doc
"Do you have any non-confluent rewrite rules?"
    ]

assertPath :: Type -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
assertPath :: Type -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
assertPath Type
t = Type -> TCMT IO Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t TCMT IO Type -> (Type -> TCMT IO PathView) -> TCMT IO PathView
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> TCMT IO PathView
forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView TCMT IO PathView
-> (PathView
    -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term))
-> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  PathType Sort
s QName
q Arg Term
l Arg Term
b Arg Term
u Arg Term
v -> (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
-> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort
s,QName
q,Arg Term
l,Arg Term
b,Arg Term
u,Arg Term
v)
  OType Type
t -> Type -> TCM (Sort, QName, Arg Term, Arg Term, Arg Term, Arg Term)
forall a. Type -> TCM a
errNotPath Type
t

errNotPath :: Type -> TCM a
errNotPath :: forall a. Type -> TCM a
errNotPath Type
t = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
IlltypedRewriteRule (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
    , TCMT IO Doc
"should be a path type, but it isn't."
    , TCMT IO Doc
"Do you have any non-confluent rewrite rules?"
    ]

assertProjOf :: QName -> Type -> TCM (Dom Type, Abs Type)
assertProjOf :: QName -> Type -> TCM (Dom Type, Abs Type)
assertProjOf QName
f Type
t = do
  t <- Type -> TCMT IO Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
  getDefType f t >>= \case
    Just (El Sort
_ (Pi Dom Type
a Abs Type
b)) -> (Dom Type, Abs Type) -> TCM (Dom Type, Abs Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dom Type
a,Abs Type
b)
    Maybe Type
_ -> QName -> Type -> TCM (Dom Type, Abs Type)
forall a. QName -> Type -> TCM a
errNotProjOf QName
f Type
t

errNotProjOf :: QName -> Type -> TCM a
errNotProjOf :: forall a. QName -> Type -> TCM a
errNotProjOf QName
f Type
t = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
IlltypedRewriteRule (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f , TCMT IO Doc
"should be a projection from type"
      , Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t , TCMT IO Doc
"but it isn't."
      , TCMT IO Doc
"Do you have any non-confluent rewrite rules?"
      ]

assertConOf :: ConHead -> Type -> TCM Type
assertConOf :: ConHead -> Type -> TCMT IO Type
assertConOf ConHead
c Type
t = 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 TCMT IO (Maybe ((QName, Type, Args), Type))
-> (Maybe ((QName, Type, Args), Type) -> TCMT IO Type)
-> TCMT IO Type
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just ((QName, Type, Args)
_ , Type
ct) -> Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ct
    Maybe ((QName, Type, Args), Type)
Nothing -> ConHead -> Type -> TCMT IO Type
forall a. ConHead -> Type -> TCM a
errNotConOf ConHead
c Type
t

errNotConOf :: ConHead -> Type -> TCM a
errNotConOf :: forall a. ConHead -> Type -> TCM a
errNotConOf ConHead
c Type
t = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
IlltypedRewriteRule (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ ConHead -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c , TCMT IO Doc
"should be a constructor of type"
      , Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t , TCMT IO Doc
"but it isn't."
      , TCMT IO Doc
"Do you have any non-confluent rewrite rules?"
      ]