Agda-2.6.4.1: src/full/Agda/Auto/SearchControl.hs
{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wno-orphans #-}
#if __GLASGOW_HASKELL__ > 907
{-# OPTIONS_GHC -Wno-x-partial #-}
#endif
module Agda.Auto.SearchControl where
import Control.Monad
import Data.IORef
import Control.Monad.State
import Data.Maybe (mapMaybe, fromMaybe)
import Agda.Syntax.Common (Hiding(..))
import Agda.Auto.NarrowingSearch
import Agda.Auto.Syntax
import Agda.Utils.Impossible
instance Refinable (ArgList o) (RefInfo o) where
refinements _ infos _ = return $ fmap (Move 0) $
[ return ALNil, cons NotHidden, cons Hidden ]
++ if getIsDep infos then []
else [ proj NotHidden, proj Hidden ]
where
getIsDep :: [RefInfo o] -> Bool
getIsDep (x : xs) = case x of
RICheckElim isDep -> isDep
_ -> getIsDep xs
getIsDep _ = __IMPOSSIBLE__
proj :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
proj hid = ALProj <$> newPlaceholder <*> newPlaceholder
<*> return hid <*> newPlaceholder
cons :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
cons hid = ALCons hid <$> newPlaceholder <*> newPlaceholder
data ExpRefInfo o = ExpRefInfo
{ eriMain :: Maybe (RefInfo o)
, eriUnifs :: [RefInfo o]
, eriInfTypeUnknown :: Bool
, eriIsEliminand :: Bool
, eriUsedVars :: Maybe ([UId o], [Elr o])
, eriIotaStep :: Maybe Bool
, eriPickSubsVar :: Bool
, eriEqRState :: Maybe EqReasoningState
}
initExpRefInfo :: ExpRefInfo o
initExpRefInfo = ExpRefInfo
{ eriMain = Nothing
, eriUnifs = []
, eriInfTypeUnknown = False
, eriIsEliminand = False
, eriUsedVars = Nothing
, eriIotaStep = Nothing
, eriPickSubsVar = False
, eriEqRState = Nothing
}
getinfo :: [RefInfo o] -> ExpRefInfo o
getinfo = foldl step initExpRefInfo where
step :: ExpRefInfo o -> RefInfo o -> ExpRefInfo o
step eri x@RIMainInfo{} = eri { eriMain = Just x }
step eri x@RIUnifInfo{} = eri { eriUnifs = x : eriUnifs eri }
step eri RIInferredTypeUnknown = eri { eriInfTypeUnknown = True }
step eri RINotConstructor = eri { eriIsEliminand = True }
step eri (RIUsedVars nuids nused) = eri { eriUsedVars = Just (nuids, nused) }
step eri (RIIotaStep semif) = eri { eriIotaStep = Just iota' } where
iota' = semif || (Just True ==) (eriIotaStep eri)
step eri RIPickSubsvar = eri { eriPickSubsVar = True }
step eri (RIEqRState s) = eri { eriEqRState = Just s }
step eri _ = __IMPOSSIBLE__
-- | @univar sub v@ figures out what the name of @v@ "outside" of
-- the substitution @sub@ ought to be, if anything.
univar :: [CAction o] -> Nat -> Maybe Nat
univar cl v = getOutsideName cl v 0 where
getOutsideName :: [CAction o] -> Nat -> Nat -> Maybe Nat
-- @v@ is offset by @v'@ binders
getOutsideName [] v v' = Just (v' + v)
-- @v@ was introduced by the weakening: disappears
getOutsideName (Weak n : _) v v' | v < n = Nothing
-- @v@ was introduced before the weakening: strengthened
getOutsideName (Weak n : xs) v v' = getOutsideName xs (v - n) v'
-- Name of @v@ before the substitution was pushed in
-- had to be offset by 1
getOutsideName (Sub _ : xs) v v' = getOutsideName xs v (v' + 1)
-- If this is the place where @v@ was bound, it used to
-- be called 0 + offset of all the vars substituted for
getOutsideName (Skip : _) 0 v' = Just v'
-- Going over a binder: de Bruijn name of @v@ decreased
-- but offset increased
getOutsideName (Skip : xs) v v' = getOutsideName xs (v - 1) (v' + 1)
-- | List of the variables instantiated by the substitution
subsvars :: [CAction o] -> [Nat]
subsvars = f 0 where
f :: Nat -> [CAction o] -> [Nat]
f n [] = []
f n (Weak _ : xs) = f n xs -- why?
f n (Sub _ : xs) = n : f (n + 1) xs
f n (Skip : xs) = f (n + 1) xs
-- | Moves
-- A move is composed of a @Cost@ together with an action
-- computing the refined problem.
type Move o = Move' (RefInfo o) (Exp o)
-- | New constructors
-- Taking a step towards a solution consists in picking a
-- constructor and filling in the missing parts with
-- placeholders to be discharged later on.
newAbs :: MId -> RefCreateEnv blk (Abs (MM a blk))
newAbs mid = Abs mid <$> newPlaceholder
newLam :: Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)
newLam hid mid = Lam hid <$> newAbs mid
newPi :: UId o -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)
newPi uid dep hid = Pi (Just uid) hid dep <$> newPlaceholder <*> newAbs NoId
foldArgs :: [(Hiding, MExp o)] -> MArgList o
foldArgs = foldr (\ (h, a) sp -> NotM $ ALCons h a sp) (NotM ALNil)
-- | New spine of arguments potentially using placeholders
newArgs' :: [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)
newArgs' h tms = foldArgs . zip h . (++ tms) <$> replicateM size newPlaceholder
where size = length h - length tms
newArgs :: [Hiding] -> RefCreateEnv (RefInfo o) (MArgList o)
newArgs h = newArgs' h []
-- | New @App@lication node using a new spine of arguments
-- respecting the @Hiding@ annotation
newApp' :: UId o -> ConstRef o -> [Hiding] -> [MExp o] ->
RefCreateEnv (RefInfo o) (Exp o)
newApp' meta cst hds tms =
App (Just meta) <$> newOKHandle <*> return (Const cst) <*> newArgs' hds tms
newApp :: UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
newApp meta cst hds = newApp' meta cst hds []
-- | Equality reasoning steps
-- The begin token is accompanied by two steps because
-- it does not make sense to have a derivation any shorter
-- than that.
eqStep :: UId o -> EqReasoningConsts o -> Move o
eqStep meta eqrc = Move costEqStep $ newApp meta (eqrcStep eqrc)
[Hidden, Hidden, NotHidden, Hidden, Hidden, NotHidden, NotHidden]
eqEnd :: UId o -> EqReasoningConsts o -> Move o
eqEnd meta eqrc = Move costEqEnd $ newApp meta (eqrcEnd eqrc)
[Hidden, Hidden, NotHidden]
eqCong :: UId o -> EqReasoningConsts o -> Move o
eqCong meta eqrc = Move costEqCong $ newApp meta (eqrcCong eqrc)
[Hidden, Hidden, Hidden, Hidden, NotHidden, Hidden, Hidden, NotHidden]
eqSym :: UId o -> EqReasoningConsts o -> Move o
eqSym meta eqrc = Move costEqSym $ newApp meta (eqrcSym eqrc)
[Hidden, Hidden, Hidden, Hidden, NotHidden]
eqBeginStep2 :: UId o -> EqReasoningConsts o -> Move o
eqBeginStep2 meta eqrc = Move costEqStep $ do
e1 <- newApp meta (eqrcStep eqrc)
[Hidden, Hidden, NotHidden, Hidden, Hidden, NotHidden, NotHidden]
e2 <- newApp' meta (eqrcStep eqrc)
[Hidden, Hidden, NotHidden, Hidden, Hidden, NotHidden, NotHidden]
[NotM e1]
newApp' meta (eqrcBegin eqrc) [Hidden, Hidden, Hidden, Hidden, NotHidden]
[NotM e2]
-- | Pick the first unused UId amongst the ones you have seen (GA: ??)
-- Defaults to the head of the seen ones.
pickUid :: forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)
pickUid used seen = maybe (head seen, False) (, True) $ firstUnused seen where
{- ?? which uid to pick -}
firstUnused :: [Maybe (UId o)] -> Maybe (Maybe (UId o))
firstUnused [] = Nothing
firstUnused (Nothing : _) = Just Nothing
firstUnused (mu@(Just u) : us) =
if u `elem` used then firstUnused us else Just mu
instance Refinable (Exp o) (RefInfo o) where
refinements envinfo infos meta =
let
hints = rieHints envinfo
deffreevars = rieDefFreeVars envinfo
meqr = rieEqReasoningConsts envinfo
ExpRefInfo { eriMain = Just (RIMainInfo n tt iotastepdone)
, eriUnifs = unis
, eriInfTypeUnknown = inftypeunknown
, eriIsEliminand = iseliminand -- TODO:: Defined but not used
, eriUsedVars = Just (uids, usedvars)
, eriIotaStep = iotastep
, eriPickSubsVar = picksubsvar -- TODO:: Defined but not used
, eriEqRState = meqrstate
} = getinfo infos
eqrstate = fromMaybe EqRSNone meqrstate
set l = return $ Sort (Set l)
in case unis of
[] ->
let
eqr = fromMaybe __IMPOSSIBLE__ meqr
eq_end = eqEnd meta eqr
eq_step = eqStep meta eqr
eq_cong = eqCong meta eqr
eq_sym = eqSym meta eqr
eq_begin_step2 = eqBeginStep2 meta eqr
adjustCost i = if inftypeunknown then costInferredTypeUnkown else i
varcost v | v < n - deffreevars = adjustCost $
if v `elem` (mapMaybe getVar usedvars)
then costAppVarUsed else costAppVar
varcost v | otherwise = adjustCost costAppHint
varapps = map (\ v -> Move (varcost v) $ app n meta Nothing (Var v)) [0..n - 1]
hintapps = map (\(c, hm) -> Move (cost c hm) (app n meta Nothing (Const c))) hints
where
cost :: ConstRef o -> HintMode -> Cost
cost c hm = adjustCost $ case (iotastep , hm) of
(Just _ , _ ) -> costIotaStep
(Nothing , HMNormal) ->
if c `elem` (mapMaybe getConst usedvars)
then costAppHintUsed else costAppHint
(Nothing , HMRecCall) ->
if c `elem` (mapMaybe getConst usedvars)
then costAppRecCallUsed else costAppRecCall
generics = varapps ++ hintapps
in case rawValue tt of
_ | eqrstate == EqRSChain ->
return [eq_end, eq_step]
HNPi hid _ _ (Abs id _) -> return $
Move (adjustCost (if iotastepdone then costLamUnfold else costLam)) (newLam hid id)
: Move costAbsurdLam (return $ AbsurdLambda hid)
: generics
HNSort (Set l) -> return $
map (Move (adjustCost costSort) . set) [0..l - 1]
++ map (Move (adjustCost costPi) . newPi meta True) [NotHidden, Hidden]
++ generics
HNApp (Const c) _ -> do
cd <- readIORef c
return $ case cdcont cd of
Datatype cons _ | eqrstate == EqRSNone ->
map (\c -> Move (adjustCost $ case iotastep of
Just True -> costUnification
_ -> if length cons <= 1
then costAppConstructorSingle
else costAppConstructor)
$ app n meta Nothing (Const c)) cons
++ generics
++ (guard (maybe False ((c ==) . eqrcId) meqr)
*> [eq_sym, eq_cong, eq_begin_step2])
_ | eqrstate == EqRSPrf1 -> generics ++ [eq_sym, eq_cong]
_ | eqrstate == EqRSPrf2 -> generics ++ [eq_cong]
_ -> generics
_ -> return generics
(RIUnifInfo cl hne : _) ->
let
subsvarapps = map (Move costUnification . app n meta Nothing . Var) (subsvars cl)
mlam = case rawValue tt of
HNPi hid _ _ (Abs id _) -> [Move costUnification (newLam hid id)]
_ -> []
generics = mlam ++ subsvarapps
in
return $ case rawValue hne of
HNApp (Var v) _ ->
let (uid, isunique) = pickUid uids $ seenUIds hne
uni = case univar cl v of
Just v | v < n -> [Move (costUnificationIf isunique) $ app n meta uid (Var v)]
_ -> []
in uni ++ generics
HNApp (Const c) _ ->
let (uid, isunique) = pickUid uids $ seenUIds hne
in Move (costUnificationIf isunique) (app n meta uid (Const c)) : generics
HNLam{} -> generics
HNPi hid possdep _ _ ->
let (uid, isunique) = pickUid uids $ seenUIds hne
in Move (costUnificationIf isunique) (newPi (fromMaybe meta uid) possdep hid) : generics
HNSort (Set l) -> map (Move costUnification . set) [0..l] ++ generics
HNSort _ -> generics
_ -> __IMPOSSIBLE__
where
app :: Nat -> UId o -> Maybe (UId o) -> Elr o ->
RefCreateEnv (RefInfo o) (Exp o)
app n meta muid elr = do
p <- newPlaceholder
p <- case elr of
Var{} -> return p
Const c -> do
cd <- RefCreateEnv $ lift $ readIORef c
let dfvapp 0 _ = p
dfvapp i n = NotM $ ALCons NotHidden
(NotM $ App Nothing (NotM $ OKVal) (Var n) (NotM ALNil))
(dfvapp (i - 1) (n - 1))
-- NotHidden is ok because agda reification throws these arguments
-- away and agsy skips typechecking them
return $ dfvapp (cddeffreevars cd) (n - 1)
okh <- newOKHandle
return $ App (Just $ fromMaybe meta muid) okh elr p
extraref :: UId o -> [Maybe (UId o)] -> ConstRef o -> Move o
extraref meta seenuids c = Move costAppExtraRef $ app (head seenuids) (Const c)
where
app muid elr = App (Just $ fromMaybe meta muid)
<$> newOKHandle <*> return elr <*> newPlaceholder
instance Refinable (ICExp o) (RefInfo o) where
refinements _ infos _ =
let (RICopyInfo e : _) = infos
in return [Move 0 (return e)]
instance Refinable (ConstRef o) (RefInfo o) where
refinements _ [RICheckProjIndex projs] _ = return $ map (Move 0 . return) projs
refinements _ _ _ = __IMPOSSIBLE__
-- ---------------------------------
costIncrease, costUnificationOccurs, costUnification, costAppVar,
costAppVarUsed, costAppHint, costAppHintUsed, costAppRecCall,
costAppRecCallUsed, costAppConstructor, costAppConstructorSingle,
costAppExtraRef, costLam, costLamUnfold, costPi, costSort, costIotaStep,
costInferredTypeUnkown, costAbsurdLam
:: Cost
costUnificationIf :: Bool -> Cost
costUnificationIf b = if b then costUnification else costUnificationOccurs
costIncrease = 1000
costUnificationOccurs = 100 -- 1000001 -- 1 -- 100
costUnification = 0000
costAppVar = 0000 -- 0, 1
costAppVarUsed = 1000 -- 5
costAppHint = 3000 -- 2, 5
costAppHintUsed = 5000
costAppRecCall = 0 -- 1000?
costAppRecCallUsed = 10000 -- 1000?
costAppConstructor = 1000
costAppConstructorSingle = 0000
costAppExtraRef = 1000
costLam = 0000 -- 1, 0
costLamUnfold = 1000 -- 1, 0
costPi = 1000003 -- 100 -- 5
costSort = 1000004 -- 0
costIotaStep = 3000 -- 1000005 -- 2 -- 100
costInferredTypeUnkown = 1000006 -- 100
costAbsurdLam = 0
costEqStep, costEqEnd, costEqSym, costEqCong :: Cost
costEqStep = 2000
costEqEnd = 0
costEqSym = 0
costEqCong = 500
prioNo, prioTypeUnknown, prioTypecheckArgList, prioInferredTypeUnknown,
prioCompBeta, prioCompBetaStructured, prioCompareArgList, prioCompIota,
prioCompChoice, prioCompUnif, prioCompCopy, prioNoIota, prioAbsurdLambda,
prioProjIndex
:: Prio
prioNo = (-1)
prioTypeUnknown = 0
prioTypecheckArgList = 3000
prioInferredTypeUnknown = 4000
prioCompBeta = 4000
prioCompBetaStructured = 4000
prioCompIota = 4000
prioCompChoice = 5000 -- 700 -- 5000
prioCompUnif = 6000 -- 2
prioCompCopy = 8000
prioCompareArgList = 7000 -- 5 -- 2
prioNoIota = 500 -- 500
prioAbsurdLambda = 1000
prioProjIndex = 3000
prioTypecheck :: Bool -> Prio
prioTypecheck False = 1000
prioTypecheck True = 0
-- ---------------------------------
instance Trav a => Trav [a] where
type Block [a] = Block a
trav _ [] = return ()
trav f (x:xs) = trav f x >> trav f xs
instance Trav (MId, CExp o) where
type Block (MId, CExp o) = RefInfo o
trav f (_, ce) = trav f ce
instance Trav (TrBr a o) where
type Block (TrBr a o) = RefInfo o
trav f (TrBr es _) = trav f es
instance Trav (Exp o) where
type Block (Exp o) = RefInfo o
trav f = \case
App _ _ _ args -> trav f args
Lam _ (Abs _ b) -> trav f b
Pi _ _ _ it (Abs _ ot) -> trav f it >> trav f ot
Sort _ -> return ()
AbsurdLambda{} -> return ()
instance Trav (ArgList o) where
type Block (ArgList o) = RefInfo o
trav _ ALNil = return ()
trav f (ALCons _ arg args) = trav f arg >> trav f args
trav f (ALProj eas _ _ as) = trav f eas >> trav f as
trav f (ALConPar args) = trav f args
-- ---------------------------------