module Agda.Syntax.Translation.InternalToAbstract
( Reify(..)
, NamedClause
, reifyPatterns
) where
import Prelude hiding (mapM_, mapM)
import Control.Applicative
import Control.Monad.State hiding (mapM_, mapM)
import Control.Monad.Reader hiding (mapM_, mapM)
import Data.Foldable (foldMap)
import Data.List hiding (sort)
import qualified Data.Map as Map
import Data.Maybe
import Data.Monoid
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable as Trav
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Concrete (FieldAssignment'(..), exprFieldA)
import Agda.Syntax.Info as Info
import Agda.Syntax.Abstract as A
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 as M hiding (MetaInfo, tick)
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Records
import Agda.TypeChecking.CompiledClause (CompiledClauses(Fail))
import Agda.TypeChecking.DisplayForm
import Agda.TypeChecking.Level
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.DropArgs
import Agda.Utils.Except ( MonadError(catchError) )
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
napps :: Expr -> [NamedArg Expr] -> TCM Expr
napps e args = do
dontShowImp <- not <$> showImplicitArguments
let apply1 e arg | notVisible arg && dontShowImp = e
| otherwise = App exprInfo e arg
foldl' apply1 e <$> reify args
apps :: Expr -> [Arg Expr] -> TCM Expr
apps e args = napps e $ map (fmap unnamed) args
reifyApp :: Expr -> [Arg Term] -> TCM Expr
reifyApp e vs = apps e =<< reifyIArgs vs
reifyIArg :: Reify i a => Arg i -> TCM (Arg a)
reifyIArg i = Arg (argInfo i) <$> reify (unArg i)
reifyIArgs :: Reify i a => [Arg i] -> TCM [Arg a]
reifyIArgs = mapM reifyIArg
elims :: Expr -> [I.Elim' Expr] -> TCM Expr
elims e [] = return e
elims e (I.Apply arg : es) =
elims (A.App exprInfo e $ fmap unnamed arg) es
elims e (I.Proj d : es) = elims (A.App exprInfo (A.Proj d) $ defaultNamedArg e) es
reifyIElim :: Reify i a => I.Elim' i -> TCM (I.Elim' a)
reifyIElim (I.Apply i) = I.Apply <$> traverse reify i
reifyIElim (I.Proj d) = return $ I.Proj d
reifyIElims :: Reify i a => [I.Elim' i] -> TCM [I.Elim' a]
reifyIElims = mapM reifyIElim
exprInfo :: ExprInfo
exprInfo = 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
mi <- mvInfo <$> lookupMeta x
let mi' = Info.MetaInfo
{ metaRange = getRange $ miClosRange mi
, metaScope = M.clScope $ miClosRange mi
, metaNumber = Just x
, metaNameSuggestion = miNameSuggestion mi
}
underscore = return $ A.Underscore mi'
ifNotM shouldReifyInteractionPoints underscore $
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 vs -> apps (A.Con (AmbQ [conName c])) =<< reifyIArgs vs
DDef f es -> elims (A.Def f) =<< reifyIElims es
DWithApp u us vs -> do
(e, es) <- reify (u, us)
reifyApp (if null es then e else A.WithApp exprInfo e es) vs
reifyDisplayForm :: QName -> I.Args -> TCM A.Expr -> TCM A.Expr
reifyDisplayForm f vs fallback = do
ifNotM displayFormsEnabled fallback $ do
caseMaybeM (liftTCM $ displayForm f vs) fallback reify
reifyDisplayFormP :: A.SpineLHS -> TCM A.SpineLHS
reifyDisplayFormP lhs@(A.SpineLHS i f ps wps) =
ifNotM displayFormsEnabled (return lhs) $ do
let vs = [ setHiding h $ defaultArg $ I.var i
| (i, h) <- zip [0..] $ map getHiding ps
]
md <- liftTCM $
displayForm f vs
reportSLn "reify.display" 60 $
"display form of " ++ show f ++ " " ++ show ps ++ " " ++ show wps ++ ":\n " ++ show md
case md of
Just d | okDisplayForm d -> do
lhs' <- displayLHS (map namedArg ps) wps d
reportSDoc "reify.display" 70 $ do
doc <- prettyA lhs'
return $ vcat
[ text "rewritten lhs to"
, text " lhs' = " <+> doc
]
reifyDisplayFormP lhs'
_ -> do
reportSLn "reify.display" 70 $ "display form absent or not valid as lhs"
return lhs
where
okDisplayForm (DWithApp d ds args) =
okDisplayForm d && all okDisplayTerm ds && all okToDrop args
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 (DTerm v) = okTerm v
okDisplayTerm DDot{} = True
okDisplayTerm DCon{} = True
okDisplayTerm DDef{} = False
okDisplayTerm _ = False
okDElim (I.Apply v) = okDisplayTerm $ unArg v
okDElim I.Proj{} = True
okToDrop arg = notVisible arg && case ignoreSharing $ unArg arg of
I.Var _ [] -> True
I.DontCare{} -> True
I.Level{} -> True
_ -> False
okArg = okTerm . unArg
okElim (I.Apply a) = okArg a
okElim (I.Proj{}) = True
okTerm (I.Var _ []) = True
okTerm (I.Con c vs) = all okArg vs
okTerm (I.Def x []) = isNoName $ qnameToConcrete x
okTerm _ = False
flattenWith :: DisplayTerm -> (QName, [I.Elim' DisplayTerm], [DisplayTerm])
flattenWith (DWithApp d ds1 ds2) = case flattenWith d of
(f, es, ds0) -> (f, es, ds0 ++ ds1 ++ map (DTerm . unArg) ds2)
flattenWith (DDef f es) = (f, es, [])
flattenWith (DTerm (I.Def f es)) = (f, map (fmap DTerm) es, [])
flattenWith _ = __IMPOSSIBLE__
displayLHS :: [A.Pattern] -> [A.Pattern] -> DisplayTerm -> TCM A.SpineLHS
displayLHS ps wps d = case flattenWith d of
(f, vs, ds) -> do
ds <- mapM termToPat ds
vs <- mapM elimToPat vs
return $ SpineLHS i f vs (ds ++ wps)
where
ci = ConPatInfo ConPCon patNoRange
argToPat arg = fmap unnamed <$> traverse termToPat arg
elimToPat (I.Apply arg) = argToPat arg
elimToPat (I.Proj d) = return $ defaultNamedArg $ A.DefP patNoRange d []
termToPat :: DisplayTerm -> TCM A.Pattern
termToPat (DTerm (I.Var n [])) = return $ case ps !!! n of
Nothing -> __IMPOSSIBLE__
Just p -> p
termToPat (DCon c vs) = tryRecPFromConP =<< do
A.ConP ci (AmbQ [conName c]) <$> mapM argToPat vs
termToPat (DTerm (I.Con c vs)) = tryRecPFromConP =<< do
A.ConP ci (AmbQ [conName c]) <$> mapM (argToPat . fmap DTerm) vs
termToPat (DTerm (I.Def _ [])) = return $ A.WildP patNoRange
termToPat (DDef _ []) = return $ A.WildP patNoRange
termToPat (DDot v) = A.DotP patNoRange <$> termToExpr v
termToPat v = A.DotP patNoRange <$> reify v
len = genericLength ps
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 vs ->
apps (A.Con (AmbQ [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 $ 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
expandAnonDefs <- return expandAnonDefs0 `and2M` displayFormsEnabled
v <- unSpine <$> instantiate v
case v of
I.Var n es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
x <- liftTCM $ nameOfBV n `catchError` \_ -> freshName_ ("@" ++ show n)
reifyApp (A.Var x) vs
I.Def x es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
reifyDisplayForm x vs $ reifyDef expandAnonDefs x vs
I.Con c vs -> do
let x = conName c
isR <- isGeneratedRecordConstructor x
case isR of
True -> do
showImp <- showImplicitArguments
let keep (a, v) = showImp || notHidden a
r <- getConstructorData x
xs <- getRecordFieldNames r
vs <- map unArg <$> reifyIArgs vs
return $ A.Rec exprInfo $ map (Left . uncurry FieldAssignment . mapFst unArg) $ filter keep $ zip xs vs
False -> reifyDisplayForm x vs $ do
ci <- getConstInfo x
let Constructor{conPars = np} = theDef ci
n <- getDefFreeVars x
when (n > np) __IMPOSSIBLE__
let h = A.Con (AmbQ [x])
if null vs then return h else do
es <- reifyIArgs vs
if np == 0 then apps h es else do
TelV tel _ <- telView (defType ci)
case genericDrop np $ telToList tel of
(Dom info _ : _) | isHidden info -> do
let us = genericReplicate (np n) $
setRelevance Relevant $ Arg info underscore
apps h $ us ++ es
_ -> apps h es
I.Lam info b -> do
(x,e) <- reify b
return $ A.Lam exprInfo (DomainFree info x) e
I.Lit l -> reify l
I.Level l -> reify l
I.Pi a b -> case b of
NoAbs _ b'
| notHidden a -> uncurry (A.Fun $ exprInfo) <$> 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
return $ A.Pi exprInfo [TypedBindings noRange $ Arg info (TBind noRange [pure 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
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
x' <- reify x
apps x' =<< reifyIArgs vs
I.DontCare v -> A.DontCare <$> reifyTerm expandAnonDefs v
I.Shared p -> reifyTerm expandAnonDefs $ derefPtr p
where
reifyDef :: Bool -> QName -> I.Args -> TCM Expr
reifyDef True x vs =
ifM (not . null . inverseScopeLookupName x <$> getScope) (reifyDef' x vs) $ do
r <- reduceDefCopy x vs
case r of
YesReduction _ v -> do
reportSLn "reify.anon" 60 $ unlines
[ "reduction on defined ident. in anonymous module"
, "x = " ++ show x
, "v = " ++ show v
]
reify v
NoReduction () -> do
reportSLn "reify.anon" 60 $ unlines
[ "no reduction on defined ident. in anonymous module"
, "x = " ++ show x
, "vs = " ++ show vs
]
reifyDef' x vs
reifyDef _ x vs = reifyDef' x vs
reifyDef' :: QName -> I.Args -> TCM Expr
reifyDef' x@(QName _ name) vs = do
n <- getDefFreeVars x
mdefn <- liftTCM $ (Just <$> getConstInfo x) `catchError` \_ -> return Nothing
let reifyAbsurdLambda cont =
case theDef <$> mdefn of
Just Function{ funCompiled = Just Fail, funClauses = [cl] }
| isAbsurdLambdaName x -> do
let h = getHiding $ last (clausePats cl)
apps (A.AbsurdLam exprInfo h) =<< reifyIArgs vs
_ -> cont
reifyAbsurdLambda $ do
(pad, vs :: [NamedArg Term]) <- do
case mdefn of
Nothing -> return ([], map (fmap unnamed) $ genericDrop n vs)
Just defn -> do
let def = theDef defn
(np, pad, dom) <-
case def of
Function{ funProjection = Just Projection{ projIndex = np } } | np > 0 -> do
TelV tel _ <- telView (defType defn)
scope <- getScope
let (as, dom:_) = splitAt (np 1) $ telToList tel
whocares = A.Underscore $ Info.emptyMetaInfo { metaScope = scope }
return (np, map (argFromDom . (fmap $ const whocares)) as, dom)
_ -> return (0, [], __IMPOSSIBLE__)
let pad' = genericDrop n pad
vs' = genericDrop (max 0 (n size pad)) vs
showImp <- showImplicitArguments
return (filter visible pad',
if not (null pad) && showImp && notVisible (last pad)
then nameFirstIfHidden [dom] vs'
else map (fmap unnamed) vs')
df <- displayFormsEnabled
let extLam = case mdefn of
Nothing -> Nothing
Just defn -> case theDef defn of
Function{ funExtLam = Just (ExtLamInfo h nh) } -> Just (h + nh)
_ -> Nothing
case extLam of
Just pars | df -> do
info <- getConstInfo x
reifyExtLam x pars (defClauses info) vs
_ -> do
let apps = foldl' (\e a -> A.App exprInfo e (fmap unnamed a))
napps (A.Def x `apps` pad) =<< reifyIArgs vs
reifyExtLam :: QName -> Int -> [I.Clause] -> [NamedArg Term] -> TCM Expr
reifyExtLam x n cls vs = do
reportSLn "reify.def" 10 $ "reifying extended lambda with definition: x = " ++ show x
cls <- mapM (reify . QNamed x . dropArgs n) $ cls
let cx = nameConcrete $ qnameName x
dInfo = mkDefInfo cx noFixity' PublicAccess ConcreteDef (getRange x)
napps (A.ExtendedLam exprInfo dInfo x cls) =<< reifyIArgs vs
nameFirstIfHidden :: [Dom (ArgName, t)] -> [Arg a] -> [NamedArg a]
nameFirstIfHidden _ [] = []
nameFirstIfHidden [] (_ : _) = __IMPOSSIBLE__
nameFirstIfHidden (dom : _) (Arg info e : es) | isHidden info =
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 (argInfoRelevance info /= Irrelevant) `or2M` showIrrelevantArguments)
reifyWhen b i = traverse (reifyWhen b) i
instance Reify Elim Expr where
reifyWhen = reifyWhenE
reify e = case e of
I.Apply v -> appl "apply" <$> reify v
I.Proj f -> appl "proj" <$> reify ((defaultArg $ I.Def f []) :: Arg Term)
where
appl :: String -> Arg Expr -> Expr
appl s v = A.App exprInfo (A.Lit (LitString noRange s)) $ fmap unnamed v
type NamedClause = QNamed I.Clause
instance Reify ClauseBody RHS where
reify NoBody = return AbsurdRHS
reify (Body v) = RHS <$> reify v
reify (Bind b) = reify $ absBody b
data DotBind = BindFirstExplicit | BindFirstImplicit | AlreadyBound deriving (Show)
data DoBind = YesBind | NoBind | DontTouch deriving (Eq, Show)
newtype MonoidMap k v = MonoidMap { unMonoidMap :: Map.Map k v }
instance (Ord k, Monoid v) => Monoid (MonoidMap k v) where
mempty = MonoidMap Map.empty
mappend (MonoidMap m1) (MonoidMap m2) = MonoidMap (Map.unionWith mappend m1 m2)
shuffleDots :: ([NamedArg A.Pattern], [A.Pattern]) -> TCM ([NamedArg A.Pattern], [A.Pattern])
shuffleDots (ps, wps) = do
return $ (`evalState` xs)
$ (`runReaderT` NotHidden)
$ (,) <$> redotArgs ps <*> redotPats wps
where
implicit = All False
explicit = All True
xs = Map.map (\(_, h) -> if getAny h then BindFirstExplicit else BindFirstImplicit)
$ Map.filter (getAny . fst)
$ unMonoidMap
$ argsVars explicit ps `mappend` foldMap (patVars explicit) wps
argsVars h = foldMap (argVars h)
argVars h a = (foldMap $ foldMap $ patVars (h `mappend` h')) a
where h' = if getHiding a == NotHidden then explicit else implicit
patVars h p = case p of
A.VarP x -> MonoidMap $ Map.singleton x (Any False, Any $ getAll h)
A.DotP _ (A.Var x) -> MonoidMap $ Map.singleton x (Any True, Any $ getAll h)
A.DotP{} -> mempty
A.ConP _ _ ps -> argsVars h ps
A.DefP _ _ ps -> argsVars h ps
A.PatternSynP _ _ ps -> argsVars h ps
A.WildP{} -> mempty
A.AbsurdP{} -> mempty
A.LitP{} -> mempty
A.AsP{} -> __IMPOSSIBLE__
A.RecP _ as -> foldMap (foldMap (patVars h)) as
shouldBind x = do
xs <- get
h <- ask
let b = case Map.lookup x xs of
Nothing -> DontTouch
Just s -> case s of
BindFirstExplicit | h == NotHidden -> YesBind
| otherwise -> NoBind
BindFirstImplicit -> YesBind
AlreadyBound -> NoBind
when (b == YesBind) $ put $ Map.adjust (const AlreadyBound) x xs
return b
redotArgs = traverse redotArg
redotArg a = hide $ traverse (traverse redotPat) a
where hide | getHiding a /= NotHidden = local (const Hidden)
| otherwise = id
redotPats = traverse redotPat
redotPat p = case p of
A.VarP x -> redotVar p x
A.DotP _ (A.Var x) -> redotVar p x
A.DotP{} -> pure p
A.ConP i c ps -> A.ConP i c <$> redotArgs ps
A.DefP i f ps -> A.DefP i f <$> redotArgs ps
A.PatternSynP i x ps -> A.PatternSynP i x <$> redotArgs ps
A.WildP{} -> pure p
A.AbsurdP{} -> pure p
A.LitP{} -> pure p
A.AsP{} -> __IMPOSSIBLE__
A.RecP i as -> A.RecP i <$> traverse (traverse redotPat) as
redotVar p x = do
b <- shouldBind x
return $ case b of
DontTouch -> p
YesBind -> A.VarP x
NoBind -> A.DotP (Info.PatRange $ getRange p) (A.Var x)
stripImplicits :: ([NamedArg A.Pattern], [A.Pattern]) ->
TCM ([NamedArg A.Pattern], [A.Pattern])
stripImplicits (ps, wps) = do
ifM showImplicitArguments (return (map (unnamed . namedThing <$>) ps, wps)) $ do
let vars = dotVars (ps, wps)
reportSLn "reify.implicit" 30 $ unlines
[ "stripping implicits"
, " ps = " ++ show ps
, " wps = " ++ show wps
, " vars = " ++ show vars
]
let allps = ps ++ map defaultNamedArg wps
sps = blankDots $ foldl (.) (strip Set.empty) (map rearrangeBinding $ Set.toList vars) $ allps
(ps', wps') = splitAt (length sps length wps) sps
reportSLn "reify.implicit" 30 $ unlines
[ " ps' = " ++ show ps'
, " wps' = " ++ show (map namedArg wps')
]
return (ps', map namedArg wps')
where
argsVars = Set.unions . map argVars
argVars = patVars . namedArg
patVars p = case p of
A.VarP x -> Set.singleton x
A.ConP _ _ ps -> argsVars ps
A.DefP _ _ ps -> Set.empty
A.DotP _ e -> Set.empty
A.WildP _ -> Set.empty
A.AbsurdP _ -> Set.empty
A.LitP _ -> Set.empty
A.AsP _ _ p -> patVars p
A.PatternSynP _ _ _ -> __IMPOSSIBLE__
A.RecP _ as -> foldMap (foldMap patVars) as
blankDots ps = (map . fmap . fmap . fmap) blank ps
where
bound = argsVars ps
blank e | Set.null (Set.difference (dotVars e) bound) = e
| otherwise = A.Underscore emptyMetaInfo
rearrangeBinding x ps = ps
strip dvs ps = stripArgs True ps
where
stripArgs _ [] = []
stripArgs fixedPos (a : as) =
case getHiding a of
Hidden | canStrip a as -> stripArgs False as
Instance | canStrip a as -> stripArgs False as
_ -> stripName fixedPos (stripArg a) :
stripArgs True as
stripName True = fmap (unnamed . namedThing)
stripName False = id
canStrip a as = and
[ varOrDot p
, noInterestingBindings p
, all (flip canStrip []) $ takeWhile isUnnamedHidden as
]
where p = namedArg a
isUnnamedHidden x = notVisible x && nameOf (unArg x) == Nothing
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.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
noInterestingBindings p =
Set.null $ dvs `Set.intersection` patVars p
varOrDot A.VarP{} = True
varOrDot A.WildP{} = True
varOrDot A.DotP{} = True
varOrDot _ = False
class DotVars a where
dotVars :: a -> Set Name
isConPat :: a -> Bool
isConPat _ = False
instance DotVars a => DotVars (Arg a) where
dotVars a = if notVisible a && not (isConPat a)
then Set.empty
else dotVars (unArg a)
isConPat = isConPat . unArg
instance DotVars a => DotVars (Named s a) where
dotVars = dotVars . namedThing
isConPat = isConPat . namedThing
instance DotVars a => DotVars [a] where
dotVars = Set.unions . map dotVars
instance (DotVars a, DotVars b) => DotVars (a, b) where
dotVars (x, y) = Set.union (dotVars x) (dotVars y)
instance (DotVars a, DotVars b) => DotVars (Either a b) where
dotVars = either dotVars dotVars
instance DotVars A.Clause where
dotVars (A.Clause _ rhs [] _) = dotVars rhs
dotVars (A.Clause _ rhs (_:_) _) = __IMPOSSIBLE__
instance DotVars A.Pattern where
dotVars p = case p of
A.VarP _ -> Set.empty
A.ConP _ _ ps -> dotVars ps
A.DefP _ _ ps -> dotVars ps
A.DotP _ e -> dotVars e
A.WildP _ -> Set.empty
A.AbsurdP _ -> Set.empty
A.LitP _ -> Set.empty
A.AsP _ _ p -> dotVars p
A.PatternSynP _ _ _ -> __IMPOSSIBLE__
A.RecP _ fs -> dotVars fs
isConPat A.ConP{} = True
isConPat A.LitP{} = True
isConPat _ = False
instance DotVars A.Expr where
dotVars e = case e of
A.ScopedExpr _ e -> dotVars e
A.Var x -> Set.singleton x
A.Def _ -> Set.empty
A.Proj _ -> Set.empty
A.Con _ -> Set.empty
A.Lit _ -> Set.empty
A.QuestionMark{} -> Set.empty
A.Underscore _ -> Set.empty
A.App _ e1 e2 -> dotVars (e1, e2)
A.WithApp _ e es -> dotVars (e, es)
A.Lam _ _ e -> dotVars e
A.AbsurdLam _ _ -> Set.empty
A.ExtendedLam _ _ _ cs -> dotVars cs
A.Pi _ tel e -> dotVars (tel, e)
A.Fun _ a b -> dotVars (a, b)
A.Set _ _ -> Set.empty
A.Prop _ -> Set.empty
A.Let _ _ _ -> __IMPOSSIBLE__
A.Rec _ es -> dotVars es
A.RecUpdate _ e es -> dotVars (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 -> dotVars v
A.PatternSyn {} -> Set.empty
A.Macro {} -> Set.empty
instance DotVars a => DotVars (FieldAssignment' a) where
dotVars a = dotVars (a ^. exprFieldA)
instance DotVars A.ModuleName where
dotVars _ = Set.empty
instance DotVars RHS where
dotVars (RHS e) = dotVars e
dotVars AbsurdRHS = Set.empty
dotVars (WithRHS _ es clauses) = __IMPOSSIBLE__
dotVars (RewriteRHS xes rhs _) = __IMPOSSIBLE__
instance DotVars TypedBindings where
dotVars (TypedBindings _ bs) = dotVars bs
instance DotVars TypedBinding where
dotVars (TBind _ _ e) = dotVars e
dotVars (TLet _ _) = __IMPOSSIBLE__
class MonadTick m where
tick :: m Nat
newtype TickT m a = TickT { unTickT :: StateT Nat m a }
deriving (Functor, Applicative, Monad, MonadReader r, MonadTrans, MonadIO)
instance Monad m => MonadTick (TickT m) where
tick = TickT $ do i <- get; put (i + 1); return i
instance MonadState s m => MonadState s (TickT m) where
state f = lift $ state f
instance MonadTCM tcm => MonadTCM (TickT tcm) where
liftTCM = lift . liftTCM
runTickT :: Monad m => TickT m a -> m a
runTickT m = evalStateT (unTickT m) 0
reifyPatterns :: I.Telescope -> Permutation -> [NamedArg I.Pattern] -> TCM [NamedArg A.Pattern]
reifyPatterns tel perm ps = runTickT (reifyArgs ps)
where
reifyArgs :: [NamedArg I.Pattern] -> TickT TCM [NamedArg A.Pattern]
reifyArgs is = mapM reifyArg is
reifyArg :: NamedArg I.Pattern -> TickT TCM (NamedArg A.Pattern)
reifyArg i = stripNameFromExplicit <$>
traverse (traverse reifyPat) i
stripNameFromExplicit a
| getHiding a == NotHidden = fmap (unnamed . namedThing) a
| otherwise = a
translate n = fromMaybe __IMPOSSIBLE__ $ vars !!! n
where
vars = permPicks $ invertP __IMPOSSIBLE__ perm
reifyPat :: I.Pattern -> TickT TCM A.Pattern
reifyPat p = do
liftTCM $ reportSLn "reify.pat" 80 $ "reifying pattern " ++ show p
case p of
I.VarP "()" -> A.AbsurdP patNoRange <$ tick
I.VarP s -> do
i <- tick
let j = translate i
liftTCM $ A.VarP <$> nameOfBV (size tel 1 j)
I.DotP v -> do
t <- liftTCM $ reify v
_ <- tick
let vars = Set.map show (dotVars t)
t' = if Set.member "()" vars then underscore else t
return $ A.DotP patNoRange t'
I.LitP l -> return $ A.LitP l
I.ProjP d -> return $ A.DefP patNoRange d []
I.ConP c cpi ps -> do
liftTCM $ reportSLn "reify.pat" 60 $ "reifying pattern " ++ show p
tryRecPFromConP =<< do A.ConP ci (AmbQ [conName c]) <$> reifyArgs ps
where
origin = fromMaybe ConPCon $ I.conPRecord cpi
ci = ConPatInfo origin patNoRange
tryRecPFromConP :: MonadTCM tcm => A.Pattern -> tcm A.Pattern
tryRecPFromConP p = do
let fallback = return p
case p of
A.ConP ci (AmbQ [c]) ps -> do
caseMaybeM (liftTCM $ isRecordConstructor c) fallback $ \ (r, def) -> do
if recNamedCon def && patOrigin ci /= ConPRec 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 NamedClause A.Clause where
reify (QNamed f (I.Clause _ tel ps' body _ catchall)) = addCtxTel tel $ do
ps <- reifyPatterns tel perm ps
lhs <- liftTCM $ reifyDisplayFormP $ SpineLHS info f ps []
nfv <- getDefFreeVars f `catchError` \_ -> return 0
lhs <- stripImps $ dropParams nfv lhs
reportSLn "reify.clause" 60 $ "reifying NamedClause, lhs = " ++ show lhs
rhs <- reify $ renameP (reverseP perm) <$> body
reportSLn "reify.clause" 60 $ "reifying NamedClause, rhs = " ++ show rhs
let result = A.Clause (spineToLhs lhs) rhs [] catchall
reportSLn "reify.clause" 60 $ "reified NamedClause, result = " ++ show result
return result
where
info = LHSRange noRange
ps = unnumberPatVars ps'
perm = dbPatPerm ps'
dropParams n (SpineLHS i f ps wps) = SpineLHS i f (genericDrop n ps) wps
stripImps (SpineLHS i f ps wps) = do
(ps, wps) <- stripImplicits =<< shuffleDots (ps, wps)
return $ SpineLHS i f ps wps
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 exprInfo 0
I.Type (I.Max [I.ClosedLevel n]) -> return $ A.Set exprInfo n
I.Type a -> do
a <- reify a
return $ A.App exprInfo (A.Set exprInfo 0) (defaultNamedArg a)
I.Prop -> return $ A.Prop exprInfo
I.Inf -> A.Var <$> freshName_ ("SetĪ" :: String)
I.SizeUniv -> do
I.Def sizeU [] <- primSizeUniv
return $ A.Def sizeU
I.DLub s1 s2 -> do
lub <- freshName_ ("dLub" :: String)
(e1,e2) <- reify (s1, I.Lam defaultArgInfo $ fmap Sort s2)
let app x y = A.App exprInfo x (defaultNamedArg y)
return $ A.Var lub `app` e1 `app` e2
instance Reify Level Expr where
reifyWhen = reifyWhenE
reify l = reify =<< reallyUnLevelView l
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 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] [a] where
reify = traverse reify
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