module Agda.Interaction.BasicOps where
import Control.Monad.Error
import Control.Monad.Reader
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.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.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
parseExprIn :: InteractionId -> Range -> String -> TCM Expr
parseExprIn ii rng s = do
mId <- lookupInteractionId ii
updateMetaVarRange mId rng
mi <- getMetaInfo <$> lookupMeta mId
let pos = case rStart (getRange mi) of
Just pos -> pos
Nothing -> __IMPOSSIBLE__
e <- liftIO $ parsePosString exprParser pos 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 (Arg NotHidden $ unnamed metaVar)
evalInCurrent :: Expr -> TCM Expr
evalInCurrent e =
do t <- newTypeMeta_
v <- checkExpr e t
v' <- etaContract =<< 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 = etaContract =<< reduce t
rewrite Normalised t = etaContract =<< normalise t
data OutputForm a b
= OfType b a | CmpInType Comparison a b b
| JustType b | CmpTypes 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
JustType 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 (CmpTypes cmp e e') = CmpTypes 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 (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 (CmpTypes 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 <*> toConcrete t
toConcrete (JustType e) = JustType <$> toConcrete e
toConcrete (JustSort e) = JustSort <$> toConcrete e
toConcrete (CmpInType cmp t e e') =
CmpInType cmp <$> toConcrete t <*> toConcrete e <*> toConcrete e'
toConcrete (CmpTypes cmp e e') = CmpTypes cmp <$> toConcrete e <*> toConcrete e'
toConcrete (CmpTeles cmp e e') = CmpTeles cmp <$> toConcrete e <*> toConcrete e'
toConcrete (CmpSorts cmp e e') = CmpSorts cmp <$> toConcrete e <*> toConcrete e'
toConcrete (Guard o os) = Guard <$> toConcrete o <*> toConcrete os
toConcrete (Assign m e) = Assign <$> toConcrete m <*> toConcrete e
toConcrete (TypedAssign m e a) = TypedAssign <$> toConcrete m <*> toConcrete e <*> toConcrete a
toConcrete (IsEmptyType a) = IsEmptyType <$> toConcrete 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 <*> toConcrete 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
OfType i <$> reify (t `piApply` 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
typeOfMetas :: Rewrite -> TCM ([OutputForm Expr InteractionId],[OutputForm Expr MetaId])
typeOfMetas norm = liftTCM $
do ips <- getInteractionPoints
js <- mapM (typeOfMeta norm) ips
hidden <- hiddenMetas
return $ (js,hidden)
where hiddenMetas =
do is <- getInteractionMetas
store <- Map.filterWithKey (openAndImplicit is) <$> getMetaStore
let mvs = Map.keys store
mapM (typeOfMetaMI norm) mvs
where
openAndImplicit is x (MetaVar _ _ _ M.Open _) = x `notElem` is
openAndImplicit is x (MetaVar _ _ _ (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 <- normalise =<< piApply t <$> getContextArgs
case unEl t of
I.Def d _ -> do
def <- getConstInfo d
case theDef def of
Datatype{} -> introData t
Record{} -> introRec d
_ -> return []
_ -> case telView t of
TelV EmptyTel _ -> return []
TelV 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 (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 [Arg NotHidden ("_", t)]
perm = idP 1
pat = [Arg NotHidden (I.VarP "c")]
r <- split 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 snd hfs)
(return [ f | (NotHidden, f) <- hfs ])
return
[ concat $
"record " :
zipWith (\c f -> unwords [c, show f, "= ?"])
("{":repeat ";") fs ++
[" }"]
]