module Agda.TypeChecking.Generalize
( generalizeType
, generalizeType'
, generalizeTelescope ) where
import Prelude hiding (null)
import Control.Arrow (first)
import Control.Monad
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Data.List (partition, sortBy)
import Data.Monoid
import Data.Function (on)
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name (LensInScope(..))
import Agda.Syntax.Position
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Scope.Monad (bindVariable, outsideLocalVars)
import Agda.Syntax.Scope.Base (BindingSource(..))
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Free
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.List (hasElem)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Size
import Agda.Utils.Permutation
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 = Map.keysSet 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 __IMPOSSIBLE__ 1 (prettyTCM t') ]
return (genTelNames, t', userdata)
createMetasAndTypeCheck :: Set QName -> TCM a -> TCM (a, Map MetaId QName, IntSet)
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 -> IntSet -> TCM (Telescope, [Maybe name], Substitution)
computeGeneralization genRecMeta nameMap allmetas = postponeInstanceConstraints $ do
reportSDoc "tc.generalize" 10 $ "computing generalization for type" <+> prettyTCM genRecMeta
mvs <- mapM ((\ x -> (x,) <$> lookupMeta x) . MetaId) $ IntSet.toList allmetas
constrainedMetas <- Set.unions <.> mapM (constraintMetas . clValue . theConstraint) =<<
((++) <$> useTC stAwakeConstraints
<*> useTC stSleepingConstraints)
reportSDoc "tc.generalize" 30 $ nest 2 $
"constrainedMetas = " <+> prettyList_ (map prettyTCM $ Set.toList constrainedMetas)
let isConstrained x = Set.member x constrainedMetas
isGeneralizable (x, mv) = Map.member x nameMap ||
not (isConstrained x) && 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
reportSDoc "tc.generalize" 30 $ nest 2 $ vcat
[ "generalizable = " <+> prettyList_ (map (prettyTCM . fst) generalizable)
, "generalizableOpen = " <+> prettyList_ (map (prettyTCM . fst) generalizableOpen)
, "openSortMetas = " <+> prettyList_ (map (prettyTCM . fst) openSortMetas)
]
unlessNull openSortMetas $ \ ms ->
warning $ CantGeneralizeOverSorts $ map fst ms
cp <- viewTC eCurrentCheckpoint
let canGeneralize x | isConstrained x = return False
canGeneralize x = do
mv <- lookupMeta x
msub <- enterClosure 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 . allMetasList =<< 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
shouldGeneralize = (generalizeOver `hasElem`)
reportSDoc "tc.generalize" 30 $ nest 2 $ vcat
[ "alsoGeneralize = " <+> prettyList_ (map prettyTCM alsoGeneralize)
, "reallyDontGeneralize = " <+> prettyList_ (map prettyTCM reallyDontGeneralize)
]
reportSDoc "tc.generalize" 10 $ "we're generalizing over" <+> prettyList_ (map prettyTCM generalizeOver)
allSortedMetas <- fromMaybeM (typeError GeneralizeCyclicDependency) $
dependencySortMetas (generalizeOver ++ reallyDontGeneralize)
let sortedMetas = filter shouldGeneralize allSortedMetas
let dropCxt err = updateContext (strengthenS err 1) (drop 1)
(genRecName, genRecCon, genRecFields) <- dropCxt __IMPOSSIBLE__ $
createGenRecordType genRecMeta sortedMetas
reportSDoc "tc.generalize" 30 $ vcat $
[ "created genRecordType"
, nest 2 $ "genRecName = " <+> prettyTCM genRecName
, nest 2 $ "genRecCon = " <+> prettyTCM genRecCon
, nest 2 $ "genRecFields = " <+> prettyList_ (map prettyTCM genRecFields)
]
cxtTel <- getContextTelescope
let solve m field = do
reportSDoc "tc.generalize" 30 $ "solving generalized meta" <+>
prettyTCM m <+> ":=" <+> prettyTCM (Var 0 [Proj ProjSystem field])
whenM (isInstantiatedMeta m) __IMPOSSIBLE__
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
perm = mvPermutation mv
t' <- piApplyM t $ permute (takeP (length args) perm) args
return [(Arg info $ miNameSuggestion $ mvInfo mv, t')]
let genTel = buildGeneralizeTel genRecCon teleTypes
reportSDoc "tc.generalize" 40 $ vcat
[ text "genTel =" <+> prettyTCM genTel ]
let inscope (ii, InteractionPoint{ipMeta = Just x})
| IntSet.member (metaId x) allmetas = [(x, ii)]
inscope _ = []
ips <- Map.fromList . concatMap inscope . Map.toList <$> useTC stInteractionPoints
pruneUnsolvedMetas genRecName genRecCon genTel genRecFields ips shouldGeneralize allSortedMetas
dropCxt __IMPOSSIBLE__ $ fillInGenRecordDetails genRecName genRecCon genRecFields genRecMeta genTel
let sub = unpackSub genRecCon (map (argInfo . fst) teleTypes) (length teleTypes)
return (genTel, telNames, sub)
pruneUnsolvedMetas :: QName -> ConHead -> Telescope -> [QName] -> Map MetaId InteractionId -> (MetaId -> Bool) -> [MetaId] -> TCM ()
pruneUnsolvedMetas genRecName genRecCon genTel genRecFields interactionPoints isGeneralized metas
| all isGeneralized metas = return ()
| otherwise = prune [] genTel metas
where
prune _ _ [] = return ()
prune cxt tel (x : xs) | not (isGeneralized x) = do
whenM (not <$> isBlockedTerm x) $ do
x <- if size tel > 0 then prePrune x
else return x
pruneMeta (telFromList $ reverse cxt) x
prune cxt tel xs
prune cxt (ExtendTel a tel) (x : xs) = prune (fmap (x,) a : cxt) (unAbs tel) xs
where x = absName tel
prune _ _ _ = __IMPOSSIBLE__
sub = unpackSub genRecCon $ map getArgInfo $ telToList genTel
prepruneError :: MetaId -> String -> TCM a
prepruneError x code = do
r <- getMetaRange x
let msg = "Congratulations! You have found an easter egg (#" ++ code ++ "). " ++
"Be the first to submit a self-contained test case (max 50 lines of code) " ++
"producing this error message to https://github.com/agda/agda/issues/3672 " ++
"to receive a small prize."
cause = "The error is caused by complicated dependencies between unsolved " ++
"metavariables and generalized variables. In particular, this meta:"
genericDocError =<<
(fwords msg $+$
sep [fwords cause, nest 2 $ prettyTCM (MetaV x []) <+> "at" <+> pretty r]
)
prePrune x = do
cp <- viewTC eCurrentCheckpoint
mv <- lookupMeta x
(i, _A) <- enterClosure mv $ \ _ -> do
δ <- checkpointSubstitution cp
_A <- case mvJudgement mv of
IsSort{} -> return Nothing
HasType{} -> Just <$> getMetaTypeInContext x
case δ of
Wk n IdS -> return (n, _A)
IdS -> return (0, _A)
_ -> prepruneError x "RFCX"
if i == 0 then return x else do
reportSDoc "tc.generalize.prune.pre" 40 $ vcat
[ "prepruning"
, nest 2 $ pretty x <+> ":" <+> pretty (jMetaType $ mvJudgement mv)
, nest 2 $ "|Δ| =" <+> pshow i ]
case IntSet.minView (allFreeVars _A) of
Just (j, _) | j < i -> prepruneError x "FVTY"
_ -> return ()
let ρ = strengthenS __IMPOSSIBLE__ i
ρ' = raiseS i
(y, u) <- newMetaFromOld mv ρ _A
let uρ' = applySubst ρ' u
reportSDoc "tc.generalize.prune.pre" 40 $ nest 2 $ vcat
[ "u =" <+> pretty u
, "uρ⁻¹ =" <+> pretty uρ' ]
enterClosure mv $ \ _ -> do
v <- case _A of
Nothing -> Sort . MetaS x . map Apply <$> getMetaContextArgs mv
Just{} -> MetaV x . map Apply <$> getMetaContextArgs mv
noConstraints (doPrune x mv _A v uρ') `catchError` \ _ -> prepruneError x "INST"
setInteractionPoint x y
return y
pruneMeta _Θ x = do
cp <- viewTC eCurrentCheckpoint
mv <- lookupMeta x
enterClosure mv $ \ _ ->
whenJustM (findGenRec mv) $ \ i -> do
reportSDoc "tc.generalize.prune" 30 $ vcat
[ "pruning"
, nest 2 $ inTopContext $ prettyTCM (mvJudgement mv)
, nest 2 $ "GenRecTel is var" <+> pretty i ]
_ΓrΔ <- getContextTelescope
let (_Γ, _Δ) = (telFromList gs, telFromList ds)
where (gs, _ : ds) = splitAt (size _ΓrΔ - i - 1) (telToList _ΓrΔ)
_A <- case mvJudgement mv of
IsSort{} -> return Nothing
HasType{} -> Just <$> getMetaTypeInContext x
δ <- checkpointSubstitution cp
v <- case _A of
Nothing -> Sort . MetaS x . map Apply <$> getMetaContextArgs mv
Just{} -> MetaV x . map Apply <$> getMetaContextArgs mv
let σ = sub (size _Θ)
γ = strengthenS __IMPOSSIBLE__ (i + 1) `composeS` δ `composeS` raiseS 1
_Θγ = applySubst γ _Θ
_Δσ = applySubst σ _Δ
let ρ = liftS i σ
ρ' = liftS i $ [ Var 0 [Proj ProjSystem fld] | fld <- reverse $ take (size _Θ) $ genRecFields ] ++# raiseS 1
reportSDoc "tc.generalize.prune" 30 $ nest 2 $ vcat
[ "Γ =" <+> pretty _Γ
, "Θ =" <+> pretty _Θ
, "Δ =" <+> pretty _Δ
, "σ =" <+> pretty σ
, "γ =" <+> pretty γ
, "δ =" <+> pretty δ
, "ρ =" <+> pretty ρ
, "ρ⁻¹ =" <+> pretty ρ'
, "Θγ =" <+> pretty _Θγ
, "Δσ =" <+> pretty _Δσ
, "_A =" <+> pretty _A
]
(newCxt, rΘ) <- do
(rΔ, _ : rΓ) <- splitAt i <$> getContext
let setName = traverse $ \ (s, ty) -> (,ty) <$> freshName_ s
rΘ <- mapM setName $ reverse $ telToList _Θγ
let rΔσ = zipWith (\ name dom -> first (const name) <$> dom)
(map (fst . unDom) rΔ)
(reverse $ telToList _Δσ)
return (rΔσ ++ rΘ ++ rΓ, rΘ)
(y, u) <- updateContext ρ (const newCxt) $ localScope $ do
outsideLocalVars i $ addNamedVariablesToScope rΘ
newMetaFromOld mv ρ _A
let uρ' = applySubst ρ' u
reportSDoc "tc.generalize.prune" 80 $ vcat
[ "solving"
, nest 2 $ sep [ pretty v <+> "=="
, pretty uρ' <+> ":"
, pretty _A ] ]
noConstraints (doPrune x mv _A v uρ') `catchError` niceError x v
reportSDoc "tc.generalize.prune" 80 $ vcat
[ "solved"
, nest 2 $ "v =" <+> (pretty =<< instantiateFull v)
, nest 2 $ "uρ⁻¹ =" <+> (pretty =<< instantiateFull uρ') ]
setInteractionPoint x y
findGenRec :: MetaVariable -> TCM (Maybe Int)
findGenRec 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..] cxt,
q == genRecName, elem i notPruned ] of
[] -> return Nothing
_:_:_ -> __IMPOSSIBLE__
[i] -> return (Just i)
newMetaFromOld :: MetaVariable -> Substitution -> Maybe Type -> TCM (MetaId, Term)
newMetaFromOld mv ρ mA = setCurrentRange mv $
case mA of
Nothing -> do
s @ (MetaS y _) <- newSortMeta
return (y, Sort s)
Just _A -> do
let _Aρ = applySubst ρ _A
newNamedValueMeta DontRunMetaOccursCheck
(miNameSuggestion $ mvInfo mv)
(jComparison $ mvJudgement mv) _Aρ
setInteractionPoint x y =
whenJust (Map.lookup x interactionPoints) (`connectInteractionPoint` y)
doPrune :: MetaId -> MetaVariable -> Maybe Type -> Term -> Term -> TCM ()
doPrune x mv mt v u =
case mt of
_ | isOpen -> assign DirEq x (getArgs v) u $ maybe AsTypes AsTermsOf mt
Nothing -> equalSort (unwrapSort v) (unwrapSort u)
Just t -> equalTerm t v u
where
isOpen = isOpenMeta $ mvInstantiation mv
getArgs = \case
Sort (MetaS _ es) -> fromMaybe __IMPOSSIBLE__ $ allApplyElims es
MetaV _ es -> fromMaybe __IMPOSSIBLE__ $ allApplyElims es
_ -> __IMPOSSIBLE__
unwrapSort (Sort s) = s
unwrapSort _ = __IMPOSSIBLE__
niceError x u err = do
u <- instantiateFull u
let err' = case err of
TypeError{tcErrClosErr = cl} ->
err{ tcErrClosErr = cl{ clEnv = (clEnv cl) { envCall = Nothing } } }
_ -> err
telList = telToList genTel
names = map (fst . unDom) telList
late = map (fst . unDom) $ filter (getAny . allMetas (Any . (== x))) telList
projs (Proj _ q)
| elem q genRecFields = Set.fromList [x | Just x <- [getGeneralizedFieldName q]]
projs _ = Set.empty
early = Set.toList $ flip foldTerm u $ \ case
Var _ es -> foldMap projs es
Def _ es -> foldMap projs es
MetaV _ es -> foldMap projs es
_ -> Set.empty
commas [] = __IMPOSSIBLE__
commas [x] = x
commas [x, y] = x ++ ", and " ++ y
commas (x : xs) = x ++ ", " ++ commas xs
cause = "There were unsolved constraints that obscured the " ++
"dependencies between the generalized variables."
solution = "The most reliable solution is to provide enough information to make the dependencies " ++
"clear, but simply mentioning the variables in the right order should also work."
order = sep [ fwords "Dependency analysis suggested this (likely incorrect) order:",
nest 2 $ fwords (unwords names) ]
guess = "After constraint solving it looks like " ++ commas late ++ " actually depend" ++ s ++
" on " ++ commas early
where
s | length late == 1 = "s"
| otherwise = ""
genericDocError =<< vcat
[ fwords $ "Variable generalization failed."
, nest 2 $ sep ["- Probable cause", nest 4 $ fwords cause]
, nest 2 $ sep ["- Suggestion", nest 4 $ fwords solution]
, nest 2 $ sep $ ["- Further information"
, nest 2 $ "-" <+> order ] ++
[ nest 2 $ "-" <+> fwords guess | not (null late), not (null early) ] ++
[ nest 2 $ "-" <+> sep [ fwords "The dependency I error is", prettyTCM err' ] ]
]
addNamedVariablesToScope cxt =
forM_ cxt $ \ 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
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 = setCurrentRange 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
metaType <- piApplyM ty args
let name = show (nameConcrete $ qnameName x)
(m, term) <- newNamedValueMeta DontRunMetaOccursCheck name CmpLeq metaType
updateMetaVar m $ \ mv -> mv { mvFrozen = 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 })
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 (defaultDom <.> mkFieldName) sortedMetas
genRecName <- freshQName "GeneralizeTel"
genRecCon <- freshQName "mkGeneralizeTel" <&> \ con -> ConHead
{ conName = con
, conInductive = Inductive
, conFields = map argFromDom genRecFields }
projIx <- succ . size <$> getContext
inTopContext $ forM_ (zip sortedMetas genRecFields) $ \ (meta, fld) -> do
fieldTy <- getMetaType meta
let field = unDom fld
addConstant field $ defaultDefn (getArgInfo fld) field fieldTy $
let proj = Projection { projProper = Just genRecName
, projOrig = field
, projFromType = defaultArg genRecName
, projIndex = projIx
, projLams = ProjLams [defaultArg "gtel"] } in
Function { funClauses = []
, funCompiled = Nothing
, funSplitTree = Nothing
, funTreeless = Nothing
, funInv = NotInjective
, funMutual = Just []
, funAbstr = ConcreteDef
, funDelayed = NotDelayed
, funProjection = Just proj
, funFlags = Set.empty
, funTerminates = Just True
, funExtLam = Nothing
, funWith = Nothing
, funCovering = []
}
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
, conProj = Nothing
, conForced = []
, conErased = Nothing
}
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" 20 $ vcat
[ text "created genRec" <+> prettyList_ (map (text . show . unDom) genRecFields) ]
reportSDoc "tc.generalize" 80 $ 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 unDom 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 (defaultDom 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 }