{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.Syntax.Translation.InternalToAbstract
( Reify(..)
, MonadReify
, NamedClause(..)
, reifyPatterns
, reifyUnblocked
, blankNotInScope
, reifyDisplayFormP
) where
import Prelude hiding (mapM_, mapM, null)
import Control.Arrow ((&&&))
import Control.Monad.State hiding (mapM_, mapM)
import Data.Foldable (Foldable, foldMap)
import qualified Data.List as List
import qualified Data.Map as Map
import Data.Maybe
import Data.Monoid ( Monoid, mempty, mappend )
import Data.Semigroup ( Semigroup, (<>) )
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (traverse, mapM)
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Concrete (FieldAssignment'(..))
import Agda.Syntax.Info as Info
import Agda.Syntax.Abstract as A hiding (Binder)
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pattern
import Agda.Syntax.Abstract.Pretty
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I
import Agda.Syntax.Scope.Base (inverseScopeLookupName)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Reduce
import {-# SOURCE #-} Agda.TypeChecking.Records
import Agda.TypeChecking.CompiledClause (CompiledClauses'(Fail))
import Agda.TypeChecking.DisplayForm
import Agda.TypeChecking.Level
import {-# SOURCE #-} Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Interaction.Options
import Agda.Utils.Either
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Impossible
reifyUnblocked :: Reify i a => i -> TCM a
reifyUnblocked t = locallyTCState stInstantiateBlocking (const True) $ reify t
apps :: MonadReify m => Expr -> [Arg Expr] -> m Expr
apps e = elims e . map I.Apply
nelims :: MonadReify m => Expr -> [I.Elim' (Named_ Expr)] -> m Expr
nelims e [] = return e
nelims e (I.IApply x y r : es) =
nelims (A.App defaultAppInfo_ e $ defaultArg r) es
nelims e (I.Apply arg : es) = do
arg <- reify arg
dontShowImp <- not <$> showImplicitArguments
let hd | notVisible arg && dontShowImp = e
| otherwise = A.App defaultAppInfo_ e arg
nelims hd es
nelims e (I.Proj ProjPrefix d : es) = nelimsProjPrefix e d es
nelims e (I.Proj o d : es) | isSelf e = nelims (A.Proj ProjPrefix $ unambiguous d) es
| otherwise =
nelims (A.App defaultAppInfo_ e (defaultNamedArg $ A.Proj o $ unambiguous d)) es
nelimsProjPrefix :: MonadReify m => Expr -> QName -> [I.Elim' (Named_ Expr)] -> m Expr
nelimsProjPrefix e d es =
nelims (A.App defaultAppInfo_ (A.Proj ProjPrefix $ unambiguous d) $ defaultNamedArg e) es
isSelf :: Expr -> Bool
isSelf = \case
A.Var n -> nameIsRecordName n
_ -> False
elims :: MonadReify m => Expr -> [I.Elim' Expr] -> m Expr
elims e = nelims e . map (fmap unnamed)
noExprInfo :: ExprInfo
noExprInfo = ExprRange noRange
reifyWhenE :: (Reify i Expr, MonadReify m) => Bool -> i -> m Expr
reifyWhenE True i = reify i
reifyWhenE False t = return underscore
type MonadReify m =
( MonadReduce m
, MonadAddContext m
, MonadInteractionPoints m
, MonadFresh NameId m
, HasConstInfo m
, HasOptions m
, HasBuiltins m
, MonadDebug m
)
class Reify i a | i -> a where
reify :: MonadReify m => i -> m a
reifyWhen :: MonadReify m => Bool -> i -> m a
reifyWhen _ = reify
instance Reify Bool Bool where
reify = return
instance Reify Name Name where
reify = return
instance Reify Expr Expr where
reifyWhen = reifyWhenE
reify = return
instance Reify MetaId Expr where
reifyWhen = reifyWhenE
reify x@(MetaId n) = do
b <- asksTC envPrintMetasBare
mi <- mvInfo <$> lookupMeta x
let mi' = Info.MetaInfo
{ metaRange = getRange $ miClosRange mi
, metaScope = clScope $ miClosRange mi
, metaNumber = if b then Nothing else Just x
, metaNameSuggestion = if b then "" else miNameSuggestion mi
}
underscore = return $ A.Underscore mi'
isInteractionMeta x >>= \case
Nothing | b -> do
ii <- registerInteractionPoint False noRange Nothing
connectInteractionPoint ii x
return $ A.QuestionMark mi' ii
Just ii | b -> underscore
Nothing -> underscore
Just ii -> return $ A.QuestionMark mi' ii
instance Reify DisplayTerm Expr where
reifyWhen = reifyWhenE
reify d = case d of
DTerm v -> reifyTerm False v
DDot v -> reify v
DCon c ci vs -> apps (A.Con (unambiguous (conName c))) =<< reify vs
DDef f es -> elims (A.Def f) =<< reify es
DWithApp u us es0 -> do
(e, es) <- reify (u, us)
elims (if null es then e else A.WithApp noExprInfo e es) =<< reify es0
reifyDisplayForm :: MonadReify m => QName -> I.Elims -> m A.Expr -> m A.Expr
reifyDisplayForm f es fallback =
ifNotM displayFormsEnabled fallback $
caseMaybeM (displayForm f es) fallback reify
reifyDisplayFormP
:: MonadReify m
=> QName
-> A.Patterns
-> A.Patterns
-> m (QName, A.Patterns)
reifyDisplayFormP f ps wps = do
let fallback = return (f, ps ++ wps)
ifNotM displayFormsEnabled fallback $ do
md <-
displayForm f $ zipWith (\ p i -> I.Apply $ p $> I.var i) ps [0..]
reportSLn "reify.display" 60 $
"display form of " ++ prettyShow f ++ " " ++ show ps ++ " " ++ show wps ++ ":\n " ++ show md
case md of
Just d | okDisplayForm d -> do
(f', ps', wps') <- displayLHS ps d
reportSDoc "reify.display" 70 $ do
doc <- prettyA $ SpineLHS empty f' (ps' ++ wps' ++ wps)
return $ vcat
[ "rewritten lhs to"
, " lhs' = " <+> doc
]
reifyDisplayFormP f' ps' (wps' ++ wps)
_ -> do
reportSLn "reify.display" 70 $ "display form absent or not valid as lhs"
fallback
where
okDisplayForm :: DisplayTerm -> Bool
okDisplayForm (DWithApp d ds es) =
okDisplayForm d && all okDisplayTerm ds && all okToDropE es
okDisplayForm (DTerm (I.Def f vs)) = all okElim vs
okDisplayForm (DDef f es) = all okDElim es
okDisplayForm DDot{} = False
okDisplayForm DCon{} = False
okDisplayForm DTerm{} = False
okDisplayTerm :: DisplayTerm -> Bool
okDisplayTerm (DTerm v) = okTerm v
okDisplayTerm DDot{} = True
okDisplayTerm DCon{} = True
okDisplayTerm DDef{} = False
okDisplayTerm _ = False
okDElim :: Elim' DisplayTerm -> Bool
okDElim (I.IApply x y r) = okDisplayTerm r
okDElim (I.Apply v) = okDisplayTerm $ unArg v
okDElim I.Proj{} = True
okToDropE :: Elim' Term -> Bool
okToDropE (I.Apply v) = okToDrop v
okToDropE I.Proj{} = False
okToDropE (I.IApply x y r) = False
okToDrop :: Arg I.Term -> Bool
okToDrop arg = notVisible arg && case unArg arg of
I.Var _ [] -> True
I.DontCare{} -> True
I.Level{} -> True
_ -> False
okArg :: Arg I.Term -> Bool
okArg = okTerm . unArg
okElim :: Elim' I.Term -> Bool
okElim (I.IApply x y r) = okTerm r
okElim (I.Apply a) = okArg a
okElim I.Proj{} = True
okTerm :: I.Term -> Bool
okTerm (I.Var _ []) = True
okTerm (I.Con c ci vs) = all okElim vs
okTerm (I.Def x []) = isNoName $ qnameToConcrete x
okTerm _ = False
flattenWith :: DisplayTerm -> (QName, [I.Elim' DisplayTerm], [I.Elim' DisplayTerm])
flattenWith (DWithApp d ds1 es2) =
let (f, es, ds0) = flattenWith d
in (f, es, ds0 ++ map (I.Apply . defaultArg) ds1 ++ map (fmap DTerm) es2)
flattenWith (DDef f es) = (f, es, [])
flattenWith (DTerm (I.Def f es)) = (f, map (fmap DTerm) es, [])
flattenWith _ = __IMPOSSIBLE__
displayLHS
:: MonadReify m
=> A.Patterns
-> DisplayTerm
-> m (QName, A.Patterns, A.Patterns)
displayLHS ps d = do
let (f, vs, es) = flattenWith d
ps <- mapM elimToPat vs
wps <- mapM (updateNamedArg (A.WithP empty) <.> elimToPat) es
return (f, ps, wps)
where
argToPat :: MonadReify m => Arg DisplayTerm -> m (NamedArg A.Pattern)
argToPat arg = traverse termToPat arg
elimToPat :: MonadReify m => I.Elim' DisplayTerm -> m (NamedArg A.Pattern)
elimToPat (I.IApply _ _ r) = argToPat (Arg defaultArgInfo r)
elimToPat (I.Apply arg) = argToPat arg
elimToPat (I.Proj o d) = return $ defaultNamedArg $ A.ProjP patNoRange o $ unambiguous d
termToPat :: MonadReify m => DisplayTerm -> m (Named_ A.Pattern)
termToPat (DTerm (I.Var n [])) = return $ unArg $ fromMaybe __IMPOSSIBLE__ $ ps !!! n
termToPat (DCon c ci vs) = fmap unnamed <$> tryRecPFromConP =<< do
A.ConP (ConPatInfo ci patNoRange ConPatEager) (unambiguous (conName c)) <$> mapM argToPat vs
termToPat (DTerm (I.Con c ci vs)) = fmap unnamed <$> tryRecPFromConP =<< do
A.ConP (ConPatInfo ci patNoRange ConPatEager) (unambiguous (conName c)) <$> mapM (elimToPat . fmap DTerm) vs
termToPat (DTerm (I.Def _ [])) = return $ unnamed $ A.WildP patNoRange
termToPat (DDef _ []) = return $ unnamed $ A.WildP patNoRange
termToPat (DTerm (I.Lit l)) = return $ unnamed $ A.LitP l
termToPat (DDot v) = unnamed . A.DotP patNoRange <$> termToExpr v
termToPat v = unnamed . A.DotP patNoRange <$> reify v
len = length ps
argsToExpr :: MonadReify m => I.Args -> m [Arg A.Expr]
argsToExpr = mapM (traverse termToExpr)
termToExpr :: MonadReify m => Term -> m A.Expr
termToExpr v = do
reportSLn "reify.display" 60 $ "termToExpr " ++ show v
case unSpine v of
I.Con c ci es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es
apps (A.Con (unambiguous (conName c))) =<< argsToExpr vs
I.Def f es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es
apps (A.Def f) =<< argsToExpr vs
I.Var n es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es
e <- if n < len
then return $ A.patternToExpr $ namedArg $ indexWithDefault __IMPOSSIBLE__ ps n
else reify (I.var (n - len))
apps e =<< argsToExpr vs
_ -> return underscore
instance Reify Literal Expr where
reifyWhen = reifyWhenE
reify l = return (A.Lit l)
instance Reify Term Expr where
reifyWhen = reifyWhenE
reify v = reifyTerm True v
reifyPathPConstAsPath :: MonadReify m => QName -> Elims -> m (QName, Elims)
reifyPathPConstAsPath x es@[I.Apply l, I.Apply t, I.Apply lhs, I.Apply rhs] = do
reportSLn "reify.def" 100 $ "reifying def path " ++ show (x,es)
mpath <- getBuiltinName' builtinPath
mpathp <- getBuiltinName' builtinPathP
let fallback = return (x,es)
case (,) <$> mpath <*> mpathp of
Just (path,pathp) | x == pathp -> do
let a = case unArg t of
I.Lam _ (NoAbs _ b) -> Just b
I.Lam _ (Abs _ b)
| not $ 0 `freeIn` b -> Just (strengthen __IMPOSSIBLE__ b)
_ -> Nothing
case a of
Just a -> return (path, [I.Apply l, I.Apply (setHiding Hidden $ defaultArg a), I.Apply lhs, I.Apply rhs])
Nothing -> fallback
_ -> fallback
reifyPathPConstAsPath x es = return (x,es)
reifyTerm :: MonadReify m => Bool -> Term -> m Expr
reifyTerm expandAnonDefs0 v0 = do
metasBare <- asksTC envPrintMetasBare
v <- instantiate v0 >>= \case
I.MetaV x _ | metasBare -> return $ I.MetaV x []
v -> return v
expandAnonDefs <- return expandAnonDefs0 `and2M` displayFormsEnabled
havePfp <- optPostfixProjections <$> pragmaOptions
let pred = if havePfp then (== ProjPrefix) else (/= ProjPostfix)
case unSpine' pred v of
_ | I.Var n (I.Proj _ p : es) <- v,
Just name <- getGeneralizedFieldName p -> do
let fakeName = (qnameName p) { nameConcrete = C.Name noRange C.InScope [C.Id name] }
elims (A.Var fakeName) =<< reify es
I.Var n es -> do
x <- fromMaybeM (freshName_ $ "@" ++ show n) $ nameOfBV' n
elims (A.Var x) =<< reify es
I.Def x es -> do
reportSLn "reify.def" 100 $ "reifying def " ++ prettyShow x
(x,es) <- reifyPathPConstAsPath x es
reifyDisplayForm x es $ reifyDef expandAnonDefs x es
I.Con c ci vs -> do
let x = conName c
isR <- isGeneratedRecordConstructor x
case isR || ci == ConORec of
True -> do
showImp <- showImplicitArguments
let keep (a, v) = showImp || visible a
r <- getConstructorData x
xs <- fromMaybe __IMPOSSIBLE__ <$> getRecordFieldNames_ r
vs <- map unArg <$> reify (fromMaybe __IMPOSSIBLE__ $ allApplyElims vs)
return $ A.Rec noExprInfo $ map (Left . uncurry FieldAssignment . mapFst unDom) $ filter keep $ zip xs vs
False -> reifyDisplayForm x vs $ do
def <- getConstInfo x
let Constructor{conPars = np} = theDef def
n <- getDefFreeVars x
when (n > np) __IMPOSSIBLE__
let h = A.Con (unambiguous x)
if null vs then return h else do
es <- reify (map (fromMaybe __IMPOSSIBLE__ . isApplyElim) vs)
if np == 0 then apps h es else do
TelV tel _ <- telView (defType def)
let (pars, rest) = splitAt np $ telToList tel
case rest of
(Dom {domInfo = info} : _) | notVisible info -> do
let us = for (drop n pars) $ \ (Dom {domInfo = ai}) ->
hideOrKeepInstance $ Arg ai underscore
apps h $ us ++ es
_ -> apps h es
I.Lam info b -> do
(x,e) <- reify b
return $ A.Lam exprNoRange (mkDomainFree $ unnamedArg info $ mkBinder_ x) e
I.Lit l -> reify l
I.Level l -> reify l
I.Pi a b -> case b of
NoAbs _ b'
| visible a -> uncurry (A.Fun $ noExprInfo) <$> reify (a, b')
| otherwise -> mkPi b =<< reify a
b -> mkPi b =<< do
ifM (domainFree a (absBody b))
(pure $ Arg (domInfo a) underscore)
(reify a)
where
mkPi b (Arg info a') = do
tac <- traverse reify $ domTactic a
(x, b) <- reify b
return $ A.Pi noExprInfo [TBind noRange tac [Arg info $ Named (domName a) $ mkBinder_ x] a'] b
domainFree a b = do
df <- asksTC envPrintDomainFreePi
return $ and [df, freeIn 0 b, closed a]
I.Sort s -> reify s
I.MetaV x es -> do
x' <- reify x
es' <- reify es
mv <- lookupMeta x
(msub1,meta_tel,msub2) <- do
local_chkpt <- viewTC eCurrentCheckpoint
(chkpt, tel, msub2) <- enterClosure mv $ \ _ ->
(,,) <$> viewTC eCurrentCheckpoint
<*> getContextTelescope
<*> viewTC (eCheckpoints . key local_chkpt)
(,,) <$> viewTC (eCheckpoints . key chkpt) <*> pure tel <*> pure msub2
let
addNames [] es = map (fmap unnamed) es
addNames _ [] = []
addNames xs (I.Proj{} : _) = __IMPOSSIBLE__
addNames xs (I.IApply x y r : es) =
addNames xs (I.Apply (defaultArg r) : es)
addNames (x:xs) (I.Apply arg : es) =
I.Apply (Named (Just x) <$> (setOrigin Substitution arg)) : addNames xs es
p = mvPermutation mv
applyPerm p vs = permute (takeP (size vs) p) vs
names = map (WithOrigin Inserted . unranged) $ p `applyPerm` teleNames meta_tel
named_es' = addNames names es'
dropIdentitySubs sub_local2G sub_tel2G =
let
args_G = applySubst sub_tel2G $ p `applyPerm` (teleArgs meta_tel :: [Arg Term])
es_G = sub_local2G `applySubst` es
sameVar x (I.Apply y) = isJust xv && xv == deBruijnView (unArg y)
where
xv = deBruijnView $ unArg x
sameVar _ _ = False
dropArg = take (size names) $ zipWith sameVar args_G es_G
doDrop (b : xs) (e : es) = (if b then id else (e :)) $ doDrop xs es
doDrop [] es = es
doDrop _ [] = []
in doDrop dropArg $ named_es'
simpl_named_es' | Just sub_mtel2local <- msub1 = dropIdentitySubs IdS sub_mtel2local
| Just sub_local2mtel <- msub2 = dropIdentitySubs sub_local2mtel IdS
| otherwise = named_es'
nelims x' simpl_named_es'
I.DontCare v -> do
showIrr <- optShowIrrelevant <$> pragmaOptions
if | showIrr -> reifyTerm expandAnonDefs v
| otherwise -> return underscore
I.Dummy s [] -> return $ A.Lit $ LitString noRange s
I.Dummy "applyE" es | I.Apply (Arg _ h) : es' <- es -> do
h <- reify h
es' <- reify es'
elims h es'
| otherwise -> __IMPOSSIBLE__
I.Dummy s es -> do
s <- reify (I.Dummy s [])
es <- reify es
elims s es
where
reifyDef :: MonadReify m => Bool -> QName -> I.Elims -> m Expr
reifyDef True x es =
ifM (not . null . inverseScopeLookupName x <$> getScope) (reifyDef' x es) $ do
r <- reduceDefCopy x es
case r of
YesReduction _ v -> do
reportS "reify.anon" 60
[ "reduction on defined ident. in anonymous module"
, "x = " ++ prettyShow x
, "v = " ++ show v
]
reify v
NoReduction () -> do
reportS "reify.anon" 60
[ "no reduction on defined ident. in anonymous module"
, "x = " ++ prettyShow x
, "es = " ++ show es
]
reifyDef' x es
reifyDef _ x es = reifyDef' x es
reifyDef' :: MonadReify m => QName -> I.Elims -> m Expr
reifyDef' x es = do
reportSLn "reify.def" 60 $ "reifying call to " ++ prettyShow x
n <- getDefFreeVars x
reportSLn "reify.def" 70 $ "freeVars for " ++ prettyShow x ++ " = " ++ show n
let fallback _ = elims (A.Def x) =<< reify (drop n es)
caseEitherM (getConstInfo' x) fallback $ \ defn -> do
let def = theDef defn
case def of
Function{ funCompiled = Just Fail, funClauses = [cl] }
| isAbsurdLambdaName x -> do
let h = getHiding $ last $ namedClausePats cl
n = length (namedClausePats cl) - 1
absLam = A.AbsurdLam exprNoRange h
if | n > length es -> do
let name (I.VarP _ x) = patVarNameToString $ dbPatVarName x
name _ = __IMPOSSIBLE__
vars = map (getArgInfo &&& name . namedArg) $ drop (length es) $ init $ namedClausePats cl
lam (i, s) = do
x <- freshName_ s
return $ A.Lam exprNoRange (A.mkDomainFree $ unnamedArg i $ A.mkBinder_ x)
foldr ($) absLam <$> mapM lam vars
| otherwise -> elims absLam =<< reify (drop n es)
_ -> do
df <- displayFormsEnabled
alreadyPrinting <- viewTC ePrintingPatternLambdas
extLam <- case def of
Function{ funExtLam = Just{}, funProjection = Just{} } -> __IMPOSSIBLE__
Function{ funExtLam = Just (ExtLamInfo m sys) } -> Just . (,sys) . size <$> lookupSection m
_ -> return Nothing
case extLam of
Just (pars, sys) | df, notElem x alreadyPrinting ->
locallyTC ePrintingPatternLambdas (x :) $
reifyExtLam x pars sys (defClauses defn) es
_ -> do
(pad, nes :: [Elim' (Named_ Term)]) <- case def of
Function{ funProjection = Just Projection{ projIndex = np } } | np > 0 -> do
reportSLn "reify.def" 70 $ " def. is a projection with projIndex = " ++ show np
TelV tel _ <- telViewUpTo np (defType defn)
let (as, rest) = splitAt (np - 1) $ telToList tel
dom = headWithDefault __IMPOSSIBLE__ rest
scope <- getScope
let underscore = A.Underscore $ Info.emptyMetaInfo { metaScope = scope }
let pad :: [NamedArg Expr]
pad = for as $ \ (Dom{domInfo = ai, unDom = (x, _)}) ->
Arg ai $ Named (Just $ WithOrigin Inserted $ unranged x) underscore
let pad' = drop n pad
es' = drop (max 0 (n - size pad)) es
showImp <- showImplicitArguments
let (padVisNamed, padRest) = filterAndRest visible pad'
let padVis = map (fmap $ unnamed . namedThing) padVisNamed
let padTail = filter (sameHiding dom) padRest
let padSame = filter ((Just (fst $ unDom dom) ==) . bareNameOf) padTail
return $ if null padTail || not showImp
then (padVis , map (fmap unnamed) es')
else (padVis ++ padSame, nameFirstIfHidden dom es')
_ -> return ([], map (fmap unnamed) $ drop n es)
reportS "reify.def" 70
[ " pad = " ++ show pad
, " nes = " ++ show nes
]
let hd0 | isProperProjection def = A.Proj ProjPrefix $ AmbQ $ singleton x
| otherwise = A.Def x
let hd = List.foldl' (A.App defaultAppInfo_) hd0 pad
nelims hd =<< reify nes
reifyExtLam :: MonadReify m => QName -> Int -> Maybe System -> [I.Clause] -> I.Elims -> m Expr
reifyExtLam x npars msys cls es = do
reportSLn "reify.def" 10 $ "reifying extended lambda " ++ prettyShow x
reportSLn "reify.def" 50 $ render $ nest 2 $ vcat
[ "npars =" <+> pretty npars
, "es =" <+> fsep (map (prettyPrec 10) es)
, "def =" <+> vcat (map pretty cls) ]
let (pares, rest) = splitAt npars es
let pars = fromMaybe __IMPOSSIBLE__ $ allApplyElims pares
cls <- caseMaybe msys
(mapM (reify . NamedClause x False . (`apply` pars)) cls)
(reify . QNamed x . (`apply` pars))
let cx = nameConcrete $ qnameName x
dInfo = mkDefInfo cx noFixity' PublicAccess ConcreteDef (getRange x)
elims (A.ExtendedLam exprNoRange dInfo x cls) =<< reify rest
nameFirstIfHidden :: Dom (ArgName, t) -> [Elim' a] -> [Elim' (Named_ a)]
nameFirstIfHidden dom (I.Apply (Arg info e) : es) | notVisible info =
I.Apply (Arg info (Named (Just $ WithOrigin Inserted $ unranged $ fst $ unDom dom) e)) :
map (fmap unnamed) es
nameFirstIfHidden _ es =
map (fmap unnamed) es
instance Reify i a => Reify (Named n i) (Named n a) where
reify = traverse reify
reifyWhen b = traverse (reifyWhen b)
instance (Reify i a) => Reify (Arg i) (Arg a) where
reify (Arg info i) = Arg info <$> (flip reifyWhen i =<< condition)
where condition = (return (argInfoHiding info /= Hidden) `or2M` showImplicitArguments)
`and2M` (return (getRelevance info /= Irrelevant) `or2M` showIrrelevantArguments)
reifyWhen b i = traverse (reifyWhen b) i
data NamedClause = NamedClause QName Bool I.Clause
newtype MonoidMap k v = MonoidMap { _unMonoidMap :: Map.Map k v }
instance (Ord k, Monoid v) => Semigroup (MonoidMap k v) where
MonoidMap m1 <> MonoidMap m2 = MonoidMap (Map.unionWith mappend m1 m2)
instance (Ord k, Monoid v) => Monoid (MonoidMap k v) where
mempty = MonoidMap Map.empty
mappend = (<>)
removeNameUnlessUserWritten :: (LensNamed n a, LensOrigin n) => a -> a
removeNameUnlessUserWritten a
| (getOrigin <$> getNameOf a) == Just UserWritten = a
| otherwise = setNameOf Nothing a
stripImplicits :: MonadReify m => A.Patterns -> A.Patterns -> m A.Patterns
stripImplicits params ps = do
ifM showImplicitArguments (return $ map (fmap removeNameUnlessUserWritten) ps) $ do
reportS "reify.implicit" 30
[ "stripping implicits"
, " ps = " ++ show ps
]
let ps' = blankDots $ strip ps
reportS "reify.implicit" 30
[ " ps' = " ++ show ps'
]
return ps'
where
blankDots ps = blank (varsBoundIn $ params ++ ps) ps
strip ps = stripArgs True ps
where
stripArgs _ [] = []
stripArgs fixedPos (a : as)
| canStrip a =
if all canStrip $ takeWhile isUnnamedHidden as
then stripArgs False as
else goWild
| otherwise = stripName fixedPos (stripArg a) : stripArgs True as
where
a' = setNamedArg a $ A.WildP $ Info.PatRange $ getRange a
goWild = stripName fixedPos a' : stripArgs True as
stripName True = fmap removeNameUnlessUserWritten
stripName False = id
canStrip a = and
[ notVisible a
, getOrigin a `notElem` [ UserWritten , CaseSplit ]
, (getOrigin <$> getNameOf a) /= Just UserWritten
, varOrDot (namedArg a)
]
isUnnamedHidden x = notVisible x && isNothing (getNameOf x) && isNothing (isProjP x)
stripArg a = fmap (fmap stripPat) a
stripPat p = case p of
A.VarP _ -> p
A.ConP i c ps -> A.ConP i c $ stripArgs True ps
A.ProjP{} -> p
A.DefP _ _ _ -> p
A.DotP _ e -> p
A.WildP _ -> p
A.AbsurdP _ -> p
A.LitP _ -> p
A.AsP i x p -> A.AsP i x $ stripPat p
A.PatternSynP _ _ _ -> __IMPOSSIBLE__
A.RecP i fs -> A.RecP i $ map (fmap stripPat) fs
A.EqualP{} -> p
A.WithP i p -> A.WithP i $ stripPat p
varOrDot A.VarP{} = True
varOrDot A.WildP{} = True
varOrDot A.DotP{} = True
varOrDot (A.ConP cpi _ ps) | conPatOrigin cpi == ConOSystem
= conPatLazy cpi == ConPatLazy || all (varOrDot . namedArg) ps
varOrDot _ = False
blankNotInScope :: (MonadTCEnv m, BlankVars a) => a -> m a
blankNotInScope e = do
names <- Set.fromList . filter ((== C.InScope) . C.isInScope) <$> getContextNames
return $ blank names e
class BlankVars a where
blank :: Set Name -> a -> a
default blank :: (Functor f, BlankVars b, f b ~ a) => Set Name -> a -> a
blank = fmap . blank
instance BlankVars a => BlankVars (Arg a) where
instance BlankVars a => BlankVars (Named s a) where
instance BlankVars a => BlankVars [a] where
instance BlankVars a => BlankVars (FieldAssignment' a) where
instance (BlankVars a, BlankVars b) => BlankVars (a, b) where
blank bound (x, y) = (blank bound x, blank bound y)
instance (BlankVars a, BlankVars b) => BlankVars (Either a b) where
blank bound (Left x) = Left $ blank bound x
blank bound (Right y) = Right $ blank bound y
instance BlankVars A.ProblemEq where
blank bound = id
instance BlankVars A.Clause where
blank bound (A.Clause lhs strippedPats rhs (A.WhereDecls _ []) ca) =
let bound' = varsBoundIn lhs `Set.union` bound
in A.Clause (blank bound' lhs)
(blank bound' strippedPats)
(blank bound' rhs) noWhereDecls ca
blank bound (A.Clause lhs strippedPats rhs _ ca) = __IMPOSSIBLE__
instance BlankVars A.LHS where
blank bound (A.LHS i core) = A.LHS i $ blank bound core
instance BlankVars A.LHSCore where
blank bound (A.LHSHead f ps) = A.LHSHead f $ blank bound ps
blank bound (A.LHSProj p b ps) = uncurry (A.LHSProj p) $ blank bound (b, ps)
blank bound (A.LHSWith h wps ps) = uncurry (uncurry A.LHSWith) $ blank bound ((h, wps), ps)
instance BlankVars A.Pattern where
blank bound p = case p of
A.VarP _ -> p
A.ConP c i ps -> A.ConP c i $ blank bound ps
A.ProjP{} -> p
A.DefP i f ps -> A.DefP i f $ blank bound ps
A.DotP i e -> A.DotP i $ blank bound e
A.WildP _ -> p
A.AbsurdP _ -> p
A.LitP _ -> p
A.AsP i n p -> A.AsP i n $ blank bound p
A.PatternSynP _ _ _ -> __IMPOSSIBLE__
A.RecP i fs -> A.RecP i $ blank bound fs
A.EqualP{} -> p
A.WithP i p -> A.WithP i (blank bound p)
instance BlankVars A.Expr where
blank bound e = case e of
A.ScopedExpr i e -> A.ScopedExpr i $ blank bound e
A.Var x -> if x `Set.member` bound then e
else A.Underscore emptyMetaInfo
A.Def _ -> e
A.Proj{} -> e
A.Con _ -> e
A.Lit _ -> e
A.QuestionMark{} -> e
A.Underscore _ -> e
A.Dot i e -> A.Dot i $ blank bound e
A.App i e1 e2 -> uncurry (A.App i) $ blank bound (e1, e2)
A.WithApp i e es -> uncurry (A.WithApp i) $ blank bound (e, es)
A.Lam i b e -> let bound' = varsBoundIn b `Set.union` bound
in A.Lam i (blank bound b) (blank bound' e)
A.AbsurdLam _ _ -> e
A.ExtendedLam i d f cs -> A.ExtendedLam i d f $ blank bound cs
A.Pi i tel e -> let bound' = varsBoundIn tel `Set.union` bound
in uncurry (A.Pi i) $ blank bound' (tel, e)
A.Generalized {} -> __IMPOSSIBLE__
A.Fun i a b -> uncurry (A.Fun i) $ blank bound (a, b)
A.Set _ _ -> e
A.Prop _ _ -> e
A.Let _ _ _ -> __IMPOSSIBLE__
A.Rec i es -> A.Rec i $ blank bound es
A.RecUpdate i e es -> uncurry (A.RecUpdate i) $ blank bound (e, es)
A.ETel _ -> __IMPOSSIBLE__
A.Quote {} -> __IMPOSSIBLE__
A.QuoteTerm {} -> __IMPOSSIBLE__
A.Unquote {} -> __IMPOSSIBLE__
A.Tactic {} -> __IMPOSSIBLE__
A.DontCare v -> A.DontCare $ blank bound v
A.PatternSyn {} -> e
A.Macro {} -> e
instance BlankVars A.ModuleName where
blank bound = id
instance BlankVars RHS where
blank bound (RHS e mc) = RHS (blank bound e) mc
blank bound AbsurdRHS = AbsurdRHS
blank bound (WithRHS _ es clauses) = __IMPOSSIBLE__
blank bound (RewriteRHS xes spats rhs _) = __IMPOSSIBLE__
instance BlankVars A.LamBinding where
blank bound b@A.DomainFree{} = b
blank bound (A.DomainFull bs) = A.DomainFull $ blank bound bs
instance BlankVars TypedBinding where
blank bound (TBind r t n e) = TBind r t n $ blank bound e
blank bound (TLet _ _) = __IMPOSSIBLE__
class Binder a where
varsBoundIn :: a -> Set Name
default varsBoundIn :: (Foldable f, Binder b, f b ~ a) => a -> Set Name
varsBoundIn = foldMap varsBoundIn
instance Binder A.LHS where
varsBoundIn (A.LHS _ core) = varsBoundIn core
instance Binder A.LHSCore where
varsBoundIn (A.LHSHead _ ps) = varsBoundIn ps
varsBoundIn (A.LHSProj _ b ps) = varsBoundIn (b, ps)
varsBoundIn (A.LHSWith h wps ps) = varsBoundIn ((h, wps), ps)
instance Binder A.Pattern where
varsBoundIn = foldAPattern $ \case
A.VarP x -> varsBoundIn x
A.AsP _ x _ -> empty
A.ConP _ _ _ -> empty
A.ProjP{} -> empty
A.DefP _ _ _ -> empty
A.WildP{} -> empty
A.DotP{} -> empty
A.AbsurdP{} -> empty
A.LitP{} -> empty
A.PatternSynP _ _ _ -> empty
A.RecP _ _ -> empty
A.EqualP{} -> empty
A.WithP _ _ -> empty
instance Binder a => Binder (A.Binder' a) where
varsBoundIn (A.Binder p n) = varsBoundIn (p, n)
instance Binder A.LamBinding where
varsBoundIn (A.DomainFree _ x) = varsBoundIn x
varsBoundIn (A.DomainFull b) = varsBoundIn b
instance Binder TypedBinding where
varsBoundIn (TBind _ _ xs _) = varsBoundIn xs
varsBoundIn (TLet _ bs) = varsBoundIn bs
instance Binder BindName where
varsBoundIn x = singleton (unBind x)
instance Binder LetBinding where
varsBoundIn (LetBind _ _ x _ _) = varsBoundIn x
varsBoundIn (LetPatBind _ p _) = varsBoundIn p
varsBoundIn LetApply{} = empty
varsBoundIn LetOpen{} = empty
varsBoundIn LetDeclaredVariable{} = empty
instance Binder a => Binder (FieldAssignment' a) where
instance Binder a => Binder (Arg a) where
instance Binder a => Binder (Named x a) where
instance Binder a => Binder [a] where
instance Binder a => Binder (Maybe a) where
instance (Binder a, Binder b) => Binder (a, b) where
varsBoundIn (x, y) = varsBoundIn x `Set.union` varsBoundIn y
reifyPatterns :: MonadReify m => [NamedArg I.DeBruijnPattern] -> m [NamedArg A.Pattern]
reifyPatterns = mapM $ (stripNameFromExplicit . stripHidingFromPostfixProj) <.>
traverse (traverse reifyPat)
where
stripNameFromExplicit :: NamedArg p -> NamedArg p
stripNameFromExplicit a
| visible a = fmap (unnamed . namedThing) a
| otherwise = a
stripHidingFromPostfixProj :: IsProjP p => NamedArg p -> NamedArg p
stripHidingFromPostfixProj a = case isProjP a of
Just (o, _) | o /= ProjPrefix -> setHiding NotHidden a
_ -> a
reifyPat :: MonadReify m => I.DeBruijnPattern -> m A.Pattern
reifyPat p = do
reportSLn "reify.pat" 80 $ "reifying pattern " ++ show p
keepVars <- optKeepPatternVariables <$> pragmaOptions
case p of
p | Just (PatternInfo PatOLit asB) <- patternInfo p -> do
reduce (I.patternToTerm p) >>= \case
I.Lit l -> addAsBindings asB $ return $ A.LitP l
_ -> __IMPOSSIBLE__
I.VarP i x -> addAsBindings (patAsNames i) $ case patOrigin i of
o@PatODot -> reifyDotP o $ var $ dbPatVarIndex x
PatOWild -> return $ A.WildP patNoRange
PatOAbsurd -> return $ A.AbsurdP patNoRange
_ -> reifyVarP x
I.DotP i v -> addAsBindings (patAsNames i) $ case patOrigin i of
PatOWild -> return $ A.WildP patNoRange
PatOAbsurd -> return $ A.AbsurdP patNoRange
o@(PatOVar x) | I.Var i [] <- v -> do
x' <- nameOfBV i
if nameConcrete x == nameConcrete x' then
return $ A.VarP $ mkBindName x'
else
reifyDotP o v
o -> reifyDotP o v
I.LitP i l -> addAsBindings (patAsNames i) $ return $ A.LitP l
I.ProjP o d -> return $ A.ProjP patNoRange o $ unambiguous d
I.ConP c cpi ps | conPRecord cpi -> addAsBindings (patAsNames $ conPInfo cpi) $
case patOrigin (conPInfo cpi) of
PatOWild -> return $ A.WildP patNoRange
PatOAbsurd -> return $ A.AbsurdP patNoRange
PatOVar x | keepVars -> return $ A.VarP $ mkBindName x
_ -> reifyConP c cpi ps
I.ConP c cpi ps -> addAsBindings (patAsNames $ conPInfo cpi) $ reifyConP c cpi ps
I.DefP i f ps -> addAsBindings (patAsNames i) $ case patOrigin i of
PatOWild -> return $ A.WildP patNoRange
PatOAbsurd -> return $ A.AbsurdP patNoRange
PatOVar x | keepVars -> return $ A.VarP $ mkBindName x
_ -> A.DefP patNoRange (unambiguous f) <$> reifyPatterns ps
I.IApplyP i _ _ x -> addAsBindings (patAsNames i) $ case patOrigin i of
o@PatODot -> reifyDotP o $ var $ dbPatVarIndex x
PatOWild -> return $ A.WildP patNoRange
PatOAbsurd -> return $ A.AbsurdP patNoRange
_ -> reifyVarP x
reifyVarP :: MonadReify m => DBPatVar -> m A.Pattern
reifyVarP x = do
n <- nameOfBV $ dbPatVarIndex x
let y = dbPatVarName x
if | y == "_" -> return $ A.VarP $ mkBindName n
| prettyShow (nameConcrete n) == "()" -> return $ A.VarP (mkBindName n)
| otherwise -> return $ A.VarP $
mkBindName n { nameConcrete = C.Name noRange C.InScope [ C.Id y ] }
reifyDotP :: MonadReify m => PatOrigin -> Term -> m A.Pattern
reifyDotP o v = do
keepVars <- optKeepPatternVariables <$> pragmaOptions
if | PatOVar x <- o
, keepVars -> return $ A.VarP $ mkBindName x
| otherwise -> A.DotP patNoRange <$> reify v
reifyConP :: MonadReify m
=> ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern]
-> m A.Pattern
reifyConP c cpi ps = do
tryRecPFromConP =<< do A.ConP ci (unambiguous (conName c)) <$> reifyPatterns ps
where
ci = ConPatInfo origin patNoRange lazy
lazy | conPLazy cpi = ConPatLazy
| otherwise = ConPatEager
origin = fromConPatternInfo cpi
addAsBindings :: Functor m => [A.Name] -> m A.Pattern -> m A.Pattern
addAsBindings xs p = foldr (fmap . AsP patNoRange . mkBindName) p xs
tryRecPFromConP :: MonadReify m => A.Pattern -> m A.Pattern
tryRecPFromConP p = do
let fallback = return p
case p of
A.ConP ci c ps -> do
caseMaybeM (isRecordConstructor $ headAmbQ c) fallback $ \ (r, def) -> do
if recNamedCon def && conPatOrigin ci /= ConORec then fallback else do
fs <- fromMaybe __IMPOSSIBLE__ <$> getRecordFieldNames_ r
unless (length fs == length ps) __IMPOSSIBLE__
return $ A.RecP patNoRange $ zipWith mkFA fs ps
where
mkFA ax nap = FieldAssignment (unDom ax) (namedArg nap)
_ -> __IMPOSSIBLE__
instance Reify (QNamed I.Clause) A.Clause where
reify (QNamed f cl) = reify (NamedClause f True cl)
instance Reify NamedClause A.Clause where
reify (NamedClause f toDrop cl) = addContext (clauseTel cl) $ do
reportSLn "reify.clause" 60 $ "reifying NamedClause"
++ "\n f = " ++ prettyShow f
++ "\n toDrop = " ++ show toDrop
++ "\n cl = " ++ show cl
let ell = clauseEllipsis cl
ps <- reifyPatterns $ namedClausePats cl
lhs <- uncurry (SpineLHS $ empty { lhsEllipsis = ell }) <$> reifyDisplayFormP f ps []
(params , lhs) <- if not toDrop then return ([] , lhs) else do
nfv <- getDefModule f >>= \case
Left _ -> return 0
Right m -> size <$> lookupSection m
return $ splitParams nfv lhs
lhs <- stripImps params lhs
reportSLn "reify.clause" 60 $ "reifying NamedClause, lhs = " ++ show lhs
rhs <- caseMaybe (clauseBody cl) (return AbsurdRHS) $ \ e ->
RHS <$> reify e <*> pure Nothing
reportSLn "reify.clause" 60 $ "reifying NamedClause, rhs = " ++ show rhs
let result = A.Clause (spineToLhs lhs) [] rhs A.noWhereDecls (I.clauseCatchall cl)
reportSLn "reify.clause" 60 $ "reified NamedClause, result = " ++ show result
return result
where
splitParams n (SpineLHS i f ps) =
let (params , pats) = splitAt n ps
in (params , SpineLHS i f pats)
stripImps :: MonadReify m => [NamedArg A.Pattern] -> SpineLHS -> m SpineLHS
stripImps params (SpineLHS i f ps) = SpineLHS i f <$> stripImplicits params ps
instance Reify (QNamed System) [A.Clause] where
reify (QNamed f (System tel sys)) = addContext tel $ do
reportS "reify.system" 40 $ show tel : map show sys
view <- intervalView'
unview <- intervalUnview'
sys <- flip filterM sys $ \ (phi,t) -> do
allM phi $ \ (u,b) -> do
u <- reduce u
return $ case (view u, b) of
(IZero, True) -> False
(IOne, False) -> False
_ -> True
forM sys $ \ (alpha,u) -> do
rhs <- RHS <$> reify u <*> pure Nothing
ep <- fmap (A.EqualP patNoRange) . forM alpha $ \ (phi,b) -> do
let
d True = unview IOne
d False = unview IZero
reify (phi, d b)
ps <- reifyPatterns $ teleNamedArgs tel
ps <- stripImplicits [] $ ps ++ [defaultNamedArg ep]
let
lhs = SpineLHS empty f ps
result = A.Clause (spineToLhs lhs) [] rhs A.noWhereDecls False
return result
instance Reify Type Expr where
reifyWhen = reifyWhenE
reify (I.El _ t) = reify t
instance Reify Sort Expr where
reifyWhen = reifyWhenE
reify s = do
s <- instantiateFull s
case s of
I.Type (I.ClosedLevel n) -> return $ A.Set noExprInfo n
I.Type a -> do
a <- reify a
return $ A.App defaultAppInfo_ (A.Set noExprInfo 0) (defaultNamedArg a)
I.Prop (I.ClosedLevel n) -> return $ A.Prop noExprInfo n
I.Prop a -> do
a <- reify a
return $ A.App defaultAppInfo_ (A.Prop noExprInfo 0) (defaultNamedArg a)
I.Inf -> do
I.Def inf [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSetOmega
return $ A.Def inf
I.SizeUniv -> do
I.Def sizeU [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSizeUniv
return $ A.Def sizeU
I.PiSort a s -> do
pis <- freshName_ ("piSort" :: String)
(e1,e2) <- reify (getSort a, I.Lam defaultArgInfo $ fmap Sort s)
let app x y = A.App defaultAppInfo_ x (defaultNamedArg y)
return $ A.Var pis `app` e1 `app` e2
I.UnivSort s -> do
univs <- freshName_ ("univSort" :: String)
e <- reify s
return $ A.App defaultAppInfo_ (A.Var univs) $ defaultNamedArg e
I.MetaS x es -> reify $ I.MetaV x es
I.DefS d es -> reify $ I.Def d es
I.DummyS s -> return $ A.Lit $ LitString noRange s
instance Reify Level Expr where
reifyWhen = reifyWhenE
reify l = ifM haveLevels (reify =<< reallyUnLevelView l) $ do
name <- freshName_ (".#Lacking_Level_Builtins#" :: String)
return $ A.Var name
instance (Free i, Reify i a) => Reify (Abs i) (Name, a) where
reify (NoAbs x v) = freshName_ x >>= \name -> (name,) <$> reify v
reify (Abs s v) = do
s <- return $ if isUnderscore s && 0 `freeIn` v then "z" else s
x <- C.setNotInScope <$> freshName_ s
e <- addContext x
$ reify v
return (x,e)
instance Reify I.Telescope A.Telescope where
reify EmptyTel = return []
reify (ExtendTel arg tel) = do
Arg info e <- reify arg
(x, bs) <- reify tel
let r = getRange e
name = domName arg
tac <- traverse reify $ domTactic arg
return $ TBind r tac [Arg info $ Named name $ A.mkBinder_ x] e : bs
instance Reify i a => Reify (Dom i) (Arg a) where
reify (Dom{domInfo = info, unDom = i}) = Arg info <$> reify i
instance Reify i a => Reify (I.Elim' i) (I.Elim' a) where
reify = traverse reify
reifyWhen b = traverse (reifyWhen b)
instance Reify i a => Reify [i] [a] where
reify = traverse reify
reifyWhen b = traverse (reifyWhen b)
instance (Reify i1 a1, Reify i2 a2) => Reify (i1,i2) (a1,a2) where
reify (x,y) = (,) <$> reify x <*> reify y
instance (Reify i1 a1, Reify i2 a2, Reify i3 a3) => Reify (i1,i2,i3) (a1,a2,a3) where
reify (x,y,z) = (,,) <$> reify x <*> reify y <*> reify z
instance (Reify i1 a1, Reify i2 a2, Reify i3 a3, Reify i4 a4) => Reify (i1,i2,i3,i4) (a1,a2,a3,a4) where
reify (x,y,z,w) = (,,,) <$> reify x <*> reify y <*> reify z <*> reify w