MiniAgda-0.2014.1.9: TypeChecker.hs
{-# LANGUAGE FlexibleInstances, TypeSynonymInstances,
PatternGuards, TupleSections, NamedFieldPuns #-}
module TypeChecker where
import Prelude hiding (null)
import Control.Applicative hiding (Const) -- ((<$>))
import Control.Monad
import Control.Monad.IfElse
import Control.Monad.Identity
import Control.Monad.State
import Control.Monad.Error
import Control.Monad.Reader
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Foldable as Foldable
import qualified Data.Traversable as Traversable
import Debug.Trace
import qualified Text.PrettyPrint as PP
import Util
import qualified Util as Util
import Abstract hiding (Substitute)
import Polarity as Pol
import Value
import TCM
import Eval
import Extract
-- import SPos (nocc) -- RETIRED
-- import CallStack
import PrettyTCM
import TraceError
import Warshall hiding (Flex) -- size constraint checking
import Termination
-- import Completness
traceCheck msg a = a -- trace msg a
traceCheckM msg = return () -- traceM msg
{-
traceCheck msg a = trace msg a
traceCheckM msg = traceM msg
-}
traceSing msg a = a -- trace msg a
traceSingM msg = return () -- traceM msg
{-
traceSing msg a = trace msg a
traceSingM msg = traceM msg
-}
traceAdm msg a = a -- trace msg a
traceAdmM msg = return () -- traceM msg
{-
traceAdm msg a = trace msg a
traceAdmM msg = traceM msg
-}
{- DEAD CODE
runWhnf :: Signature -> TypeCheck a -> IO (Either TraceError (a,Signature))
runWhnf sig tc = (runErrorT (runStateT tc sig))
-}
doNf sig e = runErrorT (runReaderT (runStateT (whnf emptyEnv e >>= reify) (initWithSig sig)) emptyContext)
doWhnf sig e = runErrorT (runReaderT (runStateT (whnf emptyEnv e >>= whnfClos) (initWithSig sig)) emptyContext)
-- top-level functions -------------------------------------------
runTypeCheck :: TCState -> TypeCheck a -> IO (Either TraceError (a,TCState))
runTypeCheck st tc = runErrorT (runReaderT (runStateT tc st) emptyContext)
-- runTypeCheck st tc = runCallStackT (runReaderT (runStateT tc st) emptyContext) []
typeCheck dl = runTypeCheck initSt (typeCheckDecls dl)
-- checking top-level declarations -------------------------------
echo :: MonadIO m => String -> m ()
echo = liftIO . putStrLn
echoR = echo
-- echoR s = echo $ "R> " ++ s
echoTySig :: (Show n, MonadIO m) => n -> Expr -> m ()
echoTySig n t = return () -- echo $ "I> " ++ n ++ " : " ++ show t
echoKindedTySig :: (Show n, MonadIO m) => Kind -> n -> Expr -> m ()
echoKindedTySig ki n t = echo $ prettyKind ki ++ " " ++ show n ++ " : " ++ show t
echoKindedDef :: (Show n, MonadIO m) => Kind -> n -> Expr -> m ()
echoKindedDef ki n t = echo $ prettyKind ki ++ " " ++ show n ++ " = " ++ show t
echoEPrefix = "E> "
echoTySigE :: (Show n, MonadIO m) => n -> Expr -> m ()
echoTySigE n t = echo $ echoEPrefix ++ show n ++ " : " ++ show t
echoDefE :: (Show n, MonadIO m) => n -> Expr -> m ()
echoDefE n t = echo $ echoEPrefix ++ show n ++ " = " ++ show t
-- the type checker returns pruned (extracted) terms
-- with irrelevant subterms replaced by Irr
typeCheckDecls :: [Declaration] -> TypeCheck [EDeclaration]
typeCheckDecls [] = return []
typeCheckDecls (d:ds) = do
de <- typeCheckDeclaration d
dse <- typeCheckDecls ds
return (de ++ dse)
-- since a data declaration generates destructor declarations
-- we need to return a list here
typeCheckDeclaration :: Declaration -> TypeCheck [EDeclaration]
typeCheckDeclaration (OverrideDecl Check ds) = do
st <- get
typeCheckDecls ds
put st -- forget the effect of these decls
return []
typeCheckDeclaration (OverrideDecl Fail ds) = do
st <- get
r <- (typeCheckDecls ds >> return True) `catchError`
(\ s -> do liftIO $ putStrLn ("block fails as expected, error message:\n" ++ show s)
return False)
if r then fail "unexpected success" else do
put st
return []
typeCheckDeclaration (OverrideDecl TrustMe ds) =
newAssertionHandling Warning $ typeCheckDecls ds
typeCheckDeclaration (OverrideDecl Impredicative ds) =
goImpredicative $ typeCheckDecls ds
typeCheckDeclaration (RecordDecl n tel t0 c fields) =
-- just one "mutual" declaration
checkingMutual (Just $ DefId DatK $ QName n) $ do
result <- typeCheckDataDecl n NotSized CoInd [] tel t0 [c] fields
checkPositivityGraph
return result
typeCheckDeclaration (DataDecl n sz co pos0 tel t0 cs fields) =
-- just one "mutual" declaration
checkingMutual (Just $ DefId DatK $ QName n) $ do
result <- typeCheckDataDecl n sz co pos0 tel t0 cs fields
checkPositivityGraph
return result
typeCheckDeclaration (LetDecl eval n tel mt e) = enter (show n) $ do
{- MOVED to checkLetDef
(tel, (vt, te, Kinded ki ee)) <- checkTele tel $ checkOrInfer neutralDec e mt
te <- return $ teleToType tel te
ee <- return $ teleLam tel ee
vt <- whnf' te
-}
(vt, te, Kinded ki ee) <- checkLetDef neutralDec tel mt e
rho <- getEnv -- is emptyEnv
-- TODO: solve size constraints
-- does not work with emptyEnv
-- [te, ee] <- solveAndModify [te, ee] rho -- solve size constraints
let v = mkClos rho ee -- delay whnf computation
-- v <- whnf' ee -- WAS: whnf' e'
addSig n (LetSig vt ki v $ undefinedFType $ QName n) -- late (var -> expr) binding, but ok since no shadowing
-- addSig n (LetSig vt e') -- late (var -> expr) binding, but ok since no shadowing
echoKindedTySig ki n te
-- echoTySigE n te
-- echoDefE n ee
echoKindedDef ki n ee
return [LetDecl eval n emptyTel (Just te) ee]
typeCheckDeclaration d@(PatternDecl x xs p) = do
{- WHY DOES THIS NOT TYPECHECK?
let doc = (PP.text "pattern") <+> (PP.hsep (List.map Util.pretty (x:xs))) <+> PP.equals <+> Util.pretty p
echo $ PP.render $ doc
-}
echo $ "pattern " ++ Util.showList " " show (x:xs) ++ " = " ++ show p
v <- whnf' $ foldr (Lam defaultDec) (patternToExpr p) xs
addSig x (PatSig xs p v)
return [d]
typeCheckDeclaration (MutualFunDecl False co funs) =
-- traceCheck ("type checking a function block") $
do
funse <- typeCheckFuns co funs
return $ [MutualFunDecl False co funse]
typeCheckDeclaration (MutualFunDecl True co funs) =
-- traceCheck ("type checking a block of measured function") $
do
funse <- typeCheckMeasuredFuns co funs
return $ [MutualFunDecl False co funse]
typeCheckDeclaration (MutualDecl measured ds) = do
-- first check type signatures
-- we add the typings into the context, not the signature
ktss <- typeCheckMutualSigs ds
-- register the mutually defined names
let ns = for ktss $ \ (Kinded _ (TypeSig n _)) -> n
addMutualNames = local $ \ e -> e { mutualNames = ns ++ mutualNames e }
-- then check bodies
-- we need to construct a positivity graph
edss <- addKindedTypeSigs ktss $ addMutualNames $
zipWithM (typeCheckMutualBody measured) (map (predKind . kindOf) ktss) ds
-- check and reset positivity graph
checkPositivityGraph
return $ concat edss
-- check signatures of a flattened mutual block
typeCheckMutualSigs :: [Declaration] -> TypeCheck [Kinded (TySig TVal)]
typeCheckMutualSigs [] = return []
typeCheckMutualSigs (d:ds) = do
kts@(Kinded ki (TypeSig n tv)) <- typeCheckMutualSig d
new' n (Domain tv ki defaultDec) $ do
ktss <- typeCheckMutualSigs ds
return $ kts : ktss
typeCheckSignature :: TySig Type -> TypeCheck (Kinded (TySig TVal))
typeCheckSignature (TypeSig n t) = do
echoTySig n t
Kinded ki te <- checkType t
tv <- whnf' te
return $ Kinded (predKind ki) $ TypeSig n tv
typeCheckMutualSig :: Declaration -> TypeCheck (Kinded (TySig TVal))
typeCheckMutualSig (LetDecl ev n tel (Just t) e) =
typeCheckSignature $ TypeSig n $ teleToType tel t
typeCheckMutualSig (DataDecl n sz co pos tel t cs fields) = do
Kinded ki ts <- typeCheckSignature (TypeSig n (teleToType tel t))
return $ Kinded ki ts
typeCheckMutualSig (FunDecl co (Fun ts n' ar cls)) =
typeCheckSignature ts
typeCheckMutualSig (OverrideDecl TrustMe [d]) =
newAssertionHandling Warning $ typeCheckMutualSig d
typeCheckMutualSig (OverrideDecl Impredicative [d]) =
goImpredicative $ typeCheckMutualSig d
typeCheckMutualSig d = fail $ "typeCheckMutualSig: panic: unexpected declaration " ++ show d
-- typeCheckMutualBody measured kindCandidate
typeCheckMutualBody :: Bool -> Kind -> Declaration -> TypeCheck [EDeclaration]
typeCheckMutualBody measured _ (DataDecl n sz co pos tel t cs fields) = do
-- set name of mutual thing whose body we are checking
checkingMutual (Just $ DefId DatK $ QName n) $
--
typeCheckDataDecl n sz co pos tel t cs fields
typeCheckMutualBody measured@False ki (FunDecl co fun@(Fun ts@(TypeSig n t) n' ar cls)) = do
checkingMutual (Just $ DefId FunK $ QName n) $ do
fun' <- typeCheckFunBody co ki fun
return $ [FunDecl co fun']
typeCheckDataDecl :: Name -> Sized -> Co -> [Pol] -> Telescope -> Type -> [Constructor] -> [Name] -> TypeCheck [EDeclaration]
typeCheckDataDecl n sz co pos0 tel0 t0 cs0 fields = enter (show n) $
(do -- sig <- gets signature
let params = size tel0
-- in case we are dealing with a sized type, check that
-- the polarity annotation (if present) at the size arg. is correct.
(p', pos, t) <- do
case sz of
Sized -> do
let polsz = if co==Ind then Pos else Neg
t <- case t0 of
Quant Pi (TBind x (Domain domt ki dec)) b | isSize domt ->
case (polarity dec) of
-- insert correct polarity annotation if none was there
pol | pol `elem` [Param,Rec] -> return $ Quant Pi (TBind x $ Domain tSize kSize $ setPol polsz dec) b
pol | pol == polsz -> return t0
pol -> fail $ "sized type " ++ show n ++ " has wrong polarity annotation " ++ show pol ++ " at Size argument, it should be " ++ show polsz
t0 -> return t0
return (params + 1, pos0 ++ [polsz], t)
NotSized -> return (params, pos0, t0)
-- compute full type signature (including parameter telescope)
let dt = (teleToType tel0 t)
echoTySig n dt
{- mmh, this does not work, e.g. data Id (A : Set)(a : A) : A -> Set
then A -> Set is not distinguishable from Set -> Set (GADT)
unclear what to do...
dte <- checkTele tel $ \ tele -> do
te <- checkSmallType t
return (teleToType tele te)
-}
-- get the target sort ds of the datatype
Kinded ki0 (ds, dte) <- checkDataType p' dt -- TODO?: use above code?
let ki = dataKind ki0
echoKindedTySig ki n dte
-- echoTySigE n dte
v <- whnf emptyEnv dte
Just fkind <- extractKind v
-- get the updated telescope which contains the kinds
let (tel, dtcore) = typeToTele' params dte
-- compute the constructor telescopes
cs0 <- mapM (insertConstructorTele tel dtcore) cs0
let cis = analyzeConstructors co n tel cs0
let cs = map reassembleConstructor cis
addSig n (DataSig { numPars = params
, positivity = pos
, isSized = sz
, isCo = co
, symbTyp = v
, symbolKind = ki
, constructors = cis
, etaExpand = False
, isTuple = False
-- if cs==[] then Just [] else Nothing
{- OLD CODE
, constructors = map namePart cs
-- at first, do not add destructors, get them out later
, destructors = Nothing
, isFamily = t /= Set -- currently UNUSED
-}
, extrTyp = fkind
})
when (sz == Sized) $
szType co params v
(isRecList, kcse) <- liftM unzip $
mapM (typeCheckConstructor n dte sz co pos tel) cs
-- compute the kind of the data type from the kinds of the
-- constructor arguments (mmh, DOES NOT WORK FOR MUTUAL DATA!)
let newki = case (foldl unionKind NoKind (map kindOf kcse)) of
NoKind -> kType -- no non-rec constructor arguments
AnyKind -> AnyKind
Kind s s' -> Kind (Set Zero) s' -- a data type is always also a type
-- echoKindedTySig newki n dte -- 2012-01-26 disabled (repetitive)
-- solve for size variables
sol <- solveConstraints
-- TODO: substitute
resetConstraints
-- add destructors only for the constructors that are non-overlapping
let decls = concat $ map mkDestrs cis
-- cEtaExp = True means that all field names are present
-- and constructor is not overlapping with others
mkDestrs ci | cEtaExp ci = concat $ map mkDestr (cFields ci)
| otherwise = []
mkDestr fi =
case (fClass fi) of
Field (Just (ty, arity, cl)) | not (erased $ fDec fi) && not (emptyName $ fName fi) ->
let n' = fName fi
n = internal n'
in
[MutualFunDecl False Ind [Fun (TypeSig n ty) n' arity [cl]]]
_ -> []
when (not (null decls)) $
traceCheckM $ "generated destructors: " ++ show decls
declse <- mapM (\ d@(MutualFunDecl False co [Fun (TypeSig n t) n' ar cls]) -> do
-- echo $ "G> " ++ showFun co ++ " " ++ show n ++ " : " ++ show t
-- echo $ "G> " ++ PP.render (prettyFun n cls)
checkingMutual Nothing $ typeCheckDeclaration d)
decls
-- decide whether to eta-expand at this type
-- all patterns need to be proper and non-overlapping
-- at least one constructor needs to be eta-expandable
let isPatIndFam = all (\ ci -> fst (cPatFam ci) /= NotPatterns && cEtaExp ci) cis
-- && not (or overlapList)
-- do not eta-expand recursive constructors (might not terminate)
let disableRec ci {-ov-} rec' = ci
{ cRec = rec'
, cEtaExp = cEtaExp ci -- all destructors present
&& fst (cPatFam ci) /= NotPatterns -- proper pattern to compute indices
-- && not ov -- non-overlapping
&& not (co==Ind && rec') } -- non-recursive
let cis' = zipWith disableRec cis {-overlapList-} isRecList
let typeEtaExpandable = isPatIndFam && (null cis || any cEtaExp cis')
traceEtaM $ "data " ++ show n ++ " eta-expandable " ++ show typeEtaExpandable ++ " constructors " ++ show cis'
modifySig n (\ dataSig ->
dataSig { symbolKind = newki
, etaExpand = typeEtaExpandable
, constructors = cis'
, isTuple = length cis' >= 1 && isPatIndFam
})
-- compute extracted data decl
let (tele, te) = typeToTele' (size tel) dte
return $ (DataDecl n sz co pos tele te (map valueOf kcse) fields) : concat declse
) -- `throwTrace` n -- in case of an error, add name n to the trace
insertConstructorTele :: Telescope -> Type -> Constructor -> TypeCheck Constructor
insertConstructorTele dtel dt c@(Constructor n Nothing t) = return c
insertConstructorTele dtel dt c@(Constructor n Just{} t) = do
res <- computeConstructorTele dtel dt t
return $ Constructor n (Just res) t
-- | @computeConstructorTele dtel t = return ctel@
-- Computes the constructor telescope from the target.
computeConstructorTele :: Telescope -> Type -> Type -> TypeCheck (Telescope, [Pattern])
computeConstructorTele dtel dt t = do
-- target is data name applied to parameters and indices
let (_, target) = typeToTele t
(_, es) = spineView target
pars = take (size dtel) es
(cxt, ps) <- checkConstructorParams pars =<< whnf' (teleToType dtel dt)
(,ps) . setDec (Dec Param) <$> do local (const cxt) $ contextToTele cxt
-- | @checkConstructorParams pars tv = return cxt@
-- Checks that parameters @pars@ are patterns elimating the datatype @tv@.
-- Returns a context @cxt@ that binds the pattern variables in
-- left-to-right order.
checkConstructorParams :: [Expr] -> TVal -> TypeCheck (TCContext, [Pattern])
checkConstructorParams es tv = do
-- for now, we only allow patterns in parameters
-- could be extended to unifyable expressions in general
ps <- mapM (\ e -> maybe (errorParamNotPattern e) return $ exprToPattern e) es
-- no goals from dot patterns, no absurd pattern
([],_,cxt,_,_,_,False) <- checkPatterns defaultDec [] emptySub tv ps
return (cxt, ps)
where
errorParamNotPattern e = fail $
"expected parameter to be a pattern, but I found " ++ show es
-- |
-- Precondition: @ce@ is included in the current context.
contextToTele :: TCContext -> TypeCheck Telescope
contextToTele ce = do
let n :: Int
n = len (context ce) -- context length
delta :: Map Int (OneOrTwo Domain)
delta = cxt (context ce) -- types for dB levels
names :: Map Int Name
names = naming ce -- names for dB levels
-- traverse the context from left to right
Telescope <$> do
forM [0..n-1] $ \ k -> do
x <- lookupM k names
One dom <- lookupM k delta
TBind x <$> Traversable.traverse toExpr dom
-- | @typeCheckConstructor d dt sz co pols tel (TypeSig c t)@
--
-- returns True if constructor has recursive argument
typeCheckConstructor :: Name -> Type -> Sized -> Co -> [Pol] -> Telescope -> Constructor -> TypeCheck (Bool, Kinded EConstructor)
typeCheckConstructor d dt sz co pos dtel (Constructor n mctel t) = enter ("constructor " ++ show n) $ do
let tel = maybe dtel fst mctel
{-
tel <- case cpars of
-- old style data parameters
Nothing -> return dtel
-- new style pattern parameters
Just{} -> computeConstructorTele dtel dt t
-}
sig <- gets signature
let telE = setDec irrelevantDec tel -- need kinded tel!!
-- parameters are erased in types of constructors
let tt = teleToType telE t
echoTySig n tt
let params = size tel
-- when checking constructor types, do NOT resurrect telescope
-- data T [A : Set] : Set { inn : A -> T A }
-- should be rejected, since A ~= T A, and T A = T B means A ~=B for arb. A, B!
-- add data name as spos var, to check positivity
-- and as NoKind, to compute the true kind from the constructors
let telWithD = Telescope $ (TBind d $ Domain dt NoKind $ Dec SPos) : telescope tel
Kinded ki te <- addBinds telWithD $
checkConType sz t -- do NOT resurrect telescope!!
-- Check target of constructor.
dv <- whnf' dt
let (Telescope argts,target) = typeToTele te
whenNothing mctel $ -- only for old-style parameters
addBinds telWithD $ addBinds (Telescope argts) $ checkTarget d dv tel target
-- Make type of a constructor a singleton type.
let mkName i n | emptyName n = fresh $ "y" ++ show i
| otherwise = n
fields = map boundName argts
argns = zipWith mkName [0..] $ fields
argtbs = zipWith (\ n tb -> tb { boundName = n }) argns argts
-- core = (foldl App (con (coToConK co) n) $ map Var argns)
core = Record (NamedRec (coToConK co) n False notDotted) $ zip fields $ map Var argns
tsing = teleToType (Telescope argtbs) $ Sing core target
let tte = teleToType telE tsing -- te -- DO resurrect here!
vt <- whnf' tte
-- Now, compute the remaining information concerning the constructor.
{- old code was more accurate, since it evaluated before checking
for recursive occurrence.
recOccs <- sposConstructor d 0 pos vt -- get recursive occurrences
-}
mutualNames <- asks mutualNames
let mutOcc tb = not $ null $ List.intersect (d:mutualNames) $ usedDefs $ boundType tb
recOccs = map mutOcc argts
isRec = or recOccs
-- fType <- extractType vt -- moved to Extract
let fType = undefinedFType n
isSz <- if sz /= Sized then return Nothing else do
szConstructor d co params vt -- check correct use of sizes
if co == CoInd then return $ Just $ error "impossible lhs type of coconstructor" else do
let (x, lte) = mapSnd (teleToType telE) $ mkConLType params te
echoKindedTySig kTerm n lte
ltv <- whnf' lte
return $ Just (x, ltv)
-- Add the type constructor to the signature.
let cpars = fmap (mapFst (map boundName . telescope)) mctel -- deletes types, keeps names
addSigQ n (ConSig cpars isSz recOccs vt d (size dtel) fType)
-- let (tele, te) = typeToTele (length tel) tte -- NOT NECESSARY
echoKindedTySig kTerm n tte
-- traceM ("kind of " ++ n ++ "'s args: " ++ show ki)
-- echoTySigE n tte
return (isRec, Kinded ki $ Constructor n (fmap (mapFst (const telE)) mctel) te)
typeCheckMeasuredFuns :: Co -> [Fun] -> TypeCheck [EFun]
typeCheckMeasuredFuns co funs0 = do
-- echo $ show funs
kfse <- mapM typeCheckFunSig funs0 -- NO LONGER erases measure
-- use erased type signatures with retaines measure
let funs = zipWith (\ (Kinded ki ts) f -> f { funTypeSig = ts }) kfse funs0
-- type check and solve size constraints
-- return clauses with meta vars resolved
kcle <- installFuns co (zipWith Kinded (map kindOf kfse) funs) $
mapM typeCheckFunClauses funs
let kis = map kindOf kcle
let clse = map valueOf kcle
{-
-- replace old clauses by new ones in funs
let funs' = zipWith (\(tysig,(ar,cls)) cls' -> (tysig,(ar,cls'))) funs clss
-}
-- get the list of mutually defined function names
let funse = List.zipWith4 Fun
(map (fmap eraseMeasure . valueOf) kfse)
(map funExtName funs)
(map funArity funs)
clse
-- print reconstructed clauses
mapM_ (\ (Fun (TypeSig n t) n' ar cls) -> do
-- echoR $ n ++ " : " ++ show t
echoR $ (PP.render $ prettyFun n cls))
funse
-- replace in signature by erased clauses
zipWithM (enableSig co) (zipWith intersectKind kis $ map kindOf kfse) funse
return $ funse
where
enableSig :: Co -> Kind -> Fun -> TypeCheck ()
enableSig co ki (Fun (TypeSig n t) n' ar' cl') = do
vt <- whnf' t
addSig n (FunSig co vt ki ar' cl' True $ undefinedFType $ QName n)
-- add a let binding for external use
v <- up False (vFun n) vt
addSig n' (LetSig vt ki v $ undefinedFType $ QName n')
-- type check the body of one function in a mutual block
-- type signature is already checked and added to local context
typeCheckFunBody :: Co -> Kind -> Fun -> TypeCheck EFun
typeCheckFunBody co ki0 fun@(Fun ts@(TypeSig n t) n' ar cls0) = do
-- echo $ show fun
addFunSig co $ Kinded ki0 fun
-- type check and solve size constraints
-- return clauses with meta vars resolved
Kinded ki clse <- setCo co $ typeCheckFunClauses fun
-- check new clauses for admissibility, inserting "unusuable" flags in the patterns where necessary
-- TODO: proper cleanup, proper removal of admissibility check!
-- clse <- admCheckFunSig co names ts clse
-- print reconstructed clauses
-- echoR $ n ++ " : " ++ show t
echoR $ (PP.render $ prettyFun n clse)
-- replace in signature by erased clauses
let fune = Fun ts n' ar clse
enableSig ki fune
return fune
typeCheckFuns :: Co -> [Fun] -> TypeCheck [EFun]
typeCheckFuns co funs0 = do
-- echo $ show funs
kfse <- mapM typeCheckFunSig funs0
let kfuns = zipWith (\ (Kinded ki ts) (Fun ts0 n' ar cls) -> Kinded ki (Fun ts n' ar cls)) kfse funs0
-- zipWithM (addFunSig co) (map kindOf kfse) funs
mapM (addFunSig co) kfuns
let funs = map valueOf kfuns
-- type check and solve size constraints
-- return clauses with meta vars resolved
kce <- setCo co $ mapM typeCheckFunClauses funs
let kis = map kindOf kce
let clse = map valueOf kce
-- get the list of mutually defined function names
let names = map (\ (Fun (TypeSig n t) n' ar cls) -> n) funs
-- check new clauses for admissibility, inserting "unusuable" flags in the patterns where necessary
-- TODO: proper cleanup, proper removal of admissibility check!
clse <- zipWithM (\ (Fun tysig _ _ _) cls' -> admCheckFunSig co names tysig cls') funs clse
-- replace old clauses by new ones in funs
let funse = List.zipWith4 Fun
(map valueOf kfse)
(map funExtName funs)
(map funArity funs)
clse
-- let funse = zipWith (\(tysig,(ar,cls)) cls' -> (tysig,(ar,cls'))) funs clse
-- print reconstructed clauses
mapM_ (\ (Fun (TypeSig n t) n' ar cls) -> do
-- echoR $ n ++ " : " ++ show t
echoR $ (PP.render $ prettyFun n cls))
funse
terminationCheck funse
-- replace in signature by erased clauses
zipWithM enableSig kis funse
return $ funse
addFunSig :: Co -> Kinded Fun -> TypeCheck ()
addFunSig co (Kinded ki (Fun (TypeSig n t) n' ar cl)) = do
sig <- gets signature
vt <- whnf' t -- TODO: PROBLEM for internal extraction (would need te here)
addSig n (FunSig co vt ki ar cl False $ undefinedFType $ QName n) --not yet type checked / termination checked
-- ADMCHECK FOR COFUN is not taking place in checking the lhs
-- TODO: proper analysis for size patterns!
-- admCheckFunSig mutualNames (TypeSig thisName thisType, clauses)
admCheckFunSig :: Co -> [Name] -> TypeSig -> [Clause] -> TypeCheck [Clause]
admCheckFunSig CoInd mutualNames (TypeSig n t) cls = return cls
admCheckFunSig co@Ind mutualNames (TypeSig n t) cls = traceAdm ("admCheckFunSig: checking admissibility of " ++ show n ++ " : " ++ show t) $
(
do -- a function is not recursive if did does not mention any of the
-- mutually defined function names
let usedNames = rhsDefs cls
let notRecursive = all (\ n -> not (n `elem` usedNames)) mutualNames
-- for non-recursive functions, we can skip the admissibility check
if notRecursive then
-- trace ("function " ++ n ++ " is not recursive") $
return cls
else -- trace ("function " ++ n ++ " is recursive ") $
do vt <- whnf' t
admFunDef co cls vt
) `throwTrace` ("checking type of " ++ show n ++ " for admissibility")
enableSig :: Kind -> Fun -> TypeCheck ()
enableSig ki (Fun (TypeSig n _) n' ar' cl') = do
(FunSig co vt ki0 ar cl _ ftyp) <- lookupSymb n
addSig n (FunSig co vt (intersectKind ki ki0) ar cl' True ftyp)
-- add a let binding for external use
v <- up False (vFun n) vt
addSig n' (LetSig vt ki v ftyp)
-- typeCheckFunSig (TypeSig thisName thisType, clauses)
typeCheckFunSig :: Fun -> TypeCheck (Kinded ETypeSig)
typeCheckFunSig (Fun (TypeSig n t) n' ar cls) = enter ("type of " ++ show n) $ do
echoTySig n t
Kinded ki0 te <- checkType t
-- let te = eraseMeasure te0
let ki = predKind ki0
echoKindedTySig ki n (eraseMeasure te)
-- echoTySigE n te
return $ Kinded ki $ TypeSig n te
typeCheckFunClauses :: Fun -> TypeCheck (Kinded [EClause])
typeCheckFunClauses (Fun (TypeSig n t) n' ar cl) = enter (show n) $
do result@(Kinded _ cle) <- checkFun t cl
-- traceCheck (show (TypeSig n t)) $
-- traceCheck (show cl') $
-- echo $ PP.render $ prettyFun n cle
return result
-- checkConType sz t = Kinded ki te
-- the returned kind is the kind of the constructor arguments
-- check that result is a universe
-- ( params were already checked by checkDataType and are not included in t )
-- called initially in the context consisting of the parameter telescope
checkConType :: Sized -> Expr -> TypeCheck (Kinded Extr)
checkConType NotSized t = checkConType' t
checkConType Sized t =
case t of
Quant Pi tb@(TBind _ (Domain t1 _ _)) t2 | isSize t1 -> do
addBind (mapDec (const paramDec) tb) $ do -- size is parametric in constructor type
Kinded ki t2e <- checkConType' t2
return $ Kinded ki $ Quant Pi (mapDec (const irrelevantDec) tb) t2e -- size is irrelevant in constructor
_ -> fail $ "checkConType: expecting size quantification, found " ++ show t
checkConType' :: Expr -> TypeCheck (Kinded Extr)
checkConType' t = do
(s, kte) <- checkingCon True $ inferType t
case s of
Set{} -> return kte
CoSet{} -> return kte
_ -> fail $ "checkConType: type " ++ show t ++ " of constructor not a universe"
-- check that the data type and the parameter arguments (written down like declared in telescope)
-- precondition: target tg type checks in current context
checkTarget :: Name -> TVal -> Telescope -> Type -> TypeCheck ()
checkTarget d dv tel tg = do
tv <- whnf' tg
case tv of
VApp (VDef (DefId DatK (QName n))) vs | n == d -> do
telvs <- mapM (\ tb -> whnf' (Var (boundName tb))) $ telescope tel
enter ("checking datatype parameters in constructor target") $
leqVals' N mixed (One dv) (take (size tel) vs) telvs
return ()
_ -> fail $ "constructor should produce something in data type " ++ show d
{- RETIRED (syntactic check)
checkTarget :: Name -> Telescope -> Type -> TypeCheck ()
checkTarget d tel tg =
case spineView tg of
(Def (DefId Dat n), args) | n == d -> checkParams tel (take (length tel) args)
_ -> throwErrorMsg $ "target mismatch" ++ show tg
where checkParams :: Telescope -> [Expr] -> TypeCheck ()
checkParams [] [] = return ()
checkParams (tb : tl) ((Var n') : el) | boundName tb == n'
= checkParams tl el
checkParams tl al = throwErrorMsg $ "target param mismatch " ++
d ++ " " ++ show tel ++ " != " ++ show tg ++ "\ncheckParams " ++ show tl ++ " " ++ show al ++ " failed"
-}
-- check that params are types
-- check that arguments are stypes
-- check that target is set
checkDataType :: Int -> Expr -> TypeCheck (Kinded (Sort Expr, Extr))
checkDataType p e = do
traceCheckM ("checkDataType " ++ show e ++ " p=" ++ show p)
case e of
Quant Pi tb@(TBind x (Domain t1 _ dec)) t2 -> do
k <- getLen
traceCheckM ("length of context = " ++ show k)
-- t1e <- checkingDom $ if k <= p then checkType t1 else checkSmallType t1
(s1, Kinded ki0 t1e) <- checkingDom $ inferType t1
let ki1 = predKind ki0
addBind (TBind x (Domain t1 ki1 defaultDec)) $ do
Kinded ki2 (s, t2e) <- checkDataType p t2
-- when k <= p $ ltSort s1 s -- check size of indices (disabled)
return $ Kinded ki2 (s, Quant Pi (TBind x (Domain t1e ki1 dec)) t2e)
Sort s@(Set e1) -> do
(_, e1e) <- checkLevel e1
return $ Kinded (kUniv e1e) (s, Sort $ Set e1e)
Sort s@(CoSet e1) -> do
e1e <- checkSize e1
return $ Kinded (kUniv Zero) (s, Sort $ CoSet e1e)
_ -> throwErrorMsg "doesn't target Set or CoSet"
{-
checkSize :: Expr -> TypeCheck Extr
checkSize Infty = return Infty
checkSize e = valueOf <$> checkExpr e vSize
-}
checkSize :: Expr -> TypeCheck Extr
checkSize e =
case e of
Meta i -> do
ren <- asks renaming
addMeta ren i
return e
e -> inferSize e
inferSize :: Expr -> TypeCheck Extr
inferSize e =
case e of
Zero -> return e
Infty -> return e
Succ e -> Succ <$> checkSize e
Plus es -> Plus <$> mapM checkSize es
Max es -> maxE <$> mapM checkSize es
e -> do
(v, Kinded ki e) <- inferExpr e
subtype v vSize
return e
checkBelow :: Expr -> LtLe -> Val -> TypeCheck Extr
checkBelow e Le VInfty = checkSize e
checkBelow e ltle v = do
e' <- checkSize e
v' <- whnf' e
leSize ltle Pos v' v
return e'
-- checkLevel e = (value of e, ee)
-- if e : Size and value of e != Infty
checkLevel :: Expr -> TypeCheck (Val, Extr)
checkLevel e = do
Kinded _ ee <- checkExpr e vSize
v <- whnf' e
when (v == VInfty) $ recoverFail $ "# is not a valid universe level"
return (v, ee)
{- Kind inference
i : Size : Type
t : Nat : Set : Set1 : ... : Type = Set\omega
p : P : Prop : Set : ...
Functional, cumulative PTS (s,s',s') written (s,s')
(Size,s) s != Size size-dependency
(s,Prop) impredicative Prop
(Set_i,Set_j) i <= j predicativity
Kind can be used to construct Kinds
term t terms, types, universes, proofs, propositions
type T types, universes, propositions
size i types, universes, propositions
prf p proofs
pred P types, universes, propositions
We like to infer kinds of expressions
Tm < Set < Set1 < Set2 < ...
For t : A if kind(A) = Tm then t is a term,
= Set then t is a type,
= Set1 then t is a type1 (e.g, a universe) ...
Then, if t : (x : A) -> B
and kind(A) `irrelevantFor` kind(B) [ with irrelevantFor := > ]
we can change the type signature to
t : [x : A] -> B
This is because you cannot eliminate a type to produce a term.
kind(Set) = Set
kind(Size) = Size -- this means that we treat sizes as types, they cannot
kind(s) = s -- if s is a sort
kind((x : A) -> B) = kind(B)
kind(A : Set0) = Tm
kind(A : Prop) = Prf
kind(A : Size) = <<impossible>>
kind(A : Setk) = k-1
irrFor Tm _ = False
irrFor Ty Tm = True
irrFor Ty Prf = True
irrFor Ty _ = False
irrFor Size Tm = True
irrFor Size Prf = True
One problem is that we cannot infer exact kinds, e.g.
fun T : Bool -> Set 1 -- T is a type
{ T true = Bool -- T true is a type
; T false = Set 0 -- T false is a universe
}
T is either a type or a universe. So we can only assign intervals.
This is like in Augustsson's Cayenne [not in his paper, though].
A datatype is always a type. A size is a type.
A constructor is always a term.
-}
-- type checking
-- checkExpr e tv = (e', ki)
-- e' is the version of e with erasure marker at irrelevant positions
-- ki is the kind of e (Tm, Ty, Set ...)
-- ki is at most the predecessor of the sort of tv
--
-- this is *internal* extraction in the style of Barras and Bernardo
-- e.g., does not prune t : Id A a b
-- thus, we can use the pruned version for evaluation!
checkExpr :: Expr -> TVal -> TypeCheck (Kinded Extr)
checkExpr e v = do
l <- getLen
enterDoc (text ("checkExpr " ++ show l ++ " |-") <+> prettyTCM e <+> colon <+> prettyTCM v) $ do
ce <- ask
traceCheck ("checkExpr: " ++ show (renaming ce) ++ ";" ++ show (context ce) ++ " |- " ++ show e ++ " : " ++ show v ++ " in env" ++ show (environ ce)) $ do
(case (e, v) of
{- In the presence of full bracket types,
we could implement the following "resurrecting version of let"
Gamma |- s : [A]
Gamma, x:A |- t : C Gamma, x:A, y:A |- t = t[y/x] : C
-------------------------------------------------------
Gamma |- let x:[A] = s in t : C
-}
(App (Lam dec x f) e, v) | inferable e -> checkLet dec x emptyTel Nothing e f v
{-
(LLet (TBind x (Domain Nothing _ dec)) e1 e2, v) -> checkUntypedLet x dec e1 e2 v
(LLet (TBind x (Domain (Just t1) _ dec)) e1 e2, v) -> checkTypedLet x t1 dec e1 e2 v
-}
(LLet (TBind x (Domain mt _ dec)) tel e1 e2, v) -> checkLet dec x tel mt e1 e2 v
(Case (Var x) Nothing [Clause _ [SuccP (VarP y)] (Just rhs)], v) -> do
(tv, _) <- resurrect $ inferExpr (Var x)
subtype tv vSize
vx@(VGen i) <- whnf' (Var x)
endsInSizedCo i v
let dom = Domain vSize kSize defaultDec
newWithGen y dom $ \ j vy -> do
let vp = VSucc vy
addSizeRel j 1 i $
addRewrite (Rewrite vx vp) [v] $ \ [v'] -> do
Kinded ki2 rhse <- checkRHS emptySub rhs v'
return $ Kinded ki2 $ Case (Var x) (Just tSize) [Clause [TBind y dom] [SuccP (VarP y)] (Just rhse)]
(Case e mt cs, v) -> do
(tv, t, Kinded ki1 ee) <- checkOrInfer neutralDec e mt
ve <- whnf' ee
-- tv' <- sing' ee tv -- DOES NOT WORK
Kinded ki2 cle <- checkCases ve (arrow tv v) cs
return $ Kinded ki2 $ Case ee (Just t) cle
{-
(Case e Nothing cs, _) -> do
(tv, Kinded ki1 ee) <- inferExpr e
ve <- whnf' ee
-- tv' <- sing' ee tv -- DOES NOT WORK
Kinded ki2 cle <- checkCases ve (arrow tv v) cs
t <- toExpr tv
return $ Kinded ki2 $ Case ee (Just t) cle
-}
(_, VGuard beta bv) ->
addBoundHyp beta $ checkExpr e bv
(e,v) | inferable e -> do
(v2, Kinded ki1 ee) <- inferExpr e
checkSubtype ee v2 v
return $ Kinded ki1 ee
_ -> checkForced e v
) -- >> (trace ("checkExpr successful: " ++ show e ++ ":" ++ show v) $ return ())
-- | checkLet @let .x tel : t = e1 in e2@
checkLet :: Dec -> Name -> Telescope -> Maybe Type -> Expr -> Expr -> TVal -> TypeCheck (Kinded Extr)
checkLet dec x tel mt1 e1 e2 v = do
(v_t1, t1e, Kinded ki1 e1e) <- checkLetDef dec tel mt1 e1
-- (v_t1, t1e, Kinded ki1 e1e) <- checkOrInfer dec e1 mt1
checkLetBody x t1e v_t1 ki1 dec e1e e2 v
-- | checkLetDef @.x tel : t = e@ becomes @.x : tel -> t = \ tel -> e@
checkLetDef :: Dec -> Telescope -> Maybe Type -> Expr -> TypeCheck (TVal, EType, Kinded Extr)
checkLetDef dec tel mt e = local (\ cxt -> cxt {consistencyCheck = True}) $ do
-- 2013-04-01
-- since a let telescope is treated like a lambda abstraction
-- and the let-defined symbol reduces by itself, we need to
-- do the context consistency check at each introduction.
(tel, (vt, te, Kinded ki ee)) <- checkTele tel $ checkOrInfer dec e mt
te <- return $ teleToType tel te
ee <- return $ teleLam tel ee
vt <- whnf' te
return (vt, te, Kinded ki ee)
{-
checkTypedLet :: Name -> Type -> Dec -> Expr -> Expr -> TVal -> TypeCheck (Kinded Extr)
checkTypedLet x t1 dec e1 e2 v = do
Kinded kit t1e <- checkType t1
v_t1 <- whnf' t1
Kinded ki0 e1e <- applyDec dec $ checkExpr e1 v_t1
let ki1 = intersectKind ki0 (predKind kit)
checkLetBody x t1e v_t1 ki1 dec e1e e2 v
{-
v_e1 <- whnf' e1
new x (Domain v_t1 ki1 dec) $ \ vx -> do
addRewrite (Rewrite vx v_e1) [v] $ \ [v'] -> do
Kinded ki2 e2e <- checkExpr e2 v'
return $ Kinded ki2 $ LLet (TBind x (Domain t1e ki1 dec)) e1e e2e -- if e2e==Irr then Irr else LLet n t1e e1e e2e
-}
checkUntypedLet :: Name -> Dec -> Expr -> Expr -> TVal -> TypeCheck (Kinded Extr)
checkUntypedLet x dec e1 e2 v = do
(v_t1, Kinded ki1 e1e) <- applyDec dec $ inferExpr e1
v_e1 <- whnf' e1
t1e <- toExpr v_t1
checkLetBody x t1e v_t1 ki1 dec e1e e2 v
-}
checkLetBody :: Name -> EType -> TVal -> Kind -> Dec -> Extr -> Expr -> TVal -> TypeCheck (Kinded Extr)
checkLetBody x t1e v_t1 ki1 dec e1e e2 v = do
v_e1 <- whnf' e1e
new x (Domain v_t1 ki1 dec) $ \ vx -> do
addRewrite (Rewrite vx v_e1) [v] $ \ [v'] -> do
Kinded ki2 e2e <- checkExpr e2 v'
return $ Kinded ki2 $ LLet (TBind x (Domain (Just t1e) ki1 dec)) emptyTel e1e e2e
{-
-- Dependent let: not checkable in rho;Delta style
-- v_e1 <- whnf rho e1
-- checkExpr (update rho n v_e1) (v_t1 : delta) e2 v
-}
-- | @checkPair e1 e2 y dom env b@ checks @Pair e1 e2@ against
-- @VQuant Sigma y dom env b@.
checkPair :: Expr -> Expr -> Name -> Domain -> FVal -> TypeCheck (Kinded Expr)
checkPair e1 e2 y dom@(Domain av ki dec) fv = do
case av of
VBelow Lt VInfty -> do
lowerSemi <- underAbs y dom fv $ \ i _ bv -> lowerSemiCont i bv
continue $ if lowerSemi then VBelow Le VInfty else av
_ -> continue av
where
continue av = do
Kinded k1 e1 <- applyDec dec $ checkExpr e1 av
v1 <- whnf' e1
bv <- app fv v1
Kinded k2 e2 <- checkExpr e2 bv
return $ Kinded (unionKind k1 k2) $ Pair (maybeErase dec e1) e2
-- check expression after forcing the type
checkForced :: Expr -> TVal -> TypeCheck (Kinded Expr)
checkForced e v = do
ren <- asks renaming
v <- force v
-- enter ("checkForced " ++ show ren ++ " |- " ++ show e ++ " : " ++ show v) $ do
enterDoc (text ("checkForced " ++ show ren ++ " |-") <+> prettyTCM e <+> colon <+> prettyTCM v) $ do
case (e,v) of
{-
(_, VGuard (Bound (Measure [VGen i]) (Measure [VGen j])) bv) ->
addSizeRel i j $ checkForced e bv
-}
(_, VGuard beta bv) ->
addBoundHyp beta $ checkForced e bv
(Pair e1 e2, VQuant Sigma y dom@(Domain av ki dec) fv) ->
checkPair e1 e2 y dom fv
(Record ri rs, t@(VApp (VDef (DefId DatK d)) vl)) -> do
let fail1 = failDoc (text "expected" <+> prettyTCM t <+> text "to be a record type")
-- DataSig { numPars, isTuple } <- lookupSymb d
-- unless isTuple $ fail1
mfs <- getFieldsAtType d vl
case mfs of
Nothing -> fail1
Just ptv -> do
let checkField :: (Name, Expr) -> TypeCheck (Kinded [(Name,Expr)]) -> TypeCheck (Kinded [(Name,Expr)])
checkField (p,e) cont =
case lookup p ptv of
Nothing -> failDoc (prettyTCM p <+> text "is not a field of record" <+> prettyTCM t)
Just tv -> do
tv <- piApp tv VIrr -- remove record argument (cannot be dependent!)
Kinded k e <- checkExpr e tv
Kinded k' es <- cont
return $ Kinded (unionKind k k') ((p,e) : es)
Kinded k rs <- foldr checkField (return $ Kinded NoKind []) rs
return $ Kinded k $ Record ri rs
{- OLD:
Following Awodey/Bauer 2001, the following rule is valid
Gamma, x:A |- t : B Gamma, x:A, y:A |- t = t[y/x] : B
--------------------------------------------------------
Gamma |- \xt : Pi x:[A]. B
(Lam _ y e1, VPi dec x va env t1) -> do
rho <- getEnv -- get the environment corresponding to Gamma
new y (Domain va (resurrectDec dec)) $ \ vy -> do
v_t1 <- whnf (update env x vy) t1
-- traceCheckM $ "checking " ++ show e1 ++ " : " ++ show v_t1
e1e <- checkExpr e1 v_t1
when (erased dec) $ do -- now check invariance of the e1
new y (Domain va (resurrectDec dec)) $ \ vy' -> do
ve <- whnf (update rho y vy) e1e
ve' <- whnf (update rho y vy') e1e
eqVal v_t1 ve ve' -- BUT: ve' does not have type v_t1 !?
-- prune the lambda if body has been pruned
return $ if e1e==Irr then Irr else Lam y e1e
-}
-- NOW just my rule (LICS 2010 draft) a la Barras/Bernardo
(Lam _ y e1, VQuant Pi x dom fv) -> do
-- rho <- getEnv -- get the environment corresponding to Gamma
underAbs y dom fv $ \ _ vy bv -> do
-- traceCheckM $ "checking " ++ show e1 ++ " : " ++ show v_t1
Kinded ki1 e1e <- checkExpr e1 bv
-- the kind of a lambda is the kind of its body
return $ Kinded ki1 $ Lam (decor dom) y e1e
-- lone projection: eta-expand!
(Proj Pre p, VQuant Pi x dom fv) -> do
let y = nonEmptyName x "y"
checkForced (Lam (decor dom) y $ App e (Var y)) v
{-
-- should be subsumed by checkBelow:
(e, v) | isVSize v -> Kinded kSize <$> checkSize e
-}
{- MOVED to checkSize
-- metavariables must have type size
(Meta i, _) | isVSize v -> do
addMeta ren i
return $ Kinded kSize $ Meta i
(Infty, v) | isVSize v -> return $ Kinded kSize $ Infty
(Zero, v) | isVSize v -> return $ Kinded kSize $ Zero
(Plus es, v) | isVSize v -> do
ese <- mapM checkSize es
return $ Kinded kSize $ Plus ese
(Max es, v) | isVSize v -> do
ese <- mapM checkSize es
return $ Kinded kSize $ Max ese
(Succ e2, v) | isVSize v -> do
e2e <- checkSize e2
return $ Kinded kSize $ Succ e2e
-}
(e, VBelow ltle v) -> Kinded kSize <$> checkBelow e ltle v
{-
-- prune sizes
return $ if e2e==Irr then Irr else Succ e2e
-}
(e,v) -> do
case spineView e of
-- unfold defined patterns
(h@(Def (DefId (ConK DefPat) c)), es) -> do
PatSig xs pat _ <- lookupSymbQ c
let (xs1, xs2) = splitAt (length es) xs
phi x = maybe (Var x) id $ lookup x (zip xs1 es)
body = parSubst phi (patternToExpr pat)
e = foldr (Lam defaultDec) body xs2
checkForced e v
-- check constructor term
(h@(Def (DefId (ConK co) c)), es) -> checkConTerm co c es v
{-
(h@(Def (DefId (ConK co) c)), es) -> do
tv <- conType c v
(knes, dv) <- checkSpine es tv
let e = foldl App h $ map (snd . valueOf) knes
checkSubtype e dv v
e <- etaExpandPis e dv -- a bit similiar to checkSubtype, which computes a singleton
return $ Kinded kTerm $ e
-}
-- else infer
_ -> do
(v2,kee) <- inferExpr e
checkSubtype (valueOf kee) v2 v
return kee
-- | Check (partially applied) constructor term, eta-expand it and turn it
-- into a named record.
checkConTerm :: ConK -> QName -> [Expr] -> TVal -> TypeCheck (Kinded Extr)
checkConTerm co c es v = do
case v of
VQuant Pi x dom fv -> do
let y = freshen $ nonEmptyName x "y"
underAbs y dom fv $ \ _ _ bv -> do
Kinded ki ee <- checkConTerm co c (es ++ [Var y]) bv
return $ Kinded ki $ Lam (decor dom) y ee
_ -> do
c <- disambigCon c v
tv <- conType c v
(knes, dv) <- checkSpine es tv
let ee = Record (NamedRec co c False notDotted) $ map valueOf knes
checkSubtype ee dv v
return $ Kinded kTerm ee
{-
-- | Check (partially applied) constructor term, eta-expand it and turn it
-- into a named record.
checkConTerm :: ConK -> Name -> [Expr] -> TVal -> TypeCheck (Kinded Extr)
checkConTerm co c es v = do
tv <- conType c v
(knes, dv) <- checkSpine es tv
let e0 = foldl App (Def (DefId (ConK co) c)) $ map (snd . valueOf) knes
checkSubtype e0 dv v
(vTel, _) <- telView dv
let xs = map (boundName . snd) vTel
decs = map (decor . boundDom . snd) vTel
ys = map freshen xs
rs = map valueOf knes ++ (zip xs $ map Var ys)
e1 = Record (NamedRec co c False) rs
e = foldr (uncurry Lam) e1 (zip decs ys)
return $ Kinded kTerm e
-}
{-
-- | Only eta-expand at function types, do not force.
etaExpandPis :: Expr -> TVal -> TypeCheck Expr
etaExpandPis e tv = do
case tv of
VQuant Pi x dom env b -> new x dom $ \ xv -> do
let y = freshen x
Lam (decor dom) y <$> do
etaExpandPis (App e (Var y)) =<< whnf (update env x xv) b
_ -> return e
-}
checkSpine :: [Expr] -> TVal -> TypeCheck ([Kinded (Name, Extr)], TVal)
checkSpine [] tv = return ([], tv)
checkSpine (e : es) tv = do
(kne, tv) <- checkApp e tv
(knes, tv) <- checkSpine es tv
return (kne : knes, tv)
maybeErase dec = if erased dec then erasedExpr else id
-- | checking e against (x : A) -> B returns (x,e) and B[e/x]
checkApp :: Expr -> TVal -> TypeCheck (Kinded (Name, Extr), TVal)
checkApp e2 v = do
v <- force v -- if v is a corecursively defined type in Set, unfold!
enter ("checkApp " ++ show v ++ " eliminated by " ++ show e2) $ do
case v of
VQuant Pi x dom@(Domain av@(VBelow Lt VInfty) _ dec) fv -> do
upperSemi <- underAbs x dom fv $ \ i _ bv -> upperSemiCont i bv
continue $ if upperSemi then VQuant Pi x dom{ typ = VBelow Le VInfty} fv
else v
_ -> continue v
where
continue v = case v of
VQuant Pi x (Domain av _ dec) fv -> do
(ki, v2, e2e) <- do
if inferable e2 then do
-- if e2 has a singleton type, we should not take v2 = whnf e2
-- but use the single value of e2
-- this is against the spirit of bidir. checking
-- if checking a type we need to resurrect
(av', Kinded ki e2e) <- applyDec dec $ inferExpr e2
case av' of
VSing v2 av'' -> do subtype av' av
return (ki, v2, e2e)
_ -> do checkSubtype e2e av' av
v2 <- whnf' e2e
return (ki, v2, e2e)
else do
Kinded ki e2e <- applyDec dec $ checkExpr e2 av
v2 <- whnf' e2e
return (ki, v2, e2e)
bv <- app fv v2
-- the kind of the application is the kind of its head
return (Kinded ki $ (x,) $ maybeErase dec e2e, bv)
-- if e1e==Irr then Irr else if e2e==Irr then e1e else App e1e [e2e])
_ -> throwErrorMsg $ "checking application to " ++ show e2 ++ ": expected function type, found " ++ show v
-- checkSubtype expr : infered_type <= ascribed_type
checkSubtype :: Expr -> TVal -> TVal -> TypeCheck ()
checkSubtype e v2 v = do
rho <- getEnv
traceSingM $ "computing singleton <" ++ show e ++ " : " ++ show v2 ++ ">" -- ++ " in environment " ++ show rho
v2principal <- sing rho e v2
traceSingM $ "subtype checking " ++ show v2principal ++ " ?<= " ++ show v ++ " in environment " ++ show rho
subtype v2principal v
-- ptsRule s1 s2 = s if (s1,s2,s) is a valid rule
-- precondition: s1,s2 are proper sorts, i.e., not Size or Tm
ptsRule :: Bool -> Sort Val -> Sort Val -> TypeCheck (Sort Val)
ptsRule er s1 s2 = do
cxt <- ask
let parametric = checkingConType cxt -- are we dealing with a parametric pi?
let err = "ptsRule " ++ show (s1,s2) ++ " " ++ (if parametric then "(in type of constructor)" else "") ++ ": "
case (s1,s2) of
(Set VInfty,_) -> fail $ err ++ "domain too big"
(Set v1, Set v2) ->
if parametric then do
unless er $ leqSize Pos v1 v2 -- when we are checking a constructor, to reject
{- data Bad : Set { bad : Set -> Bad } -}
return s2
else return $ Set $ maxSize [v1,v2]
(CoSet v1, Set VZero)
| parametric -> return $ CoSet v1
| v1 == VInfty -> return $ Set VZero
| otherwise -> fail $ err ++ "domain cannot be sized"
(CoSet v1, CoSet v2)
| parametric -> do
let v2' = maybe v2 id $ predSize v2
case minSize v1 v2 of
Just v -> return $ CoSet v
Nothing -> fail $ err ++ "min" ++ show (v1,v2) ++ " does not exist"
| v1 == VInfty -> return $ CoSet $ succSize v2
| otherwise -> fail $ err ++ "domain cannot be sized"
_ -> return s2
checkOrInfer :: Dec -> Expr -> Maybe Type -> TypeCheck (TVal, EType, Kinded Extr)
checkOrInfer dec e Nothing = do
(tv, ke) <- applyDec dec $ inferExpr e
te <- toExpr tv
return (tv, te, ke)
checkOrInfer dec e (Just t) = do
Kinded kt te <- checkType t
tv <- whnf' te
Kinded ke ee <- applyDec dec $ checkExpr e tv
let ki = intersectKind ke $ predKind kt
return $ (tv, te, Kinded ki ee)
-- inferType t = (s, te)
inferType :: Expr -> TypeCheck (Sort Val, Kinded Extr)
inferType t = do
(sv, te) <- inferExpr t
case sv of
VSort s | not (s `elem` map SortC [Tm,Size]) -> return (s,te)
_ -> fail $ "inferExpr: expected " ++ show t ++ " to be a type!"
-- inferExpr e = (tv, s, ee)
-- input : expr e | inferable e
-- output: type tv, kind s, and erased form ee of e
-- the kind tells whether e is a term, a size, a set, ...
inferExpr :: Expr -> TypeCheck (TVal, Kinded Extr)
inferExpr e = do
(tv, ee) <- inferExpr' e
case tv of
VGuard beta vb -> do
checkGuard beta
return (vb, ee)
_ -> return (tv, ee)
inferProj :: Expr -> PrePost -> Name -> TypeCheck (TVal, Kinded Extr)
inferProj e1 fx p = checkingCon False $ do
(v, Kinded ki1 e1e) <- inferExpr e1
{-
let fail1 = failDoc (text "expected" <+> prettyTCM e1 <+> text "to be of record type when taking the projection" <+> text p <> comma <+> text "but found type" <+> prettyTCM v)
let fail2 = failDoc (text "record" <+> prettyTCM e1 <+> text "of type" <+> prettyTCM v <+> text "does not have field" <+> text p)
-}
v <- force v -- if v is a corecursively defined type in Set, unfold!
tv <- projectType v p =<< whnf' e1e
return (tv, Kinded ki1 (proj e1e fx p))
{-
case v of
VApp (VDef (DefId Dat d)) vl -> do
mfs <- getFieldsAtType d vl
case mfs of
Nothing -> fail1
Just ptvs ->
case lookup p ptvs of
Nothing -> fail2
Just tv -> do
tv <- piApp tv VIrr -- cut of record arg
return (tv, Kinded ki1 (App e1e (Proj p)))
_ -> fail1
-}
-- inferExpr' might return a VGuard, this is removed in inferExpr
-- the returned kind for constructor type is computed as the union
-- of the kinds of the non-erased arguments
-- otherwise it is the kind of the target
inferExpr' :: Expr -> TypeCheck (TVal, Kinded Extr)
inferExpr' e = enter ("inferExpr' " ++ show e) $
let returnSing (Kinded ki ee) tv = do
tv' <- sing' ee tv
return (tv', Kinded ki ee)
in
(case e of
Var x -> do
traceCheckM ("infer variable " ++ show x)
item <- lookupName1 x
traceCheckM ("infer variable: retrieved item ")
let dom = domain item
av = typ dom
traceCheckM ("infer variable: " ++ show av)
enterDoc (text "inferExpr: variable" <+> prettyTCM x <+> colon <+> prettyTCM av <+> text "may not occur") $ do
let dec = decor dom
udec = upperDec item
pol = polarity dec
upol = polarity udec
when (erased dec && not (erased udec)) $
recoverFail ", because it is marked as erased"
enter ", because of polarity" $
leqPolM pol upol
traceCheckM ("infer variable returns")
traceCheckM ("infer variable " ++ show x ++ " : " ++ show av)
return $ (av, Kinded (kind dom) $ Var x)
{-
let err = "inferExpr: variable " ++ x ++ " : " ++ show (typ item) ++
" may not occur"
let dec = decor item
let pol = polarity dec
if erased dec then
fail $ err ++ ", because it is marked as erased"
else if not (leqPol pol SPos) then
fail $ err ++ ", because it has polarity " ++ show pol
else do
-- traceCheckM ("infer variable " ++ x ++ " : " ++ show (typ item))
return $ (typ item, Var x) -- TODO: (typ item, kind item, Var x)
-}
-- for constants, the kind coincides with the type!
Sort (CoSet e) -> do
ee <- checkSize e
return (VSort (Set (VSucc VZero)), Kinded (kUniv Zero) $ Sort $ CoSet ee)
Sort (Set e) -> do
(v, ee) <- checkLevel e
return (VSort (Set (succSize v)), Kinded (kUniv ee) $ Sort $ Set ee)
Sort (SortC Size) -> return (vTSize, Kinded kTSize $ e)
Zero -> return (vSize, Kinded kSize Zero)
Infty -> return (vSize, Kinded kSize Infty)
Below ltle e -> do
ee <- checkSize e
return (vTSize, Kinded kTSize $ Below ltle ee)
Quant pisig (TBind n (Domain t1 _ dec)) t2 -> do
-- make sure that in a constructor declaration the constructor args are
-- mixed-variant (there is no subtyping between constrs anyway)
checkCon <- asks checkingConType
{- TODO
when (checkCon && polarity dec /= Mixed) $
fail $ "constructor arguments must be declared mixed-variant"
-}
(s1, Kinded ki0 t1e) <- (if pisig==Pi then checkingDom else id) $
checkingCon False $ inferType t1 -- switch off parametric Pi
-- the kind of the bound variable is the precedessor of the kind of its type
let ki1 = predKind ki0
addBind (TBind n (Domain t1e ki1 $ defaultDec)) $ do -- ignore erasure flag AND polarity in Pi! (except for irrelevant, only becomes parametric)
-- TODO:
-- addBind (TBind n (Domain t1e ki1 $ coDomainDec dec)) $ do -- ignore erasure flag AND polarity in Pi! (except for irrelevant, only becomes parametric)
(s2, Kinded ki2 t2e) <- inferType t2
ce <- ask
let er = erased dec
s <- if impredicative ce && er && s2 == Set VZero then return s2 else ptsRule er s1 s2 -- Impredicativity!
-- improve erasure annotation: irrelevant arguments can be erased!
let (ki',dec') = if checkCon then
-- in case of constructor types the kind is the union
-- of the kinds of the constructor arguments
if ki0 == kTSize then (ki2, irrelevantDec)
else if erased dec then (ki2, dec) -- do not count erased args in
else (unionKind ki0 ki2, dec)
else (ki2, if argKind ki0 `irrelevantFor` (predKind ki2)
then irrelevantDec
else dec)
-- the kind of the Pi-type is the kind of its target (codomain)
return (VSort s, Kinded ki' $ Quant pisig (TBind n (Domain t1e ki1 dec')) t2e)
Quant Pi (TMeasure (Measure mu)) t2 -> do
mue <- mapM checkSize mu
(s, Kinded ki2 t2e) <- inferType t2
return (VSort s, Kinded ki2 $ Quant Pi (TMeasure (Measure mue)) t2e)
Quant Pi (TBound (Bound ltle (Measure mu) (Measure mu'))) t2 -> do
(mue,mue') <- checkingDom $ do
mue <- checkingDom $ mapM checkSize mu
mue' <- mapM checkSize mu'
return (mue,mue')
(s, Kinded ki2 t2e) <- inferType t2
return (VSort s, Kinded ki2 $ Quant Pi (TBound (Bound ltle (Measure mue) (Measure mue'))) t2e)
Sing e1 t -> do
(s, Kinded ki te) <- inferType t
tv <- whnf' te
Kinded ki1 e1e <- checkExpr e1 tv
return (VSort $ s, Kinded (intersectKind ki $ succKind ki1) -- not sure how useful the intersection is, maybe just ki is good enough
$ Sing e1e te)
{- Not safe to infer pairs because of irrelevance!
Pair e1 e2 -> do
(tv1, Kinded k1 e1) <- inferExpr e1
(tv2, Kinded k2 e2) <- inferExpr e2
let ki = unionKind k1 k2
tv = prod tv1 tv2
return (tv, Kinded ki $ Pair e1 e2)
-}
App (Proj Pre p) e -> inferProj e Pre p
App e (Proj Post p) -> inferProj e Post p
App e1 e2 -> checkingCon False $ do
(v, Kinded ki1 e1e) <- inferExpr e1
(Kinded ki2 (_, e2e), bv) <- checkApp e2 v
-- the kind of the application is the kind of its head
return (bv, Kinded ki1 $ App e1e e2e)
{-
v <- force v -- if v is a corecursively defined type in Set, unfold!
case v of
VQuant Pi x (Domain av _ dec) env b -> do
(v2,e2e) <-
if inferable e2 then do
-- if e2 has a singleton type, we should not take v2 = whnf e2
-- but use the single value of e2
-- this is against the spirit of bidir. checking
-- if checking a type we need to resurrect
(av', Kinded _ e2e) <- applyDec dec $ inferExpr e2
case av' of
VSing v2 av'' -> do subtype av' av
return (v2,e2e)
_ -> do checkSubtype e2e av' av
v2 <- whnf' e2e
return (v2, e2e)
else do
Kinded _ e2e <- applyDec dec $ checkExpr e2 av
v2 <- whnf' e2
return (v2, e2e)
bv <- whnf (update env x v2) b
-- the kind of the application is the kind of its head
return (bv, Kinded ki1 $ App e1e (if erased dec then erasedExpr e2e else e2e))
-- if e1e==Irr then Irr else if e2e==Irr then e1e else App e1e [e2e])
_ -> throwErrorMsg $ "inferExpr : expected Pi with expression : " ++ show e1 ++ "," ++ show v
-}
-- App e1 (e2:el) -> inferExpr $ (e1 `App` [e2]) `App` el
-- 2012-01-22 no longer infer constructors
(Def id@(DefId {idKind, idName = name})) | not (conKind idKind) -> do -- traceCheckM ("infer defined head " ++ show n)
mitem <- errorToMaybe $ lookupName1 $ unqual name
case mitem of -- first check if it is also a var name
Just item -> do -- we are inside a mutual declaration (not erased!)
let pol = (polarity $ decor $ domain item)
let upol = (polarity $ upperDec item)
mId <- asks checkingMutualName
case mId of
Just srcId ->
-- we are checking constructors or function bodies
addPosEdge srcId id upol
Nothing ->
-- we are checking signatures
enter ("recursive occurrence of " ++ show name ++ " not strictly positive") $
leqPolM pol upol
return (typ $ domain item, Kinded (kind $ domain item) $ e)
Nothing -> -- otherwise, it is not the data type name just being defined
do sige <- lookupSymbQ name
case sige of
-- data types have always kind Set 0!
(DataSig { symbTyp = tv }) -> return (tv, Kinded (symbolKind sige) e)
(FunSig { symbTyp = tv }) -> return (tv, Kinded (symbolKind sige) e)
-- constructors are always terms
(ConSig { symbTyp = tv }) -> returnSing (Kinded kTerm e) tv -- constructors have sing.type!
(LetSig { symbTyp = tv }) -> return (tv, Kinded (symbolKind sige) e) -- return $ vSing v tv
{-
(Con _ n) -> do sig <- gets signature
case (lookupSig n sig) of
(Let n) -> do sig <- gets signature
case (lookupSig n sig) of
-}
_ -> throwErrorMsg $ "cannot infer type of " ++ show e
) >>= \ tv -> ask >>= \ ce ->
traceCheck ("inferExpr: " ++ show (renaming ce) ++ ";" ++ show (context ce) ++ " |- " ++ show e ++ " :=> " ++ show tv ++ " in env" ++ show (environ ce)) $
-- traceCheck ("inferExpr: " ++ show e ++ " :=> " ++ show tv) $
return tv
{- BAD IDEA!
improveDec :: Dec -> TVal -> Dec
improveDec dec v = if v == VSet || v == VSize then erased else dec
-}
{-
-- entry point 3: resurrects
checkType :: Expr -> TypeCheck Extr
checkType e = (resurrect $ checkType' e) `throwTrace` ("not a type: " ++ show e )
checkType' :: Expr -> TypeCheck Extr
checkType' e = case e of
Sort s -> return e
Pi dec x t1 t2 -> do
t1e <- checkType' t1
-- ignore erasure flag in types!
-- t1v <- whnf' t1e
-- new' x (Domain (Dec False) t1v) $ do
addBind x (Dec False) t1e $ do
t2e <- checkType' t2
return $ Pi dec x t1e t2e -- Pi (improveDec dec t1v) x t1e t2e
_ -> checkExpr' e $ VSort Set
-}
checkType :: Expr -> TypeCheck (Kinded Extr)
checkType t =
enter ("not a type: " ++ show t) $
resurrect $ do
(s, te) <- inferType t
leqSort Pos s (Set VInfty)
return te
checkSmallType :: Expr -> TypeCheck (Kinded Extr)
checkSmallType t =
enter ("not a set: " ++ show t) $
resurrect $ do
(s, te) <- inferType t
case s of
Set VZero -> return te
CoSet{} -> return te
_ -> fail $ "expected " ++ show s ++ " to be Set or CoSet _"
{-
-- small type
checkSmallType :: Expr -> TypeCheck Extr
checkSmallType e = (resurrect $ checkExpr' e $ VSort Set) `throwTrace` ("not a set: " ++ show e )
-}
-- check telescope and add bindings to contexts
checkTele :: Telescope -> TypeCheck a -> TypeCheck (ETelescope, a)
checkTele (Telescope tel) k = loop tel where
loop tel = case tel of
[] -> (emptyTel,) <$> k
tb@(TBind x (Domain t _ dec)) : tel -> do
Kinded ki te <- checkType t
let tb = TBind x (Domain te (predKind ki) dec)
(tel, a) <- addBind tb $ loop tel
return (Telescope $ tb : telescope tel, a)
-- the integer argument is the number of the clause, used just for user feedback
checkCases :: Val -> TVal -> [Clause] -> TypeCheck (Kinded [EClause])
checkCases = checkCases' 1
checkCases' :: Int -> Val -> TVal -> [Clause] -> TypeCheck (Kinded [EClause])
checkCases' i v tv [] = return $ Kinded NoKind []
checkCases' i v tv (c : cl) = do
Kinded k1 ce <- checkCase i v tv c
Kinded k2 cle <- checkCases' (i + 1) v tv cl
return $ Kinded (unionKind k1 k2) $ ce : cle
checkCase :: Int -> Val -> TVal -> Clause -> TypeCheck (Kinded EClause)
checkCase i v tv cl@(Clause _ [p] mrhs) = enter ("case " ++ show i) $
-- traceCheck ("checking case " ++ show i) $
do
-- clearDots -- NOT NEEDED
(flex,ins,cxt,vt,pe,pv,absp) <- checkPattern neutral [] emptySub tv p
local (\ _ -> cxt) $ do
mapM (checkGoal ins) flex
tel <- getContextTele -- TODO!
case (absp,mrhs) of
(True,Nothing) -> return $ Kinded NoKind (Clause tel [pe] Nothing)
(False,Nothing) -> fail ("missing right hand side in case " ++ showCase cl)
(True,Just rhs) -> fail ("absurd pattern requires no right hand side in case " ++ showCase cl)
(False,Just rhs) -> do
-- pv <- whnf' (patternToExpr p) -- DIFFICULT FOR DOT PATTERNS!
-- vp <- patternToVal p -- BUG: INTRODUCES FRESH GENS, BUT THEY HAVE ALREADY BEEN INTRODUCED IN checkPattern
addRewrite (Rewrite v pv) [vt] $ \ [vt'] -> do
Kinded ki rhse <- checkRHS ins rhs vt'
return $ Kinded ki (Clause tel [pe] (Just rhse))
-- [rhs'] <- solveAndModify [rhs] (environ cxt)
-- return (Clause [p] rhs')
-- type check a function
checkFun :: Type -> [Clause] -> TypeCheck (Kinded [EClause])
checkFun t cl = do
tv <- whnf' t
checkClauses tv cl
-- the integer argument is the number of the clause, used just for user feedback
checkClauses :: TVal -> [Clause] -> TypeCheck (Kinded [EClause])
checkClauses = checkClauses' 1
checkClauses' :: Int -> TVal -> [Clause] -> TypeCheck (Kinded [EClause])
checkClauses' i tv [] = return $ Kinded NoKind ([])
checkClauses' i tv (c:cl) = do
Kinded ki1 ce <- checkClause i tv c
Kinded ki2 cle <- checkClauses' (i + 1) tv cl
return $ Kinded (unionKind ki1 ki2) $ (ce : cle)
-- checkClause i tv cl = (cl', cle)
-- checking one equation cl of a function at type tv
-- solve size constraints
-- substitute solution into clause, resulting in cl'
-- return also extracted clause cle
checkClause :: Int -> TVal -> Clause -> TypeCheck (Kinded EClause)
checkClause i tv cl@(Clause _ pl mrhs) = enter ("clause " ++ show i) $ do
-- traceCheck ("checking function clause " ++ show i) $
-- clearDots -- NOT NEEDED
(flex,ins,cxt,tv0,ple,plv,absp) <- checkPatterns neutral [] emptySub tv pl
-- 2013-03-30 When checking the rhs, we only allow new size hypotheses
-- if they do not break any valuation of the existing hypotheses.
-- See ICFP 2013 paper.
-- We exclude cofuns here, for experimentation.
-- Note that cofuns need not be SN, so the strict consistency may be
-- not necessary.
local (\ _ -> cxt { consistencyCheck = (mutualCo cxt == Ind) }) $ do
mapM (checkGoal ins) flex
{-
dots <- openDots
unless (null dots) $
recoverFailDoc $ text "the following dotted constructors could not be confirmed: " <+> prettyTCM dots
-}
-- TODO: insert meta var solution in dot patterns
tel <- getContextTele -- WRONG TELE, has VGens for DotPs
case (absp,mrhs) of
(True,Nothing) -> return $ Kinded NoKind (Clause tel ple Nothing)
(False,Nothing) -> fail ("missing right hand side in clause " ++ show cl)
(True,Just rhs) -> fail ("absurd pattern requires no right hand side in clause " ++ show cl)
(False,Just rhs) -> do
Kinded ki rhse <- checkRHS ins rhs tv0
env <- getEnv
[rhse] <- solveAndModify [rhse] env
return $ Kinded ki (Clause tel ple (Just rhse))
-- * Pattern checking ------------------------------------------------
type Substitution = Valuation -- [(Int,Val)]
emptySub = emptyVal
sgSub = sgVal
lookupSub i = lookup i . valuation
type DotFlex = (Int,(Expr,Domain))
-- left over goals
data Goal
= DotFlex Int (Maybe Expr) Domain
-- ^ @Just@ : Flexible variable from inaccessible pattern.
-- ^ @Nothing@ : Flexible variable from hidden function type.
| MaxMatches Int TVal
| DottedCons Dotted Pattern TVal
deriving Show
-- checkPatterns is initially called with an empty local context
-- in the type checking monad
checkPatterns :: Dec -> [Goal] -> Substitution -> TVal -> [Pattern] -> TypeCheck ([Goal],Substitution,TCContext,TVal,[EPattern],[Val],Bool)
checkPatterns dec0 flex ins v pl =
case v of
VMeasured mu vb -> setMeasure mu $ checkPatterns dec0 flex ins vb pl
VGuard beta vb -> addBoundHyp beta $ checkPatterns dec0 flex ins vb pl
{-
VGuard beta vb -> fail $ "checkPattern at type " ++ show v ++ " --- introduction of constraints not supported"
-}
_ -> case pl of
[] -> do cxt <- ask
return (flex,ins,cxt,v,[],[],False)
(p:pl') -> do (flex',ins',cxt',v',pe,pv,absp) <- checkPattern dec0 flex ins v p
local (\ _ -> cxt') $ do
(flex'',ins'',cxt'',v'',ple,plv,absps) <- checkPatterns dec0 flex' ins' v' pl'
return (flex'',ins'',cxt'',v'', pe:ple, pv:plv, absp || absps) -- if pe==IrrP then ple else pe:ple)
{-
checkPattern dec0 flex subst tv p = (flex', subst', cxt', tv', pe, pv, absp)
Input :
dec0 : context in which pattern occurs (irrelevant, parametric, recursive)
are we checking an erased argument? (constr. pat. needs to be forced!)
flex : list of pairs (flexible variable, its dot pattern + supposed type)
subst : list of pairs (flexible variable, its valuation)
cxt : in monad, containing
rho : binding of variables to values
delta : binding of generic values to their types
tv : type of the expression \ p -> t
p : the pattern to check
Output
tv' : type of t
pe : erased pattern
pv : value of pattern (this is in essence whnf' pe,
but we cannot evaluate because of dot patterns)
absp : did we encounter an absurd pattern
-}
checkPattern :: Dec -> [Goal] -> Substitution -> TVal -> Pattern -> TypeCheck ([Goal],Substitution,TCContext,TVal,EPattern,Val,Bool)
checkPattern dec0 flex ins tv p = -- ask >>= \ TCContext { context = delta, environ = rho } -> trace ("checkPattern" ++ ("\n dot pats: " +?+ show flex) ++ ("\n substion: " +?+ show ins) ++ ("\n environ : " +?+ show rho) ++ ("\n context : " +?+ show delta) ++ "\n pattern : " ++ show p ++ "\n at type : " ++ show tv ++ "\t<>") $
enter ("pattern " ++ show p) $ do
tv <- force tv
case tv of
-- record type can be eliminated
VApp (VDef (DefId DatK d)) vl ->
case p of
ProjP proj -> do
tv <- projectType tv proj VIrr -- do not have record value here
cxt <- ask
return (flex, ins, cxt, tv, p, VProj Post proj, False)
{-
mfs <- getFieldsAtType d vl
case mfs of
Nothing -> failDoc (text "cannot eliminate type" <+> prettyTCM tv <+> text "with projection pattern" <+> prettyTCM p)
Just ptvs ->
case lookup proj ptvs of
Nothing -> failDoc (text "record type" <+> prettyTCM tv <+> text "does not know projection" <+> text proj)
Just tv -> do
tv <- piApp tv VIrr -- cut of record arg
cxt <- ask
return (flex, ins, cxt, tv, p, VProj proj, False)
-}
_ -> failDoc (text "cannot eliminate type" <+> prettyTCM tv <+> text "with a non-projection pattern")
-- intersection type
VQuant Pi x dom@(Domain av ki Hidden) fv -> do
-- introduce new flexible variable
newWithGen x dom $ \ i xv -> do
tv <- fv `app` xv
checkPattern dec0 (DotFlex i Nothing dom : flex) ins tv p
-- function type can be eliminated
VQuant Pi x (Domain av ki dec) fv -> do
{-
let erased' = er || erased dec
let decEr = if erased' then irrelevantDec else dec -- dec {erased = erased'}
-}
let decEr = dec `compose` dec0
let domEr = (Domain av ki decEr)
case p of
-- treat successor pattern here, because of admissibility check
SuccP p2 -> do
when (av /= vSize) $ throwErrorMsg "checkPattern: expected type Size"
when (isSuccessorPattern p2) $ cannotMatchDeep p tv
co <- asks mutualCo
when (co /= CoInd) $
fail ("successor pattern only allowed in cofun")
enterDoc (text ("checkPattern " ++ show p ++" : matching on size, checking that target") <+> prettyTCM tv <+> text "ends in correct coinductive sized type") $
underAbs x domEr fv $ \ i _ bv -> endsInSizedCo i bv
cxt <- ask
-- 2012-02-05 assume size variable in SuccP to be < #
let sucTy = (vFinSize `arrow` vFinSize)
(flex',ins',cxt',tv',p2e,p2v,absp) <- checkPattern decEr flex ins sucTy p2
-- leqVal Mixed delta' VSet VSize av -- av = VSize
let pe = SuccP p2e
let pv = VSucc p2v
-- pv0 <- local (\ _ -> cxt') $ whnf' $ patternToExpr pe
-- pv0 <- patternToVal p -- RETIRE patternToVal
-- pv <- up False pv0 av -- STUPID what can be eta-exanded at type Size??
vb <- app fv pv
{-
endsInCoind <- endsInSizedCo pv vb
when (not endsInCoind) $ throwErrorMsg $ "checkPattern " ++ show p ++" : cannot match on size since target " ++ show tv ++ " does not end in correct coinductive sized type"
-}
return (flex',ins',cxt',vb,pe,pv,absp)
-- other patterns: no need to know about result type
_ -> do
(flex',ins',cxt',pe,pv,absp) <- checkPattern' flex ins domEr p
-- traceM ("checkPattern' returns " ++ show (flex',ins',cxt',pe,pv,absp))
vb <- app fv pv
vb <- substitute ins' vb -- from ConP case -- ?? why not first subst and then whnf?
-- traceCheckM ("Returning type " ++ show vb)
return (flex',ins',cxt',vb,pe,pv,absp)
_ -> throwErrorMsg $ "checkPattern: expected function type, found " ++ show tv
-- TODO: refactor with monad transformers
-- put absp into writer monad
turnIntoVarPatAtUnitType :: TVal -> Pattern -> TypeCheck Pattern
turnIntoVarPatAtUnitType (VApp (VDef (DefId DatK n)) _) p@(ConP pi c []) =
flip (ifM $ isUnitData n) (return p) $ do
let x = fresh "un!t"
return $ VarP x
turnIntoVarPatAtUnitType _ p = return p
checkPattern' :: [Goal] -> Substitution -> Domain -> Pattern -> TypeCheck ([Goal],Substitution,TCContext,EPattern,Val,Bool)
checkPattern' flex ins domEr@(Domain av ki decEr) p = do
p <- turnIntoVarPatAtUnitType av p
case p of
SuccP{} -> failDoc (text "successor pattern" <+> prettyTCM p <+> text "not allowed here")
PairP p1 p2 -> do
av <- force av
case av of
VQuant Sigma y dom1@(Domain av1 ki1 dec1) fv -> do
(flex, ins, cxt, pe1, pv1, absp1) <-
checkPattern' flex ins (Domain av1 ki1 $ dec1 `compose` decEr) p1
av2 <- app fv pv1
(flex, ins, cxt, pe2, pv2, absp2) <-
local (const cxt) $
checkPattern' flex ins (Domain av2 ki decEr) p2
return (flex, ins, cxt, PairP pe1 pe2, VPair pv1 pv2, absp1 || absp2)
_ -> failDoc (text "pair pattern" <+> prettyTCM p <+> text "could not be checked against type" <+> prettyTCM av)
{-
(x : Sigma y:A. B) -> C
=iso= (y : A) -> (x' : B) -> C[(y,x')/x]
(x : Sigma y:V. <B;rho1>) -> <C;rho2>
=iso= (y : V) -> <(x': B) -> C; ?? x=(y,x')>
-}
{-
case av of
VQuant Sigma y dom1@(Domain av1 ki1 dec1) env1 a2 -> do
let x' = x ++ "#2"
ep = Pair (Var y) (Var x')
tv = VQuant Pi y dom1 env1 $
Quant x' (Domain a2
-}
ProjP proj -> failDoc (text "cannot eliminate type" <+> prettyTCM av <+> text "with projection pattern" <+> prettyTCM p)
VarP y -> do
new y domEr $ \ xv -> do
cxt' <- ask
p' <- case av of
VBelow Lt v -> flip SizeP y <$> toExpr v
_ -> return p
return (flex, ins, cxt', maybeErase $ p', xv, False)
{- checking bounded size patterns
ex : [i : Size] -> [j : Below< i] -> ...
ex i (j < i) = ...
type of pattern : Below< i needs to cover type of parameter Below< i
zero : [j : Size] -> Nat $j -- need to hold a "sized con type"
zero : [j < i] -> Nat i
ex : [i : Size] -> (n : Nat i) -> ...
ex i (zero (j < i) = ...
type of size-pat : Below< i
-}
SizeP e y -> do -- pattern (z > y), y is the bound variable, z the bound of z
e <- resurrect $ checkSize e -- (Var z)
newWithGen y domEr $ \ j xv -> do
{-
VGen k <- whnf' (Var z)
addSizeRel j 1 k $ do -- j < k
-}
ve <- whnf' e
addBoundHyp (Bound Lt (Measure [xv]) (Measure [ve])) $ do
subtype av (VBelow Lt ve)
cxt' <- ask
return (flex, ins, cxt', maybeErase $ SizeP e y, xv, False)
AbsurdP -> do
when (isFunType av) $ fail ("absurd pattern " ++ show p ++ " does not match function types, like " ++ show av)
cxt' <- ask
return (MaxMatches 0 av : flex, ins, cxt', maybeErase $ AbsurdP, VIrr, True)
{-
cenvs <- matchingConstructors av -- TODO: av might be MVar
-- need to be postponed
case cenvs of
[] -> do bv <- whnf (update env x VIrr) b
cxt' <- ask
return (flex, ins, cxt', bv, maybeErase $ AbsurdP, True)
_ -> throwErrorMsg $ "type " ++ show av ++ " of absurd pattern not empty"
-}
-- always expand defined patterns!
p@(ConP pi n ps) | coPat pi == DefPat -> do
checkPattern' flex ins domEr =<< expandDefPat p
-- ConP pi n pl | not $ dottedPat pi -> do
ConP pi n pl -> do
-- disambiguate constructor first
n <- disambigCon n av
let co = coPat pi
dotted = dottedPat pi
-- First check that we do not match against an irrelevant argument.
unless dotted $ nonDottedConstructorChecks n co pl
{- TODO
enter ("can only match non parametric arguments") $
leqPolM (polarity dec) (pprod defaultPol)
-}
(vc,(flex',ins',cxt',vc',ple,pvs,absp)) <- checkConstructorPattern co n pl
when (isFunType vc') $ fail ("higher-order matching of pattern " ++ show p ++ " of type " ++ show vc' ++ " not allowed")
let flexgen = concat $ map (\ g -> case g of
DotFlex i _ _ -> [i]
_ -> []) flex'
-- fst $ unzip flex'
-- av1 <- sing (environ cxt') (patternToExpr p) vc'
-- av2 <- sing (environ cxt') (patternToExpr p) av
-- subst <- local (\ _ -> cxt') $ inst flexgen VSet av1 av2
-- need to evaluate the erased pattern!
let pe = ConP pi n ple -- erased pattern
-- dot <- if dottedPat pi then newDotted p else return notDotted
dot <- if dottedPat pi then mkDotted True else return notDotted
pv0 <- mkConVal dot co n pvs vc
-- OLD: let pv0 = VDef (DefId (ConK co) n) `VApp` pvs
{-
let epe = patternToExpr pe
pv0 <- local (\ _ -> cxt') $ whnf' epe
-- pv0 <- patternToVal p -- THIS USE should be ok, since the new GENs are not in the global context yet, only in cxt' -- NO LONGER ok with erasure!
-- traceM $ "sucessfully computed value " ++ show pv0 ++ " of pattern " ++ show epe
-}
subst <- local (\ _ -> cxt') $ do
case av of -- TODO: need subtyping-unify instead of unify??
VSing vav av0 -> do
vav <- whnfClos vav
inst Pos flexgen av0 pv0 vav
_ -> unifyIndices flexgen vc' av -- vc' <= av ?!
-- THIS IMPLEMENTATION RELIES HEAVILY ON INJECTIVITY OF DATAS
{- moved to checkRHS
-- apply substitution to measures in environment
let mmu = (envBound . environ) cxt'
mmu' <- Traversable.mapM (substitute subst) mmu
-}
{-
ins'' <- compSubst ins' subst
vb <- substitute ins'' vb
delta' <- substitute ins'' delta'
-}
ins'' <- compSubst ins' subst -- 2010-07-27 not ok to switch!
delta'' <- substitute ins'' (context cxt')
traceCheckM $ "delta'' = " ++ show delta''
av <- substitute ins'' av -- 2010-09-22: update av
pv <- up False pv0 av
-- if the constructor was dotted, make sure it is the only match
let flex'' = fwhen dotted (DottedCons dot p av :) flex'
return (flex'', ins'', cxt' { context = delta'' },
maybeErase pe, pv, absp)
{- DO NOT UPDATE measure here, its done in checkRHS
return (flex', ins'', cxt' { context = delta'', environ = (environ cxt') { envBound = mmu' } }, vb',
maybeErase pe, absp)
-}
{- UNUSED
-- If we encounter a dotted constructor, we simply
-- compute the pattern variable context
-- and then treat the pattern as dot pattern.
p@(ConP pi n ps) | dottedPat pi -> do
(vc,(flex',ins',cxt',vc',ple,pvs,absp)) <-
checkConstructorPattern (coPat pi) n ps
local (const cxt') $
checkPattern' flex ins domEr $ DotP $ patternToExpr p
-}
DotP e -> do
-- create an informative, but irrelevant identifier for dot pattern
let xp = fresh $ "." ++ case e of Var z -> suggestion z; _ -> Util.parens $ show e
newWithGen xp domEr $ \ k xv -> do
cxt' <- ask
-- traceCheck ("Returning type " ++ show vb) $
return (DotFlex k (Just e) domEr : flex
,ins
,cxt'
,maybeErase $ DotP e -- $ Var xp -- DotP $ Meta k -- e -- Meta k
-- ,maybeErase $ -- AbsurdP -- VarP $ show e
,xv
,False) -- TODO: Erase in e/ Meta subst!
{- original code
do let (k, delta') = cxtPush dec av delta
vb <- whnf (update env x (VGen k)) b
return ((k,(e,Domain av dec)):flex
,ins
,rho
,delta'
,vb)
-}
where
maybeErase p = if erased decEr then ErasedP p else p
checkConstructorPattern co n pl = do
when (isFunType av) $ fail ("higher-order matching of pattern " ++ show p ++ " at type " ++ show av ++ " not allowed")
-- TODO: ensure that matchings against erased arguments are forced
-- when (erased dec) $ throwErrorMsg $ "checkPattern: cannot match on erased argument " ++ show p ++ " : " ++ show av
ConSig {conPars, lhsTyp = sz, recOccs, symbTyp = vc, dataName, dataPars} <- lookupSymbQ n
-- the following is a hack to still support old-style
-- add .($ i) (zero i) ...
-- fun defs: if (zero i) is matched against (Nat flexvar$i)
-- we use the old constructor type [i : Size] -> Nat $i
-- else, the new one [j < i] -> Nat i
let flexK k (DotFlex k' _ _) = k == k'
flexK k _ = False
-- use lhs con type only if sizeindex is not a rigid var
isFlex (VGen k) = List.any (flexK k) flex
isFlex _ = True
isSz = if co == Cons then sz else Nothing
vc <- instConLType n conPars vc isSz isFlex dataPars =<< force av
{-
vc <- case sz of
Nothing -> instConType n nPars vc =<< force av
Just vc -> instConType n (nPars+1) vc =<< force av
-}
-- (flex',ins',cxt',vc',ple,pvs,absp) <-
(vc,) <$> checkPatterns decEr flex ins vc pl
-- These checks are only relevant if a constructor is an actual match.
nonDottedConstructorChecks n co pl = do
ConSig {conPars, lhsTyp = sz, recOccs, symbTyp = vc, dataName, dataPars} <- lookupSymbQ n
-- check that size argument of coconstr is dotted
when (co == CoCons && isJust sz) $ do
let sizep = head pl -- 2012-01-22: WAS (pl !! nPars)
unless (isDotPattern sizep) $
fail $ "in pattern " ++ show p ++ ", coinductive size sub pattern " ++ show sizep ++ " must be dotted"
when (not $ decEr `elem` map Dec [Const,Rec]) $
recoverFail $ "cannot match pattern " ++ show p ++ " against non-computational argument"
-- check not to match non-trivially against erased stuff
when (decEr == Dec Const) $ do
let failNotForced = recoverFail $ "checkPattern: constructor " ++ show n ++ " of non-computational argument " ++ show p ++ " : " ++ show av ++ " not forced"
mcenvs <- matchingConstructors av
case mcenvs of
Nothing -> do -- now check whether dataName is a record type
DataSig { constructors } <- lookupSymb dataName
unless (length constructors == 1) $ failNotForced
return ()
Just [] -> recoverFail $ "checkPattern: no constructor matches type " ++ show av
Just [(ci, _)] | cName ci == n -> return ()
_ -> failNotForced
{- New treatment of size matching (see examples/Sized/Cody.ma)
sized data O : Size -> Set
{ Z : [i : Size] -> O ($ i)
; S : [i : Size] -> O i -> O ($ i)
; L : [i : Size] -> (Nat -> O i) -> O ($ i)
; M : [i : Size] -> O i -> O i -> O ($ i)
}
fun deep : [i : Size] -> O i -> Nat -> Nat
{ deep i4 (M i3 (L j2 f) (S i2 (S i1 (S i x)))) n
= deep _ (M _ (L _ (pre _ f)) (S _ (f n))) (succ (succ (succ n)))
; deep i x n = n
}
Explicit form: Size variables and their constraints are noted explicitely,
to be able to do untyped call extraction in the termination module.
deep i4
(M (i4 > i3)
(L (i3 > j2) f)
(S (i3 > i2)
(S (i2 > i1)
(S (i1 > i) x)))) n
= deep _ (M _ (L _ (pre _ f)) (S _ (f n))) (succ (succ (succ n)))
i4, i3, ... are all rigid variables with constraints between them.
There is a tree hierarchy, but I do not know whether I can exploit
this.
i4 > i3 > i2 > i1 > i
> j3
This could be stored in a union-find-like data structure, or just in
the constraint matrix.
How to pattern match?
id : [i : Size] -> List i -> List i
id i (cons (i > j) x xs) = cons j x (id j xs)
Only a size variable matches a size arguments
match (cons (i > j) x xs) against List i
get cons : [j : Size] -> Nat -> List j -> List ($ j)
yield x : Nat, xs : List j, cons j x xs : List ($ j)
check List ($ j) <= List i
-}
{- RETIRED
-- checkDot does not need to extract
checkDot :: Substitution -> DotFlex -> TypeCheck ()
checkDot subst (i,(e,it)) = enter ("dot pattern " ++ show e) $
case (lookup i subst) of
Nothing -> fail $ "not instantiated"
Just v -> do
tv <- substitute subst (typ it)
ask >>= \ ce -> traceCheckM ("checking dot pattern " ++ show ce ++ " |- " ++ show e ++ " : " ++ show (decor it) ++ " " ++ show tv)
applyDec (decor it) $ do
checkExpr e tv
v' <- whnf' e -- TODO: has subst erased terms?
enter ("inferred value " ++ show v ++ " does not match given dot pattern value " ++ show v') $
eqVal Pos tv v v'
-}
-- checkDot does not need to extract
-- 2012-01-25 now we do since "extraction" turns also con.terms into records
checkGoal :: Substitution -> Goal -> TypeCheck ()
checkGoal subst (DotFlex i me it) = enter ("dot pattern " ++ show me) $
case lookupSub i subst of
Nothing -> recoverFail $ "not instantiated"
Just v -> whenJust me $ \ e -> do
tv <- substitute subst (typ it)
ask >>= \ ce -> traceCheckM ("checking dot pattern " ++ show ce ++ " |- " ++ show e ++ " : " ++ show (decor it) ++ " " ++ show tv)
-- applyDec (decor it) $ do
resurrect $ do -- consider a DotP e always as irrelevant!
e <- valueOf <$> checkExpr e tv
v' <- whnf' e -- TODO: has subst erased terms?
enterDoc (text "inferred value" <+> prettyTCM v <+> text "does not match given dot pattern value" <+> prettyTCM v') $
leqVal Pos tv v v' -- WAS: eqVal
checkGoal subst (MaxMatches n av) = do
traceCheckM ("checkGoal _ $ MaxMatches " ++ show n ++ " $ " ++ show av)
av' <- substitute subst av
traceCheckM ("checkGoal _ $ MaxMatches " ++ show n ++ " $ " ++ show av')
-- av' <- reval av'
-- traceCheckM ("checkGoal: reevalutated " ++ show av')
mcenvs <- matchingConstructors av'
traceCheckM ("checkGoal matching constructors = " ++ show mcenvs)
maybe (recoverFail $ "not a data type: " ++ show av')
(\ cenvs ->
if length cenvs > n then recoverFail $
if n==0 then "absurd pattern does not match since type " ++ show av' ++ " is not empty"
else
"more than one constructor matches type " ++ show av'
else return ())
mcenvs
checkGoal subst (DottedCons dot p av)
| isDotted dot =
enterDoc (text "confirming dotted constructor" <+> prettyTCM p) $ do
checkGoal subst (MaxMatches 1 av)
| otherwise = return ()
checkRHS :: Substitution -> Expr -> TVal -> TypeCheck (Kinded Extr)
checkRHS ins rhs v = do
traceCheckM ("checking rhs " ++ show rhs ++ " : " ++ show v)
enter "right hand side" $ do
-- first update measure according to substitution for dot variables
cxt <- ask
let rho = environ cxt
mmu' <- Traversable.mapM (substitute ins) (envBound rho)
local (\ _ -> cxt { environ = rho { envBound = mmu' }}) $
activateFuns $
checkExpr rhs v
-- TODO type directed unification
-- unifyIndices flex tv1 tv2
-- tv1 = D pars inds is the type of the pattern
-- tv2 = D pars' inds' is the type matched against
-- Note that in this case we can unify without using the principle of
-- injective data type constructors,
-- we are only calling unifyIndices from the constructor pattern case
-- in Checkpattern
unifyIndices :: [Int] -> Val -> Val -> TypeCheck Substitution
unifyIndices flex v1 v2 = ask >>= \ cxt -> enterDoc (text ("unifyIndices " ++ show (context cxt) ++ " |-") <+> prettyTCM v1 <+> text ("?<=" ++ show Pos) <+> prettyTCM v2) $ do
-- {-
case (v1,v2) of
(VSing _ v1, VApp (VDef (DefId DatK d2)) vl2) ->
flip (unifyIndices flex) v2 =<< whnfClos v1
(VApp (VDef (DefId DatK d1)) vl1, VApp (VDef (DefId DatK d2)) vl2) | d1 == d2 -> do
(DataSig { numPars = np, symbTyp = tv, positivity = posl}) <- lookupSymbQ d1
instList posl flex tv vl1 vl2 -- unify also parameters to solve dot patterns
_ ->
-- -}
inst Pos flex vTopSort v1 v2
-- throwErrorMsg ("unifyIndices " ++ show v1 ++ " =?= " ++ show v2 ++ " failed, not applied to data types")
-- unify, but first produce whnf
instWh :: Pol -> [Int] -> TVal -> Val -> Val -> TypeCheck Substitution
instWh pos flex tv w1 w2 = do
v1 <- whnfClos w1
v2 <- whnfClos w2
inst pos flex tv v1 v2
-- | Check occurrence and return singleton substitution.
assignFlex :: Int -> Val -> TypeCheck Substitution
assignFlex k v = do
unlessM (nocc [k] v) $
failDoc $
text "variable " <+> prettyTCM (VGen k) <+>
text " may not occur in " <+> prettyTCM v
return $ sgSub k v
-- match v1 against v2 by unification , yielding a substition
inst :: Pol -> [Int] -> TVal -> Val -> Val -> TypeCheck Substitution
inst pos flex tv v1 v2 = ask >>= \ cxt -> enterDoc (text ("inst " ++ show (context cxt) ++ " |-") <+> prettyTCM v1 <+> text ("?<=" ++ show pos) <+> prettyTCM v2 <+> colon <+> prettyTCM tv) $ do
-- case tv of
-- (VPi dec x av env b) ->
case (v1,v2) of
(VGen k, VGen j) | k == j -> return emptySub
(VGen k, _) | elem k flex -> assignFlex k v2
(_, VGen k) | elem k flex -> assignFlex k v1
-- injectivity of data type constructors is unsound in general
(VApp (VDef (DefId DatK d1)) vl1,
VApp (VDef (DefId DatK d2)) vl2) | d1 == d2 -> do
(DataSig { numPars, symbTyp = tv, positivity = posl }) <- lookupSymbQ d1
instList' numPars posl flex tv vl1 vl2
-- ignore parameters (first numPars args)
-- this is sound because we have irrelevance for parameters
-- we assume injectivity for indices
-- Constructor applications are represented as VRecord
(VRecord (NamedRec _ c1 _ dot1) rs1,
VRecord (NamedRec _ c2 _ dot2) rs2) | c1 == c2 -> do
alignDotted dot1 dot2
sige <- lookupSymbQ c1
instList [] flex (symbTyp sige) (map snd rs1) (map snd rs2)
(VSucc v1', VSucc v2') -> instWh pos flex tv v1' v2'
(VSucc v, VInfty) -> instWh pos flex tv v VInfty
(VSing v1' tv1, VSing v2' tv2) -> do
subst <- inst pos flex tv tv1 tv2
u1 <- substitute subst v1'
u2 <- substitute subst v2'
tv1' <- substitute subst tv1
inst pos flex tv1' u1 u2 >>= compSubst subst
-- HACK AHEAD
(VUp v1 _, _) -> inst pos flex tv v1 v2
(_, VUp v2 _) -> inst pos flex tv v1 v2
-- (VUp v1' a1, VUp v2' a2) -> instList flex [a1,v1'] [a2,v2']
-- (VPi dec x1 av1 env1 b1, VPi dec x2 av2 env2 b2) ->
{- TODO: REPAIR THIS
_ -> traceCheck ("inst: WARNING! assuming " ++ show (context cxt) ++ " |- " ++ show v1 ++ " == " ++ show v2) $
return [] -- throwErrorMsg $ "inst: NYI"
-}
_ -> do leqVal pos tv v1 v2 `throwTrace` ("inst: leqVal " ++ show v1 ++ " ?<=" ++ show pos ++ " " ++ show v2 ++ " : " ++ show tv ++ " failed")
return emptySub
instList :: [Pol] -> [Int] -> TVal -> [Val] -> [Val] -> TypeCheck Substitution
instList = instList' 0
-- unify lists, ignoring the first np items
instList' :: Int -> [Pol] -> [Int] -> TVal -> [Val] -> [Val] -> TypeCheck Substitution
instList' np posl flex tv [] [] = return emptySub
instList' np posl flex tv (v1:vl1) (v2:vl2) = do
v1 <- whnfClos v1
v2 <- whnfClos v2
if (np <= 0 || isMeta flex v1 || isMeta flex v2) then
case tv of
(VQuant Pi x dom fv) -> do
let pol = getPol dom -- WAS: (headPosl posl)
subst <- inst pol flex (typ dom) v1 v2
vl1' <- mapM (substitute subst) vl1
vl2' <- mapM (substitute subst) vl2
v <- substitute subst v1
fv <- substitute subst fv
vb <- app fv v
subst' <- instList' (np - 1) (tailPosl posl) flex vb vl1' vl2'
compSubst subst subst'
else
case tv of
(VQuant Pi x dom fv) -> do
vb <- app fv v2
instList' (np - 1) (tailPosl posl) flex vb vl1 vl2
instList' np pos flex tv vl1 vl2 = fail $ "internal error: instList' " ++ show (np,pos,flex,tv,vl1,vl2) ++ " not handled"
headPosl :: [Pol] -> Pol
headPosl [] = mixed
headPosl (pos:_) = pos
tailPosl :: [Pol] -> [Pol]
tailPosl [] = []
tailPosl (_:posl) = posl
isMeta :: [Int] -> Val -> Bool
isMeta flex (VGen k) = k `elem` flex
isMeta _ _ = False
----------------------------------------------------------------------
-- * Substitution into values
----------------------------------------------------------------------
-- | Overloaded substitution of values for generic values (free variables).
class Substitute a where
substitute :: Substitution -> a -> TypeCheck a
instance Substitute v => Substitute (x,v) where
substitute subst (x,v) = (x,) <$> substitute subst v
instance Substitute v => Substitute [v] where
substitute = mapM . substitute
instance Substitute v => Substitute (Maybe v) where
substitute = Traversable.mapM . substitute
instance Substitute v => Substitute (Map k v) where
substitute = Traversable.mapM . substitute
instance Substitute v => Substitute (OneOrTwo v) where
substitute = Traversable.mapM . substitute
instance Substitute v => Substitute (Dom v) where
substitute = Traversable.mapM . substitute
instance Substitute v => Substitute (Measure v) where
substitute = Traversable.mapM . substitute
instance Substitute v => Substitute (Bound v) where
substitute = Traversable.mapM . substitute
instance Substitute v => Substitute (Sort v) where
substitute = Traversable.mapM . substitute
-- substitute generic variable in value
instance Substitute Val where
substitute subst v = do -- enterDoc (text "substitute" <$> prettyTCM v) $ do
let sub v = substitute subst v
case v of
VGen k -> return $ valuateGen k subst
VApp v1 vl -> foldM app ==<< (sub v1, sub vl)
VSing v1 vt -> vSing ==<< (sub v1, sub vt) -- TODO: Check reevaluation necessary?
VSucc v1 -> succSize <$> substitute subst v1
VMax vs -> maxSize <$> mapM (substitute subst) vs
VPlus vs -> plusSizes <$> mapM (substitute subst) vs
VCase v1 tv1 env cl -> VCase <$> sub v1 <*> sub tv1 <*> sub env <*> return cl
VMeasured mu bv -> VMeasured <$> sub mu <*> sub bv
VGuard beta bv -> VGuard <$> sub beta <*> sub bv
VBelow ltle v -> VBelow ltle <$> substitute subst v
VQuant pisig x dom fv -> VQuant pisig x <$> sub dom <*> sub fv
VRecord ri rs -> VRecord ri <$> sub rs
VPair v1 v2 -> VPair <$> sub v1 <*> sub v2
VProj{} -> return v
VLam x env b -> flip (VLam x) b <$> sub env
VConst v -> VConst <$> sub v
VAbs x i v valu -> VAbs x i v <$> sub valu
VClos env e -> flip VClos e <$> sub env
VUp v1 vt -> up False ==<< (sub v1, sub vt)
VSort s -> VSort <$> sub s
VZero -> return $ v
VInfty -> return $ v
VIrr -> return $ v
VDef id -> return $ vDef id -- because empty list of apps will be rem.
VMeta x env n -> flip (VMeta x) n <$> sub env
{- REDUNDANT
_ -> error $ "substitute: internal error: not defined for " ++ show v
-}
instance Substitute SemCxt where
substitute subst delta = do
cxt' <- substitute subst (cxt delta)
return $ delta { cxt = cxt' }
-- | Substitute in environment.
instance Substitute Env where
substitute subst (Environ rho mmeas) =
Environ <$> substitute subst rho <*> substitute subst mmeas
instance Substitute Substitution where
substitute subst2 subst1 = compSubst subst1 subst2
-- | "merge" substitutions by first applying the second to the first, then
-- appending them @t[sigma][tau] = t[sigma . tau]@
compSubst :: Substitution -> Substitution -> TypeCheck Substitution
compSubst (Valuation subst1) subst2@(Valuation subst2') =
Valuation . (++ subst2') <$> substitute subst2 subst1
----------------------------------------------------------------------
-- * Size checking
----------------------------------------------------------------------
{- TODO: From a sized data declaration
sized data D pars : Size -> t
{ c : [j : Size] -> args -> D pars $j ts
}
with constructor type
c : .pars -> [j : Size] -> args -> D pars $j ts
extract new-style constructor type
c : .pars -> [i : Size] -> [j < i : Size] -> args -> D pars i ts
Then replace in ConSig filed isSized :: Sized by :: Maybe Expr
which stores the new-style constructor type
-}
mkConLType :: Int -> Expr -> (Name, Expr)
mkConLType npars t =
let (Telescope (sizetb : tel), t0) = typeToTele t
in case spineView t0 of
(d@(Def (DefId DatK _)), args) ->
let (pars, sizeindex : inds) = splitAt npars args
i = fresh "s!ze"
args' = pars ++ Var i : inds
core = foldl App d args'
tbi = TBind i $ sizeDomain irrelevantDec
tbj = sizetb { boundDom = belowDomain irrelevantDec Lt (Var i) }
tel' = Telescope $ tbi : tbj : tel
in (i, teleToType tel' core)
_ -> error $ "conLType " ++ show npars ++ " (" ++ show t ++ "): illformed constructor type"
-- * check wether the data type is sized type
-- check data declaration type
-- called from typeCheckDeclaration (DataDecl{})
-- parameters : number of params, type
szType :: Co -> Int -> TVal -> TypeCheck ()
szType co p tv = doVParams p tv $ \ tv' -> do
let polsz = if co==Ind then Pos else Neg
case tv' of
VQuant Pi x (Domain av ki dec) fv | isVSize av && not (erased dec) && polarity dec == polsz -> return ()
_ -> throwErrorMsg $ "not a sized type, target " ++ show tv' ++ " must have non-erased domain " ++ show Size ++ " with polarity " ++ show polsz
-- * constructors of sized type
-- check data constructors
-- called from typeCheckConstructor
szConstructor :: Name -> Co -> Int -> TVal -> TypeCheck ()
szConstructor n co p tv = enterDoc (text ("szConstructor " ++ show n ++ " :") <+> prettyTCM tv) $ do
doVParams p tv $ \ tv' ->
case tv' of
VQuant Pi x dom fv | isVSize (typ dom) ->
underAbs x dom fv $ \ k xv bv -> do
szSizeVarUsage n co p k bv
_ -> fail $ "not a valid sized constructor: expected size quantification"
szSizeVarUsage :: Name -> Co -> Int -> Int -> TVal -> TypeCheck ()
szSizeVarUsage n co p i tv = enterDoc (text "szSizeVarUsage of" <+> prettyTCM (VGen i) <+> text "in" <+> prettyTCM tv) $
case tv of
VQuant Pi x dom fv -> do
let av = typ dom
szSizeVarDataArgs n p i av -- recursive calls of for D..i..
enterDoc (text "checking" <+> prettyTCM av <+> text (" to be " ++
(if co == CoInd then "antitone" else "isotone") ++ " in variable")
<+> prettyTCM (VGen i)) $
szMono co i av -- monotone in i
underAbs x dom fv $ \ _ xv bv -> do
szSizeVarUsage n co p i bv
_ -> szSizeVarTarget p i tv
-- check that Target is of form D ... (Succ i) ...
szSizeVarTarget :: Int -> Int -> TVal -> TypeCheck ()
szSizeVarTarget p i tv = enterDoc (text "szSizeVarTarget, variable" <+> prettyTCM (VGen i) <+> text ("argument no. " ++ show p ++ " in") <+> prettyTCM tv) $ do
let err = text "expected target" <+> prettyTCM tv <+> text "of size" <+> prettyTCM (VSucc (VGen i))
case tv of
VSing _ tv -> szSizeVarTarget p i =<< whnfClos tv
VApp d vl -> do
v0 <- whnfClos (vl !! p)
case v0 of
(VSucc (VGen i')) | i == i' -> return ()
_ -> failDoc err
_ -> failDoc err
-- check that rec. arguments are of form D ... i ....
-- and size used nowhere else ?? -- Andreas, 2009-11-27 TOO STRICT!
{- accepts, for instance
Nat -> Ord i as argument of a constructor of Ord ($ i)
List (Rose A i) as argument of a constructor of Rose A ($i)
-}
szSizeVarDataArgs :: Name -> Int -> Int -> TVal -> TypeCheck ()
szSizeVarDataArgs n p i tv = enterDoc (text "sizeVarDataArgs" <+> prettyTCM (VGen i) <+> text "in" <+> prettyTCM tv) $ do
case tv of
{- case D pars sizeArg args -}
VApp (VDef (DefId DatK (QName m))) vl | n == m -> do
let (pars, v0 : idxs) = splitAt p vl
v0 <- whnfClos v0
case v0 of
VGen i' | i' == i -> do
forM_ (pars ++ idxs) $ \ v -> nocc [i] v >>= do
boolToErrorDoc $
text "variable" <+> prettyTCM (VGen i) <+>
text "may not occur in" <+> prettyTCM v
_ -> failDoc $
text "wrong size index" <+> prettyTCM v0 <+>
text "at recursive occurrence" <+> prettyTCM tv
-- not necessary: check for monotonicity above
-- {- case D' pars sizeArg args -}
-- VApp (VDef m) vl | n /= m -> do
VApp v1 vl -> mapM_ (\ v -> whnfClos v >>= szSizeVarDataArgs n p i) (v1:vl)
VQuant Pi x dom fv -> do
szSizeVarDataArgs n p i (typ dom)
underAbs x dom fv $ \ _ xv bv -> do
szSizeVarDataArgs n p i bv
fv | isFun fv ->
addName (absName fv) $ \ xv -> szSizeVarDataArgs n p i =<< app fv xv
{-
VLam x env b ->
addName x $ \ xv -> do
bv <- whnf (update env x xv) b
szSizeVarDataArgs n p i bv
-}
_ -> return ()
{- REMOVED, 2009-11-28, replaced by monotonicity check
VGen i' -> return $ i' /= i
VSucc tv' -> szSizeVarDataArgs n p i tv'
-}
-- doVParams number_of_params constructor_or_datatype_signature
-- skip over parameters of type signature of a constructor/data type
doVParams :: Int -> TVal -> (TVal -> TypeCheck a) -> TypeCheck a
doVParams 0 tv k = k tv
doVParams p (VQuant Pi x dom fv) k =
underAbs x dom fv $ \ _ xv bv -> do
doVParams (p - 1) bv k
--------------------------------------
-- check for admissible type
{-
- admissibility needs to be check clausewise, because of Karl's example
fun nonAdmissibleType : Unit -> Set
fun diverge : (u : Unit) -> nonAdmissibleType u
{
diverge unit patterns = badRhs
}
- the type must be admissible in the current position
only if the size pattern is a successor.
If the pattern is a variable, then there is no induction on that size
argument, so no limit case, so no upper semi-continuity necessary
for the type.
- when checking
... (s i) ps admissible (j : Size) -> A
we will check
A admissible in j
and continue with
... ps admissible A[s i / j]
just to maintain type wellformedness. The (s i) in A does not
really matter, since there is no case distinction on ordinals.
- a size pattern which is not inductive (meaning there is an
inductive type indexed by that size) nor coinductive (meaning that
the result type is coinductive and is indexed by that size) must
be flagged unusable for termination checking.
- the fun/cofun distinction could be inferred by the termination checker
or be clausewise as in Agda 2
-}
admFunDef :: Co -> [Clause] -> TVal -> TypeCheck [Clause]
admFunDef co cls tv = do
(cls, inco) <- admClauses cls tv
when (co==CoInd && not (co `elem` inco)) $
fail $ show tv ++ " is not a type of a cofun" -- ++ if co==Ind then "fun" else "cofun"
return cls
admClauses :: [Clause] -> TVal -> TypeCheck ([Clause], [Co])
admClauses [] tv = return ([], [])
admClauses (cl:cls) tv = do
(cl',inco) <- admClause cl tv
(cls',inco') <- admClauses cls tv
return (cl' : cls', inco ++ inco')
admClause :: Clause -> TVal -> TypeCheck (Clause, [Co])
admClause (Clause tel ps e) tv = traceAdm ("admClause: admissibility of patterns " ++ show ps) $
introPatterns ps tv $ \ pvs _ -> do
(ps', inco) <- admPatterns pvs tv
return (Clause tel ps' e, inco)
admPatterns :: [(Pattern,Val)] -> TVal -> TypeCheck ([Pattern], [Co])
admPatterns [] tv = do
isCo <- endsInCo tv
return ([], if isCo then [CoInd] else [])
admPatterns ((p,v):pvs) tv = do
(p, inco1) <- admPattern p tv
bv <- piApp tv v
(ps, inco2) <- admPatterns pvs bv
return (p:ps, inco1 ++ inco2)
{-
-- turn a pattern into a value
-- extend delta by generic values but do not introduce their types
evalPat :: Pattern -> (Val -> TypeCheck a) -> TypeCheck a
evalPat p f =
case p of
VarP n -> addName n f
ConP co n [] -> f (VCon co n)
ConP co n pl -> evalPats pl $ \ vl -> f (VApp (VCon co n) vl)
SuccP p -> evalPat p $ \ v -> f (VSucc v)
-- DOES NOT WORK SINCE e has unbound variables
DotP e -> do
v <- whnf' e
f v
evalPats :: [Pattern] -> ([Val] -> TypeCheck a) -> TypeCheck a
evalPats [] f = f []
evalPats (p:ps) f = evalPat p $ \ v -> evalPats ps $ \ vs -> f (v:vs)
-}
{-
evalPat :: Pattern -> TypeCheck (State TCContext Val)
evalPat p =
case p of
VarP n -> return $ State $ \ ce ->
let (k, delta) = cxtPushGen (context ce)
rho = update n (VGen k) (environ ce)
in (VGen k, TCContext { context = delta, environ = rho })
ConP co n [] -> return (VCon co n)
ConP co n pl -> do
vl <- mapM evalPat pl
return (VApp (VCon co n) vl)
SuccP p -> do
v <- evalPat p
return (VSucc v)
-- TODO: does not work!
-- DotP e -> return $ State $ \ ce ->
-}
{- 2013-03-31 On instantiation of quantifiers [i < #] - F i
If F is upper semi-continuous then
[i < #] -> F i is a sub"set" of F #
so we can instantiate i to #. (Hughes et al., POPL 96; Abel, LMCS 08)
1) Consider the special case
F i = [j < i] -> G i
Because # is a limit, thus, j < i < # iff j < #, we reason:
F # = [j < #] -> G j
[i < #] -> F i
= [i < #] -> [j < i] -> G j (since # is a limit)
= [j < #] -> G j
2) Consider the special case
F i = [j <= i] -> G j
We have
F # = [j <= #] -> G j
= G # /\ ([j < #] -> G j)
[i < #] -> F i
= [i < #] -> [j <= i] -> G j
= [j < #] -> G j
So if G is upper semi-continuous, so is F.
-}
-- | Check whether a type is upper semi-continuous.
lowerSemiCont :: Int -> TVal -> TypeCheck Bool
lowerSemiCont i tv = errorToBool $ lowerSemiContinuous i tv
docNotLowerSemi i av = text "type " <+> prettyTCM av <+>
text " not lower semi continuous in " <+> prettyTCM (VGen i)
lowerSemiContinuous :: Int -> TVal -> TypeCheck ()
lowerSemiContinuous i av = do
av <- force av
let fallback = szAntitone i av `newErrorDoc` docNotLowerSemi i av
case av of
-- [j < i] & F j is lower semi-cont in i
-- because [i < #] & [j < i] & F j is the same as [j < #] & F j
-- [but what if i in FV(F j)? should not matter!] 2013-04-01
VQuant Sigma x dom@Domain{ typ = VBelow Lt (VGen i') } fv | i == i' -> return ()
-- [j <= i] & F j is lower semi-cont in i if F is
VQuant Sigma x dom@Domain{ typ = VBelow Le (VGen i') } fv | i == i' -> do
underAbs x dom fv $ \ j xv bv -> lowerSemiContinuous j bv
-- Sigma-type general case
VQuant Sigma x dom@Domain{ typ = av } fv -> do
lowerSemiContinuous i av
underAbs x dom fv $ \ _ xv bv -> lowerSemiContinuous i bv
VApp (VDef (DefId DatK n)) vl -> do
sige <- lookupSymbQ n
case sige of
-- finite tuple type
DataSig { symbTyp = dv, constructors = cis, isTuple = True } -> do
-- match target of constructor against tv to instantiate
-- c : ... -> D ps -- ps = snd (cPatFam ci)
mrhoci <- Util.firstJustM $ map (\ ci -> fmap (,ci) <$> nonLinMatchList False emptyEnv (snd $ cPatFam ci) vl dv) cis
case mrhoci of
Nothing -> fallback
Just (rho,ci) -> if (cRec ci) then fallback else do
-- infinite tuples (recursive constructor) are not lower semi cont
enter ("lowerSemiContinuous: detected tuple type, checking components") $
allComponentTypes (cFields ci) rho (lowerSemiContinuous i)
-- i-sized inductive types are lower semi-cont in i
DataSig { numPars, isSized = Sized, isCo = Ind } | length vl > numPars -> do
s <- whnfClos $ vl !! numPars -- the size argument is the first fgter the parameters
case s of
VGen i' | i == i' -> return ()
_ -> fallback
-- finite inductive type
DataSig { symbTyp = dv, constructors = cis, isCo = Ind } ->
-- if any cRec cis then fallback else do -- we loop on recursive data, so exclude
-- check that we do not loop on the same data names...
ifM ((n `elem`) <$> asks callStack) fallback $ do
local (\ ce -> ce { callStack = n : callStack ce }) $ do
-- match target of constructor against tv to instantiate
-- c : ... -> D ps -- ps = snd (cPatFam ci)
forM_ cis $ \ ci -> do
match <- nonLinMatchList False emptyEnv (snd $ cPatFam ci) vl dv
Foldable.forM_ match $ \ rho -> do
enter ("lowerSemiContinuous: detected tuple type, checking components") $
allComponentTypes (cFields ci) rho (lowerSemiContinuous i)
_ -> fallback
_ -> fallback
-- | Check whether a type is upper semi-continuous.
upperSemiCont :: Int -> TVal -> TypeCheck Bool
upperSemiCont i tv = errorToBool $ endsInSizedCo' False i tv
-- 2013-03-30
-- endsInSizedCo needs tv[0/i] = Top
-- upperSemiCont does not need this, the target can also be constant in i
-- | @endsInSizedCo i tv@ checks that @tv@ is lower semi-continuous in @i@
-- and that @tv[0/i] = Top@.
endsInSizedCo :: Int -> TVal -> TypeCheck ()
endsInSizedCo = endsInSizedCo' True
-- | @endsInSizedCo' False i tv@ checks that @tv@ is lower semi-continuous in @i@.
-- @endsInSizedCo' True i tv@ additionally checks that @tv[0/i] = Top@.
endsInSizedCo' :: Bool -> Int -> TVal -> TypeCheck ()
endsInSizedCo' endInCo i tv = enterDoc (text "endsInSizedCo:" <+> prettyTCM tv) $ do
tv <- force tv
let fallback
| endInCo = failDoc $ text "endsInSizedCo: target" <+> prettyTCM tv <+> text "of corecursive function is neither a CoSet or codata of size" <+> prettyTCM (VGen i) <+> text "nor a tuple type"
| otherwise = szMonotone i tv
case tv of
VSort (CoSet (VGen i)) -> return ()
VMeasured mu bv -> endsInSizedCo' endInCo i bv
-- case forall j <= i. C j coinductive in i
VQuant Pi x dom@Domain{ typ = VBelow Le (VGen i') } fv | i == i' ->
underAbs x dom fv $ \ j xv bv ->
endsInSizedCo' endInCo j bv
VGuard (Bound Le (Measure [VGen j]) (Measure [VGen i'])) bv | i == i' ->
endsInSizedCo' endInCo j bv
-- same case again, written as j < i+1. C j
VQuant Pi x dom@Domain{ typ = VBelow Lt (VSucc (VGen i')) } fv | i == i' ->
underAbs x dom fv $ \ j xv bv ->
endsInSizedCo' endInCo j bv
VGuard (Bound Lt (Measure [VGen j]) (Measure [VSucc (VGen i')])) bv | i == i' ->
endsInSizedCo' endInCo j bv
-- case forall j < i. C j: already coinductive in i !!
-- Trivially, forall j < 0. C j is the top type.
-- And, forall i < # forall j < i is equivalent to forall j < #
-- so we can instantiate i to #.
VGuard (Bound Lt (Measure [VGen j]) (Measure [VGen i'])) bv | i == i' ->
return ()
VQuant Pi x dom@Domain{ typ = VBelow Lt (VGen i') } fv | i == i' -> return ()
VQuant Pi x dom fv -> do
lowerSemiContinuous i $ typ dom
underAbs x dom fv $ \ _ xv bv -> endsInSizedCo' endInCo i bv
VSing _ tv -> endsInSizedCo' endInCo i =<< whnfClos tv
VApp (VDef (DefId DatK n)) vl -> do
sige <- lookupSymbQ n
case sige of
DataSig { numPars = np, isSized = Sized, isCo = CoInd }
| length vl > np -> do
v <- whnfClos $ vl !! np
if isVGeni v then return () else fallback
where isVGeni (VGen i) = True
isVGeni (VPlus vs) = and $ map isVGeni vs
isVGeni (VMax vs) = and $ map isVGeni vs
isVGeni VZero = True
isVGeni _ = False
{- WE DO NOT HAVE SUBST ON VALUES!
case vl !! np of
VGen j -> if i == j then return () else fail1
VZero -> return ()
VClos rho e -> do
v <- whnf (update rho i VZero) e -- BUGGER
if v == VZero then return () else fail1
-}
-- we also allow the target to be a tuple if all of its components
-- fulfill "endsInSizedCo"
DataSig { symbTyp = dv, constructors = cis, isTuple = True } -> do
allTypesOfTuple tv vl dv cis (endsInSizedCo' endInCo i)
{-
-- match target of constructor against tv to instantiate
-- c : ... -> D ps -- ps = snd (cPatFam ci)
mrhoci <- Util.firstJustM $ map (\ ci -> fmap (,ci) <$> nonLinMatchList False emptyEnv (snd $ cPatFam ci) vl dv) cis
case mrhoci of
Nothing -> failDoc $ text "endsInSizedCo: panic: target type" <+> prettyTCM tv <+> text "is not an instance of any constructor"
Just (rho,ci) -> enter ("endsInSizedCo: detected tuple target, checking components") $
fieldsEndInSizedCo endInCo i (cFields ci) rho
-}
_ -> fallback
_ -> fallback
{- failDoc $ text "endsInSizedCo: target" <+> prettyTCM tv <+> text "of corecursive function is neither a function type nor a codata nor a tuple type"
-}
-- | @allTypesOfTyples args dv cis check@ performs @check@ on all component
-- types of tuple type @tv = d args@ where @dv@ is the type of @d@.
allTypesOfTuple :: TVal -> [Val] -> TVal -> [ConstructorInfo] -> (TVal -> TypeCheck ()) -> TypeCheck ()
allTypesOfTuple tv vl dv cis check = do
-- match target of constructor against tv to instantiate
-- c : ... -> D ps -- ps = snd (cPatFam ci)
mrhoci <- Util.firstJustM $
map (\ ci -> fmap (,ci) <$> nonLinMatchList False emptyEnv (snd $ cPatFam ci) vl dv) cis
-- we know that only one constructor can match, otherwise it would not be a tuple type
case mrhoci of
Nothing -> failDoc $ text "allTypesOfTuple: panic: target type" <+> prettyTCM tv <+> text "is not an instance of any constructor"
Just (rho,ci) -> enter ("allTypesOfTuple: detected tuple target, checking components") $
allComponentTypes (cFields ci) rho check
{-
fieldsEndInSizedCo :: Bool -> Int -> [FieldInfo] -> Env -> TypeCheck ()
fieldsEndInSizedCo endInCo i fis rho0 = allComponentTypes fis rho0 (endsInSizedCo' endInCo i)
fieldsEndInSizedCo endInCo i fis rho0 = enter ("fieldsEndInSizedCo: checking fields of tuple type " ++ show fis ++ " in environment " ++ show rho0) $
loop fis rho0 where
loop [] rho = return ()
-- nothing to check for erased index fields
loop (f : fs) rho | fClass f == Index && erased (fDec f) =
loop fs rho
loop (f : fs) rho | fClass f == Index = do
tv <- whnf rho (fType f)
endsInSizedCo' endInCo i tv
loop fs rho
loop (f : fs) rho = do
tv <- whnf rho (fType f)
when (not $ erased (fDec f)) $ endsInSizedCo' endInCo i tv
-- for non-index fields, value is not given by matching, so introduce
-- generic value
new (fName f) (Domain tv defaultKind (fDec f)) $ \ xv -> do
let rho' = update rho (fName f) xv
-- do not need to check erased fields?
loop fs rho'
-}
-- | @allComponentTypes fis env check@ applies @check@ to all field types
-- in @fis@ (evaluated wrt to environment @env@).
-- Erased fields are skipped. (Is this correct?)
allComponentTypes :: [FieldInfo] -> Env -> (TVal -> TypeCheck ()) -> TypeCheck ()
allComponentTypes fis rho0 check = enter ("allComponentTypes: checking fields of tuple type " ++ show fis ++ " in environment " ++ show rho0) $
loop fis rho0 where
loop [] rho = return ()
-- nothing to check for erased index fields
loop (f : fs) rho | fClass f == Index && erased (fDec f) =
loop fs rho
-- ordinary index field types are checked
loop (f : fs) rho | fClass f == Index = do
check =<< whnf rho (fType f)
loop fs rho
-- proper fields
loop (f : fs) rho = do
tv <- whnf rho (fType f)
-- do not need to check erased fields?
when (not $ erased (fDec f)) $ check tv
-- for non-index fields, value is not given by matching, so introduce
-- generic value
new (fName f) (Domain tv defaultKind (fDec f)) $ \ xv -> do
loop fs $ update rho (fName f) xv
endsInCo :: TVal -> TypeCheck Bool
endsInCo tv = -- traceCheck ("endsInCo: " ++ show tv) $
case tv of
VQuant Pi x dom fv -> underAbs x dom fv $ \ _ _ bv -> endsInCo bv
VApp (VDef (DefId DatK n)) vl -> do
sige <- lookupSymbQ n
case sige of
DataSig { isCo = CoInd } -> -- traceCheck ("found non-sized coinductive target") $
return True
_ -> return False
_ -> return False
-- precondition: Pattern does not contain "Unusable"
admPattern :: Pattern -> TVal -> TypeCheck (Pattern, [Co])
admPattern p tv = traceAdm ("admPattern " ++ show p ++ " type: " ++ show tv) $
case tv of
VGuard beta bv -> addBoundHyp beta $ admPattern p bv
VApp (VDef (DefId DatK d)) vl -> do
case p of
ProjP n -> return (p, [])
_ -> fail "admPattern: IMPOSSIBLE: non-projection pattern for record type"
VQuant Pi x dom fv -> underAbs x dom fv $ \ k xv bv -> do
{-
if p is successor pattern
check that bv is admissible in k, returning subset of [Ind, CoInd]
p is usable if either CoInd or it is a var or dot pattern and Ind
-}
if isSuccessorPattern p then do
inco <- admType k bv
when (CoInd `elem` inco && not (shallowSuccP p)) $ cannotMatchDeep p tv
if (CoInd `elem` inco)
|| (inco /= [] && completeP p)
then return (p, inco)
else return (UnusableP p, inco)
else return (p, [])
_ -> fail "admPattern: IMPOSSIBLE: pattern for a non-function type"
cannotMatchDeep p tv = recoverFailDoc $
text "cannot match against deep successor pattern"
<+> text (show p) <+> text "at type" <+> prettyTCM tv
admType :: Int -> TVal -> TypeCheck [Co]
admType i tv = enter ("admType: checking " ++ show tv ++ " admissible in v" ++ show i) $
case tv of
VQuant Pi x dom@(Domain av _ _) fv -> do
isInd <- szUsed Ind i av
when (not isInd) $
szAntitone i av `newErrorDoc` docNotLowerSemi i av
underAbs x dom fv $ \ gen _ bv -> do
inco <- admType i bv
if isInd then return (Ind : inco) else return inco
_ -> do
isCoind <- szUsed CoInd i tv
if isCoind then return [CoInd]
else do
szMonotone i tv
return []
szUsed :: Co -> Int -> TVal -> TypeCheck Bool
szUsed co i tv = traceAdm ("szUsed: " ++ show tv ++ " " ++ show co ++ " in v" ++ show i) $
case tv of
(VApp (VDef (DefId DatK n)) vl) ->
do sige <- lookupSymbQ n
case sige of
DataSig { numPars = p
, isSized = Sized
, isCo = co' } | co == co' && length vl > p ->
-- p is the number of parameters
-- it is also the index of the size argument
do s <- whnfClos $ vl !! p
case s of
VGen i' | i == i' -> return True
_ -> return False
_ -> return False
_ -> return False
-- for inductive fun, and for every size argument i
-- - every argument needs to be either inductive or antitone in i
-- - the result needs to be monotone in i
{- szCheckIndFun admpos delta tv
entry point for admissibility check for recursive functions
- scans for the first size quantification
- passes on to szCheckIndFunSize
- currently: also continues to look for the next size quantification...
-}
szCheckIndFun :: [Int] -> TVal -> TypeCheck ()
szCheckIndFun admpos tv = -- traceCheck ("szCheckIndFun: " ++ show delta ++ " |- " ++ show tv ++ " adm?") $
case tv of
VQuant Pi x dom fv -> underAbs x dom fv $ \ k _ bv -> do
-- bv <- whnf' b
if isVSize (typ dom) then do
when (k `elem` admpos) $
szCheckIndFunSize k bv
szCheckIndFun admpos bv -- this is for lexicographic induction on sizes, I suppose? Probably should me more fine grained! Andreas, 2008-12-01
else szCheckIndFun admpos bv
_ -> return ()
{- szCheckIndFunSize delta i tv
checks whether type tv is admissible for recursion in index i
- every argument needs to be either inductive or antitone in i
- the result needs to be monotone in i
-}
szCheckIndFunSize :: Int -> TVal -> TypeCheck ()
szCheckIndFunSize i tv = -- traceCheck ("szCheckIndFunSize: " ++ show delta ++ " |- " ++ show tv ++ " adm(v" ++ show i ++ ")?") $
case tv of
VQuant Pi x dom fv -> do
szLowerSemiCont i (typ dom)
-- new x dom $ \ k _ -> szCheckIndFunSize i =<< app fv (VGen k)
underAbs x dom fv $ \ _ _ bv -> szCheckIndFunSize i bv
{-
new' x dom $ do
bv <- whnf' b
szCheckIndFunSize i bv
-}
_ -> szMonotone i tv
{- szLowerSemiCont
- check for lower semi-continuity [Abel, CSL 2006]
- current approximation: inductive type or antitone
-}
szLowerSemiCont :: Int -> TVal -> TypeCheck ()
szLowerSemiCont i av = -- traceCheck ("szlowerSemiCont: checking " ++ show av ++ " lower semi continuous in v" ++ show i) $
(szAntitone i av `catchError`
(\ msg -> -- traceCheck (show msg) $
szInductive i av))
`newErrorDoc` docNotLowerSemi i av
{- checking cofun-types for admissibility
conditions:
1. type must end in coinductive type or in sized coinductive type
indexed by just a variable i which has been quantified in the type
2. in the second case, each argument must be inductive or antitone in i
optimization:
arguments types before the quantification over i can be ignored
-}
data CoFunType
= CoFun -- yes, but not sized cotermination
| SizedCoFun Int -- yes an admissible sized type (the Int specifies the number of the recursive size argument)
{-
design:
admCoFun delta tv : IsCoFunType
endsInCo delta tv (len delta) id
admEndsInCo delta tv firstVar jobs : IsCoFunType
traverse tv, gather continutations in jobs, check for CoInd in the end
if tv = (x:A) -> B
push A on delta
add the following task to jobs:
check A for lower semicontinuity in delta
continue on B
if tv = Codata^i
run (jobs i)
if they return (), return YesSized Int, otherwise No
if tv = Codata
return Yes
otherwise
return No
-}
-- {- TODO: FINISH THIS!!
admCoFun :: TVal -> TypeCheck CoFunType
admCoFun tv = do
l <- getLen
admEndsInCo tv l (\ i -> return ())
admEndsInCo :: TVal -> Int -> (Int -> TypeCheck ()) -> TypeCheck CoFunType
admEndsInCo tv firstVar jobs = -- traceCheck ("admEndsInCo: " ++ show tv) $
case tv of
VQuant Pi x dom fv -> do
l <- getLen
let jobs' = (addJob l (typ dom) jobs)
underAbs x dom fv $ \ _ _ bv -> admEndsInCo bv firstVar jobs'
{-
new' x dom $ do
bv <- whnf' b
admEndsInCo bv firstVar jobs'
-}
{-
-- if not applied, it cannot be a sized type
VDef n -> do
sig <- gets signature
case (lookupSig n sig) of
DataSig { isCo = CoInd } -> -- traceCheck ("found non-sized coinductive target") $
return CoFun
_ -> throwErrorMsg $ "type of cofun does not end in coinductive type"
-}
VApp (VDef (DefId DatK n)) vl -> do
sige <- lookupSymbQ n
case sige of
DataSig { isSized = NotSized, isCo = CoInd } -> -- traceCheck ("found non-sized coinductive target") $
return CoFun
DataSig { numPars = p, isSized = Sized, isCo = CoInd } | length vl > p -> -- traceCheck ("found sized coinductive target") $
do
-- p is the number of parameters
-- it is also the index of the size argument
s <- whnfClos $ vl !! p
case s of
VGen i -> do
jobs i
return $ SizedCoFun $ i - firstVar
_ -> throwErrorMsg $ "size argument in result type must be a variable"
_ -> throwErrorMsg $ "type of cofun does not end in coinductive type"
addJob :: Int -> TVal -> (Int -> TypeCheck ())
-> (Int -> TypeCheck ())
addJob l tv jobs recVar = do
-- is the "recursive" size variable actually in scope?
jobs recVar
when (recVar < l) $ szLowerSemiCont recVar tv
-- -}
{- szCheckCoFun OBSOLETE!!
entry point for admissibility check for corecursive functions
- scans for the first size quantification
- passes on to szCheckIndFunSize
- currently: also continues to look for the next size quantification
- and checks in the end whether the target is a coinductive type
-- STALE COMMENT: for a cofun : arguments nocc i and result coinductive in i
szCheckCoFun :: SemCxt -> TVal -> TypeCheck ()
szCheckCoFun delta tv =
case tv of
VPi dec x av env b -> do
let (k, delta') = cxtPush dec av delta
bv <- whnf (update env x (VGen k)) b
case av of
VSize -> do szCheckCoFunSize delta' k bv
szCheckCoFun delta' bv
_ -> szCheckCoFun delta' bv
-- result
(VApp (VDef n) vl) ->
do sig <- gets signature
case (lookupSig n sig) of
(DataSig _ _ _ CoInd _) ->
return ()
_ -> throwErrorMsg $ "cofun doesn't target coinductive type"
(VDef n) ->
do sig <- gets signature
case (lookupSig n sig) of
(DataSig _ _ _ CoInd _) ->
return ()
_ -> throwErrorMsg $ "cofun doesn't target coinductive type"
_ -> throwErrorMsg $ "cofun doesn't target coinductive type"
szCheckCoFunSize :: SemCxt -> Int -> TVal -> TypeCheck ()
szCheckCoFunSize delta i tv = -- traceCheck ("szco " ++ show tv) $
case tv of
VPi dec x av env b -> do
let (k, delta') = cxtPush dec av delta
bv <- whnf (update env x (VGen k)) b
szLowerSemiCont delta i av
szCheckCoFunSize delta' i bv
-- result must be coinductive
_ -> szCoInductive delta i tv
-}
szMono :: Co -> Int -> TVal -> TypeCheck ()
szMono co i tv =
case co of
Ind -> szMonotone i tv
CoInd -> szAntitone i tv
szMonotone :: Int -> TVal -> TypeCheck ()
szMonotone i tv = traceCheck ("szMonotone: " -- ++ show delta ++ " |- "
++ show tv ++ " mon(v" ++ show i ++ ")?") $
do
let si = VSucc (VGen i)
tv' <- substitute (sgSub i si) tv
leqVal Pos vTopSort tv tv'
szAntitone :: Int -> TVal -> TypeCheck ()
szAntitone i tv = traceCheck ("szAntitone: " -- ++ show delta ++ " |- "
++ show tv ++ " anti(v" ++ show i ++ ")?") $
do
let si = VSucc (VGen i)
tv' <- substitute (sgSub i si) tv
leqVal Neg vTopSort tv tv'
-- checks if tv is a sized inductive type of size i
szInductive :: Int -> TVal -> TypeCheck ()
szInductive i tv = szUsed' Ind i tv
-- checks if tv is a sized coinductive type of size i
szCoInductive :: Int -> TVal -> TypeCheck ()
szCoInductive i tv = szUsed' CoInd i tv
szUsed' :: Co -> Int -> TVal -> TypeCheck ()
szUsed' co i tv =
case tv of
(VApp (VDef (DefId DatK n)) vl) ->
do sige <- lookupSymbQ n
case sige of
DataSig { numPars = p, isSized = Sized, isCo = co' } | co == co' && length vl > p ->
-- p is the number of parameters
-- it is also the index of the size argument
do s <- whnfClos $ vl !! p
case s of
VGen i' | i == i' -> return ()
_ -> fail $ "expected size variable"
_ -> fail $ "expected (co)inductive sized type"
_ -> fail $ "expected (co)inductive sized type"