{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Data where
import Control.Monad
import Control.Monad.Trans
import Control.Monad.Trans.Maybe
import Data.Foldable (traverse_)
import Data.Maybe (fromMaybe, catMaybes, isJust)
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Concrete.Name as C
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.Syntax.Scope.Monad
import Agda.Syntax.Fixity
import {-# SOURCE #-} Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Generalize
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Names
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Free
import Agda.TypeChecking.Forcing
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.ProjectionLike
import {-# SOURCE #-} Agda.TypeChecking.Rules.Term ( isType_ )
import Agda.Utils.Except
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
import Agda.Utils.Impossible
checkDataDef :: A.DefInfo -> QName -> UniverseCheck -> A.DataDefParams -> [A.Constructor] -> TCM ()
checkDataDef i name uc (A.DataDefParams gpars ps) cs =
traceCall (CheckDataDef (getRange name) name ps cs) $ do
addSection (qnameToMName name)
def <- instantiateDef =<< getConstInfo name
t <- instantiateFull $ defType def
let npars =
case theDef def of
DataOrRecSig n -> n
_ -> __IMPOSSIBLE__
let unTelV (TelV tel a) = telePi tel a
t <- unTelV <$> telView t
parNames <- getGeneralizedParameters gpars name
freeVars <- getContextSize
dataDef <- bindGeneralizedParameters parNames t $ \ gtel t0 ->
bindParameters (npars - length parNames) ps t0 $ \ ptel t0 -> do
let tel = abstract gtel ptel
tel' = hideAndRelParams <$> tel
let TelV ixTel s0 = telView' t0
nofIxs = size ixTel
s <- workOnTypes $ do
s <- newSortMetaBelowInf
catchError_ (addContext ixTel $ equalType s0 $ raise nofIxs $ sort s) $ \ err ->
if any (`freeIn` s0) [0..nofIxs - 1] then typeError . GenericDocError =<<
fsep [ "The sort of" <+> prettyTCM name
, "cannot depend on its indices in the type"
, prettyTCM t0
]
else throwError err
reduce s
let s' = case s of
Prop l -> Type l
_ -> s
unless (uc == NoUniverseCheck) $
whenM withoutKOption $ checkIndexSorts s' ixTel
reportSDoc "tc.data.sort" 20 $ vcat
[ "checking datatype" <+> prettyTCM name
, nest 2 $ vcat
[ "type (parameters instantiated): " <+> prettyTCM t0
, "type (full): " <+> prettyTCM t
, "sort: " <+> prettyTCM s
, "indices:" <+> text (show nofIxs)
, "gparams:" <+> text (show parNames)
, "params: " <+> text (show $ deepUnscope ps)
]
]
let npars = size tel
let dataDef = Datatype
{ dataPars = npars
, dataIxs = nofIxs
, dataClause = Nothing
, dataCons = []
, dataSort = s
, dataAbstr = Info.defAbstract i
, dataMutual = Nothing
, dataPathCons = []
}
unsafeEscapeContext npars $ do
addConstant name $
defaultDefn defaultArgInfo name t dataDef
pathCons <- forM cs $ \ c -> do
isPathCons <- checkConstructor name uc tel' nofIxs s c
return $ if isPathCons == PathCons then Just (A.axiomName c) else Nothing
return dataDef{ dataPathCons = catMaybes pathCons }
let s = dataSort dataDef
cons = map A.axiomName cs
addConstant name $
defaultDefn defaultArgInfo name t $
dataDef{ dataCons = cons }
forceSort :: Type -> TCM Sort
forceSort t = reduce (unEl t) >>= \case
Sort s -> return s
_ -> do
s <- newSortMetaBelowInf
equalType t (sort s)
return s
checkConstructor
:: QName
-> UniverseCheck
-> Telescope
-> Nat
-> Sort
-> A.Constructor
-> TCM IsPathCons
checkConstructor d uc tel nofIxs s (A.ScopedDecl scope [con]) = do
setScope scope
checkConstructor d uc tel nofIxs s con
checkConstructor d uc 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"
NonStrict -> typeError $ GenericError $ "Shape-irrelevant constructors are not supported"
case getQuantity ai of
Quantityω{} -> return ()
Quantity0{} -> typeError $ GenericError $ "Erased constructors are not supported"
Quantity1{} -> typeError $ GenericError $ "Quantity-restricted constructors are not supported"
(t, isPathCons) <- checkConstructorType e d
forcedArgs <- if isPathCons == PointCons
then computeForcingAnnotations c t
else return []
debugFitsIn s
let s' = case s of
Prop l -> Type l
_ -> s
arity <- traceCall (CheckConstructorFitsIn c t s') $ fitsIn uc forcedArgs t s'
s <- reduce s
debugAdd c t
(TelV fields _, boundary) <- telViewUpToPathBoundaryP (-1) t
params <- getContextTelescope
unsafeEscapeContext (size tel) $ do
(con, comp, projNames) <- if nofIxs /= 0 || (Info.defAbstract i == AbstractDef)
then return (ConHead c Inductive [], emptyCompKit, Nothing)
else unsafeInTopContext $ do
names <- forM [0 .. size fields - 1] $ \ i ->
freshAbstractQName'_ $ P.prettyShow (A.qnameName c) ++ "-" ++ show i
dataT <- El s <$> (pure $ Def d $ map Apply $ teleArgs params)
reportSDoc "tc.data.con.comp" 5 $ vcat $
[ "params =" <+> pretty params
, "dataT =" <+> pretty dataT
, "fields =" <+> pretty fields
, "names =" <+> pretty names
]
let con = ConHead c Inductive $ zipWith (<$) names $ map argFromDom $ telToList fields
defineProjections d con params names fields dataT
comp <- defineCompData d con params names fields dataT boundary
return (con, comp, Just names)
addConstant c $
defaultDefn defaultArgInfo c (telePi tel t) $ Constructor
{ conPars = size tel
, conArity = arity
, conSrcCon = con
, conData = d
, conAbstr = Info.defAbstract i
, conInd = Inductive
, conComp = comp
, conProj = projNames
, conForced = forcedArgs
, conErased = Nothing
}
traverse_ (mapM_ makeProjection) $ projNames
when (Info.defInstance i == InstanceDef) $ do
addNamedInstance c d
return isPathCons
where
checkConstructorType (A.ScopedExpr s e) d = withScope_ s $ checkConstructorType e d
checkConstructorType e d = do
let check k e = do
t <- workOnTypes $ isType_ e
n <- getContextSize
debugEndsIn t d (n - k)
isPathCons <- constructs (n - k) k t d
return (t, isPathCons)
case e of
A.Generalized s e -> do
(_, t, isPathCons) <- generalizeType' s (check 1 e)
return (t, isPathCons)
_ -> check 0 e
debugEnter c e =
reportSDoc "tc.data.con" 5 $ vcat
[ "checking constructor" <+> prettyTCM c <+> ":" <+> prettyTCM e
]
debugEndsIn t d n =
reportSDoc "tc.data.con" 15 $ vcat
[ sep [ "checking that"
, nest 2 $ prettyTCM t
, "ends in" <+> prettyTCM d
]
, nest 2 $ "nofPars =" <+> text (show n)
]
debugFitsIn s =
reportSDoc "tc.data.con" 15 $ sep
[ "checking that the type fits in"
, nest 2 $ prettyTCM s
]
debugAdd c t =
reportSDoc "tc.data.con" 5 $ vcat
[ "adding constructor" <+> prettyTCM c <+> ":" <+> prettyTCM t
]
checkConstructor _ _ _ _ _ _ = __IMPOSSIBLE__
defineCompData :: QName
-> ConHead
-> Telescope
-> [QName]
-> Telescope
-> Type
-> Boundary
-> TCM CompKit
defineCompData d con params names fsT t boundary = do
required <- mapM getTerm'
[ builtinInterval
, builtinIZero
, builtinIOne
, builtinIMin
, builtinIMax
, builtinINeg
, builtinPOr
, builtinItIsOne
]
if not (all isJust required) then return $ emptyCompKit else do
hcomp <- whenDefined (null boundary) [builtinHComp,builtinTrans] (defineTranspOrHCompD DoHComp d con params names fsT t boundary)
transp <- whenDefined True [builtinTrans] (defineTranspOrHCompD DoTransp d con params names fsT t boundary)
return $ CompKit
{ nameOfTransp = transp
, nameOfHComp = hcomp
}
where
sub tel = parallelS [ var n `apply` [Arg defaultArgInfo $ var 0] | n <- [1..size tel] ]
withArgInfo tel = zipWith Arg (map domInfo . telToList $ tel)
defineTranspOrHCompD cmd d con params names fsT t boundary
= do
let project = (\ t p -> apply (Def p []) [argN t])
stuff <- defineTranspOrHCompForFields cmd
(guard (not $ null boundary) >> (Just $ Con con ConOSystem $ teleElims fsT boundary))
project d params fsT (map argN names) t
caseMaybe stuff (return Nothing) $ \ ((theName, gamma , ty, _cl_types , bodies), theSub) -> do
iz <- primIZero
body <- do
case cmd of
DoHComp -> return $ Con con ConOSystem (map Apply $ withArgInfo fsT bodies)
DoTransp | null boundary -> return $ Con con ConOSystem (map Apply $ withArgInfo fsT bodies)
| otherwise -> do
io <- primIOne
tIMax <- primIMax
tIMin <- primIMin
tINeg <- primINeg
tPOr <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinPOr
tHComp <- primHComp
let
u = Con con ConOSystem $ teleElims fsT boundary
the_u = liftS (size fsT) d0 `applySubst` u
where
d0 :: Substitution
d0 = wkS 1
(consS iz IdS `composeS` sub params)
the_phi = raise (size fsT) $ var 0
sigma = reverse bodies ++# d1
where
d1 :: Substitution
d1 = wkS (size gamma - size params)
(consS io IdS `composeS` sub params)
bs = fullBoundary fsT boundary
w1' = Con con ConOSystem $ sigma `applySubst` teleElims fsT boundary
imax x y = pure tIMax <@> x <@> y
ineg r = pure tINeg <@> r
lvlOfType = (\ (Type l) -> Level l) . getSort
pOr la i j u0 u1 = pure tPOr <#> (lvlOfType <$> la) <@> i <@> j
<#> (ilam "o" $ \ _ -> unEl <$> la) <@> u0 <@> u1
absAp x y = liftM2 absApp x y
mkFace (r,(u1,u2)) = runNamesT [] $ do
phi <- open the_phi
ty <- open (Abs "i" $ (liftS 1 (raiseS (size gamma - size params)) `composeS` sub params) `applySubst` t)
bind "i" $ \ i -> do
[r,u1,u2] <- mapM (open . applySubst theSub) [r,u1,u2]
psi <- imax r (ineg r)
let
squeeze u = cl primTrans
<#> (lam "j" $ \ j -> lvlOfType <$> ty `absAp` (imax i j))
<@> (lam "j" $ \ j -> unEl <$> ty `absAp` (imax i j))
<@> (phi `imax` i)
<@> u
alpha <- pOr (ty `absAp` i)
(ineg r)
r
(ilam "o" $ \ _ -> squeeze u1) (ilam "o" $ \ _ -> squeeze u2)
return $ (psi, alpha)
faces <- mapM mkFace bs
runNamesT [] $ do
w1' <- open w1'
phi <- open the_phi
u <- open the_u
ty <- open ty
faces <- mapM (\ x -> liftM2 (,) (open . noabsApp __IMPOSSIBLE__ $ fmap fst x) (open $ fmap snd x)) faces
let
thePsi = foldl1 imax (map fst faces)
hcomp ty phi sys a0 = pure tHComp <#> (lvlOfType <$> ty)
<#> (unEl <$> ty)
<#> phi
<@> sys
<@> a0
let
sys = lam "i" $ \ i -> do
let
recurse [(psi,alpha)] = alpha `absAp` (ineg i)
recurse ((psi,alpha):xs) = pOr ty
psi theOr
(alpha `absAp` (ineg i)) (recurse xs)
where
theOr = foldl1 imax (map fst xs)
recurse [] = __IMPOSSIBLE__
sys_alpha = recurse faces
pOr ty
thePsi phi
sys_alpha (ilam "o" $ \ _ -> u)
hcomp ty (thePsi `imax` phi) sys w1'
let
d0 :: Substitution
d0 = wkS 1
(consS iz IdS `composeS` sub params)
up = ConP con (ConPatternInfo defaultPatternInfo False False Nothing False) $
telePatterns (d0 `applySubst` fsT) (liftS (size fsT) d0 `applySubst` boundary)
let
clause | null boundary
= Clause
{ clauseTel = gamma
, clauseType = Just . argN $ ty
, namedClausePats = teleNamedArgs gamma
, clauseFullRange = noRange
, clauseLHSRange = noRange
, clauseCatchall = False
, clauseBody = Just $ body
, clauseUnreachable = Just False
, clauseEllipsis = NoEllipsis
}
| otherwise
= Clause
{ clauseTel = gamma
, clauseType = Just . argN $ ty
, namedClausePats = take (size gamma - size fsT) (teleNamedArgs gamma) ++ [argN $ unnamed $ up]
, clauseFullRange = noRange
, clauseLHSRange = noRange
, clauseCatchall = False
, clauseBody = Just $ body
, clauseUnreachable = Just False
, clauseEllipsis = NoEllipsis
}
cs = [clause]
addClauses theName cs
(mst, _, cc) <- inTopContext (compileClauses Nothing cs)
whenJust mst $ setSplitTree theName
setCompiledClauses theName cc
setTerminates theName True
return $ Just theName
whenDefined False _ _ = return Nothing
whenDefined True xs m = do
xs <- mapM getTerm' xs
if all isJust xs then m else return Nothing
defineProjections :: QName
-> ConHead
-> Telescope
-> [QName]
-> Telescope
-> Type
-> TCM ()
defineProjections dataname con params names fsT t = do
let
fieldTypes = ([ Def f [] `apply` [argN $ var 0] | f <- reverse names ] ++# raiseS 1) `applySubst`
flattenTel fsT
projTel = abstract params (ExtendTel (defaultDom t) (Abs "d" EmptyTel))
forM_ (zip3 (downFrom (size fieldTypes)) names fieldTypes) $ \ (i,projName,ty) -> do
let
projType = abstract projTel <$> ty
inTopContext $ do
reportSDoc "tc.data.proj" 20 $ sep [ "proj" <+> prettyTCM (i,ty) , nest 2 $ prettyTCM projType ]
let
cpi = ConPatternInfo defaultPatternInfo False False (Just $ argN $ raise (size fsT) t) False
conp = defaultArg $ ConP con cpi $ teleNamedArgs fsT
clause = Clause
{ clauseTel = abstract params fsT
, clauseType = Just . argN $ ([Con con ConOSystem (map Apply $ teleArgs fsT)] ++# raiseS (size fsT)) `applySubst` unDom ty
, namedClausePats = raise (size fsT) (teleNamedArgs params) ++ [Named Nothing <$> conp]
, clauseFullRange = noRange
, clauseLHSRange = noRange
, clauseCatchall = False
, clauseBody = Just $ var i
, clauseUnreachable = Just False
, clauseEllipsis = NoEllipsis
}
noMutualBlock $ do
let cs = [clause]
(mst, _, cc) <- inTopContext $ compileClauses Nothing cs
let fun = emptyFunction
{ funClauses = cs
, funTerminates = Just True
, funCompiled = Just cc
, funSplitTree = mst
, funMutual = Just []
}
addConstant projName $
(defaultDefn defaultArgInfo projName (unDom projType) fun)
{ defNoCompilation = True }
inTopContext $ do
reportSDoc "tc.data.proj.fun" 60 $ sep [ "proj" <+> prettyTCM i, nest 2 $ pretty fun ]
freshAbstractQName'_ :: String -> TCM QName
freshAbstractQName'_ s = freshAbstractQName noFixity' (C.Name noRange C.InScope [C.Id $ s])
data LType = LEl Level Term deriving (Eq,Show)
fromLType :: LType -> Type
fromLType (LEl l t) = El (Type l) t
lTypeLevel :: LType -> Level
lTypeLevel (LEl l t) = l
toLType :: MonadReduce m => Type -> m (Maybe LType)
toLType ty = do
sort <- reduce $ getSort ty
case sort of
Type l -> return $ Just $ LEl l (unEl ty)
_ -> return $ Nothing
instance Subst Term LType where
applySubst rho (LEl l t) = LEl (applySubst rho l) (applySubst rho t)
data CType = ClosedType QName | LType LType deriving (Eq,Show)
fromCType :: CType -> Type
fromCType (ClosedType q) = El Inf (Def q [])
fromCType (LType t) = fromLType t
toCType :: MonadReduce m => Type -> m (Maybe CType)
toCType ty = do
sort <- reduce $ getSort ty
case sort of
Type l -> return $ Just $ LType (LEl l (unEl ty))
Inf -> do
t <- reduce (unEl ty)
case t of
Def q [] -> return $ Just $ ClosedType q
_ -> return $ Nothing
_ -> return $ Nothing
instance Subst Term CType where
applySubst rho t@ClosedType{} = t
applySubst rho (LType t) = LType $ applySubst rho t
defineTranspOrHCompForFields
:: TranspOrHComp
-> (Maybe Term)
-> (Term -> QName -> Term)
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM (Maybe ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
defineTranspOrHCompForFields cmd pathCons project name params fsT fns rect =
case cmd of
DoTransp -> runMaybeT $ do
fsT' <- traverse (traverse (MaybeT . toCType)) fsT
lift $ defineTranspForFields pathCons project name params fsT' fns rect
DoHComp -> runMaybeT $ do
fsT' <- traverse (traverse (MaybeT . toLType)) fsT
rect' <- MaybeT $ toLType rect
lift $ defineHCompForFields project name params fsT' fns rect'
defineTranspForFields
:: (Maybe Term)
-> (Term -> QName -> Term)
-> QName
-> Telescope
-> Tele (Dom CType)
-> [Arg QName]
-> Type
-> TCM ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
defineTranspForFields pathCons applyProj name params fsT fns rect = do
interval <- elInf primInterval
let deltaI = expTelescope interval params
iz <- primIZero
io <- primIOne
imin <- getPrimitiveTerm "primIMin"
imax <- getPrimitiveTerm "primIMax"
ineg <- getPrimitiveTerm "primINeg"
transp <- getPrimitiveTerm builtinTrans
por <- getPrimitiveTerm "primPOr"
one <- primItIsOne
reportSDoc "trans.rec" 20 $ text $ show params
reportSDoc "trans.rec" 20 $ text $ show deltaI
reportSDoc "trans.rec" 10 $ text $ show fsT
let thePrefix = "transp-"
theName <- freshAbstractQName'_ $ thePrefix ++ P.prettyShow (A.qnameName name)
reportSLn "trans.rec" 5 $ ("Generated name: " ++ show theName ++ " " ++ showQNameId theName)
theType <- (abstract deltaI <$>) $ runNamesT [] $ do
rect' <- open (runNames [] $ bind "i" $ \ x -> let _ = x `asTypeOf` pure (undefined :: Term) in
pure rect')
nPi' "phi" (elInf $ cl primInterval) $ \ phi ->
(absApp <$> rect' <*> pure iz) --> (absApp <$> rect' <*> pure io)
reportSDoc "trans.rec" 20 $ prettyTCM theType
reportSDoc "trans.rec" 60 $ text $ "sort = " ++ show (getSort rect')
noMutualBlock $ addConstant theName $ (defaultDefn defaultArgInfo theName theType
(emptyFunction { funTerminates = Just True }))
{ defNoCompilation = True }
TelV gamma rtype <- telView theType
let
theTerm = Def theName [] `apply` teleArgs gamma
clause_types = parallelS [theTerm `applyProj` (unArg fn)
| fn <- reverse fns] `applySubst`
flattenTel (singletonS 0 io `applySubst` fsT')
delta_i = (liftS 1 (raiseS (size gamma - size deltaI)) `composeS` sub params)
fsT' = (liftS 1 (raiseS (size gamma - size deltaI)) `composeS` sub params) `applySubst`
fsT
lam_i = Lam defaultArgInfo . Abs "i"
gamma' = telFromList $ take (size gamma - 1) $ telToList gamma
d0 :: Substitution
d0 = wkS 1
(consS iz IdS `composeS` sub params)
(tel,theta,the_phi,the_u0, the_fields) =
case pathCons of
Just u -> (abstract gamma' (d0 `applySubst` fmap (fmap fromCType) fsT)
, (liftS (size fsT) d0 `applySubst` u) `consS` raiseS (size fsT)
, raise (size fsT) (var 0)
, (liftS (size fsT) d0 `applySubst` u)
, drop (size gamma') $ map unArg $ teleArgs tel)
Nothing -> (gamma, IdS, var 1, var 0, map (\ fname -> var 0 `applyProj` unArg fname) fns )
fsT_tel = (liftS 1 (raiseS (size tel - size deltaI)) `composeS` sub params) `applySubst` fsT
iMin x y = imin `apply` [argN x, argN y]
iMax x y = imax `apply` [argN x, argN y]
iNeg x = ineg `apply` [argN x]
mkBody (field, filled_ty') = do
let
filled_ty = lam_i $ (unEl . fromCType . unDom) filled_ty'
case unDom filled_ty' of
LType (LEl l _) -> do
let lvl = lam_i $ Level l
return $ runNames [] $ do
lvl <- open lvl
[phi,field] <- mapM open [the_phi,field]
pure transp <#> lvl <@> pure filled_ty
<@> phi
<@> field
ClosedType{} ->
return $ runNames [] $ do
[field] <- mapM open [field]
field
let
tau = parallelS $ us ++ (phi `iMax` iNeg (var 0))
: map (\ d -> Lam defaultArgInfo $ Abs "i" $ raise 1 d `apply` [argN $ (iMin (var 0) (var 1))]) ds
where
(us, phi:ds) = splitAt (size tel - size gamma') $ reverse (raise 1 (map unArg (teleArgs tel)))
let
go acc [] = return []
go acc ((fname,field_ty) : ps) = do
let
filled_ty = parallelS (tau `applySubst` acc) `applySubst` field_ty
b <- mkBody (fname,filled_ty)
bs <- go (b : acc) ps
return $ b : bs
bodys <- go [] (zip the_fields (map (fmap snd) $ telToList fsT_tel))
let
theSubst = reverse (tau `applySubst` bodys) ++# (liftS 1 (raiseS (size tel - size deltaI)) `composeS` sub params)
return $ ((theName, tel, theta `applySubst` rtype, map (fmap fromCType) clause_types, bodys), theSubst)
where
rect' = sub params `applySubst` rect
sub tel = parallelS [ var n `apply` [Arg defaultArgInfo $ var 0] | n <- [1..size tel] ]
expTelescope :: Type -> Telescope -> Telescope
expTelescope int tel = unflattenTel names ys
where
xs = flattenTel tel
names = teleNames tel
t = ExtendTel (defaultDom $ raise (size tel) int) (Abs "i" EmptyTel)
s = sub tel
ys = map (fmap (abstract t) . applySubst s) xs
defineHCompForFields
:: (Term -> QName -> Term)
-> QName
-> Telescope
-> Tele (Dom LType)
-> [Arg QName]
-> LType
-> TCM ((QName, Telescope, Type, [Dom Type], [Term]),Substitution)
defineHCompForFields applyProj name params fsT fns rect = do
interval <- elInf primInterval
let delta = params
iz <- primIZero
io <- primIOne
imin <- getPrimitiveTerm "primIMin"
imax <- getPrimitiveTerm "primIMax"
tIMax <- getPrimitiveTerm "primIMax"
ineg <- getPrimitiveTerm "primINeg"
hcomp <- getPrimitiveTerm builtinHComp
transp <- getPrimitiveTerm builtinTrans
por <- getPrimitiveTerm "primPOr"
one <- primItIsOne
reportSDoc "comp.rec" 20 $ text $ show params
reportSDoc "comp.rec" 20 $ text $ show delta
reportSDoc "comp.rec" 10 $ text $ show fsT
let thePrefix = "hcomp-"
theName <- freshAbstractQName'_ $ thePrefix ++ P.prettyShow (A.qnameName name)
reportSLn "hcomp.rec" 5 $ ("Generated name: " ++ show theName ++ " " ++ showQNameId theName)
theType <- (abstract delta <$>) $ runNamesT [] $ do
rect <- open $ fromLType rect
nPi' "phi" (elInf $ cl primInterval) $ \ phi ->
(nPi' "i" (elInf $ cl primInterval) $ \ i ->
pPi' "o" phi $ \ _ -> rect) -->
rect --> rect
reportSDoc "hcomp.rec" 20 $ prettyTCM theType
reportSDoc "hcomp.rec" 60 $ text $ "sort = " ++ show (lTypeLevel rect)
noMutualBlock $ addConstant theName $ (defaultDefn defaultArgInfo theName theType
(emptyFunction { funTerminates = Just True }))
{ defNoCompilation = True }
TelV gamma rtype <- telView theType
let
drect_gamma = raiseS (size gamma - size delta) `applySubst` rect
reportSDoc "hcomp.rec" 60 $ text $ "sort = " ++ show (lTypeLevel drect_gamma)
let
compTerm = Def theName [] `apply` teleArgs gamma
the_phi = var 2
the_u = var 1
the_u0 = var 0
fillTerm = runNames [] $ do
rect <- open . unEl . fromLType $ drect_gamma
lvl <- open . Level . lTypeLevel $ drect_gamma
params <- mapM open $ take (size delta) $ teleArgs gamma
[phi,w,w0] <- mapM open [the_phi,the_u,the_u0]
lam "i" $ \ i -> do
args <- sequence params
psi <- pure imax <@> phi <@> (pure ineg <@> i)
u <- lam "j" (\ j -> pure por <#> lvl
<@> phi
<@> (pure ineg <@> i)
<#> (lam "_" $ \ o -> rect)
<@> (w <@> (pure imin <@> i <@> j))
<@> (lam "_" $ \ o -> w0)
)
u0 <- w0
pure $ Def theName [] `apply` (args ++ [argN psi, argN u, argN u0])
where
underArg k m = Arg <$> (argInfo <$> m) <*> (k (unArg <$> m))
clause_types = parallelS [compTerm `applyProj` (unArg fn)
| fn <- reverse fns] `applySubst`
flattenTel (raiseS (size gamma - size delta) `applySubst` fsT)
fsT' = raiseS ((size gamma - size delta) + 1) `applySubst` fsT
filled_types = parallelS [raise 1 fillTerm `apply` [argN $ var 0] `applyProj` (unArg fn)
| fn <- reverse fns] `applySubst`
flattenTel fsT'
comp <- do
let
imax i j = pure tIMax <@> i <@> j
let forward la bA r u = pure transp <#> (lam "i" $ \ i -> la <@> (i `imax` r))
<@> (lam "i" $ \ i -> bA <@> (i `imax` r))
<@> r
<@> u
return $ \ la bA phi u u0 ->
pure hcomp <#> (la <@> pure io) <#> (bA <@> pure io) <#> phi
<@> (lam "i" $ \ i -> ilam "o" $ \ o ->
forward la bA i (u <@> i <..> o))
<@> forward la bA (pure iz) u0
let
mkBody (fname, filled_ty') = do
let
proj t = (`applyProj` unArg fname) <$> t
filled_ty = Lam defaultArgInfo (Abs "i" $ (unEl . fromLType . unDom) filled_ty')
l <- reduce $ lTypeLevel $ unDom filled_ty'
let lvl = Lam defaultArgInfo (Abs "i" $ Level l)
return $ runNames [] $ do
lvl <- open lvl
[phi,w,w0] <- mapM open [the_phi,the_u,the_u0]
filled_ty <- open filled_ty
comp lvl
filled_ty
phi
(lam "i" $ \ i -> lam "o" $ \ o -> proj $ w <@> i <@> o)
(proj w0)
reportSDoc "hcomp.rec" 60 $ text $ "filled_types sorts:" ++ show (map (getSort . fromLType . unDom) filled_types)
bodys <- mapM mkBody (zip fns filled_types)
return $ ((theName, gamma, rtype, map (fmap fromLType) clause_types, bodys),IdS)
getGeneralizedParameters :: Set Name -> QName -> TCM [Maybe Name]
getGeneralizedParameters gpars name | Set.null gpars = return []
getGeneralizedParameters gpars name = do
let inscope x = x <$ guard (Set.member x gpars)
map (>>= inscope) . defGeneralizedParams <$> (instantiateDef =<< getConstInfo name)
bindGeneralizedParameters :: [Maybe Name] -> Type -> (Telescope -> Type -> TCM a) -> TCM a
bindGeneralizedParameters [] t ret = ret EmptyTel t
bindGeneralizedParameters (name : names) t ret =
case unEl t of
Pi a b -> ext $ bindGeneralizedParameters names (unAbs b) $ \ tel t -> ret (ExtendTel a (tel <$ b)) t
where
ext | Just x <- name = addContext (x, a)
| otherwise = addContext (absName b, a)
_ -> __IMPOSSIBLE__
bindParameters
:: Int
-> [A.LamBinding]
-> Type
-> (Telescope -> Type -> TCM a)
-> TCM a
bindParameters 0 [] a ret = ret EmptyTel a
bindParameters 0 (par : _) _ _ = setCurrentRange par $
typeError . GenericDocError =<< do
text "Unexpected parameter" <+> prettyA par
bindParameters npars [] t ret =
case unEl t of
Pi a b | not (visible a) -> do
x <- freshName_ (absName b)
bindParameter npars [] x a b ret
| otherwise ->
typeError . GenericDocError =<<
sep [ "Expected binding for parameter"
, text (absName b) <+> text ":" <+> prettyTCM (unDom a) ]
_ -> __IMPOSSIBLE__
bindParameters npars par@(A.DomainFull (A.TBind _ _ xs e) : bs) a ret =
setCurrentRange par $
typeError . GenericDocError =<< do
let s | length xs > 1 = "s"
| otherwise = ""
text ("Unexpected type signature for parameter" ++ s) <+> sep (map prettyA xs)
bindParameters _ (A.DomainFull A.TLet{} : _) _ _ = __IMPOSSIBLE__
bindParameters _ (par@(A.DomainFree _ arg) : ps) _ _
| getModality arg /= defaultModality = setCurrentRange par $
typeError . GenericDocError =<< do
text "Unexpected modality/relevance annotation in" <+> prettyA par
bindParameters npars ps0@(par@(A.DomainFree _ arg) : ps) t ret = do
let x = namedArg arg
TelV tel _ = telView' t
case insertImplicit arg $ telToList tel of
NoInsertNeeded -> continue ps $ A.unBind $ A.binderName x
ImpInsert _ -> continue ps0 =<< freshName_ (absName b)
BadImplicits -> setCurrentRange par $
typeError . GenericDocError =<< do
text "Unexpected parameter" <+> prettyA par
NoSuchName x -> setCurrentRange par $
typeError . GenericDocError =<< do
text ("No parameter of name " ++ x)
where
Pi dom@(Dom{domInfo = info', unDom = a}) b = unEl t
continue ps x = bindParameter npars ps x dom b ret
bindParameter :: Int -> [A.LamBinding] -> Name -> Dom Type -> Abs Type -> (Telescope -> Type -> TCM a) -> TCM a
bindParameter npars ps x a b ret =
addContext (x, a) $
bindParameters (npars - 1) ps (absBody b) $ \ tel s ->
ret (ExtendTel a $ Abs (nameToArgName x) tel) s
fitsIn :: UniverseCheck -> [IsForced] -> Type -> Sort -> TCM Int
fitsIn uc forceds t s = do
reportSDoc "tc.data.fits" 10 $
sep [ "does" <+> prettyTCM t
, "of sort" <+> prettyTCM (getSort t)
, "fit in" <+> prettyTCM s <+> "?"
]
vt <- do
t <- pathViewAsPi t
return $ case t of
Left (a,b) -> Just (True ,a,b)
Right (El _ t) | Pi a b <- t
-> Just (False,a,b)
_ -> Nothing
case vt of
Just (isPath, dom, b) -> do
withoutK <- withoutKOption
let (forced,forceds') = nextIsForced forceds
unless (isForced forced && not withoutK) $ do
sa <- reduce $ getSort dom
unless (isPath || uc == NoUniverseCheck || sa == SizeUniv) $ sa `leqSort` s
addContext (absName b, dom) $ do
succ <$> fitsIn uc forceds' (absBody b) (raise 1 s)
_ -> do
getSort t `leqSort` s
return 0
checkIndexSorts :: Sort -> Telescope -> TCM ()
checkIndexSorts s = \case
EmptyTel -> return ()
ExtendTel a tel' -> do
getSort a `leqSort` s
underAbstraction a tel' $ checkIndexSorts (raise 1 s)
data IsPathCons = PathCons | PointCons
deriving (Eq,Show)
constructs :: Int -> Int -> Type -> QName -> TCM IsPathCons
constructs nofPars nofExtraVars t q = constrT nofExtraVars t
where
constrT :: Nat -> Type -> TCM IsPathCons
constrT n t = do
t <- reduce t
pathV <- pathViewAsPi'whnf
case unEl t of
Pi _ (NoAbs _ b) -> constrT n b
Pi a b -> underAbstraction a b $ constrT (n + 1)
_ | Left ((a,b),_) <- pathV t -> do
_ <- case b of
NoAbs _ b -> constrT n b
b -> underAbstraction a b $ constrT (n + 1)
return PathCons
Def d es | d == q -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
(pars, ixs) <- normalise $ splitAt nofPars vs
checkParams n pars
return PointCons
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 (raise n $ dataSort $ theDef def) $ Def q $ map Apply $ us ++ xs
ifM (tryConversion $ equalType t t')
(constrT n t')
(typeError $ ShouldEndInApplicationOfTheDatatype t)
_ -> typeError $ ShouldEndInApplicationOfTheDatatype t
checkParams n vs = zipWithM_ sameVar vs ps
where
nvs = length vs
ps = reverse $ take nvs [n..]
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)
DataOrRecSig{} -> return Nothing
Function {} -> return Nothing
Datatype {} -> return (Just False)
Record { recInduction = Just CoInductive } -> return (Just True)
Record { recInduction = _ } -> return (Just False)
GeneralizableVar{} -> __IMPOSSIBLE__
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__
Dummy s _ -> __IMPOSSIBLE_VERBOSE__ s