{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.LHS
( checkLeftHandSide
, LHSResult(..)
, bindAsPatterns
, IsFlexiblePattern(..)
, checkSortOfSplitVar
) where
import Prelude hiding ( mapM, null, sequence )
import Data.Maybe
import Control.Arrow (left)
import Control.Monad
import Control.Monad.Reader
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.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.List (findIndex)
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
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'(..),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 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 (ensureEmptyType)
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.Null
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Impossible
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
| conPRecord i , PatOSystem <- patOrigin (conPInfo i) -> return ImplicitFlex
| 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
updateLHSState :: LHSState a -> TCM (LHSState a)
updateLHSState st = do
let tel = st ^. lhsTel
problem = st ^. lhsProblem
eqs' <- addContext tel $ updateProblemEqs $ problem ^. problemEqs
tel' <- useNamesFromProblemEqs eqs' tel
updateProblemRest $ set lhsTel tel' $ set (lhsProblem . problemEqs) eqs' st
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@(A.AsP info x p') v a) =
(ProblemEq (A.VarP x) v a :) <$> update (ProblemEq p' v a)
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{} -> __IMPOSSIBLE__
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 <- map argFromDom . 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 :: ProblemEq -> TCM ()
noShadowingOfConstructors (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{unBind = 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
]
equalTerm a u v
checkAbsurdPattern :: AbsurdPattern -> TCM ()
checkAbsurdPattern (Absurd r a) = ensureEmptyType r a
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' <- mapNameOf (maybe id (const . Just) $ getNameOf p)
. 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 (asView p , q) of
((asB , A.ConP pi _ ps) , ConP c (ConPatternInfo i r ft mb l) qs) -> do
let cpi = ConPatternInfo (PatternInfo PatOCon asB) r ft mb l
ConP c cpi <$> transfers ps qs
((asB , A.RecP pi fs) , ConP c (ConPatternInfo i r ft mb l) qs) -> do
let Def d _ = unEl $ unArg $ fromMaybe __IMPOSSIBLE__ mb
axs = map (nameConcrete . qnameName . unArg) (conFields c) `withArgsFrom` qs
cpi = ConPatternInfo (PatternInfo PatORec asB) r ft mb l
ps <- insertMissingFields d (const $ A.WildP patNoRange) fs axs
ConP c cpi <$> transfers ps qs
((asB , p) , ConP c (ConPatternInfo i r ft mb l) qs) -> do
let cpi = ConPatternInfo (PatternInfo (patOrig p) asB) r ft mb l
return $ ConP c cpi qs
((asB , p) , VarP _ x) -> return $ VarP (PatternInfo (patOrig p) asB) x
((asB , p) , DotP _ u) -> return $ DotP (PatternInfo (patOrig p) asB) u
((asB , p) , LitP _ l) -> return $ LitP (PatternInfo (patOrig p) asB) l
_ -> return q
patOrig :: A.Pattern -> PatOrigin
patOrig (A.VarP x) = PatOVar (A.unBind x)
patOrig A.DotP{} = PatODot
patOrig A.ConP{} = PatOCon
patOrig A.RecP{} = PatORec
patOrig A.WildP{} = PatOWild
patOrig A.AbsurdP{} = PatOAbsurd
patOrig A.LitP{} = PatOLit
patOrig A.EqualP{} = PatOCon
patOrig A.AsP{} = __IMPOSSIBLE__
patOrig A.ProjP{} = __IMPOSSIBLE__
patOrig A.DefP{} = __IMPOSSIBLE__
patOrig A.PatternSynP{} = __IMPOSSIBLE__
patOrig 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 (getNameOf p) = True
| sameHiding p q && namedSame p 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
reportSLn "tc.lhs.linear" 60 $
let y = A.unBind x
in "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 CmpLeq (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 :: IntSet
}
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 call f ps a withSub' strippedPats =
Bench.billToCPS [Bench.Typing, Bench.CheckLHS] $
traceCallCPS call $ \ ret -> do
cxt <- map (setOrigin Inserted) . reverse <$> getContext
let tel = telFromList' prettyShow cxt
cps = [ unnamed . A.VarP . A.mkBindName . 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 addContext delta $ vcat $ map prettyTCM eqs
, "qs0 =" <+> addContext delta (prettyTCMPatternList qs0)
]
unless (null rps) __IMPOSSIBLE__
addContext delta $ do
mapM_ noShadowingOfConstructors 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
leftovers@(LeftoverPatterns patVars asb0 dots absurds otherPats)
<- addContext delta $ getLeftoverPatterns eqs
reportSDoc "tc.lhs.leftover" 30 $ vcat
[ "leftover patterns: " , nest 2 (addContext delta $ prettyTCM leftovers) ]
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 (IntSet.fromList $ 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) <- unsafeInTopContext $ 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, MonadAddContext tcm, MonadWriter Blocked_ tcm, HasConstInfo tcm, MonadError TCErr tcm, MonadDebug tcm, MonadReader Nat tcm)
=> Maybe QName
-> LHSState a
-> tcm a
checkLHS mf = updateModality checkLHS_ where
updateModality 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
reportSDoc "tc.lhs.top" 30 $ vcat
[ "LHS state: " , nest 2 (prettyTCM st) ]
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 $ updateLHSState (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 defaultPatternInfo (DBPatVar "x" i)
mkConP _ = __IMPOSSIBLE__
rho0 = fmap mkConP sigma
rho = liftS (size delta2) $ consS (DotP defaultPatternInfo itisone) rho0
delta' = abstract gamma delta2
eqs' = applyPatSubst rho $ problem ^. problemEqs
ip' = applySubst rho ip
target' = applyPatSubst rho target
let problem' = set problemEqs eqs' problem
reportSDoc "tc.lhs.split.partial" 60 $ text (show problem')
liftTCM $ updateLHSState (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
unlessM (splittableCohesion info) $
addContext delta1 $ softTypeError $ SplitOnUnusableCohesion dom
suspendErrors $ equalType a =<< litType lit
let problem' = set problemEqs eqs' problem
liftTCM $ updateLHSState (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)
, nest 2 $ "mod =" <+> (text $ show $ getModality 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
unlessM (splittableCohesion info) $
addContext delta1 $ softTypeError $ SplitOnUnusableCohesion 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 _ _ | conPatLazy cpi == ConPatLazy ->
unlessM (isEtaRecord d) $ 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 <- map argFromDom . 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))
]
]
cforced <- ifM (viewTC eMakeCase) (return []) $
defForced <$> getConstInfo (conName c)
let delta1Gamma = delta1 `abstract` gamma
da' = raise (size gamma) da
ixs' = raise (size gamma) ixs
forced = replicate (size delta1) NotForced ++ cforced
let flex = allFlexVars forced $ delta1Gamma
da' <- do
let updCoh = composeCohesion (getCohesion info)
TelV tel dt <- telView da'
return $ abstract (mapCohesion updCoh <$> tel) a
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 { conPInfo = PatternInfo PatOCon []
, conPRecord = isJust isRec
, 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
problem' = set problemEqs eqs' problem
st' <- liftTCM $ updateLHSState $ 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 :: (ReadTCState m, MonadError TCErr m, MonadTCEnv m) => TypeError -> m a
softTypeError err = throwError =<< typeError_ err
hardTypeError :: (MonadTCM m) => TypeError -> m a
hardTypeError = liftTCM . typeError
isDataOrRecordType :: (MonadTCM m, MonadDebug m, ReadTCState 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 (map argFromDom fs)
]
tryDisambiguate False fs r vs $ \ _ ->
tryDisambiguate True fs r vs $ \case
([] , [] ) -> __IMPOSSIBLE__
(err:_, [] ) -> throwError err
(_ , disambs@((d,a):_)) -> typeError . GenericDocError =<< vcat
[ "Ambiguous projection " <> prettyTCM d <> "."
, "It could refer to any of"
, nest 2 $ vcat $ map (prettyDisamb . fst) disambs
]
_ -> __IMPOSSIBLE__
where
tryDisambiguate constraintsOk fs r vs failure = do
disambiguations <- mapM (runExceptT . tryProj constraintsOk fs r vs) ds
case partitionEithers $ NonEmpty.toList disambiguations of
(_ , (d,a) : disambs) | constraintsOk <= null disambs -> do
liftTCM $ storeDisambiguatedName d
return (d,a)
other -> failure other
notRecord = wrongProj $ NonEmpty.head ds
wrongProj :: (MonadTCM m, MonadError TCErr m, ReadTCState 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, ReadTCState m) => QName -> m a
wrongHiding d = softTypeError =<< do
liftTCM $ GenericDocError <$> sep
[ "Wrong hiding used for projection " , prettyTCM d ]
tryProj
:: Bool
-> [Dom 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 ==) . unDom) fs
let ai = setModality (getModality argd) $ projArgInfo proj
reportSDoc "tc.lhs.split" 20 $ vcat
[ text $ "original proj relevance = " ++ show (getRelevance argd)
, text $ "original proj quantity = " ++ show (getQuantity 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__
tryDisambiguate False cons d $ \ _ ->
tryDisambiguate True cons d $ \case
([] , [] ) -> __IMPOSSIBLE__
(err:_, [] ) -> throwError err
(_ , disambs@((_c0,c,_a):_)) -> typeError . GenericDocError =<< vcat
[ "Ambiguous constructor " <> prettyTCM (qnameName $ conName c) <> "."
, "It could refer to any of"
, nest 2 $ vcat $ map (prettyDisamb . fst3) disambs
]
where
tryDisambiguate constraintsOk cons d failure = do
disambiguations <- mapM (runExceptT . tryCon constraintsOk cons d pars) cs
case partitionEithers $ NonEmpty.toList disambiguations of
(_, (c0,c,a) : disambs) | constraintsOk <= null disambs -> do
when (isAmbiguous ambC) $ liftTCM $ storeDisambiguatedName c0
return (c,a)
other -> failure other
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) `withRangeOf` c
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)
prettyDisamb :: QName -> TCM Doc
prettyDisamb x = do
let d = pretty =<< dropTopLevelModule x
let mr = lastMaybe $ filter (noRange /=) $ map nameBindingSite $ mnameToList $ qnameModule x
caseMaybe mr d $ \ r -> d <+> ("(introduced at " <> prettyTCM r <> ")")
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 m, MonadReduce m, MonadError TCErr m, ReadTCState m, MonadDebug m,
LensSort a, PrettyTCM a, LensSort ty, PrettyTCM ty)
=> DataOrRecord -> a -> Maybe ty -> m ()
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"