{-# LANGUAGE CPP #-}
{-# LANGUAGE MultiWayIf #-}
module Agda.TypeChecking.Rules.Data where
import Control.Monad
import Data.List (genericTake)
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.Constraints
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.Interaction.Options
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
#include "undefined.h"
import Agda.Utils.Impossible
checkDataDef :: Info.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
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
, dataInduction = Inductive
, dataClause = Nothing
, dataCons = []
, dataSort = s
, dataAbstr = Info.defAbstract i
, dataMutual = Nothing
, dataPathCons = []
}
escapeContext 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"
(t, isPathCons) <- checkConstructorType e d
forcedArgs <- computeForcingAnnotations c t
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
let con = ConHead c Inductive []
escapeContext (size tel) $ do
cnames <- if nofIxs /= 0 || (Info.defAbstract i == AbstractDef) then return (emptyCompKit, Nothing) else do
inTopContext $ 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
]
defineProjections d con params names fields dataT
comp <- defineCompData d con params names fields dataT boundary
return $ (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 = cnames
, conForced = forcedArgs
, conErased = []
}
case snd cnames of
Nothing -> return ()
Just names -> mapM_ makeProjection names
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
]
sortsOk <- sortOk t `and2M` allM (map unDom (flattenTel fsT)) sortOkField
if not sortsOk || 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
((theName, gamma , ty, _cl_types , bodies), theSub) <-
(case cmd of DoTransp -> defineTranspForFields' (guard (not $ null boundary) >> (Just $ Con con ConOSystem $ teleElims fsT boundary))
; DoHComp -> defineHCompForFields)
(\ t p -> apply (Def p []) [argN t]) d params fsT (map argN names) t
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 Nothing 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
}
| 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
}
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
sortOk :: Type -> TCM Bool
sortOk a = reduce (getSort a) >>= \case
Type{} -> return True
_ -> return False
sortOkField :: Type -> TCM Bool
sortOkField a = reduce (getSort a) >>= \case
Type{} -> return True
Inf -> return True
_ -> return False
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 Nothing 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
}
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])
defineTranspForFields
:: (Term -> QName -> Term)
-> QName
-> Telescope
-> Telescope
-> [Arg QName]
-> Type
-> TCM ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
defineTranspForFields = defineTranspForFields' Nothing
defineTranspForFields'
:: (Maybe Term)
-> (Term -> QName -> Term)
-> QName
-> Telescope
-> Telescope
-> [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` 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 . unDom) filled_ty'
sort <- reduce $ getSort $ unDom filled_ty'
case sort of
Type 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
Inf ->
return $ runNames [] $ do
[field] <- mapM open [field]
field
_ -> __IMPOSSIBLE__
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, 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
-> Telescope
-> [Arg QName]
-> Type
-> 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 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 (getSort 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 (getSort 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 drect_gamma
lvl <- open . (\ (Type l) -> Level l) $ getSort 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 . unDom) filled_ty')
Type l <- reduce $ getSort $ 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 . unDom) filled_types)
bodys <- mapM mkBody (zip fns filled_types)
return $ ((theName, gamma, rtype, 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 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 { dataInduction = CoInductive } -> return (Just True)
Datatype { dataInduction = Inductive } -> 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