{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.LHS
( checkLeftHandSide
, LHSResult(..)
, bindAsPatterns
, IsFlexiblePattern(..)
, checkSortOfSplitVar
) where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ( (<>), mapM, null, sequence )
#else
import Prelude hiding ( mapM, null, sequence )
#endif
import Data.Maybe
import Control.Arrow (left)
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer hiding ((<>))
import Control.Monad.Trans.Maybe
import Data.Either (partitionEithers)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.List (delete, sortBy, stripPrefix, (\\), findIndex)
import qualified Data.List as List
import Data.Monoid ( Monoid, mempty, mappend )
import Data.Semigroup ( Semigroup )
import qualified Data.Semigroup as Semigroup
import Data.Map (Map)
import qualified Data.Map as Map
import Agda.Interaction.Highlighting.Generate (storeDisambiguatedName, disambiguateRecordFields)
import Agda.Interaction.Options
import Agda.Interaction.Options.Lenses
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Abstract (IsProjP(..))
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views (asView, deepUnscope)
import Agda.Syntax.Concrete (FieldAssignment'(..),NameInScope(..),LensInScope(..))
import Agda.Syntax.Common as Common
import Agda.Syntax.Info as A
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (litType, constructorForm)
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.CheckInternal (checkInternal)
import Agda.TypeChecking.Datatypes hiding (isDataOrRecordType)
import Agda.TypeChecking.Errors (dropTopLevelModule)
import Agda.TypeChecking.Irrelevance
import {-# SOURCE #-} Agda.TypeChecking.Empty
import Agda.TypeChecking.Forcing
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records hiding (getRecordConstructor)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Monad.Builtin
import {-# SOURCE #-} Agda.TypeChecking.Rules.Term (checkExpr)
import Agda.TypeChecking.Rules.LHS.Problem
import Agda.TypeChecking.Rules.LHS.ProblemRest
import Agda.TypeChecking.Rules.LHS.Unify
import Agda.TypeChecking.Rules.LHS.Implicit
import Agda.TypeChecking.Rules.Data
import Agda.Utils.Except (MonadError(..), ExceptT, runExceptT)
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.NonemptyList
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
flexiblePatterns :: [NamedArg A.Pattern] -> TCM FlexibleVars
flexiblePatterns nps = do
forMaybeM (zip (downFrom $ length nps) nps) $ \ (i, Arg ai p) -> do
runMaybeT $ (\ f -> FlexibleVar (getHiding ai) (getOrigin ai) f (Just i) i) <$> maybeFlexiblePattern p
class IsFlexiblePattern a where
maybeFlexiblePattern :: a -> MaybeT TCM FlexibleVarKind
isFlexiblePattern :: a -> TCM Bool
isFlexiblePattern p =
maybe False notOtherFlex <$> runMaybeT (maybeFlexiblePattern p)
where
notOtherFlex = \case
RecordFlex fls -> all notOtherFlex fls
ImplicitFlex -> True
DotFlex -> True
OtherFlex -> False
instance IsFlexiblePattern A.Pattern where
maybeFlexiblePattern p = do
reportSDoc "tc.lhs.flex" 30 $ "maybeFlexiblePattern" <+> prettyA p
reportSDoc "tc.lhs.flex" 60 $ "maybeFlexiblePattern (raw) " <+> (text . show . deepUnscope) p
case p of
A.DotP{} -> return DotFlex
A.VarP{} -> return ImplicitFlex
A.WildP{} -> return ImplicitFlex
A.AsP _ _ p -> maybeFlexiblePattern p
A.ConP _ cs qs | Just c <- getUnambiguous cs ->
ifM (isNothing <$> isRecordConstructor c) (return OtherFlex)
(maybeFlexiblePattern qs)
A.LitP{} -> return OtherFlex
_ -> mzero
instance IsFlexiblePattern (I.Pattern' a) where
maybeFlexiblePattern p =
case p of
I.DotP{} -> return DotFlex
I.ConP _ i ps
| Just PatOSystem <- conPRecord i -> return ImplicitFlex
| Just _ <- conPRecord i -> maybeFlexiblePattern ps
| otherwise -> mzero
I.VarP{} -> mzero
I.LitP{} -> mzero
I.ProjP{} -> mzero
I.IApplyP{} -> mzero
I.DefP{} -> mzero
instance IsFlexiblePattern a => IsFlexiblePattern [a] where
maybeFlexiblePattern ps = RecordFlex <$> mapM maybeFlexiblePattern ps
instance IsFlexiblePattern a => IsFlexiblePattern (Arg a) where
maybeFlexiblePattern = maybeFlexiblePattern . unArg
instance IsFlexiblePattern a => IsFlexiblePattern (Common.Named name a) where
maybeFlexiblePattern = maybeFlexiblePattern . namedThing
updateProblemEqs
:: [ProblemEq] -> TCM [ProblemEq]
updateProblemEqs eqs = do
reportSDoc "tc.lhs.top" 20 $ vcat
[ "updateProblem: equations to update"
, nest 2 $ if null eqs then "(none)" else vcat $ map prettyTCM eqs
]
eqs' <- updates eqs
reportSDoc "tc.lhs.top" 20 $ vcat
[ "updateProblem: new equations"
, nest 2 $ if null eqs' then "(none)" else vcat $ map prettyTCM eqs'
]
return eqs'
where
updates :: [ProblemEq] -> TCM [ProblemEq]
updates = concat <.> traverse update
update :: ProblemEq -> TCM [ProblemEq]
update eq@(ProblemEq A.WildP{} _ _) = return []
update eq@(ProblemEq p@A.ProjP{} _ _) = typeError $ IllformedProjectionPattern p
update eq@(ProblemEq p v a) = reduce v >>= constructorForm >>= \case
Con c ci es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
contype <- getFullyAppliedConType c =<< reduce (unDom a)
caseMaybe contype (return [eq]) $ \((d,_,pars),b) -> do
TelV ctel _ <- telViewPath b
let bs = instTel ctel (map unArg vs)
p <- expandLitPattern p
case p of
A.AsP info x p' ->
(ProblemEq (A.VarP x) v a :) <$> update (ProblemEq p' v a)
A.ConP cpi ambC ps -> do
(c',_) <- disambiguateConstructor ambC d pars
if conName c /= conName c' then return [eq] else do
ps <- insertImplicitPatterns ExpandLast ps ctel
reportSDoc "tc.lhs.imp" 20 $
"insertImplicitPatternsT returned" <+> fsep (map prettyA ps)
let checkArgs [] [] = return ()
checkArgs (p : ps) (v : vs)
| getHiding p == getHiding v = checkArgs ps vs
| otherwise = setCurrentRange p $ genericDocError =<< do
fsep $ pwords ("Expected an " ++ which (getHiding v) ++ " argument " ++
"instead of " ++ which (getHiding p) ++ " argument") ++
[ prettyA p ]
where which NotHidden = "explicit"
which Hidden = "implicit"
which Instance{} = "instance"
checkArgs [] vs = genericDocError =<< do
fsep $ pwords "Too few arguments to constructor" ++ [prettyTCM c <> ","] ++
pwords ("expected " ++ show n ++ " more explicit " ++ arguments)
where n = length (filter visible vs)
arguments | n == 1 = "argument"
| otherwise = "arguments"
checkArgs (p : _) [] = setCurrentRange p $ genericDocError =<< do
fsep $ pwords "Too many arguments to constructor" ++ [prettyTCM c]
checkArgs ps vs
updates $ zipWith3 ProblemEq (map namedArg ps) (map unArg vs) bs
A.RecP pi fs -> do
axs <- recFields . theDef <$> getConstInfo d
disambiguateRecordFields (map _nameFieldA fs) (map unArg axs)
let cxs = map (fmap (nameConcrete . qnameName)) axs
ps <- insertMissingFields d (const $ A.WildP patNoRange) fs cxs
ps <- insertImplicitPatterns ExpandLast ps ctel
let eqs = zipWith3 ProblemEq (map namedArg ps) (map unArg vs) bs
updates eqs
_ -> return [eq]
Lit l | A.LitP l' <- p , l == l' -> return []
_ | A.EqualP{} <- p -> do
itisone <- liftTCM primItIsOne
ifM (tryConversion $ equalTerm (unDom a) v itisone) (return []) (return [eq])
_ -> return [eq]
instTel :: Telescope -> [Term] -> [Dom Type]
instTel EmptyTel _ = []
instTel (ExtendTel arg tel) (u : us) = arg : instTel (absApp tel u) us
instTel ExtendTel{} [] = __IMPOSSIBLE__
isSolvedProblem :: Problem a -> Bool
isSolvedProblem problem = null (problem ^. problemRestPats) &&
problemAllVariables problem
problemAllVariables :: Problem a -> Bool
problemAllVariables problem =
all (isSolved . snd . asView) $
map namedArg (problem ^. problemRestPats) ++ problemInPats problem
where
isSolved A.ConP{} = False
isSolved A.LitP{} = False
isSolved A.RecP{} = False
isSolved A.VarP{} = True
isSolved A.WildP{} = True
isSolved A.DotP{} = True
isSolved A.AbsurdP{} = True
isSolved A.ProjP{} = __IMPOSSIBLE__
isSolved A.DefP{} = __IMPOSSIBLE__
isSolved A.AsP{} = __IMPOSSIBLE__
isSolved A.PatternSynP{} = __IMPOSSIBLE__
isSolved A.EqualP{} = False
isSolved A.WithP{} = __IMPOSSIBLE__
noShadowingOfConstructors
:: Call
-> [ProblemEq] -> TCM ()
noShadowingOfConstructors mkCall eqs =
traceCall mkCall $ mapM_ noShadowing eqs
where
noShadowing (ProblemEq p _ (Dom{domInfo = info, unDom = El _ a})) = case snd $ asView p of
A.WildP {} -> return ()
A.AbsurdP {} -> return ()
A.DotP {} -> return ()
A.EqualP {} -> return ()
A.ConP {} -> __IMPOSSIBLE__
A.RecP {} -> __IMPOSSIBLE__
A.ProjP {} -> __IMPOSSIBLE__
A.DefP {} -> __IMPOSSIBLE__
A.AsP {} -> __IMPOSSIBLE__
A.LitP {} -> __IMPOSSIBLE__
A.PatternSynP {} -> __IMPOSSIBLE__
A.WithP {} -> __IMPOSSIBLE__
A.VarP (A.BindName x) -> when (getOrigin info == UserWritten) $ do
reportSDoc "tc.lhs.shadow" 30 $ vcat
[ text $ "checking whether pattern variable " ++ prettyShow x ++ " shadows a constructor"
, nest 2 $ "type of variable =" <+> prettyTCM a
, nest 2 $ "position of variable =" <+> (text . show) (getRange x)
]
reportSDoc "tc.lhs.shadow" 70 $ nest 2 $ "a =" <+> pretty a
a <- reduce a
case a of
Def t _ -> do
d <- theDef <$> getConstInfo t
case d of
Datatype { dataCons = cs } -> do
case filter ((A.nameConcrete x ==) . A.nameConcrete . A.qnameName) cs of
[] -> return ()
(c : _) -> setCurrentRange x $
typeError $ PatternShadowsConstructor (nameConcrete x) c
AbstractDefn{} -> return ()
Axiom {} -> return ()
DataOrRecSig{} -> return ()
Function {} -> return ()
Record {} -> return ()
Constructor {} -> __IMPOSSIBLE__
GeneralizableVar{} -> __IMPOSSIBLE__
Primitive {} -> return ()
Var {} -> return ()
Pi {} -> return ()
Sort {} -> return ()
MetaV {} -> return ()
Lam {} -> __IMPOSSIBLE__
Lit {} -> __IMPOSSIBLE__
Level {} -> __IMPOSSIBLE__
Con {} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
Dummy s -> __IMPOSSIBLE_VERBOSE__ s
checkDotPattern :: DotPattern -> TCM ()
checkDotPattern (Dot e v (Dom{domInfo = info, unDom = a})) =
traceCall (CheckDotPattern e v) $ do
reportSDoc "tc.lhs.dot" 15 $
sep [ "checking dot pattern"
, nest 2 $ prettyA e
, nest 2 $ "=" <+> prettyTCM v
, nest 2 $ ":" <+> prettyTCM a
]
applyModalityToContext info $ do
u <- checkExpr e a
reportSDoc "tc.lhs.dot" 50 $
sep [ "equalTerm"
, nest 2 $ pretty a
, nest 2 $ pretty u
, nest 2 $ pretty v
]
noConstraints $ equalTerm a u v
checkAbsurdPattern :: AbsurdPattern -> TCM ()
checkAbsurdPattern (Absurd r a) = ensureEmptyType r a
data LeftoverPatterns = LeftoverPatterns
{ patternVariables :: IntMap [A.Name]
, asPatterns :: [AsBinding]
, dotPatterns :: [DotPattern]
, absurdPatterns :: [AbsurdPattern]
, otherPatterns :: [A.Pattern]
}
instance Semigroup LeftoverPatterns where
x <> y = LeftoverPatterns
{ patternVariables = IntMap.unionWith (++) (patternVariables x) (patternVariables y)
, asPatterns = asPatterns x ++ asPatterns y
, dotPatterns = dotPatterns x ++ dotPatterns y
, absurdPatterns = absurdPatterns x ++ absurdPatterns y
, otherPatterns = otherPatterns x ++ otherPatterns y
}
instance Monoid LeftoverPatterns where
mempty = LeftoverPatterns empty [] [] [] []
mappend = (Semigroup.<>)
getLeftoverPatterns :: [ProblemEq] -> TCM LeftoverPatterns
getLeftoverPatterns eqs = do
reportSDoc "tc.lhs.top" 30 $ "classifying leftover patterns"
mconcat <$> mapM getLeftoverPattern eqs
where
patternVariable x i = LeftoverPatterns (singleton (i,[x])) [] [] [] []
asPattern x v a = LeftoverPatterns empty [AsB x v (unDom a)] [] [] []
dotPattern e v a = LeftoverPatterns empty [] [Dot e v a] [] []
absurdPattern info a = LeftoverPatterns empty [] [] [Absurd info a] []
otherPattern p = LeftoverPatterns empty [] [] [] [p]
getLeftoverPattern :: ProblemEq -> TCM LeftoverPatterns
getLeftoverPattern (ProblemEq p v a) = case p of
(A.VarP (A.BindName x)) -> isEtaVar v (unDom a) >>= \case
Just i -> return $ patternVariable x i
Nothing -> return $ asPattern x v a
(A.WildP _) -> return mempty
(A.AsP info (A.BindName x) p) -> (asPattern x v a `mappend`) <$> do
getLeftoverPattern $ ProblemEq p v a
(A.DotP info e) -> return $ dotPattern e v a
(A.AbsurdP info) -> return $ absurdPattern (getRange info) (unDom a)
_ -> return $ otherPattern p
getUserVariableNames :: Telescope -> IntMap [A.Name]
-> ([Maybe A.Name], [AsBinding])
getUserVariableNames tel names = runWriter $
zipWithM makeVar (flattenTel tel) (downFrom $ size tel)
where
makeVar :: Dom Type -> Int -> Writer [AsBinding] (Maybe A.Name)
makeVar a i | Just (x:xs) <- IntMap.lookup i names = do
tell $ map (\y -> AsB y (var i) (unDom a)) xs
return $ Just x
makeVar a i = return Nothing
transferOrigins :: [NamedArg A.Pattern]
-> [NamedArg DeBruijnPattern]
-> TCM [NamedArg DeBruijnPattern]
transferOrigins ps qs = do
reportSDoc "tc.lhs.origin" 40 $ vcat
[ "transferOrigins"
, nest 2 $ vcat
[ "ps = " <+> prettyA ps
, "qs = " <+> pretty qs
]
]
transfers ps qs
where
transfers :: [NamedArg A.Pattern]
-> [NamedArg DeBruijnPattern]
-> TCM [NamedArg DeBruijnPattern]
transfers [] qs
| all notVisible qs = return $ map (setOrigin Inserted) qs
| otherwise = __IMPOSSIBLE__
transfers (p : ps) [] = __IMPOSSIBLE__
transfers (p : ps) (q : qs)
| matchingArgs p q = do
q' <- setOrigin (getOrigin p) <$>
(traverse $ traverse $ transfer $ namedArg p) q
(q' :) <$> transfers ps qs
| otherwise = (setOrigin Inserted q :) <$> transfers (p : ps) qs
transfer :: A.Pattern -> DeBruijnPattern -> TCM DeBruijnPattern
transfer p q = case (snd (asView p) , q) of
(A.ConP pi _ ps , ConP c (ConPatternInfo mo ft mb l) qs) -> do
let cpi = ConPatternInfo (mo $> PatOCon) ft mb l
ConP c cpi <$> transfers ps qs
(A.RecP pi fs , ConP c (ConPatternInfo mo ft mb l) qs) -> do
let Def d _ = unEl $ unArg $ fromMaybe __IMPOSSIBLE__ mb
axs = map (nameConcrete . qnameName . unArg) (conFields c) `withArgsFrom` qs
cpi = ConPatternInfo (mo $> PatORec) ft mb l
ps <- insertMissingFields d (const $ A.WildP patNoRange) fs axs
ConP c cpi <$> transfers ps qs
(p , ConP c (ConPatternInfo mo ft mb l) qs) -> do
let cpi = ConPatternInfo (mo $> patOrigin p) ft mb l
return $ ConP c cpi qs
(p , VarP _ x) -> return $ VarP (patOrigin p) x
(p , DotP _ u) -> return $ DotP (patOrigin p) u
_ -> return q
patOrigin :: A.Pattern -> PatOrigin
patOrigin (A.VarP x) = PatOVar (A.unBind x)
patOrigin A.DotP{} = PatODot
patOrigin A.ConP{} = PatOCon
patOrigin A.RecP{} = PatORec
patOrigin A.WildP{} = PatOWild
patOrigin A.AbsurdP{} = PatOAbsurd
patOrigin A.LitP{} = PatOLit
patOrigin A.EqualP{} = PatOCon
patOrigin A.AsP{} = __IMPOSSIBLE__
patOrigin A.ProjP{} = __IMPOSSIBLE__
patOrigin A.DefP{} = __IMPOSSIBLE__
patOrigin A.PatternSynP{} = __IMPOSSIBLE__
patOrigin A.WithP{} = __IMPOSSIBLE__
matchingArgs :: NamedArg A.Pattern -> NamedArg DeBruijnPattern -> Bool
matchingArgs p q
| isJust (A.isProjP p) = isJust (isProjP q)
| visible p && visible q = True
| sameHiding p q && isNothing (nameOf (unArg p)) = True
| sameHiding p q && nameOf (unArg p) == nameOf (unArg q) = True
| otherwise = False
checkPatternLinearity :: [ProblemEq] -> TCM [ProblemEq]
checkPatternLinearity eqs = do
reportSDoc "tc.lhs.linear" 30 $ "Checking linearity of pattern variables"
check Map.empty eqs
where
check :: Map A.BindName Term -> [ProblemEq] -> TCM [ProblemEq]
check _ [] = return []
check vars (eq@(ProblemEq p u a) : eqs) = do
reportSDoc "tc.lhs.linear" 40 $ sep
[ "linearity: checking pattern "
, prettyA p
, " equal to term "
, prettyTCM u
]
case p of
A.VarP x -> do
verboseS "tc.lhs.linear" 60 $ do
let y = A.unBind x
reportSLn "tc.lhs.linear" 60 $
"pattern variable " ++ show (A.nameConcrete y) ++ " with id " ++ show (A.nameId y)
case Map.lookup x vars of
Just v -> do
noConstraints $ equalTerm (unDom a) u v
check vars eqs
Nothing -> (eq:) <$> do
check (Map.insert x u vars) eqs
A.AsP _ x p ->
check vars $ [ProblemEq (A.VarP x) u a, ProblemEq p u a] ++ eqs
A.WildP{} -> continue
A.DotP{} -> continue
A.AbsurdP{} -> continue
A.ConP{} -> __IMPOSSIBLE__
A.ProjP{} -> __IMPOSSIBLE__
A.DefP{} -> __IMPOSSIBLE__
A.LitP{} -> __IMPOSSIBLE__
A.PatternSynP{} -> __IMPOSSIBLE__
A.RecP{} -> __IMPOSSIBLE__
A.EqualP{} -> __IMPOSSIBLE__
A.WithP{} -> __IMPOSSIBLE__
where continue = (eq:) <$> check vars eqs
computeLHSContext :: [Maybe A.Name] -> Telescope -> TCM Context
computeLHSContext = go [] []
where
go cxt _ [] tel@ExtendTel{} = do
reportSDoc "impossible" 10 $
"computeLHSContext: no patterns left, but tel =" <+> prettyTCM tel
__IMPOSSIBLE__
go cxt _ (_ : _) EmptyTel = __IMPOSSIBLE__
go cxt _ [] EmptyTel = return cxt
go cxt taken (x : xs) tel0@(ExtendTel a tel) = do
name <- maybe (dummyName taken $ absName tel) return x
let e = (name,) <$> a
go (e : cxt) (name : taken) xs (absBody tel)
dummyName taken s =
if isUnderscore s then freshNoName_
else setNotInScope <$> freshName_ (argNameToString s)
bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
bindAsPatterns [] ret = ret
bindAsPatterns (AsB x v a : asb) ret = do
reportSDoc "tc.lhs.as" 10 $ "as pattern" <+> prettyTCM x <+>
sep [ ":" <+> prettyTCM a
, "=" <+> prettyTCM v
]
addLetBinding defaultArgInfo x v a $ bindAsPatterns asb ret
recheckStrippedWithPattern :: ProblemEq -> TCM ()
recheckStrippedWithPattern (ProblemEq p v a) = checkInternal v (unDom a)
`catchError` \_ -> typeError . GenericDocError =<< vcat
[ "Ill-typed pattern after with abstraction: " <+> prettyA p
, "(perhaps you can replace it by `_`?)"
]
data LHSResult = LHSResult
{ lhsParameters :: Nat
, lhsVarTele :: Telescope
, lhsPatterns :: [NamedArg DeBruijnPattern]
, lhsHasAbsurd :: Bool
, lhsBodyType :: Arg Type
, lhsPatSubst :: Substitution
, lhsAsBindings :: [AsBinding]
, lhsPartialSplit :: [Int]
}
instance InstantiateFull LHSResult where
instantiateFull' (LHSResult n tel ps abs t sub as psplit) = LHSResult n
<$> instantiateFull' tel
<*> instantiateFull' ps
<*> instantiateFull' abs
<*> instantiateFull' t
<*> instantiateFull' sub
<*> instantiateFull' as
<*> pure psplit
checkLeftHandSide :: forall a.
Call
-> Maybe QName
-> [NamedArg A.Pattern]
-> Type
-> Maybe Substitution
-> [ProblemEq]
-> (LHSResult -> TCM a)
-> TCM a
checkLeftHandSide c f ps a withSub' strippedPats = Bench.billToCPS [Bench.Typing, Bench.CheckLHS] $ \ ret -> do
cxt <- map (setOrigin Inserted) . reverse <$> getContext
let tel = telFromList' prettyShow cxt
cps = [ unnamed . A.VarP . A.BindName . fst <$> argFromDom d
| d <- cxt ]
eqs0 = zipWith3 ProblemEq (map namedArg cps) (map var $ downFrom $ size tel) (flattenTel tel)
let finalChecks :: LHSState a -> TCM a
finalChecks (LHSState delta qs0 (Problem eqs rps _) b psplit) = do
reportSDoc "tc.lhs.top" 20 $ vcat
[ "lhs: final checks with remaining equations"
, nest 2 $ if null eqs then "(none)" else vcat $ map prettyTCM eqs
, "qs0 =" <+> addContext delta (prettyTCMPatternList qs0)
]
unless (null rps) __IMPOSSIBLE__
delta <- forceTranslateTelescope delta qs0
addContext delta $ do
noShadowingOfConstructors c eqs
noPatternMatchingOnCodata qs0
let notProj ProjP{} = False
notProj _ = True
numPats = length $ takeWhile (notProj . namedArg) qs0
weakSub :: Substitution
weakSub | isJust withSub' = wkS (max 0 $ numPats - arity a) idS
| otherwise = wkS (numPats - length cxt) idS
withSub = fromMaybe idS withSub'
patSub = (map (patternToTerm . namedArg) $ reverse $ take numPats qs0) ++# (EmptyS __IMPOSSIBLE__)
paramSub = patSub `composeS` weakSub `composeS` withSub
eqs <- addContext delta $ checkPatternLinearity eqs
LeftoverPatterns patVars asb0 dots absurds otherPats
<- addContext delta $ getLeftoverPatterns eqs
unless (null otherPats) __IMPOSSIBLE__
let (vars, asb1) = getUserVariableNames delta patVars
asb = asb0 ++ asb1
let makeVar = maybe deBruijnVar $ debruijnNamedVar . nameToArgName
ren = parallelS $ zipWith makeVar (reverse vars) [0..]
qs <- transferOrigins (cps ++ ps) $ applySubst ren qs0
let hasAbsurd = not . null $ absurds
let lhsResult = LHSResult (length cxt) delta qs hasAbsurd b patSub asb (catMaybes psplit)
reportSDoc "tc.lhs.top" 10 $
vcat [ "checked lhs:"
, nest 2 $ vcat
[ "delta = " <+> prettyTCM delta
, "dots = " <+> addContext delta (brackets $ fsep $ punctuate comma $ map prettyTCM dots)
, "asb = " <+> addContext delta (brackets $ fsep $ punctuate comma $ map prettyTCM asb)
, "absurds = " <+> addContext delta (brackets $ fsep $ punctuate comma $ map prettyTCM absurds)
, "qs = " <+> addContext delta (prettyList $ map pretty qs)
]
]
reportSDoc "tc.lhs.top" 30 $
nest 2 $ vcat
[ "vars = " <+> text (show vars)
]
reportSDoc "tc.lhs.top" 20 $ nest 2 $ "withSub = " <+> pretty withSub
reportSDoc "tc.lhs.top" 20 $ nest 2 $ "weakSub = " <+> pretty weakSub
reportSDoc "tc.lhs.top" 20 $ nest 2 $ "patSub = " <+> pretty patSub
reportSDoc "tc.lhs.top" 20 $ nest 2 $ "paramSub = " <+> pretty paramSub
newCxt <- computeLHSContext vars delta
updateContext paramSub (const newCxt) $ do
reportSDoc "tc.lhs.top" 10 $ "bound pattern variables"
reportSDoc "tc.lhs.top" 60 $ nest 2 $ "context = " <+> (pretty =<< getContextTelescope)
reportSDoc "tc.lhs.top" 10 $ nest 2 $ "type = " <+> prettyTCM b
reportSDoc "tc.lhs.top" 60 $ nest 2 $ "type = " <+> pretty b
bindAsPatterns asb $ do
mapM_ checkDotPattern dots
mapM_ checkAbsurdPattern absurds
ret lhsResult
st0 <- initLHSState tel eqs0 ps a finalChecks
let withSub = fromMaybe __IMPOSSIBLE__ withSub'
withEqs <- updateProblemEqs $ applySubst withSub strippedPats
inTopContext $ addContext (st0 ^. lhsTel) $
forM_ withEqs recheckStrippedWithPattern
let st = over (lhsProblem . problemEqs) (++ withEqs) st0
(result, block) <- inTopContext $ runWriterT $ (`runReaderT` (size cxt)) $ checkLHS f st
return result
splitStrategy :: [ProblemEq] -> [ProblemEq]
splitStrategy = filter shouldSplit
where
shouldSplit :: ProblemEq -> Bool
shouldSplit (ProblemEq p v a) = case snd $ asView p of
A.LitP{} -> True
A.RecP{} -> True
A.ConP{} -> True
A.EqualP{} -> True
A.VarP{} -> False
A.WildP{} -> False
A.DotP{} -> False
A.AbsurdP{} -> False
A.ProjP{} -> __IMPOSSIBLE__
A.DefP{} -> __IMPOSSIBLE__
A.AsP{} -> __IMPOSSIBLE__
A.PatternSynP{} -> __IMPOSSIBLE__
A.WithP{} -> __IMPOSSIBLE__
checkLHS
:: forall tcm a. (MonadTCM tcm, MonadReduce tcm, MonadWriter Blocked_ tcm, HasConstInfo tcm, MonadError TCErr tcm, MonadDebug tcm, MonadReader Nat tcm)
=> Maybe QName
-> LHSState a
-> tcm a
checkLHS mf = updateRelevance checkLHS_ where
updateRelevance cont st@(LHSState tel ip problem target psplit) = do
let m = getModality target
applyModalityToContext m $ do
cont $ over (lhsTel . listTel) (map $ inverseApplyModality m) st
checkLHS_ st@(LHSState tel ip problem target psplit) = do
if isSolvedProblem problem then
liftTCM $ (problem ^. problemCont) st
else do
unlessM (optPatternMatching <$> getsTC getPragmaOptions) $
unless (problemAllVariables problem) $
typeError $ GenericError $ "Pattern matching is disabled"
let splitsToTry = splitStrategy $ problem ^. problemEqs
foldr trySplit trySplitRest splitsToTry >>= \case
Right st' -> checkLHS mf st'
Left (err:_) -> throwError err
Left [] -> __IMPOSSIBLE__
where
trySplit :: ProblemEq
-> tcm (Either [TCErr] (LHSState a))
-> tcm (Either [TCErr] (LHSState a))
trySplit eq tryNextSplit = runExceptT (splitArg eq) >>= \case
Right st' -> return $ Right st'
Left err -> left (err:) <$> tryNextSplit
trySplitRest :: tcm (Either [TCErr] (LHSState a))
trySplitRest = case problem ^. problemRestPats of
[] -> return $ Left []
(p:_) -> left singleton <$> runExceptT (splitRest p)
splitArg :: ProblemEq -> ExceptT TCErr tcm (LHSState a)
splitArg (ProblemEq p v Dom{unDom = a}) = traceCall (CheckPattern p tel a) $ do
reportSDoc "tc.lhs.split" 30 $ sep
[ "split looking at pattern"
, nest 2 $ "p =" <+> prettyA p
]
i <- liftTCM $ addContext tel $ ifJustM (isEtaVar v a) return $
softTypeError $ SplitOnNonVariable v a
let pos = size tel - (i+1)
(delta1, tel'@(ExtendTel dom adelta2)) = splitTelescopeAt pos tel
p <- liftTCM $ expandLitPattern p
case snd $ asView p of
(A.LitP l) -> splitLit delta1 dom adelta2 l
p@A.RecP{} -> splitCon delta1 dom adelta2 p Nothing
p@(A.ConP _ c ps) -> splitCon delta1 dom adelta2 p $ Just c
p@(A.EqualP _ ts) -> splitPartial delta1 dom adelta2 ts
A.VarP{} -> __IMPOSSIBLE__
A.WildP{} -> __IMPOSSIBLE__
A.DotP{} -> __IMPOSSIBLE__
A.AbsurdP{} -> __IMPOSSIBLE__
A.ProjP{} -> __IMPOSSIBLE__
A.DefP{} -> __IMPOSSIBLE__
A.AsP{} -> __IMPOSSIBLE__
A.PatternSynP{} -> __IMPOSSIBLE__
A.WithP{} -> __IMPOSSIBLE__
splitRest :: NamedArg A.Pattern -> ExceptT TCErr tcm (LHSState a)
splitRest p = setCurrentRange p $ do
reportSDoc "tc.lhs.split" 20 $ sep
[ "splitting problem rest"
, nest 2 $ "projection pattern =" <+> prettyA p
, nest 2 $ "eliminates type =" <+> prettyTCM target
]
reportSDoc "tc.lhs.split" 80 $ sep
[ nest 2 $ text $ "projection pattern (raw) = " ++ show p
]
(orig, ambProjName) <- ifJust (A.isProjP p) return $
addContext tel $ softTypeError $ CannotEliminateWithPattern p (unArg target)
(projName, projType) <- suspendErrors $ do
let h = if orig == ProjPostfix then Nothing else Just $ getHiding p
addContext tel $ disambiguateProjection h ambProjName target
f <- ifJust mf return $ hardTypeError $
GenericError "Cannot use copatterns in a let binding"
let self = Def f $ patternsToElims ip
target' <- traverse (`piApplyM` self) projType
let projP = applyWhen (orig == ProjPostfix) (setHiding NotHidden) $
target' $> Named Nothing (ProjP orig projName)
ip' = ip ++ [projP]
problem' = over problemRestPats tail problem
liftTCM $ updateProblemRest (LHSState tel ip' problem' target' psplit)
splitPartial :: Telescope
-> Dom Type
-> Abs Telescope
-> [(A.Expr, A.Expr)]
-> ExceptT TCErr tcm (LHSState a)
splitPartial delta1 dom adelta2 ts = do
unless (domFinite dom) $ softTypeError $ GenericError $ "Not a finite domain: " ++ show dom
tInterval <- liftTCM $ elInf primInterval
names <- liftTCM $ addContext tel $ do
LeftoverPatterns{patternVariables = vars} <- getLeftoverPatterns $ problem ^. problemEqs
return $ take (size delta1) $ fst $ getUserVariableNames tel vars
lhsCxtSize <- ask
reportSDoc "tc.lhs.split.partial" 10 $ "lhsCxtSize =" <+> prettyTCM lhsCxtSize
newContext <- liftTCM $ computeLHSContext names delta1
reportSDoc "tc.lhs.split.partial" 10 $ "newContext =" <+> prettyTCM newContext
let cpSub = raiseS $ size newContext - lhsCxtSize
(gamma,sigma) <- liftTCM $ updateContext cpSub (const newContext) $ do
ts <- forM ts $ \ (t,u) -> do
reportSDoc "tc.lhs.split.partial" 10 $ "currentCxt =" <+> (prettyTCM =<< getContext)
reportSDoc "tc.lhs.split.partial" 10 $ text "t, u (Expr) =" <+> prettyTCM (t,u)
t <- checkExpr t tInterval
u <- checkExpr u tInterval
reportSDoc "tc.lhs.split.partial" 10 $ text "t, u =" <+> pretty (t, u)
u <- intervalView =<< reduce u
case u of
IZero -> primINeg <@> pure t
IOne -> return t
_ -> typeError $ GenericError $ "Only 0 or 1 allowed on the rhs of face"
phi <- case ts of
[] -> do
a <- reduce (unEl $ unDom dom)
isone <- fromMaybe __IMPOSSIBLE__ <$>
getBuiltinName' builtinIsOne
case a of
Def q [Apply phi] | q == isone -> return (unArg phi)
_ -> typeError . GenericDocError =<< do
prettyTCM a <+> " is not IsOne."
_ -> foldl (\ x y -> primIMin <@> x <@> y) primIOne (map pure ts)
reportSDoc "tc.lhs.split.partial" 10 $ text "phi =" <+> prettyTCM phi
reportSDoc "tc.lhs.split.partial" 30 $ text "phi =" <+> pretty phi
phi <- reduce phi
reportSDoc "tc.lhs.split.partial" 10 $ text "phi (reduced) =" <+> prettyTCM phi
refined <- forallFaceMaps phi (\ bs m t -> typeError $ GenericError $ "face blocked on meta")
(\ sigma -> (,sigma) <$> getContextTelescope)
case refined of
[(gamma,sigma)] -> return (gamma,sigma)
[] -> typeError $ GenericError $ "The face constraint is unsatisfiable."
_ -> typeError $ GenericError $ "Cannot have disjunctions in a face constraint."
itisone <- liftTCM primItIsOne
reportSDoc "tc.lhs.faces" 60 $ text $ show sigma
let oix = size adelta2
o_n = fromMaybe __IMPOSSIBLE__ $
flip findIndex ip (\ x -> case namedThing (unArg x) of
VarP _ x -> dbPatVarIndex x == oix
_ -> False)
delta2' = absApp adelta2 itisone
delta2 = applySubst sigma delta2'
mkConP (Con c _ [])
= ConP c (noConPatternInfo { conPType = Just (Arg defaultArgInfo tInterval)
, conPFallThrough = True })
[]
mkConP (Var i []) = VarP PatOSystem (DBPatVar "x" i)
mkConP _ = __IMPOSSIBLE__
rho0 = fmap mkConP sigma
rho = liftS (size delta2) $ consS (DotP PatOSystem itisone) rho0
delta' = abstract gamma delta2
eqs' = applyPatSubst rho $ problem ^. problemEqs
ip' = applySubst rho ip
target' = applyPatSubst rho target
eqs' <- liftTCM $ addContext delta' $ updateProblemEqs eqs'
let problem' = set problemEqs eqs' problem
reportSDoc "tc.lhs.split.partial" 60 $ text (show problem')
liftTCM $ updateProblemRest (LHSState delta' ip' problem' target' (psplit ++ [Just o_n]))
splitLit :: Telescope
-> Dom Type
-> Abs Telescope
-> Literal
-> ExceptT TCErr tcm (LHSState a)
splitLit delta1 dom@Dom{domInfo = info, unDom = a} adelta2 lit = do
let delta2 = absApp adelta2 (Lit lit)
delta' = abstract delta1 delta2
rho = singletonS (size delta2) (LitP lit)
eqs' = applyPatSubst rho $ problem ^. problemEqs
ip' = applySubst rho ip
target' = applyPatSubst rho target
unless (usableRelevance info) $
addContext delta1 $ softTypeError $ SplitOnIrrelevant dom
suspendErrors $ equalType a =<< litType lit
eqs' <- liftTCM $ addContext delta' $ updateProblemEqs eqs'
let problem' = set problemEqs eqs' problem
liftTCM $ updateProblemRest (LHSState delta' ip' problem' target' psplit)
splitCon :: Telescope
-> Dom Type
-> Abs Telescope
-> A.Pattern
-> Maybe AmbiguousQName
-> ExceptT TCErr tcm (LHSState a)
splitCon delta1 dom@Dom{domInfo = info, unDom = a} adelta2 focusPat ambC = do
let delta2 = absBody adelta2
reportSDoc "tc.lhs.split" 10 $ vcat
[ "checking lhs"
, nest 2 $ "tel =" <+> prettyTCM tel
, nest 2 $ "rel =" <+> (text $ show $ getRelevance info)
]
reportSDoc "tc.lhs.split" 15 $ vcat
[ "split problem"
, nest 2 $ vcat
[ "delta1 = " <+> prettyTCM delta1
, "a = " <+> addContext delta1 (prettyTCM a)
, "delta2 = " <+> addContext delta1
(addContext ("x" :: String, dom) (prettyTCM delta2))
]
]
reportSLn "tc.lhs.split" 30 $ "split ConP: relevance is " ++ show (getRelevance info)
unless (usableRelevance info) $ addContext delta1 $
softTypeError $ SplitOnIrrelevant dom
(dr, d, pars, ixs) <- addContext delta1 $ isDataOrRecordType a
checkSortOfSplitVar dr a (Just target)
(c, b) <- liftTCM $ addContext delta1 $ case ambC of
Just ambC -> disambiguateConstructor ambC d pars
Nothing -> getRecordConstructor d pars a
case focusPat of
A.ConP cpi _ _ | patLazy cpi == ConPatLazy -> softTypeError $
ForcedConstructorNotInstantiated focusPat
_ -> return ()
(TelV gamma (El _ ctarget), boundary) <- liftTCM $ telViewPathBoundaryP b
let Def d' es' = ctarget
cixs = drop (size pars) $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es'
reportSDoc "tc.lhs.split.con" 50 $ text " boundary = " <+> prettyTCM boundary
unless (d == d') __IMPOSSIBLE__
gamma <- liftTCM $ case focusPat of
A.ConP _ _ ps -> do
ps <- insertImplicitPatterns ExpandLast ps gamma
return $ useNamesFromPattern ps gamma
A.RecP _ fs -> do
axs <- recordFieldNames . theDef <$> getConstInfo d
ps <- insertMissingFields d (const $ A.WildP patNoRange) fs axs
ps <- insertImplicitPatterns ExpandLast ps gamma
return $ useNamesFromPattern ps gamma
_ -> __IMPOSSIBLE__
let updMod = composeModality (getModality info)
gamma <- return $ mapModality updMod <$> gamma
da <- (`piApply` pars) . defType <$> getConstInfo d
reportSDoc "tc.lhs.split" 30 $ " da = " <+> prettyTCM da
reportSDoc "tc.lhs.top" 15 $ addContext delta1 $
sep [ "preparing to unify"
, nest 2 $ vcat
[ "c =" <+> prettyTCM c <+> ":" <+> prettyTCM b
, "d =" <+> prettyTCM (Def d (map Apply pars)) <+> ":" <+> prettyTCM da
, "gamma =" <+> prettyTCM gamma
, "pars =" <+> brackets (fsep $ punctuate comma $ map prettyTCM pars)
, "ixs =" <+> brackets (fsep $ punctuate comma $ map prettyTCM ixs)
, "cixs =" <+> addContext gamma (brackets (fsep $ punctuate comma $ map prettyTCM cixs))
]
]
let delta1Gamma = delta1 `abstract` gamma
da' = raise (size gamma) da
ixs' = raise (size gamma) ixs
let flex = allFlexVars $ delta1Gamma
liftTCM (unifyIndices delta1Gamma flex da' cixs ixs') >>= \case
NoUnify neg -> hardTypeError $ ImpossibleConstructor (conName c) neg
DontKnow errs -> softTypeError $ SplitError $
UnificationStuck (conName c) (delta1 `abstract` gamma) cixs ixs' errs
Unifies (delta1',rho0,es) -> do
reportSDoc "tc.lhs.top" 15 $ "unification successful"
reportSDoc "tc.lhs.top" 20 $ nest 2 $ vcat
[ "delta1' =" <+> prettyTCM delta1'
, "rho0 =" <+> addContext delta1' (prettyTCM rho0)
, "es =" <+> addContext delta1' (prettyTCM $ (fmap . fmap . fmap) patternToTerm es)
]
let (rho1,rho2) = splitS (size gamma) rho0
reportSDoc "tc.lhs.top" 20 $ addContext delta1' $ nest 2 $ vcat
[ "rho1 =" <+> prettyTCM rho1
, "rho2 =" <+> prettyTCM rho2
]
let a' = applyPatSubst rho1 a
isRec <- isRecord d
let cpi = ConPatternInfo { conPRecord = isRec $> PatOCon
, conPFallThrough = False
, conPType = Just $ Arg info a'
, conPLazy = False }
let crho = ConP c cpi $ applySubst rho0 $ (telePatterns gamma boundary)
rho3 = consS crho rho1
delta2' = applyPatSubst rho3 delta2
delta' = delta1' `abstract` delta2'
rho = liftS (size delta2) rho3
reportSDoc "tc.lhs.top" 20 $ addContext delta1' $ nest 2 $ vcat
[ "crho =" <+> prettyTCM crho
, "rho3 =" <+> prettyTCM rho3
, "delta2' =" <+> prettyTCM delta2'
]
reportSDoc "tc.lhs.top" 70 $ addContext delta1' $ nest 2 $ vcat
[ "crho =" <+> pretty crho
, "rho3 =" <+> pretty rho3
, "delta2' =" <+> pretty delta2'
]
reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
[ "delta' =" <+> prettyTCM delta'
, "rho =" <+> addContext delta' (prettyTCM rho)
]
let ip' = applySubst rho ip
target' = applyPatSubst rho target
let eqs' = applyPatSubst rho $ problem ^. problemEqs
eqs' <- liftTCM $ addContext delta' $ updateProblemEqs eqs'
let problem' = set problemEqs eqs' problem
st' <- liftTCM $ updateProblemRest $ LHSState delta' ip' problem' target' psplit
reportSDoc "tc.lhs.top" 12 $ sep
[ "new problem from rest"
, nest 2 $ vcat
[ "delta' =" <+> prettyTCM (st' ^. lhsTel)
, "eqs' =" <+> addContext (st' ^. lhsTel) (prettyTCM $ st' ^. lhsProblem ^. problemEqs)
, "ip' =" <+> addContext (st' ^. lhsTel) (pretty $ st' ^. lhsOutPat)
]
]
return st'
noPatternMatchingOnCodata :: [NamedArg DeBruijnPattern] -> TCM ()
noPatternMatchingOnCodata = mapM_ (check . namedArg)
where
check (VarP {}) = return ()
check (DotP {}) = return ()
check (ProjP{}) = return ()
check (IApplyP{}) = return ()
check (LitP {}) = return ()
check (DefP{}) = return ()
check (ConP con _ ps) = do
reportSDoc "tc.lhs.top" 40 $
"checking whether" <+> prettyTCM con <+> "is a coinductive constructor"
TelV _ t <- telView' . defType <$> do getConstInfo $ conName con
c <- isCoinductive t
case c of
Nothing -> __IMPOSSIBLE__
Just False -> mapM_ (check . namedArg) ps
Just True -> typeError $
GenericError "Pattern matching on coinductive types is not allowed"
suspendErrors :: (MonadTCM m, MonadError TCErr m) => TCM a -> m a
suspendErrors f = do
ok <- liftTCM $ (Right <$> f) `catchError` (return . Left)
either throwError return ok
softTypeError :: (MonadTCM m, MonadError TCErr m) => TypeError -> m a
softTypeError err = throwError =<< typeError_ err
hardTypeError :: (MonadTCM m) => TypeError -> m a
hardTypeError = liftTCM . typeError
isDataOrRecordType :: (MonadTCM m, MonadDebug m)
=> Type
-> ExceptT TCErr m (DataOrRecord, QName, Args, Args)
isDataOrRecordType a = liftTCM (reduceB a) >>= \case
NotBlocked ReallyNotBlocked a -> case unEl a of
Def d es -> (liftTCM $ theDef <$> getConstInfo d) >>= \case
Datatype{dataPars = np} -> do
let (pars, ixs) = splitAt np $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
return (IsData, d, pars, ixs)
Record{} -> do
let pars = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
return (IsRecord, d, pars, [])
AbstractDefn{} -> hardTypeError . GenericDocError =<< do
liftTCM $ "Cannot split on abstract data type" <+> prettyTCM d
Axiom{} -> hardTypeError =<< notData
DataOrRecSig{} -> hardTypeError . GenericDocError =<< do
liftTCM $ "Cannot split on data type" <+> prettyTCM d <+> "whose definition has not yet been checked"
Function{} -> hardTypeError =<< notData
Constructor{} -> __IMPOSSIBLE__
Primitive{} -> hardTypeError =<< notData
GeneralizableVar{} -> __IMPOSSIBLE__
Var{} -> softTypeError =<< notData
MetaV{} -> softTypeError =<< notData
Pi{} -> hardTypeError =<< notData
Sort{} -> hardTypeError =<< notData
Lam{} -> __IMPOSSIBLE__
Lit{} -> __IMPOSSIBLE__
Con{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
Dummy s -> __IMPOSSIBLE_VERBOSE__ s
_ -> softTypeError =<< notData
where notData = liftTCM $ SplitError . NotADatatype <$> buildClosure a
getRecordConstructor
:: QName
-> Args
-> Type
-> TCM (ConHead, Type)
getRecordConstructor d pars a = do
con <- (theDef <$> getConstInfo d) >>= \case
Record{recConHead = con} -> return $ killRange con
_ -> typeError $ ShouldBeRecordType a
b <- (`piApply` pars) . defType <$> getConstInfo (conName con)
return (con, b)
disambiguateProjection
:: Maybe Hiding
-> AmbiguousQName
-> Arg Type
-> TCM (QName, Arg Type)
disambiguateProjection h ambD@(AmbQ ds) b = do
caseMaybeM (liftTCM $ isRecordType $ unArg b) notRecord $ \(r, vs, def) -> case def of
Record{ recFields = fs } -> do
reportSDoc "tc.lhs.split" 20 $ sep
[ text $ "we are of record type r = " ++ prettyShow r
, text "applied to parameters vs = " <+> prettyTCM vs
, text $ "and have fields fs = " ++ prettyShow fs
]
disambiguations <- mapM (runExceptT . tryProj False fs r vs) ds
case partitionEithers $ toList disambiguations of
(_ , (d,a):_) -> do
liftTCM $ storeDisambiguatedName d
return (d,a)
(_ , [] ) -> do
disambiguations <- mapM (runExceptT . tryProj True fs r vs) ds
case partitionEithers $ toList disambiguations of
([] , [] ) -> __IMPOSSIBLE__
(err:_, [] ) -> throwError err
(errs , [(d,a)]) -> do
liftTCM $ storeDisambiguatedName d
return (d,a)
(errs , disambs@((d,a):_)) -> typeError . GenericDocError =<< vcat
[ "Ambiguous projection " <> prettyTCM d <> "."
, "It could refer to any of"
, nest 2 $ vcat $ map showDisamb disambs
]
_ -> __IMPOSSIBLE__
where
showDisamb (d,_) =
let r = head $ filter (noRange /=) $ map nameBindingSite $ reverse $ mnameToList $ qnameModule d
in (pretty =<< dropTopLevelModule d) <+> "(introduced at " <> prettyTCM r <> ")"
notRecord = wrongProj $ headNe ds
wrongProj :: (MonadTCM m, MonadError TCErr m) => QName -> m a
wrongProj d = softTypeError =<< do
liftTCM $ GenericDocError <$> sep
[ "Cannot eliminate type "
, prettyTCM (unArg b)
, " with projection "
, if isAmbiguous ambD then
text . prettyShow =<< dropTopLevelModule d
else
prettyTCM d
]
wrongHiding :: (MonadTCM m, MonadError TCErr m) => QName -> m a
wrongHiding d = softTypeError =<< do
liftTCM $ GenericDocError <$> sep
[ "Wrong hiding used for projection " , prettyTCM d ]
tryProj
:: Bool
-> [Arg QName]
-> QName
-> Args
-> QName
-> ExceptT TCErr TCM (QName, Arg Type)
tryProj constraintsOk fs r vs d0 = isProjection d0 >>= \case
Nothing -> wrongProj d0
Just proj -> do
let d = projOrig proj
qr <- maybe (wrongProj d) return $ projProper proj
when (null $ projLams proj) $ wrongProj d
reportSLn "tc.lhs.split" 90 "we are a projection pattern"
reportSDoc "tc.lhs.split" 20 $ sep
[ text $ "proj d0 = " ++ prettyShow d0
, text $ "original proj d = " ++ prettyShow d
]
argd <- maybe (wrongProj d) return $ List.find ((d ==) . unArg) fs
let ai = setRelevance (getRelevance argd) $ projArgInfo proj
reportSDoc "tc.lhs.split" 20 $ sep
[ text $ "original proj relevance = " ++ show (getRelevance argd)
]
unless (caseMaybe h True $ sameHiding ai) $ wrongHiding d
suspendErrors $ applyUnless constraintsOk noConstraints $
checkParameters qr r vs
dType <- liftTCM $ defType <$> getConstInfo d
reportSDoc "tc.lhs.split" 20 $ sep
[ "we are being projected by dType = " <+> prettyTCM dType
]
projType <- liftTCM $ dType `piApplyM` vs
return (d0 , Arg ai projType)
disambiguateConstructor
:: AmbiguousQName
-> QName
-> Args
-> TCM (ConHead, Type)
disambiguateConstructor ambC@(AmbQ cs) d pars = do
d <- canonicalName d
cons <- theDef <$> getConstInfo d >>= \case
def@Datatype{} -> return $ dataCons def
def@Record{} -> return $ [conName $ recConHead def]
_ -> __IMPOSSIBLE__
disambiguations <- mapM (runExceptT . tryCon False cons d pars) cs
case partitionEithers $ toList disambiguations of
(_ , (c0,c,a):_) -> do
when (isAmbiguous ambC) $ liftTCM $ storeDisambiguatedName c0
return (c,a)
(_ , [] ) -> do
disambiguations <- mapM (runExceptT . tryCon True cons d pars) cs
case partitionEithers $ toList disambiguations of
([] , [] ) -> __IMPOSSIBLE__
(err:_, [] ) -> throwError err
(errs , [(c0,c,a)]) -> do
when (isAmbiguous ambC) $ liftTCM $ storeDisambiguatedName c0
return (c,a)
(errs , disambs@((c0,c,a):_)) -> typeError . GenericDocError =<< vcat
[ "Ambiguous constructor " <> prettyTCM (qnameName $ conName c) <> "."
, "It could refer to any of"
, nest 2 $ vcat $ map showDisamb disambs
]
where
showDisamb (c0,_,_) =
let r = head $ filter (noRange /=) $ map nameBindingSite $ reverse $ mnameToList $ qnameModule c0
in (pretty =<< dropTopLevelModule c0) <+> "(introduced at " <> prettyTCM r <> ")"
abstractConstructor c = softTypeError $
AbstractConstructorNotInScope c
wrongDatatype c d = softTypeError $
ConstructorPatternInWrongDatatype c d
tryCon
:: Bool
-> [QName]
-> QName
-> Args
-> QName
-> ExceptT TCErr TCM (QName, ConHead, Type)
tryCon constraintsOk cons d pars c = getConstInfo' c >>= \case
Left (SigUnknown err) -> __IMPOSSIBLE__
Left SigAbstract -> abstractConstructor c
Right def -> do
let con = conSrcCon $ theDef def
unless (conName con `elem` cons) $ wrongDatatype c d
suspendErrors $ applyUnless constraintsOk noConstraints $
checkConstructorParameters c d pars
cType <- (`piApply` pars) . defType <$> getConInfo con
return (c, con, cType)
checkConstructorParameters :: MonadTCM tcm => QName -> QName -> Args -> tcm ()
checkConstructorParameters c d pars = do
dc <- liftTCM $ getConstructorData c
checkParameters dc d pars
checkParameters
:: MonadTCM tcm
=> QName
-> QName
-> Args
-> tcm ()
checkParameters dc d pars = liftTCM $ do
a <- reduce (Def dc [])
case a of
Def d0 es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
reportSDoc "tc.lhs.split" 40 $
vcat [ nest 2 $ "d =" <+> (text . prettyShow) d
, nest 2 $ "d0 (should be == d) =" <+> (text . prettyShow) d0
, nest 2 $ "dc =" <+> (text . prettyShow) dc
, nest 2 $ "vs =" <+> prettyTCM vs
]
t <- typeOfConst d
compareArgs [] [] t (Def d []) vs (take (length vs) pars)
_ -> __IMPOSSIBLE__
checkSortOfSplitVar :: (MonadTCM tcm, MonadReduce tcm, MonadError TCErr tcm, LensSort a)
=> DataOrRecord -> a -> Maybe (Arg Type) -> tcm ()
checkSortOfSplitVar dr a mtarget = do
infOk <- optOmegaInOmega <$> pragmaOptions
liftTCM (reduce $ getSort a) >>= \case
Type{} -> return ()
Prop{}
| IsRecord <- dr -> return ()
| Just target <- mtarget -> unlessM (isPropM target) splitOnPropError
| otherwise -> splitOnPropError
Inf{} | infOk -> return ()
_ -> softTypeError =<< do
liftTCM $ GenericDocError <$> sep
[ "Cannot split on datatype in sort" , prettyTCM (getSort a) ]
where
splitOnPropError = softTypeError $ GenericError
"Cannot split on datatype in Prop unless target is in Prop"