module Agda.Interaction.BasicOps where
import Control.Monad.Error
import Control.Monad.Reader
import Control.Monad.State
import qualified Data.Map as Map
import Data.Map (Map)
import Data.List
import Data.Maybe
import Agda.Interaction.Monad
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Position
import Agda.Syntax.Abstract as A hiding (Open)
import Agda.Syntax.Common
import Agda.Syntax.Info(ExprInfo(..),MetaInfo(..))
import Agda.Syntax.Internal as I
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(..))
import Agda.Syntax.Parser
import Agda.TypeChecker
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Monad as M
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.EtaContract (etaContract)
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Records
import Agda.TypeChecking.Pretty (prettyTCM)
import qualified Agda.TypeChecking.Pretty as TP
import Agda.Utils.Monad
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 = liftIO $ parsePosString exprParser pos s
where
pos = case rStart rng of
Just pos -> pos
Nothing -> startPos Nothing
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 :: MetaId -> Expr -> TCM Expr
giveExpr mi e =
do mv <- lookupMeta mi
withMetaInfo (getMetaInfo mv) $ metaTypeCheck' mi e mv
where metaTypeCheck' mi e mv =
case mvJudgement mv of
HasType _ t -> do
ctx <- getContextArgs
let t' = t `piApply` ctx
v <- checkExpr e t'
case mvInstantiation mv of
InstV v' ->
addConstraints =<< equalTerm t' v (v' `apply` ctx)
_ -> updateMeta mi v
reify v
IsSort _ -> __IMPOSSIBLE__
give :: InteractionId -> Maybe Range -> Expr -> TCM (Expr,[InteractionId])
give ii mr e = liftTCM $ do
mi <- lookupInteractionId ii
mis <- getInteractionPoints
r <- getInteractionRange ii
updateMetaVarRange mi $ maybe r id mr
giveExpr mi e `catchError` \err -> case errError err of
PatternErr _ -> do
err <- withInteractionId ii $ TP.text "Failed to give" TP.<+> prettyTCM e
typeError $ GenericError $ show err
_ -> throwError err
removeInteractionPoint ii
mis' <- getInteractionPoints
return (e, mis' \\ mis)
addDecl :: Declaration -> TCM ([InteractionId])
addDecl d = do
mis <- getInteractionPoints
checkDecl d
mis' <- getInteractionPoints
return (mis' \\ mis)
refine :: InteractionId -> Maybe Range -> Expr -> TCM (Expr,[InteractionId])
refine ii mr e =
do mi <- lookupInteractionId ii
mv <- lookupMeta mi
let range = maybe (getRange mv) id mr
let scope = M.getMetaScope mv
tryRefine 10 range scope e
where tryRefine :: Int -> Range -> ScopeInfo -> Expr -> TCM (Expr,[InteractionId])
tryRefine nrOfMetas r scope e = try nrOfMetas e
where try 0 e = throwError (strMsg "Can not refine")
try n e = give ii (Just r) e `catchError` (\_ -> try (n1) (appMeta e))
appMeta :: Expr -> Expr
appMeta e =
let metaVar = QuestionMark
$ Agda.Syntax.Info.MetaInfo
{ Agda.Syntax.Info.metaRange = r
, Agda.Syntax.Info.metaScope = scope { scopePrecedence = ArgumentCtx }
, metaNumber = Nothing
}
in App (ExprRange $ r) e (defaultArg $ unnamed metaVar)
evalInCurrent :: Expr -> TCM Expr
evalInCurrent e =
do t <- newTypeMeta_
v <- checkExpr e t
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 | Normalised
rewrite AsIs t = return t
rewrite Instantiated t = return t
rewrite HeadNormal t = reduce t
rewrite Normalised t = normalise t
data OutputForm a b
= OfType b a | CmpInType Comparison a b b
| CmpTerms [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 (OutputForm a b) [OutputForm a b]
| Assign b a | TypedAssign b a a
| IsEmptyType a
data OutputForm' a b = OfType' { ofName :: b
, ofExpr :: a
}
outputFormId :: OutputForm a b -> b
outputFormId o = case o of
OfType i _ -> i
CmpInType _ _ i _ -> i
CmpTerms _ _ (i:_) _ -> i
CmpTerms _ _ [] _ -> __IMPOSSIBLE__
JustType i -> i
CmpLevels _ i _ -> i
CmpTypes _ i _ -> i
CmpTeles _ i _ -> i
JustSort i -> i
CmpSorts _ i _ -> i
Guard o _ -> outputFormId o
Assign i _ -> i
TypedAssign i _ _ -> i
IsEmptyType _ -> __IMPOSSIBLE__
instance Functor (OutputForm a) where
fmap f (OfType e t) = OfType (f e) t
fmap f (JustType e) = JustType (f e)
fmap f (JustSort e) = JustSort (f e)
fmap f (CmpInType cmp t e e') = CmpInType cmp t (f e) (f e')
fmap f (CmpTerms cmp t e e') = CmpTerms cmp t (map f e) (map f e')
fmap f (CmpTypes cmp e e') = CmpTypes cmp (f e) (f e')
fmap f (CmpLevels cmp e e') = CmpLevels cmp (f e) (f e')
fmap f (CmpTeles cmp e e') = CmpTeles cmp (f e) (f e')
fmap f (CmpSorts cmp e e') = CmpSorts cmp (f e) (f e')
fmap f (Guard o os) = Guard (fmap f o) (fmap (fmap f) os)
fmap f (Assign m e) = Assign (f m) e
fmap f (TypedAssign m e a) = TypedAssign (f m) e a
fmap f (IsEmptyType a) = IsEmptyType a
instance Reify Constraint (OutputForm Expr Expr) where
reify (ValueCmp cmp t u v) = CmpInType cmp <$> reify t <*> reify u <*> reify v
reify (ArgsCmp cmp t u v) = CmpTerms cmp <$> reify t
<*> mapM (reify . unArg) u
<*> mapM (reify . unArg) v
reify (LevelCmp cmp t t') = CmpLevels cmp <$> reify t <*> reify t'
reify (TypeCmp cmp t t') = CmpTypes cmp <$> reify t <*> reify t'
reify (TelCmp 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 cs) = do
o <- reify c
os <- mapM (withConstraint reify) cs
return $ Guard o os
reify (UnBlock m) = do
mi <- mvInstantiation <$> lookupMeta m
case mi of
BlockedConst t -> do
e <- reify t
m' <- reify (MetaV m [])
return $ Assign m' e
PostponedTypeCheckingProblem cl -> enterClosure cl $ \(e, a, _) -> do
a <- reify a
m' <- reify (MetaV m [])
return $ TypedAssign m' e a
Open{} -> __IMPOSSIBLE__
InstS{} -> __IMPOSSIBLE__
InstV{} -> __IMPOSSIBLE__
reify (IsEmpty a) = IsEmptyType <$> reify a
showComparison :: Comparison -> String
showComparison CmpEq = " = "
showComparison CmpLeq = " =< "
instance (Show a,Show b) => Show (OutputForm a b) where
show (OfType e t) = show e ++ " : " ++ show t
show (JustType e) = "Type " ++ show e
show (JustSort e) = "Sort " ++ show e
show (CmpInType cmp t e e') = show e ++ showComparison cmp ++ show e' ++ " : " ++ show t
show (CmpTerms cmp t e e') = show e ++ "~~" ++ show e' ++ " : " ++ show t
show (CmpTypes cmp t t') = show t ++ showComparison cmp ++ show t'
show (CmpLevels cmp t t') = show t ++ showComparison cmp ++ show t'
show (CmpTeles cmp t t') = show t ++ showComparison cmp ++ show t'
show (CmpSorts cmp s s') = show s ++ showComparison cmp ++ show s'
show (Guard o os) = show o ++ " if " ++ show os
show (Assign m e) = show m ++ " := " ++ show e
show (TypedAssign m e a) = show m ++ " := " ++ show e ++ " : " ++ show a
show (IsEmptyType a) = "Is empty: " ++ show a
instance (ToConcrete a c, ToConcrete b d) =>
ToConcrete (OutputForm a b) (OutputForm 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 (CmpTerms cmp t e e') =
CmpTerms cmp <$> toConcreteCtx TopCtx t <*> mapM toConcrete e <*> mapM toConcrete 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 os) = Guard <$> toConcrete o <*> toConcrete os
toConcrete (Assign m e) = Assign <$> toConcrete m <*> toConcreteCtx TopCtx e
toConcrete (TypedAssign m e a) = TypedAssign <$> toConcrete m <*> toConcreteCtx TopCtx e
<*> toConcreteCtx TopCtx a
toConcrete (IsEmptyType a) = IsEmptyType <$> toConcreteCtx TopCtx a
instance (Pretty a, Pretty b) => Pretty (OutputForm' a b) where
pretty (OfType' e t) = pretty e <+> text ":" <+> pretty t
instance (ToConcrete a c, ToConcrete b d) =>
ToConcrete (OutputForm' a b) (OutputForm' c d) where
toConcrete (OfType' e t) = OfType' <$> toConcrete e <*> toConcreteCtx TopCtx t
instance ToConcrete InteractionId C.Expr where
toConcrete (InteractionId i) = return $ C.QuestionMark noRange (Just i)
instance ToConcrete MetaId C.Expr where
toConcrete (MetaId i) = return $ C.Underscore noRange (Just i)
judgToOutputForm :: Judgement a c -> OutputForm a c
judgToOutputForm (HasType e t) = OfType e t
judgToOutputForm (IsSort s) = JustSort s
getConstraint :: Int -> TCM (OutputForm Expr Expr)
getConstraint ci =
do cc <- lookupConstraint ci
cc <- reduce cc
withConstraint reify cc
getConstraints :: TCM [OutputForm C.Expr C.Expr]
getConstraints = liftTCM $ do
cs <- mapM (withConstraint (abstractToConcrete_ <.> reify)) =<< reduce =<< M.getConstraints
ss <- mapM toOutputForm =<< getSolvedInteractionPoints
return $ ss ++ cs
where
toOutputForm (ii, mi, e) = do
mv <- getMetaInfo <$> lookupMeta mi
withMetaInfo mv $ do
let m = QuestionMark $ MetaInfo noRange emptyScopeInfo (Just $ fromIntegral ii)
abstractToConcrete_ $ Assign m e
getSolvedInteractionPoints :: TCM [(InteractionId, MetaId, Expr)]
getSolvedInteractionPoints = do
is <- getInteractionPoints
concat <$> mapM solution is
where
solution i = do
m <- lookupInteractionId i
mv <- lookupMeta m
withMetaInfo (getMetaInfo mv) $ do
args <- getContextArgs
scope <- getScope
let sol v = do e <- reify v; return [(i, m, ScopedExpr scope e)]
unsol = return []
case mvInstantiation mv of
InstV{} -> sol (MetaV m args)
InstS{} -> sol (Sort $ MetaS m args)
Open{} -> unsol
BlockedConst{} -> unsol
PostponedTypeCheckingProblem{} -> unsol
typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputForm Expr MetaId)
typeOfMetaMI norm mi =
do mv <- lookupMeta mi
withMetaInfo (getMetaInfo mv) $
rewriteJudg mv (mvJudgement mv)
where
rewriteJudg mv (HasType i t) = do
t <- rewrite norm t
vs <- getContextArgs
reportSDoc "interactive.meta" 10 $ TP.vcat
[ TP.text $ unwords ["permuting", show i, "with", show $ mvPermutation mv]
, TP.nest 2 $ TP.vcat
[ TP.text "len =" TP.<+> TP.text (show $ length vs)
, TP.text "args =" TP.<+> prettyTCM vs
, TP.text "t =" TP.<+> prettyTCM t
]
]
OfType i <$> reify (t `piApply` permute (takeP (size vs) $ mvPermutation mv) vs)
rewriteJudg mv (IsSort i) = return $ JustSort i
typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputForm Expr InteractionId)
typeOfMeta norm ii =
do mi <- lookupInteractionId ii
out <- typeOfMetaMI norm mi
return $ fmap (\_ -> ii) out
typesOfVisibleMetas :: Rewrite -> TCM [OutputForm Expr InteractionId]
typesOfVisibleMetas norm =
liftTCM $ mapM (typeOfMeta norm) =<< getInteractionPoints
typesOfHiddenMetas :: Rewrite -> TCM [OutputForm Expr MetaId]
typesOfHiddenMetas norm = liftTCM $ do
is <- getInteractionMetas
store <- Map.filterWithKey (openAndImplicit is) <$> getMetaStore
mapM (typeOfMetaMI norm) $ Map.keys store
where
openAndImplicit is x (MetaVar{mvInstantiation = M.Open}) = x `notElem` is
openAndImplicit is x (MetaVar{mvInstantiation = M.BlockedConst _}) = True
openAndImplicit _ _ _ = False
contextOfMeta :: InteractionId -> Rewrite -> TCM [OutputForm' Expr Name]
contextOfMeta ii norm = do
info <- getMetaInfo <$> (lookupMeta =<< lookupInteractionId ii)
let localVars = map ctxEntry . envContext . clEnv $ info
withMetaInfo info $ gfilter visible <$> reifyContext localVars
where gfilter p = catMaybes . map p
visible (OfType x y) | show x /= "_" = Just (OfType' x y)
| otherwise = Nothing
visible _ = __IMPOSSIBLE__
reifyContext xs = reverse <$> zipWithM out [1..] xs
out i (Arg h _ (x, t)) = escapeContext i $ do
t' <- reify =<< rewrite norm t
return $ OfType x t'
typeInCurrent :: Rewrite -> Expr -> TCM Expr
typeInCurrent norm e =
do (_,t) <- inferExpr e
v <- rewrite 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
info <- lookupMeta m
withMetaInfo (mvInfo info) ret
introTactic :: InteractionId -> TCM [String]
introTactic ii = do
mi <- lookupInteractionId ii
mv <- lookupMeta mi
withMetaInfo (getMetaInfo mv) $ case mvJudgement mv of
HasType _ t -> do
t <- reduce =<< piApply t <$> getContextArgs
case unEl t of
I.Def d _ -> do
def <- getConstInfo d
case theDef def of
Datatype{} -> introData t
Record{ recNamedCon = name }
| name -> introData t
| otherwise -> introRec d
_ -> return []
_ -> do
TelV tel _ <- telView t
case tel of
EmptyTel -> return []
tel -> introFun tel
`catchError` \_ -> return []
_ -> __IMPOSSIBLE__
where
conName [Arg _ _ (I.ConP c _ _)] = [c]
conName [_] = []
conName _ = __IMPOSSIBLE__
showTCM v = show <$> prettyTCM v
introFun tel = addCtxTel tel' $ do
imp <- showImplicitArguments
let okHiding h = imp || h == NotHidden
vars <- mapM showTCM [ Arg h Relevant (I.Var i [])
| (h, i) <- zip hs $ reverse [0..n 1]
, okHiding h
]
return [ unwords $ ["λ"] ++ vars ++ ["→", "?"] ]
where
n = size tel
hs = map argHiding $ telToList tel
tel' = telFromList [ fmap makeName b | b <- telToList tel ]
makeName ("_", t) = ("x", t)
makeName (x, t) = (x, t)
introData t = do
let tel = telFromList [defaultArg ("_", t)]
perm = idP 1
pat = [defaultArg (I.VarP "c")]
r <- split CoInductive tel perm pat 0
case r of
Left err -> return []
Right cs -> mapM showTCM $ concatMap (conName . scPats) cs
introRec d = do
hfs <- getRecordFieldNames d
fs <- ifM showImplicitArguments
(return $ map unArg hfs)
(return [ f | (Arg NotHidden _ f) <- hfs ])
return
[ concat $
"record {" :
intersperse ";" (map (\ f -> show f ++ " = ?") fs) ++
["}"]
]
atTopLevel :: TCM a -> TCM a
atTopLevel m = do
mCurrent <- stCurrentModule <$> get
case mCurrent of
Nothing -> typeError $
GenericError "The file has not been loaded yet."
Just current -> do
r <- getVisitedModule (toTopLevelModuleName current)
case r of
Nothing -> __IMPOSSIBLE__
Just mi -> do
tel <- lookupSection current
M.withCurrentModule current $
withScope_ (iInsideScope $ miInterface mi) $
addCtxTel tel $
m
moduleContents :: Range
-> String
-> TCM ([C.Name], [(C.Name, Type)])
moduleContents rng s = do
m <- parseExpr rng s
m <- case m of
C.Ident m -> return m
C.RawApp _ [C.Ident m] -> return m
_ -> typeError $
GenericError $ "Not a module name: " ++ show m ++ "."
modScope <- getNamedScope . amodName =<< resolveModule m
let modules :: ThingsInScope AbstractModule
modules = exportedNamesInScope modScope
names :: ThingsInScope AbstractName
names = exportedNamesInScope modScope
types <- mapM (\(x, n) -> do
d <- getConstInfo $ anameName n
t <- defType <$> instantiateDef d
return (x, t))
(concatMap (\(x, ns) -> map ((,) x) ns) $
Map.toList names)
return (Map.keys modules, types)