{-# 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        ( (>=>), 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.Syntax.Internal.MetaVars ( AllMetas, unblockOnAllMetasIn )

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

-- | 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 a b where
  patternFrom :: Relevance -> Int -> TypeOf a -> a -> TCM b

instance (PatternFrom a b) => PatternFrom (Arg a) (Arg b) where
  patternFrom :: Relevance -> Int -> TypeOf (Arg a) -> Arg a -> TCM (Arg b)
patternFrom Relevance
r Int
k TypeOf (Arg a)
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse (Relevance -> Int -> TypeOf a -> a -> TCMT IO b
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r' 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 [Elim' NLPat] where
  patternFrom :: Relevance -> Int -> TypeOf Elims -> Elims -> TCM [Elim' NLPat]
patternFrom Relevance
r Int
k (Type
t,Elims -> Term
hd) = \case
    [] -> [Elim' NLPat] -> TCM [Elim' NLPat]
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 r 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 r 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 r k interval i
      ps  <- patternFrom r 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 r k (t',applyE hd') es
      return $ Proj o f : ps

instance (PatternFrom a b) => PatternFrom (Dom a) (Dom b) where
  patternFrom :: Relevance -> Int -> TypeOf (Dom a) -> Dom a -> TCM (Dom b)
patternFrom Relevance
r 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
$ Relevance -> Int -> TypeOf a -> a -> TCMT IO b
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k TypeOf a
TypeOf (Dom a)
t

instance PatternFrom Type NLPType where
  patternFrom :: Relevance -> Int -> TypeOf Type -> Type -> TCM NLPType
patternFrom Relevance
r 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
<$> Relevance -> Int -> TypeOf Sort -> Sort -> TCMT IO NLPSort
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> 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 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
<*> Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> 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 -> TypeOf Sort -> Sort -> TCMT IO NLPSort
patternFrom Relevance
r 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
<$> Relevance
-> Int -> TypeOf (Level' Term) -> Level' Term -> TCM NLPat
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r 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 :: Relevance
-> Int -> TypeOf (Level' Term) -> Level' Term -> TCM NLPat
patternFrom Relevance
r 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 r k t v

instance PatternFrom Term NLPat where
  patternFrom :: Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat
patternFrom Relevance
r0 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
    prop <- isPropM t
    let r = if Bool
prop then Relevance
Irrelevant else Relevance
r0
    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 (Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r (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 (Relevance -> Int -> TypeOf Term -> Term -> TCM NLPat
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r (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 :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
           PBoundVar i <$> patternFrom r 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 :: * -> *).
(Applicative m, MonadFail 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 -> 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
           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 :: 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 a. a -> TCMT IO a
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
        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 => QName -> m Definition
getConstInfo QName
d
        (tel, c, ci, vs) <- etaExpandRecord_ d pars def v
        ct <- assertConOf c t
        PDef (conName c) <$> patternFrom r 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) | Relevance -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Relevance
r -> 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 => QName -> m Definition
getConstInfo QName
f
            PDef f <$> patternFrom r k (ft , Def f) 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) -> do
        ct <- ConHead -> Type -> TCMT IO Type
assertConOf ConHead
c Type
t
        PDef (conName c) <$> patternFrom r k (ct , Con c ci) 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
        pa <- Relevance
-> Int -> TypeOf (Dom Type) -> Dom Type -> TCM (Dom NLPType)
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> a -> TCM b
patternFrom Relevance
r Int
k () Dom Type
a
        pb <- addContext a (patternFrom r (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
<$> Relevance -> Int -> TypeOf Sort -> Sort -> TCMT IO NLPSort
forall a b.
PatternFrom a b =>
Relevance -> Int -> TypeOf a -> 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 MetaId
m Elims
_)  -> 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)
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 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 [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 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
<$> [Elim' NLPat] -> m Elims
forall p a (m :: * -> *). (NLPatToTerm p a, PureTCM m) => p -> m a
forall (m :: * -> *). PureTCM m => [Elim' NLPat] -> m Elims
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
forall (m :: * -> *). PureTCM m => [Elim' NLPat] -> m Elims
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
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 [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
forall (m :: * -> *). PureTCM m => [Elim' NLPat] -> m Elims
nlPatToTerm [Elim' NLPat]
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

-- | 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 m a. Monoid m => (a -> m) -> f a -> m
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
    PUniv Univ
_ NLPat
l   -> Int -> NLPat -> IntSet
forall a. NLPatVars a => Int -> a -> IntSet
nlPatVarsUnder Int
k NLPat
l
    PInf Univ
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
    NLPSort
PLevelUniv -> IntSet
forall a. Null a => a
empty
    NLPSort
PIntervalUniv -> 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
k Int -> 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 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 Int
_ [Arg Int]
_       -> [QName]
forall a. Null a => a
empty
      PDef QName
f [Elim' NLPat]
es      -> QName -> [QName]
forall el coll. Singleton el coll => el -> coll
singleton QName
f [QName] -> [QName] -> [QName]
forall a. [a] -> [a] -> [a]
++ [Elim' NLPat] -> [QName]
forall a. GetMatchables a => a -> [QName]
getMatchables [Elim' NLPat]
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 [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
    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 = [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' :: forall a c. IsVarSet a c => 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
forall a c. IsVarSet a c => [Elim' NLPat] -> 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
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
_ [Elim' NLPat]
es -> [Elim' NLPat] -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => [Elim' NLPat] -> 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
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
GenericDocError (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
GenericDocError (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
GenericDocError (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
GenericDocError (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?"
      ]