module Agda.TypeChecking.Rules.Def where
import Prelude hiding (mapM)
import Control.Arrow ((***), (&&&))
import Control.Applicative
import Control.Monad.State hiding (mapM)
import Control.Monad.Reader hiding (mapM)
import Control.Monad.Error hiding (mapM)
import Control.Monad hiding (mapM)
import Data.Function
import Data.List hiding (sort)
import Data.Traversable
import Data.Set (Set)
import qualified Data.Set as Set
import Agda.Syntax.Common
import Agda.Syntax.Position
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Internal
import qualified Agda.Syntax.Info as Info
import qualified Agda.Syntax.Abstract.Pretty as A
import Agda.Syntax.Fixity
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Info
import Agda.Syntax.Scope.Base (emptyScopeInfo)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (primRefl, primEquality)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Empty
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Rebind
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.With
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.Polarity
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.CompiledClause (CompiledClauses(..))
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Rules.Term ( checkExpr, inferExpr, inferExprForWith, inferOrCheck, checkTelescope_, isType_ )
import Agda.TypeChecking.Rules.LHS ( checkLeftHandSide )
import Agda.TypeChecking.Rules.LHS.Implicit ( insertImplicitPatterns )
import Agda.TypeChecking.Rules.Decl ( checkDecls )
import Agda.TypeChecking.Rules.Data ( isCoinductive )
import Agda.Interaction.Options
import Agda.Utils.Tuple
import Agda.Utils.Size
import Agda.Utils.Function
import Agda.Utils.List
import Agda.Utils.Permutation
import Agda.Utils.Monad
#include "../../undefined.h"
import Agda.Utils.Impossible
checkFunDef :: Delayed -> Info.DefInfo -> QName -> [A.Clause] -> TCM ()
checkFunDef delayed i name cs = do
t <- typeOfConst name
rel <- relOfConst name
case trivialClause cs of
Just e | isMeta (ignoreSharing $ unEl t) ->
traceCall (CheckFunDef (getRange i) (qnameName name) cs) $
checkAlias t rel delayed i name e
_ -> checkFunDef' t rel delayed i name cs
where
isMeta MetaV{} = True
isMeta _ = False
trivialClause [A.Clause (A.LHS i (A.LHSHead f []) []) (A.RHS e) []] = Just e
trivialClause _ = Nothing
checkAlias :: Type -> Relevance -> Delayed -> Info.DefInfo -> QName -> A.Expr -> TCM ()
checkAlias t' rel 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, t) <- applyRelevanceToContext rel $ inferOrCheck e (Just t')
reportSDoc "tc.def.alias" 20 $ text "checkAlias: finished checking"
solveSizeConstraints
v <- instantiateFull v
addConstant name $ Defn rel name t [] [] (defaultDisplayForm name) 0 noCompiledRep
$ Function
{ funClauses = [Clause (getRange i) EmptyTel (idP 0) [] $ Body v]
, funCompiled = Done [] v
, funDelayed = delayed
, funInv = NotInjective
, funAbstr = Info.defAbstract i
, funMutual = []
, funProjection = Nothing
, funStatic = False
, funCopy = False
, funTerminates = Nothing
}
reportSDoc "tc.def.alias" 20 $ text "checkAlias: leaving"
checkFunDef' :: Type -> Relevance -> Delayed -> Info.DefInfo -> QName -> [A.Clause] -> TCM ()
checkFunDef' t rel delayed 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 <- trailingImplicits t cs
let check c = do
c <- applyRelevanceToContext rel $ checkClause t c
solveSizeConstraints
return c
cs <- traceCall NoHighlighting $
mapM check cs
unless (allEqual $ map npats cs) $ typeError DifferentArities
reportSDoc "tc.cc" 15 $ do
sep [ text "clauses before rebindClause"
, nest 2 $ prettyTCM (map (QNamed name) cs)
]
cs <- instantiateFull =<< mapM rebindClause cs
inv <- checkInjectivity name cs
reportSDoc "tc.cc" 15 $ do
sep [ text "clauses before compilation"
, nest 2 $ prettyTCM (map (QNamed name) cs)
]
cc <- compileClauses (Just (name, t)) cs
reportSDoc "tc.cc" 10 $ do
sep [ text "compiled clauses of" <+> prettyTCM name
, nest 2 $ text (show cc)
]
addConstant name $ Defn rel name t [] [] (defaultDisplayForm name) 0 noCompiledRep
$ Function
{ funClauses = cs
, funCompiled = cc
, funDelayed = delayed
, funInv = inv
, funAbstr = Info.defAbstract i
, funMutual = []
, funProjection = Nothing
, funStatic = False
, funCopy = False
, funTerminates = Nothing
}
reportSDoc "tc.def.fun" 10 $ do
sep [ text "added " <+> prettyTCM name <+> text ":"
, nest 2 $ prettyTCM . defType =<< getConstInfo name
]
where
npats = size . clausePats
trailingImplicits :: Type -> [A.Clause] -> TCM [A.Clause]
trailingImplicits t [] = __IMPOSSIBLE__
trailingImplicits t cs@(c:_) = do
pps@((ps,ips):_) <- mapM splitTrailingImplicits cs
TelV tel t0 <- telView t
let
nh = genericLength $ filter ((NotHidden ==) . argHiding) ps
l = dropNonHidden nh $ telToList tel
is = takeWhile ((NotHidden /=) . domHiding) l
itel = telFromList is
ipss = map snd pps
ipss <- mapM (\ ps -> insertImplicitPatterns DontExpandLast ps itel) ipss
let longest = head $ sortBy (compare `on` ((0) . length)) ipss
pps' = zip (map fst pps) ipss
return $ zipWith (patchUpTrailingImplicits longest) pps' cs
dropNonHidden :: Nat -> [Dom (String, Type)] -> [Dom (String, Type)]
dropNonHidden 0 l = l
dropNonHidden n l = case dropWhile ((NotHidden /=) . domHiding) l of
[] -> []
(_:l) -> dropNonHidden (n1) l
splitTrailingImplicits :: A.Clause -> TCM (A.Patterns, A.Patterns)
splitTrailingImplicits (A.Clause (A.LHS _ A.LHSProj{} []) _ _) =
typeError $ NotImplemented "type checking definitions by copatterns"
splitTrailingImplicits (A.Clause (A.LHS _ _ ps@(_ : _)) _ _) =
typeError $ UnexpectedWithPatterns ps
splitTrailingImplicits (A.Clause (A.LHS _ (A.LHSHead _ aps) []) _ _) = do
let (ips, ps) = span ((Hidden==) . argHiding) $ reverse aps
return (reverse ps, reverse ips)
patchUpTrailingImplicits :: A.Patterns -> (A.Patterns, A.Patterns) -> A.Clause -> A.Clause
patchUpTrailingImplicits should (ps, is) c | length is >= length should = c
patchUpTrailingImplicits should (ps, is) (A.Clause (A.LHS i (A.LHSHead x aps) []) rhs0 wh) =
let imp = Arg Hidden Relevant $ Named Nothing $ A.ImplicitP $
Info.PatRange noRange
imps = replicate (length should length is) imp
in A.Clause (A.LHS i (A.LHSHead x (ps ++ is ++ imps)) []) rhs0 wh
patchUpTrailingImplicits _ _ _ = __IMPOSSIBLE__
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)
= A.Clause (A.LHS i lhscore (pats ++ ps)) (insertPatterns pats rhs) ds
insertPatterns pats (A.RewriteRHS qs eqs rhs wh) = A.RewriteRHS qs eqs (insertPatterns pats rhs) wh
insertPatterns pats rhs = rhs
data WithFunctionProblem
= NoWithFunction
| WithFunction QName
QName
Telescope
Telescope
Telescope
[Term]
[Type]
Type
[Arg Pattern]
Permutation
Permutation
[A.Clause]
checkClause :: Type -> A.Clause -> TCM Clause
checkClause t c@(A.Clause (A.LHS i (A.LHSProj{}) []) rhs0 wh) =
typeError $ NotImplemented "type checking definitions by copatterns"
checkClause t c@(A.Clause (A.LHS i (A.LHSHead x aps) []) rhs0 wh) =
traceCall (CheckClause t c) $
checkLeftHandSide (CheckPatternShadowing c) aps t $ \ mgamma delta sub xs ps t' perm -> do
let mkBody v = foldr (\x t -> Bind $ Abs x t) (Body $ applySubst sub v) xs
TelV htel t0 <- telViewUpTo' (1) ((Hidden==) . domHiding) t'
let n = size htel
(body, with) <- addCtxTel htel $ checkWhere (size delta + n) wh $ escapeContext (size htel) $ let
handleRHS rhs =
case rhs of
A.RHS e
| any (containsAbsurdPattern . namedArg) aps ->
typeError $ AbsurdPatternRequiresNoRHS aps
| otherwise -> do
v <- checkExpr e t'
return (mkBody v, NoWithFunction)
A.AbsurdRHS
| any (containsAbsurdPattern . namedArg) aps
-> return (NoBody, NoWithFunction)
| otherwise -> typeError $ NoRHSRequiresAbsurdPattern aps
A.RewriteRHS [] (_:_) _ _ -> __IMPOSSIBLE__
A.RewriteRHS (_:_) [] _ _ -> __IMPOSSIBLE__
A.RewriteRHS [] [] rhs [] -> handleRHS rhs
A.RewriteRHS [] [] _ (_:_) -> __IMPOSSIBLE__
A.RewriteRHS (qname:names) (eq:eqs) rhs wh -> do
(proof,t) <- inferExpr eq
t' <- reduce =<< instantiateFull t
equality <- primEquality >>= \eq ->
let lamV (Lam h b) = ((h:) *** id) $ lamV (unAbs b)
lamV (Shared p) = lamV (derefPtr p)
lamV v = ([], v) in
return $ case lamV eq of
([Hidden, Hidden], Def equality _) -> equality
([Hidden], Def equality _) -> equality
([], Def equality _) -> equality
_ -> __IMPOSSIBLE__
reflCon <- primRefl >>= \refl -> return $ case ignoreSharing refl of
Con reflCon [] -> reflCon
_ -> __IMPOSSIBLE__
(rewriteType,rewriteFrom,rewriteTo) <- case ignoreSharing $ unEl t' of
Def equality' [_level, Arg Hidden Relevant rewriteType,
Arg NotHidden Relevant rewriteFrom, Arg NotHidden Relevant rewriteTo]
| equality' == equality ->
return (rewriteType, rewriteFrom, rewriteTo)
_ -> do
err <- text "Cannot rewrite by equation of type" <+> prettyTCM t'
typeError $ GenericError $ show err
let info = PatRange noRange
metaInfo = Info.emptyMetaInfo
underscore = A.Underscore metaInfo
[rewriteFromExpr,rewriteToExpr,rewriteTypeExpr, proofExpr] <-
disableDisplayForms $ withShowAllArguments $ reify
[rewriteFrom, rewriteTo, rewriteType , proof]
let (inner, outer)
| null eqs = ([], wh)
| otherwise = (wh, [])
newRhs = A.WithRHS qname [rewriteFromExpr, proofExpr]
[A.Clause (A.LHS i (A.LHSHead x aps) pats)
(A.RewriteRHS names eqs (insertPatterns pats rhs) inner)
outer]
pats = [A.DotP info underscore,
A.ConP info (AmbQ [reflCon]) []]
reportSDoc "tc.rewrite.top" 25 $ vcat
[ text "from = " <+> prettyTCM rewriteFromExpr,
text "to = " <+> prettyTCM rewriteToExpr,
text "typ = " <+> prettyTCM rewriteType,
text "proof = " <+> prettyTCM proofExpr,
text "equ = " <+> prettyTCM t' ]
handleRHS newRhs
A.WithRHS aux es cs -> do
reportSDoc "tc.with.top" 5 $
text "TC.Rules.Def.checkclause reached A.WithRHS"
reportSDoc "tc.with.top" 30 $
prettyA c
vas <- mapM inferExprForWith es
(vs0, as) <- instantiateFull (unzip vas)
(vs, as) <- normalise (vs0, as)
m <- currentModule
reportSDoc "tc.with.top" 20 $ text "with function module:" <+> prettyList (map prettyTCM $ mnameToList m)
let fv = allVars $ freeVars (vs, as)
SplitTel delta1 delta2 perm' = splitTelescope fv delta
finalPerm = composeP perm' perm
reportSDoc "tc.with.top" 25 $ escapeContext (size delta) $ vcat
[ text "delta =" <+> prettyTCM delta
, text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> addCtxTel delta1 (prettyTCM delta2)
]
reportSDoc "tc.with.top" 25 $ vcat
[ text "vs =" <+> prettyTCM vs
, text "as =" <+> prettyTCM as
, text "perm' =" <+> text (show perm')
, 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 $ us0 ++ us1 ++ (map defaultArg vs0) ++ us2
t' <- return $ renameP (reverseP perm') t'
(vs, as) <- do
let
rho = parallelS (replicate (size delta2) __IMPOSSIBLE__)
return $ applySubst rho $ renameP (reverseP perm') (vs, as)
reportSDoc "tc.with.top" 20 $ vcat
[ text " with arguments" <+> do escapeContext (size delta2) $ prettyList (map prettyTCM vs)
, text " types" <+> do escapeContext (size delta2) $ prettyList (map prettyTCM as)
, text "with function call" <+> prettyTCM v
, text " context" <+> (prettyTCM =<< getContextTelescope)
, text " delta" <+> do escapeContext (size delta) $ prettyTCM delta
, text " fv" <+> text (show fv)
, text " body" <+> (addCtxTel delta $ prettyTCM $ mkBody v)
]
gamma <- maybe (typeError $ NotImplemented "with clauses for functions with unfolding arity") return mgamma
return (mkBody v, WithFunction x aux gamma delta1 delta2 vs as t' ps perm' finalPerm cs)
in handleRHS 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
]
]
return $
Clause { clauseRange = getRange i
, clauseTel = killRange delta
, clausePerm = perm
, clausePats = ps
, clauseBody = body
}
checkClause t (A.Clause (A.LHS _ _ ps@(_ : _)) _ _) = typeError $ UnexpectedWithPatterns ps
checkWithFunction :: WithFunctionProblem -> TCM ()
checkWithFunction NoWithFunction = return ()
checkWithFunction (WithFunction f aux gamma delta1 delta2 vs as b qs perm' perm cs) = do
reportSDoc "tc.with.top" 10 $ vcat
[ text "checkWithFunction"
, nest 2 $ vcat
[ text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> addCtxTel delta1 (prettyTCM delta2)
, text "gamma =" <+> prettyTCM gamma
, text "as =" <+> addCtxTel delta1 (prettyTCM as)
, text "vs =" <+> 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)
]
]
df <- makeClosed <$> withDisplayForm f aux delta1 delta2 (size as) qs perm'
reportSLn "tc.with.top" 20 "created with display form"
candidateType <- withFunctionType delta1 vs as delta2 b
reportSDoc "tc.with.type" 10 $ sep [ text "candidate type:", nest 2 $ prettyTCM candidateType ]
reportSDoc "tc.with.type" 50 $ sep [ text "candidate type:", nest 2 $ text $ show candidateType ]
absAuxType <- withShowAllArguments
$ disableDisplayForms
$ dontReifyInteractionPoints
$ reify candidateType
reportSDoc "tc.with.type" 15 $
vcat [ text "type of with function:"
, nest 2 $ prettyTCM absAuxType
]
reportSDoc "tc.with.type" 50 $
vcat [ text "type of with function:"
, nest 2 $ text $ show absAuxType
]
auxType <- setCurrentRange (getRange cs)
(traceCall NoHighlighting $
isType_ $ killRange absAuxType)
`catchError` \err -> case err of
TypeError s e -> put s >> enterClosure e (traceCall (CheckWithFunctionType absAuxType) . typeError)
_ -> throwError err
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 (Defn Relevant aux auxType [] [] [df] 0 noCompiledRep Axiom)
solveSizeConstraints
reportSDoc "tc.with.top" 10 $ sep
[ text "added with function" <+> (prettyTCM aux) <+> text "of type"
, nest 2 $ prettyTCM auxType
, nest 2 $ text "-|" <+> (prettyTCM =<< getContextTelescope)
]
cs <- buildWithFunction aux gamma qs perm (size delta1) (size as) cs
checkFunDef NotDelayed info aux cs
where
info = Info.mkDefInfo (nameConcrete $ qnameName aux) defaultFixity' PublicAccess ConcreteDef (getRange cs)
checkWhere :: Nat -> [A.Declaration] -> TCM a -> TCM a
checkWhere _ [] ret = ret
checkWhere n [A.ScopedDecl scope ds] ret = withScope_ scope $ checkWhere n ds ret
checkWhere n [A.Section _ m tel ds] ret = do
checkTelescope_ tel $ \tel' -> do
reportSDoc "tc.def.where" 10 $
text "adding section:" <+> prettyTCM m <+> text (show (size tel')) <+> text (show n)
addSection m (size tel' + n)
verboseS "tc.def.where" 10 $ do
dx <- prettyTCM m
dtel <- mapM prettyA tel
dtel' <- prettyTCM =<< lookupSection m
reportSLn "" 0 $ "checking where section " ++ show dx ++ " " ++ show dtel
reportSLn "" 0 $ " actual tele: " ++ show dtel'
withCurrentModule m $ checkDecls ds >> ret
checkWhere _ _ _ = __IMPOSSIBLE__
containsAbsurdPattern :: A.Pattern -> Bool
containsAbsurdPattern p = case p of
A.AbsurdP _ -> True
A.VarP _ -> False
A.WildP _ -> False
A.ImplicitP _ -> False
A.DotP _ _ -> False
A.LitP _ -> False
A.AsP _ _ p -> containsAbsurdPattern p
A.ConP _ _ ps -> any (containsAbsurdPattern . namedArg) ps
A.DefP _ _ _ -> __IMPOSSIBLE__
A.PatternSynP _ _ _ -> __IMPOSSIBLE__
actualConstructor :: QName -> TCM QName
actualConstructor c = do
v <- constructorForm =<< normalise (Con c [])
case ignoreSharing v of
Con c _ -> return c
_ -> actualConstructor =<< stripLambdas v
where
stripLambdas v = case ignoreSharing v of
Con c _ -> return c
Lam h b -> do
x <- freshName_ $ absName b
addCtx x (Dom h Relevant $ sort Prop) $ stripLambdas (absBody b)
_ -> typeError $ GenericError $ "Not a constructor: " ++ show c