module Agda.Syntax.Translation.InternalToAbstract
( Reify(..)
, NamedClause
, reifyPatterns
) where
import Prelude hiding (mapM_, mapM)
import Control.Applicative
import Control.Arrow
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 hiding (Arg, Dom, NamedArg, ArgInfo)
import Agda.Syntax.Fixity
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Info as Info
import Agda.Syntax.Abstract as A
import Agda.Syntax.Internal as I
import qualified Agda.Utils.VarSet as VSet
import Agda.TypeChecking.Monad as M hiding (MetaInfo)
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.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
napps :: Expr -> [I.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 -> [I.Arg Expr] -> TCM Expr
apps e args = napps e $ map (fmap unnamed) args
reifyApp :: Expr -> [I.Arg Term] -> TCM Expr
reifyApp e vs = apps e =<< reifyIArgs vs
reifyIArg :: Reify i a => I.Arg i -> TCM (I.Arg a)
reifyIArg i = Common.Arg (argInfo i) <$> reify (unArg i)
reifyIArgs :: Reify i a => [I.Arg i] -> TCM [I.Arg a]
reifyIArgs = mapM reifyIArg
reifyIArg' :: I.Arg e -> TCM (A.Arg e)
reifyIArg' e = flip Common.Arg (unArg e) <$> reify (argInfo e)
reifyIArgs' :: [I.Arg e] -> TCM [A.Arg e]
reifyIArgs' = mapM reifyIArg'
exprInfo :: ExprInfo
exprInfo = ExprRange noRange
instance Underscore Expr where
underscore = A.Underscore $ Info.emptyMetaInfo
isUnderscore = __IMPOSSIBLE__
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 n
, metaNameSuggestion = miNameSuggestion mi
}
underscore = return $ A.Underscore mi'
ifNotM shouldReifyInteractionPoints underscore $
caseMaybeM (isInteractionMeta x) underscore $ \ ii@InteractionId{} ->
return $ A.QuestionMark (mi' {metaNumber = Just n}) 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 vs -> apps (A.Def f) =<< reifyIArgs vs
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 `catchError` \_ -> return Nothing
reportSLn "reify.display" 20 $
"display form of " ++ show f ++ " " ++ show ps ++ " " ++ show wps ++ ":\n " ++ show md
case md of
Just d | okDisplayForm d ->
reifyDisplayFormP =<< displayLHS (map namedArg ps) wps d
_ -> return lhs
where
okDisplayForm (DWithApp d ds []) =
okDisplayForm d && all okDisplayTerm ds
okDisplayForm (DTerm (I.Def f vs)) = all okElim vs
okDisplayForm (DDef f vs) = all okDArg vs
okDisplayForm DDot{} = False
okDisplayForm DCon{} = False
okDisplayForm DTerm{} = True
okDisplayForm DWithApp{} = True
okDisplayTerm (DTerm v) = okTerm v
okDisplayTerm DDot{} = True
okDisplayTerm DCon{} = True
okDisplayTerm DDef{} = False
okDisplayTerm _ = False
okDArg = okDisplayTerm . unArg
okArg = okTerm . unArg
okElim (I.Apply a) = okArg a
okElim (I.Proj{}) = False
okTerm (I.Var _ []) = True
okTerm (I.Con c vs) = all okArg vs
okTerm (I.Def x []) = isNoName $ qnameToConcrete x
okTerm _ = True
flattenWith :: DisplayTerm -> (QName, [I.Arg DisplayTerm], [DisplayTerm])
flattenWith (DWithApp d ds1 ds2) = case flattenWith d of
(f, vs, ds0) -> (f, vs, ds0 ++ ds1 ++ map (DTerm . unArg) ds2)
flattenWith (DDef f vs) = (f, vs, [])
flattenWith (DTerm (I.Def f es)) =
let vs = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es
in (f, map (fmap DTerm) vs, [])
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 argToPat vs
vs <- reifyIArgs' vs
return $ SpineLHS i f vs (ds ++ wps)
where
ci = ConPatInfo False patNoRange
argToPat arg = fmap unnamed <$> traverse termToPat arg
termToPat :: DisplayTerm -> TCM A.Pattern
termToPat (DTerm (I.Var n [])) = return $ ps !! n
termToPat (DCon c vs) = A.ConP ci (AmbQ [conName c]) <$> do
mapM argToPat =<< reifyIArgs' vs
termToPat (DTerm (I.Con c vs)) = A.ConP ci (AmbQ [conName c]) <$> do
mapM (argToPat . fmap DTerm) =<< reifyIArgs' 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@(LitInt {}) = return (A.Lit l)
reify l@(LitFloat {}) = return (A.Lit l)
reify l@(LitString {}) = return (A.Lit l)
reify l@(LitChar {}) = return (A.Lit l)
reify l@(LitQName {}) = 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
hasDisplayForms <- displayFormsEnabled
let expandAnonDefs = expandAnonDefs0 && hasDisplayForms
v <- unSpine <$> instantiate v
case v of
_ | isHackReifyToMeta v -> return $ A.Underscore emptyMetaInfo
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 (unArg *** id) $ 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
unquote <- isReifyingUnquoted
if np == 0 || unquote then apps h es else do
TelV tel _ <- telView (defType ci)
case genericDrop np $ telToList tel of
(Common.Dom info _ : _) | isHidden info -> do
let us = genericReplicate (np n) $
setRelevance Relevant $ Common.Arg info underscore
apps h $ us ++ es
_ -> apps h es
I.Lam info b -> do
(x,e) <- reify b
info <- reify info
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))
(Common.Arg <$> reify (domInfo a) <*> pure underscore)
(reify a)
where
mkPi b (Common.Arg info a) = do
(x, b) <- reify b
return $ A.Pi exprInfo [TypedBindings noRange $ Common.Arg info (TBind noRange [x] a)] b
domainFree a b = do
df <- asks envPrintDomainFreePi
return $ and [df, freeIn 0 b, VSet.null $ allVars $ freeVars 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
I.ExtLam cls args -> do
x <- freshName_ "extlam"
reifyExtLam (qnameFromList [x]) 0 cls (map (fmap unnamed) args)
where
reifyDef :: Bool -> QName -> I.Args -> TCM Expr
reifyDef True x@(QName m name) vs | A.isAnonymousModuleName m = 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 :: [I.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 } } -> 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__)
pad' <- reifyIArgs' $ genericDrop n pad
let vs' :: [I.Arg Term]
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 (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] -> [I.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 defaultFixity' PublicAccess ConcreteDef (getRange x)
napps (A.ExtendedLam exprInfo dInfo x cls) =<< reifyIArgs vs
nameFirstIfHidden :: [I.Dom (ArgName, t)] -> [I.Arg a] -> [I.NamedArg a]
nameFirstIfHidden _ [] = []
nameFirstIfHidden [] (_ : _) = __IMPOSSIBLE__
nameFirstIfHidden (dom : _) (Common.Arg info e : es) | isHidden info =
Common.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 (I.Arg i) (A.Arg a) where
reify (Common.Arg info i) = liftM2 Common.Arg (reify info)
(flip reifyWhen i =<< condition)
where condition = (return (argInfoHiding info /= Hidden) `or2M` showImplicitArguments)
`and2M` (return (argInfoRelevance info /= Irrelevant) `or2M` showIrrelevantArguments)
reifyWhen b i = do info <- reify $ argInfo i
traverse (reifyWhen b) $ i { argInfo = info }
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 []) :: I.Arg Term)
where
appl :: String -> A.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 :: ([A.NamedArg A.Pattern], [A.Pattern]) -> TCM ([A.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.ImplicitP{} -> mempty
A.AsP{} -> __IMPOSSIBLE__
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.ImplicitP{} -> pure p
A.AsP{} -> __IMPOSSIBLE__
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 :: ([A.NamedArg A.Pattern], [A.Pattern]) ->
TCM ([A.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.ImplicitP _ -> Set.empty
A.AsP _ _ p -> patVars p
A.PatternSynP _ _ _ -> __IMPOSSIBLE__
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.ImplicitP _ -> p
A.AsP i x p -> A.AsP i x $ stripPat p
A.PatternSynP _ _ _ -> __IMPOSSIBLE__
noInterestingBindings p =
Set.null $ dvs `Set.intersection` patVars p
varOrDot A.VarP{} = True
varOrDot A.WildP{} = True
varOrDot A.DotP{} = True
varOrDot A.ImplicitP{} = True
varOrDot _ = False
class DotVars a where
dotVars :: a -> Set Name
isConPat :: a -> Bool
isConPat _ = False
instance DotVars a => DotVars (A.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.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.ImplicitP _ -> Set.empty
A.AsP _ _ p -> dotVars p
A.PatternSynP _ _ _ -> __IMPOSSIBLE__
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 $ map snd es
A.RecUpdate _ e es -> dotVars (e, map snd es)
A.ETel _ -> __IMPOSSIBLE__
A.QuoteGoal {} -> __IMPOSSIBLE__
A.QuoteContext {} -> __IMPOSSIBLE__
A.Quote {} -> __IMPOSSIBLE__
A.QuoteTerm {} -> __IMPOSSIBLE__
A.Unquote {} -> __IMPOSSIBLE__
A.DontCare v -> dotVars v
A.PatternSyn n -> Set.empty
instance DotVars RHS where
dotVars (RHS e) = dotVars e
dotVars AbsurdRHS = Set.empty
dotVars (WithRHS _ es clauses) = __IMPOSSIBLE__
dotVars (RewriteRHS _ es rhs _) = __IMPOSSIBLE__
instance DotVars TypedBindings where
dotVars (TypedBindings _ bs) = dotVars bs
instance DotVars TypedBinding where
dotVars (TBind _ _ e) = dotVars e
dotVars (TLet _ _) = __IMPOSSIBLE__
reifyPatterns :: I.Telescope -> Permutation -> [I.NamedArg I.Pattern] -> TCM [A.NamedArg A.Pattern]
reifyPatterns tel perm ps = evalStateT (reifyArgs ps) 0
where
reifyArgs :: [I.NamedArg I.Pattern] -> StateT Nat TCM [A.NamedArg A.Pattern]
reifyArgs is = mapM reifyArg is
reifyArg :: I.NamedArg I.Pattern -> StateT Nat TCM (A.NamedArg A.Pattern)
reifyArg i = stripNameFromExplicit <$>
traverse (traverse reifyPat) (setArgColors [] i)
stripNameFromExplicit a
| getHiding a == NotHidden = fmap (unnamed . namedThing) a
| otherwise = a
tick = do i <- get; put (i + 1); return i
translate = (vars !!)
where
vars = permute (invertP __IMPOSSIBLE__ perm) [0..]
reifyPat :: I.Pattern -> StateT Nat TCM A.Pattern
reifyPat p = case p of
I.VarP "()" -> A.AbsurdP patNoRange <$ tick
I.VarP s -> do
i <- tick
let j = translate i
lift $ A.VarP <$> nameOfBV (size tel 1 j)
I.DotP v -> do
t <- lift $ 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 mt ps -> A.ConP ci (AmbQ [conName c]) <$> reifyArgs ps
where ci = flip ConPatInfo patNoRange $ maybe False fst mt
instance Reify NamedClause A.Clause where
reify (QNamed f (I.Clause _ tel perm ps body _)) = 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 []
reportSLn "reify.clause" 60 $ "reified NamedClause, result = " ++ show result
return result
where
info = LHSRange noRange
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.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
Common.Arg info e <- reify arg
(x,bs) <- reify tel
let r = getRange e
return $ TypedBindings r (Common.Arg info (TBind r [x] e)) : bs
instance Reify I.ArgInfo A.ArgInfo where
reify i = flip (mapArgInfoColors.const) i <$> reify (argInfoColors i)
instance Reify i a => Reify (I.Dom i) (A.Arg a) where
reify (Common.Dom info i) = liftM2 Common.Arg (reify 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
instance (Reify t t', Reify a a')
=> Reify (Judgement t a) (Judgement t' a') where
reify (HasType i t) = HasType <$> reify i <*> reify t
reify (IsSort i t) = IsSort <$> reify i <*> reify t