module Agda.TypeChecking.Rules.Data where
import Control.Applicative
import Control.Monad
import Control.Monad.Trans
import Data.List (genericTake)
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.Irrelevance
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Rules.Term ( isType_ )
import Agda.Interaction.Options
import Agda.Utils.List
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 countPars A.DomainFree{} = 1
countPars (A.DomainFull (A.TypedBindings _ (Arg _ _ b))) = case b of
A.TNoBind{} -> 1
A.TBind _ xs _ -> size xs
npars = sum $ map countPars ps
addSection (qnameToMName name) 0
t <- instantiateFull =<< typeOfConst name
let unTelV (TelV tel a) = telePi tel a
t <- unTelV <$> telView t
dataDef <- bindParameters ps t $ \tel t0 -> do
let tel' = hideTel tel
(nofIxs, s) <- splitType 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 (parameters instantiated): " <+> prettyTCM t0
, text "type (full): " <+> prettyTCM t
, text "sort: " <+> prettyTCM s
, text "indices:" <+> text (show nofIxs)
, text "params:" <+> text (show ps)
]
]
let dataDef = Datatype { dataPars = npars
, dataIxs = nofIxs
, dataInduction = Inductive
, dataClause = Nothing
, dataCons = []
, dataSort = s
, dataAbstr = Info.defAbstract i
, dataMutual = []
}
escapeContext (size tel) $ do
addConstant name ( Defn Relevant name t [] [] (defaultDisplayForm name) 0 noCompiledRep 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 Relevant name t [] [] (defaultDisplayForm name) 0 noCompiledRep $
dataDef { dataCons = map cname cs }
)
where
cname (A.ScopedDecl _ [d]) = cname d
cname (A.Axiom _ _ x _) = x
cname _ = __IMPOSSIBLE__
hideTel EmptyTel = EmptyTel
hideTel (ExtendTel a tel) = ExtendTel (hideAndRelParams a) $ hideTel <$> tel
splitType :: Type -> TCM (Int, Sort)
splitType t = case ignoreSharing $ unEl t of
Pi a b -> ((+ 1) -*- id) <$> do addCtxString (absName b) a $ splitType (absBody b)
Sort s -> return (0, s)
_ -> do
s <- newSortMeta
equalType t (sort s)
return (0, s)
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
debugEnter c e
t <- isType_ e
n <- size <$> getContextTelescope
debugEndsIn t d n
constructs n t d
debugFitsIn s
t `fitsIn` s
t' <- addForcingAnnotations t
debugAdd c t'
escapeContext (size tel)
$ addConstant c
$ Defn Relevant c (telePi tel t') [] [] (defaultDisplayForm c) 0 noCompiledRep
$ Constructor (size tel) c d (Info.defAbstract i) Inductive
where
debugEnter c e =
reportSDoc "tc.data.con" 5 $ vcat
[ text "checking constructor" <+> prettyTCM c <+> text ":" <+> prettyTCM e
]
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
]
debugAdd c t =
reportSDoc "tc.data.con" 5 $ vcat
[ text "adding constructor" <+> prettyTCM c <+> text ":" <+> prettyTCM t
]
checkConstructor _ _ _ _ _ = __IMPOSSIBLE__
bindParameters :: [A.LamBinding] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
bindParameters [] a ret = ret EmptyTel a
bindParameters (A.DomainFull (A.TypedBindings _ (Arg h rel (A.TBind _ xs _))) : bs) a ret =
bindParameters ([ A.DomainFree h rel x | x <- xs ] ++ bs) a ret
bindParameters (A.DomainFull (A.TypedBindings _ (Arg h rel (A.TNoBind _))) : bs) a ret = do
x <- freshNoName_
bindParameters (A.DomainFree h rel x : bs) a ret
bindParameters ps0@(A.DomainFree h rel x : ps) (El _ (Pi arg@(Dom h' rel' a) b)) ret
| h /= h' =
__IMPOSSIBLE__
| otherwise = addCtx x arg $ bindParameters ps (absBody b) $ \tel s ->
ret (ExtendTel arg $ Abs (show x) tel) s
bindParameters bs (El s (Shared p)) ret = bindParameters bs (El s $ derefPtr p) ret
bindParameters (b : bs) t _ = __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 ignoreSharing $ unEl t of
Pi arg@(Dom h r a) _ -> do
let s' = getSort a
s' `leqSort` s
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 :: Nat -> Type -> TCM ()
constrT n (El s v) = constr n s v
constr :: Nat -> Sort -> Term -> TCM ()
constr n s v = do
v <- reduce v
case ignoreSharing v of
Pi _ (NoAbs _ b) -> constrT n b
Pi a b -> underAbstraction a b $ \t ->
constrT (n + 1) t
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 vs ps
where
nvs = size vs
ps = genericTake nvs $ downFrom (n + nvs)
sameVar arg i
| argRelevance arg == Irrelevant = return ()
| otherwise = do
t <- typeOfBV i
equalTerm t (unArg arg) (var i)
isCoinductive :: Type -> TCM (Maybe Bool)
isCoinductive t = do
El s t <- normalise t
case ignoreSharing 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__
Level {} -> __IMPOSSIBLE__
Con {} -> __IMPOSSIBLE__
Pi {} -> return (Just False)
Sort {} -> return (Just False)
MetaV {} -> return Nothing
Shared{} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__