#if __GLASGOW_HASKELL__ >= 710
#endif
module Agda.TypeChecking.Rules.Data where
import Control.Applicative
import Control.Monad
import Data.List (genericTake)
import Data.Maybe (fromMaybe)
import qualified Data.Set as Set
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.Monad.Builtin (primLevel)
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 Agda.TypeChecking.Rules.Term ( isType_ )
import Agda.Interaction.Options
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.Tuple
import qualified Agda.Utils.VarSet as VarSet
#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
let countPars A.DomainFree{} = 1
countPars (A.DomainFull (A.TypedBindings _ (Arg _ b))) = case b of
A.TLet{} -> 0
A.TBind _ xs _ -> size xs
npars = sum $ map countPars ps
addSection (qnameToMName name)
t <- instantiateFull =<< typeOfConst name
let unTelV (TelV tel a) = telePi tel a
t <- unTelV <$> telView t
freeVars <- getContextArgs
dataDef <- bindParameters ps t $ \tel t0 -> do
let tel' = hideAndRelParams <$> 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
smallPars <- smallParams tel 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)
, text "small params:" <+> text (show smallPars)
]
]
let dataDef = Datatype
{ dataPars = npars
, dataSmallPars = Perm npars smallPars
, dataNonLinPars = Drop 0 $ Perm npars []
, dataIxs = nofIxs
, dataInduction = Inductive
, dataClause = Nothing
, dataCons = []
, dataSort = s
, dataAbstr = Info.defAbstract i
, dataMutual = []
}
escapeContext (size tel) $ do
addConstant name $
defaultDefn defaultArgInfo name t dataDef
nonLins <- mapM (checkConstructor name tel' nofIxs s) cs
let nonLinPars0 = Set.toAscList $ Set.unions $ map Set.fromList nonLins
nonLinPars = Drop (size freeVars) $ Perm (npars + size freeVars) nonLinPars0
return dataDef{ dataNonLinPars = nonLinPars }
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 }
where
splitType :: Type -> TCM (Int, Sort)
splitType t = case ignoreSharing $ unEl t of
Pi a b -> mapFst (+ 1) <$> do addContext (absName b, a) $ splitType (absBody b)
Sort s -> return (0, s)
_ -> do
s <- newSortMeta
equalType t (sort s)
return (0, s)
smallParams :: Telescope -> Sort -> TCM [Int]
smallParams tel s = do
let as = map (snd . unDom) $ telToList tel
concat <$> do
forM (zip [0..] as) $ \ (i, a) -> do
localTCState $ do
([] <$ do equalTerm topSort (unEl a) =<< primLevel)
<|> ([i] <$ (getSort a `leqSort` s))
<|> return []
where
(<|>) m1 m2 = m1 `catchError_` (const m2)
checkConstructor
:: QName
-> Telescope
-> Nat
-> Sort
-> A.Constructor
-> TCM [Int]
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 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 <- isType_ e
n <- getContextSize
debugEndsIn t d n
nonLinPars <- constructs n t d
debugNonLinPars nonLinPars
t' <- addForcingAnnotations t
debugFitsIn s
t' `fitsIn` s
debugAdd c t'
let con = ConHead c Inductive []
escapeContext (size tel) $
addConstant c $
defaultDefn defaultArgInfo c (telePi tel t') $
Constructor (size tel) con d (Info.defAbstract i) Inductive
when (Info.defInstance i == InstanceDef) $ do
addNamedInstance c d
return nonLinPars
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)
]
debugNonLinPars xs =
reportSDoc "tc.data.con" 15 $ text $ "these constructor parameters are non-linear: " ++ show xs
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 info (A.TBind _ xs _))) : bs) a ret =
bindParameters (map (mergeHiding . fmap (A.DomainFree info)) xs ++ bs) a ret
bindParameters (A.DomainFull (A.TypedBindings _ (Arg info (A.TLet _ lbs))) : bs) a ret =
__IMPOSSIBLE__
bindParameters ps0@(A.DomainFree info x : ps) (El _ (Pi arg@(Dom info' a) b)) ret
| argInfoHiding info /= argInfoHiding info' =
__IMPOSSIBLE__
| otherwise = addContext (x, arg) $ bindParameters ps (absBody b) $ \tel s ->
ret (ExtendTel arg $ Abs (nameToArgName 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
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 ignoreSharing $ unEl t of
Pi dom b -> do
withoutK <- optWithoutK <$> pragmaOptions
when (withoutK || notForced (getRelevance dom)) $ do
sa <- reduce $ getSort dom
unless (sa == SizeUniv) $ sa `leqSort` s
addContext (absName b, dom) $ fitsIn (absBody b) (raise 1 s)
_ -> return ()
where
notForced Forced{} = False
notForced _ = True
constructs :: Int -> Type -> QName -> TCM [Int]
constructs nofPars t q = constrT 0 t
where
constrT :: Nat -> Type -> TCM [Int]
constrT n t = do
t <- reduce t
case ignoreSharing $ 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
m <- getContextSize
let nl = nonLinearParams m pars ixs
when (any (< 0) nl) __IMPOSSIBLE__
when (any (>= nofPars) nl) __IMPOSSIBLE__
return nl
_ -> 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)
nonLinearParams n pars ixs =
let fv = allRelevantVarsIgnoring IgnoreInAnnotations ixs
xs = map ((n1) ) $ VarSet.toList fv
in reverse $ filter (< size pars) xs
isCoinductive :: Type -> TCM (Maybe Bool)
isCoinductive t = do
El s t <- reduce 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 { recInduction = Just CoInductive } -> return (Just True)
Record { recInduction = _ } -> 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__