module Agda.TypeChecking.Rules.Def where
import Prelude hiding (mapM)
import Control.Arrow ((***))
import Control.Applicative
import Control.Monad.State hiding (forM, mapM)
import Control.Monad.Reader hiding (forM, mapM)
import Data.Function
import Data.List hiding (sort)
import Data.Maybe
import Data.Traversable
import Agda.Syntax.Common
import Agda.Syntax.Concrete (exprFieldA)
import Agda.Syntax.Position
import qualified Agda.Syntax.Abstract 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.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Patterns.Abstract (expandPatternSynonyms)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.TypeChecking.CheckInternal (checkType)
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.CompiledClause (CompiledClauses(..))
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Rules.Term ( checkExpr, inferExpr, inferExprForWith, checkDontExpandLast, checkTelescope )
import Agda.TypeChecking.Rules.LHS ( checkLeftHandSide, LHSResult(..) )
import Agda.TypeChecking.Rules.Decl ( checkDecls )
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.Lens
import Agda.Utils.Maybe ( whenNothing )
import Agda.Utils.Monad
import Agda.Utils.Permutation
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, x) ->
traceCall (CheckFunDef (getRange i) (qnameName name) cs) $ do
whenM (isFrozen x) $ unfreezeMeta x
checkAlias t info delayed i name e
_ -> checkFunDef' t info delayed Nothing Nothing i name cs
isAlias :: [A.Clause] -> Type -> Maybe (A.Expr, MetaId)
isAlias cs t =
case trivialClause cs of
Just e | Just x <- isMeta (ignoreSharing $ unEl t) -> Just (e, 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 _ = Nothing
checkAlias :: Type -> ArgInfo -> Delayed -> Info.DefInfo -> QName -> A.Expr -> TCM ()
checkAlias t' ai delayed i name e = do
reportSDoc "tc.def.alias" 10 $ text "checkAlias" <+> vcat
[ text (show name) <+> colon <+> prettyTCM t'
, text (show name) <+> equals <+> prettyTCM e
]
v <- applyRelevanceToContext (getRelevance ai) $ checkDontExpandLast e t'
let t = t'
reportSDoc "tc.def.alias" 20 $ text "checkAlias: finished checking"
solveSizeConstraints DontDefaultToInfty
v <- instantiateFull v
let bodyMod = case getRelevance ai of
Irrelevant -> dontCare
_ -> id
addConstant name $ defaultDefn ai name t
$ Function
{ funClauses = [ Clause
{ clauseRange = getRange i
, clauseTel = EmptyTel
, namedClausePats = []
, clauseBody = Body $ 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
}
reportSDoc "tc.def.alias" 20 $ text "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 =
traceCall (CheckFunDef (getRange i) (qnameName name) cs) $ do
reportSDoc "tc.def.fun" 10 $
sep [ text "checking body of" <+> prettyTCM name
, nest 2 $ text ":" <+> prettyTCM t
, nest 2 $ text "full type:" <+> (prettyTCM . defType =<< getConstInfo name)
]
cs <- return $ map A.lhsToSpine cs
cs <- traceCall NoHighlighting $ do
forM cs $ \ c -> do
c <- applyRelevanceToContext (argInfoRelevance ai) $ do
checkClause t c
whenNothing extlam $ solveSizeConstraints DontDefaultToInfty
addClauses name [c]
return c
modifyFunClauses name (const [])
reportSDoc "tc.cc" 25 $ do
sep [ text "clauses before injectivity test"
, nest 2 $ prettyTCM $ map (QNamed name) cs
]
reportSDoc "tc.cc" 60 $ do
sep [ text "raw clauses: "
, nest 2 $ sep $ map (text . show . QNamed name) cs
]
cs <- instantiateFull cs
reportSLn "tc.inj.def" 20 $ "checkFunDef': checking injectivity..."
inv <- Bench.billTo [Bench.Injectivity] $
checkInjectivity name cs
reportSDoc "tc.cc" 15 $ do
sep [ text "clauses before compilation"
, nest 2 $ sep $ map (prettyTCM . QNamed name) cs
]
addClauses name cs
cc <- Bench.billTo [Bench.Coverage] $
compileClauses (Just (name, t)) cs
reportSDoc "tc.cc" 10 $ do
sep [ text "compiled clauses of" <+> prettyTCM name
, nest 2 $ text (show cc)
]
addConstant name =<< do
useTerPragma $ defaultDefn ai name t $
Function
{ 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
}
reportSDoc "tc.def.fun" 10 $ do
sep [ text "added " <+> prettyTCM name <+> text ":"
, nest 2 $ prettyTCM . defType =<< getConstInfo name
]
where
npats = size . clausePats
useTerPragma :: Definition -> TCM Definition
useTerPragma def@Defn{ defName = name, theDef = fun@Function{}} = do
tc <- asks envTerminationCheck
let terminates = case tc of
NonTerminating -> Just False
Terminating -> Just True
_ -> Nothing
reportSLn "tc.fundef" 30 $ unlines $
[ "funTerminates of " ++ show 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 (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
insertPatterns pats (A.RewriteRHS qes rhs wh) = A.RewriteRHS qes (insertPatterns pats rhs) wh
insertPatterns pats rhs = rhs
data WithFunctionProblem
= NoWithFunction
| WithFunction
{ wfParentName :: QName
, wfName :: QName
, wfParentType :: Type
, wfBeforeTel :: Telescope
, wfAfterTel :: Telescope
, wfExprs :: [Term]
, wfExprTypes :: [EqualityView]
, wfRHSType :: Type
, wfParentPats :: [NamedArg Pattern]
, wfPermSplit :: Permutation
, wfPermParent :: Permutation
, wfPermFinal :: Permutation
, wfClauses :: [A.Clause]
}
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] ]
checkClause
:: Type
-> A.SpineClause
-> TCM Clause
checkClause t c@(A.Clause (A.SpineLHS i x aps withPats) 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
(body, with) <- checkWhere (unArg trhs) wh $ checkRHS i x aps t lhsResult rhs0
escapeContext (size delta) $ checkWithFunction 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
]
]
rel <- asks envRelevance
let bodyMod body = case rel of
Irrelevant -> dontCare <$> body
_ -> body
return $
Clause { clauseRange = getRange i
, clauseTel = killRange delta
, namedClausePats = numberPatVars perm ps
, clauseBody = bodyMod body
, clauseType = Just trhs
, clauseCatchall = catchall
}
checkRHS
:: LHSInfo
-> QName
-> [NamedArg A.Pattern]
-> Type
-> LHSResult
-> A.RHS
-> TCM (ClauseBody, WithFunctionProblem)
checkRHS i x aps t lhsResult@(LHSResult delta ps trhs perm) rhs0 = handleRHS rhs0
where
absurdPat = any (containsAbsurdPattern . namedArg) aps
handleRHS rhs =
case rhs of
A.RHS e -> do
when absurdPat $ typeError $ AbsurdPatternRequiresNoRHS aps
v <- checkExpr e $ unArg trhs
return (mkBody perm v, NoWithFunction)
A.AbsurdRHS -> do
unless absurdPat $ typeError $ NoRHSRequiresAbsurdPattern aps
return (NoBody, NoWithFunction)
A.RewriteRHS [] rhs [] -> handleRHS rhs
A.RewriteRHS [] rhs wh -> checkWhere (unArg trhs) wh $ handleRHS rhs
A.RewriteRHS ((qname,eq):qes) rhs wh -> do
st <- get
let recurse = do
st' <- get
let sameIP = (==) `on` (^.stInteractionPoints)
when (sameIP st st') $ put st
handleRHS $ A.RewriteRHS qes rhs wh
(proof, eqt) <- inferExpr eq
solveSizeConstraints DefaultToInfty
t' <- reduce =<< instantiateFull eqt
(eqt,rewriteType,rewriteFrom,rewriteTo) <- equalityView t' >>= \case
eqt@(EqualityType s _eq _level dom a b) -> return (eqt, El s (unArg dom), unArg a, unArg b)
OtherType{} -> typeError . GenericDocError =<< do
text "Cannot rewrite by equation of type" <+> prettyTCM t'
Con reflCon [] <- ignoreSharing <$> primRefl
let isReflProof = do
v <- reduce proof
case ignoreSharing v of
Con c [] | c == reflCon -> return True
_ -> return False
ifM isReflProof recurse $ do
let reflPat = A.ConP (ConPatInfo ConPCon patNoRange) (AmbQ [conName reflCon]) []
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 rhs' wh, [])
cs = [A.Clause (A.LHS i (A.LHSHead x (killRange aps)) pats) rhs'' outerWhere False]
checkWithRHS x qname t lhsResult [withExpr] [withType] cs
A.WithRHS aux es cs -> do
reportSDoc "tc.with.top" 15 $ vcat
[ text "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 [ text "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 (ClauseBody, WithFunctionProblem)
checkWithRHS x aux t (LHSResult delta ps trhs perm) vs0 as cs = do
let withArgs = withArguments vs0 as
(vs, as) <- normalise (vs0, as)
reportSDoc "tc.with.top" 25 $ escapeContext (size delta) $ vcat
[ text "delta =" <+> prettyTCM delta
]
reportSDoc "tc.with.top" 25 $ vcat
[ text "vs =" <+> prettyTCM vs
, text "as =" <+> prettyTCM as
, text "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
[ text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> addCtxTel delta1 (prettyTCM delta2)
]
reportSDoc "tc.with.top" 25 $ vcat
[ text "perm' =" <+> text (show perm')
, text "fPerm =" <+> text (show finalPerm)
]
us <- getContextArgs
let n = size us
m = size delta
(us0, us1') = genericSplitAt (n m) us
(us1, us2) = genericSplitAt (size delta1) $ permute perm' us1'
v = Def aux $ map Apply $ us0 ++ us1 ++ map defaultArg withArgs ++ us2
body = mkBody perm v
addConstant aux =<< do
useTerPragma $ defaultDefn defaultArgInfo aux typeDontCare emptyFunction
reportSDoc "tc.with.top" 20 $
text " with arguments" <+> do escapeContext (size delta) $ addContext delta1 $ prettyList (map prettyTCM vs)
reportSDoc "tc.with.top" 20 $
text " types" <+> do escapeContext (size delta) $ addContext delta1 $ prettyList (map prettyTCM as)
reportSDoc "tc.with.top" 20 $
text "with function call" <+> prettyTCM v
reportSDoc "tc.with.top" 20 $
text " context" <+> (prettyTCM =<< getContextTelescope)
reportSDoc "tc.with.top" 20 $
text " delta" <+> do escapeContext (size delta) $ prettyTCM delta
reportSDoc "tc.with.top" 20 $
text " body" <+> (addCtxTel delta $ prettyTCM body)
return (body, WithFunction x aux t delta1 delta2 vs as t' ps perm' perm finalPerm cs)
checkWithFunction :: WithFunctionProblem -> TCM ()
checkWithFunction NoWithFunction = return ()
checkWithFunction (WithFunction f aux t delta1 delta2 vs as b qs perm' perm finalPerm cs) = do
reportSDoc "tc.with.top" 10 $ vcat
[ text "checkWithFunction"
, nest 2 $ vcat
[ text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> addCtxTel 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 "perm' =" <+> text (show perm')
, text "perm =" <+> text (show perm)
, text "fperm =" <+> text (show finalPerm)
]
]
delta1 <- normalise delta1
(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 ]
setCurrentRange cs
(traceCall NoHighlighting $
checkType withFunType)
`catchError` \err -> case err of
TypeError s e -> do
put s
wt <- reify withFunType
enterClosure e $ do
traceCall (CheckWithFunctionType wt) . typeError
err -> throwError err
df <- makeClosed <$> 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
]
addConstant aux =<< do
useTerPragma $ (defaultDefn defaultArgInfo aux withFunType emptyFunction)
{ defDisplay = [df] }
reportSDoc "tc.with.top" 10 $ sep
[ text "added with function" <+> (prettyTCM aux) <+> text "of type"
, nest 2 $ prettyTCM withFunType
, nest 2 $ text "-|" <+> (prettyTCM =<< getContextTelescope)
]
cs <- return $ map (A.lhsToSpine) cs
cs <- buildWithFunction f aux t qs finalPerm (size delta1) n cs
cs <- return $ map (A.spineToLhs) cs
checkFunDef' withFunType defaultArgInfo NotDelayed Nothing (Just f) info aux cs
where
info = Info.mkDefInfo (nameConcrete $ qnameName aux) noFixity' PublicAccess ConcreteDef (getRange cs)
checkWhere
:: Type
-> [A.Declaration]
-> TCM a
-> TCM a
checkWhere trhs ds ret0 = do
TelV htel _ <- telViewUpTo' (1) (not . visible) trhs
let
ret = escapeContext (size htel) $ ret0
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
checkDecls ds
ret
_ -> __IMPOSSIBLE__
addCtxTel htel $ loop ds
containsAbsurdPattern :: A.Pattern -> Bool
containsAbsurdPattern p = case p of
A.AbsurdP _ -> True
A.VarP _ -> False
A.WildP _ -> 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
A.PatternSynP _ _ _ -> __IMPOSSIBLE__