{-# LANGUAGE CPP #-}
{-# LANGUAGE MultiWayIf #-}
module Agda.TypeChecking.Rules.Data where
import Control.Monad
import Data.List (genericTake)
import Data.Maybe (fromMaybe)
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views (deepUnscope)
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.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Free
import Agda.TypeChecking.Forcing
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Telescope
import {-# SOURCE #-} Agda.TypeChecking.Rules.Term ( isType_ )
import Agda.Interaction.Options
import Agda.Utils.Except
import Agda.Utils.List
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
checkDataDef :: Info.DefInfo -> QName -> [A.LamBinding] -> [A.Constructor] -> TCM ()
checkDataDef i name ps cs =
traceCall (CheckDataDef (getRange name) (qnameName name) ps cs) $ do
addSection (qnameToMName name)
t <- instantiateFull =<< typeOfConst name
let unTelV (TelV tel a) = telePi tel a
t <- unTelV <$> telView t
freeVars <- getContextSize
dataDef <- bindParameters ps t $ \tel t0 -> do
let tel' = hideAndRelParams <$> tel
let TelV ixTel s0 = telView' t0
nofIxs = size ixTel
s <- workOnTypes $ do
s <- applyRelevanceToContext NonStrict newSortMetaBelowInf
catchError_ (addContext ixTel $ equalType s0 $ raise nofIxs $ sort s) $ \ err ->
if any (`freeIn` s0) [0..nofIxs - 1] then typeError . GenericDocError =<<
fsep [ text "The sort of" <+> prettyTCM name
, text "cannot depend on its indices in the type"
, prettyTCM t0
]
else throwError err
return 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 $ deepUnscope ps)
]
]
let npars = size tel
let dataDef = Datatype
{ dataPars = npars
, dataIxs = nofIxs
, dataInduction = Inductive
, dataClause = Nothing
, dataCons = []
, dataSort = s
, dataAbstr = Info.defAbstract i
, dataMutual = Nothing
}
escapeContext npars $ do
addConstant name $
defaultDefn defaultArgInfo name t dataDef
mapM_ (checkConstructor name tel' nofIxs s) cs
return dataDef
let s = dataSort dataDef
cons = map A.axiomName cs
do proofIrr <- proofIrrelevance
case (proofIrr, s, cs) of
(True, Prop, _:_:_) -> setCurrentRange cons $
typeError PropMustBeSingleton
_ -> return ()
addConstant name $
defaultDefn defaultArgInfo name t $
dataDef{ dataCons = cons }
forceSort :: Type -> TCM Sort
forceSort t = case unEl t of
Sort s -> return s
_ -> do
s <- applyRelevanceToContext NonStrict newSortMetaBelowInf
equalType t (sort s)
return 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 ai Nothing c e) =
traceCall (CheckConstructor d tel s con) $ do
debugEnter c e
case getRelevance ai of
Relevant -> return ()
Irrelevant -> typeError $ GenericError $ "Irrelevant constructors are not supported"
_ -> __IMPOSSIBLE__
t <- workOnTypes $ isType_ e
n <- getContextSize
debugEndsIn t d n
constructs n t d
forcedArgs <- computeForcingAnnotations t
debugFitsIn s
arity <- fitsIn forcedArgs t s
debugAdd c t
let con = ConHead c Inductive []
escapeContext (size tel) $
addConstant c $
defaultDefn defaultArgInfo c (telePi tel t) $ Constructor
{ conPars = size tel
, conArity = arity
, conSrcCon = con
, conData = d
, conAbstr = Info.defAbstract i
, conInd = Inductive
, conForced = forcedArgs
, conErased = []
}
when (Info.defInstance i == InstanceDef) $ do
addNamedInstance c d
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 = bindParameters' []
bindParameters'
:: [Type]
-> [A.LamBinding]
-> Type
-> (Telescope -> Type -> TCM a)
-> TCM a
bindParameters' _ [] a ret = ret EmptyTel a
bindParameters' ts (A.DomainFull (A.TypedBindings _ (Arg info (A.TBind _ xs e))) : bs) a ret = do
unless (null ts) __IMPOSSIBLE__
t <- workOnTypes $ isType_ e
bindParameters' (t <$ xs) (map (mergeHiding . fmap (A.DomainFree info)) xs ++ bs) a ret
bindParameters' _ (A.DomainFull (A.TypedBindings _ (Arg _ A.TLet{})) : _) _ _ =
__IMPOSSIBLE__
bindParameters' ts0 ps0@(A.DomainFree info x : ps) t ret = do
case unEl t of
Pi arg@(Dom info' a) b -> do
if | info == info' -> do
ts <- caseList ts0 (return []) $ \ t0 ts -> do
equalType t0 a
return ts
continue ts ps $ A.unBind x
| visible info, notVisible info' ->
continue ts0 ps0 =<< freshName_ (absName b)
| otherwise -> __IMPOSSIBLE__
where
continue ts ps x = do
addContext (x, arg) $
bindParameters' (raise 1 ts) ps (absBody b) $ \ tel s ->
ret (ExtendTel arg $ Abs (nameToArgName x) tel) s
_ -> __IMPOSSIBLE__
fitsIn :: [IsForced] -> Type -> Sort -> TCM Int
fitsIn forceds t s = do
reportSDoc "tc.data.fits" 10 $
sep [ text "does" <+> prettyTCM t
, text "of sort" <+> prettyTCM (getSort t)
, text "fit in" <+> prettyTCM s <+> text "?"
]
t <- reduce t
case unEl t of
Pi dom b -> do
withoutK <- optWithoutK <$> pragmaOptions
let (forced,forceds') = nextIsForced forceds
unless (isForced forced && not withoutK) $ do
sa <- reduce $ getSort dom
unless (sa == SizeUniv) $ sa `leqSort` s
addContext (absName b, dom) $ do
succ <$> fitsIn forceds' (absBody b) (raise 1 s)
_ -> return 0
constructs :: Int -> Type -> QName -> TCM ()
constructs nofPars t q = constrT 0 t
where
constrT :: Nat -> Type -> TCM ()
constrT n t = do
t <- reduce t
case unEl t of
Pi _ (NoAbs _ b) -> constrT n b
Pi a b -> underAbstraction a b $ constrT (n + 1)
Def d es | d == q -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
(pars, ixs) <- normalise $ splitAt nofPars vs
checkParams n pars
MetaV{} -> do
def <- getConstInfo q
let td = defType def
TelV tel core <- telView td
let us = zipWith (\ arg x -> var x <$ arg ) (telToArgs tel) $
take nofPars $ downFrom (nofPars + n)
xs <- newArgsMeta =<< piApplyM td us
let t' = El (dataSort $ theDef def) $ Def q $ map Apply $ us ++ xs
noConstraints $ equalType t t'
constrT n t'
_ -> typeError $ ShouldEndInApplicationOfTheDatatype t
checkParams n vs = zipWithM_ sameVar vs ps
where
nvs = size vs
ps = genericTake nvs $ downFrom (n + nvs)
sameVar arg i
| isIrrelevant arg = return ()
| otherwise = do
t <- typeOfBV i
equalTerm t (unArg arg) (var i)
isCoinductive :: Type -> TCM (Maybe Bool)
isCoinductive t = do
El s t <- reduce 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 { recInduction = Just CoInductive } -> return (Just True)
Record { recInduction = _ } -> return (Just False)
Constructor {} -> __IMPOSSIBLE__
Primitive {} -> __IMPOSSIBLE__
AbstractDefn{} -> __IMPOSSIBLE__
Var {} -> return Nothing
Lam {} -> __IMPOSSIBLE__
Lit {} -> __IMPOSSIBLE__
Level {} -> __IMPOSSIBLE__
Con {} -> __IMPOSSIBLE__
Pi {} -> return (Just False)
Sort {} -> return (Just False)
MetaV {} -> return Nothing
DontCare{} -> __IMPOSSIBLE__