{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Def where
import Prelude hiding ( mapM, null )
import Control.Arrow (first,second)
import Control.Monad.State hiding (forM, mapM)
import Data.Function
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Maybe
import Data.Traversable (forM, mapM)
import Data.Semigroup (Semigroup((<>)))
import Data.Tuple ( swap )
import Agda.Interaction.Options
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete as C
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.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.Reduce
import Agda.TypeChecking.Patterns.Abstract (expandPatternSynonyms)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
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.Rewriting.Confluence
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 {-# SOURCE #-} Agda.TypeChecking.Rules.Decl ( checkDecls )
import Agda.Utils.Except ( MonadError(catchError) )
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.Permutation
import Agda.Utils.Pretty ( prettyShow )
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
import Agda.Utils.Impossible
checkFunDef :: Delayed -> A.DefInfo -> QName -> [A.Clause] -> TCM ()
checkFunDef delayed i name cs = do
def <- instantiateDef =<< getConstInfo name
let t = defType def
let info = getArgInfo def
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
let ismacro = isMacro . theDef $ def
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 -> A.DefInfo -> QName -> A.Expr -> Maybe C.Expr -> TCM ()
checkAlias t ai delayed i name e mc =
let clause = A.Clause { clauseLHS = A.SpineLHS (LHSInfo (getRange i) NoEllipsis) name []
, clauseStrippedPats = []
, clauseRHS = A.RHS e mc
, clauseWhereDecls = A.noWhereDecls
, clauseCatchall = False } in
atClause name 0 t Nothing clause $ 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
, clauseEllipsis = NoEllipsis
} ]
, 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
-> A.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
-> A.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 t withSub 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
]
applyCohesionToContext ai $ applyQuantityToContext ai $ do
(cs,sys) <- if not isSystem then return (cs, Nothing) else do
fullType <- flip abstract t <$> getContextTelescope
sys <- unsafeInTopContext $ checkSystemCoverage name (IntSet.toList 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
, clauseEllipsis = NoEllipsis
}
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, _recordExpressionBecameCopatternLHS, cc) <- Bench.billTo [Bench.Coverage] $
unsafeInTopContext $ 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
whenM (optConfluenceCheck <$> pragmaOptions) $ inTopContext $
forM_ (zip cs [0..]) $ \(c , clauseNo) ->
checkConfluenceOfClause name clauseNo c
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
, funCovering = covering
}
useTerPragma $
updateDefCopatternLHS (const $ hasProjectionPatterns cc) $
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 <- viewTC eTerminationCheck
let terminates = case tc of
NonTerminating -> Just False
Terminating -> Just True
_ -> Nothing
reportS "tc.fundef" 30 $
[ "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 :: [WithHiding (Term, 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 :: IntSet
}
instance Semigroup ClausesPostChecks where
CPC xs <> CPC xs' = CPC (IntSet.union xs xs')
instance Monoid ClausesPostChecks where
mempty = CPC empty
mappend = (<>)
checkClauseLHS :: Type -> Maybe Substitution -> A.SpineClause -> (LHSResult -> TCM a) -> TCM a
checkClauseLHS t withSub c@(A.Clause lhs@(A.SpineLHS i x aps) strippedPats rhs0 wh catchall) ret = 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
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 (CheckLHS lhs) (Just x) aps t withSub strippedPats ret
checkClause
:: Type
-> Maybe Substitution
-> A.SpineClause
-> TCM (Clause,ClausesPostChecks)
checkClause t withSub c@(A.Clause lhs@(A.SpineLHS i x aps) strippedPats rhs0 wh catchall) = do
cxtNames <- reverse . map (fst . unDom) <$> getContext
checkClauseLHS t withSub c $ \ 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
unsafeInTopContext $ 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 CmpLeq $ unArg trhs
Nothing -> return ()
reportSDoc "tc.lhs.top" 10 $ vcat
[ "Clause before translation:"
, nest 2 $ vcat
[ "delta =" <+> do unsafeEscapeContext (size delta) $ prettyTCM delta
, "ps =" <+> do P.fsep <$> prettyTCMPatterns ps
, "body =" <+> maybe "_|_" prettyTCM body
, "type =" <+> prettyTCM t
]
]
reportSDoc "tc.lhs.top" 60 $ unsafeEscapeContext (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 getRelevance
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
, clauseEllipsis = lhsEllipsis i
}
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 :: A.RHS -> TCM (Maybe Term, WithFunctionProblem)
handleRHS rhs = case rhs of
A.RHS e _ -> ordinaryRHS e
A.AbsurdRHS -> noRHS
A.RewriteRHS eqs ps rhs wh -> rewriteEqnsRHS eqs ps rhs wh
A.WithRHS aux es cs -> withRHS aux es cs
ordinaryRHS :: A.Expr -> TCM (Maybe Term, WithFunctionProblem)
ordinaryRHS e = Bench.billTo [Bench.Typing, Bench.CheckRHS] $ do
mv <- if absurdPat
then Nothing <$ setCurrentRange e (warning $ AbsurdPatternRequiresNoRHS ps)
else Just <$> checkExpr e (unArg trhs)
return (mv, NoWithFunction)
noRHS :: TCM (Maybe Term, WithFunctionProblem)
noRHS = do
unless absurdPat $ typeError $ NoRHSRequiresAbsurdPattern aps
return (Nothing, NoWithFunction)
withRHS :: QName
-> [WithHiding A.Expr]
-> [A.Clause]
-> TCM (Maybe Term, WithFunctionProblem)
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
]
vtys <- mapM (traverse (fmap OtherType <.> inferExprForWith)) es
solveSizeConstraints DefaultToInfty
checkWithRHS x aux t lhsResult vtys cs
rewriteEqnsRHS :: [A.RewriteEqn] -> [A.ProblemEq] -> A.RHS -> A.WhereDeclarations -> TCM (Maybe Term, WithFunctionProblem)
rewriteEqnsRHS [] strippedPats rhs wh = checkWhere wh $ handleRHS rhs
rewriteEqnsRHS (r:rs) strippedPats rhs wh = case r of
Rewrite ((qname, eq) : qes) ->
rewriteEqnRHS qname eq (case qes of { [] -> rs; _ -> Rewrite qes : rs })
Invert _ [] -> __IMPOSSIBLE__
Invert qname pes -> invertEqnRHS qname pes rs
Rewrite [] -> __IMPOSSIBLE__
where
invertEqnRHS :: QName -> [(A.Pattern,A.Expr)] -> [A.RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
invertEqnRHS qname pes rs = do
let (pats, es) = unzip pes
vtys <- mapM (WithHiding NotHidden <.> fmap OtherType <.> inferExprForWith) es
solveSizeConstraints DefaultToInfty
let rhs' = insertPatterns pats rhs
(rhs'', outerWhere)
| null rs = (rhs', wh)
| otherwise = (A.RewriteRHS rs strippedPats rhs' wh, A.noWhereDecls)
cl = A.Clause (A.LHS i $ insertPatternsLHSCore pats $ A.LHSHead x $ killRange aps)
strippedPats rhs'' outerWhere False
reportSDoc "tc.invert" 60 $ vcat
[ text "invert"
, " rhs' = " <> (text . show) rhs'
]
checkWithRHS x qname t lhsResult vtys [cl]
rewriteEqnRHS :: QName -> A.Expr
-> [A.RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
rewriteEqnRHS qname eq rs = do
st <- getTC
let recurse = do
st' <- getTC
let sameIP = (==) `on` (^.stInteractionPoints)
when (sameIP st st') $ putTC st
handleRHS $ A.RewriteRHS rs 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 rs = (rhs', wh)
| otherwise = (A.RewriteRHS rs 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
[ text "rewrite"
, " rhs' = " <> (text . show) rhs'
]
checkWithRHS x qname t lhsResult [WithHiding NotHidden (withExpr, withType)] [cl]
checkWithRHS
:: QName
-> QName
-> Type
-> LHSResult
-> [WithHiding (Term, EqualityView)]
-> [A.Clause]
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS x aux t (LHSResult npars delta ps _absurdPat trhs _ _asb _) vtys0 cs =
Bench.billTo [Bench.Typing, Bench.With] $ do
let withArgs = withArguments vtys0
perm = fromMaybe __IMPOSSIBLE__ $ dbPatPerm ps
vtys0 <- normalise vtys0
reportSDoc "tc.with.top" 25 $ unsafeEscapeContext (size delta) $ vcat
[ "delta =" <+> prettyTCM delta
]
reportSDoc "tc.with.top" 25 $ vcat $
let (vs, as) = unzipWith whThing vtys0 in
[ "vs =" <+> prettyTCM vs
, "as =" <+> prettyTCM as
, "perm =" <+> text (show perm)
]
let (delta1, delta2, perm', t', vtys) = splitTelForWith delta (unArg trhs) vtys0
let finalPerm = composeP perm' perm
reportSLn "tc.with.top" 75 $ "delta = " ++ show delta
reportSDoc "tc.with.top" 25 $ unsafeEscapeContext (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'
mkWithArg = \ (WithHiding h e) -> setHiding h $ defaultArg e
v = Def aux $ map Apply $ us0 ++ us1 ++ map mkWithArg withArgs ++ us2
addConstant aux =<< do
useTerPragma $ defaultDefn defaultArgInfo aux __DUMMY_TYPE__ emptyFunction
reportSDoc "tc.with.top" 20 $ vcat $
let (vs, as) = unzipWith whThing vtys in
[ " with arguments" <+> do unsafeEscapeContext (size delta) $ addContext delta1 $ prettyList (map prettyTCM vs)
, " types" <+> do unsafeEscapeContext (size delta) $ addContext delta1 $ prettyList (map prettyTCM as)
, "with function call" <+> prettyTCM v
, " context" <+> (prettyTCM =<< getContextTelescope)
, " delta" <+> do unsafeEscapeContext (size delta) $ prettyTCM delta
, " delta1" <+> do unsafeEscapeContext (size delta) $ prettyTCM delta1
, " delta2" <+> do unsafeEscapeContext (size delta) $ addContext delta1 $ prettyTCM delta2
, " body" <+> prettyTCM v
]
return (Just v, WithFunction x aux t delta delta1 delta2 vtys t' ps npars perm' perm finalPerm cs)
checkWithFunction :: [Name] -> WithFunctionProblem -> TCM ()
checkWithFunction _ NoWithFunction = return ()
checkWithFunction cxtNames (WithFunction f aux t delta delta1 delta2 vtys b qs npars perm' perm finalPerm cs) = do
let
withSub :: Substitution
withSub = let as = map (snd . whThing) vtys in
liftS (size delta2) (wkS (countWithArgs as) idS)
`composeS` renaming __IMPOSSIBLE__ (reverseP perm')
reportSDoc "tc.with.top" 10 $ vcat
[ "checkWithFunction"
, nest 2 $ vcat $
let (vs, as) = unzipWith whThing vtys in
[ "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 vtys 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 <- inTopContext $ 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 -> Type -> Maybe Substitution -> A.SpineClause -> TCM a -> TCM a
atClause name i t sub cl ret = do
clo <- buildClosure ()
localTC (\ e -> e { envClause = IPClause name i t sub cl clo [] }) ret