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.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
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 <- checkClause t c
solveSizeConstraints
return c
cs <- mapM check cs
unless (allEqual $ map npats cs) $ typeError DifferentArities
cs <- mapM rebindClause cs
inv <- checkInjectivity name cs
addConstant name $ Defn name t (defaultDisplayForm name) 0
$ Function
{ funClauses = cs
, funDelayed = delayed
, funInv = inv
, funAbstr = Info.defAbstract i
, funPolarity = []
, funArgOccurrences = []
}
computePolarity name
verboseS "tc.def.fun" 10 $ do
dx <- prettyTCM name
t' <- prettyTCM . defType =<< getConstInfo name
liftIO $ LocIO.putStrLn $ "added " ++ show dx ++ " : " ++ show t'
checkCoverage name
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 Clause
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
_ -> __IMPOSSIBLE__
reflCon <- primRefl >>= \refl -> return $ case refl of
Lam Hidden (Abs _typ (Lam Hidden (Abs _val (Con reflCon [])))) -> reflCon
_ -> __IMPOSSIBLE__
(rewriteType,rewriteFrom,rewriteTo) <- case t' of
El _Set0 (Def equality' [Arg Hidden rewriteType,
Arg NotHidden rewriteFrom, Arg NotHidden rewriteTo])
| equality' == equality ->
return (rewriteType, rewriteFrom, rewriteTo)
El _Set0 (Def equality' [_level,Arg Hidden rewriteType,
Arg NotHidden rewriteFrom, Arg NotHidden 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] <- 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
vas <- mapM inferExpr es
(vs, as) <- instantiateFull $ unzip vas
m <- currentModule
reportSDoc "tc.with.top" 20 $ text "with function module:" <+> prettyList (map prettyTCM $ mnameToList m)
let fv = allVars $ freeVars vs
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)
]
ctx <- getContextTelescope
let n = size ctx
m = size delta
us = [ Arg h (Var i []) | (i, Arg h _) <- 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 (Arg NotHidden) vs) ++ 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)
]
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 $ vcat
[ text "Final clause:"
, nest 2 $ vcat
[ text "delta =" <+> prettyTCM delta
, text "perm =" <+> text (show perm)
, text "ps =" <+> text (show ps)
, text "body =" <+> text (show 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 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 =" <+> prettyTCM as
, text "vs =" <+> 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 aux auxType [df] 0 $ Axiom 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 $ sort Prop) $ stripLambdas (absBody b)
_ -> typeError $ GenericError $ "Not a constructor: " ++ show c