{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Generalize
( generalizeType
, generalizeType'
, generalizeTelescope ) where
import Control.Arrow ((***), first, second)
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 (nub, partition, init, sortBy)
import Data.Monoid
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.Internal.Generic
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.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.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Singleton
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, 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
mvs <- mapM ((\ x -> (x,) <$> lookupMeta x) . MetaId) $ IntSet.toList allmetas
constrainedMetas <- Set.unions <.> mapM (constraintMetas . clValue . theConstraint) =<<
((++) <$> useTC stAwakeConstraints
<*> useTC stSleepingConstraints)
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
case openSortMetas of
[] -> return ()
ms -> warning $ CantGeneralizeOverSorts (map fst ms)
cp <- viewTC eCurrentCheckpoint
let canGeneralize x | isConstrained x = return False
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 . 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 = (`Set.member` Set.fromList generalizeOver)
allSortedMetas <- sortMetas (generalizeOver ++ reallyDontGeneralize)
let sortedMetas = filter shouldGeneralize allSortedMetas
let dropCxt err = updateContext (strengthenS err 1) (drop 1)
(genRecName, genRecCon, genRecFields) <- dropCxt __IMPOSSIBLE__ $
createGenRecordType genRecMeta sortedMetas
cxtTel <- getContextTelescope
let solve m field = do
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
return [(Arg info $ miNameSuggestion $ mvInfo mv, piApply t args)]
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 (miClosRange $ mvInfo 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 (miClosRange $ mvInfo 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 (miClosRange $ mvInfo 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
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) _Aρ
setInteractionPoint x y =
whenJust (Map.lookup x interactionPoints) (`connectInteractionPoint` y)
doPrune :: MetaId -> MetaVariable -> Maybe Type -> Term -> Term -> TCM ()
doPrune x mv _A v u =
case _A of
_ | isOpen -> assign DirEq x (getArgs v) u
Nothing -> equalSort (unwrapSort v) (unwrapSort u)
Just _A -> equalTerm _A v u
where
isOpen = isOpenMeta $ mvInstantiation mv
getArgs v = case v of
Sort (MetaS _ es) -> unApply es
MetaV _ es -> unApply es
_ -> __IMPOSSIBLE__
where unApply es = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
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
let metaType = piApply ty args
name = show (nameConcrete $ qnameName x)
(m, term) <- newNamedValueMeta DontRunMetaOccursCheck name 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 })
sortMetas :: [MetaId] -> TCM [MetaId]
sortMetas metas = do
metaGraph <- concat <$> do
forM metas $ \ m -> do
deps <- allMetas (\ m' -> if m' `elem` metas then singleton m' else mempty) <$> getType m
return [ (m, m') | m' <- Set.toList deps ]
caseMaybe (Graph.topSort metas metaGraph)
(typeError GeneralizeCyclicDependency)
return
where
getType m = do
mv <- lookupMeta m
case mvJudgement mv of
IsSort{} -> return Nothing
HasType{ jMetaType = t } -> Just <$> instantiateFull t
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
, 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
, funCopatternLHS = False
, 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, 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 }