module Agda.TypeChecking.Rules.Def where
import Prelude hiding (mapM)
import Control.Applicative
import Control.Monad.State hiding (mapM)
import Control.Monad.Reader hiding (mapM)
import Control.Monad hiding (mapM)
import Data.List hiding (sort)
import Data.Traversable
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Agda.Utils.IO.Locale as LocIO
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.SizedTypes
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Rules.Term ( checkExpr, inferExpr, checkTelescope_, isType_ )
import Agda.TypeChecking.Rules.LHS ( checkLeftHandSide )
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 =
traceCall (CheckFunDef (getRange i) (qnameName name) cs) $ do
t <- typeOfConst name
rel <- relOfConst name
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)
]
let check c = do
c <- applyRelevanceToContext rel $ checkClause t c
solveSizeConstraints
return c
cs <- mapM check cs
unless (allEqual $ map (npats . translatedClause) cs) $
typeError DifferentArities
reportSDoc "tc.cc" 15 $ do
sep [ text "clauses before rebindClause"
, nest 2 $ prettyTCM (map (NamedClause name . translatedClause) cs)
]
cs <- instantiateFull =<< mapM rebindClause cs
inv <- checkInjectivity name $ map translatedClause cs
reportSDoc "tc.cc" 15 $ do
sep [ text "clauses before compilation"
, nest 2 $ prettyTCM (map (NamedClause name . translatedClause) cs)
]
let cc = compileClauses 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
$ Function
{ funClauses = cs
, funCompiled = cc
, funDelayed = delayed
, funInv = inv
, funAbstr = Info.defAbstract i
, funPolarity = []
, funArgOccurrences = []
, funProjection = Nothing
}
computePolarity name
reportSDoc "tc.def.fun" 10 $ do
sep [ text "added " <+> prettyTCM name <+> text ":"
, nest 2 $ prettyTCM . defType =<< getConstInfo name
]
checkCoverage name
reportSLn "tc.def.fun.compile" 10 $
"compiled clauses for " ++ show name ++ ":\n" ++ show cc
where
npats = size . clausePats
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 x aps ps) rhs ds)
= A.Clause (A.LHS i x aps (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
[A.Clause]
checkClause :: Type -> A.Clause -> TCM Clauses
checkClause t c@(A.Clause (A.LHS i x aps []) rhs0 wh) =
traceCall (CheckClause t c) $
checkLeftHandSide c aps t $ \gamma delta sub xs ps t' perm -> do
let mkBody v = foldr (\x t -> Bind $ Abs x t) (Body $ substs sub v) xs
(body, with) <- checkWhere (size delta) wh $ let
handleRHS rhs =
case rhs of
A.RHS e
| any (containsAbsurdPattern . namedThing . unArg) aps ->
typeError $ AbsurdPatternRequiresNoRHS aps
| otherwise -> do
v <- checkExpr e t'
return (mkBody v, NoWithFunction)
A.AbsurdRHS
| any (containsAbsurdPattern . namedThing . unArg) 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 -> return $ case eq of
Lam Hidden (Abs _ (Def equality _)) -> equality
Def equality _ -> equality
_ -> __IMPOSSIBLE__
reflCon <- primRefl >>= \refl -> return $ case refl of
Con reflCon [] -> reflCon
_ -> __IMPOSSIBLE__
(rewriteType,rewriteFrom,rewriteTo) <- case t' of
El _Set0 (Def equality' [Arg Hidden Relevant rewriteType,
Arg NotHidden Relevant rewriteFrom, Arg NotHidden Relevant rewriteTo])
| equality' == equality ->
return (rewriteType, rewriteFrom, rewriteTo)
El _Set0 (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.MetaInfo noRange emptyScopeInfo Nothing
underscore = A.Underscore metaInfo
[rewriteFromExpr,rewriteToExpr,rewriteTypeExpr, proofExpr] <-
disableDisplayForms $ setShowImplicitArguments True $ reify
[rewriteFrom, rewriteTo, rewriteType , proof]
let (inner, outer)
| null eqs = ([], wh)
| otherwise = (wh, [])
newRhs = A.WithRHS qname [rewriteFromExpr, proofExpr]
[A.Clause (A.LHS i 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 $
text (show c)
vas <- mapM inferExpr 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 $ vcat
[ text "delta =" <+> prettyTCM delta
, text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> addCtxTel delta1 (prettyTCM delta2)
, text "vs =" <+> prettyTCM vs
, text "as =" <+> prettyTCM as
]
ctx <- getContextTelescope
let n = size ctx
m = size delta
us = [ Arg h r (Var i []) | (i, Arg h r _) <- zip [n 1,n 2..0] $ telToList ctx ]
(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 $ rename (reverseP perm') t'
(vs, as) <- do
let var = flip Var []
rho = replicate (size delta2) __IMPOSSIBLE__ ++ map var [0..]
return $ substs rho $ rename (reverseP perm') (vs, as)
reportSDoc "tc.with.top" 20 $ vcat
[ text " with arguments" <+> prettyList (map prettyTCM vs)
, text " types" <+> prettyList (map prettyTCM as)
, text "with function call" <+> prettyTCM v
, text " context" <+> (prettyTCM =<< getContextTelescope)
, text " delta" <+> prettyTCM delta
, text " fv" <+> text (show fv)
, text " body" <+> (addCtxTel delta $ prettyTCM $ mkBody v)
]
return (mkBody v, WithFunction x aux gamma delta1 delta2 vs as t' ps 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
]
]
translateRecordPatterns $
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 cs) = do
reportSDoc "tc.with.top" 10 $ vcat
[ text "checkWithFunction"
, nest 2 $ vcat
[ text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> prettyTCM delta2
, text "gamma =" <+> prettyTCM gamma
, text "as =" <+> addCtxTel delta1 (prettyTCM as)
, text "vs =" <+> addCtxTel delta1 (prettyTCM vs)
, text "b =" <+> prettyTCM b
, text "qs =" <+> text (show qs)
, 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 ]
absAuxType <- setShowImplicitArguments True
$ disableDisplayForms
$ dontReifyInteractionPoints
$ reify candidateType
reportSDoc "tc.with.top" 15 $
vcat [ text "type of with function:"
, nest 2 $ prettyTCM absAuxType
]
auxType <- setCurrentRange (getRange cs) $ isType_ $ killRange absAuxType
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 $ Axiom Nothing Nothing)
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
liftIO $ LocIO.putStrLn $ "checking where section " ++ show dx ++ " " ++ show dtel
liftIO $ LocIO.putStrLn $ " actual tele: " ++ show dtel'
x <- withCurrentModule m $ checkDecls ds >> ret
return x
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 . namedThing . unArg) ps
A.DefP _ _ _ -> __IMPOSSIBLE__
actualConstructor :: MonadTCM tcm => QName -> tcm QName
actualConstructor c = do
v <- constructorForm =<< normalise (Con c [])
case v of
Con c _ -> return c
_ -> actualConstructor =<< stripLambdas v
where
stripLambdas v = case v of
Con c _ -> return c
Lam h b -> do
x <- freshName_ $ absName b
addCtx x (Arg h Relevant $ sort Prop) $ stripLambdas (absBody b)
_ -> typeError $ GenericError $ "Not a constructor: " ++ show c