module Agda.Auto.Auto (auto) where
import Agda.Utils.Impossible
#include "../undefined.h"
import Control.Monad.Error
import Control.Monad.State
import System.IO.Unsafe (unsafePerformIO)
import Data.List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.IORef
import qualified System.Timeout
import Data.Maybe (catMaybes)
import Agda.Utils.Permutation (permute, takeP)
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 Agda.Syntax.Abstract.Pretty (prettyA)
import qualified Text.PrettyPrint as PP
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, runAbsToCon, toConcrete)
import Agda.Interaction.BasicOps hiding (refine)
import Agda.Interaction.MakeCase (findClause)
import Agda.TypeChecking.Reduce (normalise)
import qualified Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad (withCurrentModule)
import qualified Agda.Syntax.Abstract.Name as AN
import qualified Agda.TypeChecking.Monad.Base as MB
import Agda.TypeChecking.EtaContract (etaContract)
import Agda.Auto.Convert
import Agda.Auto.NarrowingSearch
import Agda.Auto.Syntax
import Agda.Auto.SearchControl
import Agda.Auto.Typecheck
import Agda.Auto.CaseSplit
insertAbsurdPattern [] = []
insertAbsurdPattern s@(_:_) | take (length abspatvarname) s == abspatvarname = "()" ++ drop (length abspatvarname) s
insertAbsurdPattern (c:s) = c : insertAbsurdPattern s
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 (Left [], Just msg)
auto :: InteractionId -> Range -> String -> TCM (Either [(InteractionId, String)] (Either [String] String), Maybe String)
auto ii rng argstr = liftTCM $ do
let (hints, timeout, pick, mode, hintmode) = parseargs argstr
ahints <- mapM (parseExprIn ii rng) (case mode of {MRefine{} -> []; _ -> hints})
eqstuff <- liftM (maybe Nothing (mapM getName)) $
catchError (liftM Just $ mapM (parseExprIn ii rng) ["_≡_", "begin_", "_≡⟨_⟩_", "_∎", "sym", "cong"]) (\_ -> return Nothing)
case mapM getName ahints of
Nothing -> dispmsg "Hints must be a list of constant names"
Just ehints -> do
mi <- lookupInteractionId ii
thisdefinfo <- findClauseDeep mi
ehints <- liftM (ehints ++) $ autohints hintmode mi (case thisdefinfo of {Just (def, _, _) -> Just def; Nothing -> Nothing})
mrectyp <- case thisdefinfo of
Nothing -> return []
Just (def, _, _) -> do
recdef <- getConstInfo def
let rectyp = MB.defType recdef
rectyp <- normalise rectyp
return [rectyp]
let ehints' = ehints ++ maybe [] id eqstuff
(myhints', mymrectyp, tccons, eqcons, cmap) <- tomy mi ehints' mrectyp
let myhints = take (length myhints' (length ehints' length ehints)) myhints'
meqr = case eqstuff of
Nothing -> Nothing
Just _ -> let [c1, c2, c3, c4, c5, c6] = drop (length myhints' (length ehints' length ehints)) myhints'
in Just $ EqReasoningConsts c1 c2 c3 c4 c5 c6
let tcSearchSC isdep ctx typ trm =
(case meqr of
Nothing -> id
Just eqr -> mpret . Sidecondition (calcEqRState eqr trm)
)
(tcSearch isdep ctx typ trm)
let (mainm, _, _, _) = tccons Map.! mi
case mode of
MNormal listmode disprove -> do
sols <- liftIO $ newIORef ([] :: [[I.Term]])
nsol <- liftIO $ newIORef (if listmode then (pick + 10) else (pick + 1))
let hsol =
if listmode then do
nsol' <- readIORef nsol
when (nsol' <= 10) $ runErrorT (mapM (\(m, _, _, _) -> frommy (Meta m)) (Map.elems tccons)) >>= \trms -> case trms of {Left{} -> writeIORef nsol $! nsol' + 1; Right trms -> modifyIORef sols (trms :)}
else do
nsol' <- readIORef nsol
when (nsol' == 1) $ runErrorT (mapM (\(m, _, _, _) -> frommy (Meta m)) (Map.elems tccons)) >>= \trms -> case trms of {Left{} -> writeIORef nsol $! nsol' + 1; Right trms -> writeIORef sols [trms]}
ticks <- liftIO $ newIORef 0
let exsearch initprop recinfo defdfv = liftIO $ System.Timeout.timeout (timeout * 1000000) (
let r d = do
let rechint x = case recinfo of
Nothing -> x
Just (_, recdef) -> (recdef, HMRecCall) : x
env = RIEnv {rieHints = rechint $ map (\x -> (x, HMNormal)) myhints,
rieDefFreeVars = defdfv
, rieEqReasoningConsts = meqr
}
depreached <- topSearch ticks nsol hsol env (initprop) d costIncrease
nsol' <- readIORef nsol
if nsol' /= 0 && depreached then
r (d + costIncrease)
else
return depreached
in r 0)
let getsols sol = do
exprs <- mapM (\(mi, e) -> do
mv <- lookupMeta mi
e <- etaContract e
expr <- liftM modifyAbstractExpr $ 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
if disprove then
case eqcons of
[] -> case Map.elems tccons of
(m, mytype, mylocalVars, _) : [] -> do
defdfv <- case thisdefinfo of
Just (def, _, _) -> fromIntegral `liftM` getdfv mi def
Nothing -> return 0
ee <- liftIO $ newIORef $ ConstDef {cdname = "T", cdorigin = __IMPOSSIBLE__, cdtype = NotM $ Sort (Set 0), cdcont = Postulate, cddeffreevars = 0}
let modargs = drop (length mylocalVars defdfv) mylocalVars
restargs = take (length mylocalVars defdfv) mylocalVars
mytype' = foldl (\x y -> NotM $ Pi Nothing Agda.Auto.Syntax.NotHidden (freeIn 0 y) y (Abs NoId x)) mytype restargs
htyp = negtype ee mytype'
sctx = (Id "h", closify htyp) : map (\x -> (NoId, closify x)) modargs
ntt = closify (NotM $ App Nothing (NotM OKVal) (Const ee) (NotM ALNil))
res <- exsearch (tcSearchSC False sctx ntt (Meta m)) Nothing defdfv
rsols <- liftM reverse $ liftIO $ readIORef sols
if null rsols then do
nsol' <- liftIO $ readIORef nsol
dispmsg $ insuffsols (pick + (if listmode then 10 else 1) 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 ss = dropWhile (== ' ') . dropWhile (/= ' ') . show
disp [(_, cexpr)] = ss cexpr
disp cexprs = concat (map (\(mi, cexpr) -> ss cexpr ++ " ") cexprs)
ticks <- liftIO $ readIORef ticks
dispmsg $ "Listing disproof(s) " ++ show pick ++ "-" ++ show (pick + length rsols 1) ++
"\n" ++ unlines (map (\(x, y) -> show y ++ " " ++ disp x) $ zip cexprss [pick..])
_ -> dispmsg "Metavariable dependencies not allowed in disprove mode"
_ -> dispmsg "Metavariable dependencies not allowed in disprove mode"
else do
(recinfo, defdfv) <-
case thisdefinfo of
Just (def, clause, _) -> do
let [rectyp'] = mymrectyp
defdfv <- getdfv mi def
myrecdef <- liftIO $ newIORef $ ConstDef {cdname = "", cdorigin = (Nothing, def), cdtype = rectyp', cdcont = Postulate, cddeffreevars = fromIntegral defdfv}
(_, pats) <- constructPats cmap mi clause
defdfv <- fromIntegral `liftM` getdfv mi def
return $ if contains_constructor pats then
(Just (pats, myrecdef), defdfv)
else
(Nothing, defdfv)
Nothing -> return (Nothing, 0)
let tc (m, mytype, mylocalVars) isdep = tcSearchSC 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, _) ->
if hequalMetavar m mainm then
case recinfo of
Just (recpats, recdef) ->
mpret $ Sidecondition (localTerminationSidecond (localTerminationEnv recpats) recdef (Meta m))
(tc (m, mt, mlv) False)
Nothing -> mpret $ And Nothing x (tc (m, mt, mlv) False)
else
mpret $ And Nothing x (tc (m, mt, mlv) True)
)
(mpret OK)
(Map.elems tccons)
) eqcons
res <- exsearch initprop recinfo defdfv
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)
ticks <- liftIO $ readIORef ticks
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 agsyinfo ticks 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 (Left $ catMaybes giveress, msg)
MCaseSplit -> do
case thisdefinfo of
Just (def, clause, True) ->
case Map.elems tccons of
((m, mytype, mylocalVars, _) : []) | null eqcons -> do
(ids, pats) <- constructPats cmap mi clause
let pids = concat $ map (\(_, x) -> " " ++ case x of {Id s -> s; NoId -> "noid"}) ids
ctx = map (\((hid, id), t) -> HI hid (id, t)) (zip ids mylocalVars)
ticks <- liftIO $ newIORef 0
let [rectyp'] = mymrectyp
defdfv <- getdfv mi def
myrecdef <- liftIO $ newIORef $ ConstDef {cdname = "", cdorigin = (Nothing, def), cdtype = rectyp', cdcont = Postulate, cddeffreevars = fromIntegral defdfv}
sols <- liftIO $ System.Timeout.timeout (timeout * 1000000) (
let r d = do
sols <- liftIO $ caseSplitSearch ticks __IMPOSSIBLE__ myhints meqr __IMPOSSIBLE__ d myrecdef ctx mytype pats
case sols of
[] -> r (d + costIncrease)
(_:_) -> return sols
in r 0)
case sols of
Just (cls : _) -> withInteractionId ii $ do
cls' <- liftIO $ runErrorT (mapM frommyClause cls)
case cls' of
Left{} -> dispmsg "No solution found"
Right cls' -> do
cls'' <- mapM (\(I.Clause _ tel perm ps body) ->
withCurrentModule (AN.qnameModule def) $ do
ps <- addCtxTel tel $ normalise ps
body <- etaContractBody body
liftM modifyAbstractClause $ inContext [] $ reify $ NamedClause def $ I.Clause noRange tel perm ps body
) cls'
pcs <- withInteractionId ii $ mapM prettyA cls''
ticks <- liftIO $ readIORef ticks
return (Right $ Left (map (insertAbsurdPattern . PP.renderStyle (PP.style { PP.mode = PP.OneLineMode })) pcs), Nothing)
Just [] -> dispmsg "No solution found"
Nothing -> dispmsg $ "No solution found at time out (" ++ show timeout ++ "s)"
_ -> dispmsg "Metavariable dependencies not allowed in case split mode"
_ -> dispmsg "Metavariable is not at top level of clause RHS"
MRefine listmode -> do
mv <- lookupMeta mi
let HasType _ tt = mvJudgement mv
minfo = getMetaInfo mv
targettyp <- withMetaInfo minfo $ do
vs <- getContextArgs
let targettype = tt `piApply` permute (takeP (fromIntegral $ length vs) $ mvPermutation mv) vs
normalise targettype
let tctx = length $ envContext $ clEnv minfo
hits <- if elem "-a" hints then do
st <- liftTCM $ join $ pureTCM $ \st _ -> return st
let defs = sigDefinitions $ stSignature st
idefs = sigDefinitions $ stImports st
alldefs = Map.keys defs ++ Map.keys idefs
liftM catMaybes $ mapM (\n ->
case thisdefinfo of
Just (def, _, _) | def == n -> return Nothing
_ -> do
cn <- withMetaInfo minfo $ runAbsToCon $ toConcrete n
if head (show cn) == '.' then
return Nothing
else do
c <- getConstInfo n
ctyp <- normalise $ defType c
cdfv <- withMetaInfo minfo $ getDefFreeVars n
return $ case matchType cdfv (fromIntegral tctx) ctyp targettyp of
Nothing -> Nothing
Just score -> Just (show cn, score)
) alldefs
else do
let scopeinfo = clScope (getMetaInfo mv)
namespace = Agda.Syntax.Scope.Base.everythingInScope scopeinfo
names = Agda.Syntax.Scope.Base.nsNames namespace
qnames = map (\(x, y) -> (x, Agda.Syntax.Scope.Base.anameName $ head y)) $ Map.toList names
modnames = case thisdefinfo of
Just (def, _, _) -> filter (\(_, n) -> n /= def) qnames
Nothing -> qnames
liftM catMaybes $ mapM (\(cn, n) -> do
c <- getConstInfo n
ctyp <- normalise $ defType c
cdfv <- withMetaInfo minfo $ getDefFreeVars n
return $ case matchType cdfv (fromIntegral tctx) ctyp targettyp of
Nothing -> Nothing
Just score -> Just (show cn, score)
) modnames
let sorthits = sortBy (\(_, (pa1, pb1)) (_, (pa2, pb2)) -> case compare pa2 pa1 of {EQ -> compare pb1 pb2; o -> o}) hits
if listmode || pick == (1) then
let pick' = max 0 pick
in if pick' >= length sorthits then
dispmsg $ insuffcands $ length sorthits
else
let showhits = take 10 $ drop pick' sorthits
in dispmsg $ "Listing candidate(s) " ++ show pick' ++ "-" ++ show (pick' + length showhits 1) ++ " (found " ++ show (length sorthits) ++ " in total)\n" ++
unlines (map (\(i, (cn, _)) -> show i ++ " " ++ cn) (zip [pick'..pick' + length showhits 1] showhits))
else
if pick >= length sorthits then
dispmsg $ insuffcands $ length sorthits
else
return (Right $ Right (fst $ sorthits !! pick), Nothing)
where
agsyinfo ticks = ""
autohints AHMModule mi (Just def) = do
mv <- lookupMeta mi
let scopeinfo = clScope (getMetaInfo mv)
namespace = Agda.Syntax.Scope.Base.everythingInScope scopeinfo
names = Agda.Syntax.Scope.Base.nsNames namespace
qnames = map (Agda.Syntax.Scope.Base.anameName . head) $ Map.elems names
modnames = filter (\n -> AN.qnameModule n == AN.qnameModule def && n /= def) qnames
modnames' <- filterM (\n -> do
c <- getConstInfo n
return (case theDef c of
Axiom{} -> True
Function{} -> True
_ -> False
)
) modnames
return $ map (\x -> (False, x)) modnames'
autohints _ _ _ = return []
insuffsols 0 = "No solution found"
insuffsols n = "Only " ++ show n ++ " solution(s) found"
insuffcands 0 = "No candidate found"
insuffcands n = "Only " ++ show n ++ " candidate(s) found"
data Mode = MNormal Bool Bool
| MCaseSplit
| MRefine Bool
data AutoHintMode = AHMNone
| AHMModule
parseargs :: String -> ([String], Int, Int, Mode, AutoHintMode)
parseargs s =
let r ("-t" : timeout : ws) (_, pick, mode, hintmode) =
r ws (read timeout, pick, mode, hintmode)
r ("-s" : pick : ws) (timeout, _, mode, hintmode) =
r ws (timeout, read pick, mode, hintmode)
r ("-l" : ws) (timeout, pick, MNormal _ disprove, hintmode) =
r ws (timeout, pick, MNormal True disprove, hintmode)
r ("-l" : ws) (timeout, pick, MRefine _, hintmode) =
r ws (timeout, pick, MRefine True, hintmode)
r ("-d" : ws) (timeout, pick, MNormal listmode _, hintmode) =
r ws (timeout, pick, MNormal listmode True, hintmode)
r ("-m" : ws) (timeout, pick, mode, _) =
r ws (timeout, pick, mode, AHMModule)
r ("-c" : ws) (timeout, pick, _, hintmode) =
r ws (timeout, pick, MCaseSplit, hintmode)
r ("-r" : ws) (timeout, pick, _, hintmode) =
r ws (timeout, (1), MRefine False, hintmode)
r (h : ws) x =
let (hints, timeout, pick, mode, hintmode) = r ws x
in (h : hints, timeout, pick, mode, hintmode)
r [] (x,y,z,w) = ([],x,y,z,w)
in r (words s) (5, 0, MNormal False False, AHMNone)