{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Def where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ( (<>), mapM, null )
#else
import Prelude hiding ( mapM, null )
#endif
import Control.Arrow ((***),first,second)
import Control.Monad.State hiding (forM, mapM)
import Control.Monad.Reader hiding (forM, mapM)
import Data.Function
import qualified Data.List as List
import Data.Maybe
import Data.Traversable (Traversable, traverse, forM, mapM)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Semigroup (Semigroup((<>)))
import Agda.Interaction.Options
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete (exprFieldA)
import Agda.Syntax.Position
import Agda.Syntax.Abstract.Pattern as A
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Views as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Fixity
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Info
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Warnings ( warning )
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Inlining
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Patterns.Abstract (expandPatternSynonyms)
import Agda.TypeChecking.Pretty hiding ((<>))
import qualified Agda.TypeChecking.Pretty as Pr
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.TypeChecking.CheckInternal
import Agda.TypeChecking.With
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.SizedTypes.Solve
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.Records
import Agda.TypeChecking.CompiledClause (CompiledClauses'(..), hasProjectionPatterns)
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Rules.Term
import Agda.TypeChecking.Rules.LHS ( checkLeftHandSide, LHSResult(..), bindAsPatterns )
import Agda.TypeChecking.Rules.LHS.Problem ( AsBinding(..) )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl ( checkDecls )
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe ( whenNothing )
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty ( prettyShow )
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
checkFunDef :: Delayed -> Info.DefInfo -> QName -> [A.Clause] -> TCM ()
checkFunDef delayed i name cs = do
t <- typeOfConst name
info <- flip setRelevance defaultArgInfo <$> relOfConst name
case isAlias cs t of
Just (e, mc, x) ->
traceCall (CheckFunDefCall (getRange i) name cs) $ do
whenM (isFrozen x) $ unfreezeMeta x
checkAlias t info delayed i name e mc
_ -> checkFunDef' t info delayed Nothing Nothing i name cs
ismacro <- isMacro . theDef <$> getConstInfo name
when (ismacro || Info.defMacro i == MacroDef) $ checkMacroType t
`catchIlltypedPatternBlockedOnMeta` \ (err, x) -> do
reportSDoc "tc.def" 20 $ vcat $
[ "checking function definition got stuck on meta: " <+> text (show x) ]
addConstraint $ CheckFunDef delayed i name cs
checkMacroType :: Type -> TCM ()
checkMacroType t = do
t' <- normalise t
TelV tel tr <- telView t'
let telList = telToList tel
resType = abstract (telFromList (drop (length telList - 1) telList)) tr
expectedType <- el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit)
equalType resType expectedType
`catchError` \ _ -> typeError . GenericDocError =<< sep [ "Result type of a macro must be"
, nest 2 $ prettyTCM expectedType ]
isAlias :: [A.Clause] -> Type -> Maybe (A.Expr, Maybe C.Expr, MetaId)
isAlias cs t =
case trivialClause cs of
Just (e, mc) | Just x <- isMeta (unEl t) -> Just (e, mc, x)
_ -> Nothing
where
isMeta (MetaV x _) = Just x
isMeta _ = Nothing
trivialClause [A.Clause (A.LHS i (A.LHSHead f [])) _ (A.RHS e mc) (A.WhereDecls _ []) _] = Just (e, mc)
trivialClause _ = Nothing
checkAlias :: Type -> ArgInfo -> Delayed -> Info.DefInfo -> QName -> A.Expr -> Maybe C.Expr -> TCM ()
checkAlias t ai delayed i name e mc = atClause name 0 (A.RHS e mc) $ do
reportSDoc "tc.def.alias" 10 $ "checkAlias" <+> vcat
[ text (prettyShow name) <+> colon <+> prettyTCM t
, text (prettyShow name) <+> equals <+> prettyTCM e
]
v <- applyModalityToContextFunBody ai $ checkDontExpandLast CmpLeq e t
reportSDoc "tc.def.alias" 20 $ "checkAlias: finished checking"
solveSizeConstraints DontDefaultToInfty
v <- instantiateFull v
let bodyMod = case getRelevance ai of
Irrelevant -> dontCare
_ -> id
addConstant name $ defaultDefn ai name t
$ set funMacro (Info.defMacro i == MacroDef) $
emptyFunction
{ funClauses = [ Clause
{ clauseLHSRange = getRange i
, clauseFullRange = getRange i
, clauseTel = EmptyTel
, namedClausePats = []
, clauseBody = Just $ bodyMod v
, clauseType = Just $ Arg ai t
, clauseCatchall = False
, clauseUnreachable = Just False
} ]
, funCompiled = Just $ Done [] $ bodyMod v
, funSplitTree = Just $ SplittingDone 0
, funDelayed = delayed
, funAbstr = Info.defAbstract i
}
when (Info.defInstance i == InstanceDef) $ do
addTypedInstance name t
reportSDoc "tc.def.alias" 20 $ "checkAlias: leaving"
checkFunDef' :: Type
-> ArgInfo
-> Delayed
-> Maybe ExtLamInfo
-> Maybe QName
-> Info.DefInfo
-> QName
-> [A.Clause]
-> TCM ()
checkFunDef' t ai delayed extlam with i name cs =
checkFunDefS t ai delayed extlam with i name Nothing cs
checkFunDefS :: Type
-> ArgInfo
-> Delayed
-> Maybe ExtLamInfo
-> Maybe QName
-> Info.DefInfo
-> QName
-> Maybe Substitution
-> [A.Clause]
-> TCM ()
checkFunDefS t ai delayed extlam with i name withSub cs = do
traceCall (CheckFunDefCall (getRange i) name cs) $ do
reportSDoc "tc.def.fun" 10 $
sep [ "checking body of" <+> prettyTCM name
, nest 2 $ ":" <+> prettyTCM t
, nest 2 $ "full type:" <+> (prettyTCM . defType =<< getConstInfo name)
]
reportSDoc "tc.def.fun" 70 $
sep $ [ "clauses:" ] ++ map (nest 2 . text . show . A.deepUnscope) cs
cs <- return $ map A.lhsToSpine cs
reportSDoc "tc.def.fun" 70 $
sep $ [ "spine clauses:" ] ++ map (nest 2 . text . show . A.deepUnscope) cs
cs <- traceCall NoHighlighting $ do
forM (zip cs [0..]) $ \ (c, clauseNo) -> do
atClause name clauseNo (A.clauseRHS c) $ do
(c,b) <- applyModalityToContextFunBody ai $ do
checkClause t withSub c
whenNothing extlam $ solveSizeConstraints DontDefaultToInfty
inTopContext $ addClauses name [c]
return (c,b)
(cs, CPC isOneIxs) <- return $ (second mconcat . unzip) cs
let isSystem = not . null $ isOneIxs
canBeSystem <- do
let pss = map namedClausePats cs
allowed p = case p of
VarP{} -> True
ConP _ cpi [] | conPFallThrough cpi -> True
DotP{} -> True
_ -> False
return $! all (allowed . namedArg) (concat pss)
when isSystem $ unless canBeSystem $
typeError $ GenericError "no pattern matching or path copatterns in systems!"
reportSDoc "tc.def.fun" 70 $ inTopContext $ do
sep $ [ "checked clauses:" ] ++ map (nest 2 . text . show) cs
modifyFunClauses name (const [])
reportSDoc "tc.cc" 25 $ inTopContext $ do
sep [ "clauses before injectivity test"
, nest 2 $ prettyTCM $ map (QNamed name) cs
]
reportSDoc "tc.cc" 60 $ inTopContext $ do
sep [ "raw clauses: "
, nest 2 $ sep $ map (text . show . QNamed name) cs
]
(cs,sys) <- if not isSystem then return (cs, Nothing) else do
fullType <- flip abstract t <$> getContextTelescope
sys <- inTopContext $ checkSystemCoverage name isOneIxs fullType cs
tel <- getContextTelescope
let c = Clause
{ clauseFullRange = noRange
, clauseLHSRange = noRange
, clauseTel = tel
, namedClausePats = teleNamedArgs tel
, clauseBody = Nothing
, clauseType = Just (defaultArg t)
, clauseCatchall = False
, clauseUnreachable = Just False
}
return (cs ++ [c], Just sys)
cs <- instantiateFull cs
reportSLn "tc.inj.def" 20 $ "checkFunDef': checking injectivity..."
inv <- Bench.billTo [Bench.Injectivity] $
checkInjectivity name cs
reportSDoc "tc.cc" 15 $ inTopContext $ do
sep [ "clauses before compilation"
, nest 2 $ sep $ map (prettyTCM . QNamed name) cs
]
reportSDoc "tc.cc.raw" 65 $ do
sep [ "clauses before compilation"
, nest 2 $ sep $ map (text . show) cs
]
inTopContext $ addClauses name cs
reportSDoc "tc.cc.type" 60 $ " type : " <+> (text . prettyShow) t
reportSDoc "tc.cc.type" 60 $ " context: " <+> (text . prettyShow =<< getContextTelescope)
fullType <- flip telePi t <$> getContextTelescope
reportSLn "tc.cc.type" 80 $ show fullType
(mst, cc) <- Bench.billTo [Bench.Coverage] $
inTopContext $ compileClauses (if isSystem then Nothing else (Just (name, fullType)))
cs
cs <- defClauses <$> getConstInfo name
reportSDoc "tc.cc" 60 $ inTopContext $ do
sep [ "compiled clauses of" <+> prettyTCM name
, nest 2 $ pretty cc
]
ismacro <- isMacro . theDef <$> getConstInfo name
covering <- funCovering . theDef <$> getConstInfo name
inTopContext $ addConstant name =<< do
defn <- autoInline $
set funMacro (ismacro || Info.defMacro i == MacroDef) $
emptyFunction
{ funClauses = cs
, funCompiled = Just cc
, funSplitTree = mst
, funDelayed = delayed
, funInv = inv
, funAbstr = Info.defAbstract i
, funExtLam = (\ e -> e { extLamSys = sys }) <$> extlam
, funWith = with
, funCopatternLHS = hasProjectionPatterns cc
, funCovering = covering
}
useTerPragma $ defaultDefn ai name fullType defn
reportSDoc "tc.def.fun" 10 $ do
sep [ "added " <+> prettyTCM name <+> ":"
, nest 2 $ prettyTCM . defType =<< getConstInfo name
]
useTerPragma :: Definition -> TCM Definition
useTerPragma def@Defn{ defName = name, theDef = fun@Function{}} = do
tc <- asksTC envTerminationCheck
let terminates = case tc of
NonTerminating -> Just False
Terminating -> Just True
_ -> Nothing
reportSLn "tc.fundef" 30 $ unlines $
[ "funTerminates of " ++ prettyShow name ++ " set to " ++ show terminates
, " tc = " ++ show tc
]
return $ def { theDef = fun { funTerminates = terminates }}
useTerPragma def = return def
insertPatterns :: [A.Pattern] -> A.RHS -> A.RHS
insertPatterns pats = \case
A.WithRHS aux es cs -> A.WithRHS aux es $ for cs $
\ (A.Clause (A.LHS info core) spats rhs ds catchall) ->
A.Clause (A.LHS info (insertPatternsLHSCore pats core)) spats (insertPatterns pats rhs) ds catchall
A.RewriteRHS qes spats rhs wh -> A.RewriteRHS qes spats (insertPatterns pats rhs) wh
rhs@A.AbsurdRHS -> rhs
rhs@A.RHS{} -> rhs
insertPatternsLHSCore :: [A.Pattern] -> A.LHSCore -> A.LHSCore
insertPatternsLHSCore pats = \case
A.LHSWith core wps [] -> A.LHSWith core (pats ++ wps) []
core -> A.LHSWith core pats []
data WithFunctionProblem
= NoWithFunction
| WithFunction
{ wfParentName :: QName
, wfName :: QName
, wfParentType :: Type
, wfParentTel :: Telescope
, wfBeforeTel :: Telescope
, wfAfterTel :: Telescope
, wfExprs :: [Term]
, wfExprTypes :: [EqualityView]
, wfRHSType :: Type
, wfParentPats :: [NamedArg DeBruijnPattern]
, wfParentParams :: Nat
, wfPermSplit :: Permutation
, wfPermParent :: Permutation
, wfPermFinal :: Permutation
, wfClauses :: [A.Clause]
}
checkSystemCoverage
:: QName
-> [Int]
-> Type
-> [Clause]
-> TCM System
checkSystemCoverage f [n] t cs = do
reportSDoc "tc.sys.cover" 10 $ text (show (n , length cs)) <+> prettyTCM t
TelV gamma t <- telViewUpTo n t
addContext gamma $ do
TelV (ExtendTel a _) _ <- telViewUpTo 1 t
a <- reduce $ unEl $ unDom a
case a of
Def q [Apply phi] -> do
[iz,io] <- mapM getBuiltinName' [builtinIZero, builtinIOne]
ineg <- primINeg
imin <- primIMin
imax <- primIMax
i0 <- primIZero
i1 <- primIOne
let
isDir (ConP q _ []) | Just (conName q) == iz = Just False
isDir (ConP q _ []) | Just (conName q) == io = Just True
isDir _ = Nothing
collectDirs :: [Int] -> [DeBruijnPattern] -> [(Int,Bool)]
collectDirs [] [] = []
collectDirs (i : is) (p : ps) | Just d <- isDir p = (i,d) : collectDirs is ps
| otherwise = collectDirs is ps
collectDirs _ _ = __IMPOSSIBLE__
dir :: (Int,Bool) -> Term
dir (i,False) = ineg `apply` [argN $ var i]
dir (i,True) = var i
andI, orI :: [Term] -> Term
andI [] = i1
andI [t] = t
andI (t:ts) = (\ x -> imin `apply` [argN t, argN x]) $ andI ts
orI [] = i0
orI [t] = t
orI (t:ts) = imax `apply` [argN t, argN (orI ts)]
let
pats = map (take n . map (namedThing . unArg) . namedClausePats) cs
alphas :: [[(Int,Bool)]]
alphas = map (collectDirs (downFrom n)) pats
phis :: [Term]
phis = map andI $ map (map dir) alphas
psi = orI $ phis
pcs = zip phis cs
boolToI True = i1
boolToI False = i0
reportSDoc "tc.sys.cover" 20 $ fsep $ map prettyTCM pats
interval <- elInf primInterval
reportSDoc "tc.sys.cover" 10 $ "equalTerm " <+> prettyTCM (unArg phi) <+> prettyTCM psi
equalTerm interval (unArg phi) psi
forM_ (init $ init $ List.tails pcs) $ \ ((phi1,cl1):pcs') -> do
forM_ pcs' $ \ (phi2,cl2) -> do
phi12 <- reduce (imin `apply` [argN phi1, argN phi2])
forallFaceMaps phi12 (\ _ _ -> __IMPOSSIBLE__) $ \ sigma -> do
let args = sigma `applySubst` teleArgs gamma
t' = sigma `applySubst` t
fromReduced (YesReduction _ x) = x
fromReduced (NoReduction x) = ignoreBlocking x
body cl = do
let extra = length (drop n $ namedClausePats cl)
TelV delta _ <- telViewUpTo extra t'
fmap (abstract delta) $ addContext delta $ do
fmap fromReduced $ runReduceM $
appDef' (Def f []) [cl] [] (map notReduced $ raise (size delta) args ++ teleArgs delta)
v1 <- body cl1
v2 <- body cl2
equalTerm t' v1 v2
sys <- forM (zip alphas cs) $ \ (alpha,cl) -> do
let
delta = clauseTel cl
Just b = clauseBody cl
ps = namedClausePats cl
extra = length (drop (size gamma + 1) ps)
takeLast n xs = drop (length xs - n) xs
weak [] = idS
weak (i:is) = weak is `composeS` liftS i (raiseS 1)
tel = telFromList (takeLast extra (telToList delta))
u = abstract tel (liftS extra (weak $ List.sort $ map fst alpha) `applySubst` b)
return (map (first var) alpha,u)
reportSDoc "tc.sys.cover.sys" 20 $ fsep $ prettyTCM gamma : map prettyTCM sys
reportSDoc "tc.sys.cover.sys" 40 $ fsep $ (text . show) gamma : map (text . show) sys
return (System gamma sys)
_ -> __IMPOSSIBLE__
checkSystemCoverage _ _ t cs = __IMPOSSIBLE__
data ClausesPostChecks = CPC
{ cpcPartialSplits :: [Int]
}
instance Semigroup ClausesPostChecks where
(<>) (CPC xs) (CPC xs') = CPC (List.nub $ mappend xs xs')
instance Monoid ClausesPostChecks where
mempty = CPC []
mappend = (<>)
checkClause
:: Type
-> Maybe Substitution
-> A.SpineClause
-> TCM (Clause,ClausesPostChecks)
checkClause t withSub c@(A.Clause (A.SpineLHS i x aps) strippedPats rhs0 wh catchall) = do
reportSDoc "tc.lhs.top" 30 $ "Checking clause" $$ prettyA c
unlessNull (trailingWithPatterns aps) $ \ withPats -> do
typeError $ UnexpectedWithPatterns $ map namedArg withPats
traceCall (CheckClause t c) $ do
aps <- expandPatternSynonyms aps
cxtNames <- reverse . map (fst . unDom) <$> getContext
when (not $ null strippedPats) $ reportSDoc "tc.lhs.top" 50 $
"strippedPats:" <+> vcat [ prettyA p <+> "=" <+> prettyTCM v <+> ":" <+> prettyTCM a | A.ProblemEq p v a <- strippedPats ]
closed_t <- flip abstract t <$> getContextTelescope
checkLeftHandSide (CheckPatternShadowing c) (Just x) aps t withSub strippedPats $ \ lhsResult@(LHSResult npars delta ps absurdPat trhs patSubst asb psplit) -> do
t' <- case withSub of
Just{} -> return t
Nothing -> do
theta <- lookupSection (qnameModule x)
return $ abstract theta t
let rhs = updateRHS rhs0
updateRHS rhs@A.RHS{} = rhs
updateRHS rhs@A.AbsurdRHS{} = rhs
updateRHS (A.WithRHS q es cs) = A.WithRHS q es (map updateClause cs)
updateRHS (A.RewriteRHS qes spats rhs wh) =
A.RewriteRHS qes (applySubst patSubst spats) (updateRHS rhs) wh
updateClause (A.Clause f spats rhs wh ca) =
A.Clause f (applySubst patSubst spats) (updateRHS rhs) wh ca
(body, with) <- bindAsPatterns asb $ checkWhere wh $ checkRHS i x aps t' lhsResult rhs
inTopContext $ Bench.billTo [Bench.Typing, Bench.With] $ checkWithFunction cxtNames with
whenM (optDoubleCheck <$> pragmaOptions) $ case body of
Just v -> do
reportSDoc "tc.lhs.top" 30 $ vcat
[ "double checking rhs"
, nest 2 (prettyTCM v <+> " : " <+> prettyTCM (unArg trhs))
]
noConstraints $ dontAssignMetas $ checkInternal v $ unArg trhs
Nothing -> return ()
reportSDoc "tc.lhs.top" 10 $ vcat
[ "Clause before translation:"
, nest 2 $ vcat
[ "delta =" <+> do escapeContext (size delta) $ prettyTCM delta
, "ps =" <+> do P.fsep <$> prettyTCMPatterns ps
, "body =" <+> maybe "_|_" prettyTCM body
, "type =" <+> prettyTCM t
]
]
reportSDoc "tc.lhs.top" 60 $ escapeContext (size delta) $ vcat
[ "Clause before translation (raw):"
, nest 2 $ vcat
[ "ps =" <+> text (show ps)
, "body =" <+> text (show body)
, "type =" <+> text (show t)
]
]
let
iApplyVars :: [NamedArg DeBruijnPattern] -> [(Int, (Term,Term))]
iApplyVars ps = flip concatMap (map namedArg ps) $ \case
IApplyP _ t u x -> [(dbPatVarIndex x,(t,u))]
VarP{} -> []
ProjP{}-> []
LitP{} -> []
DotP{} -> []
DefP _ _ ps -> iApplyVars ps
ConP _ _ ps -> iApplyVars ps
rel <- asksTC envRelevance
let bodyMod body = case rel of
Irrelevant -> dontCare <$> body
_ -> body
let catchall' = catchall || isNothing body
return $ (, CPC psplit)
Clause { clauseLHSRange = getRange i
, clauseFullRange = getRange c
, clauseTel = killRange delta
, namedClausePats = ps
, clauseBody = bodyMod body
, clauseType = Just trhs
, clauseCatchall = catchall'
, clauseUnreachable = Nothing
}
checkRHS
:: LHSInfo
-> QName
-> [NamedArg A.Pattern]
-> Type
-> LHSResult
-> A.RHS
-> TCM (Maybe Term, WithFunctionProblem)
checkRHS i x aps t lhsResult@(LHSResult _ delta ps absurdPat trhs _ _asb _) rhs0 = handleRHS rhs0
where
handleRHS rhs =
case rhs of
A.RHS e _ -> Bench.billTo [Bench.Typing, Bench.CheckRHS] $ do
mv <- if absurdPat
then Nothing <$ setCurrentRange rhs (warning $ AbsurdPatternRequiresNoRHS ps)
else Just <$> checkExpr e (unArg trhs)
return (mv, NoWithFunction)
A.AbsurdRHS -> do
unless absurdPat $ typeError $ NoRHSRequiresAbsurdPattern aps
return (Nothing, NoWithFunction)
A.RewriteRHS [] strippedPats rhs wh -> checkWhere wh $ handleRHS rhs
A.RewriteRHS ((qname,eq):qes) strippedPats rhs wh -> do
st <- getTC
let recurse = do
st' <- getTC
let sameIP = (==) `on` (^.stInteractionPoints)
when (sameIP st st') $ putTC st
handleRHS $ A.RewriteRHS qes strippedPats rhs wh
(proof, eqt) <- inferExpr eq
solveSizeConstraints DefaultToInfty
t' <- reduce =<< instantiateFull eqt
(eqt,rewriteType,rewriteFrom,rewriteTo) <- equalityView t' >>= \case
eqt@(EqualityType _s _eq _params (Arg _ dom) a b) -> do
s <- inferSort dom
return (eqt, El s dom, unArg a, unArg b)
OtherType{} -> typeError . GenericDocError =<< do
"Cannot rewrite by equation of type" <+> prettyTCM t'
Con reflCon _ [] <- primRefl
reflInfo <- fmap (setOrigin Inserted) <$> getReflArgInfo reflCon
let reflPat = A.ConP (ConPatInfo ConOCon patNoRange ConPatEager) (unambiguous $ conName reflCon) $
maybeToList $ fmap (\ ai -> Arg ai $ unnamed $ A.WildP patNoRange) reflInfo
let isReflexive = tryConversion $ dontAssignMetas $
equalTerm rewriteType rewriteFrom rewriteTo
(pats, withExpr, withType) <- do
ifM isReflexive
(return ([ reflPat ], proof, OtherType t'))
(return ([ A.WildP patNoRange, reflPat ], proof, eqt))
let rhs' = insertPatterns pats rhs
(rhs'', outerWhere)
| null qes = (rhs', wh)
| otherwise = (A.RewriteRHS qes strippedPats rhs' wh, A.noWhereDecls)
cl = A.Clause (A.LHS i $ insertPatternsLHSCore pats $ A.LHSHead x $ killRange aps)
strippedPats rhs'' outerWhere False
reportSDoc "tc.rewrite" 60 $ vcat
[ "rewrite"
, " rhs' = " Pr.<> (text . show) rhs'
]
checkWithRHS x qname t lhsResult [withExpr] [withType] [cl]
A.WithRHS aux es cs -> do
reportSDoc "tc.with.top" 15 $ vcat
[ "TC.Rules.Def.checkclause reached A.WithRHS"
, sep $ prettyA aux : map (parens . prettyA) es
]
reportSDoc "tc.with.top" 20 $ do
nfv <- getCurrentModuleFreeVars
m <- currentModule
sep [ "with function module:" <+>
prettyList (map prettyTCM $ mnameToList m)
, text $ "free variables: " ++ show nfv
]
(vs0, as) <- unzip <$> mapM inferExprForWith es
solveSizeConstraints DefaultToInfty
checkWithRHS x aux t lhsResult vs0 (map OtherType as) cs
checkWithRHS
:: QName
-> QName
-> Type
-> LHSResult
-> [Term]
-> [EqualityView]
-> [A.Clause]
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS x aux t (LHSResult npars delta ps _absurdPat trhs _ _asb _) vs0 as cs = Bench.billTo [Bench.Typing, Bench.With] $ do
let withArgs = withArguments vs0 as
perm = fromMaybe __IMPOSSIBLE__ $ dbPatPerm ps
(vs, as) <- normalise (vs0, as)
reportSDoc "tc.with.top" 25 $ escapeContext (size delta) $ vcat
[ "delta =" <+> prettyTCM delta
]
reportSDoc "tc.with.top" 25 $ vcat
[ "vs =" <+> prettyTCM vs
, "as =" <+> prettyTCM as
, "perm =" <+> text (show perm)
]
(delta1, delta2, perm', t', as, vs) <- return $
splitTelForWith delta (unArg trhs) as vs
let finalPerm = composeP perm' perm
reportSLn "tc.with.top" 75 $ "delta = " ++ show delta
reportSDoc "tc.with.top" 25 $ escapeContext (size delta) $ vcat
[ "delta1 =" <+> prettyTCM delta1
, "delta2 =" <+> addContext delta1 (prettyTCM delta2)
]
reportSDoc "tc.with.top" 25 $ vcat
[ "perm' =" <+> text (show perm')
, "fPerm =" <+> text (show finalPerm)
]
us <- getContextArgs
let n = size us
m = size delta
(us0, us1') = splitAt (n - m) us
(us1, us2) = splitAt (size delta1) $ permute perm' us1'
v = Def aux $ map Apply $ us0 ++ us1 ++ map defaultArg withArgs ++ us2
addConstant aux =<< do
useTerPragma $ defaultDefn defaultArgInfo aux __DUMMY_TYPE__ emptyFunction
reportSDoc "tc.with.top" 20 $
" with arguments" <+> do escapeContext (size delta) $ addContext delta1 $ prettyList (map prettyTCM vs)
reportSDoc "tc.with.top" 20 $
" types" <+> do escapeContext (size delta) $ addContext delta1 $ prettyList (map prettyTCM as)
reportSDoc "tc.with.top" 20 $
"with function call" <+> prettyTCM v
reportSDoc "tc.with.top" 20 $
" context" <+> (prettyTCM =<< getContextTelescope)
reportSDoc "tc.with.top" 20 $
" delta" <+> do escapeContext (size delta) $ prettyTCM delta
reportSDoc "tc.with.top" 20 $
" delta1" <+> do escapeContext (size delta) $ prettyTCM delta1
reportSDoc "tc.with.top" 20 $
" delta2" <+> do escapeContext (size delta) $ addContext delta1 $ prettyTCM delta2
reportSDoc "tc.with.top" 20 $
" body" <+> prettyTCM v
return (Just v, WithFunction x aux t delta delta1 delta2 vs as t' ps npars perm' perm finalPerm cs)
checkWithFunction :: [Name] -> WithFunctionProblem -> TCM ()
checkWithFunction _ NoWithFunction = return ()
checkWithFunction cxtNames (WithFunction f aux t delta delta1 delta2 vs as b qs npars perm' perm finalPerm cs) = do
let
withSub :: Substitution
withSub = liftS (size delta2) (wkS (countWithArgs as) idS) `composeS` renaming __IMPOSSIBLE__ (reverseP perm')
reportSDoc "tc.with.top" 10 $ vcat
[ "checkWithFunction"
, nest 2 $ vcat
[ "delta1 =" <+> prettyTCM delta1
, "delta2 =" <+> addContext delta1 (prettyTCM delta2)
, "t =" <+> prettyTCM t
, "as =" <+> addContext delta1 (prettyTCM as)
, "vs =" <+> do addContext delta1 $ prettyTCM vs
, "b =" <+> do addContext delta1 $ addContext delta2 $ prettyTCM b
, "qs =" <+> do addContext delta $ prettyTCMPatternList qs
, "perm' =" <+> text (show perm')
, "perm =" <+> text (show perm)
, "fperm =" <+> text (show finalPerm)
, "withSub=" <+> text (show withSub)
]
]
delta1 <- normalise delta1
(withFunType, n) <- withFunctionType delta1 vs as delta2 b
reportSDoc "tc.with.type" 10 $ sep [ "with-function type:", nest 2 $ prettyTCM withFunType ]
reportSDoc "tc.with.type" 50 $ sep [ "with-function type:", nest 2 $ pretty withFunType ]
setCurrentRange cs $
traceCall NoHighlighting $
traceCall (CheckWithFunctionType withFunType) $
checkType withFunType
df <- safeInTopContext $ makeOpen =<< withDisplayForm f aux delta1 delta2 n qs perm' perm
reportSLn "tc.with.top" 20 "created with display form"
case dget df of
Display n ts dt ->
reportSDoc "tc.with.top" 20 $ "Display" <+> fsep
[ text (show n)
, prettyList $ map prettyTCM ts
, prettyTCM dt
]
addConstant aux =<< do
useTerPragma $ (defaultDefn defaultArgInfo aux withFunType emptyFunction)
{ defDisplay = [df] }
reportSDoc "tc.with.top" 10 $ sep
[ "added with function" <+> (prettyTCM aux) <+> "of type"
, nest 2 $ prettyTCM withFunType
, nest 2 $ "-|" <+> (prettyTCM =<< getContextTelescope)
]
reportSDoc "tc.with.top" 70 $ vcat
[ nest 2 $ text $ "raw with func. type = " ++ show withFunType
]
cs <- return $ map (A.lhsToSpine) cs
cs <- buildWithFunction cxtNames f aux t delta qs npars withSub finalPerm (size delta1) n cs
cs <- return $ map (A.spineToLhs) cs
checkFunDefS withFunType defaultArgInfo NotDelayed Nothing (Just f) info aux (Just withSub) cs
where
info = Info.mkDefInfo (nameConcrete $ qnameName aux) noFixity' PublicAccess ConcreteDef (getRange cs)
checkWhere
:: A.WhereDeclarations
-> TCM a
-> TCM a
checkWhere wh@(A.WhereDecls whmod ds) ret = do
ensureNoNamedWhereInRefinedContext whmod
loop ds
where
loop ds = case ds of
[] -> ret
[A.ScopedDecl scope ds] -> withScope_ scope $ loop ds
[A.Section _ m tel ds] -> newSection m tel $ do
localTC (\ e -> e { envCheckingWhere = True }) $ do
checkDecls ds
ret
_ -> __IMPOSSIBLE__
ensureNoNamedWhereInRefinedContext Nothing = return ()
ensureNoNamedWhereInRefinedContext (Just m) = traceCall (CheckNamedWhere m) $ do
args <- map unArg <$> (moduleParamsToApply =<< currentModule)
unless (isWeakening args) $
genericDocError =<< do
names <- map (argNameToString . fst . unDom) . telToList <$>
(lookupSection =<< currentModule)
let pr x v = text (x ++ " =") <+> prettyTCM v
vcat
[ fsep (pwords $ "Named where-modules are not allowed when module parameters have been refined by pattern matching. " ++
"See https://github.com/agda/agda/issues/2897.")
, text $ "In this case the module parameter" ++
(if length args > 0 then "s have" else " has") ++
" been refined to"
, nest 2 $ vcat (zipWith pr names args) ]
where
isWeakening [] = True
isWeakening (Var i [] : args) = isWk (i - 1) args
where
isWk i [] = True
isWk i (Var j [] : args) = i == j && isWk (i - 1) args
isWk _ _ = False
isWeakening _ = False
newSection :: ModuleName -> A.GeneralizeTelescope -> TCM a -> TCM a
newSection m gtel@(A.GeneralizeTel _ tel) cont = do
reportSDoc "tc.section" 10 $
"checking section" <+> prettyTCM m <+> fsep (map prettyA tel)
checkGeneralizeTelescope gtel $ \ _ tel' -> do
reportSDoc "tc.section" 10 $
"adding section:" <+> prettyTCM m <+> text (show (size tel'))
addSection m
reportSDoc "tc.section" 10 $ inTopContext $
nest 4 $ "actual tele:" <+> do prettyTCM =<< lookupSection m
withCurrentModule m cont
atClause :: QName -> Int -> A.RHS -> TCM a -> TCM a
atClause name i rhs = localTC $ \ e -> e { envClause = IPClause name i rhs }