module Agda.Auto.Auto (auto) where
import Control.Monad.Error
import Control.Monad.State
import System.IO.Unsafe (unsafePerformIO)
import Data.List
import Data.Generics
import Data.Map (Map)
import qualified Data.Map as Map
import Data.IORef
import qualified System.Timeout
import Data.Maybe (catMaybes)
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.MetaVars
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Signature
import Agda.TypeChecking.Monad.State (getScope)
import Agda.TypeChecking.Substitute
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Position
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Common
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Translation.AbstractToConcrete (abstractToConcrete, abstractToConcrete_, makeEnv)
import Agda.Interaction.Monad
import Agda.Interaction.BasicOps hiding (refine)
import Agda.Auto.Convert
import Agda.Auto.NarrowingSearch
import Agda.Auto.Syntax
import Agda.Auto.Typecheck
import Agda.Auto.Print
getName :: A.Expr -> Maybe (Bool, I.QName)
getName (A.ScopedExpr _ e) = getName e
getName (A.Def qname) = Just (False, qname)
getName (A.Con qname) = Just (True, head $ I.unAmbQ qname)
getName _ = Nothing
dispmsg msg = return ([], Just msg)
auto :: InteractionId -> Range -> String -> TCM ([(InteractionId, String)], Maybe String)
auto ii rng argstr = liftTCM $
do let (hints, timeout, pick, mode) = parseargs argstr
ahints <- mapM (parseExprIn ii rng) hints
case mapM getName ahints of
Nothing -> dispmsg "Hints must be a list of constant names"
Just ehints -> do
mi <- lookupInteractionId ii
(myhints, tccons, eqcons, cmap) <- tomy mi ehints
let (mainm, _, _, _) = tccons Map.! mi
case mode of
MNormal listmode -> do
sols <- liftIO $ newIORef []
nsol <- liftIO $ newIORef (if listmode then (pick + 10) else (pick + 1))
let hsol = if listmode then do
nsol' <- readIORef nsol
when (nsol' <= 10) $ mapM (\(m, _, _, _) -> frommy (Meta m)) (Map.elems tccons) >>= \trms -> modifyIORef sols (trms :)
else do
nsol' <- readIORef nsol
when (nsol' == 1) $ mapM (\(m, _, _, _) -> frommy (Meta m)) (Map.elems tccons) >>= \trms -> writeIORef sols [trms]
ticks <- liftIO $ newIORef 0
res <- liftIO $ System.Timeout.timeout (timeout * 1000000) $
let r d =
do
let tc (m, mytype, mylocalVars) isdep = tcExp isdep (map (\x -> (NoId, closify x)) mylocalVars) (closify mytype) (Meta m)
initprop = foldl (\x (ineq, e, i) -> mpret $ And Nothing x (comp ineq (closify e) (closify i)))
(foldl (\x (m, mt, mlv, _) -> mpret $ And Nothing x (tc (m, mt, mlv) (not $ hequalMetavar m mainm)))
(mpret OK)
(Map.elems tccons)
)
eqcons
depreached <- topSearch ticks nsol hsol undefined False (RIEnv myhints) (initprop) d 1
nsol' <- readIORef nsol
if nsol' /= 0 && depreached then
r (d + 1)
else
return depreached
in r 0
let getsols sol = do
exprs <- mapM (\(mi, e) -> do
mv <- lookupMeta mi
expr <- withMetaInfo (getMetaInfo mv) $ reify e
return (mi, expr)
) (zip (Map.keys tccons) sol)
let r :: I.MetaId -> StateT [I.MetaId] TCM [(I.MetaId, A.Expr)]
r midx = do
let (m, _, _, deps) = tccons Map.! midx
asolss <- mapM r deps
dones <- get
asols <- if (midx `notElem` dones) then do
put (midx : dones)
return [(midx, let Just e = lookup midx exprs in e)]
else
return []
return $ concat asolss ++ asols
(asols, _) <- runStateT (r mi) []
return asols
iis <- getInteractionPoints
riis <- mapM (\ii -> lookupInteractionId ii >>= \mi -> return (mi, ii)) iis
if listmode then do
rsols <- liftM reverse $ liftIO $ readIORef sols
if null rsols then do
nsol' <- liftIO $ readIORef nsol
dispmsg $ insuffsols (pick + 10 nsol')
else do
aexprss <- mapM getsols rsols
cexprss <- mapM (mapM (\(mi, e) -> lookupMeta mi >>= \mv -> withMetaInfo (getMetaInfo mv) $ abstractToConcrete_ e >>= \e' -> return (mi, e'))) aexprss
let disp [(_, cexpr)] = show cexpr
disp cexprs = concat (map (\(mi, cexpr) -> case lookup mi riis of {Nothing -> show mi; Just ii -> show ii} ++ " := " ++ show cexpr ++ " ") cexprs)
dispmsg $ "Listing solution(s) " ++ show pick ++ "-" ++ show (pick + length rsols 1) ++ "\n" ++
unlines (map (\(x, y) -> show y ++ " " ++ disp x) $ zip cexprss [pick..])
else
case res of
Nothing -> do
nsol' <- liftIO $ readIORef nsol
dispmsg $ insuffsols (pick + 1 nsol') ++ " at time out (" ++ show timeout ++ "s)"
Just depthreached -> do
ticks <- liftIO $ readIORef ticks
rsols <- liftIO $ readIORef sols
case rsols of
[] -> do
nsol' <- liftIO $ readIORef nsol
dispmsg $ insuffsols (pick + 1 nsol')
(term : _) -> do
exprs <- getsols term
giveress <-
mapM (\(mi, expr) ->
case lookup mi riis of
Nothing -> giveExpr mi expr >>= \_ -> return Nothing
Just ii' -> do (ae, []) <- give ii' Nothing expr
mv <- lookupMeta mi
let scope = getMetaScope mv
ce = abstractToConcrete (makeEnv scope) ae
let cmnt = if ii' == ii then " {- by agsy" ++ (if null argstr then "" else " (" ++ argstr ++ ")") ++ " -}" else ""
return $ Just (ii', show ce ++ cmnt)
) exprs
let msg = if length exprs == 1 then
Nothing
else
Just $ "Also gave solution(s) for hole(s)" ++
concatMap (\(mi', _) ->
if mi' == mi then "" else (" " ++ case lookup mi' riis of {Nothing -> show mi'; Just ii -> show ii})
) exprs
return (catMaybes giveress, msg)
MDumpProblem (Just dumpfile) -> do
tcconss <- mapM (\(m, mytype, mylocalVars, _) -> do
let typ = foldl (\x y -> NotM $ Pi Agda.Auto.Syntax.NotHidden undefined y (Abs NoId x)) mytype mylocalVars
trm = foldl (\x _ -> NotM $ Lam Agda.Auto.Syntax.NotHidden (Abs NoId x)) (Meta m) mylocalVars
typs <- liftIO $ printExp [] typ
trms <- liftIO $ printExp [] trm
return $ (if hequalMetavar m mainm then "the_prob : " else "extra_con : ") ++ typs ++ " {\n = " ++ trms ++ ";\n};\n\n"
) (Map.elems tccons)
constss <- liftIO $ mapM (\(_, (TMAll, c)) -> printConst c >>= \s -> return $ s ++ "\n") (Map.toList cmap)
eqconss <- liftIO $ mapM (\(ineq, e1, e2) -> do
pe1 <- printExp [] e1
pe2 <- printExp [] e2
return $ "-- " ++ pe1 ++ (if ineq then " >= " else " == ") ++ pe2
) eqcons
let probs = concat constss ++ concat tcconss ++ (if null ehints then "" else ("-- hints: " ++ concatMap (\(_, n) -> " " ++ show n) ehints) ++ "\n") ++
"-- " ++ show (length eqcons) ++ " eqcons\n" ++ unlines eqconss
liftIO $ writeFile dumpfile probs
dispmsg $ "Dumping problem to " ++ dumpfile
MDumpProblem Nothing -> do
mv <- lookupMeta mi
let HasType _ tt = mvJudgement mv
minfo = getMetaInfo mv
localVars = map (snd . unArg . ctxEntry) . envContext . clEnv $ minfo
withMetaInfo minfo $ do
vs <- getContextArgs
let targettype = tt `piApply` vs
targettype <- rewrite Normalised targettype
localVars <- mapM (rewrite Normalised) localVars
dispmsg $ "Target type: " ++ show (localVars, targettype)
insuffsols 0 = "No solution found"
insuffsols n = "Only " ++ show n ++ " solution(s) were found"
data Mode = MNormal Bool
| MDumpProblem (Maybe String)
parseargs s =
let r ("-t" : timeout : ws) (_, pick, mode) =
r ws (read timeout, pick, mode)
r ("-s" : pick : ws) (timeout, _, mode) =
r ws (timeout, read pick, mode)
r ("-dump" : dumpfile : ws) (timeout, pick, _) =
r ws (timeout, pick, MDumpProblem (Just dumpfile))
r ("-dumpa" : ws) (timeout, pick, _) =
r ws (timeout, pick, MDumpProblem Nothing)
r ("-l" : ws) (timeout, pick, _) =
r ws (timeout, pick, MNormal True)
r (h : ws) x =
let (hints, timeout, pick, mode) = r ws x
in (h : hints, timeout, pick, mode)
r [] (x,y,z) = ([],x,y,z)
in r (words s) (1, 0, MNormal False)