    {-# LANGUAGE NondecreasingIndentation #-}

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

    module Agda.TypeChecking.Rewriting.NonLinPattern where

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

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

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

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

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

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

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

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

    instance PatternFrom (Type, Term) Elims [Elim' NLPat] where
      patternFrom :: Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
    patternFrom Relevance
    r Int
    k (Type
    t,Term
    hd) = \case
        [] -> [Elim' NLPat] -> TCM [Elim' NLPat]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        (Apply Arg Term
    u : Elims
    es) -> do
          ~(Pi Dom Type
    a Abs Type
    b) <- Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> TCMT IO Type -> TCMT IO Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t
          Arg NLPat
    p   <- Relevance -> Int -> Dom Type -> Arg Term -> TCM (Arg NLPat)
    forall t a b.
    PatternFrom t a b =>
    Relevance -> Int -> t -> a -> TCM b
    patternFrom Relevance
    r Int
    k Dom Type
    a Arg Term
    u
          Type
    t'  <- Type
    t Type -> Arg Term -> TCMT IO Type
    forall a (m :: * -> *).
    (PiApplyM a, MonadReduce m, HasBuiltins m) =>
    Type -> a -> m Type
    `piApplyM` Arg Term
    u
          let hd' :: Term
    hd' = Term
    hd Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ Arg Term
    u ]
          [Elim' NLPat]
    ps  <- Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
    forall t a b.
    PatternFrom t a b =>
    Relevance -> Int -> t -> a -> TCM b
    patternFrom Relevance
    r Int
    k (Type
    t',Term
    hd') Elims
    es
          [Elim' NLPat] -> TCM [Elim' NLPat]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Elim' NLPat] -> TCM [Elim' NLPat])
    -> [Elim' NLPat] -> TCM [Elim' NLPat]
    forall a b. (a -> b) -> a -> b
    $ Arg NLPat -> Elim' NLPat
    forall a. Arg a -> Elim' a
    Apply Arg NLPat
    p Elim' NLPat -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. a -> [a] -> [a]
    : [Elim' NLPat]
    ps
        (IApply Term
    x Term
    y Term
    i : Elims
    es) -> do
          ~(PathType Sort
    s QName
    q Arg Term
    l Arg Term
    b Arg Term
    u Arg Term
    v) <- Type -> TCMT IO PathView
    forall (m :: * -> *). HasBuiltins m => Type -> m PathView
    pathView (Type -> TCMT IO PathView) -> TCMT IO Type -> TCMT IO PathView
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t
          let t' :: Type
    t' = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    b Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    i ]
          let hd' :: Term
    hd' = Term
    hd Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [Term -> Term -> Term -> Elim' Term
    forall a. a -> a -> a -> Elim' a
    IApply Term
    x Term
    y Term
    i]
          Type
    interval <- TCMT IO Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType
          NLPat
    p   <- Relevance -> Int -> Type -> Term -> TCM NLPat
    forall t a b.
    PatternFrom t a b =>
    Relevance -> Int -> t -> a -> TCM b
    patternFrom Relevance
    r Int
    k Type
    interval Term
    i
          [Elim' NLPat]
    ps  <- Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
    forall t a b.
    PatternFrom t a b =>
    Relevance -> Int -> t -> a -> TCM b
    patternFrom Relevance
    r Int
    k (Type
    t',Term
    hd') Elims
    es
          [Elim' NLPat] -> TCM [Elim' NLPat]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Elim' NLPat] -> TCM [Elim' NLPat])
    -> [Elim' NLPat] -> TCM [Elim' NLPat]
    forall a b. (a -> b) -> a -> b
    $ NLPat -> NLPat -> NLPat -> Elim' NLPat
    forall a. a -> a -> a -> Elim' a
    IApply (Term -> NLPat
    PTerm Term
    x) (Term -> NLPat
    PTerm Term
    y) NLPat
    p Elim' NLPat -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. a -> [a] -> [a]
    : [Elim' NLPat]
    ps
        (Proj ProjOrigin
    o QName
    f : Elims
    es) -> do
          ~(Just (El Sort
    _ (Pi Dom Type
    a Abs Type
    b))) <- QName -> Type -> TCMT IO (Maybe Type)
    forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
    getDefType QName
    f (Type -> TCMT IO (Maybe Type))
    -> TCMT IO Type -> TCMT IO (Maybe Type)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t
          let t' :: Type
    t' = Abs Type
    b Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Term
    SubstArg Type
    hd
          Term
    hd' <- ProjOrigin -> QName -> Arg Term -> TCMT IO Term
    forall (m :: * -> *).
    HasConstInfo m =>
    ProjOrigin -> QName -> Arg Term -> m Term
    applyDef ProjOrigin
    o QName
    f (Dom Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom Dom Type
    a Arg Type -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Term
    hd)
          [Elim' NLPat]
    ps  <- Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]
    forall t a b.
    PatternFrom t a b =>
    Relevance -> Int -> t -> a -> TCM b
    patternFrom Relevance
    r Int
    k (Type
    t',Term
    hd') Elims
    es
          [Elim' NLPat] -> TCM [Elim' NLPat]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Elim' NLPat] -> TCM [Elim' NLPat])
    -> [Elim' NLPat] -> TCM [Elim' NLPat]
    forall a b. (a -> b) -> a -> b
    $ ProjOrigin -> QName -> Elim' NLPat
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    o QName
    f Elim' NLPat -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. a -> [a] -> [a]
    : [Elim' NLPat]
    ps

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

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

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

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

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

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

    class NLPatToTerm p a where
      nlPatToTerm :: PureTCM m => p -> m a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    instance Free NLPat where
      freeVars' :: 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
    freeVars' [Elim' NLPat]
    es
        PLam ArgInfo
    _ Abs NLPat
    u       -> Abs NLPat -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' Abs NLPat
    u
        PPi Dom NLPType
    a Abs NLPType
    b        -> (Dom NLPType, Abs NLPType) -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' (Dom NLPType
    a,Abs NLPType
    b)
        PSort NLPSort
    s        -> NLPSort -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' NLPSort
    s
        PBoundVar Int
    _ [Elim' NLPat]
    es -> [Elim' NLPat] -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' [Elim' NLPat]
    es
        PTerm Term
    t        -> Term -> FreeM a c
    forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
    freeVars' Term
    t

    instance Free NLPType where
      freeVars' :: 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
    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
    freeVars' NLPat
    a)

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