module Agda.TypeChecking.Rules.Data where
import Control.Applicative
import Control.Monad
import Control.Monad.Trans
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.Syntax.Position
import qualified Agda.Syntax.Info as Info
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Polarity
import Agda.TypeChecking.Free
import Agda.TypeChecking.Forcing
import Agda.TypeChecking.Rules.Term ( isType_ )
import Agda.Interaction.Options
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "../../undefined.h"
import Agda.Utils.Impossible
checkDataDef :: Info.DefInfo -> QName -> [A.LamBinding] -> [A.Constructor] -> TCM ()
checkDataDef i name ps cs =
traceCall (CheckDataDef (getRange i) (qnameName name) ps cs) $ do
let npars = size ps
addSection (qnameToMName name) 0
t <- instantiateFull =<< typeOfConst name
dataDef <- bindParameters ps t $ \tel t0 -> do
let tel' = hideTel tel
(nofIxs, s) <- splitType =<< normalise t0
when (any (`freeIn` s) [0..nofIxs 1]) $ do
err <- fsep [ text "The sort of" <+> prettyTCM name
, text "cannot depend on its indices in the type"
, prettyTCM t0
]
typeError $ GenericError $ show err
s <- return $ raise (nofIxs) s
reportSDoc "tc.data.sort" 20 $ vcat
[ text "checking datatype" <+> prettyTCM name
, nest 2 $ vcat
[ text "type: " <+> prettyTCM t0
, text "sort: " <+> prettyTCM s
, text "indices:" <+> text (show nofIxs)
]
]
let dataDef = Datatype { dataPars = npars
, dataIxs = nofIxs
, dataInduction = Inductive
, dataClause = Nothing
, dataCons = []
, dataSort = s
, dataHsType = Nothing
, dataAbstr = Info.defAbstract i
, dataPolarity = []
, dataArgOccurrences = []
}
escapeContext (size tel) $ do
addConstant name ( Defn name t (defaultDisplayForm name) 0 dataDef )
mapM_ (checkConstructor name tel' nofIxs s) cs
return dataDef
let nofIxs = dataIxs dataDef
s = dataSort dataDef
do proofIrr <- proofIrrelevance
case (proofIrr, s, cs) of
(True, Prop, _:_:_) -> setCurrentRange (getRange $ map conName cs) $
typeError PropMustBeSingleton
where conName (A.Axiom _ c _) = c
conName (A.ScopedDecl _ (d:_)) = conName d
conName _ = __IMPOSSIBLE__
_ -> return ()
addConstant name (Defn name t (defaultDisplayForm name) 0 $
dataDef { dataCons = map cname cs }
)
computePolarity name
where
cname (A.ScopedDecl _ [d]) = cname d
cname (A.Axiom _ x _) = x
cname _ = __IMPOSSIBLE__
hideTel EmptyTel = EmptyTel
hideTel (ExtendTel (Arg _ r t) tel) = ExtendTel (Arg Hidden r t) $ hideTel <$> tel
splitType (El _ (Pi _ b)) = ((+ 1) -*- id) <$> splitType (absBody b)
splitType (El _ (Fun _ b)) = ((+ 1) -*- raise 1) <$> splitType b
splitType (El _ (Sort s)) = return (0, s)
splitType (El _ t) = typeError $ DataMustEndInSort t
checkConstructor :: QName -> Telescope -> Nat -> Sort
-> A.Constructor -> TCM ()
checkConstructor d tel nofIxs s (A.ScopedDecl scope [con]) = do
setScope scope
checkConstructor d tel nofIxs s con
checkConstructor d tel nofIxs s con@(A.Axiom i c e) =
traceCall (CheckConstructor d tel s con) $ do
t <- isType_ e
n <- size <$> getContextTelescope
debugEndsIn t d n
constructs n t d
debugFitsIn s
t `fitsIn` s
t' <- addForcingAnnotations t
escapeContext (size tel)
$ addConstant c
$ Defn c (telePi tel t') (defaultDisplayForm c) 0
$ Constructor (size tel) c d Nothing (Info.defAbstract i) Inductive
where
debugEndsIn t d n =
reportSDoc "tc.data.con" 15 $ vcat
[ sep [ text "checking that"
, nest 2 $ prettyTCM t
, text "ends in" <+> prettyTCM d
]
, nest 2 $ text "nofPars =" <+> text (show n)
]
debugFitsIn s =
reportSDoc "tc.data.con" 15 $ sep
[ text "checking that the type fits in"
, nest 2 $ prettyTCM s
]
checkConstructor _ _ _ _ _ = __IMPOSSIBLE__
bindParameters :: [A.LamBinding] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
bindParameters [] a ret = ret EmptyTel a
bindParameters (A.DomainFree h x : ps) (El _ (Pi (Arg h' Relevant a) b)) ret
| h /= h' =
__IMPOSSIBLE__
| otherwise = addCtx x arg $ bindParameters ps (absBody b) $ \tel s ->
ret (ExtendTel arg $ Abs (show x) tel) s
where
arg = Arg h Relevant a
bindParameters (A.DomainFree h x : ps) (El _ (Fun (Arg h' Relevant a) b)) ret
| h /= h' =
__IMPOSSIBLE__
| otherwise = addCtx x arg $ bindParameters ps (raise 1 b) $ \tel s ->
ret (ExtendTel arg $ Abs (show x) tel) s
where
arg = Arg h Relevant a
bindParameters _ _ _ = __IMPOSSIBLE__
fitsIn :: Type -> Sort -> TCM ()
fitsIn t s = do
t <- instantiateFull t
s' <- instantiateFull (getSort t)
reportSDoc "tc.data.fits" 10 $
sep [ text "does" <+> prettyTCM t
, text "of sort" <+> prettyTCM s'
, text "fit in" <+> prettyTCM s <+> text "?"
]
case funView $ unEl t of
FunV arg@(Arg h r a) _ -> do
let s' = getSort a
cs <- s' `leqSort` s
addConstraints cs
x <- freshName_ (argName t)
let v = Arg h r $ Var 0 []
t' = piApply (raise 1 t) [v]
addCtx x arg $ fitsIn t' (raise 1 s)
_ -> return ()
constructs :: Int -> Type -> QName -> TCM ()
constructs nofPars t q = constrT 0 t
where
constrT n (El s v) = constr n s v
constr n s v = do
v <- reduce v
case v of
Pi a b -> underAbstraction a b $ \t ->
constrT (n + 1) t
Fun _ b -> constrT n b
Def d vs
| d == q -> checkParams n =<< reduce (take nofPars vs)
_ -> bad $ El s v
bad t = typeError $ ShouldEndInApplicationOfTheDatatype t
checkParams n vs = zipWithM_ sameVar (map unArg vs) ps
where
ps = reverse [ i | (i,_) <- zip [n..] vs ]
sameVar v i = do
t <- typeOfBV i
addConstraints =<< equalTerm t v (Var i [])
forceData :: MonadTCM tcm => QName -> Type -> tcm Type
forceData d (El s0 t) = liftTCM $ do
t' <- reduce t
d <- canonicalName d
case t' of
Def d' _
| d == d' -> return $ El s0 t'
| otherwise -> fail $ "wrong datatype " ++ show d ++ " != " ++ show d'
MetaV m vs -> do
Defn _ t _ _ Datatype{dataSort = s} <- getConstInfo d
ps <- newArgsMeta t
noConstraints $ leqType (El s0 t') (El s (Def d ps))
reduce $ El s0 t'
_ -> typeError $ ShouldBeApplicationOf (El s0 t) d
isCoinductive :: MonadTCM tcm => Type -> tcm (Maybe Bool)
isCoinductive t = do
El _ t <- normalise t
case t of
Def q _ -> do
def <- getConstInfo q
case theDef def of
Axiom {} -> return (Just False)
Function {} -> return Nothing
Datatype { dataInduction = CoInductive } -> return (Just True)
Datatype { dataInduction = Inductive } -> return (Just False)
Record {} -> return (Just False)
Constructor {} -> __IMPOSSIBLE__
Primitive {} -> __IMPOSSIBLE__
Var {} -> return Nothing
Lam {} -> __IMPOSSIBLE__
Lit {} -> __IMPOSSIBLE__
Con {} -> __IMPOSSIBLE__
Pi {} -> return (Just False)
Fun {} -> return (Just False)
Sort {} -> return (Just False)
MetaV {} -> return Nothing
DontCare -> __IMPOSSIBLE__