    {-# OPTIONS_GHC -fno-warn-orphans #-}

    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 :: RefInfo o
    -> [RefInfo o]
    -> Metavar (ArgList o) (RefInfo o)
    -> IO [Move' (RefInfo o) (ArgList o)]
    refinements RefInfo o
    _ [RefInfo o]
    infos Metavar (ArgList o) (RefInfo o)
    _ = [Move' (RefInfo o) (ArgList o)]
    -> IO [Move' (RefInfo o) (ArgList o)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Move' (RefInfo o) (ArgList o)]
     -> IO [Move' (RefInfo o) (ArgList o)])
    -> [Move' (RefInfo o) (ArgList o)]
    -> IO [Move' (RefInfo o) (ArgList o)]
    forall a b. (a -> b) -> a -> b
    $ (RefCreateEnv (RefInfo o) (ArgList o)
     -> Move' (RefInfo o) (ArgList o))
    -> [RefCreateEnv (RefInfo o) (ArgList o)]
    -> [Move' (RefInfo o) (ArgList o)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Cost
    -> RefCreateEnv (RefInfo o) (ArgList o)
    -> Move' (RefInfo o) (ArgList o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move Cost
    0) ([RefCreateEnv (RefInfo o) (ArgList o)]
     -> [Move' (RefInfo o) (ArgList o)])
    -> [RefCreateEnv (RefInfo o) (ArgList o)]
    -> [Move' (RefInfo o) (ArgList o)]
    forall a b. (a -> b) -> a -> b
    $
       [ ArgList o -> RefCreateEnv (RefInfo o) (ArgList o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ArgList o
    forall o. ArgList o
    ALNil, Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
    cons Hiding
    NotHidden, Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
    cons Hiding
    Hidden ]
       [RefCreateEnv (RefInfo o) (ArgList o)]
    -> [RefCreateEnv (RefInfo o) (ArgList o)]
    -> [RefCreateEnv (RefInfo o) (ArgList o)]
    forall a. [a] -> [a] -> [a]
    ++ if [RefInfo o] -> Bool
    getIsDep [RefInfo o]
    infos then []
          else [ Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
    proj Hiding
    NotHidden, Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
    proj Hiding
    Hidden ]

       where

        getIsDep :: [RefInfo o] -> Bool
        getIsDep :: [RefInfo o] -> Bool
    getIsDep (RefInfo o
    x : [RefInfo o]
    xs) = case RefInfo o
    x of
          RICheckElim Bool
    isDep -> Bool
    isDep
          RefInfo o
    _                 -> [RefInfo o] -> Bool
    getIsDep [RefInfo o]
    xs
        getIsDep [RefInfo o]
    _ = Bool
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        proj :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
        proj :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
    proj Hiding
    hid = MArgList o
    -> MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o
    forall o.
    MArgList o
    -> MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o
    ALProj (MArgList o
     -> MM (ConstRef o) (RefInfo o)
     -> Hiding
     -> MArgList o
     -> ArgList o)
    -> RefCreateEnv (RefInfo o) (MArgList o)
    -> RefCreateEnv
         (RefInfo o)
         (MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RefCreateEnv (RefInfo o) (MArgList o)
    forall blk a. RefCreateEnv blk (MM a blk)
    newPlaceholder RefCreateEnv
      (RefInfo o)
      (MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o)
    -> RefCreateEnv (RefInfo o) (MM (ConstRef o) (RefInfo o))
    -> RefCreateEnv (RefInfo o) (Hiding -> MArgList o -> ArgList o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> RefCreateEnv (RefInfo o) (MM (ConstRef o) (RefInfo o))
    forall blk a. RefCreateEnv blk (MM a blk)
    newPlaceholder
                          RefCreateEnv (RefInfo o) (Hiding -> MArgList o -> ArgList o)
    -> RefCreateEnv (RefInfo o) Hiding
    -> RefCreateEnv (RefInfo o) (MArgList o -> ArgList o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Hiding -> RefCreateEnv (RefInfo o) Hiding
    forall (m :: * -> *) a. Monad m => a -> m a
    return Hiding
    hid     RefCreateEnv (RefInfo o) (MArgList o -> ArgList o)
    -> RefCreateEnv (RefInfo o) (MArgList o)
    -> RefCreateEnv (RefInfo o) (ArgList o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> RefCreateEnv (RefInfo o) (MArgList o)
    forall blk a. RefCreateEnv blk (MM a blk)
    newPlaceholder

        cons :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
        cons :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
    cons Hiding
    hid = Hiding -> MExp o -> MArgList o -> ArgList o
    forall o. Hiding -> MExp o -> MArgList o -> ArgList o
    ALCons Hiding
    hid (MExp o -> MArgList o -> ArgList o)
    -> RefCreateEnv (RefInfo o) (MExp o)
    -> RefCreateEnv (RefInfo o) (MArgList o -> ArgList o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RefCreateEnv (RefInfo o) (MExp o)
    forall blk a. RefCreateEnv blk (MM a blk)
    newPlaceholder RefCreateEnv (RefInfo o) (MArgList o -> ArgList o)
    -> RefCreateEnv (RefInfo o) (MArgList o)
    -> RefCreateEnv (RefInfo o) (ArgList o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> RefCreateEnv (RefInfo o) (MArgList o)
    forall blk a. RefCreateEnv blk (MM a blk)
    newPlaceholder

    data ExpRefInfo o = ExpRefInfo
      { forall o. ExpRefInfo o -> Maybe (RefInfo o)
    eriMain           :: Maybe (RefInfo o)
      , forall o. ExpRefInfo o -> [RefInfo o]
    eriUnifs          :: [RefInfo o]
      , forall o. ExpRefInfo o -> Bool
    eriInfTypeUnknown :: Bool
      , forall o. ExpRefInfo o -> Bool
    eriIsEliminand    :: Bool
      , forall o. ExpRefInfo o -> Maybe ([UId o], [Elr o])
    eriUsedVars       :: Maybe ([UId o], [Elr o])
      , forall o. ExpRefInfo o -> Maybe Bool
    eriIotaStep       :: Maybe Bool
      , forall o. ExpRefInfo o -> Bool
    eriPickSubsVar    :: Bool
      , forall o. ExpRefInfo o -> Maybe EqReasoningState
    eriEqRState       :: Maybe EqReasoningState
      }

    initExpRefInfo :: ExpRefInfo o
    initExpRefInfo :: forall o. ExpRefInfo o
    initExpRefInfo = ExpRefInfo :: forall o.
    Maybe (RefInfo o)
    -> [RefInfo o]
    -> Bool
    -> Bool
    -> Maybe ([UId o], [Elr o])
    -> Maybe Bool
    -> Bool
    -> Maybe EqReasoningState
    -> ExpRefInfo o
    ExpRefInfo
      { eriMain :: Maybe (RefInfo o)
    eriMain           = Maybe (RefInfo o)
    forall a. Maybe a
    Nothing
      , eriUnifs :: [RefInfo o]
    eriUnifs          = []
      , eriInfTypeUnknown :: Bool
    eriInfTypeUnknown = Bool
    False
      , eriIsEliminand :: Bool
    eriIsEliminand    = Bool
    False
      , eriUsedVars :: Maybe ([UId o], [Elr o])
    eriUsedVars       = Maybe ([UId o], [Elr o])
    forall a. Maybe a
    Nothing
      , eriIotaStep :: Maybe Bool
    eriIotaStep       = Maybe Bool
    forall a. Maybe a
    Nothing
      , eriPickSubsVar :: Bool
    eriPickSubsVar    = Bool
    False
      , eriEqRState :: Maybe EqReasoningState
    eriEqRState       = Maybe EqReasoningState
    forall a. Maybe a
    Nothing
      }

    getinfo :: [RefInfo o] -> ExpRefInfo o
    getinfo :: forall o. [RefInfo o] -> ExpRefInfo o
    getinfo = (ExpRefInfo o -> RefInfo o -> ExpRefInfo o)
    -> ExpRefInfo o -> [RefInfo o] -> ExpRefInfo o
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl ExpRefInfo o -> RefInfo o -> ExpRefInfo o
    forall o. ExpRefInfo o -> RefInfo o -> ExpRefInfo o
    step ExpRefInfo o
    forall o. ExpRefInfo o
    initExpRefInfo where

      step :: ExpRefInfo o -> RefInfo o -> ExpRefInfo o
      step :: forall o. ExpRefInfo o -> RefInfo o -> ExpRefInfo o
    step ExpRefInfo o
    eri x :: RefInfo o
    x@RIMainInfo{}           = ExpRefInfo o
    eri { eriMain :: Maybe (RefInfo o)
    eriMain  = RefInfo o -> Maybe (RefInfo o)
    forall a. a -> Maybe a
    Just RefInfo o
    x }
      step ExpRefInfo o
    eri x :: RefInfo o
    x@RIUnifInfo{}           = ExpRefInfo o
    eri { eriUnifs :: [RefInfo o]
    eriUnifs = RefInfo o
    x RefInfo o -> [RefInfo o] -> [RefInfo o]
    forall a. a -> [a] -> [a]
    : ExpRefInfo o -> [RefInfo o]
    forall o. ExpRefInfo o -> [RefInfo o]
    eriUnifs ExpRefInfo o
    eri }
      step ExpRefInfo o
    eri RefInfo o
    RIInferredTypeUnknown    = ExpRefInfo o
    eri { eriInfTypeUnknown :: Bool
    eriInfTypeUnknown = Bool
    True }
      step ExpRefInfo o
    eri RefInfo o
    RINotConstructor         = ExpRefInfo o
    eri { eriIsEliminand :: Bool
    eriIsEliminand = Bool
    True }
      step ExpRefInfo o
    eri (RIUsedVars [UId o]
    nuids [Elr o]
    nused) = ExpRefInfo o
    eri { eriUsedVars :: Maybe ([UId o], [Elr o])
    eriUsedVars = ([UId o], [Elr o]) -> Maybe ([UId o], [Elr o])
    forall a. a -> Maybe a
    Just ([UId o]
    nuids, [Elr o]
    nused) }
      step ExpRefInfo o
    eri (RIIotaStep Bool
    semif)       = ExpRefInfo o
    eri { eriIotaStep :: Maybe Bool
    eriIotaStep = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    iota' } where
        iota' :: Bool
    iota' = Bool
    semif Bool -> Bool -> Bool
    || (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True Maybe Bool -> Maybe Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (ExpRefInfo o -> Maybe Bool
    forall o. ExpRefInfo o -> Maybe Bool
    eriIotaStep ExpRefInfo o
    eri)
      step ExpRefInfo o
    eri RefInfo o
    RIPickSubsvar            = ExpRefInfo o
    eri { eriPickSubsVar :: Bool
    eriPickSubsVar = Bool
    True }
      step ExpRefInfo o
    eri (RIEqRState EqReasoningState
    s)           = ExpRefInfo o
    eri { eriEqRState :: Maybe EqReasoningState
    eriEqRState = EqReasoningState -> Maybe EqReasoningState
    forall a. a -> Maybe a
    Just EqReasoningState
    s }
      step ExpRefInfo o
    eri RefInfo o
    _ = ExpRefInfo o
    forall a. HasCallStack => a
    __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 :: forall o. [CAction o] -> Nat -> Maybe Nat
    univar [CAction o]
    cl Nat
    v = [CAction o] -> Nat -> Nat -> Maybe Nat
    forall o. [CAction o] -> Nat -> Nat -> Maybe Nat
    getOutsideName [CAction o]
    cl Nat
    v Nat
    0 where

      getOutsideName :: [CAction o] -> Nat -> Nat -> Maybe Nat
      -- @v@ is offset by @v'@ binders
      getOutsideName :: forall o. [CAction o] -> Nat -> Nat -> Maybe Nat
    getOutsideName []            Nat
    v Nat
    v' = Nat -> Maybe Nat
    forall a. a -> Maybe a
    Just (Nat
    v' Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    v)
      -- @v@ was introduced by the weakening: disappears
      getOutsideName (Weak Nat
    n : [CAction o]
    _)  Nat
    v Nat
    v' | Nat
    v Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    n = Maybe Nat
    forall a. Maybe a
    Nothing
      -- @v@ was introduced before the weakening: strengthened
      getOutsideName (Weak Nat
    n : [CAction o]
    xs) Nat
    v Nat
    v' = [CAction o] -> Nat -> Nat -> Maybe Nat
    forall o. [CAction o] -> Nat -> Nat -> Maybe Nat
    getOutsideName [CAction o]
    xs (Nat
    v Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    n) Nat
    v'
      -- Name of @v@ before the substitution was pushed in
      -- had to be offset by 1
      getOutsideName (Sub ICExp o
    _  : [CAction o]
    xs) Nat
    v Nat
    v' = [CAction o] -> Nat -> Nat -> Maybe Nat
    forall o. [CAction o] -> Nat -> Nat -> Maybe Nat
    getOutsideName [CAction o]
    xs Nat
    v (Nat
    v' Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1)
      -- If this is the place where @v@ was bound, it used to
      -- be called 0 + offset of all the vars substituted for
      getOutsideName (CAction o
    Skip   : [CAction o]
    _)  Nat
    0 Nat
    v' = Nat -> Maybe Nat
    forall a. a -> Maybe a
    Just Nat
    v'
      -- Going over a binder: de Bruijn name of @v@ decreased
      -- but offset increased
      getOutsideName (CAction o
    Skip   : [CAction o]
    xs) Nat
    v Nat
    v' = [CAction o] -> Nat -> Nat -> Maybe Nat
    forall o. [CAction o] -> Nat -> Nat -> Maybe Nat
    getOutsideName [CAction o]
    xs (Nat
    v Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) (Nat
    v' Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1)

    -- | List of the variables instantiated by the substitution
    subsvars :: [CAction o] -> [Nat]
    subsvars :: forall o. [CAction o] -> [Nat]
    subsvars = Nat -> [CAction o] -> [Nat]
    forall o. Nat -> [CAction o] -> [Nat]
    f Nat
    0 where

      f :: Nat -> [CAction o] -> [Nat]
      f :: forall o. Nat -> [CAction o] -> [Nat]
    f Nat
    n []            = []
      f Nat
    n (Weak Nat
    _ : [CAction o]
    xs) = Nat -> [CAction o] -> [Nat]
    forall o. Nat -> [CAction o] -> [Nat]
    f Nat
    n [CAction o]
    xs -- why?
      f Nat
    n (Sub ICExp o
    _  : [CAction o]
    xs) = Nat
    n Nat -> [Nat] -> [Nat]
    forall a. a -> [a] -> [a]
    : Nat -> [CAction o] -> [Nat]
    forall o. Nat -> [CAction o] -> [Nat]
    f (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) [CAction o]
    xs
      f Nat
    n (CAction o
    Skip   : [CAction o]
    xs) = Nat -> [CAction o] -> [Nat]
    forall o. Nat -> [CAction o] -> [Nat]
    f (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1) [CAction o]
    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 :: forall blk a. MId -> RefCreateEnv blk (Abs (MM a blk))
    newAbs MId
    mid = MId -> MM a blk -> Abs (MM a blk)
    forall a. MId -> a -> Abs a
    Abs MId
    mid (MM a blk -> Abs (MM a blk))
    -> RefCreateEnv blk (MM a blk) -> RefCreateEnv blk (Abs (MM a blk))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RefCreateEnv blk (MM a blk)
    forall blk a. RefCreateEnv blk (MM a blk)
    newPlaceholder

    newLam :: Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)
    newLam :: forall o. Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)
    newLam Hiding
    hid MId
    mid = Hiding -> Abs (MExp o) -> Exp o
    forall o. Hiding -> Abs (MExp o) -> Exp o
    Lam Hiding
    hid (Abs (MExp o) -> Exp o)
    -> RefCreateEnv (RefInfo o) (Abs (MExp o))
    -> RefCreateEnv (RefInfo o) (Exp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MId -> RefCreateEnv (RefInfo o) (Abs (MExp o))
    forall blk a. MId -> RefCreateEnv blk (Abs (MM a blk))
    newAbs MId
    mid

    newPi :: UId o -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)
    newPi :: forall o.
    UId o -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)
    newPi UId o
    uid Bool
    dep Hiding
    hid = Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
    forall o.
    Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
    Pi (UId o -> Maybe (UId o)
    forall a. a -> Maybe a
    Just UId o
    uid) Hiding
    hid Bool
    dep (MExp o -> Abs (MExp o) -> Exp o)
    -> RefCreateEnv (RefInfo o) (MExp o)
    -> RefCreateEnv (RefInfo o) (Abs (MExp o) -> Exp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RefCreateEnv (RefInfo o) (MExp o)
    forall blk a. RefCreateEnv blk (MM a blk)
    newPlaceholder RefCreateEnv (RefInfo o) (Abs (MExp o) -> Exp o)
    -> RefCreateEnv (RefInfo o) (Abs (MExp o))
    -> RefCreateEnv (RefInfo o) (Exp o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> MId -> RefCreateEnv (RefInfo o) (Abs (MExp o))
    forall blk a. MId -> RefCreateEnv blk (Abs (MM a blk))
    newAbs MId
    NoId

    foldArgs :: [(Hiding, MExp o)] -> MArgList o
    foldArgs :: forall o. [(Hiding, MExp o)] -> MArgList o
    foldArgs = ((Hiding, MExp o) -> MArgList o -> MArgList o)
    -> MArgList o -> [(Hiding, MExp o)] -> MArgList o
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\ (Hiding
    h, MExp o
    a) MArgList o
    sp -> ArgList o -> MArgList o
    forall a blk. a -> MM a blk
    NotM (ArgList o -> MArgList o) -> ArgList o -> MArgList o
    forall a b. (a -> b) -> a -> b
    $ Hiding -> MExp o -> MArgList o -> ArgList o
    forall o. Hiding -> MExp o -> MArgList o -> ArgList o
    ALCons Hiding
    h MExp o
    a MArgList o
    sp) (ArgList o -> MArgList o
    forall a blk. a -> MM a blk
    NotM ArgList o
    forall o. ArgList o
    ALNil)

    -- | New spine of arguments potentially using placeholders

    newArgs' :: [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)
    newArgs' :: forall o.
    [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)
    newArgs' [Hiding]
    h [MExp o]
    tms = [(Hiding, MExp o)] -> MArgList o
    forall o. [(Hiding, MExp o)] -> MArgList o
    foldArgs ([(Hiding, MExp o)] -> MArgList o)
    -> ([MExp o] -> [(Hiding, MExp o)]) -> [MExp o] -> MArgList o
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Hiding] -> [MExp o] -> [(Hiding, MExp o)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Hiding]
    h ([MExp o] -> [(Hiding, MExp o)])
    -> ([MExp o] -> [MExp o]) -> [MExp o] -> [(Hiding, MExp o)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([MExp o] -> [MExp o] -> [MExp o]
    forall a. [a] -> [a] -> [a]
    ++ [MExp o]
    tms) ([MExp o] -> MArgList o)
    -> RefCreateEnv (RefInfo o) [MExp o]
    -> RefCreateEnv (RefInfo o) (MArgList o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Nat
    -> RefCreateEnv (RefInfo o) (MExp o)
    -> RefCreateEnv (RefInfo o) [MExp o]
    forall (m :: * -> *) a. Applicative m => Nat -> m a -> m [a]
    replicateM Nat
    size RefCreateEnv (RefInfo o) (MExp o)
    forall blk a. RefCreateEnv blk (MM a blk)
    newPlaceholder
      where size :: Nat
    size = [Hiding] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Hiding]
    h Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - [MExp o] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [MExp o]
    tms

    newArgs :: [Hiding] -> RefCreateEnv (RefInfo o) (MArgList o)
    newArgs :: forall o. [Hiding] -> RefCreateEnv (RefInfo o) (MArgList o)
    newArgs [Hiding]
    h = [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)
    forall o.
    [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)
    newArgs' [Hiding]
    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' :: forall o.
    UId o
    -> ConstRef o
    -> [Hiding]
    -> [MExp o]
    -> RefCreateEnv (RefInfo o) (Exp o)
    newApp' UId o
    meta ConstRef o
    cst [Hiding]
    hds [MExp o]
    tms =
      Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    forall o.
    Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    App (UId o -> Maybe (UId o)
    forall a. a -> Maybe a
    Just UId o
    meta) (OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o)
    -> RefCreateEnv (RefInfo o) (OKHandle (RefInfo o))
    -> RefCreateEnv (RefInfo o) (Elr o -> MArgList o -> Exp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RefCreateEnv (RefInfo o) (OKHandle (RefInfo o))
    forall blk. RefCreateEnv blk (OKHandle blk)
    newOKHandle RefCreateEnv (RefInfo o) (Elr o -> MArgList o -> Exp o)
    -> RefCreateEnv (RefInfo o) (Elr o)
    -> RefCreateEnv (RefInfo o) (MArgList o -> Exp o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Elr o -> RefCreateEnv (RefInfo o) (Elr o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ConstRef o -> Elr o
    forall o. ConstRef o -> Elr o
    Const ConstRef o
    cst) RefCreateEnv (RefInfo o) (MArgList o -> Exp o)
    -> RefCreateEnv (RefInfo o) (MArgList o)
    -> RefCreateEnv (RefInfo o) (Exp o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)
    forall o.
    [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)
    newArgs' [Hiding]
    hds [MExp o]
    tms

    newApp :: UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
    newApp :: forall o.
    UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
    newApp UId o
    meta ConstRef o
    cst [Hiding]
    hds = UId o
    -> ConstRef o
    -> [Hiding]
    -> [MExp o]
    -> RefCreateEnv (RefInfo o) (Exp o)
    forall o.
    UId o
    -> ConstRef o
    -> [Hiding]
    -> [MExp o]
    -> RefCreateEnv (RefInfo o) (Exp o)
    newApp' UId o
    meta ConstRef o
    cst [Hiding]
    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 :: forall o. UId o -> EqReasoningConsts o -> Move o
    eqStep UId o
    meta EqReasoningConsts o
    eqrc = Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move Cost
    costEqStep (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall a b. (a -> b) -> a -> b
    $ UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
    forall o.
    UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
    newApp UId o
    meta (EqReasoningConsts o -> ConstRef o
    forall o. EqReasoningConsts o -> ConstRef o
    eqrcStep EqReasoningConsts o
    eqrc)
      [Hiding
    Hidden, Hiding
    Hidden, Hiding
    NotHidden, Hiding
    Hidden, Hiding
    Hidden, Hiding
    NotHidden, Hiding
    NotHidden]

    eqEnd :: UId o -> EqReasoningConsts o -> Move o
    eqEnd :: forall o. UId o -> EqReasoningConsts o -> Move o
    eqEnd UId o
    meta EqReasoningConsts o
    eqrc = Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move Cost
    costEqEnd (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall a b. (a -> b) -> a -> b
    $ UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
    forall o.
    UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
    newApp UId o
    meta (EqReasoningConsts o -> ConstRef o
    forall o. EqReasoningConsts o -> ConstRef o
    eqrcEnd EqReasoningConsts o
    eqrc)
      [Hiding
    Hidden, Hiding
    Hidden, Hiding
    NotHidden]

    eqCong :: UId o -> EqReasoningConsts o -> Move o
    eqCong :: forall o. UId o -> EqReasoningConsts o -> Move o
    eqCong UId o
    meta EqReasoningConsts o
    eqrc = Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move Cost
    costEqCong (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall a b. (a -> b) -> a -> b
    $ UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
    forall o.
    UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
    newApp UId o
    meta (EqReasoningConsts o -> ConstRef o
    forall o. EqReasoningConsts o -> ConstRef o
    eqrcCong EqReasoningConsts o
    eqrc)
      [Hiding
    Hidden, Hiding
    Hidden, Hiding
    Hidden, Hiding
    Hidden, Hiding
    NotHidden, Hiding
    Hidden, Hiding
    Hidden, Hiding
    NotHidden]

    eqSym :: UId o -> EqReasoningConsts o -> Move o
    eqSym :: forall o. UId o -> EqReasoningConsts o -> Move o
    eqSym UId o
    meta EqReasoningConsts o
    eqrc = Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move Cost
    costEqSym (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall a b. (a -> b) -> a -> b
    $ UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
    forall o.
    UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
    newApp UId o
    meta (EqReasoningConsts o -> ConstRef o
    forall o. EqReasoningConsts o -> ConstRef o
    eqrcSym EqReasoningConsts o
    eqrc)
      [Hiding
    Hidden, Hiding
    Hidden, Hiding
    Hidden, Hiding
    Hidden, Hiding
    NotHidden]

    eqBeginStep2 :: UId o -> EqReasoningConsts o -> Move o
    eqBeginStep2 :: forall o. UId o -> EqReasoningConsts o -> Move o
    eqBeginStep2 UId o
    meta EqReasoningConsts o
    eqrc = Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move Cost
    costEqStep (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall a b. (a -> b) -> a -> b
    $ do
      Exp o
    e1 <- UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
    forall o.
    UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
    newApp UId o
    meta (EqReasoningConsts o -> ConstRef o
    forall o. EqReasoningConsts o -> ConstRef o
    eqrcStep EqReasoningConsts o
    eqrc)
              [Hiding
    Hidden, Hiding
    Hidden, Hiding
    NotHidden, Hiding
    Hidden, Hiding
    Hidden, Hiding
    NotHidden, Hiding
    NotHidden]
      Exp o
    e2 <- UId o
    -> ConstRef o
    -> [Hiding]
    -> [MExp o]
    -> RefCreateEnv (RefInfo o) (Exp o)
    forall o.
    UId o
    -> ConstRef o
    -> [Hiding]
    -> [MExp o]
    -> RefCreateEnv (RefInfo o) (Exp o)
    newApp' UId o
    meta (EqReasoningConsts o -> ConstRef o
    forall o. EqReasoningConsts o -> ConstRef o
    eqrcStep EqReasoningConsts o
    eqrc)
              [Hiding
    Hidden, Hiding
    Hidden, Hiding
    NotHidden, Hiding
    Hidden, Hiding
    Hidden, Hiding
    NotHidden, Hiding
    NotHidden]
              [Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM Exp o
    e1]
      UId o
    -> ConstRef o
    -> [Hiding]
    -> [MExp o]
    -> RefCreateEnv (RefInfo o) (Exp o)
    forall o.
    UId o
    -> ConstRef o
    -> [Hiding]
    -> [MExp o]
    -> RefCreateEnv (RefInfo o) (Exp o)
    newApp' UId o
    meta (EqReasoningConsts o -> ConstRef o
    forall o. EqReasoningConsts o -> ConstRef o
    eqrcBegin EqReasoningConsts o
    eqrc) [Hiding
    Hidden, Hiding
    Hidden, Hiding
    Hidden, Hiding
    Hidden, Hiding
    NotHidden]
        [Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM Exp o
    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 :: forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)
    pickUid [UId o]
    used [Maybe (UId o)]
    seen = (Maybe (UId o), Bool)
    -> (Maybe (UId o) -> (Maybe (UId o), Bool))
    -> Maybe (Maybe (UId o))
    -> (Maybe (UId o), Bool)
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe ([Maybe (UId o)] -> Maybe (UId o)
    forall a. [a] -> a
    head [Maybe (UId o)]
    seen, Bool
    False) (, Bool
    True) (Maybe (Maybe (UId o)) -> (Maybe (UId o), Bool))
    -> Maybe (Maybe (UId o)) -> (Maybe (UId o), Bool)
    forall a b. (a -> b) -> a -> b
    $ [Maybe (UId o)] -> Maybe (Maybe (UId o))
    firstUnused [Maybe (UId o)]
    seen where
      {- ?? which uid to pick -}

      firstUnused :: [Maybe (UId o)] -> Maybe (Maybe (UId o))
      firstUnused :: [Maybe (UId o)] -> Maybe (Maybe (UId o))
    firstUnused []                 = Maybe (Maybe (UId o))
    forall a. Maybe a
    Nothing
      firstUnused (Maybe (UId o)
    Nothing     : [Maybe (UId o)]
    _)  = Maybe (UId o) -> Maybe (Maybe (UId o))
    forall a. a -> Maybe a
    Just Maybe (UId o)
    forall a. Maybe a
    Nothing
      firstUnused (mu :: Maybe (UId o)
    mu@(Just UId o
    u) : [Maybe (UId o)]
    us) =
        if UId o
    u UId o -> [UId o] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [UId o]
    used then [Maybe (UId o)] -> Maybe (Maybe (UId o))
    firstUnused [Maybe (UId o)]
    us else Maybe (UId o) -> Maybe (Maybe (UId o))
    forall a. a -> Maybe a
    Just Maybe (UId o)
    mu

    instance Refinable (Exp o) (RefInfo o) where
     refinements :: RefInfo o
    -> [RefInfo o]
    -> Metavar (Exp o) (RefInfo o)
    -> IO [Move' (RefInfo o) (Exp o)]
    refinements RefInfo o
    envinfo [RefInfo o]
    infos Metavar (Exp o) (RefInfo o)
    meta =
      let
       hints :: [(ConstRef o, HintMode)]
    hints = RefInfo o -> [(ConstRef o, HintMode)]
    forall o. RefInfo o -> [(ConstRef o, HintMode)]
    rieHints RefInfo o
    envinfo
       deffreevars :: Nat
    deffreevars = RefInfo o -> Nat
    forall o. RefInfo o -> Nat
    rieDefFreeVars RefInfo o
    envinfo

       meqr :: Maybe (EqReasoningConsts o)
    meqr = RefInfo o -> Maybe (EqReasoningConsts o)
    forall o. RefInfo o -> Maybe (EqReasoningConsts o)
    rieEqReasoningConsts RefInfo o
    envinfo

       ExpRefInfo { eriMain :: forall o. ExpRefInfo o -> Maybe (RefInfo o)
    eriMain  = Just (RIMainInfo Nat
    n HNExp o
    tt Bool
    iotastepdone)
                  , eriUnifs :: forall o. ExpRefInfo o -> [RefInfo o]
    eriUnifs = [RefInfo o]
    unis
                  , eriInfTypeUnknown :: forall o. ExpRefInfo o -> Bool
    eriInfTypeUnknown = Bool
    inftypeunknown
                  , eriIsEliminand :: forall o. ExpRefInfo o -> Bool
    eriIsEliminand = Bool
    iseliminand -- TODO:: Defined but not used
                  , eriUsedVars :: forall o. ExpRefInfo o -> Maybe ([UId o], [Elr o])
    eriUsedVars = Just ([Metavar (Exp o) (RefInfo o)]
    uids, [Elr o]
    usedvars)
                  , eriIotaStep :: forall o. ExpRefInfo o -> Maybe Bool
    eriIotaStep = Maybe Bool
    iotastep
                  , eriPickSubsVar :: forall o. ExpRefInfo o -> Bool
    eriPickSubsVar = Bool
    picksubsvar -- TODO:: Defined but not used
                  , eriEqRState :: forall o. ExpRefInfo o -> Maybe EqReasoningState
    eriEqRState = Maybe EqReasoningState
    meqrstate
                  } = [RefInfo o] -> ExpRefInfo o
    forall o. [RefInfo o] -> ExpRefInfo o
    getinfo [RefInfo o]
    infos

       eqrstate :: EqReasoningState
    eqrstate = EqReasoningState -> Maybe EqReasoningState -> EqReasoningState
    forall a. a -> Maybe a -> a
    fromMaybe EqReasoningState
    EqRSNone Maybe EqReasoningState
    meqrstate

       set :: Nat -> m (Exp o)
    set Nat
    l = Exp o -> m (Exp o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp o -> m (Exp o)) -> Exp o -> m (Exp o)
    forall a b. (a -> b) -> a -> b
    $ Sort -> Exp o
    forall o. Sort -> Exp o
    Sort (Nat -> Sort
    Set Nat
    l)
      in case [RefInfo o]
    unis of
       [] ->
        let

         eqr :: EqReasoningConsts o
    eqr = EqReasoningConsts o
    -> Maybe (EqReasoningConsts o) -> EqReasoningConsts o
    forall a. a -> Maybe a -> a
    fromMaybe EqReasoningConsts o
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Maybe (EqReasoningConsts o)
    meqr
         eq_end :: Move' (RefInfo o) (Exp o)
    eq_end         = Metavar (Exp o) (RefInfo o)
    -> EqReasoningConsts o -> Move' (RefInfo o) (Exp o)
    forall o. UId o -> EqReasoningConsts o -> Move o
    eqEnd  Metavar (Exp o) (RefInfo o)
    meta EqReasoningConsts o
    eqr
         eq_step :: Move' (RefInfo o) (Exp o)
    eq_step        = Metavar (Exp o) (RefInfo o)
    -> EqReasoningConsts o -> Move' (RefInfo o) (Exp o)
    forall o. UId o -> EqReasoningConsts o -> Move o
    eqStep Metavar (Exp o) (RefInfo o)
    meta EqReasoningConsts o
    eqr
         eq_cong :: Move' (RefInfo o) (Exp o)
    eq_cong        = Metavar (Exp o) (RefInfo o)
    -> EqReasoningConsts o -> Move' (RefInfo o) (Exp o)
    forall o. UId o -> EqReasoningConsts o -> Move o
    eqCong Metavar (Exp o) (RefInfo o)
    meta EqReasoningConsts o
    eqr
         eq_sym :: Move' (RefInfo o) (Exp o)
    eq_sym         = Metavar (Exp o) (RefInfo o)
    -> EqReasoningConsts o -> Move' (RefInfo o) (Exp o)
    forall o. UId o -> EqReasoningConsts o -> Move o
    eqSym  Metavar (Exp o) (RefInfo o)
    meta EqReasoningConsts o
    eqr
         eq_begin_step2 :: Move' (RefInfo o) (Exp o)
    eq_begin_step2 = Metavar (Exp o) (RefInfo o)
    -> EqReasoningConsts o -> Move' (RefInfo o) (Exp o)
    forall o. UId o -> EqReasoningConsts o -> Move o
    eqBeginStep2 Metavar (Exp o) (RefInfo o)
    meta EqReasoningConsts o
    eqr

         adjustCost :: Cost -> Cost
    adjustCost Cost
    i = if Bool
    inftypeunknown then Cost
    costInferredTypeUnkown else Cost
    i
         varcost :: Nat -> Cost
    varcost Nat
    v | Nat
    v Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    deffreevars = Cost -> Cost
    adjustCost (Cost -> Cost) -> Cost -> Cost
    forall a b. (a -> b) -> a -> b
    $
           if Nat
    v Nat -> [Nat] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` ((Elr o -> Maybe Nat) -> [Elr o] -> [Nat]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe Elr o -> Maybe Nat
    forall o. Elr o -> Maybe Nat
    getVar [Elr o]
    usedvars)
           then Cost
    costAppVarUsed else Cost
    costAppVar
         varcost Nat
    v | Bool
    otherwise           = Cost -> Cost
    adjustCost Cost
    costAppHint
         varapps :: [Move' (RefInfo o) (Exp o)]
    varapps  = (Nat -> Move' (RefInfo o) (Exp o))
    -> [Nat] -> [Move' (RefInfo o) (Exp o)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ Nat
    v -> Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move (Nat -> Cost
    varcost Nat
    v) (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall a b. (a -> b) -> a -> b
    $ Nat
    -> Metavar (Exp o) (RefInfo o)
    -> Maybe (Metavar (Exp o) (RefInfo o))
    -> Elr o
    -> RefCreateEnv (RefInfo o) (Exp o)
    app Nat
    n Metavar (Exp o) (RefInfo o)
    meta Maybe (Metavar (Exp o) (RefInfo o))
    forall a. Maybe a
    Nothing (Nat -> Elr o
    forall o. Nat -> Elr o
    Var Nat
    v)) [Nat
    0..Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1]
         hintapps :: [Move' (RefInfo o) (Exp o)]
    hintapps = ((ConstRef o, HintMode) -> Move' (RefInfo o) (Exp o))
    -> [(ConstRef o, HintMode)] -> [Move' (RefInfo o) (Exp o)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(ConstRef o
    c, HintMode
    hm) -> Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move (ConstRef o -> HintMode -> Cost
    cost ConstRef o
    c HintMode
    hm) (Nat
    -> Metavar (Exp o) (RefInfo o)
    -> Maybe (Metavar (Exp o) (RefInfo o))
    -> Elr o
    -> RefCreateEnv (RefInfo o) (Exp o)
    app Nat
    n Metavar (Exp o) (RefInfo o)
    meta Maybe (Metavar (Exp o) (RefInfo o))
    forall a. Maybe a
    Nothing (ConstRef o -> Elr o
    forall o. ConstRef o -> Elr o
    Const ConstRef o
    c))) [(ConstRef o, HintMode)]
    hints
           where
             cost :: ConstRef o -> HintMode -> Cost
             cost :: ConstRef o -> HintMode -> Cost
    cost ConstRef o
    c HintMode
    hm = Cost -> Cost
    adjustCost (Cost -> Cost) -> Cost -> Cost
    forall a b. (a -> b) -> a -> b
    $ case (Maybe Bool
    iotastep , HintMode
    hm) of
               (Just Bool
    _  , HintMode
    _       ) -> Cost
    costIotaStep
               (Maybe Bool
    Nothing , HintMode
    HMNormal) ->
                 if ConstRef o
    c ConstRef o -> [ConstRef o] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` ((Elr o -> Maybe (ConstRef o)) -> [Elr o] -> [ConstRef o]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe Elr o -> Maybe (ConstRef o)
    forall o. Elr o -> Maybe (ConstRef o)
    getConst [Elr o]
    usedvars)
                 then Cost
    costAppHintUsed else Cost
    costAppHint
               (Maybe Bool
    Nothing , HintMode
    HMRecCall) ->
                 if ConstRef o
    c ConstRef o -> [ConstRef o] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` ((Elr o -> Maybe (ConstRef o)) -> [Elr o] -> [ConstRef o]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe Elr o -> Maybe (ConstRef o)
    forall o. Elr o -> Maybe (ConstRef o)
    getConst [Elr o]
    usedvars)
                 then Cost
    costAppRecCallUsed else Cost
    costAppRecCall
         generics :: [Move' (RefInfo o) (Exp o)]
    generics = [Move' (RefInfo o) (Exp o)]
    varapps [Move' (RefInfo o) (Exp o)]
    -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall a. [a] -> [a] -> [a]
    ++ [Move' (RefInfo o) (Exp o)]
    hintapps
        in case HNExp o -> HNExp' o
    forall a o. WithSeenUIds a o -> a
    rawValue HNExp o
    tt of

         HNExp' o
    _ | EqReasoningState
    eqrstate EqReasoningState -> EqReasoningState -> Bool
    forall a. Eq a => a -> a -> Bool
    == EqReasoningState
    EqRSChain ->
          [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Move' (RefInfo o) (Exp o)
    eq_end, Move' (RefInfo o) (Exp o)
    eq_step]

         HNPi Hiding
    hid Bool
    _ ICExp o
    _ (Abs MId
    id ICExp o
    _) -> [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)])
    -> [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
    forall a b. (a -> b) -> a -> b
    $
             Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move (Cost -> Cost
    adjustCost (if Bool
    iotastepdone then Cost
    costLamUnfold else Cost
    costLam)) (Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)
    forall o. Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)
    newLam Hiding
    hid MId
    id)
           Move' (RefInfo o) (Exp o)
    -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall a. a -> [a] -> [a]
    : Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move Cost
    costAbsurdLam (Exp o -> RefCreateEnv (RefInfo o) (Exp o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp o -> RefCreateEnv (RefInfo o) (Exp o))
    -> Exp o -> RefCreateEnv (RefInfo o) (Exp o)
    forall a b. (a -> b) -> a -> b
    $ Hiding -> Exp o
    forall o. Hiding -> Exp o
    AbsurdLambda Hiding
    hid)
           Move' (RefInfo o) (Exp o)
    -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall a. a -> [a] -> [a]
    : [Move' (RefInfo o) (Exp o)]
    generics

         HNSort (Set Nat
    l) -> [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)])
    -> [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
    forall a b. (a -> b) -> a -> b
    $
              (Nat -> Move' (RefInfo o) (Exp o))
    -> [Nat] -> [Move' (RefInfo o) (Exp o)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move (Cost -> Cost
    adjustCost Cost
    costSort) (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
    -> (Nat -> RefCreateEnv (RefInfo o) (Exp o))
    -> Nat
    -> Move' (RefInfo o) (Exp o)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> RefCreateEnv (RefInfo o) (Exp o)
    forall {m :: * -> *} {o}. Monad m => Nat -> m (Exp o)
    set) [Nat
    0..Nat
    l Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1]
           [Move' (RefInfo o) (Exp o)]
    -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall a. [a] -> [a] -> [a]
    ++ (Hiding -> Move' (RefInfo o) (Exp o))
    -> [Hiding] -> [Move' (RefInfo o) (Exp o)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move (Cost -> Cost
    adjustCost Cost
    costPi) (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
    -> (Hiding -> RefCreateEnv (RefInfo o) (Exp o))
    -> Hiding
    -> Move' (RefInfo o) (Exp o)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Metavar (Exp o) (RefInfo o)
    -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)
    forall o.
    UId o -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)
    newPi Metavar (Exp o) (RefInfo o)
    meta Bool
    True) [Hiding
    NotHidden, Hiding
    Hidden]
           [Move' (RefInfo o) (Exp o)]
    -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall a. [a] -> [a] -> [a]
    ++ [Move' (RefInfo o) (Exp o)]
    generics

         HNApp (Const ConstRef o
    c) ICArgList o
    _ -> do
          ConstDef o
    cd <- ConstRef o -> IO (ConstDef o)
    forall a. IORef a -> IO a
    readIORef ConstRef o
    c
          [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)])
    -> [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
    forall a b. (a -> b) -> a -> b
    $ case ConstDef o -> DeclCont o
    forall o. ConstDef o -> DeclCont o
    cdcont ConstDef o
    cd of

           Datatype [ConstRef o]
    cons [ConstRef o]
    _ | EqReasoningState
    eqrstate EqReasoningState -> EqReasoningState -> Bool
    forall a. Eq a => a -> a -> Bool
    == EqReasoningState
    EqRSNone ->
             (ConstRef o -> Move' (RefInfo o) (Exp o))
    -> [ConstRef o] -> [Move' (RefInfo o) (Exp o)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ConstRef o
    c -> Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move (Cost -> Cost
    adjustCost (Cost -> Cost) -> Cost -> Cost
    forall a b. (a -> b) -> a -> b
    $ case Maybe Bool
    iotastep of
                                             Just Bool
    True -> Cost
    costUnification
                                             Maybe Bool
    _ -> if [ConstRef o] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [ConstRef o]
    cons Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Nat
    1
                                                  then Cost
    costAppConstructorSingle
                                                  else Cost
    costAppConstructor)
                             (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall a b. (a -> b) -> a -> b
    $ Nat
    -> Metavar (Exp o) (RefInfo o)
    -> Maybe (Metavar (Exp o) (RefInfo o))
    -> Elr o
    -> RefCreateEnv (RefInfo o) (Exp o)
    app Nat
    n Metavar (Exp o) (RefInfo o)
    meta Maybe (Metavar (Exp o) (RefInfo o))
    forall a. Maybe a
    Nothing (ConstRef o -> Elr o
    forall o. ConstRef o -> Elr o
    Const ConstRef o
    c)) [ConstRef o]
    cons
             [Move' (RefInfo o) (Exp o)]
    -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall a. [a] -> [a] -> [a]
    ++ [Move' (RefInfo o) (Exp o)]
    generics
             [Move' (RefInfo o) (Exp o)]
    -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall a. [a] -> [a] -> [a]
    ++ (Bool -> [()]
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool
    -> (EqReasoningConsts o -> Bool)
    -> Maybe (EqReasoningConsts o)
    -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False ((ConstRef o
    c ConstRef o -> ConstRef o -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (ConstRef o -> Bool)
    -> (EqReasoningConsts o -> ConstRef o)
    -> EqReasoningConsts o
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . EqReasoningConsts o -> ConstRef o
    forall o. EqReasoningConsts o -> ConstRef o
    eqrcId) Maybe (EqReasoningConsts o)
    meqr)
                [()] -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
    *> [Move' (RefInfo o) (Exp o)
    eq_sym, Move' (RefInfo o) (Exp o)
    eq_cong, Move' (RefInfo o) (Exp o)
    eq_begin_step2])

           DeclCont o
    _ | EqReasoningState
    eqrstate EqReasoningState -> EqReasoningState -> Bool
    forall a. Eq a => a -> a -> Bool
    == EqReasoningState
    EqRSPrf1 -> [Move' (RefInfo o) (Exp o)]
    generics [Move' (RefInfo o) (Exp o)]
    -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall a. [a] -> [a] -> [a]
    ++ [Move' (RefInfo o) (Exp o)
    eq_sym, Move' (RefInfo o) (Exp o)
    eq_cong]
           DeclCont o
    _ | EqReasoningState
    eqrstate EqReasoningState -> EqReasoningState -> Bool
    forall a. Eq a => a -> a -> Bool
    == EqReasoningState
    EqRSPrf2 -> [Move' (RefInfo o) (Exp o)]
    generics [Move' (RefInfo o) (Exp o)]
    -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall a. [a] -> [a] -> [a]
    ++ [Move' (RefInfo o) (Exp o)
    eq_cong]

           DeclCont o
    _ -> [Move' (RefInfo o) (Exp o)]
    generics
         HNExp' o
    _ -> [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Move' (RefInfo o) (Exp o)]
    generics
       (RIUnifInfo [CAction o]
    cl HNExp o
    hne : [RefInfo o]
    _) ->
        let
         subsvarapps :: [Move' (RefInfo o) (Exp o)]
    subsvarapps = (Nat -> Move' (RefInfo o) (Exp o))
    -> [Nat] -> [Move' (RefInfo o) (Exp o)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move Cost
    costUnification (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
    -> (Nat -> RefCreateEnv (RefInfo o) (Exp o))
    -> Nat
    -> Move' (RefInfo o) (Exp o)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat
    -> Metavar (Exp o) (RefInfo o)
    -> Maybe (Metavar (Exp o) (RefInfo o))
    -> Elr o
    -> RefCreateEnv (RefInfo o) (Exp o)
    app Nat
    n Metavar (Exp o) (RefInfo o)
    meta Maybe (Metavar (Exp o) (RefInfo o))
    forall a. Maybe a
    Nothing (Elr o -> RefCreateEnv (RefInfo o) (Exp o))
    -> (Nat -> Elr o) -> Nat -> RefCreateEnv (RefInfo o) (Exp o)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Elr o
    forall o. Nat -> Elr o
    Var) ([CAction o] -> [Nat]
    forall o. [CAction o] -> [Nat]
    subsvars [CAction o]
    cl)
         mlam :: [Move' (RefInfo o) (Exp o)]
    mlam = case HNExp o -> HNExp' o
    forall a o. WithSeenUIds a o -> a
    rawValue HNExp o
    tt of
          HNPi Hiding
    hid Bool
    _ ICExp o
    _ (Abs MId
    id ICExp o
    _) -> [Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move Cost
    costUnification (Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)
    forall o. Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)
    newLam Hiding
    hid MId
    id)]
          HNExp' o
    _ -> []
         generics :: [Move' (RefInfo o) (Exp o)]
    generics = [Move' (RefInfo o) (Exp o)]
    mlam [Move' (RefInfo o) (Exp o)]
    -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall a. [a] -> [a] -> [a]
    ++ [Move' (RefInfo o) (Exp o)]
    subsvarapps

        in
         [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)])
    -> [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
    forall a b. (a -> b) -> a -> b
    $ case HNExp o -> HNExp' o
    forall a o. WithSeenUIds a o -> a
    rawValue HNExp o
    hne of
          HNApp (Var Nat
    v) ICArgList o
    _ ->
           let (Maybe (Metavar (Exp o) (RefInfo o))
    uid, Bool
    isunique) = [Metavar (Exp o) (RefInfo o)]
    -> [Maybe (Metavar (Exp o) (RefInfo o))]
    -> (Maybe (Metavar (Exp o) (RefInfo o)), Bool)
    forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)
    pickUid [Metavar (Exp o) (RefInfo o)]
    uids ([Maybe (Metavar (Exp o) (RefInfo o))]
     -> (Maybe (Metavar (Exp o) (RefInfo o)), Bool))
    -> [Maybe (Metavar (Exp o) (RefInfo o))]
    -> (Maybe (Metavar (Exp o) (RefInfo o)), Bool)
    forall a b. (a -> b) -> a -> b
    $ HNExp o -> [Maybe (Metavar (Exp o) (RefInfo o))]
    forall a o. WithSeenUIds a o -> [Maybe (UId o)]
    seenUIds HNExp o
    hne
               uni :: [Move' (RefInfo o) (Exp o)]
    uni = case [CAction o] -> Nat -> Maybe Nat
    forall o. [CAction o] -> Nat -> Maybe Nat
    univar [CAction o]
    cl Nat
    v of
                      Just Nat
    v | Nat
    v Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    n -> [Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move (Bool -> Cost
    costUnificationIf Bool
    isunique) (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall a b. (a -> b) -> a -> b
    $ Nat
    -> Metavar (Exp o) (RefInfo o)
    -> Maybe (Metavar (Exp o) (RefInfo o))
    -> Elr o
    -> RefCreateEnv (RefInfo o) (Exp o)
    app Nat
    n Metavar (Exp o) (RefInfo o)
    meta Maybe (Metavar (Exp o) (RefInfo o))
    uid (Nat -> Elr o
    forall o. Nat -> Elr o
    Var Nat
    v)]
                      Maybe Nat
    _ -> []
           in [Move' (RefInfo o) (Exp o)]
    uni [Move' (RefInfo o) (Exp o)]
    -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall a. [a] -> [a] -> [a]
    ++ [Move' (RefInfo o) (Exp o)]
    generics
          HNApp (Const ConstRef o
    c) ICArgList o
    _ ->
           let (Maybe (Metavar (Exp o) (RefInfo o))
    uid, Bool
    isunique) = [Metavar (Exp o) (RefInfo o)]
    -> [Maybe (Metavar (Exp o) (RefInfo o))]
    -> (Maybe (Metavar (Exp o) (RefInfo o)), Bool)
    forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)
    pickUid [Metavar (Exp o) (RefInfo o)]
    uids ([Maybe (Metavar (Exp o) (RefInfo o))]
     -> (Maybe (Metavar (Exp o) (RefInfo o)), Bool))
    -> [Maybe (Metavar (Exp o) (RefInfo o))]
    -> (Maybe (Metavar (Exp o) (RefInfo o)), Bool)
    forall a b. (a -> b) -> a -> b
    $ HNExp o -> [Maybe (Metavar (Exp o) (RefInfo o))]
    forall a o. WithSeenUIds a o -> [Maybe (UId o)]
    seenUIds HNExp o
    hne
           in Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move (Bool -> Cost
    costUnificationIf Bool
    isunique) (Nat
    -> Metavar (Exp o) (RefInfo o)
    -> Maybe (Metavar (Exp o) (RefInfo o))
    -> Elr o
    -> RefCreateEnv (RefInfo o) (Exp o)
    app Nat
    n Metavar (Exp o) (RefInfo o)
    meta Maybe (Metavar (Exp o) (RefInfo o))
    uid (ConstRef o -> Elr o
    forall o. ConstRef o -> Elr o
    Const ConstRef o
    c)) Move' (RefInfo o) (Exp o)
    -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall a. a -> [a] -> [a]
    : [Move' (RefInfo o) (Exp o)]
    generics
          HNLam{} -> [Move' (RefInfo o) (Exp o)]
    generics
          HNPi Hiding
    hid Bool
    possdep ICExp o
    _ Abs (ICExp o)
    _ ->
           let (Maybe (Metavar (Exp o) (RefInfo o))
    uid, Bool
    isunique) = [Metavar (Exp o) (RefInfo o)]
    -> [Maybe (Metavar (Exp o) (RefInfo o))]
    -> (Maybe (Metavar (Exp o) (RefInfo o)), Bool)
    forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)
    pickUid [Metavar (Exp o) (RefInfo o)]
    uids ([Maybe (Metavar (Exp o) (RefInfo o))]
     -> (Maybe (Metavar (Exp o) (RefInfo o)), Bool))
    -> [Maybe (Metavar (Exp o) (RefInfo o))]
    -> (Maybe (Metavar (Exp o) (RefInfo o)), Bool)
    forall a b. (a -> b) -> a -> b
    $ HNExp o -> [Maybe (Metavar (Exp o) (RefInfo o))]
    forall a o. WithSeenUIds a o -> [Maybe (UId o)]
    seenUIds HNExp o
    hne
           in Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move (Bool -> Cost
    costUnificationIf Bool
    isunique) (Metavar (Exp o) (RefInfo o)
    -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)
    forall o.
    UId o -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)
    newPi (Metavar (Exp o) (RefInfo o)
    -> Maybe (Metavar (Exp o) (RefInfo o))
    -> Metavar (Exp o) (RefInfo o)
    forall a. a -> Maybe a -> a
    fromMaybe Metavar (Exp o) (RefInfo o)
    meta Maybe (Metavar (Exp o) (RefInfo o))
    uid) Bool
    possdep Hiding
    hid) Move' (RefInfo o) (Exp o)
    -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall a. a -> [a] -> [a]
    : [Move' (RefInfo o) (Exp o)]
    generics
          HNSort (Set Nat
    l) -> (Nat -> Move' (RefInfo o) (Exp o))
    -> [Nat] -> [Move' (RefInfo o) (Exp o)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move Cost
    costUnification (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
    -> (Nat -> RefCreateEnv (RefInfo o) (Exp o))
    -> Nat
    -> Move' (RefInfo o) (Exp o)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> RefCreateEnv (RefInfo o) (Exp o)
    forall {m :: * -> *} {o}. Monad m => Nat -> m (Exp o)
    set) [Nat
    0..Nat
    l] [Move' (RefInfo o) (Exp o)]
    -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
    forall a. [a] -> [a] -> [a]
    ++ [Move' (RefInfo o) (Exp o)]
    generics
          HNSort Sort
    _ -> [Move' (RefInfo o) (Exp o)]
    generics
       [RefInfo o]
    _ -> IO [Move' (RefInfo o) (Exp o)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      where

        app :: Nat -> UId o -> Maybe (UId o) -> Elr o ->
               RefCreateEnv (RefInfo o) (Exp o)
        app :: Nat
    -> Metavar (Exp o) (RefInfo o)
    -> Maybe (Metavar (Exp o) (RefInfo o))
    -> Elr o
    -> RefCreateEnv (RefInfo o) (Exp o)
    app Nat
    n Metavar (Exp o) (RefInfo o)
    meta Maybe (Metavar (Exp o) (RefInfo o))
    muid Elr o
    elr = do
          MM (ArgList o) (RefInfo o)
    p <- RefCreateEnv (RefInfo o) (MM (ArgList o) (RefInfo o))
    forall blk a. RefCreateEnv blk (MM a blk)
    newPlaceholder
          MM (ArgList o) (RefInfo o)
    p <- case Elr o
    elr of
            Var{}   -> MM (ArgList o) (RefInfo o)
    -> RefCreateEnv (RefInfo o) (MM (ArgList o) (RefInfo o))
    forall (m :: * -> *) a. Monad m => a -> m a
    return MM (ArgList o) (RefInfo o)
    p
            Const ConstRef o
    c -> do
              ConstDef o
    cd <- StateT (IORef [SubConstraints (RefInfo o)], Nat) IO (ConstDef o)
    -> RefCreateEnv (RefInfo o) (ConstDef o)
    forall blk a.
    StateT (IORef [SubConstraints blk], Nat) IO a -> RefCreateEnv blk a
    RefCreateEnv (StateT (IORef [SubConstraints (RefInfo o)], Nat) IO (ConstDef o)
     -> RefCreateEnv (RefInfo o) (ConstDef o))
    -> StateT (IORef [SubConstraints (RefInfo o)], Nat) IO (ConstDef o)
    -> RefCreateEnv (RefInfo o) (ConstDef o)
    forall a b. (a -> b) -> a -> b
    $ IO (ConstDef o)
    -> StateT (IORef [SubConstraints (RefInfo o)], Nat) IO (ConstDef o)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO (ConstDef o)
     -> StateT
          (IORef [SubConstraints (RefInfo o)], Nat) IO (ConstDef o))
    -> IO (ConstDef o)
    -> StateT (IORef [SubConstraints (RefInfo o)], Nat) IO (ConstDef o)
    forall a b. (a -> b) -> a -> b
    $ ConstRef o -> IO (ConstDef o)
    forall a. IORef a -> IO a
    readIORef ConstRef o
    c
              let dfvapp :: Nat -> Nat -> MM (ArgList o) (RefInfo o)
    dfvapp Nat
    0 Nat
    _ = MM (ArgList o) (RefInfo o)
    p
                  dfvapp Nat
    i Nat
    n = ArgList o -> MM (ArgList o) (RefInfo o)
    forall a blk. a -> MM a blk
    NotM (ArgList o -> MM (ArgList o) (RefInfo o))
    -> ArgList o -> MM (ArgList o) (RefInfo o)
    forall a b. (a -> b) -> a -> b
    $ Hiding -> MExp o -> MM (ArgList o) (RefInfo o) -> ArgList o
    forall o. Hiding -> MExp o -> MArgList o -> ArgList o
    ALCons Hiding
    NotHidden
                              (Exp o -> MExp o
    forall a blk. a -> MM a blk
    NotM (Exp o -> MExp o) -> Exp o -> MExp o
    forall a b. (a -> b) -> a -> b
    $ Maybe (Metavar (Exp o) (RefInfo o))
    -> OKHandle (RefInfo o)
    -> Elr o
    -> MM (ArgList o) (RefInfo o)
    -> Exp o
    forall o.
    Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    App Maybe (Metavar (Exp o) (RefInfo o))
    forall a. Maybe a
    Nothing (OKVal -> OKHandle (RefInfo o)
    forall a blk. a -> MM a blk
    NotM (OKVal -> OKHandle (RefInfo o)) -> OKVal -> OKHandle (RefInfo o)
    forall a b. (a -> b) -> a -> b
    $ OKVal
    OKVal) (Nat -> Elr o
    forall o. Nat -> Elr o
    Var Nat
    n) (ArgList o -> MM (ArgList o) (RefInfo o)
    forall a blk. a -> MM a blk
    NotM ArgList o
    forall o. ArgList o
    ALNil))
                              (Nat -> Nat -> MM (ArgList o) (RefInfo o)
    dfvapp (Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1))
             -- NotHidden is ok because agda reification throws these arguments
             -- away and agsy skips typechecking them
              MM (ArgList o) (RefInfo o)
    -> RefCreateEnv (RefInfo o) (MM (ArgList o) (RefInfo o))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MM (ArgList o) (RefInfo o)
     -> RefCreateEnv (RefInfo o) (MM (ArgList o) (RefInfo o)))
    -> MM (ArgList o) (RefInfo o)
    -> RefCreateEnv (RefInfo o) (MM (ArgList o) (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ Nat -> Nat -> MM (ArgList o) (RefInfo o)
    dfvapp (ConstDef o -> Nat
    forall o. ConstDef o -> Nat
    cddeffreevars ConstDef o
    cd) (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1)
          OKHandle (RefInfo o)
    okh <- RefCreateEnv (RefInfo o) (OKHandle (RefInfo o))
    forall blk. RefCreateEnv blk (OKHandle blk)
    newOKHandle
          Exp o -> RefCreateEnv (RefInfo o) (Exp o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp o -> RefCreateEnv (RefInfo o) (Exp o))
    -> Exp o -> RefCreateEnv (RefInfo o) (Exp o)
    forall a b. (a -> b) -> a -> b
    $ Maybe (Metavar (Exp o) (RefInfo o))
    -> OKHandle (RefInfo o)
    -> Elr o
    -> MM (ArgList o) (RefInfo o)
    -> Exp o
    forall o.
    Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    App (Metavar (Exp o) (RefInfo o) -> Maybe (Metavar (Exp o) (RefInfo o))
    forall a. a -> Maybe a
    Just (Metavar (Exp o) (RefInfo o)
     -> Maybe (Metavar (Exp o) (RefInfo o)))
    -> Metavar (Exp o) (RefInfo o)
    -> Maybe (Metavar (Exp o) (RefInfo o))
    forall a b. (a -> b) -> a -> b
    $ Metavar (Exp o) (RefInfo o)
    -> Maybe (Metavar (Exp o) (RefInfo o))
    -> Metavar (Exp o) (RefInfo o)
    forall a. a -> Maybe a -> a
    fromMaybe Metavar (Exp o) (RefInfo o)
    meta Maybe (Metavar (Exp o) (RefInfo o))
    muid) OKHandle (RefInfo o)
    okh Elr o
    elr MM (ArgList o) (RefInfo o)
    p

    extraref :: UId o -> [Maybe (UId o)] -> ConstRef o -> Move o
    extraref :: forall o. UId o -> [Maybe (UId o)] -> ConstRef o -> Move o
    extraref UId o
    meta [Maybe (UId o)]
    seenuids ConstRef o
    c = Cost
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move Cost
    costAppExtraRef (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
    -> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
    forall a b. (a -> b) -> a -> b
    $ Maybe (UId o) -> Elr o -> RefCreateEnv (RefInfo o) (Exp o)
    app ([Maybe (UId o)] -> Maybe (UId o)
    forall a. [a] -> a
    head [Maybe (UId o)]
    seenuids) (ConstRef o -> Elr o
    forall o. ConstRef o -> Elr o
    Const ConstRef o
    c)
     where
       app :: Maybe (UId o) -> Elr o -> RefCreateEnv (RefInfo o) (Exp o)
    app Maybe (UId o)
    muid Elr o
    elr = Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    forall o.
    Maybe (UId o)
    -> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
    App (UId o -> Maybe (UId o)
    forall a. a -> Maybe a
    Just (UId o -> Maybe (UId o)) -> UId o -> Maybe (UId o)
    forall a b. (a -> b) -> a -> b
    $ UId o -> Maybe (UId o) -> UId o
    forall a. a -> Maybe a -> a
    fromMaybe UId o
    meta Maybe (UId o)
    muid)
                  (OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o)
    -> RefCreateEnv (RefInfo o) (OKHandle (RefInfo o))
    -> RefCreateEnv (RefInfo o) (Elr o -> MArgList o -> Exp o)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RefCreateEnv (RefInfo o) (OKHandle (RefInfo o))
    forall blk. RefCreateEnv blk (OKHandle blk)
    newOKHandle RefCreateEnv (RefInfo o) (Elr o -> MArgList o -> Exp o)
    -> RefCreateEnv (RefInfo o) (Elr o)
    -> RefCreateEnv (RefInfo o) (MArgList o -> Exp o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Elr o -> RefCreateEnv (RefInfo o) (Elr o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Elr o
    elr RefCreateEnv (RefInfo o) (MArgList o -> Exp o)
    -> RefCreateEnv (RefInfo o) (MArgList o)
    -> RefCreateEnv (RefInfo o) (Exp o)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> RefCreateEnv (RefInfo o) (MArgList o)
    forall blk a. RefCreateEnv blk (MM a blk)
    newPlaceholder

    instance Refinable (ICExp o) (RefInfo o) where
     refinements :: RefInfo o
    -> [RefInfo o]
    -> Metavar (ICExp o) (RefInfo o)
    -> IO [Move' (RefInfo o) (ICExp o)]
    refinements RefInfo o
    _ [RefInfo o]
    infos Metavar (ICExp o) (RefInfo o)
    _ =
      let (RICopyInfo ICExp o
    e : [RefInfo o]
    _) = [RefInfo o]
    infos
      in [Move' (RefInfo o) (ICExp o)] -> IO [Move' (RefInfo o) (ICExp o)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Cost
    -> RefCreateEnv (RefInfo o) (ICExp o)
    -> Move' (RefInfo o) (ICExp o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move Cost
    0 (ICExp o -> RefCreateEnv (RefInfo o) (ICExp o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ICExp o
    e)]

    instance Refinable (ConstRef o) (RefInfo o) where
     refinements :: RefInfo o
    -> [RefInfo o]
    -> Metavar (ConstRef o) (RefInfo o)
    -> IO [Move' (RefInfo o) (ConstRef o)]
    refinements RefInfo o
    _ [RICheckProjIndex [ConstRef o]
    projs] Metavar (ConstRef o) (RefInfo o)
    _ = [Move' (RefInfo o) (ConstRef o)]
    -> IO [Move' (RefInfo o) (ConstRef o)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Move' (RefInfo o) (ConstRef o)]
     -> IO [Move' (RefInfo o) (ConstRef o)])
    -> [Move' (RefInfo o) (ConstRef o)]
    -> IO [Move' (RefInfo o) (ConstRef o)]
    forall a b. (a -> b) -> a -> b
    $ (ConstRef o -> Move' (RefInfo o) (ConstRef o))
    -> [ConstRef o] -> [Move' (RefInfo o) (ConstRef o)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Cost
    -> RefCreateEnv (RefInfo o) (ConstRef o)
    -> Move' (RefInfo o) (ConstRef o)
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move Cost
    0 (RefCreateEnv (RefInfo o) (ConstRef o)
     -> Move' (RefInfo o) (ConstRef o))
    -> (ConstRef o -> RefCreateEnv (RefInfo o) (ConstRef o))
    -> ConstRef o
    -> Move' (RefInfo o) (ConstRef o)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ConstRef o -> RefCreateEnv (RefInfo o) (ConstRef o)
    forall (m :: * -> *) a. Monad m => a -> m a
    return) [ConstRef o]
    projs
     refinements RefInfo o
    _ [RefInfo o]
    _ Metavar (ConstRef o) (RefInfo o)
    _ = IO [Move' (RefInfo o) (ConstRef o)]
    forall a. HasCallStack => a
    __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 :: Bool -> Cost
    costUnificationIf Bool
    b = if Bool
    b then Cost
    costUnification else Cost
    costUnificationOccurs

    costIncrease :: Cost
    costIncrease = Cost
    1000
    costUnificationOccurs :: Cost
    costUnificationOccurs = Cost
    100 -- 1000001 -- 1 -- 100
    costUnification :: Cost
    costUnification = Cost
    0000
    costAppVar :: Cost
    costAppVar = Cost
    0000 -- 0, 1
    costAppVarUsed :: Cost
    costAppVarUsed = Cost
    1000 -- 5
    costAppHint :: Cost
    costAppHint = Cost
    3000 -- 2, 5
    costAppHintUsed :: Cost
    costAppHintUsed = Cost
    5000
    costAppRecCall :: Cost
    costAppRecCall = Cost
    0 -- 1000?
    costAppRecCallUsed :: Cost
    costAppRecCallUsed = Cost
    10000 -- 1000?
    costAppConstructor :: Cost
    costAppConstructor = Cost
    1000
    costAppConstructorSingle :: Cost
    costAppConstructorSingle = Cost
    0000
    costAppExtraRef :: Cost
    costAppExtraRef = Cost
    1000
    costLam :: Cost
    costLam = Cost
    0000 -- 1, 0
    costLamUnfold :: Cost
    costLamUnfold = Cost
    1000 -- 1, 0
    costPi :: Cost
    costPi = Cost
    1000003 -- 100 -- 5
    costSort :: Cost
    costSort = Cost
    1000004 -- 0
    costIotaStep :: Cost
    costIotaStep = Cost
    3000 -- 1000005 -- 2 -- 100
    costInferredTypeUnkown :: Cost
    costInferredTypeUnkown = Cost
    1000006 -- 100
    costAbsurdLam :: Cost
    costAbsurdLam = Cost
    0

    costEqStep, costEqEnd, costEqSym, costEqCong :: Cost
    costEqStep :: Cost
    costEqStep = Cost
    2000
    costEqEnd :: Cost
    costEqEnd = Cost
    0
    costEqSym :: Cost
    costEqSym = Cost
    0
    costEqCong :: Cost
    costEqCong = Cost
    500

    prioNo, prioTypeUnknown, prioTypecheckArgList, prioInferredTypeUnknown,
      prioCompBeta, prioCompBetaStructured, prioCompareArgList, prioCompIota,
      prioCompChoice, prioCompUnif, prioCompCopy, prioNoIota, prioAbsurdLambda,
      prioProjIndex
      :: Prio
    prioNo :: Prio
    prioNo = (-Prio
    1)
    prioTypeUnknown :: Prio
    prioTypeUnknown = Prio
    0
    prioTypecheckArgList :: Prio
    prioTypecheckArgList = Prio
    3000
    prioInferredTypeUnknown :: Prio
    prioInferredTypeUnknown = Prio
    4000
    prioCompBeta :: Prio
    prioCompBeta = Prio
    4000
    prioCompBetaStructured :: Prio
    prioCompBetaStructured = Prio
    4000
    prioCompIota :: Prio
    prioCompIota = Prio
    4000
    prioCompChoice :: Prio
    prioCompChoice = Prio
    5000 -- 700 -- 5000
    prioCompUnif :: Prio
    prioCompUnif = Prio
    6000 -- 2
    prioCompCopy :: Prio
    prioCompCopy = Prio
    8000
    prioCompareArgList :: Prio
    prioCompareArgList = Prio
    7000 -- 5 -- 2
    prioNoIota :: Prio
    prioNoIota = Prio
    500 -- 500
    prioAbsurdLambda :: Prio
    prioAbsurdLambda = Prio
    1000

    prioProjIndex :: Prio
    prioProjIndex = Prio
    3000

    prioTypecheck :: Bool -> Prio
    prioTypecheck :: Bool -> Prio
    prioTypecheck Bool
    False = Prio
    1000
    prioTypecheck Bool
    True = Prio
    0

    -- ---------------------------------

    instance Trav a => Trav [a] where
      type Block [a] = Block a
      trav :: forall (m :: * -> *).
    Monad m =>
    (forall b. TravWith b (Block [a]) => MM b (Block b) -> m ())
    -> [a] -> m ()
    trav forall b. TravWith b (Block [a]) => MM b (Block b) -> m ()
    _ []     = () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      trav forall b. TravWith b (Block [a]) => MM b (Block b) -> m ()
    f (a
    x:[a]
    xs) = (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
    -> a -> m ()
    forall a (m :: * -> *).
    (Trav a, Monad m) =>
    (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
    -> a -> m ()
    trav forall b. TravWith b (Block a) => MM b (Block b) -> m ()
    forall b. TravWith b (Block [a]) => MM b (Block b) -> m ()
    f a
    x m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> (forall b. TravWith b (Block [a]) => MM b (Block b) -> m ())
    -> [a] -> m ()
    forall a (m :: * -> *).
    (Trav a, Monad m) =>
    (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
    -> a -> m ()
    trav forall b. TravWith b (Block [a]) => MM b (Block b) -> m ()
    f [a]
    xs

    instance Trav (MId, CExp o) where
      type Block (MId, CExp o) = RefInfo o
      trav :: forall (m :: * -> *).
    Monad m =>
    (forall b.
     TravWith b (Block (MId, CExp o)) =>
     MM b (Block b) -> m ())
    -> (MId, CExp o) -> m ()
    trav forall b.
    TravWith b (Block (MId, CExp o)) =>
    MM b (Block b) -> m ()
    f (MId
    _, CExp o
    ce) = (forall b. TravWith b (Block (CExp o)) => MM b (Block b) -> m ())
    -> CExp o -> m ()
    forall a (m :: * -> *).
    (Trav a, Monad m) =>
    (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
    -> a -> m ()
    trav forall b.
    TravWith b (Block (MId, CExp o)) =>
    MM b (Block b) -> m ()
    forall b. TravWith b (Block (CExp o)) => MM b (Block b) -> m ()
    f CExp o
    ce

    instance Trav (TrBr a o) where
      type Block (TrBr a o) = RefInfo o
      trav :: forall (m :: * -> *).
    Monad m =>
    (forall b. TravWith b (Block (TrBr a o)) => MM b (Block b) -> m ())
    -> TrBr a o -> m ()
    trav forall b. TravWith b (Block (TrBr a o)) => MM b (Block b) -> m ()
    f (TrBr [MExp o]
    es a
    _) = (forall b. TravWith b (Block [MExp o]) => MM b (Block b) -> m ())
    -> [MExp o] -> m ()
    forall a (m :: * -> *).
    (Trav a, Monad m) =>
    (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
    -> a -> m ()
    trav forall b. TravWith b (Block [MExp o]) => MM b (Block b) -> m ()
    forall b. TravWith b (Block (TrBr a o)) => MM b (Block b) -> m ()
    f [MExp o]
    es

    instance Trav (Exp o) where
      type Block (Exp o) = RefInfo o
      trav :: forall (m :: * -> *).
    Monad m =>
    (forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ())
    -> Exp o -> m ()
    trav forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()
    f = \case
        App Maybe (UId o)
    _ OKHandle (RefInfo o)
    _ Elr o
    _ MArgList o
    args         -> (forall b.
     TravWith b (Block (MArgList o)) =>
     MM b (Block b) -> m ())
    -> MArgList o -> m ()
    forall a (m :: * -> *).
    (Trav a, Monad m) =>
    (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
    -> a -> m ()
    trav forall b. TravWith b (Block (MArgList o)) => MM b (Block b) -> m ()
    forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()
    f MArgList o
    args
        Lam Hiding
    _ (Abs MId
    _ MExp o
    b)        -> (forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ())
    -> MExp o -> m ()
    forall a (m :: * -> *).
    (Trav a, Monad m) =>
    (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
    -> a -> m ()
    trav forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ()
    forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()
    f MExp o
    b
        Pi Maybe (UId o)
    _ Hiding
    _ Bool
    _ MExp o
    it (Abs MId
    _ MExp o
    ot) -> (forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ())
    -> MExp o -> m ()
    forall a (m :: * -> *).
    (Trav a, Monad m) =>
    (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
    -> a -> m ()
    trav forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ()
    forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()
    f MExp o
    it m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> (forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ())
    -> MExp o -> m ()
    forall a (m :: * -> *).
    (Trav a, Monad m) =>
    (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
    -> a -> m ()
    trav forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ()
    forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()
    f MExp o
    ot
        Sort Sort
    _                 -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        AbsurdLambda{}         -> () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

    instance Trav (ArgList o) where
      type Block (ArgList o) = RefInfo o
      trav :: forall (m :: * -> *).
    Monad m =>
    (forall b.
     TravWith b (Block (ArgList o)) =>
     MM b (Block b) -> m ())
    -> ArgList o -> m ()
    trav forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
    _ ArgList o
    ALNil               = () -> m ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      trav forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
    f (ALCons Hiding
    _ MExp o
    arg MArgList o
    args) = (forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ())
    -> MExp o -> m ()
    forall a (m :: * -> *).
    (Trav a, Monad m) =>
    (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
    -> a -> m ()
    trav forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ()
    forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
    f MExp o
    arg m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> (forall b.
     TravWith b (Block (MArgList o)) =>
     MM b (Block b) -> m ())
    -> MArgList o -> m ()
    forall a (m :: * -> *).
    (Trav a, Monad m) =>
    (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
    -> a -> m ()
    trav forall b. TravWith b (Block (MArgList o)) => MM b (Block b) -> m ()
    forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
    f MArgList o
    args
      trav forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
    f (ALProj MArgList o
    eas MM (ConstRef o) (RefInfo o)
    _ Hiding
    _ MArgList o
    as) = (forall b.
     TravWith b (Block (MArgList o)) =>
     MM b (Block b) -> m ())
    -> MArgList o -> m ()
    forall a (m :: * -> *).
    (Trav a, Monad m) =>
    (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
    -> a -> m ()
    trav forall b. TravWith b (Block (MArgList o)) => MM b (Block b) -> m ()
    forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
    f MArgList o
    eas m () -> m () -> m ()
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> (forall b.
     TravWith b (Block (MArgList o)) =>
     MM b (Block b) -> m ())
    -> MArgList o -> m ()
    forall a (m :: * -> *).
    (Trav a, Monad m) =>
    (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
    -> a -> m ()
    trav forall b. TravWith b (Block (MArgList o)) => MM b (Block b) -> m ()
    forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
    f MArgList o
    as
      trav forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
    f (ALConPar MArgList o
    args)     = (forall b.
     TravWith b (Block (MArgList o)) =>
     MM b (Block b) -> m ())
    -> MArgList o -> m ()
    forall a (m :: * -> *).
    (Trav a, Monad m) =>
    (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
    -> a -> m ()
    trav forall b. TravWith b (Block (MArgList o)) => MM b (Block b) -> m ()
    forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
    f MArgList o
    args

    -- ---------------------------------