{-# LANGUAGE CPP #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.Syntax.Translation.InternalToAbstract
( Reify(..)
, NamedClause(..)
, reifyPatterns
) where
import Prelude hiding (mapM_, mapM, null)
import Control.Arrow ((&&&))
import Control.Monad.State hiding (mapM_, mapM)
import Control.Monad.Reader 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 (Traversable, traverse, mapM)
import qualified Data.Traversable as Trav
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'(..), exprFieldA)
import Agda.Syntax.Info as Info
import 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 (isNameInScope, 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.TypeChecking.DropArgs
import Agda.Interaction.Options ( optPostfixProjections )
import Agda.Utils.Either
import Agda.Utils.Except ( MonadError(catchError) )
import Agda.Utils.Function
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 hiding ((<>))
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
napps :: Expr -> [NamedArg Expr] -> TCM Expr
napps e = nelims e . map I.Apply
apps :: Expr -> [Arg Expr] -> TCM Expr
apps e = elims e . map I.Apply
nelims :: Expr -> [I.Elim' (Named_ Expr)] -> TCM Expr
nelims e [] = return e
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 = nelimsProjPrefix e d es
| otherwise =
nelims (A.App defaultAppInfo_ e (defaultNamedArg $ A.Proj o $ unambiguous d)) es
nelimsProjPrefix :: Expr -> QName -> [I.Elim' (Named_ Expr)] -> TCM Expr
nelimsProjPrefix e d es =
nelims (A.App defaultAppInfo_ (A.Proj ProjPrefix $ unambiguous d) $ defaultNamedArg e) es
isSelf :: Expr -> Bool
isSelf = \case
A.Var x -> null $ prettyShow x
_ -> False
elims :: Expr -> [I.Elim' Expr] -> TCM Expr
elims e = nelims e . map (fmap unnamed)
noExprInfo :: ExprInfo
noExprInfo = ExprRange noRange
reifyWhenE :: Reify i Expr => Bool -> i -> TCM Expr
reifyWhenE True i = reify i
reifyWhenE False t = return underscore
class Reify i a | i -> a where
reify :: i -> TCM a
reifyWhen :: Bool -> i -> TCM a
reifyWhen _ = reify
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) = liftTCM $ do
b <- asks 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'
caseMaybeM (isInteractionMeta x) underscore $ \ ii@InteractionId{} ->
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 :: QName -> I.Elims -> TCM A.Expr -> TCM A.Expr
reifyDisplayForm f es fallback = do
ifNotM displayFormsEnabled fallback $ do
caseMaybeM (liftTCM $ displayForm f es) fallback reify
reifyDisplayFormP
:: QName
-> A.Patterns
-> A.Patterns
-> TCM (QName, A.Patterns)
reifyDisplayFormP f ps wps = do
let fallback = return (f, ps ++ wps)
ifNotM displayFormsEnabled fallback $ do
md <- liftTCM $
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
[ text "rewritten lhs to"
, text " 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.Apply v) = okDisplayTerm $ unArg v
okDElim I.Proj{} = True
okToDropE :: Elim' Term -> Bool
okToDropE (I.Apply v) = okToDrop v
okToDropE I.Proj{} = 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.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
:: A.Patterns
-> DisplayTerm
-> TCM (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 :: Arg DisplayTerm -> TCM (NamedArg A.Pattern)
argToPat arg = traverse termToPat arg
elimToPat :: I.Elim' DisplayTerm -> TCM (NamedArg A.Pattern)
elimToPat (I.Apply arg) = argToPat arg
elimToPat (I.Proj o d) = return $ defaultNamedArg $ A.ProjP patNoRange o $ unambiguous d
termToPat :: DisplayTerm -> TCM (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 False) (unambiguous (conName c)) <$> mapM argToPat vs
termToPat (DTerm (I.Con c ci vs)) = fmap unnamed <$> tryRecPFromConP =<< do
A.ConP (ConPatInfo ci patNoRange False) (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 (DDot v) = unnamed . A.DotP patNoRange <$> termToExpr v
termToPat v = unnamed . A.DotP patNoRange <$> reify v
len = length ps
argsToExpr :: I.Args -> TCM [Arg A.Expr]
argsToExpr = mapM (traverse termToExpr)
termToExpr :: Term -> TCM 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 $ 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
reifyTerm :: Bool -> Term -> TCM Expr
reifyTerm expandAnonDefs0 v = do
metasBare <- asks envPrintMetasBare
expandAnonDefs <- return expandAnonDefs0 `and2M` displayFormsEnabled
havePfp <- optPostfixProjections <$> pragmaOptions
let pred = if havePfp then (== ProjPrefix) else (/= ProjPostfix)
v <- instantiate v
case applyUnless metasBare (unSpine' pred) v of
I.Var n es -> do
x <- liftTCM $ nameOfBV n `catchError` \_ -> freshName_ ("@" ++ show n)
elims (A.Var x) =<< reify es
I.Def x es -> do
reportSLn "reify.def" 100 $ "reifying def " ++ prettyShow x
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 <- getRecordFieldNames r
vs <- map unArg <$> reify (fromMaybe __IMPOSSIBLE__ $ allApplyElims vs)
return $ A.Rec noExprInfo $ map (Left . uncurry FieldAssignment . mapFst unArg) $ 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 (fromMaybe __IMPOSSIBLE__ $ allApplyElims 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 info _ : _) | notVisible info -> do
let us = for (drop n pars) $ \ (Dom 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 (DomainFree info $ BindName 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
(x, b) <- reify b{ absName = unNotInScopeName $ absName b }
return $ A.Pi noExprInfo [TypedBindings noRange $ Arg info (TBind noRange [pure $ BindName x] a)] b
domainFree a b = do
df <- asks envPrintDomainFreePi
return $ and [df, freeIn 0 b, closed a]
I.Sort s -> reify s
I.MetaV x es -> do
x' <- reify x
ifM (asks envPrintMetasBare) (return x') $
elims x' =<< reify es
I.DontCare v -> A.DontCare <$> reifyTerm expandAnonDefs v
where
reifyDef :: Bool -> QName -> I.Elims -> TCM 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
reportSLn "reify.anon" 60 $ unlines
[ "reduction on defined ident. in anonymous module"
, "x = " ++ prettyShow x
, "v = " ++ show v
]
reify v
NoReduction () -> do
reportSLn "reify.anon" 60 $ unlines
[ "no reduction on defined ident. in anonymous module"
, "x = " ++ prettyShow x
, "es = " ++ show es
]
reifyDef' x es
reifyDef _ x es = reifyDef' x es
reifyDef' :: QName -> I.Elims -> TCM 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.DomainFree i $ A.BindName x)
foldr ($) absLam <$> mapM lam vars
| otherwise -> elims absLam =<< reify (drop n es)
_ -> do
df <- displayFormsEnabled
alreadyPrinting <- view ePrintingPatternLambdas
extLam <- case def of
Function{ funExtLam = Just{}, funProjection = Just{} } -> __IMPOSSIBLE__
Function{ funExtLam = Just (ExtLamInfo m) } -> Just . size <$> lookupSection m
_ -> return Nothing
case extLam of
Just pars | df, notElem x alreadyPrinting ->
locally ePrintingPatternLambdas (x :) $
reifyExtLam x pars (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 = fromMaybe __IMPOSSIBLE__ $ headMaybe rest
scope <- getScope
let underscore = A.Underscore $ Info.emptyMetaInfo { metaScope = scope }
let pad = for as $ \ (Dom ai (x, _)) ->
Arg ai $ Named (Just $ 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)) ==) . fmap rangedThing . nameOf . unArg) 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)
reportSLn "reify.def" 70 $ unlines
[ " pad = " ++ show pad
, " nes = " ++ show nes
]
let hd = List.foldl' (A.App defaultAppInfo_) (A.Def x) pad
nelims hd =<< reify nes
reifyExtLam :: QName -> Int -> [I.Clause] -> I.Elims -> TCM Expr
reifyExtLam x npars cls es = do
reportSLn "reify.def" 10 $ "reifying extended lambda " ++ prettyShow x
reportSLn "reify.def" 50 $ render $ nest 2 $ vcat
[ text "npars =" <+> pretty npars
, text "es =" <+> fsep (map (prettyPrec 10) es)
, text "def =" <+> vcat (map pretty cls) ]
let (pars, rest) = splitAt npars es
cls <- mapM (reify . NamedClause x False . (`applyE` pars)) cls
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 $ 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 = (<>)
stripImplicits :: A.Patterns -> TCM A.Patterns
stripImplicits ps = do
ifM showImplicitArguments (return $ map (unnamed . namedThing <$>) ps) $ do
reportSLn "reify.implicit" 30 $ unlines
[ "stripping implicits"
, " ps = " ++ show ps
]
let ps' = blankDots $ strip ps
reportSLn "reify.implicit" 30 $ unlines
[ " ps' = " ++ show ps'
]
return ps'
where
blankDots ps = blank (varsBoundIn 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 (unnamed . namedThing)
stripName False = id
canStrip a = and
[ notVisible a
, getOrigin a `notElem` [ UserWritten , CaseSplit ]
, varOrDot (namedArg a)
]
isUnnamedHidden x = notVisible x && nameOf (unArg x) == Nothing && 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.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) | patOrigin cpi == ConOSystem
= all varOrDot $ map namedArg ps
varOrDot _ = False
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 (A.Pattern' 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.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.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.QuoteGoal {} -> __IMPOSSIBLE__
A.QuoteContext {} -> __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 TypedBindings where
blank bound (TypedBindings r bs) = TypedBindings r $ blank bound bs
instance BlankVars TypedBinding where
blank bound (TBind r n e) = TBind r 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 -> singleton $ unBind 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.WithP _ _ -> empty
instance Binder A.LamBinding where
varsBoundIn (A.DomainFree _ x) = singleton $ unBind x
varsBoundIn (A.DomainFull b) = varsBoundIn b
instance Binder TypedBindings where
varsBoundIn (TypedBindings _ b) = varsBoundIn b
instance Binder TypedBinding where
varsBoundIn (TBind _ xs _) = varsBoundIn xs
varsBoundIn (TLet _ bs) = varsBoundIn bs
instance Binder LetBinding where
varsBoundIn (LetBind _ _ x _ _) = singleton $ unBind x
varsBoundIn (LetPatBind _ p _) = varsBoundIn p
varsBoundIn LetApply{} = empty
varsBoundIn LetOpen{} = empty
varsBoundIn LetDeclaredVariable{} = empty
instance Binder (WithHiding Name) where
varsBoundIn (WithHiding _ x) = singleton x
instance Binder (WithHiding BindName) where
varsBoundIn (WithHiding _ x) = singleton $ unBind x
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 b) => Binder (a, b) where
varsBoundIn (x, y) = varsBoundIn x `Set.union` varsBoundIn y
reifyPatterns :: MonadTCM tcm => [NamedArg I.DeBruijnPattern] -> tcm [NamedArg A.Pattern]
reifyPatterns = mapM $ stripNameFromExplicit <.> traverse (traverse reifyPat)
where
stripNameFromExplicit :: NamedArg p -> NamedArg p
stripNameFromExplicit a
| visible a = fmap (unnamed . namedThing) a
| otherwise = a
reifyPat :: MonadTCM tcm => I.DeBruijnPattern -> tcm A.Pattern
reifyPat p = do
liftTCM $ reportSLn "reify.pat" 80 $ "reifying pattern " ++ show p
case p of
I.VarP PatODot x -> reifyDotP $ var $ dbPatVarIndex x
I.VarP PatOWild _ -> return $ A.WildP patNoRange
I.VarP PatOAbsurd _ -> return $ A.AbsurdP patNoRange
I.VarP _ x -> reifyVarP x
I.DotP PatOWild _ -> return $ A.WildP patNoRange
I.DotP PatOAbsurd _ -> return $ A.AbsurdP patNoRange
I.DotP (PatOVar x) v@(I.Var i []) -> do
x' <- nameOfBV i
if nameConcrete x == nameConcrete x' then
return $ A.VarP (BindName x')
else
reifyDotP v
I.DotP o v -> reifyDotP v
I.LitP l -> return $ A.LitP l
I.ProjP o d -> return $ A.ProjP patNoRange o $ unambiguous d
I.ConP c cpi ps -> case conPRecord cpi of
Just PatOWild -> return $ A.WildP patNoRange
Just PatOAbsurd -> return $ A.AbsurdP patNoRange
_ -> reifyConP c cpi ps
reifyVarP :: MonadTCM tcm => DBPatVar -> tcm A.Pattern
reifyVarP x = do
n <- liftTCM $ nameOfBV $ dbPatVarIndex x
case dbPatVarName x of
"_" -> return $ A.VarP $ A.BindName n
y -> if prettyShow (nameConcrete n) == "()" then return $ A.VarP $ A.BindName n else
return $ A.VarP $ A.BindName n { nameConcrete = C.Name noRange [ C.Id y ] }
reifyDotP :: MonadTCM tcm => Term -> tcm A.Pattern
reifyDotP v = do
t <- liftTCM $ reify v
return $ A.DotP patNoRange t
reifyConP :: MonadTCM tcm
=> ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern]
-> tcm A.Pattern
reifyConP c cpi ps = do
tryRecPFromConP =<< do A.ConP ci (unambiguous (conName c)) <$> reifyPatterns ps
where
ci = ConPatInfo origin patNoRange False
origin = fromConPatternInfo cpi
tryRecPFromConP :: MonadTCM tcm => A.Pattern -> tcm A.Pattern
tryRecPFromConP p = do
let fallback = return p
case p of
A.ConP ci c ps -> do
caseMaybeM (liftTCM $ isRecordConstructor $ headAmbQ c) fallback $ \ (r, def) -> do
if recNamedCon def && patOrigin ci /= ConORec then fallback else do
fs <- liftTCM $ getRecordFieldNames r
unless (length fs == length ps) __IMPOSSIBLE__
return $ A.RecP patNoRange $ zipWith mkFA fs ps
where
mkFA ax nap = FieldAssignment (unArg 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
ps <- reifyPatterns $ namedClausePats cl
lhs <- uncurry (SpineLHS empty) <$> reifyDisplayFormP f ps []
lhs <- if not toDrop then return lhs else do
nfv <- (size <.> lookupSection =<< getDefModule f) `catchError` \_ -> return 0
return $ dropParams nfv lhs
lhs <- stripImps lhs
reportSLn "reify.clause" 60 $ "reifying NamedClause, lhs = " ++ show lhs
rhs <- caseMaybe (clauseBody cl) (return AbsurdRHS) $ \ e -> do
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
dropParams n (SpineLHS i f ps) = SpineLHS i f $ drop n ps
stripImps :: SpineLHS -> TCM SpineLHS
stripImps (SpineLHS i f ps) = SpineLHS i f <$> stripImplicits ps
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.Max []) -> return $ A.Set noExprInfo 0
I.Type (I.Max [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 -> return $ A.Prop noExprInfo
I.Inf -> A.Var <$> freshName_ ("Setω" :: String)
I.SizeUniv -> do
I.Def sizeU [] <- primSizeUniv
return $ A.Def sizeU
I.PiSort s1 s2 -> do
pis <- freshName_ ("piSort" :: String)
(e1,e2) <- reify (s1, I.Lam defaultArgInfo $ fmap Sort s2)
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
instance Reify Level Expr where
reifyWhen = reifyWhenE
reify l = ifM haveLevels (reify =<< reallyUnLevelView l) $ do
A.Var <$> freshName_ (".#Lacking_Level_Builtins#" :: String)
instance (Free i, Reify i a) => Reify (Abs i) (Name, a) where
reify (NoAbs x v) = (,) <$> freshName_ x <*> reify v
reify (Abs s v) = do
s <- return $ if isUnderscore s && 0 `freeIn` v then "z" else s
x <- 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
return $ TypedBindings r (Arg info (TBind r [pure $ BindName x] e)) : bs
instance Reify i a => Reify (Dom i) (Arg a) where
reify (Dom info 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