summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Rules/Def.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Rules/Def.hs')
-rw-r--r--src/full/Agda/TypeChecking/Rules/Def.hs336
1 files changed, 202 insertions, 134 deletions
diff --git a/src/full/Agda/TypeChecking/Rules/Def.hs b/src/full/Agda/TypeChecking/Rules/Def.hs
index 56b9782..381be77 100644
--- a/src/full/Agda/TypeChecking/Rules/Def.hs
+++ b/src/full/Agda/TypeChecking/Rules/Def.hs
@@ -1,6 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Def where
@@ -15,11 +13,14 @@ import Data.Function
import Data.List hiding (sort)
import Data.Maybe
import Data.Traversable
+import qualified Data.Set as Set
import Agda.Syntax.Common
+import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete (exprFieldA)
import Agda.Syntax.Position
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
@@ -48,9 +49,11 @@ import Agda.TypeChecking.SizedTypes.Solve
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.CompiledClause (CompiledClauses(..))
import Agda.TypeChecking.CompiledClause.Compile
+import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Rules.Term ( checkExpr, inferExpr, inferExprForWith, checkDontExpandLast, checkTelescope )
-import Agda.TypeChecking.Rules.LHS ( checkLeftHandSide, LHSResult(..) )
+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) )
@@ -59,6 +62,7 @@ import Agda.Utils.Maybe ( whenNothing )
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size
+import Agda.Utils.Functor
#include "undefined.h"
import Agda.Utils.Impossible
@@ -73,33 +77,49 @@ checkFunDef delayed i name cs = do
t <- typeOfConst name
info <- flip setRelevance defaultArgInfo <$> relOfConst name
case isAlias cs t of
- Just (e, x) ->
+ Just (e, mc, x) ->
traceCall (CheckFunDef (getRange i) (qnameName name) cs) $ do
-- Andreas, 2012-11-22: if the alias is in an abstract block
-- it has been frozen. We unfreeze it to enable type inference.
-- See issue 729.
whenM (isFrozen x) $ unfreezeMeta x
- checkAlias t info delayed i name e
+ checkAlias t info delayed i name e mc
_ -> checkFunDef' t info delayed Nothing Nothing i name cs
+ -- If it's a macro check that it ends in Term → TC ⊤
+ ismacro <- isMacro . theDef <$> getConstInfo name
+ when (ismacro || Info.defMacro i == MacroDef) $ checkMacroType t
+
+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 [ text "Result type of a macro must be"
+ , nest 2 $ prettyTCM expectedType ]
+
-- | A single clause without arguments and without type signature is an alias.
-isAlias :: [A.Clause] -> Type -> Maybe (A.Expr, MetaId)
+isAlias :: [A.Clause] -> Type -> Maybe (A.Expr, Maybe C.Expr, MetaId)
isAlias cs t =
case trivialClause cs of
-- if we have just one clause without pattern matching and
-- without a type signature, then infer, to allow
-- "aliases" for things starting with hidden abstractions
- Just e | Just x <- isMeta (ignoreSharing $ unEl t) -> Just (e, x)
+ Just (e, mc) | Just x <- isMeta (ignoreSharing $ 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) [] _] = Just e
+ trivialClause [A.Clause (A.LHS i (A.LHSHead f []) []) _ (A.RHS e mc) [] _] = Just (e, mc)
trivialClause _ = Nothing
-- | Check a trivial definition of the form @f = e@
-checkAlias :: Type -> ArgInfo -> Delayed -> Info.DefInfo -> QName -> A.Expr -> TCM ()
-checkAlias t' ai delayed i name e = do
+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 $ text "checkAlias" <+> vcat
[ text (show name) <+> colon <+> prettyTCM t'
, text (show name) <+> equals <+> prettyTCM e
@@ -132,29 +152,19 @@ checkAlias t' ai delayed i name e = do
-- Add the definition
addConstant name $ defaultDefn ai name t
- $ Function
- { funClauses = [ Clause -- trivial clause @name = v@
+ $ set funMacro (Info.defMacro i == MacroDef) $
+ emptyFunction
+ { funClauses = [ Clause -- trivial clause @name = v@
{ clauseRange = getRange i
, clauseTel = EmptyTel
, namedClausePats = []
- , clauseBody = Body $ bodyMod v
+ , clauseBody = Just $ bodyMod v
, clauseType = Just $ Arg ai t
, clauseCatchall = False
} ]
- , funCompiled = Just $ Done [] $ bodyMod v
- , funTreeless = Nothing
- , funDelayed = delayed
- , funInv = NotInjective
- , funAbstr = Info.defAbstract i
- , funMutual = []
- , funProjection = Nothing
- , funSmashable = True
- , funStatic = False
- , funInline = False
- , funTerminates = Nothing
- , funExtLam = Nothing
- , funWith = Nothing
- , funCopatternLHS = False
+ , funCompiled = Just $ Done [] $ bodyMod v
+ , funDelayed = delayed
+ , funAbstr = Info.defAbstract i
}
reportSDoc "tc.def.alias" 20 $ text "checkAlias: leaving"
@@ -171,6 +181,21 @@ checkFunDef' :: Type -- ^ the type we expect the function to have
-> [A.Clause] -- ^ the clauses to check
-> TCM ()
checkFunDef' t ai delayed extlam with i name cs =
+ checkFunDefS t ai delayed extlam with i name Nothing cs
+
+-- | Type check a definition by pattern matching.
+checkFunDefS :: Type -- ^ the type we expect the function to have
+ -> ArgInfo -- ^ is it irrelevant (for instance)
+ -> Delayed -- ^ are the clauses delayed (not unfolded willy-nilly)
+ -> Maybe ExtLamInfo -- ^ does the definition come from an extended lambda
+ -- (if so, we need to know some stuff about lambda-lifted args)
+ -> Maybe QName -- ^ is it a with function (if so, what's the name of the parent function)
+ -> Info.DefInfo -- ^ range info
+ -> QName -- ^ the name of the function
+ -> Maybe Substitution -- ^ substitution (from with abstraction) that needs to be applied to module parameters
+ -> [A.Clause] -- ^ the clauses to check
+ -> TCM ()
+checkFunDefS t ai delayed extlam with i name withSub cs =
traceCall (CheckFunDef (getRange i) (qnameName name) cs) $ do -- TODO!! (qnameName)
reportSDoc "tc.def.fun" 10 $
@@ -179,8 +204,14 @@ checkFunDef' t ai delayed extlam with i name cs =
, nest 2 $ text "full type:" <+> (prettyTCM . defType =<< getConstInfo name)
]
+ reportSDoc "tc.def.fun" 70 $
+ sep $ [ text "clauses:" ] ++ map (nest 2 . text . show . A.deepUnscope) cs
+
cs <- return $ map A.lhsToSpine cs
+ reportSDoc "tc.def.fun" 70 $
+ sep $ [ text "spine clauses:" ] ++ map (nest 2 . text . show . A.deepUnscope) cs
+
-- Ensure that all clauses have the same number of trailing hidden patterns
-- This is necessary since trailing implicits are no longer eagerly inserted.
-- Andreas, 2013-10-13
@@ -190,9 +221,10 @@ checkFunDef' t ai delayed extlam with i name cs =
-- Check the clauses
cs <- traceCall NoHighlighting $ do -- To avoid flicker.
- forM cs $ \ c -> do
+ forM (zip cs [0..]) $ \ (c, clauseNo) -> do
+ atClause name clauseNo (A.clauseRHS c) $ do
c <- applyRelevanceToContext (argInfoRelevance ai) $ do
- checkClause t c
+ checkClause t withSub c
-- Andreas, 2013-11-23 do not solve size constraints here yet
-- in case we are checking the body of an extended lambda.
-- 2014-04-24: The size solver requires each clause to be
@@ -201,17 +233,16 @@ checkFunDef' t ai delayed extlam with i name cs =
whenNothing extlam $ solveSizeConstraints DontDefaultToInfty
-- Andreas, 2013-10-27 add clause as soon it is type-checked
-- TODO: instantiateFull?
- addClauses name [c]
+ inTopContext $ addClauses name [c]
return c
+ reportSDoc "tc.def.fun" 70 $
+ sep $ [ text "checked clauses:" ] ++ map (nest 2 . text . show) cs
+
-- After checking, remove the clauses again.
-- (Otherwise, @checkInjectivity@ loops for issue 801).
modifyFunClauses name (const [])
- -- Check that all clauses have the same number of arguments
- -- unless (allEqual $ map npats cs) $ typeError DifferentArities
- -- Andreas, 2013-03-15 disable this check to allow flexible arity (issue 727)
-
reportSDoc "tc.cc" 25 $ do
sep [ text "clauses before injectivity test"
, nest 2 $ prettyTCM $ map (QNamed name) cs -- broken, reify (QNamed n cl) expect cl to live at top level
@@ -243,35 +274,34 @@ checkFunDef' t ai delayed extlam with i name cs =
]
-- add clauses for the coverage checker (needs to reduce)
- addClauses name cs
+ inTopContext $ addClauses name cs
+
+ fullType <- flip telePi t <$> getContextTelescope
-- Coverage check and compile the clauses
cc <- Bench.billTo [Bench.Coverage] $
- compileClauses (Just (name, t)) cs
+ inTopContext $ compileClauses (Just (name, fullType)) cs
reportSDoc "tc.cc" 10 $ do
sep [ text "compiled clauses of" <+> prettyTCM name
, nest 2 $ text (show cc)
]
+ -- The macro tag might be on the type signature
+ ismacro <- isMacro . theDef <$> getConstInfo name
+
-- Add the definition
- addConstant name =<< do
+ inTopContext $ addConstant name =<< do
-- If there was a pragma for this definition, we can set the
-- funTerminates field directly.
- useTerPragma $ defaultDefn ai name t $
- Function
+ useTerPragma $ defaultDefn ai name fullType $
+ set funMacro (ismacro || Info.defMacro i == MacroDef) $
+ emptyFunction
{ funClauses = cs
, funCompiled = Just cc
- , funTreeless = Nothing
, funDelayed = delayed
, funInv = inv
, funAbstr = Info.defAbstract i
- , funMutual = []
- , funProjection = Nothing
- , funSmashable = True
- , funStatic = False
- , funInline = False
- , funTerminates = Nothing
, funExtLam = extlam
, funWith = with
, funCopatternLHS = isCopatternLHS cs
@@ -284,8 +314,6 @@ checkFunDef' t ai delayed extlam with i name cs =
sep [ text "added " <+> prettyTCM name <+> text ":"
, nest 2 $ prettyTCM . defType =<< getConstInfo name
]
- where
- npats = size . clausePats
-- | Set 'funTerminates' according to termination info in 'TCEnv',
-- which comes from a possible termination pragma.
@@ -307,8 +335,8 @@ useTerPragma def = return def
-- | Insert some patterns in the in with-clauses LHS of the given RHS
insertPatterns :: [A.Pattern] -> A.RHS -> A.RHS
insertPatterns pats (A.WithRHS aux es cs) = A.WithRHS aux es (map insertToClause cs)
- where insertToClause (A.Clause (A.LHS i lhscore ps) rhs ds catchall)
- = A.Clause (A.LHS i lhscore (pats ++ ps)) (insertPatterns pats rhs) ds catchall
+ where insertToClause (A.Clause (A.LHS i lhscore ps) dots rhs ds catchall)
+ = A.Clause (A.LHS i lhscore (pats ++ ps)) dots (insertPatterns pats rhs) ds catchall
insertPatterns pats (A.RewriteRHS qes rhs wh) = A.RewriteRHS qes (insertPatterns pats rhs) wh
insertPatterns pats rhs = rhs
@@ -324,53 +352,74 @@ data WithFunctionProblem
, wfExprs :: [Term] -- ^ With and rewrite expressions.
, wfExprTypes :: [EqualityView] -- ^ Types of the with and rewrite expressions.
, wfRHSType :: Type -- ^ Type of the right hand side.
- , wfParentPats :: [NamedArg Pattern] -- ^ Parent patterns.
+ , wfParentPats :: [NamedArg DeBruijnPattern] -- ^ Parent patterns.
+ , wfParentParams :: Nat -- ^ Number of module parameters in parent patterns
, wfPermSplit :: Permutation -- ^ Permutation resulting from splitting the telescope into needed and unneeded vars.
, wfPermParent :: Permutation -- ^ Permutation reordering the variables in the parent pattern.
, wfPermFinal :: Permutation -- ^ Final permutation (including permutation for the parent clause).
, wfClauses :: [A.Clause] -- ^ The given clauses for the with function
}
--- | Create a clause body from a term.
---
--- As we have type checked the term in the clause telescope, but the final
--- body should have bindings in the order of the pattern variables,
--- we need to apply the permutation to the checked term.
-
-mkBody :: Permutation -> Term -> ClauseBody
-mkBody perm v = foldr (\ x t -> Bind $ Abs x t) b xs
- where
- b = Body $ applySubst (renamingR perm) v
- xs = [ stringToArgName $ "h" ++ show n | n <- [0 .. permRange perm - 1] ]
-
-
-- | Type check a function clause.
checkClause
:: Type -- ^ Type of function defined by this clause.
+ -> Maybe Substitution -- ^ Module parameter substitution arising from with-abstraction.
-> A.SpineClause -- ^ Clause.
-> TCM Clause -- ^ Type-checked clause.
-checkClause t c@(A.Clause (A.SpineLHS i x aps withPats) rhs0 wh catchall) = do
+checkClause t withSub c@(A.Clause (A.SpineLHS i x aps withPats) namedDots rhs0 wh catchall) = do
reportSDoc "tc.lhs.top" 30 $ text "Checking clause" $$ prettyA c
unless (null withPats) $
typeError $ UnexpectedWithPatterns withPats
traceCall (CheckClause t c) $ do
aps <- expandPatternSynonyms aps
- checkLeftHandSide (CheckPatternShadowing c) (Just x) aps t $ \ lhsResult@(LHSResult delta ps trhs perm) -> do
+ cxtNames <- reverse . map (fst . unDom) <$> getContext
+ when (not $ null namedDots) $ reportSDoc "tc.lhs.top" 50 $
+ text "namedDots:" <+> vcat [ prettyTCM x <+> text "=" <+> prettyTCM v <+> text ":" <+> prettyTCM a | A.NamedDot x v a <- namedDots ]
+ -- Not really an as-pattern, but this does the right thing.
+ bindAsPatterns [ AsB x v a | A.NamedDot x v a <- namedDots ] $
+ checkLeftHandSide (CheckPatternShadowing c) (Just x) aps t withSub $ \ lhsResult@(LHSResult npars delta ps trhs patSubst asb) -> do
-- Note that we might now be in irrelevant context,
-- in case checkLeftHandSide walked over an irrelevant projection pattern.
- (body, with) <- checkWhere (unArg trhs) wh $ checkRHS i x aps t lhsResult rhs0
- escapeContext (size delta) $ checkWithFunction with
+
+ -- Subtle: checkRHS expects the function type to be the lambda lifted
+ -- type. If we're checking a with-function that's already the case,
+ -- otherwise we need to abstract over the module telescope.
+ t' <- case withSub of
+ Just{} -> return t
+ Nothing -> do
+ theta <- lookupSection (qnameModule x)
+ return $ abstract theta t
+
+ -- At this point we should update the named dots potential with-clauses
+ -- in the right-hand side. When checking a clause we expect the named
+ -- dots to live in the context of the closest parent lhs, but the named
+ -- dots added by buildWithFunction live in the context of the
+ -- with-function arguments before pattern matching. That's what we need
+ -- patSubst for.
+ 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 rhs wh) = A.RewriteRHS qes (updateRHS rhs) wh
+
+ updateClause (A.Clause f dots rhs wh ca) = A.Clause f (applySubst patSubst dots) (updateRHS rhs) wh ca
+
+ (body, with) <- bindAsPatterns asb $ checkWhere wh $ checkRHS i x aps t' lhsResult rhs
+
+ -- Note that the with function doesn't necessarily share any part of
+ -- the context with the parent (but withSub will take you from parent
+ -- to child).
+ inTopContext $ Bench.billTo [Bench.Typing, Bench.With] $ checkWithFunction cxtNames with
reportSDoc "tc.lhs.top" 10 $ escapeContext (size delta) $ vcat
[ text "Clause before translation:"
, nest 2 $ vcat
[ text "delta =" <+> prettyTCM delta
- , text "perm =" <+> text (show perm)
, text "ps =" <+> text (show ps)
, text "body =" <+> text (show body)
- , text "body =" <+> prettyTCM body
+ , text "body =" <+> maybe (text "_|_") prettyTCM body
]
]
@@ -383,7 +432,7 @@ checkClause t c@(A.Clause (A.SpineLHS i x aps withPats) rhs0 wh catchall) = do
return $
Clause { clauseRange = getRange i
, clauseTel = killRange delta
- , namedClausePats = numberPatVars perm ps
+ , namedClausePats = ps
, clauseBody = bodyMod body
, clauseType = Just trhs
, clauseCatchall = catchall
@@ -395,34 +444,33 @@ checkRHS
:: LHSInfo -- ^ Range of lhs.
-> QName -- ^ Name of function.
-> [NamedArg A.Pattern] -- ^ Patterns in lhs.
- -> Type -- ^ Type of function.
+ -> Type -- ^ Top-level type of function.
-> LHSResult -- ^ Result of type-checking patterns
-> A.RHS -- ^ Rhs to check.
- -> TCM (ClauseBody, WithFunctionProblem)
-
-checkRHS i x aps t lhsResult@(LHSResult delta ps trhs perm) rhs0 = handleRHS rhs0
+ -> TCM (Maybe Term, WithFunctionProblem)
+ -- Note: the as-bindings are already bound (in checkClause)
+checkRHS i x aps t lhsResult@(LHSResult _ delta ps trhs _ _asb) rhs0 = handleRHS rhs0
where
absurdPat = any (containsAbsurdPattern . namedArg) aps
handleRHS rhs =
case rhs of
-- Case: ordinary RHS
- A.RHS e -> do
+ A.RHS e _ -> Bench.billTo [Bench.Typing, Bench.CheckRHS] $ do
when absurdPat $ typeError $ AbsurdPatternRequiresNoRHS aps
v <- checkExpr e $ unArg trhs
- return (mkBody perm v, NoWithFunction)
+ return (Just v, NoWithFunction)
-- Case: no RHS
A.AbsurdRHS -> do
unless absurdPat $ typeError $ NoRHSRequiresAbsurdPattern aps
- return (NoBody, NoWithFunction)
+ return (Nothing, NoWithFunction)
-- Case: @rewrite@
- A.RewriteRHS [] rhs [] -> handleRHS rhs
-- Andreas, 2014-01-17, Issue 1402:
-- If the rewrites are discarded since lhs=rhs, then
-- we can actually have where clauses.
- A.RewriteRHS [] rhs wh -> checkWhere (unArg trhs) wh $ handleRHS rhs
+ A.RewriteRHS [] rhs wh -> checkWhere wh $ handleRHS rhs
A.RewriteRHS ((qname,eq):qes) rhs wh -> do
-- Action for skipping this rewrite.
@@ -462,7 +510,7 @@ checkRHS i x aps t lhsResult@(LHSResult delta ps trhs perm) rhs0 = handleRHS rhs
-- Get the name of builtin REFL.
- Con reflCon [] <- ignoreSharing <$> primRefl
+ Con reflCon _ [] <- ignoreSharing <$> primRefl
-- Andreas, 2014-05-17 Issue 1110:
-- Rewriting with @refl@ has no effect, but gives an
@@ -473,14 +521,14 @@ checkRHS i x aps t lhsResult@(LHSResult delta ps trhs perm) rhs0 = handleRHS rhs
let isReflProof = do
v <- reduce proof
case ignoreSharing v of
- Con c [] | c == reflCon -> return True
+ Con c _ [] | c == reflCon -> return True
_ -> return False
ifM isReflProof recurse $ {- else -} do
-- Process 'rewrite' clause like a suitable 'with' clause.
- let reflPat = A.ConP (ConPatInfo ConPCon patNoRange) (AmbQ [conName reflCon]) []
+ let reflPat = A.ConP (ConPatInfo ConOCon patNoRange) (AmbQ [conName reflCon]) []
-- Andreas, 2015-12-25 Issue #1740:
-- After the fix of #520, rewriting with a reflexive equation
@@ -499,7 +547,7 @@ checkRHS i x aps t lhsResult@(LHSResult delta ps trhs perm) rhs0 = handleRHS rhs
| otherwise = (A.RewriteRHS qes rhs' wh, [])
-- Andreas, 2014-03-05 kill range of copied patterns
-- since they really do not have a source location.
- cs = [A.Clause (A.LHS i (A.LHSHead x (killRange aps)) pats) rhs'' outerWhere False]
+ cs = [A.Clause (A.LHS i (A.LHSHead x (killRange aps)) pats) [] rhs'' outerWhere False]
checkWithRHS x qname t lhsResult [withExpr] [withType] cs
@@ -535,10 +583,11 @@ checkWithRHS
-> [Term] -- ^ With-expressions.
-> [EqualityView] -- ^ Types of with-expressions.
-> [A.Clause] -- ^ With-clauses to check.
- -> TCM (ClauseBody, WithFunctionProblem)
-
-checkWithRHS x aux t (LHSResult delta ps trhs perm) vs0 as cs = do
+ -> TCM (Maybe Term, WithFunctionProblem)
+ -- Note: as-bindings already bound (in checkClause)
+checkWithRHS x aux t (LHSResult npars delta ps 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)
-- Andreas, 2012-09-17: for printing delta,
@@ -564,7 +613,7 @@ checkWithRHS x aux t (LHSResult delta ps trhs perm) vs0 as cs = do
-- we should remove it from the context first
reportSDoc "tc.with.top" 25 $ escapeContext (size delta) $ vcat
[ text "delta1 =" <+> prettyTCM delta1
- , text "delta2 =" <+> addCtxTel delta1 (prettyTCM delta2)
+ , text "delta2 =" <+> addContext delta1 (prettyTCM delta2)
]
reportSDoc "tc.with.top" 25 $ vcat
[ text "perm' =" <+> text (show perm')
@@ -583,7 +632,6 @@ checkWithRHS x aux t (LHSResult delta ps trhs perm) vs0 as cs = do
(us1, us2) = genericSplitAt (size delta1) $ permute perm' us1'
-- Now stuff the with arguments in between and finish with the remaining variables
v = Def aux $ map Apply $ us0 ++ us1 ++ map defaultArg withArgs ++ us2
- body = mkBody perm v
-- Andreas, 2013-02-26 add with-name to signature for printing purposes
addConstant aux =<< do
useTerPragma $ defaultDefn defaultArgInfo aux typeDontCare emptyFunction
@@ -600,27 +648,36 @@ checkWithRHS x aux t (LHSResult delta ps trhs perm) vs0 as cs = do
reportSDoc "tc.with.top" 20 $
text " delta" <+> do escapeContext (size delta) $ prettyTCM delta
reportSDoc "tc.with.top" 20 $
- text " body" <+> (addCtxTel delta $ prettyTCM body)
+ text " delta1" <+> do escapeContext (size delta) $ prettyTCM delta1
+ reportSDoc "tc.with.top" 20 $
+ text " delta2" <+> do escapeContext (size delta) $ addContext delta1 $ prettyTCM delta2
+ reportSDoc "tc.with.top" 20 $
+ text " body" <+> prettyTCM v
+
+ return (Just v, WithFunction x aux t delta1 delta2 vs as t' ps npars perm' perm finalPerm cs)
- return (body, WithFunction x aux t delta1 delta2 vs as t' ps perm' perm finalPerm cs)
+checkWithFunction :: [Name] -> WithFunctionProblem -> TCM ()
+checkWithFunction _ NoWithFunction = return ()
+checkWithFunction cxtNames (WithFunction f aux t delta1 delta2 vs as b qs npars perm' perm finalPerm cs) = do
-checkWithFunction :: WithFunctionProblem -> TCM ()
-checkWithFunction NoWithFunction = return ()
-checkWithFunction (WithFunction f aux t delta1 delta2 vs as b qs perm' perm finalPerm cs) = do
+ let -- Δ₁ ws Δ₂ ⊢ withSub : Δ′ (where Δ′ is the context of the parent lhs)
+ withSub :: Substitution
+ withSub = liftS (size delta2) (wkS (countWithArgs as) idS) `composeS` renaming __IMPOSSIBLE__ (reverseP perm')
reportSDoc "tc.with.top" 10 $ vcat
[ text "checkWithFunction"
, nest 2 $ vcat
[ text "delta1 =" <+> prettyTCM delta1
- , text "delta2 =" <+> addCtxTel delta1 (prettyTCM delta2)
+ , text "delta2 =" <+> addContext delta1 (prettyTCM delta2)
, text "t =" <+> prettyTCM t
- , text "as =" <+> addCtxTel delta1 (prettyTCM as)
- , text "vs =" <+> do addCtxTel delta1 $ prettyTCM vs
- , text "b =" <+> do addCtxTel delta1 $ addCtxTel delta2 $ prettyTCM b
- , text "qs =" <+> text (show qs)
+ , text "as =" <+> addContext delta1 (prettyTCM as)
+ , text "vs =" <+> do addContext delta1 $ prettyTCM vs
+ , text "b =" <+> do addContext delta1 $ addContext delta2 $ prettyTCM b
+ , text "qs =" <+> prettyList (map pretty qs)
, text "perm' =" <+> text (show perm')
, text "perm =" <+> text (show perm)
, text "fperm =" <+> text (show finalPerm)
+ , text "withSub=" <+> text (show withSub)
]
]
@@ -633,7 +690,7 @@ checkWithFunction (WithFunction f aux t delta1 delta2 vs as b qs perm' perm fina
-- from module applications.
(withFunType, n) <- withFunctionType delta1 vs as delta2 b
reportSDoc "tc.with.type" 10 $ sep [ text "with-function type:", nest 2 $ prettyTCM withFunType ]
- reportSDoc "tc.with.type" 50 $ sep [ text "with-function type:", nest 2 $ text $ show withFunType ]
+ reportSDoc "tc.with.type" 50 $ sep [ text "with-function type:", nest 2 $ pretty withFunType ]
-- Andreas, 2013-10-21
-- Check generated type directly in internal syntax.
@@ -648,19 +705,19 @@ checkWithFunction (WithFunction f aux t delta1 delta2 vs as b qs perm' perm fina
traceCall (CheckWithFunctionType wt) . typeError
err -> throwError err
-
-- With display forms are closed
- df <- makeClosed <$> withDisplayForm f aux delta1 delta2 n qs perm' perm
+ df <- makeGlobal =<< withDisplayForm f aux delta1 delta2 n qs perm' perm
reportSLn "tc.with.top" 20 "created with display form"
- case df of
- OpenThing _ (Display n ts dt) -> reportSDoc "tc.with.top" 20 $ text "Display" <+> fsep
- [ text (show n)
- , prettyList $ map prettyTCM ts
- , prettyTCM dt
- ]
+ case dget df of
+ Display n ts dt ->
+ reportSDoc "tc.with.top" 20 $ text "Display" <+> fsep
+ [ text (show n)
+ , prettyList $ map prettyTCM ts
+ , prettyTCM dt
+ ]
addConstant aux =<< do
useTerPragma $ (defaultDefn defaultArgInfo aux withFunType emptyFunction)
{ defDisplay = [df] }
@@ -671,50 +728,56 @@ checkWithFunction (WithFunction f aux t delta1 delta2 vs as b qs perm' perm fina
, nest 2 $ prettyTCM withFunType
, nest 2 $ text "-|" <+> (prettyTCM =<< getContextTelescope)
]
+ reportSDoc "tc.with.top" 70 $ vcat
+ [ nest 2 $ text $ "raw with func. type = " ++ show withFunType
+ ]
+
-- Construct the body for the with function
cs <- return $ map (A.lhsToSpine) cs
- cs <- buildWithFunction f aux t qs finalPerm (size delta1) n cs
+ cs <- buildWithFunction cxtNames f aux t qs npars withSub finalPerm (size delta1) n cs
cs <- return $ map (A.spineToLhs) cs
-- Check the with function
- checkFunDef' withFunType defaultArgInfo NotDelayed Nothing (Just f) info aux 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)
-- | Type check a where clause.
checkWhere
- :: Type -- ^ Type of rhs.
- -> [A.Declaration] -- ^ Where-declarations to check.
+ :: [A.Declaration] -- ^ Where-declarations to check.
-> TCM a -- ^ Continuation.
-> TCM a
-checkWhere trhs ds ret0 = do
- -- Temporarily add trailing hidden arguments to check where-declarations.
- TelV htel _ <- telViewUpTo' (-1) (not . visible) trhs
- let
- -- Remove htel after checking ds.
- ret = escapeContext (size htel) $ ret0
+checkWhere ds ret = loop ds
+ where
loop ds = case ds of
[] -> ret
[A.ScopedDecl scope ds] -> withScope_ scope $ loop ds
- [A.Section _ m tel ds] -> do
- checkTelescope tel $ \ tel' -> do
- reportSDoc "tc.def.where" 10 $
- text "adding section:" <+> prettyTCM m <+> text (show (size tel'))
- addSection m
- verboseS "tc.def.where" 10 $ do
- dx <- prettyTCM m
- dtel <- mapM prettyAs tel
- dtel' <- prettyTCM =<< lookupSection m
- reportSLn "tc.def.where" 10 $ "checking where section " ++ show dx ++ " " ++ show dtel
- reportSLn "tc.def.where" 10 $ " actual tele: " ++ show dtel'
- withCurrentModule m $ local (\ e -> e { envCheckingWhere = True }) $ do
+ [A.Section _ m tel ds] -> newSection m tel $ do
+ local (\ e -> e { envCheckingWhere = True }) $ do
checkDecls ds
ret
_ -> __IMPOSSIBLE__
- -- Add htel to check ds.
- addCtxTel htel $ loop ds
+
+-- | Enter a new section during type-checking.
+
+newSection :: ModuleName -> A.Telescope -> TCM a -> TCM a
+newSection m tel cont = do
+ reportSDoc "tc.section" 10 $
+ text "checking section" <+> prettyTCM m <+> fsep (map prettyAs tel)
+
+ checkTelescope tel $ \ tel' -> do
+ reportSDoc "tc.section" 10 $
+ text "adding section:" <+> prettyTCM m <+> text (show (size tel'))
+
+ addSection m
+
+ reportSDoc "tc.section" 10 $ inTopContext $
+ nest 4 $ text "actual tele:" <+> do prettyTCM =<< lookupSection m
+
+ withCurrentModule m cont
+
-- | Check if a pattern contains an absurd pattern. For instance, @suc ()@
containsAbsurdPattern :: A.Pattern -> Bool
@@ -722,10 +785,15 @@ containsAbsurdPattern p = case p of
A.AbsurdP _ -> True
A.VarP _ -> False
A.WildP _ -> False
- A.DotP _ _ -> False
+ A.DotP _ _ _ -> False
A.LitP _ -> False
A.AsP _ _ p -> containsAbsurdPattern p
A.ConP _ _ ps -> any (containsAbsurdPattern . namedArg) ps
A.RecP _ fs -> any (containsAbsurdPattern . (^. exprFieldA)) fs
- A.DefP _ _ _ -> False -- projection pattern
+ A.ProjP{} -> False
+ A.DefP _ _ ps -> any (containsAbsurdPattern . namedArg) ps
A.PatternSynP _ _ _ -> __IMPOSSIBLE__ -- False
+
+-- | Set the current clause number.
+atClause :: QName -> Int -> A.RHS -> TCM a -> TCM a
+atClause name i rhs = local $ \ e -> e { envClause = IPClause name i rhs }