summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Rules/Data.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Rules/Data.hs')
-rw-r--r--src/full/Agda/TypeChecking/Rules/Data.hs145
1 files changed, 90 insertions, 55 deletions
diff --git a/src/full/Agda/TypeChecking/Rules/Data.hs b/src/full/Agda/TypeChecking/Rules/Data.hs
index f73b8af..df5d346 100644
--- a/src/full/Agda/TypeChecking/Rules/Data.hs
+++ b/src/full/Agda/TypeChecking/Rules/Data.hs
@@ -1,4 +1,5 @@
{-# LANGUAGE CPP #-}
+{-# LANGUAGE MultiWayIf #-}
module Agda.TypeChecking.Rules.Data where
@@ -10,6 +11,7 @@ import Data.Maybe (fromMaybe)
import qualified Data.Set as Set
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
@@ -35,6 +37,7 @@ import Agda.Utils.Except
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Permutation
+import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
import Agda.Utils.Tuple
import qualified Agda.Utils.VarSet as VarSet
@@ -51,11 +54,6 @@ 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 -- TODO!! (qnameName)
- 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
-- Add the datatype module
addSection (qnameToMName name)
@@ -68,7 +66,7 @@ checkDataDef i name ps cs =
t <- unTelV <$> telView t
-- Top level free vars
- freeVars <- getContextArgs
+ freeVars <- getContextSize
-- The parameters are in scope when checking the constructors.
dataDef <- bindParameters ps t $ \tel t0 -> do
@@ -111,10 +109,11 @@ checkDataDef i name ps cs =
, text "type (full): " <+> prettyTCM t
, text "sort: " <+> prettyTCM s
, text "indices:" <+> text (show nofIxs)
- , text "params:" <+> text (show ps)
+ , text "params:" <+> text (show $ deepUnscope ps)
, text "small params:" <+> text (show smallPars)
]
]
+ let npars = size tel
-- Change the datatype from an axiom to a datatype with no constructors.
let dataDef = Datatype
@@ -127,10 +126,10 @@ checkDataDef i name ps cs =
, dataCons = [] -- Constructors are added later
, dataSort = s
, dataAbstr = Info.defAbstract i
- , dataMutual = []
+ , dataMutual = Nothing
}
- escapeContext (size tel) $ do
+ escapeContext npars $ do
addConstant name $
defaultDefn defaultArgInfo name t dataDef
-- polarity and argOcc.s determined by the positivity checker
@@ -145,7 +144,7 @@ checkDataDef i name ps cs =
-- so we apply to the free module variables.
-- Unfortunately, we lose precision here, since 'abstract', which
-- is then performed by addConstant, cannot restore the linearity info.
- nonLinPars = Drop (size freeVars) $ Perm (npars + size freeVars) nonLinPars0
+ nonLinPars = Drop freeVars $ Perm (npars + freeVars) nonLinPars0
-- Return the data definition
return dataDef{ dataNonLinPars = nonLinPars }
@@ -167,8 +166,6 @@ checkDataDef i name ps cs =
defaultDefn defaultArgInfo name t $
dataDef{ dataCons = cons }
- -- Andreas 2012-02-13: postpone polarity computation until after positivity check
- -- computePolarity name
-- | Ensure that the type is a sort.
-- If it is not directly a sort, compare it to a 'newSortMetaBelowInf'.
@@ -230,7 +227,6 @@ checkConstructor d tel nofIxs s con@(A.Axiom _ i ai Nothing c e) =
t <- isType_ e
-- check that the type of the constructor ends in the data type
n <- getContextSize
- -- OLD: n <- size <$> getContextTelescope
debugEndsIn t d n
nonLinPars <- constructs n t d
debugNonLinPars nonLinPars
@@ -240,15 +236,22 @@ checkConstructor d tel nofIxs s con@(A.Axiom _ i ai Nothing c e) =
-- is contained in the sort of the data type
-- (to avoid impredicative existential types)
debugFitsIn s
- t' `fitsIn` s
+ arity <- t' `fitsIn` s
debugAdd c t'
-- add parameters to constructor type and put into signature
let con = ConHead c Inductive [] -- data constructors have no projectable fields and are always inductive
escapeContext (size tel) $
addConstant c $
- defaultDefn defaultArgInfo c (telePi tel t') $
- Constructor (size tel) con d (Info.defAbstract i) Inductive []
+ defaultDefn defaultArgInfo c (telePi tel t') $ Constructor
+ { conPars = size tel
+ , conArity = arity
+ , conSrcCon = con
+ , conData = d
+ , conAbstr = Info.defAbstract i
+ , conInd = Inductive
+ , conErased = [] -- computed during compilation to treeless
+ }
-- Add the constructor to the instance table, if needed
when (Info.defInstance i == InstanceDef) $ do
@@ -268,8 +271,9 @@ checkConstructor d tel nofIxs s con@(A.Axiom _ i ai Nothing c e) =
]
, nest 2 $ text "nofPars =" <+> text (show n)
]
- debugNonLinPars xs =
- reportSDoc "tc.data.con" 15 $ text $ "these constructor parameters are non-linear: " ++ show xs
+ debugNonLinPars ks =
+ reportSDoc "tc.data.con" 15 $
+ text "these constructor parameters are non-linear:" <+> text (show ks)
debugFitsIn s =
reportSDoc "tc.data.con" 15 $ sep
[ text "checking that the type fits in"
@@ -283,30 +287,71 @@ checkConstructor _ _ _ _ _ = __IMPOSSIBLE__ -- constructors are axioms
-- | Bind the parameters of a datatype.
+--
+-- We allow omission of hidden parameters at the definition site.
+-- Example:
+-- @
+-- data D {a} (A : Set a) : Set a
+-- data D A where
+-- c : A -> D A
+-- @
+
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 =
+bindParameters = bindParameters' []
+
+-- | Auxiliary function for 'bindParameters'.
+bindParameters'
+ :: [Type] -- ^ @n@ replicas of type if @LamBinding@s are @DomainFree@s
+ -- that came from a @DomainFull@ of @n@ binders.
+ -- Should be comsumed whenever a @DomainFree@s are consumed.
+ -> [A.LamBinding] -- ^ Bindings from definition site.
+ -> Type -- ^ Pi-type of bindings coming from signature site.
+ -> (Telescope -> Type -> TCM a)
+ -- ^ Continuation, accepting parameter telescope and rest of type.
+ -- The parameters are part of the context when the continutation is invoked.
+ -> 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{})) : _) _ _ = -- line break!
__IMPOSSIBLE__
-bindParameters ps0@(A.DomainFree info x : ps) (El _ (Pi arg@(Dom info' a) b)) ret
- -- Andreas, 2011-04-07 ignore relevance information in binding?!
- | 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__
-{- Andreas, 2012-01-17 Concrete.Definitions ensures number and hiding of parameters to be correct
--- Andreas, 2012-01-13 due to separation of data declaration/definition, the user
--- could give more parameters than declared.
-bindParameters (b : bs) t _ = typeError $ DataTooManyParameters
--}
+
+bindParameters' ts0 ps0@(A.DomainFree info x : ps) t ret = do
+ case ignoreSharing $ unEl t of
+ -- Andreas, 2011-04-07 ignore relevance information in binding?!
+ Pi arg@(Dom info' a) b -> do
+ if | info == info' -> do
+ -- Andreas, 2016-12-30, issue #1886:
+ -- If type for binding is present, check its correctness.
+ ts <- caseList ts0 (return []) $ \ t0 ts -> do
+ equalType t0 a
+ return ts
+ continue ts ps x
+
+ | visible info, notVisible info' ->
+ continue ts0 ps0 =<< freshName_ (absName b)
+
+ | otherwise -> __IMPOSSIBLE__
+ -- Andreas, 2016-12-30 Concrete.Definition excludes this case
+ 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__
-- | Check that the arguments to a constructor fits inside the sort of the datatype.
-- The first argument is the type of the constructor.
-fitsIn :: Type -> Sort -> TCM ()
+--
+-- As a side effect, return the arity of the constructor.
+
+fitsIn :: Type -> Sort -> TCM Int
fitsIn t s = do
reportSDoc "tc.data.fits" 10 $
sep [ text "does" <+> prettyTCM t
@@ -325,8 +370,9 @@ fitsIn t s = do
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 () -- getSort t `leqSort` s -- Andreas, 2013-04-13 not necessary since constructor type ends in data type
+ addContext (absName b, dom) $ do
+ succ <$> fitsIn (absBody b) (raise 1 s)
+ _ -> return 0 -- getSort t `leqSort` s -- Andreas, 2013-04-13 not necessary since constructor type ends in data type
where
notForced Forced{} = False
notForced _ = True
@@ -346,23 +392,6 @@ fitsIn t s = do
constructs :: Int -> Type -> QName -> TCM [Int]
constructs nofPars t q = constrT 0 t
where
-{- OLD
- 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 $ constrT (n + 1)
- Def d vs
- | d == q -> checkParams n =<< reduce (take nofPars vs)
- -- we only check the parameters
- _ -> bad $ El s v
-
- bad t = typeError $ ShouldEndInApplicationOfTheDatatype t
--}
constrT :: Nat -> Type -> TCM [Int]
constrT n t = do
t <- reduce t
@@ -382,6 +411,12 @@ constructs nofPars t q = constrT 0 t
when (any (< 0) nl) __IMPOSSIBLE__
when (any (>= nofPars) nl) __IMPOSSIBLE__
return nl
+ MetaV{} -> do
+ def <- getConstInfo q
+ xs <- newArgsMeta $ defType def
+ let t' = El (dataSort $ theDef def) $ Def q $ map Apply xs
+ equalType t t'
+ constrT n t'
_ -> typeError $ ShouldEndInApplicationOfTheDatatype t
checkParams n vs = zipWithM_ sameVar vs ps