{-# LANGUAGE CPP #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.Auto.CaseSplit where
import Data.IORef
import Data.Tuple (swap)
import Data.List (findIndex, union)
import Data.Monoid ((<>), Sum(..))
import Data.Foldable (foldMap)
import qualified Data.Set as Set
import qualified Data.IntMap as IntMap
import Control.Monad.State as St hiding (lift)
import Control.Monad.Reader as Rd hiding (lift)
import qualified Control.Monad.State as St
import Data.Function
import Agda.Syntax.Common (Hiding(..))
import Agda.Auto.NarrowingSearch
import Agda.Auto.Syntax
import Agda.Auto.SearchControl
import Agda.Auto.Typecheck
#include "undefined.h"
import Agda.Utils.Impossible
import Agda.Utils.Monad (or2M)
abspatvarname :: String
abspatvarname = "\0absurdPattern"
costCaseSplitVeryHigh, costCaseSplitHigh, costCaseSplitLow, costAddVarDepth
:: Cost
costCaseSplitVeryHigh = 10000
costCaseSplitHigh = 5000
costCaseSplitLow = 2000
costAddVarDepth = 1000
data HI a = HI Hiding a
drophid :: [HI a] -> [a]
drophid = map (\(HI _ x) -> x)
type CSPat o = HI (CSPatI o)
type CSCtx o = [HI (MId, MExp o)]
data CSPatI o = CSPatConApp (ConstRef o) [CSPat o]
| CSPatVar Nat
| CSPatExp (MExp o)
| CSWith (MExp o)
| CSAbsurd
| CSOmittedArg
type Sol o = [(CSCtx o, [CSPat o], Maybe (MExp o))]
caseSplitSearch ::
forall o . IORef Int -> Int -> [ConstRef o] ->
Maybe (EqReasoningConsts o) -> Int -> Cost -> ConstRef o ->
CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
caseSplitSearch ticks nsolwanted chints meqr depthinterval depth recdef ctx tt pats = do
let branchsearch :: Cost -> CSCtx o -> MExp o ->
([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
branchsearch depth ctx tt termcheckenv = do
nsol <- newIORef 1
m <- initMeta
sol <- newIORef Nothing
let trm = Meta m
hsol = do trm' <- expandMetas trm
writeIORef sol (Just trm')
initcon = mpret
$ Sidecondition
(localTerminationSidecond termcheckenv recdef trm)
$ (case meqr of
Nothing -> id
Just eqr -> mpret . Sidecondition (calcEqRState eqr trm)
) $ tcSearch False (map (fmap closify) (drophid ctx))
(closify tt) trm
recdefd <- readIORef recdef
let env = RIEnv { rieHints = (recdef, HMRecCall) : map (, HMNormal) chints
, rieDefFreeVars = cddeffreevars recdefd
, rieEqReasoningConsts = meqr
}
depreached <- topSearch ticks nsol hsol env initcon depth (depth + 1)
rsol <- readIORef sol
return rsol
ctx' = ff 1 ctx
ff _ [] = []
ff n (HI hid (id, t) : ctx) = HI hid (id, lift n t) : ff (n + 1) ctx
caseSplitSearch' branchsearch depthinterval depth recdef ctx' tt pats
caseSplitSearch' :: forall o .
(Cost -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))) ->
Int -> Cost -> ConstRef o -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
caseSplitSearch' branchsearch depthinterval depth recdef ctx tt pats = do
recdefd <- readIORef recdef
sols <- rc depth (cddeffreevars recdefd) ctx tt pats
return sols
where
rc :: Cost -> Int -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
rc depth _ _ _ _ | depth < 0 = return []
rc depth nscrutavoid ctx tt pats = do
mblkvar <- getblks tt
fork
mblkvar
where
fork :: [Nat] -> IO [Sol o]
fork mblkvar = do
sols1 <- dobody
case sols1 of
(_:_) -> return sols1
[] -> do
let r :: [Nat] -> IO [Sol o]
r [] = return []
r (v:vs) = do
sols2 <- splitvar mblkvar v
case sols2 of
(_:_) -> return sols2
[] -> r vs
r [nv - x | x <- [0..nv]]
where nv = length ctx - 1
dobody :: IO [Sol o]
dobody = do
case findperm (map snd (drophid ctx)) of
Just perm -> do
let (ctx', tt', pats') = applyperm perm ctx tt pats
res <- branchsearch depth ctx' tt' (localTerminationEnv pats')
return $ case res of
Just trm -> [[(ctx', pats', Just trm)]]
Nothing -> []
Nothing -> __IMPOSSIBLE__
splitvar :: [Nat] -> Nat -> IO [Sol o]
splitvar mblkvar scrut = do
let scruttype = infertypevar ctx scrut
case rm __IMPOSSIBLE__ scruttype of
App _ _ (Const c) _ -> do
cd <- readIORef c
case cdcont cd of
Datatype cons _ -> do
sols <- dobranches cons
return $ map (\sol -> case sol of
[] ->
case findperm (map snd (drophid ctx)) of
Just perm ->
let HI scrhid(_, scrt) = ctx !! scrut
ctx1 = take scrut ctx ++ (HI scrhid (Id abspatvarname, scrt)) : drop (scrut + 1) ctx
(ctx', _, pats') = applyperm perm ctx1 tt (pats)
in [(ctx', pats', Nothing)]
Nothing -> __IMPOSSIBLE__
_ -> sol
) sols
where
dobranches :: [ConstRef o] -> IO [Sol o]
dobranches [] = return [[]]
dobranches (con : cons) = do
cond <- readIORef con
let ff t = case rm __IMPOSSIBLE__ t of
Pi _ h _ it (Abs id ot) ->
let (xs, inft) = ff ot
in (((h, scrut + length xs), id, lift (scrut + length xs + 1) it) : xs, inft)
_ -> ([], lift scrut t)
(newvars, inftype) = ff (cdtype cond)
constrapp = NotM $ App Nothing (NotM OKVal) (Const con) (foldl (\xs ((h, v), _, _) -> NotM $ ALCons h (NotM $ App Nothing (NotM OKVal) (Var v) (NotM ALNil)) xs) (NotM ALNil) (reverse newvars))
pconstrapp = CSPatConApp con (map (\((hid, v), _, _) -> HI hid (CSPatVar v)) newvars)
thesub = replace scrut (length newvars) constrapp
Id newvarprefix = fst $ (drophid ctx) !! scrut
ctx1 = map (\(HI hid (id, t)) -> HI hid (id, thesub t)) (take scrut ctx) ++
reverse (map (\(((hid, _), id, t), i) ->
HI hid (Id (case id of {NoId -> newvarprefix; Id id -> id}), t)
) (zip newvars [0..])) ++
map (\(HI hid (id, t)) -> HI hid (id, thesub t)) (drop (scrut + 1) ctx)
tt' = thesub tt
pats' = map (replacep scrut (length newvars) pconstrapp constrapp) pats
scruttype' = thesub scruttype
case unifyexp inftype scruttype' of
Nothing -> do
res <- notequal scrut (length newvars) scruttype' inftype
if res then
dobranches cons
else
return []
Just unif ->
do
let (ctx2, tt2, pats2) = removevar ctx1 tt' pats' unif
cost = if null mblkvar then
if scrut < length ctx - nscrutavoid && nothid
then costCaseSplitLow + costAddVarDepth
* Cost (depthofvar scrut pats)
else costCaseSplitVeryHigh
else
if elem scrut mblkvar then costCaseSplitLow else (if scrut < length ctx - nscrutavoid && nothid then costCaseSplitHigh else costCaseSplitVeryHigh)
nothid = let HI hid _ = ctx !! scrut
in hid == NotHidden
sols <- rc (depth - cost) (length ctx - 1 - scrut) ctx2 tt2 pats2
case sols of
[] -> return []
_ -> do
sols2 <- dobranches cons
return $ concat (map (\sol -> map (\sol2 -> sol ++ sol2) sols2) sols)
_ -> return []
_ -> return []
infertypevar :: CSCtx o -> Nat -> MExp o
infertypevar ctx v = snd $ (drophid ctx) !! v
class Replace o t u | t u -> o where
replace' :: Nat -> MExp o -> t -> Reader (Nat, Nat) u
replace :: Replace o t u => Nat -> Nat -> MExp o -> t -> u
replace sv nnew e t = replace' 0 e t `runReader` (sv, nnew)
instance Replace o t u => Replace o (Abs t) (Abs u) where
replace' n re (Abs mid b) = Abs mid <$> replace' (n + 1) re b
instance Replace o (Exp o) (MExp o) where
replace' n re e = case e of
App uid ok elr@(Var v) args -> do
ih <- NotM <$> replace' n re args
(sv, nnew) <- ask
return $
if v >= n
then if v - n == sv
then betareduce (lift n re) ih
else if v - n > sv
then NotM $ App uid ok (Var (v + nnew - 1)) ih
else NotM $ App uid ok elr ih
else NotM $ App uid ok elr ih
App uid ok elr@Const{} args ->
NotM . App uid ok elr . NotM <$> replace' n re args
Lam hid b -> NotM . Lam hid <$> replace' (n + 1) re b
Pi uid hid possdep it b ->
fmap NotM $ Pi uid hid possdep <$> replace' n re it <*> replace' n re b
Sort{} -> return $ NotM e
AbsurdLambda{} -> return $ NotM e
instance Replace o t u => Replace o (MM t (RefInfo o)) u where
replace' n re = replace' n re . rm __IMPOSSIBLE__
instance Replace o (ArgList o) (ArgList o) where
replace' n re args = case args of
ALNil -> return ALNil
ALCons hid a as ->
ALCons hid <$> replace' n re a <*> (NotM <$> replace' n re as)
ALProj{} -> __IMPOSSIBLE__
ALConPar as -> ALConPar . NotM <$> replace' n re as
betareduce :: MExp o -> MArgList o -> MExp o
betareduce e args = case rm __IMPOSSIBLE__ args of
ALNil -> e
ALCons _ a rargs -> case rm __IMPOSSIBLE__ e of
App uid ok elr eargs -> NotM $ App uid ok elr (concatargs eargs args)
Lam _ (Abs _ b) -> betareduce (replace 0 0 a b) rargs
_ -> __IMPOSSIBLE__
ALProj{} -> __IMPOSSIBLE__
ALConPar as -> __IMPOSSIBLE__
concatargs :: MArgList o -> MArgList o -> MArgList o
concatargs xs ys = case rm __IMPOSSIBLE__ xs of
ALNil -> ys
ALCons hid x xs -> NotM $ ALCons hid x (concatargs xs ys)
ALProj{} -> __IMPOSSIBLE__
ALConPar as -> NotM $ ALConPar (concatargs xs ys)
replacep :: forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
replacep sv nnew rp re = r
where
r :: CSPat o -> CSPat o
r (HI hid (CSPatConApp c ps)) = HI hid (CSPatConApp c (map r ps))
r (HI hid (CSPatVar v)) = if v == sv then
HI hid rp
else
if v > sv then
HI hid (CSPatVar (v + nnew - 1))
else
HI hid (CSPatVar v)
r (HI hid (CSPatExp e)) = HI hid (CSPatExp $ replace sv nnew re e)
r p@(HI _ CSOmittedArg) = p
r _ = __IMPOSSIBLE__
type Assignments o = [(Nat, Exp o)]
class Unify o t | t -> o where
unify' :: t -> t -> StateT (Assignments o) Maybe ()
notequal' :: t -> t -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool
unify :: Unify o t => t -> t -> Maybe (Assignments o)
unify t u = unify' t u `execStateT` []
notequal :: Unify o t => Nat -> Nat -> t -> t -> IO Bool
notequal fstnew nbnew t1 t2 = notequal' t1 t2 `runReaderT` (fstnew, nbnew)
`evalStateT` []
instance Unify o t => Unify o (MM t (RefInfo o)) where
unify' = unify' `on` rm __IMPOSSIBLE__
notequal' = notequal' `on` rm __IMPOSSIBLE__
unifyVar :: Nat -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar v e = do
unif <- get
case lookup v unif of
Nothing -> modify ((v, e) :)
Just e' -> unify' e e'
instance Unify o t => Unify o (Abs t) where
unify' (Abs _ b1) (Abs _ b2) = unify' b1 b2
notequal' (Abs _ b1) (Abs _ b2) = notequal' b1 b2
instance Unify o (Exp o) where
unify' e1 e2 = case (e1, e2) of
(App _ _ elr1 args1, App _ _ elr2 args2) | elr1 == elr2 -> unify' args1 args2
(Lam hid1 b1, Lam hid2 b2) | hid1 == hid2 -> unify' b1 b2
(Pi _ hid1 _ a1 b1, Pi _ hid2 _ a2 b2) | hid1 == hid2 -> unify' a1 a2
>> unify' b1 b2
(Sort _, Sort _) -> return ()
(App _ _ (Var v) (NotM ALNil), _)
| elem v (freevars e2) -> St.lift Nothing
(_, App _ _ (Var v) (NotM ALNil))
| elem v (freevars e1) -> St.lift Nothing
(App _ _ (Var v) (NotM ALNil), _) -> unifyVar v e2
(_, App _ _ (Var v) (NotM ALNil)) -> unifyVar v e1
_ -> St.lift Nothing
notequal' e1 e2 = do
(fstnew, nbnew) <- ask
unifier <- get
case (e1, e2) of
(App _ _ elr1 es1, App _ _ elr2 es2) | elr1 == elr2 -> notequal' es1 es2
(_, App _ _ (Var v2) (NotM ALNil))
| fstnew <= v2 && v2 < fstnew + nbnew ->
case lookup v2 unifier of
Nothing -> modify ((v2, e1):) >> return False
Just e2' -> notequal' e1 e2'
(App _ _ (Const c1) es1, App _ _ (Const c2) es2) -> do
cd1 <- liftIO $ readIORef c1
cd2 <- liftIO $ readIORef c2
case (cdcont cd1, cdcont cd2) of
(Constructor{}, Constructor{}) -> if c1 == c2 then notequal' es1 es2
else return True
_ -> return False
_ -> return False
instance Unify o (ArgList o) where
unify' args1 args2 = case (args1, args2) of
(ALNil, ALNil) -> pure ()
(ALCons hid1 a1 as1, ALCons hid2 a2 as2) | hid1 == hid2 -> unify' a1 a2
>> unify' as1 as2
(ALConPar as1, ALCons _ _ as2) -> unify' as1 as2
(ALCons _ _ as1, ALConPar as2) -> unify' as1 as2
(ALConPar as1, ALConPar as2) -> unify' as1 as2
_ -> St.lift Nothing
notequal' args1 args2 = case (args1, args2) of
(ALCons _ e es, ALCons _ f fs) -> notequal' e f `or2M` notequal' es fs
(ALConPar es1, ALConPar es2) -> notequal' es1 es2
_ -> return False
unifyexp :: MExp o -> MExp o -> Maybe ([(Nat, MExp o)])
unifyexp e1 e2 = fmap (NotM <$>) <$> unify e1 e2
class Lift t where
lift' :: Nat -> Nat -> t -> t
lift :: Lift t => Nat -> t -> t
lift 0 = id
lift n = lift' n 0
instance Lift t => Lift (Abs t) where
lift' n j (Abs mid b) = Abs mid (lift' n (j + 1) b)
instance Lift t => Lift (MM t r) where
lift' n j = NotM . lift' n j . rm __IMPOSSIBLE__
instance Lift (Exp o) where
lift' n j e = case e of
App uid ok elr args -> case elr of
Var v | v >= j -> App uid ok (Var (v + n)) (lift' n j args)
_ -> App uid ok elr (lift' n j args)
Lam hid b -> Lam hid (lift' n j b)
Pi uid hid possdep it b -> Pi uid hid possdep (lift' n j it) (lift' n j b)
Sort{} -> e
AbsurdLambda{} -> e
instance Lift (ArgList o) where
lift' n j args = case args of
ALNil -> ALNil
ALCons hid a as -> ALCons hid (lift' n j a) (lift' n j as)
ALProj{} -> __IMPOSSIBLE__
ALConPar as -> ALConPar (lift' n j as)
removevar :: CSCtx o -> MExp o -> [CSPat o] -> [(Nat, MExp o)] -> (CSCtx o, MExp o, [CSPat o])
removevar ctx tt pats [] = (ctx, tt, pats)
removevar ctx tt pats ((v, e) : unif) =
let
e2 = replace v 0 __IMPOSSIBLE__ e
thesub = replace v 0 e2
ctx1 = map (\(HI hid (id, t)) -> HI hid (id, thesub t)) (take v ctx) ++
map (\(HI hid (id, t)) -> HI hid (id, thesub t)) (drop (v + 1) ctx)
tt' = thesub tt
pats' = map (replacep v 0 (CSPatExp e2) e2) pats
unif' = map (\(uv, ue) -> (if uv > v then uv - 1 else uv, thesub ue)) unif
in
removevar ctx1 tt' pats' unif'
findperm :: [MExp o] -> Maybe [Nat]
findperm ts =
let
frees = map freevars ts
m = IntMap.fromList $
map (\i -> (i, length (filter (elem i) frees)))
[0..length ts - 1]
r _ perm 0 = Just $ reverse perm
r m perm n =
case lookup 0 (map swap (IntMap.toList m)) of
Nothing -> Nothing
Just i -> r (foldl (flip $ IntMap.adjust (subtract 1))
(IntMap.insert i (-1) m)
(frees !! i))
(i : perm) (n - 1)
in r m [] (length ts)
freevars :: FreeVars t => t -> [Nat]
freevars = Set.toList . freeVars
applyperm :: [Nat] -> CSCtx o -> MExp o -> [CSPat o] ->
(CSCtx o, MExp o, [CSPat o])
applyperm perm ctx tt pats =
let ctx1 = map (\(HI hid (id, t)) -> HI hid (id, rename (ren perm) t)) ctx
ctx2 = map (\i -> ctx1 !! i) perm
ctx3 = seqctx ctx2
tt' = rename (ren perm) tt
pats' = map (rename (ren perm)) pats
in (ctx3, tt', pats')
ren :: [Nat] -> Nat -> Int
ren n i = let Just j = findIndex (== i) n in j
instance Renaming t => Renaming (HI t) where
renameOffset j ren (HI hid t) = HI hid $ renameOffset j ren t
instance Renaming (CSPatI o) where
renameOffset j ren e = case e of
CSPatConApp c pats -> CSPatConApp c $ map (renameOffset j ren) pats
CSPatVar i -> CSPatVar $ j + ren i
CSPatExp e -> CSPatExp $ renameOffset j ren e
CSOmittedArg -> e
_ -> __IMPOSSIBLE__
seqctx :: CSCtx o -> CSCtx o
seqctx = r (-1)
where
r _ [] = []
r n (HI hid (id, t) : ctx) = HI hid (id, lift n t) : r (n - 1) ctx
depthofvar :: Nat -> [CSPat o] -> Nat
depthofvar v pats =
let [depth] = concatMap (f 0) (drophid pats)
f d (CSPatConApp _ pats) = concatMap (f (d + 1)) (drophid pats)
f d (CSPatVar v') = if v == v' then [d] else []
f _ _ = []
in depth
class LocalTerminationEnv a where
sizeAndBoundVars :: a -> (Sum Nat, [Nat])
instance LocalTerminationEnv a => LocalTerminationEnv (HI a) where
sizeAndBoundVars (HI _ p) = sizeAndBoundVars p
instance LocalTerminationEnv (CSPatI o) where
sizeAndBoundVars p = case p of
CSPatConApp _ ps -> (1, []) <> sizeAndBoundVars ps
CSPatVar n -> (0, [n])
CSPatExp e -> sizeAndBoundVars e
_ -> (0, [])
instance LocalTerminationEnv a => LocalTerminationEnv [a] where
sizeAndBoundVars = foldMap sizeAndBoundVars
instance LocalTerminationEnv (MExp o) where
sizeAndBoundVars Meta{} = (0, [])
sizeAndBoundVars (NotM e) = case e of
App _ _ (Var v) _ -> (0, [v])
App _ _ (Const _) args -> (1, []) <> sizeAndBoundVars args
_ -> (0, [])
instance (LocalTerminationEnv a, LocalTerminationEnv b) => LocalTerminationEnv (a, b) where
sizeAndBoundVars (a, b) = sizeAndBoundVars a <> sizeAndBoundVars b
instance LocalTerminationEnv (MArgList o) where
sizeAndBoundVars as = case rm __IMPOSSIBLE__ as of
ALNil -> (0, [])
ALCons _ a as -> sizeAndBoundVars (a, as)
ALProj{} -> __IMPOSSIBLE__
ALConPar as -> sizeAndBoundVars as
localTerminationEnv :: [CSPat o] -> ([Nat], Nat, [Nat])
localTerminationEnv pats = (is, getSum s, vs) where
(is , s , vs) = g 0 pats
g :: Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
g _ [] = ([], 0, [])
g i (hp@(HI _ p) : ps) = case p of
CSPatConApp{} -> let (size, vars) = sizeAndBoundVars hp
in ([i], size, vars) <> g (i + 1) ps
_ -> g (i + 1) ps
localTerminationSidecond :: ([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)
localTerminationSidecond (is, size, vars) reccallc b =
ok b
where
ok e = mmpcase (False, prioNo, Nothing) e $ \e -> case e of
App _ _ elr args -> mpret $ Sidecondition
(oks args)
(case elr of
Const c | c == reccallc -> if size == 0 then mpret (Error "localTerminationSidecond: no size to decrement") else okcall 0 size vars args
_ -> mpret OK
)
Lam _ (Abs _ e) -> ok e
Pi _ _ _ it (Abs _ ot) -> mpret $ Sidecondition
(ok it)
(ok ot)
Sort{} -> mpret OK
AbsurdLambda{} -> mpret OK
oks as = mmpcase (False, prioNo, Nothing) as $ \as -> case as of
ALNil -> mpret OK
ALCons _ a as -> mpret $ Sidecondition
(ok a)
(oks as)
ALProj eas _ _ as -> mpret $ Sidecondition (oks eas) (oks as)
ALConPar as -> oks as
okcall i size vars as = mmpcase (False, prioNo, Nothing) as $ \as -> case as of
ALNil -> mpret OK
ALCons _ a as | elem i is ->
mbpcase prioNo Nothing (he size vars a) $ \x -> case x of
Nothing -> mpret $ Error "localTerminationSidecond: reccall not ok"
Just (size', vars') -> okcall (i + 1) size' vars' as
ALCons _ a as -> okcall (i + 1) size vars as
ALProj{} -> mpret OK
ALConPar as -> __IMPOSSIBLE__
he size vars e = mmcase e $ \e -> case e of
App _ _ (Var v) _ ->
case remove v vars of
Nothing -> mbret Nothing
Just vars' -> mbret $ Just (size, vars')
App _ _ (Const c) args -> do
cd <- readIORef c
case cdcont cd of
Constructor{} ->
if size == 1 then
mbret Nothing
else
hes (size - 1) vars args
_ -> mbret Nothing
_ -> mbret Nothing
hes size vars as = mmcase as $ \as -> case as of
ALNil -> mbret $ Just (size, vars)
ALCons _ a as ->
mbcase (he size vars a) $ \x -> case x of
Nothing -> mbret Nothing
Just (size', vars') -> hes size' vars' as
ALProj{} -> __IMPOSSIBLE__
ALConPar as -> __IMPOSSIBLE__
remove _ [] = Nothing
remove x (y : ys) | x == y = Just ys
remove x (y : ys) = case remove x ys of {Nothing -> Nothing; Just ys' -> Just (y : ys')}
getblks :: MExp o -> IO [Nat]
getblks tt = do
NotB (hntt, blks) <- hnn_blks (Clos [] tt)
case f blks of
Just v -> return [v]
Nothing -> case rawValue hntt of
HNApp (Const c) args -> do
cd <- readIORef c
case cdcont cd of
Datatype{} -> g [] args
_ -> return []
_ -> return []
where
f blks = case blks of
(_:_) -> case rawValue (last blks) of
HNApp (Var v) _ -> Just v
_ -> Nothing
_ -> Nothing
g vs args = do
NotB hnargs <- hnarglist args
case hnargs of
HNALCons _ a as -> do
NotB (_, blks) <- hnn_blks a
let vs' = case f blks of
Just v | v `notElem` vs -> v : vs
_ -> vs
g vs' as
_ -> return vs