{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.With where
import Prelude hiding ((!!))
import Control.Monad
import Control.Monad.Writer (WriterT, runWriterT, tell)
import qualified Data.List as List
import Data.Maybe
import Data.Foldable ( foldrM )
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pattern as A
import Agda.Syntax.Abstract.Views
import Agda.Syntax.Info
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Free
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive ( getRefl )
import Agda.TypeChecking.Records
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Telescope.Path
import Agda.TypeChecking.Abstract
import Agda.TypeChecking.Rules.LHS.Implicit
import Agda.TypeChecking.Rules.LHS.Problem (ProblemEq(..))
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.List1 (List1)
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null (empty)
import Agda.Utils.Permutation
import Agda.Syntax.Common.Pretty (prettyShow)
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Utils.Size
import Agda.Utils.Impossible
splitTelForWith
:: Telescope
-> Type
-> [Arg (Term, EqualityView)]
-> ( Telescope
, Telescope
, Permutation
, Type
, [Arg (Term, EqualityView)]
)
splitTelForWith :: Telescope
-> Type
-> [Arg (Term, EqualityView)]
-> (Telescope, Telescope, Permutation, Type,
[Arg (Term, EqualityView)])
splitTelForWith Telescope
delta Type
t [Arg (Term, EqualityView)]
vtys = let
fv :: VarSet
fv = [Arg (Term, EqualityView)] -> VarSet
forall t. Free t => t -> VarSet
allFreeVars [Arg (Term, EqualityView)]
vtys
SplitTel Telescope
delta1 Telescope
delta2 Permutation
perm = VarSet -> Telescope -> SplitTel
splitTelescope VarSet
fv Telescope
delta
pi :: Substitution' Term
pi = Impossible -> Permutation -> Substitution' Term
forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming Impossible
HasCallStack => Impossible
impossible (Permutation -> Permutation
reverseP Permutation
perm)
rho :: Substitution' Term
rho = Impossible -> Int -> Substitution' Term
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
HasCallStack => Impossible
impossible (Int -> Substitution' Term) -> Int -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta2
rhopi :: Substitution' Term
rhopi = Substitution' Term -> Substitution' Term -> Substitution' Term
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS Substitution' Term
rho Substitution' Term
pi
t' :: Type
t' = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Type)
pi Type
t
vtys' :: [Arg (Term, EqualityView)]
vtys' = Substitution' (SubstArg [Arg (Term, EqualityView)])
-> [Arg (Term, EqualityView)] -> [Arg (Term, EqualityView)]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg [Arg (Term, EqualityView)])
rhopi [Arg (Term, EqualityView)]
vtys
in (Telescope
delta1, Telescope
delta2, Permutation
perm, Type
t', [Arg (Term, EqualityView)]
vtys')
withFunctionType
:: Telescope
-> [Arg (Term, EqualityView)]
-> Telescope
-> Type
-> [(Int,(Term,Term))]
-> TCM (Type, Nat)
withFunctionType :: Telescope
-> [Arg (Term, EqualityView)]
-> Telescope
-> Type
-> [(Int, (Term, Term))]
-> TCM (Type, Int)
withFunctionType Telescope
delta1 [Arg (Term, EqualityView)]
vtys Telescope
delta2 Type
b [(Int, (Term, Term))]
bndry = Telescope -> TCM (Type, Int) -> TCM (Type, Int)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta1 (TCM (Type, Int) -> TCM (Type, Int))
-> TCM (Type, Int) -> TCM (Type, Int)
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.with.abstract" Int
20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"preparing for with-abstraction"
let dbg :: Int -> [Char] -> a -> m ()
dbg Int
n [Char]
s a
x = [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.abstract" Int
n (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" =") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
x
d2b <- Telescope -> Type -> [(Int, (Term, Term))] -> TCM Type
telePiPath_ Telescope
delta2 Type
b [(Int, (Term, Term))]
bndry
dbg 30 "Δ₂ → B" d2b
d2b <- normalise d2b
dbg 30 "normal Δ₂ → B" d2b
d2b <- etaContract d2b
dbg 30 "eta-contracted Δ₂ → B" d2b
vtys <- etaContract =<< normalise vtys
wd2b <- foldrM piAbstract d2b vtys
dbg 30 "wΓ → Δ₂ → B" wd2b
let nwithargs = [EqualityView] -> Int
countWithArgs ((Arg (Term, EqualityView) -> EqualityView)
-> [Arg (Term, EqualityView)] -> [EqualityView]
forall a b. (a -> b) -> [a] -> [b]
map ((Term, EqualityView) -> EqualityView
forall a b. (a, b) -> b
snd ((Term, EqualityView) -> EqualityView)
-> (Arg (Term, EqualityView) -> (Term, EqualityView))
-> Arg (Term, EqualityView)
-> EqualityView
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Term, EqualityView) -> (Term, EqualityView)
forall e. Arg e -> e
unArg) [Arg (Term, EqualityView)]
vtys)
TelV wtel _ <- telViewUpTo nwithargs wd2b
let bndry' = [(Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
sd2,(Term -> Term
lams Term
u0, Term -> Term
lams Term
u1)) | (Int
i,(Term
u0,Term
u1)) <- [(Int, (Term, Term))]
bndry, Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
sd2]
where sd2 :: Int
sd2 = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta2
lams :: Term -> Term
lams Term
u = Telescope -> Term -> Term
forall a. TeleNoAbs a => a -> Term -> Term
teleNoAbs Telescope
wtel (Telescope -> Term -> Term
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
delta2 Term
u)
d1wd2b <- telePiPath_ delta1 wd2b bndry'
dbg 30 "Δ₁ → wΓ → Δ₂ → B" d1wd2b
return (d1wd2b, nwithargs)
countWithArgs :: [EqualityView] -> Nat
countWithArgs :: [EqualityView] -> Int
countWithArgs = [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int)
-> ([EqualityView] -> [Int]) -> [EqualityView] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EqualityView -> Int) -> [EqualityView] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map EqualityView -> Int
forall {a}. Num a => EqualityView -> a
countArgs
where
countArgs :: EqualityView -> a
countArgs OtherType{} = a
1
countArgs IdiomType{} = a
2
countArgs EqualityType{} = a
2
withArguments :: [Arg (Term, EqualityView)] ->
TCM [Arg Term]
withArguments :: [Arg (Term, EqualityView)] -> TCM Args
withArguments [Arg (Term, EqualityView)]
vtys = do
tss <- [Arg (Term, EqualityView)]
-> (Arg (Term, EqualityView) -> TCM Args) -> TCMT IO [Args]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Arg (Term, EqualityView)]
vtys ((Arg (Term, EqualityView) -> TCM Args) -> TCMT IO [Args])
-> (Arg (Term, EqualityView) -> TCM Args) -> TCMT IO [Args]
forall a b. (a -> b) -> a -> b
$ \ (Arg ArgInfo
info (Term, EqualityView)
ts) -> ([Term] -> Args) -> TCMT IO [Term] -> TCM Args
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Term -> Arg Term) -> [Term] -> Args
forall a b. (a -> b) -> [a] -> [b]
map (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info)) (TCMT IO [Term] -> TCM Args) -> TCMT IO [Term] -> TCM Args
forall a b. (a -> b) -> a -> b
$ case (Term, EqualityView)
ts of
(Term
v, OtherType Type
a) -> [Term] -> TCMT IO [Term]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Term
v]
(Term
prf, eqt :: EqualityView
eqt@(EqualityType Sort
s QName
_eq Args
_pars Arg Term
_t Arg Term
v Arg Term
_v')) -> [Term] -> TCMT IO [Term]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v, Term
prf]
(Term
v, IdiomType Type
t) -> do
mkRefl <- TCM (Arg Term -> Term)
getRefl
pure [v, mkRefl (defaultArg v)]
pure (concat tss)
buildWithFunction
:: [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Nat
-> Substitution
-> Permutation
-> Nat
-> Nat
-> List1 A.SpineClause
-> TCM (List1 A.SpineClause)
buildWithFunction :: [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Int
-> Substitution' Term
-> Permutation
-> Int
-> Int
-> List1 (Clause' SpineLHS)
-> TCM (List1 (Clause' SpineLHS))
buildWithFunction [Name]
cxtNames QName
f QName
aux Type
t Telescope
delta [NamedArg DeBruijnPattern]
qs Int
npars Substitution' Term
withSub Permutation
perm Int
n1 Int
n List1 (Clause' SpineLHS)
cs = (Clause' SpineLHS -> TCMT IO (Clause' SpineLHS))
-> List1 (Clause' SpineLHS) -> TCM (List1 (Clause' SpineLHS))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
buildWithClause List1 (Clause' SpineLHS)
cs
where
buildWithClause :: Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
buildWithClause (A.Clause (A.SpineLHS LHSInfo
i QName
_ [NamedArg Pattern]
allPs) [ProblemEq]
inheritedPats RHS
rhs WhereDeclarations
wh Bool
catchall) = do
let ([NamedArg Pattern]
ps, [NamedArg Pattern]
wps) = [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
splitOffTrailingWithPatterns [NamedArg Pattern]
allPs
([NamedArg Pattern]
wps0, [NamedArg Pattern]
wps1) = Int
-> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [NamedArg Pattern]
wps
ps0 :: [NamedArg Pattern]
ps0 = (NamedArg Pattern -> NamedArg Pattern)
-> [NamedArg Pattern] -> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg Pattern -> Pattern
forall {e}. Pattern' e -> Pattern' e
fromWithP) [NamedArg Pattern]
wps0
where
fromWithP :: Pattern' e -> Pattern' e
fromWithP (A.WithP PatInfo
_ Pattern' e
p) = Pattern' e
p
fromWithP Pattern' e
_ = Pattern' e
forall a. HasCallStack => a
__IMPOSSIBLE__
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"inheritedPats:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=" 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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
a
| A.ProblemEq Pattern
p Term
v Dom Type
a <- [ProblemEq]
inheritedPats
]
(strippedPats, ps') <- [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Int
-> Permutation
-> [NamedArg Pattern]
-> TCM ([ProblemEq], [NamedArg Pattern])
stripWithClausePatterns [Name]
cxtNames QName
f QName
aux Type
t Telescope
delta [NamedArg DeBruijnPattern]
qs Int
npars Permutation
perm [NamedArg Pattern]
ps
reportSDoc "tc.with" 50 $ hang "strippedPats:" 2 $
vcat [ prettyA p <+> "==" <+> prettyTCM v <+> (":" <+> prettyTCM t)
| A.ProblemEq p v t <- strippedPats ]
rhs <- buildRHS strippedPats rhs
let (ps1, ps2) = splitAt n1 ps'
let result = SpineLHS
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Bool
-> Clause' SpineLHS
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (LHSInfo -> QName -> [NamedArg Pattern] -> SpineLHS
A.SpineLHS LHSInfo
i QName
aux ([NamedArg Pattern] -> SpineLHS) -> [NamedArg Pattern] -> SpineLHS
forall a b. (a -> b) -> a -> b
$ [NamedArg Pattern]
ps1 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps0 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps2 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
wps1)
([ProblemEq]
inheritedPats [ProblemEq] -> [ProblemEq] -> [ProblemEq]
forall a. [a] -> [a] -> [a]
++ [ProblemEq]
strippedPats)
RHS
rhs WhereDeclarations
wh Bool
catchall
reportSDoc "tc.with" 20 $ vcat
[ "buildWithClause returns" <+> prettyA result
]
return result
buildRHS :: [ProblemEq] -> RHS -> TCMT IO RHS
buildRHS [ProblemEq]
_ rhs :: RHS
rhs@A.RHS{} = RHS -> TCMT IO RHS
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return RHS
rhs
buildRHS [ProblemEq]
_ rhs :: RHS
rhs@RHS
A.AbsurdRHS = RHS -> TCMT IO RHS
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return RHS
rhs
buildRHS [ProblemEq]
_ (A.WithRHS QName
q [WithExpr]
es List1 Clause
cs) = QName -> [WithExpr] -> List1 Clause -> RHS
A.WithRHS QName
q [WithExpr]
es (List1 Clause -> RHS) -> TCMT IO (List1 Clause) -> TCMT IO RHS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(Clause -> TCMT IO Clause)
-> List1 Clause -> TCMT IO (List1 Clause)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM ((Clause' SpineLHS -> Clause
forall a b. LHSToSpine a b => b -> a
A.spineToLhs (Clause' SpineLHS -> Clause)
-> (Clause' SpineLHS -> Clause' SpineLHS)
-> Clause' SpineLHS
-> Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause' SpineLHS -> Clause' SpineLHS
permuteNamedDots) (Clause' SpineLHS -> Clause)
-> (Clause -> TCMT IO (Clause' SpineLHS))
-> Clause
-> TCMT IO Clause
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Clause' SpineLHS -> TCMT IO (Clause' SpineLHS)
buildWithClause (Clause' SpineLHS -> TCMT IO (Clause' SpineLHS))
-> (Clause -> Clause' SpineLHS)
-> Clause
-> TCMT IO (Clause' SpineLHS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Clause' SpineLHS
forall a b. LHSToSpine a b => a -> b
A.lhsToSpine) List1 Clause
cs
buildRHS [ProblemEq]
strippedPats1 (A.RewriteRHS [RewriteEqn]
qes [ProblemEq]
strippedPats2 RHS
rhs WhereDeclarations
wh) =
(RHS -> WhereDeclarations -> RHS)
-> WhereDeclarations -> RHS -> RHS
forall a b c. (a -> b -> c) -> b -> a -> c
flip ([RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
A.RewriteRHS [RewriteEqn]
qes (Substitution' (SubstArg [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg [ProblemEq])
withSub ([ProblemEq] -> [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
forall a b. (a -> b) -> a -> b
$ [ProblemEq]
strippedPats1 [ProblemEq] -> [ProblemEq] -> [ProblemEq]
forall a. [a] -> [a] -> [a]
++ [ProblemEq]
strippedPats2)) WhereDeclarations
wh (RHS -> RHS) -> TCMT IO RHS -> TCMT IO RHS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ProblemEq] -> RHS -> TCMT IO RHS
buildRHS [] RHS
rhs
permuteNamedDots :: A.SpineClause -> A.SpineClause
permuteNamedDots :: Clause' SpineLHS -> Clause' SpineLHS
permuteNamedDots (A.Clause SpineLHS
lhs [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh Bool
catchall) =
SpineLHS
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> Bool
-> Clause' SpineLHS
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause SpineLHS
lhs (Substitution' (SubstArg [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg [ProblemEq])
withSub [ProblemEq]
strippedPats) RHS
rhs WhereDeclarations
wh Bool
catchall
stripWithClausePatterns
:: [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Nat
-> Permutation
-> [NamedArg A.Pattern]
-> TCM ([A.ProblemEq], [NamedArg A.Pattern])
stripWithClausePatterns :: [Name]
-> QName
-> QName
-> Type
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Int
-> Permutation
-> [NamedArg Pattern]
-> TCM ([ProblemEq], [NamedArg Pattern])
stripWithClausePatterns [Name]
cxtNames QName
parent QName
f Type
t Telescope
delta [NamedArg DeBruijnPattern]
qs Int
npars Permutation
perm [NamedArg Pattern]
ps = do
ps <- [NamedArg Pattern] -> TCM [NamedArg Pattern]
forall a. ExpandPatternSynonyms a => a -> TCM a
expandPatternSynonyms [NamedArg Pattern]
ps
let paramPat Int
i DeBruijnPattern
_ = BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern) -> BindName -> Pattern
forall a b. (a -> b) -> a -> b
$ Name -> BindName
A.mkBindName (Name -> BindName) -> Name -> BindName
forall a b. (a -> b) -> a -> b
$ Name -> [Name] -> Int -> Name
forall a. a -> [a] -> Int -> a
indexWithDefault Name
forall a. HasCallStack => a
__IMPOSSIBLE__ [Name]
cxtNames Int
i
ps' = (Int -> NamedArg DeBruijnPattern -> NamedArg Pattern)
-> [Int] -> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ((Named NamedName DeBruijnPattern -> Named NamedName Pattern)
-> NamedArg DeBruijnPattern -> NamedArg Pattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName DeBruijnPattern -> Named NamedName Pattern)
-> NamedArg DeBruijnPattern -> NamedArg Pattern)
-> (Int
-> Named NamedName DeBruijnPattern -> Named NamedName Pattern)
-> Int
-> NamedArg DeBruijnPattern
-> NamedArg Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DeBruijnPattern -> Pattern)
-> Named NamedName DeBruijnPattern -> Named NamedName Pattern
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((DeBruijnPattern -> Pattern)
-> Named NamedName DeBruijnPattern -> Named NamedName Pattern)
-> (Int -> DeBruijnPattern -> Pattern)
-> Int
-> Named NamedName DeBruijnPattern
-> Named NamedName Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> DeBruijnPattern -> Pattern
paramPat) [Int
0..] (Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Int -> [a] -> [a]
take Int
npars [NamedArg DeBruijnPattern]
qs) [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps
psi <- insertImplicitPatternsT ExpandLast ps' t
reportSDoc "tc.with.strip" 10 $ vcat
[ "stripping patterns"
, nest 2 $ "t = " <+> prettyTCM t
, nest 2 $ "ps = " <+> fsep (punctuate comma $ map prettyA ps)
, nest 2 $ "ps' = " <+> fsep (punctuate comma $ map prettyA ps')
, nest 2 $ "psi = " <+> fsep (punctuate comma $ map prettyA psi)
, nest 2 $ "qs = " <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs)
, nest 2 $ "perm= " <+> text (show perm)
]
(ps', strippedPats) <- runWriterT $ strip (Def parent []) t psi qs
reportSDoc "tc.with.strip" 50 $ nest 2 $
"strippedPats:" <+> vcat [ prettyA p <+> "=" <+> prettyTCM v <+> ":" <+> prettyTCM a | A.ProblemEq p v a <- strippedPats ]
let psp = Permutation -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. Permutation -> [a] -> [a]
permute Permutation
perm [NamedArg Pattern]
ps'
reportSDoc "tc.with.strip" 10 $ vcat
[ nest 2 $ "ps' = " <+> fsep (punctuate comma $ map prettyA ps')
, nest 2 $ "psp = " <+> fsep (punctuate comma $ map prettyA $ psp)
]
return (strippedPats, psp)
where
varArgInfo :: DBPatVar -> ArgInfo
varArgInfo = \ DBPatVar
x -> let n :: Int
n = DBPatVar -> Int
dbPatVarIndex DBPatVar
x in
if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [ArgInfo] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ArgInfo]
infos then [ArgInfo]
infos [ArgInfo] -> Int -> ArgInfo
forall a. HasCallStack => [a] -> Int -> a
!! Int
n else ArgInfo
forall a. HasCallStack => a
__IMPOSSIBLE__
where infos :: [ArgInfo]
infos = [ArgInfo] -> [ArgInfo]
forall a. [a] -> [a]
reverse ([ArgInfo] -> [ArgInfo]) -> [ArgInfo] -> [ArgInfo]
forall a b. (a -> b) -> a -> b
$ (Dom ([Char], Type) -> ArgInfo)
-> [Dom ([Char], Type)] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map Dom ([Char], Type) -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo ([Dom ([Char], Type)] -> [ArgInfo])
-> [Dom ([Char], Type)] -> [ArgInfo]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
delta
setVarArgInfo :: DBPatVar -> NamedArg Pattern -> NamedArg Pattern
setVarArgInfo DBPatVar
x NamedArg Pattern
p = Origin -> NamedArg Pattern -> NamedArg Pattern
forall a. LensOrigin a => Origin -> a -> a
setOrigin (NamedArg Pattern -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin NamedArg Pattern
p) (NamedArg Pattern -> NamedArg Pattern)
-> NamedArg Pattern -> NamedArg Pattern
forall a b. (a -> b) -> a -> b
$ ArgInfo -> NamedArg Pattern -> NamedArg Pattern
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo (DBPatVar -> ArgInfo
varArgInfo DBPatVar
x) NamedArg Pattern
p
strip
:: Term
-> Type
-> [NamedArg A.Pattern]
-> [NamedArg DeBruijnPattern]
-> WriterT [ProblemEq] TCM [NamedArg A.Pattern]
strip :: Term
-> Type
-> [NamedArg Pattern]
-> [NamedArg DeBruijnPattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
strip Term
self Type
t [] qs :: [NamedArg DeBruijnPattern]
qs@(NamedArg DeBruijnPattern
_ : [NamedArg DeBruijnPattern]
_) = do
[Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.strip" Int
15 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
-> TCMT IO Doc -> WriterT [ProblemEq] (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
vcat
[ TCMT IO Doc
"strip (out of A.Patterns)"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"qs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> TCMT IO Doc)
-> [NamedArg DeBruijnPattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DeBruijnPattern -> m Doc
prettyTCM (DeBruijnPattern -> TCMT IO Doc)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
qs)
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"self=" 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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
self
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"t =" 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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
]
ps <- TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ ExpandHidden
-> [NamedArg Pattern] -> Type -> TCM [NamedArg Pattern]
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
MonadTrace m) =>
ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
insertImplicitPatternsT ExpandHidden
ExpandLast [] Type
t
if null ps then
typeError $ GenericError $ "Too few arguments given in with-clause"
else strip self t ps qs
strip Term
_ Type
_ [NamedArg Pattern]
ps [] = do
let implicit :: Pattern' e -> Bool
implicit (A.WildP{}) = Bool
True
implicit (A.ConP ConPatInfo
ci AmbiguousQName
_ NAPs e
_) = ConPatInfo -> ConOrigin
conPatOrigin ConPatInfo
ci ConOrigin -> ConOrigin -> Bool
forall a. Eq a => a -> a -> Bool
== ConOrigin
ConOSystem
implicit Pattern' e
_ = Bool
False
Bool
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((NamedArg Pattern -> Bool) -> [NamedArg Pattern] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern -> Bool
forall {e}. Pattern' e -> Bool
implicit (Pattern -> Bool)
-> (NamedArg Pattern -> Pattern) -> NamedArg Pattern -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg) [NamedArg Pattern]
ps) (WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ())
-> WriterT [ProblemEq] (TCMT IO) ()
-> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
TypeError -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> WriterT [ProblemEq] (TCMT IO) ())
-> TypeError -> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError ([Char] -> TypeError) -> [Char] -> TypeError
forall a b. (a -> b) -> a -> b
$ [Char]
"Too many arguments given in with-clause"
[NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. a -> WriterT [ProblemEq] (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
strip Term
self Type
t (NamedArg Pattern
p0 : [NamedArg Pattern]
ps) qs :: [NamedArg DeBruijnPattern]
qs@(NamedArg DeBruijnPattern
q : [NamedArg DeBruijnPattern]
_)
| A.AsP PatInfo
_ BindName
x Pattern
p <- NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p0 = do
(a, _) <- Type -> WriterT [ProblemEq] (TCMT IO) (Dom Type, Abs Type)
forall (m :: * -> *).
MonadReduce m =>
Type -> m (Dom Type, Abs Type)
mustBePi Type
t
let v = DeBruijnPattern -> Term
patternToTerm (NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NamedArg DeBruijnPattern
q)
tell [ProblemEq (A.VarP x) v a]
strip self t (fmap (p <$) p0 : ps) qs
strip Term
self Type
t ps0 :: [NamedArg Pattern]
ps0@(NamedArg Pattern
p0 : [NamedArg Pattern]
ps) qs0 :: [NamedArg DeBruijnPattern]
qs0@(NamedArg DeBruijnPattern
q : [NamedArg DeBruijnPattern]
qs) = do
p <- TCM (NamedArg Pattern)
-> WriterT [ProblemEq] (TCMT IO) (NamedArg Pattern)
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (NamedArg Pattern)
-> WriterT [ProblemEq] (TCMT IO) (NamedArg Pattern))
-> TCM (NamedArg Pattern)
-> WriterT [ProblemEq] (TCMT IO) (NamedArg Pattern)
forall a b. (a -> b) -> a -> b
$ ((Named NamedName Pattern -> TCMT IO (Named NamedName Pattern))
-> NamedArg Pattern -> TCM (NamedArg Pattern)
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 ((Named NamedName Pattern -> TCMT IO (Named NamedName Pattern))
-> NamedArg Pattern -> TCM (NamedArg Pattern))
-> ((Pattern -> TCMT IO Pattern)
-> Named NamedName Pattern -> TCMT IO (Named NamedName Pattern))
-> (Pattern -> TCMT IO Pattern)
-> NamedArg Pattern
-> TCM (NamedArg Pattern)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern -> TCMT IO Pattern)
-> Named NamedName Pattern -> TCMT IO (Named NamedName Pattern)
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) -> Named NamedName a -> f (Named NamedName b)
traverse) Pattern -> TCMT IO Pattern
forall (m :: * -> *).
(MonadError TCErr m, MonadTCEnv m, ReadTCState m, HasBuiltins m) =>
Pattern -> m Pattern
expandLitPattern NamedArg Pattern
p0
reportSDoc "tc.with.strip" 15 $ vcat
[ "strip"
, nest 2 $ "ps0 =" <+> fsep (punctuate comma $ map prettyA ps0)
, nest 2 $ "exp =" <+> prettyA p
, nest 2 $ "qs0 =" <+> fsep (punctuate comma $ map (prettyTCM . namedArg) qs0)
, nest 2 $ "self=" <+> prettyTCM self
, nest 2 $ "t =" <+> prettyTCM t
]
case namedArg q of
ProjP ProjOrigin
o QName
d -> case NamedArg Pattern -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
A.isProjP NamedArg Pattern
p of
Just (ProjOrigin
o', AmbQ List1 QName
ds) -> do
if ProjOrigin
o ProjOrigin -> ProjOrigin -> Bool
forall a. Eq a => a -> a -> Bool
/= ProjOrigin
o' then TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ ProjOrigin -> ProjOrigin -> TCM [NamedArg Pattern]
mismatchOrigin ProjOrigin
o ProjOrigin
o' else do
d <- TCM QName -> WriterT [ProblemEq] (TCMT IO) QName
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM QName -> WriterT [ProblemEq] (TCMT IO) QName)
-> TCM QName -> WriterT [ProblemEq] (TCMT IO) QName
forall a b. (a -> b) -> a -> b
$ QName -> TCM QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
d
found <- anyM ds $ \ QName
d' -> TCM Bool -> WriterT [ProblemEq] (TCMT IO) Bool
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> WriterT [ProblemEq] (TCMT IO) Bool)
-> TCM Bool -> WriterT [ProblemEq] (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ (QName -> Maybe QName
forall a. a -> Maybe a
Just QName
d Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe QName -> Bool)
-> (Maybe Projection -> Maybe QName) -> Maybe Projection -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Projection -> QName) -> Maybe Projection -> Maybe QName
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Projection -> QName
projOrig (Maybe Projection -> Bool)
-> TCMT IO (Maybe Projection) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isProjection QName
d'
if not found then mismatch else do
(self1, t1, ps) <- liftTCM $ do
t <- reduce t
(_, self1, t1) <- fromMaybe __IMPOSSIBLE__ <$> projectTyped self t o d
ps <- insertImplicitPatternsT ExpandLast ps t1
return (self1, t1, ps)
strip self1 t1 ps qs
Maybe (ProjOrigin, AmbiguousQName)
Nothing -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch
VarP PatternInfo
_ DBPatVar
x | A.DotP PatInfo
_ Expr
u <- NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p
, A.Var Name
y <- Expr -> Expr
unScope Expr
u -> do
(DBPatVar -> NamedArg Pattern -> NamedArg Pattern
setVarArgInfo DBPatVar
x (NamedArg Pattern -> Pattern -> NamedArg Pattern
forall a b. NamedArg a -> b -> NamedArg b
setNamedArg NamedArg Pattern
p (Pattern -> NamedArg Pattern) -> Pattern -> NamedArg Pattern
forall a b. (a -> b) -> a -> b
$ BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP (BindName -> Pattern) -> BindName -> Pattern
forall a b. (a -> b) -> a -> b
$ Name -> BindName
A.mkBindName Name
y) NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
:) ([NamedArg Pattern] -> [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse (Int -> Term
var (DBPatVar -> Int
dbPatVarIndex DBPatVar
x))
VarP PatternInfo
_ DBPatVar
x ->
(DBPatVar -> NamedArg Pattern -> NamedArg Pattern
setVarArgInfo DBPatVar
x NamedArg Pattern
p NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
:) ([NamedArg Pattern] -> [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse (Int -> Term
var (DBPatVar -> Int
dbPatVarIndex DBPatVar
x))
IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
x ->
(DBPatVar -> NamedArg Pattern -> NamedArg Pattern
setVarArgInfo DBPatVar
x NamedArg Pattern
p NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
:) ([NamedArg Pattern] -> [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse (Int -> Term
var (DBPatVar -> Int
dbPatVarIndex DBPatVar
x))
DefP{} -> TypeError -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> TypeError -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError ([Char] -> TypeError) -> [Char] -> TypeError
forall a b. (a -> b) -> a -> b
$ [Char]
"with clauses not supported in the presence of hcomp patterns"
DotP PatternInfo
i Term
v -> do
(a, _) <- Type -> WriterT [ProblemEq] (TCMT IO) (Dom Type, Abs Type)
forall (m :: * -> *).
MonadReduce m =>
Type -> m (Dom Type, Abs Type)
mustBePi Type
t
tell [ProblemEq (namedArg p) v a]
case v of
Var Int
x [] | PatOVar{} <- PatternInfo -> PatOrigin
patOrigin PatternInfo
i
-> (NamedArg Pattern
p NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
:) ([NamedArg Pattern] -> [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse (Int -> Term
var Int
x)
Term
_ -> (NamedArg Pattern -> NamedArg Pattern
makeWildP NamedArg Pattern
p NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
:) ([NamedArg Pattern] -> [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse Term
v
q' :: DeBruijnPattern
q'@(ConP ConHead
c ConPatternInfo
ci [NamedArg DeBruijnPattern]
qs') -> do
[Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.strip" Int
60 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
-> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"parent pattern is constructor " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c
(a, b) <- Type -> WriterT [ProblemEq] (TCMT IO) (Dom Type, Abs Type)
forall (m :: * -> *).
MonadReduce m =>
Type -> m (Dom Type, Abs Type)
mustBePi Type
t
Def d es <- liftTCM $ reduce (unEl $ unDom a)
let us = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
c <- either __IMPOSSIBLE__ (`withRangeOf` c) <$> do liftTCM $ getConForm $ conName c
case namedArg p of
A.DotP PatInfo
r Expr
e -> do
[ProblemEq] -> WriterT [ProblemEq] (TCMT IO) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq (PatInfo -> Expr -> Pattern
forall e. PatInfo -> e -> Pattern' e
A.DotP PatInfo
r Expr
e) (DeBruijnPattern -> Term
patternToTerm DeBruijnPattern
q') Dom Type
a]
ps' <-
case Expr -> AppView
appView Expr
e of
Application (A.Con (A.AmbQ List1 QName
cs')) [NamedArg Expr]
es -> do
cs' <- TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead]
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead])
-> TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead]
forall a b. (a -> b) -> a -> b
$ List1 (Either SigError ConHead) -> [ConHead]
forall a b. List1 (Either a b) -> [b]
List1.rights (List1 (Either SigError ConHead) -> [ConHead])
-> TCMT IO (List1 (Either SigError ConHead)) -> TCM [ConHead]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCM (Either SigError ConHead))
-> List1 QName -> TCMT IO (List1 (Either SigError ConHead))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM QName -> TCM (Either SigError ConHead)
getConForm List1 QName
cs'
unless (c `elem` cs') mismatch
return $ (map . fmap . fmap) (A.DotP r) es
AppView
_ -> [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. a -> WriterT [ProblemEq] (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> NamedArg Pattern)
-> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern -> Named NamedName Pattern
forall a name. a -> Named name a
unnamed (PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
forall a. Null a => a
empty) Named NamedName Pattern
-> NamedArg DeBruijnPattern -> NamedArg Pattern
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) [NamedArg DeBruijnPattern]
qs'
stripConP d us b c ConOCon qs' ps'
A.WildP{} -> do
let ps' :: [NamedArg Pattern]
ps' = (NamedArg DeBruijnPattern -> NamedArg Pattern)
-> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern -> Named NamedName Pattern
forall a name. a -> Named name a
unnamed (PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
forall a. Null a => a
empty) Named NamedName Pattern
-> NamedArg DeBruijnPattern -> NamedArg Pattern
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) [NamedArg DeBruijnPattern]
qs'
QName
-> Args
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
stripConP QName
d Args
us Abs Type
b ConHead
c ConOrigin
ConOCon [NamedArg DeBruijnPattern]
qs' [NamedArg Pattern]
ps'
A.VarP BindName
x -> do
[ProblemEq] -> WriterT [ProblemEq] (TCMT IO) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Pattern -> Term -> Dom Type -> ProblemEq
ProblemEq (BindName -> Pattern
forall e. BindName -> Pattern' e
A.VarP BindName
x) (DeBruijnPattern -> Term
patternToTerm DeBruijnPattern
q') Dom Type
a]
let ps' :: [NamedArg Pattern]
ps' = (NamedArg DeBruijnPattern -> NamedArg Pattern)
-> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern -> Named NamedName Pattern
forall a name. a -> Named name a
unnamed (PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
forall a. Null a => a
empty) Named NamedName Pattern
-> NamedArg DeBruijnPattern -> NamedArg Pattern
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) [NamedArg DeBruijnPattern]
qs'
QName
-> Args
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
stripConP QName
d Args
us Abs Type
b ConHead
c ConOrigin
ConOCon [NamedArg DeBruijnPattern]
qs' [NamedArg Pattern]
ps'
A.ConP ConPatInfo
_ (A.AmbQ List1 QName
cs') [NamedArg Pattern]
ps' -> do
cs' <- TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead]
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead])
-> TCM [ConHead] -> WriterT [ProblemEq] (TCMT IO) [ConHead]
forall a b. (a -> b) -> a -> b
$ List1 (Either SigError ConHead) -> [ConHead]
forall a b. List1 (Either a b) -> [b]
List1.rights (List1 (Either SigError ConHead) -> [ConHead])
-> TCMT IO (List1 (Either SigError ConHead)) -> TCM [ConHead]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCM (Either SigError ConHead))
-> List1 QName -> TCMT IO (List1 (Either SigError ConHead))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM QName -> TCM (Either SigError ConHead)
getConForm List1 QName
cs'
unless (c `elem` cs') mismatch
stripConP d us b c ConOCon qs' ps'
A.RecP ConPatInfo
_ [FieldAssignment' Pattern]
fs -> WriterT [ProblemEq] (TCMT IO) (Maybe RecordData)
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
-> (RecordData -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (TCM (Maybe RecordData)
-> WriterT [ProblemEq] (TCMT IO) (Maybe RecordData)
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe RecordData)
-> WriterT [ProblemEq] (TCMT IO) (Maybe RecordData))
-> TCM (Maybe RecordData)
-> WriterT [ProblemEq] (TCMT IO) (Maybe RecordData)
forall a b. (a -> b) -> a -> b
$ QName -> TCM (Maybe RecordData)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe RecordData)
isRecord QName
d) WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch ((RecordData -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> (RecordData -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ \ RecordData
def -> do
ps' <- TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. TCM a -> WriterT [ProblemEq] (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> TCM [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ QName
-> (Name -> Pattern)
-> [FieldAssignment' Pattern]
-> [Arg Name]
-> TCM [NamedArg Pattern]
forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsFail QName
d (Pattern -> Name -> Pattern
forall a b. a -> b -> a
const (Pattern -> Name -> Pattern) -> Pattern -> Name -> Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
forall a. Null a => a
empty) [FieldAssignment' Pattern]
fs
((Dom Name -> Arg Name) -> [Dom Name] -> [Arg Name]
forall a b. (a -> b) -> [a] -> [b]
map Dom Name -> Arg Name
forall t a. Dom' t a -> Arg a
argFromDom ([Dom Name] -> [Arg Name]) -> [Dom Name] -> [Arg Name]
forall a b. (a -> b) -> a -> b
$ RecordData -> [Dom Name]
recordFieldNames RecordData
def)
stripConP d us b c ConORec qs' ps'
p :: Pattern
p@(A.PatternSynP PatInfo
pi' AmbiguousQName
c' [NamedArg Pattern]
ps') -> do
[Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
10 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
-> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"stripWithClausePatterns: encountered pattern synonym " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__
Pattern
p -> do
[Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.strip" Int
60 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
-> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
[Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"with clause pattern is " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Pattern -> [Char]
forall a. Show a => a -> [Char]
show Pattern
p
WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch
LitP PatternInfo
_ Literal
lit -> case NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p of
A.LitP PatInfo
_ Literal
lit' | Literal
lit Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
lit' -> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse (Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
lit
A.WildP{} -> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse (Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern])
-> Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
lit
p :: Pattern
p@(A.PatternSynP PatInfo
pi' AmbiguousQName
c' [NamedArg Pattern
ps']) -> do
[Char] -> Int -> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
10 (TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ())
-> TCMT IO Doc -> WriterT [ProblemEq] (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"stripWithClausePatterns: encountered pattern synonym " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__
Pattern
_ -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch
where
recurse :: Term -> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
recurse Term
v = do
let piOrPathApplyM :: Type -> Term -> m (Elims, Type)
piOrPathApplyM Type
t Term
v = do
(TelV tel t', bs) <- Int -> Type -> m (TelV Type, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundaryP Int
1 Type
t
unless (size tel == 1) $ __IMPOSSIBLE__
return (teleElims tel bs, subst 0 v t')
(e, t') <- Type -> Term -> WriterT [ProblemEq] (TCMT IO) (Elims, Type)
forall {m :: * -> *}. PureTCM m => Type -> Term -> m (Elims, Type)
piOrPathApplyM Type
t Term
v
strip (self `applyE` e) t' ps qs
mismatch :: forall m a. (MonadAddContext m, MonadTCError m) => m a
mismatch :: forall (m :: * -> *) a. (MonadAddContext m, MonadTCError m) => m a
mismatch = Telescope -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$
Pattern -> NamedArg DeBruijnPattern -> TypeError
WithClausePatternMismatch (NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p0) NamedArg DeBruijnPattern
q
mismatchOrigin :: ProjOrigin -> ProjOrigin -> TCM [NamedArg Pattern]
mismatchOrigin ProjOrigin
o ProjOrigin
o' = Telescope -> TCM [NamedArg Pattern] -> TCM [NamedArg Pattern]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta (TCM [NamedArg Pattern] -> TCM [NamedArg Pattern])
-> (Doc -> TCM [NamedArg Pattern]) -> Doc -> TCM [NamedArg Pattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TCM [NamedArg Pattern]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM [NamedArg Pattern])
-> (Doc -> TypeError) -> Doc -> TCM [NamedArg Pattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM [NamedArg Pattern])
-> TCMT IO Doc -> TCM [NamedArg Pattern]
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
[ TCMT IO Doc
"With clause pattern"
, NamedArg Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p0
, TCMT IO Doc
"is not an instance of its parent pattern"
, [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.fsep ([Doc] -> Doc) -> TCMT IO [Doc] -> TCMT IO Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg DeBruijnPattern] -> TCMT IO [Doc]
forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m [Doc]
prettyTCMPatterns [NamedArg DeBruijnPattern
q]
, [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"since the parent pattern is " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ProjOrigin -> [Char]
forall {a}. IsString a => ProjOrigin -> a
prettyProjOrigin ProjOrigin
o [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
" and the with clause pattern is " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ProjOrigin -> [Char]
forall {a}. IsString a => ProjOrigin -> a
prettyProjOrigin ProjOrigin
o'
]
prettyProjOrigin :: ProjOrigin -> a
prettyProjOrigin ProjOrigin
ProjPrefix = a
"a prefix projection"
prettyProjOrigin ProjOrigin
ProjPostfix = a
"a postfix projection"
prettyProjOrigin ProjOrigin
ProjSystem = a
forall a. HasCallStack => a
__IMPOSSIBLE__
makeWildP :: NamedArg A.Pattern -> NamedArg A.Pattern
makeWildP :: NamedArg Pattern -> NamedArg Pattern
makeWildP = (Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg ((Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern)
-> (Pattern -> Pattern) -> NamedArg Pattern -> NamedArg Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern -> Pattern
forall a b. a -> b -> a
const (Pattern -> Pattern -> Pattern) -> Pattern -> Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange
stripConP
:: QName
-> [Arg Term]
-> Abs Type
-> ConHead
-> ConInfo
-> [NamedArg DeBruijnPattern]
-> [NamedArg A.Pattern]
-> WriterT [ProblemEq] TCM [NamedArg A.Pattern]
stripConP :: QName
-> Args
-> Abs Type
-> ConHead
-> ConOrigin
-> [NamedArg DeBruijnPattern]
-> [NamedArg Pattern]
-> WriterT [ProblemEq] (TCMT IO) [NamedArg Pattern]
stripConP QName
d Args
us Abs Type
b ConHead
c ConOrigin
ci [NamedArg DeBruijnPattern]
qs' [NamedArg Pattern]
ps' = do
Defn {defType = ct, theDef = Constructor{conPars = np}} <- ConHead -> WriterT [ProblemEq] (TCMT IO) Definition
forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo ConHead
c
let ct' = Type
ct Type -> Args -> Type
`piApply` Int -> Args -> Args
forall a. Int -> [a] -> [a]
take Int
np Args
us
TelV tel' _ <- liftTCM $ telViewPath ct'
reportSDoc "tc.with.strip" 20 $
vcat [ "ct = " <+> prettyTCM ct
, "ct' = " <+> prettyTCM ct'
, "np = " <+> text (show np)
, "us = " <+> prettyList (map prettyTCM us)
, "us' = " <+> prettyList (map prettyTCM $ take np us)
]
let v = ConHead -> ConOrigin -> Elims -> Term
Con ConHead
c ConOrigin
ci [ Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Int -> Term
var Int
i) | (Int
i, Arg ArgInfo
info Named NamedName DeBruijnPattern
_) <- [Int]
-> [NamedArg DeBruijnPattern] -> [(Int, NamedArg DeBruijnPattern)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> Int
forall a. Sized a => a -> Int
size [NamedArg DeBruijnPattern]
qs') [NamedArg DeBruijnPattern]
qs' ]
t' = Telescope
tel' Telescope -> Type -> Type
forall t. Abstract t => Telescope -> t -> t
`abstract` Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
absApp (Int -> Abs Type -> Abs Type
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel') Abs Type
b) Term
SubstArg Type
v
self' = Telescope
tel' Telescope -> Term -> Term
forall t. Abstract t => Telescope -> t -> t
`abstract` Term -> Term -> Term
forall t. Apply t => t -> Term -> t
apply1 (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel') Term
self) Term
v
reportSDoc "tc.with.strip" 15 $ sep
[ "inserting implicit"
, nest 2 $ prettyList $ map prettyA (ps' ++ ps)
, nest 2 $ ":" <+> prettyTCM t'
]
psi' <- liftTCM $ insertImplicitPatterns ExpandLast ps' tel'
unless (size psi' == size tel') $ typeError $
WrongNumberOfConstructorArguments (conName c) (size tel') (size psi')
psi <- liftTCM $ insertImplicitPatternsT ExpandLast (psi' ++ ps) t'
strip self' t' psi (qs' ++ qs)
withDisplayForm
:: QName
-> QName
-> Telescope
-> Telescope
-> Nat
-> [NamedArg DeBruijnPattern]
-> Permutation
-> Permutation
-> TCM DisplayForm
withDisplayForm :: QName
-> QName
-> Telescope
-> Telescope
-> Int
-> [NamedArg DeBruijnPattern]
-> Permutation
-> Permutation
-> TCM DisplayForm
withDisplayForm QName
f QName
aux Telescope
delta1 Telescope
delta2 Int
n [NamedArg DeBruijnPattern]
qs perm :: Permutation
perm@(Perm Int
m [Int]
_) Permutation
lhsPerm = do
let arity0 :: Int
arity0 = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta2
topArgs <- Int -> Args -> Args
forall a. Subst a => Int -> a -> a
raise Int
arity0 (Args -> Args) -> TCM Args -> TCM Args
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
let top = Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
topArgs
arity = Int
arity0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
top
wild <- freshNoName_ <&> \ Name
x -> QName -> Elims -> Term
Def (Name -> QName
qualify_ Name
x) []
let
tqs0 = [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm]
patsToElims [NamedArg DeBruijnPattern]
qs
(ys0, ys1) = splitAt (size delta1) $ permute perm $ downFrom m
ys = [Maybe Int] -> [Maybe Int]
forall a. [a] -> [a]
reverse ((Int -> Maybe Int) -> [Int] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Maybe Int
forall a. a -> Maybe a
Just [Int]
ys0 [Maybe Int] -> [Maybe Int] -> [Maybe Int]
forall a. [a] -> [a] -> [a]
++ Int -> Maybe Int -> [Maybe Int]
forall a. Int -> a -> [a]
replicate Int
n Maybe Int
forall a. Maybe a
Nothing [Maybe Int] -> [Maybe Int] -> [Maybe Int]
forall a. [a] -> [a] -> [a]
++ (Int -> Maybe Int) -> [Int] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Maybe Int
forall a. a -> Maybe a
Just [Int]
ys1)
[Maybe Int] -> [Maybe Int] -> [Maybe Int]
forall a. [a] -> [a] -> [a]
++ (Int -> Maybe Int) -> [Int] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (Int -> Int) -> Int -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+)) [Int
0..Int
topInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
rho = Int -> [Maybe Int] -> Term -> Substitution' Term
sub Int
top [Maybe Int]
ys Term
wild
tqs = Substitution' (SubstArg [Elim' DisplayTerm])
-> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg [Elim' DisplayTerm])
rho [Elim' DisplayTerm]
tqs0
es = (Arg Term -> Elim' DisplayTerm) -> Args -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Arg DisplayTerm -> Elim' DisplayTerm
forall a. Arg a -> Elim' a
Apply (Arg DisplayTerm -> Elim' DisplayTerm)
-> (Arg Term -> Arg DisplayTerm) -> Arg Term -> Elim' DisplayTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> DisplayTerm) -> Arg Term -> Arg DisplayTerm
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> DisplayTerm
DTerm) Args
topArgs [Elim' DisplayTerm] -> [Elim' DisplayTerm] -> [Elim' DisplayTerm]
forall a. [a] -> [a] -> [a]
++ [Elim' DisplayTerm]
tqs
withArgs = (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
var ([Int] -> [Term]) -> [Int] -> [Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take Int
n ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n
dt = DisplayTerm -> [DisplayTerm] -> Elims -> DisplayTerm
DWithApp (QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
f [Elim' DisplayTerm]
es) ((Term -> DisplayTerm) -> [Term] -> [DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map Term -> DisplayTerm
DTerm [Term]
withArgs) []
let display = Int -> Elims -> DisplayTerm -> DisplayForm
Display Int
arity [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i | Int
i <- Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
arity] DisplayTerm
dt
let addFullCtx = Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta1
(TCMT IO Doc -> TCMT IO Doc)
-> (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TCMT IO Doc -> [[Char]] -> TCMT IO Doc)
-> [[Char]] -> TCMT IO Doc -> TCMT IO Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip (([Char] -> TCMT IO Doc -> TCMT IO Doc)
-> TCMT IO Doc -> [[Char]] -> TCMT IO Doc
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [Char] -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => [Char] -> m a -> m a
addContext) ([Int] -> (Int -> [Char]) -> [[Char]]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
for [Int
1..Int
n] ((Int -> [Char]) -> [[Char]]) -> (Int -> [Char]) -> [[Char]]
forall a b. (a -> b) -> a -> b
$ \ Int
i -> [Char]
"w" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)
(TCMT IO Doc -> TCMT IO Doc)
-> (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta2
reportSDoc "tc.with.display" 20 $ vcat
[ "withDisplayForm"
, nest 2 $ vcat
[ "f =" <+> text (prettyShow f)
, "aux =" <+> text (prettyShow aux)
, "delta1 =" <+> prettyTCM delta1
, "delta2 =" <+> do addContext delta1 $ prettyTCM delta2
, "n =" <+> text (show n)
, "perm =" <+> text (show perm)
, "top =" <+> do addFullCtx $ prettyTCM topArgs
, "qs =" <+> prettyList (map pretty qs)
, "qsToTm =" <+> prettyTCM tqs0
, "ys =" <+> text (show ys)
, "rho =" <+> text (prettyShow rho)
, "qs[rho]=" <+> do addFullCtx $ prettyTCM tqs
, "dt =" <+> do addFullCtx $ prettyTCM dt
]
]
reportSDoc "tc.with.display" 70 $ nest 2 $ vcat
[ "raw =" <+> text (show display)
]
return display
where
sub :: Int -> [Maybe Int] -> Term -> Substitution' Term
sub Int
top [Maybe Int]
ys Term
wild = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
term [Int
0 .. Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
top Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
where
term :: Int -> Term
term Int
i = Term -> (Int -> Term) -> Maybe Int -> Term
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Term
wild Int -> Term
var (Maybe Int -> Term) -> Maybe Int -> Term
forall a b. (a -> b) -> a -> b
$ Maybe Int -> [Maybe Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i) [Maybe Int]
ys
patsToElims :: [NamedArg DeBruijnPattern] -> [I.Elim' DisplayTerm]
patsToElims :: [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm]
patsToElims = (NamedArg DeBruijnPattern -> Elim' DisplayTerm)
-> [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg DeBruijnPattern -> Elim' DisplayTerm)
-> [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm])
-> (NamedArg DeBruijnPattern -> Elim' DisplayTerm)
-> [NamedArg DeBruijnPattern]
-> [Elim' DisplayTerm]
forall a b. (a -> b) -> a -> b
$ Arg DeBruijnPattern -> Elim' DisplayTerm
toElim (Arg DeBruijnPattern -> Elim' DisplayTerm)
-> (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Elim' DisplayTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing
where
toElim :: Arg DeBruijnPattern -> I.Elim' DisplayTerm
toElim :: Arg DeBruijnPattern -> Elim' DisplayTerm
toElim (Arg ArgInfo
ai DeBruijnPattern
p) = case DeBruijnPattern
p of
ProjP ProjOrigin
o QName
d -> ProjOrigin -> QName -> Elim' DisplayTerm
forall a. ProjOrigin -> QName -> Elim' a
I.Proj ProjOrigin
o QName
d
DeBruijnPattern
p -> Arg DisplayTerm -> Elim' DisplayTerm
forall a. Arg a -> Elim' a
I.Apply (Arg DisplayTerm -> Elim' DisplayTerm)
-> Arg DisplayTerm -> Elim' DisplayTerm
forall a b. (a -> b) -> a -> b
$ ArgInfo -> DisplayTerm -> Arg DisplayTerm
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (DisplayTerm -> Arg DisplayTerm) -> DisplayTerm -> Arg DisplayTerm
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> DisplayTerm
toTerm DeBruijnPattern
p
toTerms :: [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
toTerms :: [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
toTerms = (NamedArg DeBruijnPattern -> Arg DisplayTerm)
-> [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg DeBruijnPattern -> Arg DisplayTerm)
-> [NamedArg DeBruijnPattern] -> [Arg DisplayTerm])
-> (NamedArg DeBruijnPattern -> Arg DisplayTerm)
-> [NamedArg DeBruijnPattern]
-> [Arg DisplayTerm]
forall a b. (a -> b) -> a -> b
$ (Named NamedName DeBruijnPattern -> DisplayTerm)
-> NamedArg DeBruijnPattern -> Arg DisplayTerm
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName DeBruijnPattern -> DisplayTerm)
-> NamedArg DeBruijnPattern -> Arg DisplayTerm)
-> (Named NamedName DeBruijnPattern -> DisplayTerm)
-> NamedArg DeBruijnPattern
-> Arg DisplayTerm
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> DisplayTerm
toTerm (DeBruijnPattern -> DisplayTerm)
-> (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> Named NamedName DeBruijnPattern
-> DisplayTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing
toTerm :: DeBruijnPattern -> DisplayTerm
toTerm :: DeBruijnPattern -> DisplayTerm
toTerm DeBruijnPattern
p = case PatternInfo -> PatOrigin
patOrigin (PatternInfo -> PatOrigin) -> PatternInfo -> PatOrigin
forall a b. (a -> b) -> a -> b
$ PatternInfo -> Maybe PatternInfo -> PatternInfo
forall a. a -> Maybe a -> a
fromMaybe PatternInfo
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe PatternInfo -> PatternInfo)
-> Maybe PatternInfo -> PatternInfo
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> Maybe PatternInfo
forall x. Pattern' x -> Maybe PatternInfo
patternInfo DeBruijnPattern
p of
PatOrigin
PatOSystem -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
PatOrigin
PatOSplit -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
PatOVar{} -> DeBruijnPattern -> DisplayTerm
toVarOrDot DeBruijnPattern
p
PatOrigin
PatODot -> Term -> DisplayTerm
DDot (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> Term
patternToTerm DeBruijnPattern
p
PatOrigin
PatOWild -> DeBruijnPattern -> DisplayTerm
toVarOrDot DeBruijnPattern
p
PatOrigin
PatOCon -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
PatOrigin
PatORec -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
PatOrigin
PatOLit -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
PatOrigin
PatOAbsurd -> DeBruijnPattern -> DisplayTerm
toDisplayPattern DeBruijnPattern
p
toDisplayPattern :: DeBruijnPattern -> DisplayTerm
toDisplayPattern :: DeBruijnPattern -> DisplayTerm
toDisplayPattern = \case
IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
x -> Term -> DisplayTerm
DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x
ProjP ProjOrigin
_ QName
d -> DisplayTerm
forall a. HasCallStack => a
__IMPOSSIBLE__
VarP PatternInfo
i DBPatVar
x -> Term -> DisplayTerm
DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x
DotP PatternInfo
i Term
t -> Term -> DisplayTerm
DDot (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Term
t
p :: DeBruijnPattern
p@(ConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps) -> ConHead -> ConOrigin -> [Arg DisplayTerm] -> DisplayTerm
DCon ConHead
c (ConPatternInfo -> ConOrigin
fromConPatternInfo ConPatternInfo
cpi) ([Arg DisplayTerm] -> DisplayTerm)
-> [Arg DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
toTerms [NamedArg DeBruijnPattern]
ps
LitP PatternInfo
i Literal
l -> Term -> DisplayTerm
DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit Literal
l
DefP PatternInfo
_ QName
q [NamedArg DeBruijnPattern]
ps -> QName -> [Elim' DisplayTerm] -> DisplayTerm
DDef QName
q ([Elim' DisplayTerm] -> DisplayTerm)
-> [Elim' DisplayTerm] -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ (Arg DisplayTerm -> Elim' DisplayTerm)
-> [Arg DisplayTerm] -> [Elim' DisplayTerm]
forall a b. (a -> b) -> [a] -> [b]
map Arg DisplayTerm -> Elim' DisplayTerm
forall a. Arg a -> Elim' a
Apply ([Arg DisplayTerm] -> [Elim' DisplayTerm])
-> [Arg DisplayTerm] -> [Elim' DisplayTerm]
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> [Arg DisplayTerm]
toTerms [NamedArg DeBruijnPattern]
ps
toVarOrDot :: DeBruijnPattern -> DisplayTerm
toVarOrDot :: DeBruijnPattern -> DisplayTerm
toVarOrDot DeBruijnPattern
p = case DeBruijnPattern -> Term
patternToTerm DeBruijnPattern
p of
Var Int
i [] -> Term -> DisplayTerm
DTerm (Term -> DisplayTerm) -> Term -> DisplayTerm
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i
Term
t -> Term -> DisplayTerm
DDot Term
t