{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Generalize
( generalizeType
, generalizeType'
, generalizeTelescope ) where
import Control.Arrow ((***), first, second)
import Control.Monad
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Data.List (nub, partition, init, sortBy)
import Data.Function (on)
import Data.Traversable
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name (LensInScope(..))
import Agda.Syntax.Position
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Agda.Syntax.Scope.Monad (bindVariable)
import Agda.Syntax.Scope.Base (Binder(..))
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Abstract
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.InstanceArguments (postponeInstanceConstraints)
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Warnings
import Agda.Benchmarking (Phase(Typing, Generalize))
import Agda.Utils.Benchmark
import Agda.Utils.Except
import Agda.Utils.Functor
import Agda.Utils.Impossible
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Size
import Agda.Utils.Permutation
import qualified Agda.Utils.Graph.TopSort as Graph
#include "undefined.h"
generalizeTelescope :: Map QName Name -> (forall a. (Telescope -> TCM a) -> TCM a) -> ([Maybe Name] -> Telescope -> TCM a) -> TCM a
generalizeTelescope vars typecheckAction ret | Map.null vars = typecheckAction (ret [])
generalizeTelescope vars typecheckAction ret = billTo [Typing, Generalize] $ withGenRecVar $ \ genRecMeta -> do
let s = Set.fromList (Map.keys vars)
((cxtNames, tel, letbinds), namedMetas, allmetas) <-
createMetasAndTypeCheck s $ typecheckAction $ \ tel -> do
cxt <- take (size tel) <$> getContext
lbs <- getLetBindings
return (map (fst . unDom) cxt, tel, lbs)
(genTel, genTelNames, sub) <- computeGeneralization genRecMeta namedMetas allmetas
let boundVar q = fromMaybe __IMPOSSIBLE__ $ Map.lookup q vars
genTelVars = (map . fmap) boundVar genTelNames
tel' <- applySubst sub <$> instantiateFull tel
let setName name d = first (const name) <$> d
cxtEntry (mname, d) = do
name <- maybe (setNotInScope <$> freshName_ s) return mname
return $ setName name d
where s = fst $ unDom d
dropCxt err = updateContext (strengthenS err 1) (drop 1)
genTelCxt <- dropCxt __IMPOSSIBLE__ $ mapM cxtEntry $ reverse $ zip genTelVars $ telToList genTel
let newTelCxt = zipWith setName cxtNames $ reverse $ telToList tel'
letbinds' <- applySubst (liftS (size tel) sub) <$> instantiateFull letbinds
let addLet (x, (v, dom)) = addLetBinding' x v dom
updateContext sub ((genTelCxt ++) . drop 1) $
updateContext (raiseS (size tel')) (newTelCxt ++) $
foldr addLet (ret genTelVars $ abstract genTel tel') letbinds'
generalizeType :: Set QName -> TCM Type -> TCM ([Maybe QName], Type)
generalizeType s typecheckAction = do
(ns, t, _) <- generalizeType' s $ (,()) <$> typecheckAction
return (ns, t)
generalizeType' :: Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
generalizeType' s typecheckAction = billTo [Typing, Generalize] $ withGenRecVar $ \ genRecMeta -> do
((t, userdata), namedMetas, allmetas) <- createMetasAndTypeCheck s typecheckAction
(genTel, genTelNames, sub) <- computeGeneralization genRecMeta namedMetas allmetas
t' <- abstract genTel . applySubst sub <$> instantiateFull t
reportSDoc "tc.generalize" 40 $ vcat
[ "generalized"
, nest 2 $ "t =" <+> escapeContext 1 (prettyTCM t') ]
return (genTelNames, t', userdata)
createMetasAndTypeCheck :: Set QName -> TCM a -> TCM (a, Map MetaId QName, Set MetaId)
createMetasAndTypeCheck s typecheckAction = do
((namedMetas, x), allmetas) <- metasCreatedBy $ do
(metamap, genvals) <- createGenValues s
x <- locallyTC eGeneralizedVars (const genvals) typecheckAction
return (metamap, x)
return (x, namedMetas, allmetas)
withGenRecVar :: (Type -> TCM a) -> TCM a
withGenRecVar ret = do
genRecMeta <- newTypeMeta (mkType 0)
addContext (defaultDom ("genTel" :: String, genRecMeta)) $ ret genRecMeta
computeGeneralization :: Type -> Map MetaId name -> Set MetaId -> TCM (Telescope, [Maybe name], Substitution)
computeGeneralization genRecMeta nameMap allmetas = postponeInstanceConstraints $ do
mvs <- mapM (\ x -> (x,) <$> lookupMeta x) (Set.toList allmetas)
let isGeneralizable (_, mv) = YesGeneralize == unArg (miGeneralizable (mvInfo mv))
isSort = isSortMeta_ . snd
isOpen = isOpenMeta . mvInstantiation . snd
let (generalizable, nongeneralizable) = partition isGeneralizable mvs
(generalizableOpen', generalizableClosed) = partition isOpen generalizable
(openSortMetas, generalizableOpen) = partition isSort generalizableOpen'
nongeneralizableOpen = filter isOpen nongeneralizable
case openSortMetas of
[] -> return ()
ms -> warning $ CantGeneralizeOverSorts (map fst ms)
cp <- viewTC eCurrentCheckpoint
let canGeneralize x = do
mv <- lookupMeta x
msub <- enterClosure (miClosRange $ mvInfo mv) $ \ _ ->
checkpointSubstitution' cp
let sameContext =
case (msub, mvPermutation mv) of
(Just IdS, Perm m xs) -> xs == [0 .. m - 1]
(Just (Wk n IdS), Perm m xs) -> xs == [0 .. m - n - 1]
_ -> False
when (not sameContext) $ do
ty <- getMetaType x
let Perm m xs = mvPermutation mv
reportSDoc "tc.generalize" 20 $ vcat
[ text "Don't know how to generalize over"
, nest 2 $ prettyTCM x <+> text ":" <+> prettyTCM ty
, text "in context"
, nest 2 $ inTopContext . prettyTCM =<< getContextTelescope
, text "permutation:" <+> text (show (m, xs))
, text "subst:" <+> pretty msub ]
return sameContext
inherited <- fmap Set.unions $ forM generalizableClosed $ \ (x, mv) ->
case mvInstantiation mv of
InstV _ v -> do
parentName <- getMetaNameSuggestion x
metas <- filterM canGeneralize . allMetas =<< instantiateFull v
let suggestNames i [] = return ()
suggestNames i (m : ms) = do
name <- getMetaNameSuggestion m
case name of
"" -> do
setMetaNameSuggestion m (parentName ++ "." ++ show i)
suggestNames (i + 1) ms
_ -> suggestNames i ms
Set.fromList metas <$ suggestNames 1 metas
_ -> __IMPOSSIBLE__
let (alsoGeneralize, reallyDontGeneralize) = partition (`Set.member` inherited) $ map fst nongeneralizableOpen
generalizeOver = map fst generalizableOpen ++ alsoGeneralize
sortedMetas <- sortMetas generalizeOver
let dropCxt err = updateContext (strengthenS err 1) (drop 1)
(genRecName, genRecCon, genRecFields) <- dropCxt __IMPOSSIBLE__ $
createGenRecordType genRecMeta sortedMetas
cxtTel <- getContextTelescope
let solve m field = assignTerm' m (telToArgs cxtTel) $ Var 0 [Proj ProjSystem field]
zipWithM_ solve sortedMetas genRecFields
let telNames = map (`Map.lookup` nameMap) sortedMetas
teleTypes <- do
args <- getContextArgs
fmap concat $ forM sortedMetas $ \ m -> do
mv <- lookupMeta m
let info = getArgInfo $ miGeneralizable $ mvInfo mv
HasType{ jMetaType = t } = mvJudgement mv
return [(Arg info $ miNameSuggestion $ mvInfo mv, piApply t args)]
let genTel = buildGeneralizeTel genRecCon teleTypes
reportSDoc "tc.generalize" 40 $ vcat
[ text "genTel =" <+> prettyTCM genTel ]
dropCxt __IMPOSSIBLE__ $ fillInGenRecordDetails genRecName genRecCon genRecFields genRecMeta genTel
let sub = unpackSub genRecCon (map (argInfo . fst) teleTypes) (length teleTypes)
let inscope (ii, InteractionPoint{ipMeta = Just x})
| Set.member x allmetas = [(x, ii)]
inscope _ = []
ips <- Map.fromList . concatMap inscope . Map.toList <$> useTC stInteractionPoints
cp <- viewTC eCurrentCheckpoint
forM_ reallyDontGeneralize $ \ x -> do
mv <- lookupMeta x
when (isOpenMeta $ mvInstantiation mv) $ enterClosure (miClosRange $ mvInfo mv) $ \ _ -> do
cxt <- instantiateFull =<< getContext
let notPruned = [ i | i <- permute (takeP (length cxt) $ mvPermutation mv) $
reverse $ zipWith const [0..] cxt ]
case [ i | (i, Dom{unDom = (_, El _ (Def q _))}) <- zip [(0::Int)..] cxt,
q == genRecName, elem i notPruned ] of
[] -> return ()
_:_:_ -> __IMPOSSIBLE__
[i] -> do
δ <- checkpointSubstitution cp
reportSDoc "tc.generalize.eta" 30 $ vcat
[ "eta expanding GenRec in"
, nest 2 $ prettyTCM (mvJudgement mv)
, nest 2 $ "GenRecTel is var" <+> pretty i ]
a <- case mvJudgement mv of
IsSort{} -> return Nothing
HasType{} -> Just <$> getMetaTypeInContext x
v <- MetaV x . map Apply <$> getMetaContextArgs mv
let σ = sub
let name = traverse $ \ (s, ty) -> (,ty) <$> freshName_ s
γ = composeS (strengthenS __IMPOSSIBLE__ i) δ
theta <- mapM name $ telToList $ buildGeneralizeTel genRecCon $ applySubst γ teleTypes
let ρ = liftS i σ
expand cxt = deltaRσ ++ thetaR ++ gammaR
where
(deltaR, _ : gammaR) = splitAt i cxt
thetaR = reverse theta
deltaRσ = go (length deltaR - 1) deltaR
where
go i (x : xs) = applySubst (liftS i σ) x : go (i - 1) xs
go _ [] = []
let ρinv = liftS i $ [ Var 0 [Proj ProjSystem fld] | fld <- reverse $ genRecFields ] ++# raiseS 1
reportSDoc "tc.generalize.eta" 50 $ nest 2 $ vcat
[ "ρ ∘ ρ⁻¹ =" <+> pretty (composeS ρ ρinv)
, "ρ⁻¹ ∘ ρ =" <+> pretty (composeS ρinv ρ) ]
speculateTCState_ $ updateContext ρ expand $ do
reportSDoc "tc.generalize.eta" 30 $ nest 2 $
"new context:" <+> (inTopContext . prettyTCM =<< getContextTelescope)
(y, u) <- localScope $ do
forM_ theta $ \ Dom{ unDom = (x, _) } -> do
reportSLn "tc.generalize.eta.scope" 40 $ "Adding (or not) " ++ show (nameConcrete x) ++ " to the scope"
when ('.' `notElem` show (nameConcrete x)) $ do
reportSLn "tc.generalize.eta.scope" 40 " (added)"
bindVariable LambdaBound (nameConcrete x) x
case a of
Nothing -> do
s@(MetaS y _) <- newSortMeta
return (y, Sort s)
Just a -> newNamedValueMeta DontRunMetaOccursCheck
(miNameSuggestion $ mvInfo mv)
(applySubst ρ a)
let MetaV _ es = applySubst ρ v
Just vs = allApplyElims es
reportSDoc "tc.generalize.eta" 30 $ nest 2 $
hsep ["assigning", prettyTCM (MetaV x es), ":=", prettyTCM u]
do assign DirEq x vs u
whenJust (Map.lookup x ips) (`connectInteractionPoint` y)
return SpeculateCommit
`catchError_` \ case
PatternErr{} -> do
reportSDoc "tc.generalize.eta" 20 $ nest 2 $
"Skipping eta expansion of blocked term meta" <+> pretty (MetaV x es)
return SpeculateAbort
err -> throwError err
return (genTel, telNames, sub)
unpackSub :: ConHead -> [ArgInfo] -> Int -> Substitution
unpackSub con infos i = recSub
where
ar = length infos
appl info v = Apply (Arg info v)
recVal = Con con ConOSystem $ zipWith appl infos $ [var j | j <- [i - 1, i - 2..0]] ++ replicate (ar - i) __DUMMY_TERM__
recSub = recVal :# Wk i IdS
buildGeneralizeTel :: ConHead -> [(Arg String, Type)] -> Telescope
buildGeneralizeTel con xs = go 0 xs
where
infos = map (argInfo . fst) xs
recSub i = unpackSub con infos i
go _ [] = EmptyTel
go i ((name, ty) : xs) = ExtendTel (dom ty') $ Abs (unArg name) $ go (i + 1) xs
where ty' = applySubst (recSub i) ty
dom = defaultNamedArgDom (getArgInfo name) (unArg name)
createGenValues :: Set QName -> TCM (Map MetaId QName, Map QName GeneralizedValue)
createGenValues s = do
genvals <- locallyTC eGeneralizeMetas (const YesGeneralize) $
forM (sortBy (compare `on` getRange) $ Set.toList s) createGenValue
let metaMap = Map.fromList [ (m, x) | (x, m, _) <- genvals ]
nameMap = Map.fromList [ (x, v) | (x, _, v) <- genvals ]
return (metaMap, nameMap)
createGenValue :: QName -> TCM (QName, MetaId, GeneralizedValue)
createGenValue x = do
cp <- viewTC eCurrentCheckpoint
def <- instantiateDef =<< getConstInfo x
let nGen = case defArgGeneralizable def of
NoGeneralizableArgs -> 0
SomeGeneralizableArgs n -> n
ty = defType def
TelV tel _ = telView' ty
hideExplicit arg | visible arg = hide arg
| otherwise = arg
argTel = telFromList $ map hideExplicit $ take nGen $ telToList tel
args <- newTelMeta argTel
let metaType = piApply ty args
name = show (nameConcrete $ qnameName x)
(m, term) <- newNamedValueMeta DontRunMetaOccursCheck name metaType
let fromJust' :: Lens' a (Maybe a)
fromJust' f (Just x) = Just <$> f x
fromJust' f Nothing = __IMPOSSIBLE__
stMetaStore . key m . fromJust' . metaFrozen `setTCLens` Frozen
forM_ (zip3 [1..] (map unArg args) (telToList argTel)) $ \ case
(i, MetaV m _, Dom{unDom = (x, _)}) -> do
let suf "_" = show i
suf "" = show i
suf x = x
setMetaNameSuggestion m (name ++ "." ++ suf x)
_ -> return ()
setMetaArgInfo m $ hideExplicit (defArgInfo def)
reportSDoc "tc.generalize" 50 $ vcat
[ "created metas for generalized variable" <+> prettyTCM x
, nest 2 $ "top =" <+> prettyTCM term
, nest 2 $ "args =" <+> prettyTCM args ]
case term of
MetaV{} -> return ()
_ -> genericDocError =<< ("Cannot generalize over" <+> prettyTCM x <+> "of eta-expandable type") <?>
prettyTCM metaType
return (x, m, GeneralizedValue{ genvalCheckpoint = cp
, genvalTerm = term
, genvalType = metaType })
sortMetas :: [MetaId] -> TCM [MetaId]
sortMetas metas = do
metaGraph <- fmap concat $ forM metas $ \ m -> do
deps <- nub . filter (`elem` metas) . allMetas <$> (instantiateFull =<< getMetaType m)
return [ (m, m') | m' <- deps ]
caseMaybe (Graph.topSort metas metaGraph)
(typeError GeneralizeCyclicDependency)
return
createGenRecordType :: Type -> [MetaId] -> TCM (QName, ConHead, [QName])
createGenRecordType genRecMeta@(El genRecSort _) sortedMetas = do
current <- currentModule
let freshQName s = qualify current <$> freshName_ (s :: String)
mkFieldName = freshQName . (generalizedFieldName ++) <=< getMetaNameSuggestion
genRecFields <- mapM (defaultArg <.> mkFieldName) sortedMetas
genRecName <- freshQName "GeneralizeTel"
genRecCon <- freshQName "mkGeneralizeTel" <&> \ con -> ConHead
{ conName = con
, conInductive = Inductive
, conFields = genRecFields }
forM_ (zip sortedMetas genRecFields) $ \ (meta, fld) -> do
fieldTy <- getMetaType meta
let field = unArg fld
addConstant field $ defaultDefn (argInfo fld) field fieldTy $
let proj = Projection { projProper = Just genRecName
, projOrig = field
, projFromType = defaultArg genRecName
, projIndex = 1
, projLams = ProjLams [defaultArg "gtel"] } in
Function { funClauses = []
, funCompiled = Nothing
, funTreeless = Nothing
, funInv = NotInjective
, funMutual = Just []
, funAbstr = ConcreteDef
, funDelayed = NotDelayed
, funProjection = Just proj
, funFlags = Set.empty
, funTerminates = Just True
, funExtLam = Nothing
, funWith = Nothing
, funCopatternLHS = False
}
addConstant (conName genRecCon) $ defaultDefn defaultArgInfo (conName genRecCon) __DUMMY_TYPE__ $
Constructor { conPars = 0
, conArity = length genRecFields
, conSrcCon = genRecCon
, conData = genRecName
, conAbstr = ConcreteDef
, conInd = Inductive
, conComp = (emptyCompKit, Nothing)
, conForced = []
, conErased = []
}
let dummyTel 0 = EmptyTel
dummyTel n = ExtendTel (defaultDom __DUMMY_TYPE__) $ Abs "_" $ dummyTel (n - 1)
addConstant genRecName $ defaultDefn defaultArgInfo genRecName (sort genRecSort) $
Record { recPars = 0
, recClause = Nothing
, recConHead = genRecCon
, recNamedCon = False
, recFields = genRecFields
, recTel = dummyTel (length genRecFields)
, recMutual = Just []
, recEtaEquality' = Inferred YesEta
, recInduction = Nothing
, recAbstr = ConcreteDef
, recComp = emptyCompKit }
reportSDoc "tc.generalize" 40 $ vcat
[ text "created genRec" <+> text (show genRecFields) ]
args <- getContextArgs
let genRecTy = El genRecSort $ Def genRecName $ map Apply args
noConstraints $ equalType genRecTy genRecMeta
return (genRecName, genRecCon, map unArg genRecFields)
fillInGenRecordDetails :: QName -> ConHead -> [QName] -> Type -> Telescope -> TCM ()
fillInGenRecordDetails name con fields recTy fieldTel = do
cxtTel <- fmap hideAndRelParams <$> getContextTelescope
let fullTel = cxtTel `abstract` fieldTel
let mkFieldTypes [] EmptyTel = []
mkFieldTypes (fld : flds) (ExtendTel ty ftel) =
abstract cxtTel (El s $ Pi (defaultDom recTy) (Abs "r" $ unDom ty)) :
mkFieldTypes flds (absApp ftel proj)
where
s = PiSort (getSort recTy) (Abs "r" $ getSort ty)
proj = Var 0 [Proj ProjSystem fld]
mkFieldTypes _ _ = __IMPOSSIBLE__
let fieldTypes = mkFieldTypes fields (raise 1 fieldTel)
reportSDoc "tc.generalize" 40 $ text "Field types:" <+> inTopContext (nest 2 $ vcat $ map prettyTCM fieldTypes)
zipWithM_ setType fields fieldTypes
let conType = fullTel `abstract` raise (size fieldTel) recTy
reportSDoc "tc.generalize" 40 $ text "Final genRecCon type:" <+> inTopContext (prettyTCM conType)
setType (conName con) conType
modifyGlobalDefinition name $ \ r ->
r { theDef = (theDef r) { recTel = fullTel } }
where
setType q ty = modifyGlobalDefinition q $ \ d -> d { defType = ty }