{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NondecreasingIndentation #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.Interaction.BasicOps where
import Prelude hiding (null)
import Control.Arrow ((***), first, second)
import Control.Applicative hiding (empty)
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Identity
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.List as List
import Data.Maybe
import Data.Traversable hiding (mapM, forM, for)
import Data.Monoid
import Agda.Interaction.Options
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Position
import Agda.Syntax.Abstract as A hiding (Open, Apply, Assign)
import Agda.Syntax.Abstract.Views as A
import Agda.Syntax.Abstract.Pretty
import Agda.Syntax.Common
import Agda.Syntax.Info (ExprInfo(..),MetaInfo(..),emptyMetaInfo,exprNoRange,defaultAppInfo_,defaultAppInfo)
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Internal as I
import Agda.Syntax.Literal
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Translation.AbstractToConcrete
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad
import Agda.Syntax.Fixity(Precedence(..), argumentCtx_)
import Agda.Syntax.Parser
import Agda.TheTypeChecker
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Errors ( stringTCErr )
import Agda.TypeChecking.Monad as M hiding (MetaInfo)
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.With
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Records
import Agda.TypeChecking.Irrelevance (wakeIrrelevantVars)
import Agda.TypeChecking.Pretty (prettyTCM)
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Names
import Agda.TypeChecking.Free
import Agda.TypeChecking.CheckInternal
import Agda.TypeChecking.SizedTypes.Solve
import qualified Agda.TypeChecking.Pretty as TP
import Agda.TypeChecking.Warnings ( runPM, warning )
import Agda.Termination.TermCheck (termMutual)
import Agda.Utils.Except ( MonadError(catchError, throwError) )
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.Pretty
import Agda.Utils.Permutation
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
parseExpr :: Range -> String -> TCM C.Expr
parseExpr rng s = do
C.ExprWhere e wh <- runPM $ parsePosString exprWhereParser pos s
unless (null wh) $ typeError $ GenericError $
"where clauses are not supported in holes"
return e
where pos = fromMaybe (startPos Nothing) $ rStart rng
parseExprIn :: InteractionId -> Range -> String -> TCM Expr
parseExprIn ii rng s = do
mId <- lookupInteractionId ii
updateMetaVarRange mId rng
mi <- getMetaInfo <$> lookupMeta mId
e <- parseExpr rng s
concreteToAbstract (clScope mi) e
giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM ()
giveExpr force mii mi e = do
mv <- lookupMeta mi
withMetaInfo (getMetaInfo mv) $ do
metaTypeCheck mv (mvJudgement mv)
where
metaTypeCheck mv IsSort{} = __IMPOSSIBLE__
metaTypeCheck mv (HasType _ t) = do
reportSDoc "interaction.give" 20 $
"give: meta type =" TP.<+> prettyTCM t
ctx <- getContextArgs
t' <- t `piApplyM` permute (takeP (length ctx) $ mvPermutation mv) ctx
traceCall (CheckExprCall CmpLeq e t') $ do
reportSDoc "interaction.give" 20 $
"give: instantiated meta type =" TP.<+> prettyTCM t'
v <- checkExpr e t'
case mvInstantiation mv of
InstV xs v' -> unlessM ((Irrelevant ==) <$> asksTC envRelevance) $ do
reportSDoc "interaction.give" 20 $ TP.sep
[ "meta was already set to value v' = " TP.<+> prettyTCM v'
TP.<+> " with free variables " TP.<+> return (fsep $ map pretty xs)
, "now comparing it to given value v = " TP.<+> prettyTCM v
, "in context " TP.<+> inTopContext (prettyTCM ctx)
]
when (length xs < size ctx) __IMPOSSIBLE__
let (_xs1, xs2) = splitAt (size ctx) xs
v' <- return $ foldr mkLam v' xs2
reportSDoc "interaction.give" 20 $ TP.sep
[ "in meta context, v' = " TP.<+> prettyTCM v'
]
equalTerm t' v v'
_ -> do
reportSLn "interaction.give" 20 "give: meta unassigned, assigning..."
args <- getContextArgs
nowSolvingConstraints $ assign DirEq mi args v
reportSDoc "interaction.give" 20 $ "give: meta variable updated!"
unless (force == WithForce) $ redoChecks mii
wakeupConstraints mi
solveSizeConstraints DontDefaultToInfty
cubical <- optCubical <$> pragmaOptions
unless (cubical || force == WithForce) $ do
reportSDoc "interaction.give" 20 $ "give: double checking"
vfull <- instantiateFull v
checkInternal vfull t'
redoChecks :: Maybe InteractionId -> TCM ()
redoChecks Nothing = return ()
redoChecks (Just ii) = do
reportSLn "interaction.give" 20 $
"give: redoing termination check for function surrounding " ++ show ii
ip <- lookupInteractionPoint ii
case ipClause ip of
IPNoClause -> return ()
IPClause f _ _ -> do
mb <- mutualBlockOf f
terErrs <- localTC (\ e -> e { envMutualBlock = Just mb }) $ termMutual []
unless (null terErrs) $ warning $ TerminationIssue terErrs
give
:: UseForce
-> InteractionId
-> Maybe Range
-> Expr
-> TCM Expr
give force ii mr e = liftTCM $ do
mi <- lookupInteractionId ii
whenJust mr $ updateMetaVarRange mi
reportSDoc "interaction.give" 10 $ "giving expression" TP.<+> prettyTCM e
reportSDoc "interaction.give" 50 $ TP.text $ show $ deepUnscope e
do setMetaOccursCheck mi DontRunMetaOccursCheck
giveExpr force (Just ii) mi e
`catchError` \ case
PatternErr -> typeError . GenericDocError =<< do
withInteractionId ii $ "Failed to give" TP.<+> prettyTCM e
err -> throwError err
removeInteractionPoint ii
return e
refine
:: UseForce
-> InteractionId
-> Maybe Range
-> Expr
-> TCM Expr
refine force ii mr e = do
mi <- lookupInteractionId ii
mv <- lookupMeta mi
let range = fromMaybe (getRange mv) mr
scope = M.getMetaScope mv
reportSDoc "interaction.refine" 10 $
"refining with expression" TP.<+> prettyTCM e
reportSDoc "interaction.refine" 50 $
TP.text $ show $ deepUnscope e
tryRefine 10 range scope e
where
tryRefine :: Int -> Range -> ScopeInfo -> Expr -> TCM Expr
tryRefine nrOfMetas r scope e = try nrOfMetas e
where
try :: Int -> Expr -> TCM Expr
try 0 e = throwError $ stringTCErr "Cannot refine"
try n e = give force ii (Just r) e `catchError` (\_ -> try (n - 1) =<< appMeta e)
appMeta :: Expr -> TCM Expr
appMeta e = do
let rng = rightMargin r
ii <- registerInteractionPoint False rng Nothing
let info = Info.MetaInfo
{ Info.metaRange = rng
, Info.metaScope = scope { scopePrecedence = [argumentCtx_] }
, metaNumber = Nothing
, metaNameSuggestion = ""
}
metaVar = QuestionMark info ii
count x e = getSum $ foldExpr isX e
where isX (A.Var y) | x == y = Sum 1
isX _ = mempty
lamView (A.Lam _ (DomainFree x) e) = Just (namedArg x, e)
lamView (A.Lam i (DomainFull (TBind r (x : xs) a)) e)
| null xs = Just (namedArg x, e)
| otherwise = Just (namedArg x, A.Lam i (DomainFull $ TBind r xs a) e)
lamView _ = Nothing
smartApp i e arg =
case lamView $ unScope e of
Just (A.BindName x, e) | count x e < 2 -> mapExpr subX e
where subX (A.Var y) | x == y = namedArg arg
subX e = e
_ -> App i e arg
return $ smartApp (defaultAppInfo r) e $ defaultNamedArg metaVar
evalInCurrent :: Expr -> TCM Expr
evalInCurrent e =
do (v, t) <- inferExpr e
v' <- normalise v
reify v'
evalInMeta :: InteractionId -> Expr -> TCM Expr
evalInMeta ii e =
do m <- lookupInteractionId ii
mi <- getMetaInfo <$> lookupMeta m
withMetaInfo mi $
evalInCurrent e
data Rewrite = AsIs | Instantiated | HeadNormal | Simplified | Normalised
deriving (Show, Read)
normalForm :: (Reduce t, Simplify t, Normalise t) => Rewrite -> t -> TCM t
normalForm AsIs t = return t
normalForm Instantiated t = return t
normalForm HeadNormal t = reduce t
normalForm Simplified t = simplify t
normalForm Normalised t = normalise t
data ComputeMode = DefaultCompute | IgnoreAbstract | UseShowInstance
deriving (Show, Read, Eq)
computeIgnoreAbstract :: ComputeMode -> Bool
computeIgnoreAbstract DefaultCompute = False
computeIgnoreAbstract IgnoreAbstract = True
computeIgnoreAbstract UseShowInstance = True
computeWrapInput :: ComputeMode -> String -> String
computeWrapInput UseShowInstance s = "show (" ++ s ++ ")"
computeWrapInput _ s = s
showComputed :: ComputeMode -> Expr -> TCM Doc
showComputed UseShowInstance e =
case e of
A.Lit (LitString _ s) -> pure (text s)
_ -> ("Not a string:" $$) <$> prettyATop e
showComputed _ e = prettyATop e
data UseForce
= WithForce
| WithoutForce
deriving (Eq, Read, Show)
data OutputForm a b = OutputForm Range [ProblemId] (OutputConstraint a b)
deriving (Functor)
data OutputConstraint a b
= OfType b a | CmpInType Comparison a b b
| CmpElim [Polarity] a [b] [b]
| JustType b | CmpTypes Comparison b b
| CmpLevels Comparison b b
| CmpTeles Comparison b b
| JustSort b | CmpSorts Comparison b b
| Guard (OutputConstraint a b) ProblemId
| Assign b a | TypedAssign b a a | PostponedCheckArgs b [a] a a
| IsEmptyType a
| SizeLtSat a
| FindInstanceOF b a [(a,a)]
| PTSInstance b b
| PostponedCheckFunDef QName a
deriving (Functor)
data OutputConstraint' a b = OfType' { ofName :: b
, ofExpr :: a
}
outputFormId :: OutputForm a b -> b
outputFormId (OutputForm _ _ o) = out o
where
out o = case o of
OfType i _ -> i
CmpInType _ _ i _ -> i
CmpElim _ _ (i:_) _ -> i
CmpElim _ _ [] _ -> __IMPOSSIBLE__
JustType i -> i
CmpLevels _ i _ -> i
CmpTypes _ i _ -> i
CmpTeles _ i _ -> i
JustSort i -> i
CmpSorts _ i _ -> i
Guard o _ -> out o
Assign i _ -> i
TypedAssign i _ _ -> i
PostponedCheckArgs i _ _ _ -> i
IsEmptyType _ -> __IMPOSSIBLE__
SizeLtSat{} -> __IMPOSSIBLE__
FindInstanceOF _ _ _ -> __IMPOSSIBLE__
PTSInstance i _ -> i
PostponedCheckFunDef{} -> __IMPOSSIBLE__
instance Reify ProblemConstraint (Closure (OutputForm Expr Expr)) where
reify (PConstr pids cl) = enterClosure cl $ \c -> buildClosure =<< (OutputForm (getRange c) (Set.toList pids) <$> reify c)
reifyElimToExpr :: I.Elim -> TCM Expr
reifyElimToExpr e = case e of
I.IApply _ _ v -> appl "iapply" <$> reify (defaultArg $ v)
I.Apply v -> appl "apply" <$> reify v
I.Proj _o f -> appl "proj" <$> reify ((defaultArg $ I.Def f []) :: Arg Term)
where
appl :: String -> Arg Expr -> Expr
appl s v = A.App defaultAppInfo_ (A.Lit (LitString noRange s)) $ fmap unnamed v
instance Reify Constraint (OutputConstraint Expr Expr) where
reify (ValueCmp cmp t u v) = CmpInType cmp <$> reify t <*> reify u <*> reify v
reify (ValueCmpOnFace cmp p t u v) = CmpInType cmp <$> (reify =<< ty) <*> reify (lam_o u) <*> reify (lam_o v)
where
lam_o = I.Lam (setRelevance Irrelevant defaultArgInfo) . NoAbs "_"
ty = runNamesT [] $ do
p <- open p
t <- open t
pPi' "o" p (\ o -> t)
reify (ElimCmp cmp _ t v es1 es2) =
CmpElim cmp <$> reify t <*> mapM reifyElimToExpr es1
<*> mapM reifyElimToExpr es2
reify (LevelCmp cmp t t') = CmpLevels cmp <$> reify t <*> reify t'
reify (TypeCmp cmp t t') = CmpTypes cmp <$> reify t <*> reify t'
reify (TelCmp a b cmp t t') = CmpTeles cmp <$> (ETel <$> reify t) <*> (ETel <$> reify t')
reify (SortCmp cmp s s') = CmpSorts cmp <$> reify s <*> reify s'
reify (Guarded c pid) = do
o <- reify c
return $ Guard o pid
reify (UnBlock m) = do
mi <- mvInstantiation <$> lookupMeta m
m' <- reify (MetaV m [])
case mi of
BlockedConst t -> do
e <- reify t
return $ Assign m' e
PostponedTypeCheckingProblem cl _ -> enterClosure cl $ \p -> case p of
CheckExpr cmp e a -> do
a <- reify a
return $ TypedAssign m' e a
CheckLambda cmp (Arg ai (xs, mt)) body target -> do
domType <- maybe (return underscore) reify mt
target <- reify target
let mkN (WithHiding h x) = setHiding h $ defaultNamedArg $ A.BindName x
bs = TBind noRange (map mkN xs) domType
e = A.Lam Info.exprNoRange (DomainFull bs) body
return $ TypedAssign m' e target
CheckArgs _ _ args t0 t1 _ -> do
t0 <- reify t0
t1 <- reify t1
return $ PostponedCheckArgs m' (map (namedThing . unArg) args) t0 t1
CheckProjAppToKnownPrincipalArg cmp e _ _ _ t _ _ _ -> TypedAssign m' e <$> reify t
UnquoteTactic tac _ goal -> do
tac <- A.App defaultAppInfo_ (A.Unquote exprNoRange) . defaultNamedArg <$> reify tac
OfType tac <$> reify goal
DoQuoteTerm cmp v t -> do
tm <- A.App defaultAppInfo_ (A.QuoteTerm exprNoRange) . defaultNamedArg <$> reify v
OfType tm <$> reify t
Open{} -> __IMPOSSIBLE__
OpenInstance{} -> __IMPOSSIBLE__
InstV{} -> __IMPOSSIBLE__
reify (FindInstance m _b mcands) = FindInstanceOF
<$> (reify $ MetaV m [])
<*> (reify =<< getMetaType m)
<*> (forM (fromMaybe [] mcands) $ \ (Candidate tm ty _) -> do
(,) <$> reify tm <*> reify ty)
reify (IsEmpty r a) = IsEmptyType <$> reify a
reify (CheckSizeLtSat a) = SizeLtSat <$> reify a
reify (CheckFunDef d i q cs) = do
a <- reify =<< defType <$> getConstInfo q
return $ PostponedCheckFunDef q a
reify (HasBiggerSort a) = OfType <$> reify a <*> reify (UnivSort a)
reify (HasPTSRule a b) = do
(a,(x,b)) <- reify (a,b)
return $ PTSInstance a b
instance (Pretty a, Pretty b) => Pretty (OutputForm a b) where
pretty (OutputForm r pids c)
| null pids = sep [pretty c, prange r]
| otherwise = sep [pretty pids, nest 2 $ sep [pretty c, prange r]]
where
prange r | null s = empty
| otherwise = text $ " [ at " ++ s ++ " ]"
where s = show r
instance (Pretty a, Pretty b) => Pretty (OutputConstraint a b) where
pretty oc =
case oc of
OfType e t -> pretty e .: t
JustType e -> "Type" <+> pretty e
JustSort e -> "Sort" <+> pretty e
CmpInType cmp t e e' -> pcmp cmp e e' .: t
CmpElim cmp t e e' -> pcmp cmp e e' .: t
CmpTypes cmp t t' -> pcmp cmp t t'
CmpLevels cmp t t' -> pcmp cmp t t'
CmpTeles cmp t t' -> pcmp cmp t t'
CmpSorts cmp s s' -> pcmp cmp s s'
Guard o pid -> pretty o <?> brackets ("blocked by problem" <+> pretty pid)
Assign m e -> bin (pretty m) ":=" (pretty e)
TypedAssign m e a -> bin (pretty m) ":=" $ bin (pretty e) ":?" (pretty a)
PostponedCheckArgs m es t0 t1 ->
bin (pretty m) ":=" $ (parens ("_" .: t0) <+> fsep (map (paren . pretty) es)) .: t1
where paren d = mparens (any (`elem` [' ', '\n']) $ show d) d
IsEmptyType a -> "Is empty:" <+> pretty a
SizeLtSat a -> "Not empty type of sizes:" <+> pretty a
FindInstanceOF s t cs -> vcat
[ "Resolve instance argument" <?> (pretty s .: t)
, nest 2 $ "Candidate:"
, nest 4 $ vcat [ pretty v .: t | (v, t) <- cs ] ]
PTSInstance a b -> "PTS instance for" <+> pretty (a, b)
PostponedCheckFunDef q a -> "Check definition of" <+> pretty q <+> ":" <+> pretty a
where
bin a op b = sep [a, nest 2 $ op <+> b]
pcmp cmp a b = bin (pretty a) (pretty cmp) (pretty b)
val .: ty = bin val ":" (pretty ty)
instance (ToConcrete a c, ToConcrete b d) =>
ToConcrete (OutputForm a b) (OutputForm c d) where
toConcrete (OutputForm r pid c) = OutputForm r pid <$> toConcrete c
instance (ToConcrete a c, ToConcrete b d) =>
ToConcrete (OutputConstraint a b) (OutputConstraint c d) where
toConcrete (OfType e t) = OfType <$> toConcrete e <*> toConcreteCtx TopCtx t
toConcrete (JustType e) = JustType <$> toConcrete e
toConcrete (JustSort e) = JustSort <$> toConcrete e
toConcrete (CmpInType cmp t e e') =
CmpInType cmp <$> toConcreteCtx TopCtx t <*> toConcreteCtx argumentCtx_ e
<*> toConcreteCtx argumentCtx_ e'
toConcrete (CmpElim cmp t e e') =
CmpElim cmp <$> toConcreteCtx TopCtx t <*> toConcreteCtx TopCtx e <*> toConcreteCtx TopCtx e'
toConcrete (CmpTypes cmp e e') = CmpTypes cmp <$> toConcreteCtx argumentCtx_ e
<*> toConcreteCtx argumentCtx_ e'
toConcrete (CmpLevels cmp e e') = CmpLevels cmp <$> toConcreteCtx argumentCtx_ e
<*> toConcreteCtx argumentCtx_ e'
toConcrete (CmpTeles cmp e e') = CmpTeles cmp <$> toConcrete e <*> toConcrete e'
toConcrete (CmpSorts cmp e e') = CmpSorts cmp <$> toConcreteCtx argumentCtx_ e
<*> toConcreteCtx argumentCtx_ e'
toConcrete (Guard o pid) = Guard <$> toConcrete o <*> pure pid
toConcrete (Assign m e) = noTakenNames $ Assign <$> toConcrete m <*> toConcreteCtx TopCtx e
toConcrete (TypedAssign m e a) = TypedAssign <$> toConcrete m <*> toConcreteCtx TopCtx e
<*> toConcreteCtx TopCtx a
toConcrete (PostponedCheckArgs m args t0 t1) =
PostponedCheckArgs <$> toConcrete m <*> toConcrete args <*> toConcrete t0 <*> toConcrete t1
toConcrete (IsEmptyType a) = IsEmptyType <$> toConcreteCtx TopCtx a
toConcrete (SizeLtSat a) = SizeLtSat <$> toConcreteCtx TopCtx a
toConcrete (FindInstanceOF s t cs) =
FindInstanceOF <$> toConcrete s <*> toConcrete t
<*> mapM (\(tm,ty) -> (,) <$> toConcrete tm <*> toConcrete ty) cs
toConcrete (PTSInstance a b) = PTSInstance <$> toConcrete a <*> toConcrete b
toConcrete (PostponedCheckFunDef q a) = PostponedCheckFunDef q <$> toConcrete a
instance (Pretty a, Pretty b) => Pretty (OutputConstraint' a b) where
pretty (OfType' e t) = pretty e <+> ":" <+> pretty t
instance (ToConcrete a c, ToConcrete b d) =>
ToConcrete (OutputConstraint' a b) (OutputConstraint' c d) where
toConcrete (OfType' e t) = OfType' <$> toConcrete e <*> toConcreteCtx TopCtx t
getConstraints :: TCM [OutputForm C.Expr C.Expr]
getConstraints = liftTCM $ do
cs <- M.getAllConstraints
cs <- forM cs $ \c -> do
cl <- reify c
enterClosure cl abstractToConcrete_
ss <- mapM toOutputForm =<< getSolvedInteractionPoints True AsIs
return $ ss ++ cs
where
toOutputForm (ii, mi, e) = do
mv <- getMetaInfo <$> lookupMeta mi
withMetaInfo mv $ do
let m = QuestionMark emptyMetaInfo{ metaNumber = Just $ fromIntegral ii } ii
abstractToConcrete_ $ OutputForm noRange [] $ Assign m e
getSolvedInteractionPoints :: Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)]
getSolvedInteractionPoints all norm = concat <$> do
mapM solution =<< getInteractionIdsAndMetas
where
solution (i, m) = do
mv <- lookupMeta m
withMetaInfo (getMetaInfo mv) $ do
args <- getContextArgs
scope <- getScope
let sol v = do
v <- instantiate v
let isMeta = case v of MetaV{} -> True; _ -> False
if isMeta && not all then return [] else do
e <- reify =<< normalForm norm v
return [(i, m, ScopedExpr scope e)]
unsol = return []
case mvInstantiation mv of
InstV{} -> sol (MetaV m $ map Apply args)
Open{} -> unsol
OpenInstance{} -> unsol
BlockedConst{} -> unsol
PostponedTypeCheckingProblem{} -> unsol
typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
typeOfMetaMI norm mi =
do mv <- lookupMeta mi
withMetaInfo (getMetaInfo mv) $
rewriteJudg mv (mvJudgement mv)
where
rewriteJudg :: MetaVariable -> Judgement MetaId ->
TCM (OutputConstraint Expr NamedMeta)
rewriteJudg mv (HasType i t) = do
ms <- getMetaNameSuggestion i
t <- normalForm norm t
vs <- getContextArgs
let x = NamedMeta ms i
reportSDoc "interactive.meta" 10 $ TP.vcat
[ TP.text $ unwords ["permuting", show i, "with", show $ mvPermutation mv]
, TP.nest 2 $ TP.vcat
[ "len =" TP.<+> TP.text (show $ length vs)
, "args =" TP.<+> prettyTCM vs
, "t =" TP.<+> prettyTCM t
, "x =" TP.<+> TP.pretty x
]
]
reportSDoc "interactive.meta.scope" 20 $ TP.text $ show $ getMetaScope mv
OfType x <$> do reify =<< t `piApplyM` permute (takeP (size vs) $ mvPermutation mv) vs
rewriteJudg mv (IsSort i t) = do
ms <- getMetaNameSuggestion i
return $ JustSort $ NamedMeta ms i
typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta norm ii = typeOfMeta' norm . (ii,) =<< lookupInteractionId ii
typeOfMeta' :: Rewrite -> (InteractionId, MetaId) -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta' norm (ii, mi) = fmap (\_ -> ii) <$> typeOfMetaMI norm mi
typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint Expr InteractionId]
typesOfVisibleMetas norm =
liftTCM $ mapM (typeOfMeta' norm) =<< getInteractionIdsAndMetas
typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]
typesOfHiddenMetas norm = liftTCM $ do
is <- getInteractionMetas
store <- Map.filterWithKey (openAndImplicit is) <$> getMetaStore
mapM (typeOfMetaMI norm) $ Map.keys store
where
openAndImplicit is x m =
case mvInstantiation m of
M.InstV{} -> False
M.Open -> x `notElem` is
M.OpenInstance -> x `notElem` is
M.BlockedConst{} -> True
M.PostponedTypeCheckingProblem{} -> False
metaHelperType :: Rewrite -> InteractionId -> Range -> String -> TCM (OutputConstraint' Expr Expr)
metaHelperType norm ii rng s = case words s of
[] -> failure
f : _ -> do
ensureName f
A.Application h args <- A.appView . getBody . deepUnscope <$> parseExprIn ii rng ("let " ++ f ++ " = _ in " ++ s)
withInteractionId ii $ do
cxtArgs <- getContextArgs
tel <- runIdentity . onNamesTel unW <$> getContextTelescope
a <- runIdentity . onNames unW . (`piApply` cxtArgs) <$> (getMetaType =<< lookupInteractionId ii)
(vs, as) <- unzip <$> mapM (inferExpr . namedThing . unArg) args
TelV atel _ <- telView a
let arity = size atel
(delta1, delta2, _, a', as', vs') = splitTelForWith tel a (map OtherType as) vs
a <- localTC (\e -> e { envPrintDomainFreePi = True }) $ do
reify =<< cleanupType arity args =<< normalForm norm =<< fst <$> withFunctionType delta1 vs' as' delta2 a'
reportSDoc "interaction.helper" 10 $ TP.vcat
[ "generating helper function"
, TP.nest 2 $ "tel = " TP.<+> inTopContext (prettyTCM tel)
, TP.nest 2 $ "a = " TP.<+> prettyTCM a
, TP.nest 2 $ "vs = " TP.<+> prettyTCM vs
, TP.nest 2 $ "as = " TP.<+> prettyTCM as
, TP.nest 2 $ "delta1 = " TP.<+> inTopContext (prettyTCM delta1)
, TP.nest 2 $ "delta2 = " TP.<+> inTopContext (addContext delta1 $ prettyTCM delta2)
, TP.nest 2 $ "a' = " TP.<+> inTopContext (addContext delta1 $ addContext delta2 $ prettyTCM a')
, TP.nest 2 $ "as' = " TP.<+> inTopContext (addContext delta1 $ prettyTCM as')
, TP.nest 2 $ "vs' = " TP.<+> inTopContext (addContext delta1 $ prettyTCM vs')
]
return (OfType' h a)
where
failure = typeError $ GenericError $ "Expected an argument of the form f e1 e2 .. en"
ensureName f = do
ce <- parseExpr rng f
case ce of
C.Ident{} -> return ()
C.RawApp _ [C.Ident{}] -> return ()
_ -> do
reportSLn "interaction.helper" 10 $ "ce = " ++ show ce
failure
cleanupType arity args t = do
TelV ttel _ <- telView t
let n = size ttel - arity
unless (n >= 0) __IMPOSSIBLE__
return $ evalState (renameVars $ hiding args $ stripUnused n t) args
getBody (A.Let _ _ e) = e
getBody _ = __IMPOSSIBLE__
stripUnused n (El s v) = El s $ strip n v
strip 0 v = v
strip n v = case v of
I.Pi a b -> case stripUnused (n-1) <$> b of
b | absName b == "w" -> I.Pi a b
NoAbs _ b -> unEl b
Abs s b | 0 `freeIn` b -> I.Pi (hide a) (Abs s b)
| otherwise -> strengthen __IMPOSSIBLE__ (unEl b)
_ -> v
renameVars = onNames renameVar
hiding args (El s v) = El s $ hidingTm args v
hidingTm (arg:args) (I.Pi a b) | absName b == "w" =
I.Pi (setHiding (getHiding arg) a) (hiding args <$> b)
hidingTm args (I.Pi a b) = I.Pi a (hiding args <$> b)
hidingTm _ a = a
onNames :: Applicative m => (String -> m String) -> Type -> m Type
onNames f (El s v) = El s <$> onNamesTm f v
onNamesTel :: Applicative f => (String -> f String) -> I.Telescope -> f I.Telescope
onNamesTel f I.EmptyTel = pure I.EmptyTel
onNamesTel f (I.ExtendTel a b) = I.ExtendTel <$> traverse (onNames f) a <*> onNamesAbs f onNamesTel b
onNamesTm f v = case v of
I.Var x es -> I.Var x <$> onNamesElims f es
I.Def q es -> I.Def q <$> onNamesElims f es
I.Con c ci args -> I.Con c ci <$> onNamesArgs f args
I.Lam i b -> I.Lam i <$> onNamesAbs f onNamesTm b
I.Pi a b -> I.Pi <$> traverse (onNames f) a <*> onNamesAbs f onNames b
I.DontCare v -> I.DontCare <$> onNamesTm f v
I.Lit{} -> pure v
I.Sort{} -> pure v
I.Level{} -> pure v
I.MetaV{} -> pure v
I.Dummy{} -> pure v
onNamesElims f = traverse $ traverse $ onNamesTm f
onNamesArgs f = traverse $ traverse $ onNamesTm f
onNamesAbs f = onNamesAbs' f (stringToArgName <.> f . argNameToString)
onNamesAbs' f f' nd (Abs s x) = Abs <$> f' s <*> nd f x
onNamesAbs' f f' nd (NoAbs s x) = NoAbs <$> f' s <*> nd f x
unW "w" = return ".w"
unW s = return s
renameVar "w" = betterName
renameVar s = pure s
betterName = do
arg : args <- get
put args
return $ case arg of
Arg _ (Named _ (A.Var x)) -> show $ A.nameConcrete x
Arg _ (Named (Just x) _) -> argNameToString $ rangedThing x
_ -> "w"
contextOfMeta :: InteractionId -> Rewrite -> TCM [OutputConstraint' Expr Name]
contextOfMeta ii norm = do
info <- getMetaInfo <$> (lookupMeta =<< lookupInteractionId ii)
withMetaInfo info $ do
cxt <- getContext
let n = length cxt
localVars = zipWith raise [1..] cxt
mkLet (x, lb) = do
(tm, !dom) <- getOpen lb
return $ (,) x <$> dom
letVars <- mapM mkLet . Map.toDescList =<< asksTC envLetBindings
mapMaybe visible . reverse <$> mapM out (letVars ++ localVars)
where visible (OfType x y) | not (isNoName x) = Just (OfType' x y)
| otherwise = Nothing
visible _ = __IMPOSSIBLE__
out (Dom{unDom = (x, t)}) = do
t' <- reify =<< normalForm norm t
return $ OfType x t'
typeInCurrent :: Rewrite -> Expr -> TCM Expr
typeInCurrent norm e =
do (_,t) <- wakeIrrelevantVars $ inferExpr e
v <- normalForm norm t
reify v
typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr
typeInMeta ii norm e =
do m <- lookupInteractionId ii
mi <- getMetaInfo <$> lookupMeta m
withMetaInfo mi $
typeInCurrent norm e
withInteractionId :: InteractionId -> TCM a -> TCM a
withInteractionId i ret = do
m <- lookupInteractionId i
withMetaId m ret
withMetaId :: MetaId -> TCM a -> TCM a
withMetaId m ret = do
mv <- lookupMeta m
withMetaInfo' mv ret
introTactic :: Bool -> InteractionId -> TCM [String]
introTactic pmLambda ii = do
mi <- lookupInteractionId ii
mv <- lookupMeta mi
withMetaInfo (getMetaInfo mv) $ case mvJudgement mv of
HasType _ t -> do
t <- reduce =<< piApplyM t =<< getContextArgs
TelV tel' t <- telViewUpTo' (-1) notVisible t
let fallback = do
cubical <- optCubical <$> pragmaOptions
TelV tel _ <- (if cubical then telViewPath else telView) t
reportSDoc "interaction.intro" 20 $ TP.sep
[ "introTactic/fallback"
, "tel' = " TP.<+> prettyTCM tel'
, "tel = " TP.<+> prettyTCM tel
]
case (tel', tel) of
(EmptyTel, EmptyTel) -> return []
_ -> introFun (telToList tel' ++ telToList tel)
case unEl t of
I.Def d _ -> do
def <- getConstInfo d
case theDef def of
Datatype{} -> addContext tel' $ introData t
Record{ recNamedCon = name }
| name -> addContext tel' $ introData t
| otherwise -> addContext tel' $ introRec d
_ -> fallback
_ -> fallback
`catchError` \_ -> return []
_ -> __IMPOSSIBLE__
where
conName [p] = [ c | I.ConP c _ _ <- [namedArg p] ]
conName _ = __IMPOSSIBLE__
showTCM v = show <$> prettyTCM v
introFun tel = addContext tel' $ do
reportSDoc "interaction.intro" 10 $ do "introFun" TP.<+> prettyTCM (telFromList tel)
imp <- showImplicitArguments
let okHiding0 h = imp || h == NotHidden
allHidden = null (filter okHiding0 hs)
okHiding = if allHidden then const True else okHiding0
vars <-
(if allHidden then withShowAllArguments else id) $
mapM showTCM [ setHiding h $ defaultArg $ var i :: Arg Term
| (h, i) <- zip hs $ downFrom n
, okHiding h
]
if pmLambda
then return [ unwords $ ["λ", "{"] ++ vars ++ ["→", "?", "}"] ]
else return [ unwords $ ["λ"] ++ vars ++ ["→", "?"] ]
where
n = size tel
hs = map getHiding tel
tel' = telFromList [ fmap makeName b | b <- tel ]
makeName ("_", t) = ("x", t)
makeName (x, t) = (x, t)
introData t = do
let tel = telFromList [defaultDom ("_", t)]
pat = [defaultArg $ unnamed $ debruijnNamedVar "c" 0]
r <- splitLast CoInductive tel pat
case r of
Left err -> return []
Right cov -> mapM showTCM $ concatMap (conName . scPats) $ splitClauses cov
introRec :: QName -> TCM [String]
introRec d = do
hfs <- getRecordFieldNames d
fs <- ifM showImplicitArguments
(return $ map unArg hfs)
(return [ unArg a | a <- hfs, visible a ])
let e = C.Rec noRange $ for fs $ \ f ->
Left $ C.FieldAssignment f $ C.QuestionMark noRange Nothing
return [ prettyShow e ]
atTopLevel :: TCM a -> TCM a
atTopLevel m = inConcreteMode $ do
let err = typeError $ GenericError "The file has not been loaded yet."
caseMaybeM (useTC stCurrentModule) err $ \ current -> do
caseMaybeM (getVisitedModule $ toTopLevelModuleName current) __IMPOSSIBLE__ $ \ mi -> do
let scope = iInsideScope $ miInterface mi
tel <- lookupSection current
let names :: [A.Name]
names = map localVar $ filter ((LetBound /=) . localBinder) $ map snd $ reverse $ scopeLocals scope
let types :: [Dom I.Type]
types = map (snd <$>) $ telToList tel
gamma :: ListTel' A.Name
gamma = fromMaybe __IMPOSSIBLE__ $
zipWith' (\ x dom -> (x,) <$> dom) names types
reportSDoc "interaction.top" 20 $ TP.vcat
[ "BasicOps.atTopLevel"
, " names = " TP.<+> TP.sep (map prettyA names)
, " types = " TP.<+> TP.sep (map prettyTCM types)
]
M.withCurrentModule current $
withScope_ scope $
addContext gamma $ do
cp <- viewTC eCurrentCheckpoint
stModuleCheckpoints `modifyTCLens` fmap (const cp)
m
parseName :: Range -> String -> TCM C.QName
parseName r s = do
m <- parseExpr r s
case m of
C.Ident m -> return m
C.RawApp _ [C.Ident m] -> return m
_ -> typeError $
GenericError $ "Not an identifier: " ++ show m ++ "."
isQName :: C.Expr -> Maybe C.QName
isQName m = do
case m of
C.Ident m -> return m
C.RawApp _ [C.Ident m] -> return m
_ -> Nothing
moduleContents
:: Rewrite
-> Range
-> String
-> TCM ([C.Name], [(C.Name, Type)])
moduleContents norm rng s = traceCall ModuleContents $ do
e <- parseExpr rng s
case isQName e of
Nothing -> getRecordContents norm e
Just x -> do
ms :: [AbstractModule] <- scopeLookup x <$> getScope
if null ms then getRecordContents norm e else getModuleContents norm x
getRecordContents
:: Rewrite
-> C.Expr
-> TCM ([C.Name], [(C.Name, Type)])
getRecordContents norm ce = do
e <- toAbstract ce
(_, t) <- inferExpr e
let notRecordType = typeError $ ShouldBeRecordType t
(q, vs, defn) <- fromMaybeM notRecordType $ isRecordType t
case defn of
Record{ recFields = fs, recTel = tel } -> do
let xs = map (nameConcrete . qnameName . unArg) fs
doms = telToList $ apply tel vs
ts <- mapM (normalForm norm) $ map (snd . unDom) doms
return ([], zip xs ts)
_ -> __IMPOSSIBLE__
getModuleContents
:: Rewrite
-> C.QName
-> TCM ([C.Name], [(C.Name, Type)])
getModuleContents norm m = do
modScope <- getNamedScope . amodName =<< resolveModule m
let modules :: ThingsInScope AbstractModule
modules = exportedNamesInScope modScope
names :: ThingsInScope AbstractName
names = exportedNamesInScope modScope
xns = [ (x,n) | (x, ns) <- Map.toList names, n <- ns ]
types <- forM xns $ \(x, n) -> do
d <- getConstInfo $ anameName n
t <- normalForm norm =<< (defType <$> instantiateDef d)
return (x, t)
return (Map.keys modules, types)
whyInScope :: String -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule])
whyInScope s = do
x <- parseName noRange s
scope <- getScope
return ( lookup x $ map (first C.QName) $ scopeLocals scope
, scopeLookup x scope
, scopeLookup x scope )