module Agda.Mimer.Mimer
  ( MimerResult(..)
  , mimer
  )
  where

import Control.DeepSeq (force, NFData(..))
import Control.Monad
import Control.Monad.Except (catchError)
import Control.Monad.Error.Class (MonadError)
import Control.Monad.Fail (MonadFail)
import Control.Monad.IO.Class (liftIO)
import Control.Monad.Reader (ReaderT(..), runReaderT, asks, ask, lift)
import Data.Function (on)
import Data.Functor ((<&>))
import Data.List (sortOn, intersect, transpose, (\\))
import qualified Data.List.NonEmpty as NonEmptyList (head)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Maybe (maybeToList, fromMaybe, maybe, isNothing)
import Data.PQueue.Min (MinQueue)
import qualified Data.PQueue.Min as Q
import GHC.Generics (Generic)
import qualified Text.PrettyPrint.Boxes as Box
import qualified Data.Text as Text

import qualified Agda.Benchmarking as Bench
import Agda.Interaction.MakeCase (makeCase, getClauseZipperForIP, recheckAbstractClause)
import Agda.Syntax.Abstract (Expr(AbsurdLam))
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Views as A
import Agda.Syntax.Abstract.Name (QName(..), Name(..))
import Agda.Syntax.Common (InteractionId(..), MetaId(..), ArgInfo(..), defaultArgInfo, Origin(..), ConOrigin(..), Hiding(..), setOrigin, NameId, Nat, namedThing, Arg(..), setHiding, getHiding, ProjOrigin(..), rangedThing, woThing, nameOf, visible)
import Agda.Syntax.Common.Pretty (Pretty)
import qualified Agda.Syntax.Common.Pretty as P
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Info (pattern UnificationMeta, exprNoRange)
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars (AllMetas(..))
import Agda.Syntax.Internal.Pattern (clausePerm)
import Agda.Syntax.Position (Range, rangeFile, rangeFilePath)
import qualified Agda.Syntax.Scope.Base as Scope
import Agda.Syntax.Translation.InternalToAbstract (reify, NamedClause(..))
import Agda.Syntax.Translation.AbstractToConcrete (abstractToConcrete_)
import Agda.TypeChecking.Constraints (noConstraints)
import Agda.TypeChecking.Conversion (equalType)
import qualified Agda.TypeChecking.Empty as Empty -- (isEmptyType)
import Agda.TypeChecking.Free (flexRigOccurrenceIn, freeVars)
import Agda.TypeChecking.Level (levelType)
import Agda.TypeChecking.MetaVars (newValueMeta)
import Agda.TypeChecking.Monad -- (MonadTCM, lookupInteractionId, getConstInfo, liftTCM, clScope, getMetaInfo, lookupMeta, MetaVariable(..), metaType, typeOfConst, getMetaType, MetaInfo(..), getMetaTypeInContext)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records (isRecord, isRecursiveRecord)
import Agda.TypeChecking.Reduce (reduce, instantiateFull, instantiate)
import Agda.TypeChecking.Rules.LHS.Problem (AsBinding(..))
import Agda.TypeChecking.Rules.Term  (lambdaAddContext)
import Agda.TypeChecking.Substitute.Class (apply, applyE, NoSubst(..))
import Agda.TypeChecking.Telescope (piApplyM, flattenTel, teleArgs)
import Agda.Utils.Benchmark (billTo)
import Agda.Utils.FileName (filePath)
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.Utils.Maybe (catMaybes)
import Agda.Utils.Monad (ifM)
import qualified Agda.Utils.Maybe.Strict as SMaybe
-- import Agda.Utils.Permutation (idP, permute, takeP)
import Agda.Utils.Time (CPUTime(..), getCPUTime, fromMilliseconds)
import Agda.Utils.Tuple (mapFst, mapSnd)
import Agda.Utils.FileName (AbsolutePath(..))

import Agda.Mimer.Options

import System.IO.Unsafe (unsafePerformIO)
import Data.IORef (IORef, writeIORef, readIORef, newIORef, modifyIORef')

-- Temporary (used for custom cost verbosity hack)
import qualified Agda.Utils.Maybe.Strict as Strict
import qualified Agda.Utils.Trie as Trie
import Agda.Interaction.Base (Rewrite(..))
import Agda.Interaction.BasicOps (normalForm)
import Agda.Interaction.Options.Base (parseVerboseKey)
import Agda.Utils.List (lastWithDefault)

data MimerResult
  = MimerExpr String -- ^ Returns 'String' rather than 'Expr' because the give action expects a string.
  | MimerClauses QName [A.Clause]
  | MimerList [(Int, String)]
  | MimerNoResult
  deriving ((forall x. MimerResult -> Rep MimerResult x)
-> (forall x. Rep MimerResult x -> MimerResult)
-> Generic MimerResult
forall x. Rep MimerResult x -> MimerResult
forall x. MimerResult -> Rep MimerResult x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MimerResult -> Rep MimerResult x
from :: forall x. MimerResult -> Rep MimerResult x
$cto :: forall x. Rep MimerResult x -> MimerResult
to :: forall x. Rep MimerResult x -> MimerResult
Generic)

instance NFData MimerResult

mimer :: MonadTCM tcm
  => Rewrite
  -> InteractionId
  -> Range
  -> String
  -> tcm MimerResult
mimer :: forall (tcm :: * -> *).
MonadTCM tcm =>
Rewrite -> InteractionId -> Range -> ArgName -> tcm MimerResult
mimer Rewrite
norm InteractionId
ii Range
rng ArgName
argStr = TCM MimerResult -> tcm MimerResult
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM MimerResult -> tcm MimerResult)
-> TCM MimerResult -> tcm MimerResult
forall a b. (a -> b) -> a -> b
$ do
    ArgName -> VerboseLevel -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"mimer.top" VerboseLevel
10 (TCMT IO Doc
"Running Mimer on interaction point" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> InteractionId -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty InteractionId
ii TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"with argument string" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> ArgName
forall a. Show a => a -> ArgName
show ArgName
argStr))

    start <- IO CPUTime -> TCMT IO CPUTime
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO CPUTime -> TCMT IO CPUTime) -> IO CPUTime -> TCMT IO CPUTime
forall a b. (a -> b) -> a -> b
$ IO CPUTime
forall (m :: * -> *). MonadIO m => m CPUTime
getCPUTime

    opts <- parseOptions ii rng argStr
    reportS "mimer.top" 15 ("Mimer options: " ++ show opts)

    oldState <- getTC

    sols <- runSearch norm opts ii rng
    putTC oldState

    sol <- case drop (optSkip opts) $ zip [0..] sols of
          [] -> do
            ArgName -> VerboseLevel -> ArgName -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> ArgName -> m ()
reportSLn ArgName
"mimer.top" VerboseLevel
10 ArgName
"No solution found"
            MimerResult -> TCM MimerResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MimerResult
MimerNoResult
          [(VerboseLevel, MimerResult)]
sols' | Options -> Bool
optList Options
opts -> MimerResult -> TCM MimerResult
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MimerResult -> TCM MimerResult) -> MimerResult -> TCM MimerResult
forall a b. (a -> b) -> a -> b
$ [(VerboseLevel, ArgName)] -> MimerResult
MimerList [ (VerboseLevel
i, ArgName
s) | (VerboseLevel
i, MimerExpr ArgName
s) <- [(VerboseLevel, MimerResult)]
sols' ]
          (VerboseLevel
_, MimerResult
sol) : [(VerboseLevel, MimerResult)]
_ -> do
            ArgName -> VerboseLevel -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"mimer.top" VerboseLevel
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Solution:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MimerResult -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MimerResult -> m Doc
prettyTCM MimerResult
sol
            MimerResult -> TCM MimerResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MimerResult
sol

    putTC oldState

    stop <- liftIO $ getCPUTime
    let time = CPUTime
stop CPUTime -> CPUTime -> CPUTime
forall a. Num a => a -> a -> a
- CPUTime
start
    reportSDoc "mimer.top" 10 ("Total elapsed time:" <+> pretty time)
    verboseS "mimer.stats" 50 $ writeTime ii (if null sols then Nothing else Just time)
    return sol


-- Order to try things in:
-- 1. Local variables (including let-bound)
-- 2. Data constructors
-- 3. Where clauses
-- 4. Lambda abstract
-- Other: Equality, empty type, record projections
-- - If we only use constructors if the target type is a data type, we might
--   generate η-reducible expressions, e.g. λ xs → _∷_ 0 xs


------------------------------------------------------------------------------
-- * Data types
------------------------------------------------------------------------------

type SM a = ReaderT SearchOptions TCM a

data SearchBranch = SearchBranch
  { SearchBranch -> TCState
sbTCState :: TCState
  , SearchBranch -> [Goal]
sbGoals :: [Goal]
  , SearchBranch -> VerboseLevel
sbCost :: Int
  , SearchBranch -> Map CheckpointId ComponentCache
sbCache :: Map CheckpointId ComponentCache
  , SearchBranch -> Map Name VerboseLevel
sbComponentsUsed :: Map Name Int -- ^ Number of times each component has been used
  }
  deriving ((forall x. SearchBranch -> Rep SearchBranch x)
-> (forall x. Rep SearchBranch x -> SearchBranch)
-> Generic SearchBranch
forall x. Rep SearchBranch x -> SearchBranch
forall x. SearchBranch -> Rep SearchBranch x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SearchBranch -> Rep SearchBranch x
from :: forall x. SearchBranch -> Rep SearchBranch x
$cto :: forall x. Rep SearchBranch x -> SearchBranch
to :: forall x. Rep SearchBranch x -> SearchBranch
Generic)
instance NFData SearchBranch

-- | NOTE: Equality is only on the fields `sbCost` and `sbGoals`
instance Eq SearchBranch where
  SearchBranch
sb1 == :: SearchBranch -> SearchBranch -> Bool
== SearchBranch
sb2 = SearchBranch -> VerboseLevel
sbCost SearchBranch
sb1 VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== SearchBranch -> VerboseLevel
sbCost SearchBranch
sb2 Bool -> Bool -> Bool
&& SearchBranch -> [Goal]
sbGoals SearchBranch
sb1 [Goal] -> [Goal] -> Bool
forall a. Eq a => a -> a -> Bool
== SearchBranch -> [Goal]
sbGoals SearchBranch
sb2

-- TODO: Explain
instance Ord SearchBranch where
  compare :: SearchBranch -> SearchBranch -> Ordering
compare = VerboseLevel -> VerboseLevel -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (VerboseLevel -> VerboseLevel -> Ordering)
-> (SearchBranch -> VerboseLevel)
-> SearchBranch
-> SearchBranch
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` SearchBranch -> VerboseLevel
sbCost

-- Map source component to generated components
type ComponentCache = Map Component (Maybe [Component])

data Goal = Goal
  { Goal -> MetaId
goalMeta :: MetaId
  }
  deriving ((forall x. Goal -> Rep Goal x)
-> (forall x. Rep Goal x -> Goal) -> Generic Goal
forall x. Rep Goal x -> Goal
forall x. Goal -> Rep Goal x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Goal -> Rep Goal x
from :: forall x. Goal -> Rep Goal x
$cto :: forall x. Rep Goal x -> Goal
to :: forall x. Rep Goal x -> Goal
Generic)
instance NFData Goal

-- TODO: Is this a reasonable Eq instance?
instance Eq Goal where
  Goal
g1 == :: Goal -> Goal -> Bool
== Goal
g2 = Goal -> MetaId
goalMeta Goal
g1 MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== Goal -> MetaId
goalMeta Goal
g2

-- | Components that are not changed during search. Components that do change
-- (local variables and let bindings) are stored in each 'SearchBranch'.
data BaseComponents = BaseComponents
  { BaseComponents -> [Component]
hintFns :: [Component]
  , BaseComponents -> [Component]
hintDataTypes :: [Component]
  , BaseComponents -> [Component]
hintRecordTypes :: [Component]
  , BaseComponents -> [Component]
hintAxioms :: [Component]
  -- ^ Excluding those producing Level
  , BaseComponents -> [Component]
hintLevel :: [Component]
  -- ^ A definition in a where clause
  , BaseComponents -> [Component]
hintProjections :: [Component]
  -- ^ Variables that are candidates for arguments to recursive calls
  , BaseComponents -> Maybe Component
hintThisFn :: Maybe Component
  , BaseComponents -> [Open Component]
hintLetVars :: [Open Component]
  , BaseComponents -> Open [(Term, NoSubst Term VerboseLevel)]
hintRecVars :: Open [(Term, NoSubst Term Int)] -- ^ Variable terms and which argument they come from
  , BaseComponents -> Open [Term]
hintSplitVars :: Open [Term]
  }
  deriving ((forall x. BaseComponents -> Rep BaseComponents x)
-> (forall x. Rep BaseComponents x -> BaseComponents)
-> Generic BaseComponents
forall x. Rep BaseComponents x -> BaseComponents
forall x. BaseComponents -> Rep BaseComponents x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BaseComponents -> Rep BaseComponents x
from :: forall x. BaseComponents -> Rep BaseComponents x
$cto :: forall x. Rep BaseComponents x -> BaseComponents
to :: forall x. Rep BaseComponents x -> BaseComponents
Generic)

instance NFData BaseComponents

type CompId = Int
data Component = Component
  { Component -> VerboseLevel
compId    :: CompId -- ^ Unique id for the component. Used for the cache.
  , Component -> Maybe Name
compName  :: Maybe Name -- ^ Used for keeping track of how many times a component has been used
  , Component -> VerboseLevel
compPars  :: Nat -- ^ How many arguments should be dropped (e.g. constructor parameters)
  , Component -> Term
compTerm  :: Term
  , Component -> Type
compType  :: Type
  , Component -> Bool
compRec   :: Bool -- ^ Is this a recursive call
  , Component -> [MetaId]
compMetas :: [MetaId]
  , Component -> VerboseLevel
compCost  :: Cost
  }
  deriving (Component -> Component -> Bool
(Component -> Component -> Bool)
-> (Component -> Component -> Bool) -> Eq Component
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Component -> Component -> Bool
== :: Component -> Component -> Bool
$c/= :: Component -> Component -> Bool
/= :: Component -> Component -> Bool
Eq, (forall x. Component -> Rep Component x)
-> (forall x. Rep Component x -> Component) -> Generic Component
forall x. Rep Component x -> Component
forall x. Component -> Rep Component x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Component -> Rep Component x
from :: forall x. Component -> Rep Component x
$cto :: forall x. Rep Component x -> Component
to :: forall x. Rep Component x -> Component
Generic)

instance NFData Component

-- TODO: Is this reasonable?
instance Ord Component where
  compare :: Component -> Component -> Ordering
compare = VerboseLevel -> VerboseLevel -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (VerboseLevel -> VerboseLevel -> Ordering)
-> (Component -> VerboseLevel)
-> Component
-> Component
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Component -> VerboseLevel
compId

data SearchStepResult
  = ResultExpr Expr
  | ResultClauses [A.Clause]
  | OpenBranch SearchBranch
  | NoSolution
  deriving ((forall x. SearchStepResult -> Rep SearchStepResult x)
-> (forall x. Rep SearchStepResult x -> SearchStepResult)
-> Generic SearchStepResult
forall x. Rep SearchStepResult x -> SearchStepResult
forall x. SearchStepResult -> Rep SearchStepResult x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SearchStepResult -> Rep SearchStepResult x
from :: forall x. SearchStepResult -> Rep SearchStepResult x
$cto :: forall x. Rep SearchStepResult x -> SearchStepResult
to :: forall x. Rep SearchStepResult x -> SearchStepResult
Generic)
instance NFData SearchStepResult


data SearchOptions = SearchOptions
  { SearchOptions -> BaseComponents
searchBaseComponents :: BaseComponents
  , SearchOptions -> HintMode
searchHintMode :: HintMode
  , SearchOptions -> Integer
searchTimeout :: MilliSeconds
  , SearchOptions -> Bool
searchGenProjectionsLocal :: Bool
  , SearchOptions -> Bool
searchGenProjectionsLet :: Bool
  , SearchOptions -> Bool
searchGenProjectionsExternal :: Bool
  , SearchOptions -> Bool
searchGenProjectionsRec :: Bool
  , SearchOptions -> Bool
searchSpeculateProjections :: Bool
  , SearchOptions -> MetaId
searchTopMeta :: MetaId
  , SearchOptions -> TCEnv
searchTopEnv :: TCEnv
  , SearchOptions -> CheckpointId
searchTopCheckpoint :: CheckpointId
  , SearchOptions -> InteractionId
searchInteractionId :: InteractionId
  , SearchOptions -> Maybe QName
searchFnName :: Maybe QName
  , SearchOptions -> Costs
searchCosts :: Costs
  , SearchOptions -> IORef MimerStats
searchStats :: IORef MimerStats
  , SearchOptions -> Rewrite
searchRewrite :: Rewrite
  }

type Cost = Int
data Costs = Costs
  { Costs -> VerboseLevel
costLocal :: Cost
  , Costs -> VerboseLevel
costFn :: Cost
  , Costs -> VerboseLevel
costDataCon :: Cost
  , Costs -> VerboseLevel
costRecordCon :: Cost
  , Costs -> VerboseLevel
costSpeculateProj :: Cost
  , Costs -> VerboseLevel
costProj :: Cost
  , Costs -> VerboseLevel
costAxiom :: Cost
  , Costs -> VerboseLevel
costLet :: Cost
  , Costs -> VerboseLevel
costLevel :: Cost
  , Costs -> VerboseLevel
costSet :: Cost -- Should probably be replaced with multiple different costs
  , Costs -> VerboseLevel
costRecCall :: Cost
  , Costs -> VerboseLevel
costNewMeta :: Cost -- ^ Cost of a new meta-variable appearing in a non-implicit position
  , Costs -> VerboseLevel
costNewHiddenMeta :: Cost -- ^ Cost of a new meta-variable appearing in an implicit position
  , Costs -> VerboseLevel -> VerboseLevel
costCompReuse :: Nat -> Cost -- ^ Cost of reusing a component @n@ times. Only counted when @n>1@.
  }

noCost :: Cost
noCost :: VerboseLevel
noCost = VerboseLevel
0

defaultCosts :: Costs
defaultCosts :: Costs
defaultCosts = Costs
  { costLocal :: VerboseLevel
costLocal = VerboseLevel
3
  , costFn :: VerboseLevel
costFn = VerboseLevel
10
  , costDataCon :: VerboseLevel
costDataCon = VerboseLevel
3
  , costRecordCon :: VerboseLevel
costRecordCon = VerboseLevel
3
  , costSpeculateProj :: VerboseLevel
costSpeculateProj = VerboseLevel
20
  , costProj :: VerboseLevel
costProj = VerboseLevel
3
  , costAxiom :: VerboseLevel
costAxiom = VerboseLevel
10
  , costLet :: VerboseLevel
costLet = VerboseLevel
5
  , costLevel :: VerboseLevel
costLevel = VerboseLevel
3
  , costSet :: VerboseLevel
costSet = VerboseLevel
10
  , costRecCall :: VerboseLevel
costRecCall = VerboseLevel
8
  , costNewMeta :: VerboseLevel
costNewMeta = VerboseLevel
10
  , costNewHiddenMeta :: VerboseLevel
costNewHiddenMeta = VerboseLevel
1
  , costCompReuse :: VerboseLevel -> VerboseLevel
costCompReuse = \VerboseLevel
uses -> VerboseLevel
10 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
* (VerboseLevel
uses VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1) VerboseLevel -> Integer -> VerboseLevel
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
2
  }

------------------------------------------------------------------------------
-- * Helper functions
------------------------------------------------------------------------------

predNat :: Nat -> Nat
predNat :: VerboseLevel -> VerboseLevel
predNat VerboseLevel
n | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0 = VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1
          | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
0 = VerboseLevel
0
          | Bool
otherwise = ArgName -> VerboseLevel
forall a. HasCallStack => ArgName -> a
error ArgName
"predNat of negative value"

getRecordFields :: (HasConstInfo tcm, MonadTCM tcm) => QName -> tcm [QName]
getRecordFields :: forall (tcm :: * -> *).
(HasConstInfo tcm, MonadTCM tcm) =>
QName -> tcm [QName]
getRecordFields = (Definition -> [QName]) -> tcm Definition -> tcm [QName]
forall a b. (a -> b) -> tcm a -> tcm b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Dom' Term QName -> QName) -> [Dom' Term QName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term QName -> QName
forall t e. Dom' t e -> e
unDom ([Dom' Term QName] -> [QName])
-> (Definition -> [Dom' Term QName]) -> Definition -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> [Dom' Term QName]
recFields (Defn -> [Dom' Term QName])
-> (Definition -> Defn) -> Definition -> [Dom' Term QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef) (tcm Definition -> tcm [QName])
-> (QName -> tcm Definition) -> QName -> tcm [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> tcm Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo


-- TODO: Change the signature in original module instead.
isEmptyType :: Type -> SM Bool
isEmptyType :: Type -> SM Bool
isEmptyType = TCM Bool -> SM Bool
forall a. TCM a -> ReaderT SearchOptions (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> SM Bool) -> (Type -> TCM Bool) -> Type -> SM Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TCM Bool
Empty.isEmptyType

-- TODO: Currently not using this function. Is it useful anywhere?
getDomainType :: Type -> Type
getDomainType :: Type -> Type
getDomainType Type
typ = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
typ of
  Pi Dom Type
dom Abs Type
_ -> Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom
  Term
_ -> Type
forall a. HasCallStack => a
__IMPOSSIBLE__

allOpenMetas :: (AllMetas t, ReadTCState tcm) => t -> tcm [MetaId]
allOpenMetas :: forall t (tcm :: * -> *).
(AllMetas t, ReadTCState tcm) =>
t -> tcm [MetaId]
allOpenMetas t
t = do
  openMetas <- tcm [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas
  return $ allMetas (:[]) t `intersect` openMetas

getOpenComponent :: MonadTCM tcm => Open Component -> tcm Component
getOpenComponent :: forall (tcm :: * -> *).
MonadTCM tcm =>
Open Component -> tcm Component
getOpenComponent Open Component
openComp = do
  let comp :: Component
comp = Open Component -> Component
forall a. Open a -> a
openThing Open Component
openComp
  term <- Open Term -> tcm Term
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen (Open Term -> tcm Term) -> Open Term -> tcm Term
forall a b. (a -> b) -> a -> b
$ Component -> Term
compTerm (Component -> Term) -> Open Component -> Open Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Open Component
openComp
  typ <- getOpen $ compType <$> openComp
  when (not $ null $ compMetas comp) __IMPOSSIBLE__
  return Component
    { compId    = compId comp
    , compName  = compName comp
    , compPars  = compPars comp
    , compTerm  = term
    , compType  = typ
    , compRec   = compRec comp
    , compMetas = compMetas comp
    , compCost  = compCost comp
    }

mkComponent :: CompId -> [MetaId] -> Cost -> Maybe Name -> Nat -> Term -> Type -> Component
mkComponent :: VerboseLevel
-> [MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> Component
mkComponent VerboseLevel
cId [MetaId]
metaIds VerboseLevel
cost Maybe Name
mName VerboseLevel
pars Term
term Type
typ = Component
  { compId :: VerboseLevel
compId    = VerboseLevel
cId
  , compName :: Maybe Name
compName  = Maybe Name
mName
  , compPars :: VerboseLevel
compPars  = VerboseLevel
pars
  , compTerm :: Term
compTerm  = Term
term
  , compType :: Type
compType  = Type
typ
  , compRec :: Bool
compRec   = Bool
False
  , compMetas :: [MetaId]
compMetas = [MetaId]
metaIds
  , compCost :: VerboseLevel
compCost  = VerboseLevel
cost }

mkComponentQ :: CompId -> Cost -> QName -> Nat -> Term -> Type -> Component
mkComponentQ :: VerboseLevel
-> VerboseLevel
-> QName
-> VerboseLevel
-> Term
-> Type
-> Component
mkComponentQ VerboseLevel
cId VerboseLevel
cost QName
qname = VerboseLevel
-> [MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> Component
mkComponent VerboseLevel
cId [] VerboseLevel
cost (Name -> Maybe Name
forall a. a -> Maybe a
Just (Name -> Maybe Name) -> Name -> Maybe Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
qname)

noName :: Maybe Name
noName :: Maybe Name
noName = Maybe Name
forall a. Maybe a
Nothing

newComponent :: MonadFresh CompId m => [MetaId] -> Cost -> Maybe Name -> Nat -> Term -> Type -> m Component
newComponent :: forall (m :: * -> *).
MonadFresh VerboseLevel m =>
[MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> m Component
newComponent [MetaId]
metaIds VerboseLevel
cost Maybe Name
mName VerboseLevel
pars Term
term Type
typ = m VerboseLevel
forall i (m :: * -> *). MonadFresh i m => m i
fresh m VerboseLevel -> (VerboseLevel -> Component) -> m Component
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \VerboseLevel
cId -> VerboseLevel
-> [MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> Component
mkComponent VerboseLevel
cId [MetaId]
metaIds VerboseLevel
cost Maybe Name
mName VerboseLevel
pars Term
term Type
typ

newComponentQ :: MonadFresh CompId m => [MetaId] -> Cost -> QName -> Nat -> Term -> Type -> m Component
newComponentQ :: forall (m :: * -> *).
MonadFresh VerboseLevel m =>
[MetaId]
-> VerboseLevel
-> QName
-> VerboseLevel
-> Term
-> Type
-> m Component
newComponentQ [MetaId]
metaIds VerboseLevel
cost QName
qname VerboseLevel
pars Term
term Type
typ = m VerboseLevel
forall i (m :: * -> *). MonadFresh i m => m i
fresh m VerboseLevel -> (VerboseLevel -> Component) -> m Component
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \VerboseLevel
cId -> VerboseLevel
-> [MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> Component
mkComponent VerboseLevel
cId [MetaId]
metaIds VerboseLevel
cost (Name -> Maybe Name
forall a. a -> Maybe a
Just (Name -> Maybe Name) -> Name -> Maybe Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
qname) VerboseLevel
pars Term
term Type
typ

addCost :: Cost -> Component -> Component
addCost :: VerboseLevel -> Component -> Component
addCost VerboseLevel
cost Component
comp = Component
comp { compCost = cost + compCost comp }

addBranchGoals :: [Goal] -> SearchBranch -> SearchBranch
addBranchGoals :: [Goal] -> SearchBranch -> SearchBranch
addBranchGoals [Goal]
goals SearchBranch
branch = SearchBranch
branch {sbGoals = goals ++ sbGoals branch}

withBranchState :: SearchBranch -> SM a -> SM a
withBranchState :: forall a. SearchBranch -> SM a -> SM a
withBranchState SearchBranch
br SM a
ma = do
  TCState -> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC (SearchBranch -> TCState
sbTCState SearchBranch
br)
  SM a
ma

withBranchAndGoal :: SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal :: forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
br Goal
goal SM a
ma = Goal -> SM a -> SM a
forall a. Goal -> SM a -> SM a
inGoalEnv Goal
goal (SM a -> SM a) -> SM a -> SM a
forall a b. (a -> b) -> a -> b
$ SearchBranch -> SM a -> SM a
forall a. SearchBranch -> SM a -> SM a
withBranchState SearchBranch
br SM a
ma

inGoalEnv :: Goal -> SM a -> SM a
inGoalEnv :: forall a. Goal -> SM a -> SM a
inGoalEnv Goal
goal = MetaId
-> ReaderT SearchOptions (TCMT IO) a
-> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
 ReadTCState m) =>
MetaId -> m a -> m a
withMetaId (Goal -> MetaId
goalMeta Goal
goal)

nextBranchMeta' :: SearchBranch -> SM (Goal, SearchBranch)
nextBranchMeta' :: SearchBranch -> SM (Goal, SearchBranch)
nextBranchMeta' = (Maybe (Goal, SearchBranch) -> (Goal, SearchBranch))
-> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch))
-> SM (Goal, SearchBranch)
forall a b.
(a -> b)
-> ReaderT SearchOptions (TCMT IO) a
-> ReaderT SearchOptions (TCMT IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Goal, SearchBranch)
-> Maybe (Goal, SearchBranch) -> (Goal, SearchBranch)
forall a. a -> Maybe a -> a
fromMaybe (Goal, SearchBranch)
forall a. HasCallStack => a
__IMPOSSIBLE__) (ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch))
 -> SM (Goal, SearchBranch))
-> (SearchBranch
    -> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch)))
-> SearchBranch
-> SM (Goal, SearchBranch)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchBranch
-> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch))
nextBranchMeta

nextBranchMeta :: SearchBranch -> SM (Maybe (Goal, SearchBranch))
nextBranchMeta :: SearchBranch
-> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch))
nextBranchMeta SearchBranch
branch = case SearchBranch -> [Goal]
sbGoals SearchBranch
branch of
  [] -> Maybe (Goal, SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch))
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Goal, SearchBranch)
forall a. Maybe a
Nothing
  (Goal
goal : [Goal]
goals) ->
    Maybe (Goal, SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch))
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Goal, SearchBranch)
 -> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch)))
-> Maybe (Goal, SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch))
forall a b. (a -> b) -> a -> b
$ (Goal, SearchBranch) -> Maybe (Goal, SearchBranch)
forall a. a -> Maybe a
Just (Goal
goal, SearchBranch
branch{sbGoals=goals})

-- TODO: Rename (see metaInstantiation)
getMetaInstantiation :: (MonadTCM tcm, PureTCM tcm, MonadDebug tcm, MonadInteractionPoints tcm, MonadFresh NameId tcm)
  => MetaId -> tcm (Maybe Expr)
getMetaInstantiation :: forall (tcm :: * -> *).
(MonadTCM tcm, PureTCM tcm, MonadDebug tcm,
 MonadInteractionPoints tcm, MonadFresh NameId tcm) =>
MetaId -> tcm (Maybe Expr)
getMetaInstantiation = MetaId -> tcm (Maybe Term)
forall (tcm :: * -> *).
(MonadTCM tcm, MonadDebug tcm, ReadTCState tcm) =>
MetaId -> tcm (Maybe Term)
metaInstantiation (MetaId -> tcm (Maybe Term))
-> (Maybe Term -> tcm (Maybe Expr)) -> MetaId -> tcm (Maybe Expr)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Maybe Term -> tcm (Maybe Expr)
Maybe Term -> tcm (Maybe (ReifiesTo Term))
forall {m :: * -> *} {a}.
(InstantiateFull a, Reify a, PureTCM m, MonadInteractionPoints m,
 MonadFresh NameId m) =>
Maybe a -> m (Maybe (ReifiesTo a))
go
  where
    -- TODO: Cleaner way of juggling the maybes here?
    go :: Maybe a -> m (Maybe (ReifiesTo a))
go Maybe a
Nothing = Maybe (ReifiesTo a) -> m (Maybe (ReifiesTo a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (ReifiesTo a)
forall a. Maybe a
Nothing
    go (Just a
term) = do
      expr <- a -> m a
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull a
term m a -> (a -> m (ReifiesTo a)) -> m (ReifiesTo a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> m (ReifiesTo a)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => a -> m (ReifiesTo a)
reify
      return $ Just expr

metaInstantiation :: (MonadTCM tcm, MonadDebug tcm, ReadTCState tcm) => MetaId -> tcm (Maybe Term)
metaInstantiation :: forall (tcm :: * -> *).
(MonadTCM tcm, MonadDebug tcm, ReadTCState tcm) =>
MetaId -> tcm (Maybe Term)
metaInstantiation MetaId
metaId = MetaId -> tcm MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
metaId tcm MetaVariable
-> (MetaVariable -> MetaInstantiation) -> tcm MetaInstantiation
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> MetaVariable -> MetaInstantiation
mvInstantiation tcm MetaInstantiation
-> (MetaInstantiation -> tcm (Maybe Term)) -> tcm (Maybe Term)
forall a b. tcm a -> (a -> tcm b) -> tcm b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  InstV Instantiation
inst -> Maybe Term -> tcm (Maybe Term)
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term -> tcm (Maybe Term)) -> Maybe Term -> tcm (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Instantiation -> Term
instBody Instantiation
inst
  MetaInstantiation
_ -> Maybe Term -> tcm (Maybe Term)
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
forall a. Maybe a
Nothing

isTypeDatatype :: (MonadTCM tcm, MonadReduce tcm, HasConstInfo tcm) => Type -> tcm Bool
isTypeDatatype :: forall (tcm :: * -> *).
(MonadTCM tcm, MonadReduce tcm, HasConstInfo tcm) =>
Type -> tcm Bool
isTypeDatatype Type
typ = do
  typ' <- Type -> tcm Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
typ
  case unEl typ' of
    Def QName
qname Elims
_ -> Definition -> Defn
theDef (Definition -> Defn) -> tcm Definition -> tcm Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> tcm Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qname tcm Defn -> (Defn -> tcm Bool) -> tcm Bool
forall a b. tcm a -> (a -> tcm b) -> tcm b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Datatype{} -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
      Defn
_ -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Term
_ -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

------------------------------------------------------------------------------
-- * Components
------------------------------------------------------------------------------

-- ^ NOTE: Collects components from the *current* context, not the context of
-- the 'InteractionId'.
collectComponents :: Options -> Costs -> InteractionId -> Maybe QName -> [QName] -> MetaId -> TCM BaseComponents
collectComponents :: Options
-> Costs
-> InteractionId
-> Maybe QName
-> [QName]
-> MetaId
-> TCM BaseComponents
collectComponents Options
opts Costs
costs InteractionId
ii Maybe QName
mDefName [QName]
whereNames MetaId
metaId = do
  lhsVars' <- InteractionId -> TCMT IO (Open [(Term, Maybe VerboseLevel)])
forall (tcm :: * -> *).
(MonadFail tcm, ReadTCState tcm, MonadError TCErr tcm,
 MonadTCM tcm, HasConstInfo tcm) =>
InteractionId -> tcm (Open [(Term, Maybe VerboseLevel)])
collectLHSVars InteractionId
ii
  let recVars = Open [(Term, Maybe VerboseLevel)]
lhsVars' Open [(Term, Maybe VerboseLevel)]
-> ([(Term, Maybe VerboseLevel)]
    -> [(Term, NoSubst Term VerboseLevel)])
-> Open [(Term, NoSubst Term VerboseLevel)]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ [(Term, Maybe VerboseLevel)]
vars -> [ (Term
tm, VerboseLevel -> NoSubst Term VerboseLevel
forall t a. a -> NoSubst t a
NoSubst VerboseLevel
i) | (Term
tm, Just VerboseLevel
i) <- [(Term, Maybe VerboseLevel)]
vars ]
  lhsVars <- getOpen $ map fst <$> lhsVars'
  typedLocals <- getLocalVarTerms 0
  reportSDoc "mimer.components" 40 $ "All LHS variables:" <+> prettyTCM lhsVars <+> parens ("or" <+> pretty lhsVars)
  let typedLhsVars = ((Term, Dom Type) -> Bool)
-> [(Term, Dom Type)] -> [(Term, Dom Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Term
term,Dom Type
typ) -> Term
term Term -> [Term] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Term]
lhsVars) [(Term, Dom Type)]
typedLocals
  reportSDoc "mimer.components" 40 $
    "LHS variables with types:" <+> prettyList (map prettyTCMTypedTerm typedLhsVars) <+> parens ("or"
      <+> prettyList (map prettyTypedTerm typedLhsVars))
  -- TODO: For now, we *never* split on implicit arguments even if they are
  -- written explicitly on the LHS.
  splitVarsTyped <- filterM (\(Term
term, Dom Type
typ) ->
                 ((ArgInfo -> Hiding
argInfoHiding (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
typ) Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
NotHidden) Bool -> Bool -> Bool
&&) (Bool -> Bool) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM Bool
forall (tcm :: * -> *).
(MonadTCM tcm, MonadReduce tcm, HasConstInfo tcm) =>
Type -> tcm Bool
isTypeDatatype (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
typ))
               typedLhsVars
  reportSDoc "mimer.components" 40 $
    "Splittable variables" <+> prettyList (map prettyTCMTypedTerm splitVarsTyped) <+> parens ("or"
      <+> prettyList (map prettyTypedTerm splitVarsTyped))

  splitVars <- makeOpen $ map fst splitVarsTyped

  letVars <- getLetVars (costLet costs)


  let components = BaseComponents
        { hintFns :: [Component]
hintFns = []
        , hintDataTypes :: [Component]
hintDataTypes = []
        , hintRecordTypes :: [Component]
hintRecordTypes = []
        , hintProjections :: [Component]
hintProjections = []
        , hintAxioms :: [Component]
hintAxioms = []
        , hintLevel :: [Component]
hintLevel = []
        , hintThisFn :: Maybe Component
hintThisFn = Maybe Component
forall a. Maybe a
Nothing
        , hintRecVars :: Open [(Term, NoSubst Term VerboseLevel)]
hintRecVars = Open [(Term, NoSubst Term VerboseLevel)]
recVars
        , hintLetVars :: [Open Component]
hintLetVars = [Open Component]
letVars
        , hintSplitVars :: Open [Term]
hintSplitVars = Open [Term]
splitVars
        }
  metaVar <- lookupLocalMeta metaId
  hintNames <- getEverythingInScope metaVar
  components' <- foldM go components $ explicitHints ++ (hintNames \\ explicitHints)
  return BaseComponents
    { hintFns = doSort $ hintFns components'
    , hintDataTypes = doSort $ hintDataTypes components'
    , hintRecordTypes = doSort $ hintRecordTypes components'
    , hintProjections = doSort $ hintProjections components'
    , hintAxioms = doSort $ hintAxioms components'
    , hintLevel = doSort $ hintLevel components'
    , hintThisFn = hintThisFn components'
    , hintRecVars = recVars
    , hintLetVars = letVars
    , hintSplitVars = splitVars
    }
  where
    hintMode :: HintMode
hintMode = Options -> HintMode
optHintMode Options
opts
    explicitHints :: [QName]
explicitHints = Options -> [QName]
optExplicitHints Options
opts
    -- Sort by the arity of the type
    doSort :: [Component] -> [Component]
doSort = (Component -> VerboseLevel) -> [Component] -> [Component]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Type -> VerboseLevel
arity (Type -> VerboseLevel)
-> (Component -> Type) -> Component -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Component -> Type
compType)

    isNotMutual :: QName -> Defn -> Bool
isNotMutual QName
qname Defn
f = case Maybe QName
mDefName of
      Maybe QName
Nothing -> Bool
True
      Just QName
defName -> QName
defName QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
/= QName
qname Bool -> Bool -> Bool
&& ([QName] -> Bool) -> Maybe [QName] -> Maybe Bool
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName
defName QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`)) (Defn -> Maybe [QName]
funMutual Defn
f) Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True

    go :: BaseComponents -> QName -> TCM BaseComponents
go BaseComponents
comps QName
qname = do
      info <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qname
      typ <- typeOfConst qname
      scope <- getScope
      let addLevel  = VerboseLevel -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
 MonadTCM tcm) =>
VerboseLevel -> QName -> tcm Component
qnameToComponent (Costs -> VerboseLevel
costLevel   Costs
costs) QName
qname TCMT IO Component
-> (Component -> BaseComponents) -> TCM BaseComponents
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Component
comp -> BaseComponents
comps{hintLevel     = comp : hintLevel  comps}
          addAxiom  = VerboseLevel -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
 MonadTCM tcm) =>
VerboseLevel -> QName -> tcm Component
qnameToComponent (Costs -> VerboseLevel
costAxiom   Costs
costs) QName
qname TCMT IO Component
-> (Component -> BaseComponents) -> TCM BaseComponents
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Component
comp -> BaseComponents
comps{hintAxioms    = comp : hintAxioms comps}
          addThisFn = VerboseLevel -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
 MonadTCM tcm) =>
VerboseLevel -> QName -> tcm Component
qnameToComponent (Costs -> VerboseLevel
costRecCall Costs
costs) QName
qname TCMT IO Component
-> (Component -> BaseComponents) -> TCM BaseComponents
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Component
comp -> BaseComponents
comps{hintThisFn    = Just comp{ compRec = True }}
          addFn     = VerboseLevel -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
 MonadTCM tcm) =>
VerboseLevel -> QName -> tcm Component
qnameToComponent (Costs -> VerboseLevel
costFn      Costs
costs) QName
qname TCMT IO Component
-> (Component -> BaseComponents) -> TCM BaseComponents
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Component
comp -> BaseComponents
comps{hintFns       = comp : hintFns comps}
          addData   = VerboseLevel -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
 MonadTCM tcm) =>
VerboseLevel -> QName -> tcm Component
qnameToComponent (Costs -> VerboseLevel
costSet     Costs
costs) QName
qname TCMT IO Component
-> (Component -> BaseComponents) -> TCM BaseComponents
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Component
comp -> BaseComponents
comps{hintDataTypes = comp : hintDataTypes comps}
      case theDef info of
        Axiom{} | Type -> Bool
isToLevel Type
typ    -> TCM BaseComponents
addLevel
                | ScopeInfo -> Bool
shouldKeep ScopeInfo
scope -> TCM BaseComponents
addAxiom
                | Bool
otherwise        -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
        -- TODO: Check if we want to use these
        DataOrRecSig{}   -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
        Defn
GeneralizableVar -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
        AbstractDefn{}   -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
        -- If the function is in the same mutual block, do not include it.
        f :: Defn
f@Function{}
          | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
qname Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mDefName                  -> TCM BaseComponents
addThisFn
          | Type -> Bool
isToLevel Type
typ Bool -> Bool -> Bool
&& QName -> Defn -> Bool
isNotMutual QName
qname Defn
f    -> TCM BaseComponents
addLevel
          | QName -> Defn -> Bool
isNotMutual QName
qname Defn
f Bool -> Bool -> Bool
&& ScopeInfo -> Bool
shouldKeep ScopeInfo
scope -> TCM BaseComponents
addFn
          | Bool
otherwise                               -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
        Datatype{} -> TCM BaseComponents
addData
        Record{} -> do
          projections <- (QName -> TCMT IO Component) -> [QName] -> TCMT IO [Component]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (VerboseLevel -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
 MonadTCM tcm) =>
VerboseLevel -> QName -> tcm Component
qnameToComponent (Costs -> VerboseLevel
costSpeculateProj Costs
costs)) ([QName] -> TCMT IO [Component])
-> TCMT IO [QName] -> TCMT IO [Component]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO [QName]
forall (tcm :: * -> *).
(HasConstInfo tcm, MonadTCM tcm) =>
QName -> tcm [QName]
getRecordFields QName
qname
          comp <- qnameToComponent (costSet costs) qname
          return comps{ hintRecordTypes = comp : hintRecordTypes comps
                      , hintProjections = projections ++ hintProjections comps }
        -- We look up constructors when we need them
        Constructor{} -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
        -- TODO: special treatment for primitives?
        Primitive{} | Type -> Bool
isToLevel Type
typ    -> TCM BaseComponents
addLevel
                    | ScopeInfo -> Bool
shouldKeep ScopeInfo
scope -> TCM BaseComponents
addFn
                    | Bool
otherwise        -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
        PrimitiveSort{} -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
      where
        shouldKeep :: ScopeInfo -> Bool
shouldKeep ScopeInfo
scope = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or
          [ QName
qname QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
explicitHints
          , QName
qname QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
whereNames
          , case HintMode
hintMode of
              HintMode
Unqualified -> QName -> ScopeInfo -> Bool
Scope.isNameInScopeUnqualified QName
qname ScopeInfo
scope
              HintMode
AllModules  -> Bool
True
              HintMode
Module      -> ModuleName -> Maybe ModuleName
forall a. a -> Maybe a
Just (QName -> ModuleName
qnameModule QName
qname) Maybe ModuleName -> Maybe ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe ModuleName
mThisModule
              HintMode
NoHints     -> Bool
False
          ]

        -- TODO: There is probably a better way of finding the module name
        mThisModule :: Maybe ModuleName
mThisModule = QName -> ModuleName
qnameModule (QName -> ModuleName) -> Maybe QName -> Maybe ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe QName
mDefName

    -- NOTE: We do not reduce the type before checking, so some user definitions
    -- will not be included here.
    isToLevel :: Type -> Bool
    isToLevel :: Type -> Bool
isToLevel Type
typ = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
typ of
      Pi Dom Type
_ Abs Type
abs -> Type -> Bool
isToLevel (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
abs)
      Def QName
qname Elims
_ -> QName -> ArgName
forall a. Pretty a => a -> ArgName
P.prettyShow QName
qname ArgName -> ArgName -> Bool
forall a. Eq a => a -> a -> Bool
== ArgName
builtinLevelName
      Term
_ -> Bool
False

    prettyTCMTypedTerm :: (PrettyTCM tm, PrettyTCM ty) => (tm, ty) -> TCM Doc
    prettyTCMTypedTerm :: forall tm ty.
(PrettyTCM tm, PrettyTCM ty) =>
(tm, ty) -> TCMT IO Doc
prettyTCMTypedTerm (tm
term, ty
typ) = tm -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => tm -> m Doc
prettyTCM tm
term TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ty -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ty -> m Doc
prettyTCM ty
typ
    prettyTypedTerm :: (a, a) -> m Doc
prettyTypedTerm (a
term, a
typ) = a -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
term m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
typ

qnameToComponent :: (HasConstInfo tcm, ReadTCState tcm, MonadFresh CompId tcm, MonadTCM tcm)
  => Cost -> QName -> tcm Component
qnameToComponent :: forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
 MonadTCM tcm) =>
VerboseLevel -> QName -> tcm Component
qnameToComponent VerboseLevel
cost QName
qname = do
  info <- QName -> tcm Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qname
  typ  <- typeOfConst qname
  -- #7120: typeOfConst is the type inside the module, so we need to apply the module params here
  mParams <- freeVarsToApply qname
  let def = (QName -> Elims -> Term
Def QName
qname [] Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Args
mParams, VerboseLevel
0)
      (term, pars) = case theDef info of
        c :: Defn
c@Constructor{}  -> (ConHead -> ConInfo -> Elims -> Term
Con (Defn -> ConHead
conSrcCon Defn
c) ConInfo
ConOCon [], Defn -> VerboseLevel
conPars Defn
c VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- Args -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Args
mParams)
        Axiom{}          -> (Term, VerboseLevel)
def
        Defn
GeneralizableVar -> (Term, VerboseLevel)
def
        Function{}       -> (Term, VerboseLevel)
def
        Datatype{}       -> (Term, VerboseLevel)
def
        Record{}         -> (Term, VerboseLevel)
def
        Primitive{}      -> (Term, VerboseLevel)
def
        PrimitiveSort{}  -> (Term, VerboseLevel)
def
        DataOrRecSig{}   -> (Term, VerboseLevel)
forall a. HasCallStack => a
__IMPOSSIBLE__
        AbstractDefn{}   -> (Term, VerboseLevel)
forall a. HasCallStack => a
__IMPOSSIBLE__
  newComponentQ [] cost qname pars term typ

getEverythingInScope :: MonadTCM tcm => MetaVariable -> tcm [QName]
getEverythingInScope :: forall (tcm :: * -> *). MonadTCM tcm => MetaVariable -> tcm [QName]
getEverythingInScope MetaVariable
metaVar = do
  let scope :: ScopeInfo
scope = Closure Range -> ScopeInfo
forall a. Closure a -> ScopeInfo
clScope (Closure Range -> ScopeInfo) -> Closure Range -> ScopeInfo
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Closure Range
getMetaInfo MetaVariable
metaVar
  let nameSpace :: NameSpace
nameSpace = ScopeInfo -> NameSpace
Scope.everythingInScope ScopeInfo
scope
      names :: NamesInScope
names = NameSpace -> NamesInScope
Scope.nsNames NameSpace
nameSpace
      validKind :: KindOfName -> Bool
validKind = \ case
        KindOfName
Scope.PatternSynName           -> Bool
False   -- could consider allowing pattern synonyms, but the problem is they can't be getConstInfo'd
        KindOfName
Scope.GeneralizeName           -> Bool
False   -- and any way finding the underlying constructors should be easy
        KindOfName
Scope.DisallowedGeneralizeName -> Bool
False
        KindOfName
Scope.MacroName                -> Bool
False
        KindOfName
Scope.QuotableName             -> Bool
False
        KindOfName
Scope.ConName                  -> Bool
True
        KindOfName
Scope.CoConName                -> Bool
True
        KindOfName
Scope.FldName                  -> Bool
True
        KindOfName
Scope.DataName                 -> Bool
True
        KindOfName
Scope.RecName                  -> Bool
True
        KindOfName
Scope.FunName                  -> Bool
True
        KindOfName
Scope.AxiomName                -> Bool
True
        KindOfName
Scope.PrimName                 -> Bool
True
        KindOfName
Scope.OtherDefName             -> Bool
True
      qnames :: [QName]
qnames = (AbstractName -> QName) -> [AbstractName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map AbstractName -> QName
Scope.anameName
             ([AbstractName] -> [QName])
-> ([NonEmpty AbstractName] -> [AbstractName])
-> [NonEmpty AbstractName]
-> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName -> Bool) -> [AbstractName] -> [AbstractName]
forall a. (a -> Bool) -> [a] -> [a]
filter (KindOfName -> Bool
validKind (KindOfName -> Bool)
-> (AbstractName -> KindOfName) -> AbstractName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
Scope.anameKind)
             ([AbstractName] -> [AbstractName])
-> ([NonEmpty AbstractName] -> [AbstractName])
-> [NonEmpty AbstractName]
-> [AbstractName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty AbstractName -> AbstractName)
-> [NonEmpty AbstractName] -> [AbstractName]
forall a b. (a -> b) -> [a] -> [b]
map NonEmpty AbstractName -> AbstractName
forall a. NonEmpty a -> a
NonEmptyList.head
             ([NonEmpty AbstractName] -> [QName])
-> [NonEmpty AbstractName] -> [QName]
forall a b. (a -> b) -> a -> b
$ NamesInScope -> [NonEmpty AbstractName]
forall k a. Map k a -> [a]
Map.elems NamesInScope
names
  [QName] -> tcm [QName]
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return [QName]
qnames

getLetVars :: (MonadFresh CompId tcm, MonadTCM tcm, Monad tcm) => Cost -> tcm [Open Component]
getLetVars :: forall (tcm :: * -> *).
(MonadFresh VerboseLevel tcm, MonadTCM tcm, Monad tcm) =>
VerboseLevel -> tcm [Open Component]
getLetVars VerboseLevel
cost = do
  bindings <- (TCEnv -> LetBindings) -> tcm LetBindings
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> LetBindings
envLetBindings
  mapM makeComp $ Map.toAscList bindings
  where
    -- makeComp :: (Name, Open LetBinding) -> tcm (Open Component)
    makeComp :: (Name, Open LetBinding) -> tcm (Open Component)
makeComp (Name
name, Open LetBinding
opn) = do
      cId <- tcm VerboseLevel
forall i (m :: * -> *). MonadFresh i m => m i
fresh
      return $ opn <&> \ (LetBinding Origin
_ Term
term Dom Type
typ) ->
                VerboseLevel
-> [MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> Component
mkComponent VerboseLevel
cId [] VerboseLevel
cost (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
name) VerboseLevel
0 Term
term (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
typ)

builtinLevelName :: String
builtinLevelName :: ArgName
builtinLevelName = ArgName
"Agda.Primitive.Level"

-- IDEA:
-- [x] 1. Modify the collectRecVarCandidates to get all variables.
-- [ ] 2. Go through all variables to see if they are data types (not records)
-- [ ] 3. Run makeCase for those variables.
-- [ ] 4. Find out how to get the new interaction points/metas from the cases
-- [ ] 5. After search is done, compute out-of-scope variables.
-- [ ] 6. Run make-case again to introduce those variables.
-- [ ] 7. Redo the reification in the new clauses.
-- [ ] 8. Return the new clauses and follow Auto for insertion.

-- | Returns the variables as terms together with whether they where found under
-- some constructor, and if so which argument of the function they appeared in. This
-- information is used when building recursive calls, where it's important that we don't try to
-- construct non-terminating solutions.
collectLHSVars :: (MonadFail tcm, ReadTCState tcm, MonadError TCErr tcm, MonadTCM tcm, HasConstInfo tcm)
  => InteractionId -> tcm (Open [(Term, Maybe Int)])
collectLHSVars :: forall (tcm :: * -> *).
(MonadFail tcm, ReadTCState tcm, MonadError TCErr tcm,
 MonadTCM tcm, HasConstInfo tcm) =>
InteractionId -> tcm (Open [(Term, Maybe VerboseLevel)])
collectLHSVars InteractionId
ii = do
  ipc <- InteractionPoint -> IPClause
ipClause (InteractionPoint -> IPClause)
-> tcm InteractionPoint -> tcm IPClause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionId -> tcm InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
  case ipc of
    IPClause
IPNoClause -> [(Term, Maybe VerboseLevel)]
-> tcm (Open [(Term, Maybe VerboseLevel)])
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
a -> m (Open a)
makeOpen []
    IPClause{ipcQName :: IPClause -> QName
ipcQName = QName
fnName, ipcClauseNo :: IPClause -> VerboseLevel
ipcClauseNo = VerboseLevel
clauseNr} -> do
      info <- QName -> tcm Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
fnName
      typ <- typeOfConst fnName
      parCount <- liftTCM getCurrentModuleFreeVars
      case theDef info of
        fnDef :: Defn
fnDef@Function{} -> do
          let clause :: Clause
clause = Defn -> [Clause]
funClauses Defn
fnDef [Clause] -> VerboseLevel -> Clause
forall a. HasCallStack => [a] -> VerboseLevel -> a
!! VerboseLevel
clauseNr
              naps :: NAPs
naps = Clause -> NAPs
namedClausePats Clause
clause

          -- Telescope at interaction point
          iTel <- tcm Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
          -- Telescope for the body of the clause
          let cTel = Clause -> Telescope
clauseTel Clause
clause
          -- HACK: To get the correct indices, we shift by the difference in telescope lengths
          -- TODO: Difference between teleArgs and telToArgs?
          let shift = [Arg ArgName] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length (Telescope -> [Arg ArgName]
forall a. TelToArgs a => a -> [Arg ArgName]
telToArgs Telescope
iTel) VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- [Arg ArgName] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length (Telescope -> [Arg ArgName]
forall a. TelToArgs a => a -> [Arg ArgName]
telToArgs Telescope
cTel)

          reportSDoc "mimer" 60 $ vcat
            [ "Tel:"
            , nest 2 $ pretty iTel $$ prettyTCM iTel
            , "CTel:"
            , nest 2 $ pretty cTel $$ prettyTCM cTel
            ]
          reportSDoc "mimer" 60 $ "Shift:" <+> pretty shift

          makeOpen [ (Var (n + shift) [], (i - parCount) <$ guard underCon)    -- We count arguments excluding module parameters
                   | (i, nap) <- zip [0..] naps
                   , (n, underCon) <- go False $ namedThing $ unArg nap
                   ]
        Defn
_ -> do
          [(Term, Maybe VerboseLevel)]
-> tcm (Open [(Term, Maybe VerboseLevel)])
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
a -> m (Open a)
makeOpen []
  where
    go :: Bool -> DeBruijnPattern -> [(VerboseLevel, Bool)]
go Bool
isUnderCon = \case
      VarP PatternInfo
patInf DBPatVar
x -> [(DBPatVar -> VerboseLevel
dbPatVarIndex DBPatVar
x, Bool
isUnderCon)]
      DotP PatternInfo
patInf Term
t -> [] -- Ignore dot patterns
      ConP ConHead
conHead ConPatternInfo
conPatInf NAPs
namedArgs -> (NamedArg DeBruijnPattern -> [(VerboseLevel, Bool)])
-> NAPs -> [(VerboseLevel, Bool)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool -> DeBruijnPattern -> [(VerboseLevel, Bool)]
go Bool
True (DeBruijnPattern -> [(VerboseLevel, Bool)])
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> [(VerboseLevel, Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern
forall e. Arg e -> e
unArg) NAPs
namedArgs
      LitP{} -> []
      ProjP{} -> []
      IApplyP{} -> [] -- Only for Cubical?
      DefP{} -> [] -- Only for Cubical?

declarationQnames :: A.Declaration -> [QName]
declarationQnames :: Declaration -> [QName]
declarationQnames Declaration
dec = [ QName
q | Scope.WithKind KindOfName
_ QName
q <- Declaration -> [KName]
forall m. Collection KName m => Declaration -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
A.declaredNames Declaration
dec ]

------------------------------------------------------------------------------
-- * Measure performance
------------------------------------------------------------------------------
data MimerStats = MimerStats
  { MimerStats -> VerboseLevel
statCompHit :: Nat -- ^ Could make use of an already generated component
  , MimerStats -> VerboseLevel
statCompGen :: Nat -- ^ Could use a generator for a component
  , MimerStats -> VerboseLevel
statCompRegen :: Nat -- ^ Had to regenerate the cache (new context)
  , MimerStats -> VerboseLevel
statCompNoRegen :: Nat -- ^ Did not have to regenerate the cache
  , MimerStats -> VerboseLevel
statMetasCreated :: Nat -- ^ Total number of meta-variables created explicitly (not through unification)
  , MimerStats -> VerboseLevel
statTypeEqChecks :: Nat -- ^ Number of times type equality is tested (with unification)
  , MimerStats -> VerboseLevel
statRefineSuccess :: Nat -- ^ Number of times a refinement has been successful
  , MimerStats -> VerboseLevel
statRefineFail :: Nat -- ^ Number of times a refinement has failed
  } deriving (VerboseLevel -> MimerStats -> ArgName -> ArgName
[MimerStats] -> ArgName -> ArgName
MimerStats -> ArgName
(VerboseLevel -> MimerStats -> ArgName -> ArgName)
-> (MimerStats -> ArgName)
-> ([MimerStats] -> ArgName -> ArgName)
-> Show MimerStats
forall a.
(VerboseLevel -> a -> ArgName -> ArgName)
-> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
$cshowsPrec :: VerboseLevel -> MimerStats -> ArgName -> ArgName
showsPrec :: VerboseLevel -> MimerStats -> ArgName -> ArgName
$cshow :: MimerStats -> ArgName
show :: MimerStats -> ArgName
$cshowList :: [MimerStats] -> ArgName -> ArgName
showList :: [MimerStats] -> ArgName -> ArgName
Show, MimerStats -> MimerStats -> Bool
(MimerStats -> MimerStats -> Bool)
-> (MimerStats -> MimerStats -> Bool) -> Eq MimerStats
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MimerStats -> MimerStats -> Bool
== :: MimerStats -> MimerStats -> Bool
$c/= :: MimerStats -> MimerStats -> Bool
/= :: MimerStats -> MimerStats -> Bool
Eq, (forall x. MimerStats -> Rep MimerStats x)
-> (forall x. Rep MimerStats x -> MimerStats) -> Generic MimerStats
forall x. Rep MimerStats x -> MimerStats
forall x. MimerStats -> Rep MimerStats x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MimerStats -> Rep MimerStats x
from :: forall x. MimerStats -> Rep MimerStats x
$cto :: forall x. Rep MimerStats x -> MimerStats
to :: forall x. Rep MimerStats x -> MimerStats
Generic)
instance NFData MimerStats

emptyMimerStats :: MimerStats
emptyMimerStats :: MimerStats
emptyMimerStats = MimerStats
  { statCompHit :: VerboseLevel
statCompHit = VerboseLevel
0, statCompGen :: VerboseLevel
statCompGen = VerboseLevel
0, statCompRegen :: VerboseLevel
statCompRegen = VerboseLevel
0 , statCompNoRegen :: VerboseLevel
statCompNoRegen = VerboseLevel
0 , statMetasCreated :: VerboseLevel
statMetasCreated = VerboseLevel
0, statTypeEqChecks :: VerboseLevel
statTypeEqChecks = VerboseLevel
0, statRefineSuccess :: VerboseLevel
statRefineSuccess = VerboseLevel
0 , statRefineFail :: VerboseLevel
statRefineFail = VerboseLevel
0}

incCompHit, incCompGen, incCompRegen, incCompNoRegen, incMetasCreated, incTypeEqChecks, incRefineSuccess, incRefineFail :: MimerStats -> MimerStats
incCompHit :: MimerStats -> MimerStats
incCompHit       MimerStats
stats = MimerStats
stats {statCompHit       = succ $ statCompHit stats}
incCompGen :: MimerStats -> MimerStats
incCompGen       MimerStats
stats = MimerStats
stats {statCompGen       = succ $ statCompGen stats}
incCompRegen :: MimerStats -> MimerStats
incCompRegen     MimerStats
stats = MimerStats
stats {statCompRegen     = succ $ statCompRegen stats}
incCompNoRegen :: MimerStats -> MimerStats
incCompNoRegen   MimerStats
stats = MimerStats
stats {statCompNoRegen   = succ $ statCompNoRegen stats}
incMetasCreated :: MimerStats -> MimerStats
incMetasCreated  MimerStats
stats = MimerStats
stats {statMetasCreated  = succ $ statMetasCreated stats}
incTypeEqChecks :: MimerStats -> MimerStats
incTypeEqChecks  MimerStats
stats = MimerStats
stats {statTypeEqChecks  = succ $ statTypeEqChecks stats}
incRefineSuccess :: MimerStats -> MimerStats
incRefineSuccess MimerStats
stats = MimerStats
stats {statRefineSuccess = succ $ statRefineSuccess stats}
incRefineFail :: MimerStats -> MimerStats
incRefineFail    MimerStats
stats = MimerStats
stats {statRefineFail    = succ $ statRefineFail stats}

updateStat :: (MimerStats -> MimerStats) -> SM ()
updateStat :: (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
updateStat MimerStats -> MimerStats
f = ArgName
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) ()
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> m () -> m ()
verboseS ArgName
"mimer.stats" VerboseLevel
10 (ReaderT SearchOptions (TCMT IO) ()
 -> ReaderT SearchOptions (TCMT IO) ())
-> ReaderT SearchOptions (TCMT IO) ()
-> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ do
  ref <- (SearchOptions -> IORef MimerStats)
-> ReaderT SearchOptions (TCMT IO) (IORef MimerStats)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> IORef MimerStats
searchStats
  liftIO $ modifyIORef' ref f


------------------------------------------------------------------------------
-- * Core algorithm
------------------------------------------------------------------------------

runSearch :: Rewrite -> Options -> InteractionId -> Range -> TCM [MimerResult]
runSearch :: Rewrite -> Options -> InteractionId -> Range -> TCM [MimerResult]
runSearch Rewrite
norm Options
options InteractionId
ii Range
rng = InteractionId -> TCM [MimerResult] -> TCM [MimerResult]
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM [MimerResult] -> TCM [MimerResult])
-> TCM [MimerResult] -> TCM [MimerResult]
forall a b. (a -> b) -> a -> b
$ do
  (mTheFunctionQName, whereNames) <- (InteractionPoint -> IPClause)
-> TCMT IO InteractionPoint -> TCMT IO IPClause
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap InteractionPoint -> IPClause
ipClause (InteractionId -> TCMT IO InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii) TCMT IO IPClause
-> (IPClause -> (Maybe QName, [QName]))
-> TCMT IO (Maybe QName, [QName])
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    clause :: IPClause
clause@IPClause{} -> ( QName -> Maybe QName
forall a. a -> Maybe a
Just (QName -> Maybe QName) -> QName -> Maybe QName
forall a b. (a -> b) -> a -> b
$ IPClause -> QName
ipcQName IPClause
clause
                         , case WhereDeclarations -> Maybe Declaration
A.whereDecls (WhereDeclarations -> Maybe Declaration)
-> WhereDeclarations -> Maybe Declaration
forall a b. (a -> b) -> a -> b
$ Clause' SpineLHS -> WhereDeclarations
forall lhs. Clause' lhs -> WhereDeclarations
A.clauseWhereDecls (Clause' SpineLHS -> WhereDeclarations)
-> Clause' SpineLHS -> WhereDeclarations
forall a b. (a -> b) -> a -> b
$ IPClause -> Clause' SpineLHS
ipcClause IPClause
clause of
                             Just Declaration
decl -> Declaration -> [QName]
declarationQnames Declaration
decl
                             Maybe Declaration
_ -> []
                         )
    IPClause
IPNoClause -> (Maybe QName
forall a. Maybe a
Nothing, [])

  reportSDoc "mimer.init" 15 $ "Interaction point in function:" <+> pretty mTheFunctionQName
  reportSDoc "mimer.init" 25 $ "Names in where-block" <+> pretty whereNames

  metaId <- lookupInteractionId ii
  metaVar <- lookupLocalMeta metaId

  -- We want to be able to solve with recursive calls
  setMetaOccursCheck metaId DontRunMetaOccursCheck

  metaIds <- case mvInstantiation metaVar of
    InstV Instantiation
inst -> do

      metaIds <- Term -> TCMT IO [MetaId]
forall t (tcm :: * -> *).
(AllMetas t, ReadTCState tcm) =>
t -> tcm [MetaId]
allOpenMetas (Instantiation -> Term
instBody Instantiation
inst)

      -- TODO: Make pretty instantiation for 'Instantiation'?
      reportSDoc "mimer.init" 20 $ sep [ "Interaction point already instantiated:" <+> pretty (instBody inst)
                                       , "with args" <+> pretty (instTel inst) ]

      -- ctx <- getContextTelescope
      return metaIds
    OpenMeta MetaKind
UnificationMeta -> do
      ArgName -> VerboseLevel -> ArgName -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> ArgName -> m ()
reportSLn ArgName
"mimer.init" VerboseLevel
20 ArgName
"Interaction point not instantiated."
      [MetaId] -> TCMT IO [MetaId]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [MetaId
metaId]
    MetaInstantiation
_ -> TCMT IO [MetaId]
forall a. HasCallStack => a
__IMPOSSIBLE__
  -- TODO: Print each meta-variable's full context telescope
  reportSDoc "mimer.init" 20 $ "Remaining meta-variables to solve:" <+> prettyTCM metaIds
  reportSDoc "mimer.init" 20 $ "Meta var args" <+> (prettyTCM =<< getMetaContextArgs metaVar)


  fnArgs1 <- withShowAllArguments' False $ getContextArgs >>= mapM prettyTCM
  fnArgs2 <- withShowAllArguments' True  $ getContextArgs >>= mapM prettyTCM
  let bringScope = ((Doc, Doc) -> Doc) -> [(Doc, Doc)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc, Doc) -> Doc
forall a b. (a, b) -> b
snd ([(Doc, Doc)] -> [Doc]) -> [(Doc, Doc)] -> [Doc]
forall a b. (a -> b) -> a -> b
$ ((Doc, Doc) -> Bool) -> [(Doc, Doc)] -> [(Doc, Doc)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Doc -> Doc -> Bool) -> (Doc, Doc) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Doc -> Doc -> Bool
forall a. Eq a => a -> a -> Bool
(/=)) ([(Doc, Doc)] -> [(Doc, Doc)]) -> [(Doc, Doc)] -> [(Doc, Doc)]
forall a b. (a -> b) -> a -> b
$ [Doc] -> [Doc] -> [(Doc, Doc)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Doc]
fnArgs1 [Doc]
fnArgs2
      bringScopeNoBraces = (Doc -> ArgName) -> [Doc] -> [ArgName]
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> Bool) -> ArgName -> ArgName
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> ArgName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Char
'{', Char
'}']) (ArgName -> ArgName) -> (Doc -> ArgName) -> Doc -> ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> ArgName
forall a. Doc a -> ArgName
P.render) [Doc]
bringScope
  reportSDoc "mimer.temp" 20 $ vcat
    [ "Things to bring into scope:"
    , nest 2 $ vcat
      [ "Context args (don't show):" <+> pretty fnArgs1
      , "Context args (show all):  " <+> pretty fnArgs2
      , "To bring into scope:      " <+> pretty bringScope
      , "To bring into scope (str):" <+> pretty bringScopeNoBraces
      ]
    ]

  -- Check if there are any meta-variables to be solved
  case metaIds of
    -- No variables to solve, return the instantiation given
    [] -> do
      case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
metaVar of
        InstV Instantiation
inst -> do
          expr <- InteractionId -> TCMT IO Expr -> TCMT IO Expr
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCMT IO Expr -> TCMT IO Expr) -> TCMT IO Expr -> TCMT IO Expr
forall a b. (a -> b) -> a -> b
$ do
            metaArgs <- MetaVariable -> TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVariable
metaVar
            instantiateFull (apply (MetaV metaId []) metaArgs) >>= normalForm norm >>= reify
          str <- P.render <$> prettyTCM expr
          let sol = ArgName -> MimerResult
MimerExpr ArgName
str
          reportSDoc "mimer.init" 10 $ "Goal already solved. Solution:" <+> text str
          return [sol]
        MetaInstantiation
_ -> TCM [MimerResult]
forall a. HasCallStack => a
__IMPOSSIBLE__
    [MetaId]
_ -> do
      costs <- TCM Bool -> TCMT IO Costs -> TCMT IO Costs -> TCMT IO Costs
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (ArgName -> VerboseLevel -> TCM Bool
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> m Bool
hasVerbosity ArgName
"mimer.cost.custom" VerboseLevel
10)
                 {- then -} TCMT IO Costs
customCosts
                 {- else -} (Costs -> TCMT IO Costs
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Costs
defaultCosts)
      reportSDoc "mimer.cost.custom" 10 $ "Using costs:" $$ nest 2 (pretty costs)
      components <- collectComponents options costs ii mTheFunctionQName whereNames metaId
      let startGoals = (MetaId -> Goal) -> [MetaId] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map MetaId -> Goal
Goal [MetaId]
metaIds

      state <- getTC
      env <- askTC

      let startBranch = SearchBranch
            { sbTCState :: TCState
sbTCState = TCState
state
            , sbGoals :: [Goal]
sbGoals = [Goal]
startGoals
            , sbCost :: VerboseLevel
sbCost = VerboseLevel
0
            , sbCache :: Map CheckpointId ComponentCache
sbCache = Map CheckpointId ComponentCache
forall k a. Map k a
Map.empty
            , sbComponentsUsed :: Map Name VerboseLevel
sbComponentsUsed = Map Name VerboseLevel
forall k a. Map k a
Map.empty
            }

      statsRef <- liftIO $ newIORef emptyMimerStats
      checkpoint <- viewTC eCurrentCheckpoint
      let searchOptions = SearchOptions
            { searchBaseComponents :: BaseComponents
searchBaseComponents = BaseComponents
components
            , searchHintMode :: HintMode
searchHintMode = Options -> HintMode
optHintMode Options
options
            , searchTimeout :: Integer
searchTimeout = Options -> Integer
optTimeout Options
options
            , searchGenProjectionsLocal :: Bool
searchGenProjectionsLocal = Bool
True
            , searchGenProjectionsLet :: Bool
searchGenProjectionsLet = Bool
True
            , searchGenProjectionsExternal :: Bool
searchGenProjectionsExternal = Bool
False
            , searchGenProjectionsRec :: Bool
searchGenProjectionsRec = Bool
True
            , searchSpeculateProjections :: Bool
searchSpeculateProjections = Bool
True
            , searchTopMeta :: MetaId
searchTopMeta = MetaId
metaId
            , searchTopEnv :: TCEnv
searchTopEnv = TCEnv
env
            , searchTopCheckpoint :: CheckpointId
searchTopCheckpoint = CheckpointId
checkpoint
            , searchInteractionId :: InteractionId
searchInteractionId = InteractionId
ii
            , searchFnName :: Maybe QName
searchFnName = Maybe QName
mTheFunctionQName
            , searchCosts :: Costs
searchCosts = Costs
costs
            , searchStats :: IORef MimerStats
searchStats = IORef MimerStats
statsRef
            , searchRewrite :: Rewrite
searchRewrite = Rewrite
norm
            }

      reportSDoc "mimer.init" 20 $ "Using search options:" $$ nest 2 (prettyTCM searchOptions)
      reportSDoc "mimer.init" 20 $ "Initial search branch:" $$ nest 2 (pretty startBranch)

      flip runReaderT searchOptions $ bench [] $ do

        -- TODO: Check what timing stuff is used in Agda.Utils.Time
        timeout <- fromMilliseconds <$> asks searchTimeout
        startTime <- liftIO getCPUTime
        let go :: Int -> Int -> MinQueue SearchBranch -> SM ([MimerResult], Int)
            go VerboseLevel
0 VerboseLevel
n MinQueue SearchBranch
_ = ([MimerResult], VerboseLevel) -> SM ([MimerResult], VerboseLevel)
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], VerboseLevel
n)
            go VerboseLevel
need VerboseLevel
n MinQueue SearchBranch
branchQueue = case MinQueue SearchBranch
-> Maybe (SearchBranch, MinQueue SearchBranch)
forall a. Ord a => MinQueue a -> Maybe (a, MinQueue a)
Q.minView MinQueue SearchBranch
branchQueue of
              Maybe (SearchBranch, MinQueue SearchBranch)
Nothing -> do
                ArgName
-> VerboseLevel -> ArgName -> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> ArgName -> m ()
reportSLn ArgName
"mimer.search" VerboseLevel
30 (ArgName -> ReaderT SearchOptions (TCMT IO) ())
-> ArgName -> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ ArgName
"No remaining search branches."
                ([MimerResult], VerboseLevel) -> SM ([MimerResult], VerboseLevel)
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], VerboseLevel
n)
              Just (SearchBranch
branch, MinQueue SearchBranch
branchQueue') -> do
                time <- IO CPUTime -> ReaderT SearchOptions (TCMT IO) CPUTime
forall a. IO a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO CPUTime
forall (m :: * -> *). MonadIO m => m CPUTime
getCPUTime
                mimerTrace 0 10 $ vcat
                  [ "Choosing branch"
                  , nest 2 $ sep
                    [ branchInstantiationDocCost branch <> ","
                    , nest 2 $ "metas:" <+> prettyTCM (map goalMeta $ sbGoals branch)
                    ]
                  ]
                reportSDoc "mimer.search" 50 $ "Full branch:" <+> pretty branch
                reportSMDoc "mimer.search" 50 $
                  "Instantiation of other branches:" <+> prettyList (map branchInstantiationDocCost $ Q.toAscList branchQueue')

                let elapsed = CPUTime
time CPUTime -> CPUTime -> CPUTime
forall a. Num a => a -> a -> a
- CPUTime
startTime
                if elapsed < timeout
                then do
                  (newBranches, sols) <- refine branch >>= partitionStepResult
                  let branchQueue'' = (SearchBranch -> MinQueue SearchBranch -> MinQueue SearchBranch)
-> MinQueue SearchBranch -> [SearchBranch] -> MinQueue SearchBranch
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SearchBranch -> MinQueue SearchBranch -> MinQueue SearchBranch
forall a. Ord a => a -> MinQueue a -> MinQueue a
Q.insert MinQueue SearchBranch
branchQueue' [SearchBranch]
newBranches
                  reportSLn "mimer.search" 40 $ show (length sols) ++ " solutions found during cycle " ++ show (n + 1)
                  reportSMDoc "mimer.search" 45 $ "Solutions:" <+> prettyTCM sols
                  mimerTrace 0 40 $ vcat
                     [ "Cycle" <+> pretty (n + 1) <+> "branches"
                     , nest 2 $ vcat $ map branchInstantiationDocCost $ Q.toAscList branchQueue''
                     ]
                  unless (null sols) $ mimerTrace 0 20 $ vcat
                     [ "Cycle" <+> pretty (n + 1) <+> "solutions"
                     , nest 2 $ vcat $ map prettyTCM sols
                     ]

                  let sols' = VerboseLevel -> [MimerResult] -> [MimerResult]
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
need [MimerResult]
sols
                  mapFst (sols' ++) <$> go (need - length sols') (n + 1) branchQueue''
                else do
                  reportSLn "mimer.search" 30 $ "Search time limit reached. Elapsed search time: " ++ show elapsed
                  return ([], n)
        let numSolutions | Options -> Bool
optList Options
options = VerboseLevel
10 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ Options -> VerboseLevel
optSkip Options
options
                         | Bool
otherwise       = VerboseLevel
1 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ Options -> VerboseLevel
optSkip Options
options
        (sols, nrSteps) <- go numSolutions 0 $ Q.singleton startBranch
        reportSLn "mimer.search" 20 $ "Search ended after " ++ show (nrSteps + 1) ++ " cycles"
        -- results <- liftTCM $ mapM exprToStringAndVars sols
        reportSDoc "mimer.search" 15 $ "Solutions found: " <+> prettyList (map prettyTCM sols)
        reportSMDoc "mimer.stats" 10 $ do
          ref <- asks searchStats
          stats <- liftIO $ readIORef ref
          "Statistics:" <+> text (show stats)
        return sols

tryComponents :: Goal -> Type -> SearchBranch -> [(Component, [Component])] -> SM [SearchStepResult]
tryComponents :: Goal
-> Type
-> SearchBranch
-> [(Component, [Component])]
-> SM [SearchStepResult]
tryComponents Goal
goal Type
goalType SearchBranch
branch [(Component, [Component])]
comps = SearchBranch
-> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
  checkpoint <- Lens' TCEnv CheckpointId
-> ReaderT SearchOptions (TCMT IO) CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
Lens' TCEnv CheckpointId
eCurrentCheckpoint
  let tryFor (Component
sourceComp, [Component]
comps') = do
        -- Clear out components that depend on meta-variables that have been used.
        let newCache :: ComponentCache
newCache = Component -> Maybe [Component] -> ComponentCache -> ComponentCache
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Component
sourceComp Maybe [Component]
forall a. Maybe a
Nothing (SearchBranch -> Map CheckpointId ComponentCache
sbCache SearchBranch
branch Map CheckpointId ComponentCache -> CheckpointId -> ComponentCache
forall k a. Ord k => Map k a -> k -> a
Map.! CheckpointId
checkpoint)
        newBranches <- [Maybe SearchBranch] -> [SearchBranch]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe SearchBranch] -> [SearchBranch])
-> ReaderT SearchOptions (TCMT IO) [Maybe SearchBranch]
-> ReaderT SearchOptions (TCMT IO) [SearchBranch]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Component -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch))
-> [Component]
-> ReaderT SearchOptions (TCMT IO) [Maybe SearchBranch]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Goal
-> Type
-> SearchBranch
-> Component
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
tryRefineWith Goal
goal Type
goalType SearchBranch
branch) [Component]
comps'
        return $ map (\SearchBranch
br -> SearchBranch
br{sbCache = Map.insert checkpoint newCache (sbCache branch)}) newBranches
  newBranches <- concatMapM tryFor comps
  mapM checkSolved newBranches

-- | If there is no cache entry for the checkpoint, create one. If there already
-- is one, even if the components are not yet generated for some entries, it is
-- returned as is.
prepareComponents :: Goal -> SearchBranch -> SM (SearchBranch, [(Component, [Component])])
prepareComponents :: Goal
-> SearchBranch -> SM (SearchBranch, [(Component, [Component])])
prepareComponents Goal
goal SearchBranch
branch = SearchBranch
-> Goal
-> SM (SearchBranch, [(Component, [Component])])
-> SM (SearchBranch, [(Component, [Component])])
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (SM (SearchBranch, [(Component, [Component])])
 -> SM (SearchBranch, [(Component, [Component])]))
-> SM (SearchBranch, [(Component, [Component])])
-> SM (SearchBranch, [(Component, [Component])])
forall a b. (a -> b) -> a -> b
$ do
  checkpoint <- Lens' TCEnv CheckpointId
-> ReaderT SearchOptions (TCMT IO) CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
Lens' TCEnv CheckpointId
eCurrentCheckpoint
  -- Check if we there is something in the cache for this checkpoint
  comps <- case Map.lookup checkpoint (sbCache branch) of
    -- No, generate components from scratch
    Maybe ComponentCache
Nothing -> do
      (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
updateStat MimerStats -> MimerStats
incCompRegen
      ArgName
-> VerboseLevel
-> TCMT IO Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"mimer.components" VerboseLevel
20 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
-> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"No cache found checkpoint:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> CheckpointId -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty CheckpointId
checkpoint
        , VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"with context:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc)
-> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope) ]
      -- Generate components for this context
      comps <- ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
genComponents
      reportSDoc "mimer.components" 20 $ "Generated" <+> pretty (sum $ map (length . snd) comps) <+> "components"
      return comps
    -- Yes, just update the missing generated components
    Just ComponentCache
cache -> ((Component, Maybe [Component])
 -> ReaderT SearchOptions (TCMT IO) (Component, [Component]))
-> [(Component, Maybe [Component])]
-> ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Component, Maybe [Component])
-> ReaderT SearchOptions (TCMT IO) (Component, [Component])
prepare (ComponentCache -> [(Component, Maybe [Component])]
forall k a. Map k a -> [(k, a)]
Map.toAscList ComponentCache
cache)
  let newCache = [(Component, Maybe [Component])] -> ComponentCache
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Component, Maybe [Component])] -> ComponentCache)
-> [(Component, Maybe [Component])] -> ComponentCache
forall a b. (a -> b) -> a -> b
$ ((Component, [Component]) -> (Component, Maybe [Component]))
-> [(Component, [Component])] -> [(Component, Maybe [Component])]
forall a b. (a -> b) -> [a] -> [b]
map (([Component] -> Maybe [Component])
-> (Component, [Component]) -> (Component, Maybe [Component])
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd [Component] -> Maybe [Component]
forall a. a -> Maybe a
Just) [(Component, [Component])]
comps
  branch' <- updateBranch [] branch{sbCache = Map.insert checkpoint newCache (sbCache branch)}
  return (branch', comps)
  where
  prepare :: (Component, Maybe [Component]) -> SM (Component, [Component])
  prepare :: (Component, Maybe [Component])
-> ReaderT SearchOptions (TCMT IO) (Component, [Component])
prepare (Component
sourceComp, Just [Component]
comps) = do
    (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
updateStat MimerStats -> MimerStats
incCompNoRegen
    (Component, [Component])
-> ReaderT SearchOptions (TCMT IO) (Component, [Component])
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Component
sourceComp, [Component]
comps)
  prepare (Component
sourceComp, Maybe [Component]
Nothing) = do
    (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
updateStat MimerStats -> MimerStats
incCompRegen
    (Component
sourceComp,) ([Component] -> (Component, [Component]))
-> ReaderT SearchOptions (TCMT IO) [Component]
-> ReaderT SearchOptions (TCMT IO) (Component, [Component])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Component -> ReaderT SearchOptions (TCMT IO) [Component]
genComponentsFrom Bool
True Component
sourceComp

localVarCount :: SM Int
localVarCount :: SM VerboseLevel
localVarCount = do
  top <- (SearchOptions -> VerboseLevel) -> SM VerboseLevel
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((SearchOptions -> VerboseLevel) -> SM VerboseLevel)
-> (SearchOptions -> VerboseLevel) -> SM VerboseLevel
forall a b. (a -> b) -> a -> b
$ [ContextEntry] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length ([ContextEntry] -> VerboseLevel)
-> (SearchOptions -> [ContextEntry])
-> SearchOptions
-> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> [ContextEntry]
envContext (TCEnv -> [ContextEntry])
-> (SearchOptions -> TCEnv) -> SearchOptions -> [ContextEntry]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> TCEnv
searchTopEnv
  cur <- length <$> getContext
  pure $ cur - top

genComponents :: SM [(Component, [Component])]
genComponents :: ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
genComponents = do
  opts <- ReaderT SearchOptions (TCMT IO) SearchOptions
forall r (m :: * -> *). MonadReader r m => m r
ask
  let comps = SearchOptions -> BaseComponents
searchBaseComponents SearchOptions
opts
  n <- localVarCount
  localVars <- lift (getLocalVars n (costLocal $ searchCosts opts))
    >>= genAddSource (searchGenProjectionsLocal opts)
  recCalls <- genAddSource (searchGenProjectionsRec opts) (maybeToList $ hintThisFn comps)
  letVars <- mapM getOpenComponent (hintLetVars comps)
    >>= genAddSource (searchGenProjectionsLet opts)
  fns <- genAddSource (searchGenProjectionsExternal opts) (hintFns comps)
  axioms <- genAddSource (searchGenProjectionsExternal opts) (hintAxioms comps)
  return $ localVars ++ letVars ++ recCalls ++ fns ++ axioms
  where
    genAddSource :: Bool -> [Component] -> SM [(Component, [Component])]
    genAddSource :: Bool
-> [Component]
-> ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
genAddSource Bool
genProj = (Component
 -> ReaderT SearchOptions (TCMT IO) (Component, [Component]))
-> [Component]
-> ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Component
comp -> (Component
comp,) ([Component] -> (Component, [Component]))
-> ReaderT SearchOptions (TCMT IO) [Component]
-> ReaderT SearchOptions (TCMT IO) (Component, [Component])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Component -> ReaderT SearchOptions (TCMT IO) [Component]
genComponentsFrom Bool
genProj Component
comp)


genComponentsFrom :: Bool -- ^ Apply record elimination
                  -> Component
                  -> SM [Component]
genComponentsFrom :: Bool -> Component -> ReaderT SearchOptions (TCMT IO) [Component]
genComponentsFrom Bool
appRecElims Component
origComp = do
  comps <- if | Component -> Bool
compRec Component
origComp -> (Component -> ReaderT SearchOptions (TCMT IO) Component)
-> [Component] -> ReaderT SearchOptions (TCMT IO) [Component]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Maybe VerboseLevel
-> Component -> ReaderT SearchOptions (TCMT IO) Component
applyToMetasG Maybe VerboseLevel
forall a. Maybe a
Nothing) ([Component] -> ReaderT SearchOptions (TCMT IO) [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
-> ReaderT SearchOptions (TCMT IO) [Component]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Component -> ReaderT SearchOptions (TCMT IO) [Component]
genRecCalls Component
origComp
              | Bool
otherwise        -> (Component -> [Component] -> [Component]
forall a. a -> [a] -> [a]
:[]) (Component -> [Component])
-> ReaderT SearchOptions (TCMT IO) Component
-> ReaderT SearchOptions (TCMT IO) [Component]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe VerboseLevel
-> Component -> ReaderT SearchOptions (TCMT IO) Component
applyToMetasG Maybe VerboseLevel
forall a. Maybe a
Nothing Component
origComp
  if appRecElims
  then concat <$> mapM (applyProjections Set.empty) comps
  else return comps
  where
  applyProjections :: Set QName -> Component -> SM [Component]
  applyProjections :: Set QName
-> Component -> ReaderT SearchOptions (TCMT IO) [Component]
applyProjections Set QName
seenRecords Component
comp = do
    projComps <- Type -> SM (Maybe (QName, Args, [QName], Bool))
getRecordInfo (Component -> Type
compType Component
comp) SM (Maybe (QName, Args, [QName], Bool))
-> (Maybe (QName, Args, [QName], Bool)
    -> ReaderT SearchOptions (TCMT IO) [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Maybe (QName, Args, [QName], Bool)
Nothing -> [Component] -> ReaderT SearchOptions (TCMT IO) [Component]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      Just (QName
recordName, Args
args, [QName]
fields, Bool
isRecursive)
          | QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
recordName Set QName
seenRecords -> do
              ArgName
-> VerboseLevel
-> TCMT IO Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"mimer.components" VerboseLevel
60 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
-> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
                TCMT IO Doc
"Skipping projection because recursive record already seen:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
recordName
              [Component] -> ReaderT SearchOptions (TCMT IO) [Component]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
          | Bool
otherwise -> do
              let seenRecords' :: Set QName
seenRecords' = if Bool
isRecursive then QName -> Set QName -> Set QName
forall a. Ord a => a -> Set a -> Set a
Set.insert QName
recordName Set QName
seenRecords else Set QName
seenRecords
              comps <- (QName -> ReaderT SearchOptions (TCMT IO) Component)
-> [QName] -> ReaderT SearchOptions (TCMT IO) [Component]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Args
-> Component -> QName -> ReaderT SearchOptions (TCMT IO) Component
applyProj Args
args Component
comp (QName -> ReaderT SearchOptions (TCMT IO) Component)
-> (Component -> ReaderT SearchOptions (TCMT IO) Component)
-> QName
-> ReaderT SearchOptions (TCMT IO) Component
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Maybe VerboseLevel
-> Component -> ReaderT SearchOptions (TCMT IO) Component
applyToMetasG Maybe VerboseLevel
forall a. Maybe a
Nothing) [QName]
fields
              concatMapM (applyProjections seenRecords') comps
    return $ comp : projComps

getRecordInfo :: Type
  -> SM (Maybe ( QName     -- Record name
               , Args      -- Record parameters converted to (hidden) arguments
               , [QName]   -- Field names
               , Bool      -- Is recursive?
               ))
getRecordInfo :: Type -> SM (Maybe (QName, Args, [QName], Bool))
getRecordInfo Type
typ = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
typ of
  Def QName
qname Elims
elims -> QName -> ReaderT SearchOptions (TCMT IO) (Maybe RecordData)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe RecordData)
isRecord QName
qname ReaderT SearchOptions (TCMT IO) (Maybe RecordData)
-> (Maybe RecordData -> SM (Maybe (QName, Args, [QName], Bool)))
-> SM (Maybe (QName, Args, [QName], Bool))
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe RecordData
Nothing -> Maybe (QName, Args, [QName], Bool)
-> SM (Maybe (QName, Args, [QName], Bool))
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Args, [QName], Bool)
forall a. Maybe a
Nothing
    Just RecordData
defn -> do
      fields <- QName -> ReaderT SearchOptions (TCMT IO) [QName]
forall (tcm :: * -> *).
(HasConstInfo tcm, MonadTCM tcm) =>
QName -> tcm [QName]
getRecordFields QName
qname
      return $ Just (qname, argsFromElims elims, fields, recRecursive_ defn)
  Term
_ -> Maybe (QName, Args, [QName], Bool)
-> SM (Maybe (QName, Args, [QName], Bool))
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Args, [QName], Bool)
forall a. Maybe a
Nothing

applyProj :: Args -> Component -> QName -> SM Component
applyProj :: Args
-> Component -> QName -> ReaderT SearchOptions (TCMT IO) Component
applyProj Args
recordArgs Component
comp' QName
qname = do
  cost <- (SearchOptions -> VerboseLevel) -> SM VerboseLevel
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Costs -> VerboseLevel
costProj (Costs -> VerboseLevel)
-> (SearchOptions -> Costs) -> SearchOptions -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> Costs
searchCosts)
  let newTerm = Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE (Component -> Term
compTerm Component
comp') [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
qname]
  projType <- defType <$> getConstInfo qname
  projTypeWithArgs <- piApplyM projType recordArgs
  newType <- piApplyM projTypeWithArgs (compTerm comp')
  newComponentQ (compMetas comp') (compCost comp' + cost) qname 0 newTerm newType


-- TODO: currently reducing twice
applyToMetasG
  :: Maybe Nat -- ^ Max number of arguments to apply.
  -> Component -> SM Component
applyToMetasG :: Maybe VerboseLevel
-> Component -> ReaderT SearchOptions (TCMT IO) Component
applyToMetasG (Just VerboseLevel
m) Component
comp | VerboseLevel
m VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
0 = Component -> ReaderT SearchOptions (TCMT IO) Component
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Component
comp
applyToMetasG Maybe VerboseLevel
maxArgs Component
comp = do
  ctx <- ReaderT SearchOptions (TCMT IO) Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  compTyp <- reduce $ compType comp
  case unEl compTyp of
    Pi Dom Type
dom Abs Type
abs -> do
      let domainType :: Type
domainType = Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom
      (metaId, metaTerm) <- Type -> SM (MetaId, Term)
createMeta Type
domainType
      let arg = Origin -> Arg Term -> Arg Term
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term
metaTerm Term -> Arg Type -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
dom
      newType <- reduce =<< piApplyM (compType comp) metaTerm
      -- Constructors the parameters are not included in the term
      let skip = Component -> VerboseLevel
compPars Component
comp
          newTerm | VerboseLevel
skip VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0  = Component -> Term
compTerm Component
comp
                  | Bool
otherwise = Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply (Component -> Term
compTerm Component
comp) [Arg Term
arg]
      cost <- asks $ (if getHiding arg == Hidden then costNewHiddenMeta else costNewMeta) . searchCosts
      applyToMetasG (predNat <$> maxArgs)
                    comp{ compTerm = newTerm
                        , compType = newType
                        , compPars = predNat skip
                        , compMetas = metaId : compMetas comp
                        , compCost = cost + compCost comp
                        }
    Term
_ ->
      -- Set the type to the reduced version
      Component -> ReaderT SearchOptions (TCMT IO) Component
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Component
comp{compType = compTyp}

createMeta :: Type -> SM (MetaId, Term)
createMeta :: Type -> SM (MetaId, Term)
createMeta Type
typ = do
  (metaId, metaTerm) <- RunMetaOccursCheck -> Comparison -> Type -> SM (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck Comparison
CmpLeq Type
typ
  verboseS "mimer.stats" 20 $ updateStat incMetasCreated
  reportSDoc "mimer.components" 80 $ do
    "Created meta-variable (type in context):" <+> pretty metaTerm <+> ":" <+> (pretty =<< getMetaTypeInContext metaId)
  return (metaId, metaTerm)


partitionStepResult :: [SearchStepResult] -> SM ([SearchBranch], [MimerResult])
partitionStepResult :: [SearchStepResult]
-> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
partitionStepResult [] = ([SearchBranch], [MimerResult])
-> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([],[])
partitionStepResult (SearchStepResult
x:[SearchStepResult]
xs) = do
  let rest :: ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
rest = [SearchStepResult]
-> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
partitionStepResult [SearchStepResult]
xs
  (brs',sols) <- ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
rest
  case x of
    SearchStepResult
NoSolution -> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
rest
    OpenBranch SearchBranch
br -> ([SearchBranch], [MimerResult])
-> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SearchBranch
brSearchBranch -> [SearchBranch] -> [SearchBranch]
forall a. a -> [a] -> [a]
:[SearchBranch]
brs', [MimerResult]
sols)
    ResultExpr Expr
exp -> do
      str <- Doc -> ArgName
forall a. Doc a -> ArgName
P.render (Doc -> ArgName)
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ArgName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
exp
      return $ (brs', MimerExpr str : sols)
    ResultClauses [Clause]
cls -> do
      f <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName)
-> ReaderT SearchOptions (TCMT IO) (Maybe QName)
-> ReaderT SearchOptions (TCMT IO) QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SearchOptions -> Maybe QName)
-> ReaderT SearchOptions (TCMT IO) (Maybe QName)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> Maybe QName
searchFnName
      return $ (brs', MimerClauses f cls : sols)


topInstantiationDoc :: SM Doc
topInstantiationDoc :: ReaderT SearchOptions (TCMT IO) Doc
topInstantiationDoc = (SearchOptions -> MetaId) -> ReaderT SearchOptions (TCMT IO) MetaId
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> MetaId
searchTopMeta ReaderT SearchOptions (TCMT IO) MetaId
-> (MetaId -> ReaderT SearchOptions (TCMT IO) (Maybe Expr))
-> ReaderT SearchOptions (TCMT IO) (Maybe Expr)
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= MetaId -> ReaderT SearchOptions (TCMT IO) (Maybe Expr)
forall (tcm :: * -> *).
(MonadTCM tcm, PureTCM tcm, MonadDebug tcm,
 MonadInteractionPoints tcm, MonadFresh NameId tcm) =>
MetaId -> tcm (Maybe Expr)
getMetaInstantiation ReaderT SearchOptions (TCMT IO) (Maybe Expr)
-> (Maybe Expr -> ReaderT SearchOptions (TCMT IO) Doc)
-> ReaderT SearchOptions (TCMT IO) Doc
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ReaderT SearchOptions (TCMT IO) Doc
-> (Expr -> ReaderT SearchOptions (TCMT IO) Doc)
-> Maybe Expr
-> ReaderT SearchOptions (TCMT IO) Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Doc -> ReaderT SearchOptions (TCMT IO) Doc
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
"(nothing)") Expr -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM

prettyGoalInst :: Goal -> SM Doc
prettyGoalInst :: Goal -> ReaderT SearchOptions (TCMT IO) Doc
prettyGoalInst Goal
goal = Goal
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall a. Goal -> SM a -> SM a
inGoalEnv Goal
goal (ReaderT SearchOptions (TCMT IO) Doc
 -> ReaderT SearchOptions (TCMT IO) Doc)
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$ do
  args <- (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Elims)
-> ReaderT SearchOptions (TCMT IO) Args
-> ReaderT SearchOptions (TCMT IO) Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT SearchOptions (TCMT IO) Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  prettyTCM =<< instantiate (MetaV (goalMeta goal) args)

branchInstantiationDocCost :: SearchBranch -> SM Doc
branchInstantiationDocCost :: SearchBranch -> ReaderT SearchOptions (TCMT IO) Doc
branchInstantiationDocCost SearchBranch
branch = SearchBranch -> ReaderT SearchOptions (TCMT IO) Doc
branchInstantiationDoc SearchBranch
branch ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (ReaderT SearchOptions (TCMT IO) Doc
"cost:" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseLevel -> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (SearchBranch -> VerboseLevel
sbCost SearchBranch
branch))

-- | For debug
branchInstantiationDoc :: SearchBranch -> SM Doc
branchInstantiationDoc :: SearchBranch -> ReaderT SearchOptions (TCMT IO) Doc
branchInstantiationDoc SearchBranch
branch = SearchBranch
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall a. SearchBranch -> SM a -> SM a
withBranchState SearchBranch
branch ReaderT SearchOptions (TCMT IO) Doc
topInstantiationDoc

refine :: SearchBranch -> SM [SearchStepResult]
refine :: SearchBranch -> SM [SearchStepResult]
refine SearchBranch
branch = SearchBranch -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> SM a -> SM a
withBranchState SearchBranch
branch (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
  (goal1, branch1) <- SearchBranch -> SM (Goal, SearchBranch)
nextBranchMeta' SearchBranch
branch

  withBranchAndGoal branch1 goal1 $ do
    goalType1 <- bench [Bench.Reduce] $ reduce =<< getMetaTypeInContext (goalMeta goal1)

    mimerTrace 1 10 $ sep
      [ "Refining goal"
      , nest 2 $ prettyTCM (goalMeta goal1) <+> ":" <+> prettyTCM goalType1
      , nest 2 $ "in context" <+> (inTopContext . prettyTCM =<< getContextTelescope)
      ]

    reportSDoc "mimer.refine" 30 $ "Goal type:" <+> pretty goalType1
    reportSDoc "mimer.refine" 30 $ "Goal context:" <+> (pretty =<< getContextTelescope)

    -- Lambda-abstract as far as possible
    tryLamAbs goal1 goalType1 branch1 >>= \case
      -- Abstracted with absurd pattern: solution found.
      Left Expr
expr -> do
        ArgName
-> VerboseLevel
-> TCMT IO Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"mimer.refine" VerboseLevel
30 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
-> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Abstracted with absurd lambda. Result:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
expr
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Expr -> SearchStepResult
ResultExpr Expr
expr]
      -- Normal abstraction
      Right (Goal
goal2, Type
goalType2, SearchBranch
branch2) -> SearchBranch
-> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch2 Goal
goal2 (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
        (branch3, components) <- Goal
-> SearchBranch -> SM (SearchBranch, [(Component, [Component])])
prepareComponents Goal
goal2 SearchBranch
branch2
        withBranchAndGoal branch3 goal2 $ do

          when (goalMeta goal2 /= goalMeta goal1) $ do
            mimerTrace 1 10 $ sep
              [ "Lambda refinement", nest 2 $ prettyGoalInst goal1 ]
            mimerTrace 1 10 $ sep
              [ "Refining goal"
              , nest 2 $ prettyTCM (goalMeta goal2) <+> ":" <+> prettyTCM goalType2
              , nest 2 $ "in context" <+> (inTopContext . prettyTCM =<< getContextTelescope)
              ]

          mimerTrace 2 40 $ vcat
            [ "Components:"
            , nest 2 $ vcat $ map prettyTCM $ concatMap snd components
            ]

          results1 <- tryComponents goal2 goalType2 branch3 components
          results2 <- tryDataRecord goal2 goalType2 branch3
          return $ results1 ++ results2

tryFns :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryFns :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryFns Goal
goal Type
goalType SearchBranch
branch = SearchBranch
-> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
  ArgName
-> VerboseLevel
-> TCMT IO Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"mimer.refine.fn" VerboseLevel
50 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
-> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Trying functions"
  fns <- (SearchOptions -> [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (BaseComponents -> [Component]
hintFns (BaseComponents -> [Component])
-> (SearchOptions -> BaseComponents)
-> SearchOptions
-> [Component]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> BaseComponents
searchBaseComponents)
  newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) fns
  mapM checkSolved newBranches

tryProjs :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryProjs :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryProjs Goal
goal Type
goalType SearchBranch
branch = SearchBranch
-> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
  projs <- (SearchOptions -> [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (BaseComponents -> [Component]
hintProjections (BaseComponents -> [Component])
-> (SearchOptions -> BaseComponents)
-> SearchOptions
-> [Component]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> BaseComponents
searchBaseComponents)
  newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) projs
  mapM checkSolved newBranches

tryAxioms :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryAxioms :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryAxioms Goal
goal Type
goalType SearchBranch
branch = SearchBranch
-> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
  axioms <- (SearchOptions -> [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (BaseComponents -> [Component]
hintAxioms (BaseComponents -> [Component])
-> (SearchOptions -> BaseComponents)
-> SearchOptions
-> [Component]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> BaseComponents
searchBaseComponents)
  newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) axioms
  mapM checkSolved newBranches

tryLet :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryLet :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryLet Goal
goal Type
goalType SearchBranch
branch = SearchBranch
-> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
  letVars <- (SearchOptions -> [Open Component])
-> ReaderT SearchOptions (TCMT IO) [Open Component]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (BaseComponents -> [Open Component]
hintLetVars (BaseComponents -> [Open Component])
-> (SearchOptions -> BaseComponents)
-> SearchOptions
-> [Open Component]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> BaseComponents
searchBaseComponents) ReaderT SearchOptions (TCMT IO) [Open Component]
-> ([Open Component]
    -> ReaderT SearchOptions (TCMT IO) [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Open Component -> ReaderT SearchOptions (TCMT IO) Component)
-> [Open Component] -> ReaderT SearchOptions (TCMT IO) [Component]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Open Component -> ReaderT SearchOptions (TCMT IO) Component
forall (tcm :: * -> *).
MonadTCM tcm =>
Open Component -> tcm Component
getOpenComponent
  newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) letVars
  mapM checkSolved newBranches

-- | Returns @Right@ for normal lambda abstraction and @Left@ for absurd lambda.
tryLamAbs :: Goal -> Type -> SearchBranch -> SM (Either Expr (Goal, Type, SearchBranch))
tryLamAbs :: Goal
-> Type
-> SearchBranch
-> SM (Either Expr (Goal, Type, SearchBranch))
tryLamAbs Goal
goal Type
goalType SearchBranch
branch =
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
goalType of
    Pi Dom Type
dom Abs Type
abs -> do
     e <- Type -> SM Bool
isEmptyType (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom)
     isEmptyType (unDom dom) >>= \case -- TODO: Is this the correct way of checking if absurd lambda is applicable?
      Bool
True -> do
        let argInf :: ArgInfo
argInf = ArgInfo
defaultArgInfo{argInfoOrigin = Inserted} -- domInfo dom
            term :: Term
term = ArgInfo -> Abs Term -> Term
Lam ArgInfo
argInf Abs Term
absurdBody
        newMetaIds <- MetaId -> Term -> Type -> SM [MetaId]
assignMeta (Goal -> MetaId
goalMeta Goal
goal) Term
term Type
goalType
        unless (null newMetaIds) (__IMPOSSIBLE__)
        -- TODO: Represent absurd lambda as a Term instead of Expr.
        -- Left . fromMaybe __IMPOSSIBLE__ <$> getMetaInstantiation (goalMeta metaId)
        return $ Left $ AbsurdLam exprNoRange NotHidden
      Bool
False -> do
        let bindName :: ArgName
bindName | ArgName -> Bool
forall a. IsNoName a => a -> Bool
isNoName (Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
abs) = ArgName
"z"
                     | Bool
otherwise              = Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
abs
        newName <- ArgName -> ReaderT SearchOptions (TCMT IO) Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *). MonadFresh NameId m => ArgName -> m Name
freshName_ ArgName
bindName
        (metaId', bodyType, metaTerm, env) <- lambdaAddContext newName bindName dom $ do
          goalType' <- getMetaTypeInContext (goalMeta goal)
          bodyType <- bench [Bench.Reduce] $ reduce =<< piApplyM goalType' (Var 0 []) -- TODO: Good place to reduce?
          (metaId', metaTerm) <- bench [Bench.Free] $ newValueMeta DontRunMetaOccursCheck CmpLeq bodyType
          env <- askTC
          return (metaId', bodyType, metaTerm, env)

        let argInf = Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
dom -- TODO: is this the correct arg info?
            newAbs = Abs{absName :: ArgName
absName = ArgName
bindName, unAbs :: Term
unAbs = Term
metaTerm } --MetaV metaId' [] }
            -- look at mkLam
            term = ArgInfo -> Abs Term -> Term
Lam ArgInfo
argInf Abs Term
newAbs

        newMetaIds <- assignMeta (goalMeta goal) term goalType

        withEnv env $ do
          branch' <- updateBranch newMetaIds branch
          tryLamAbs (Goal metaId') bodyType branch'
    Term
_ -> do
      branch' <- [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch [] SearchBranch
branch -- TODO: Is this necessary?
      return $ Right (goal, goalType, branch')


genRecCalls :: Component -> SM [Component]
genRecCalls :: Component -> ReaderT SearchOptions (TCMT IO) [Component]
genRecCalls Component
thisFn = do
  -- TODO: Make sure there are no pruning problems
  (SearchOptions -> Open [(Term, NoSubst Term VerboseLevel)])
-> ReaderT
     SearchOptions (TCMT IO) (Open [(Term, NoSubst Term VerboseLevel)])
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (BaseComponents -> Open [(Term, NoSubst Term VerboseLevel)]
hintRecVars (BaseComponents -> Open [(Term, NoSubst Term VerboseLevel)])
-> (SearchOptions -> BaseComponents)
-> SearchOptions
-> Open [(Term, NoSubst Term VerboseLevel)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> BaseComponents
searchBaseComponents) ReaderT
  SearchOptions (TCMT IO) (Open [(Term, NoSubst Term VerboseLevel)])
-> (Open [(Term, NoSubst Term VerboseLevel)]
    -> ReaderT
         SearchOptions (TCMT IO) [(Term, NoSubst Term VerboseLevel)])
-> ReaderT
     SearchOptions (TCMT IO) [(Term, NoSubst Term VerboseLevel)]
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Open [(Term, NoSubst Term VerboseLevel)]
-> ReaderT
     SearchOptions (TCMT IO) [(Term, NoSubst Term VerboseLevel)]
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen ReaderT SearchOptions (TCMT IO) [(Term, NoSubst Term VerboseLevel)]
-> ([(Term, NoSubst Term VerboseLevel)]
    -> ReaderT SearchOptions (TCMT IO) [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    -- No candidate arguments for a recursive call
    [] -> [Component] -> ReaderT SearchOptions (TCMT IO) [Component]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    [(Term, NoSubst Term VerboseLevel)]
recCandTerms -> do
      Costs{..} <- (SearchOptions -> Costs) -> ReaderT SearchOptions (TCMT IO) Costs
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> Costs
searchCosts
      n <- localVarCount
      localVars <- lift $ getLocalVars n costLocal
      let recCands = [ (Component
t, VerboseLevel
i) | t :: Component
t@(Component -> Term
compTerm -> v :: Term
v@Var{}) <- [Component]
localVars, NoSubst VerboseLevel
i <- Maybe (NoSubst Term VerboseLevel) -> [NoSubst Term VerboseLevel]
forall a. Maybe a -> [a]
maybeToList (Maybe (NoSubst Term VerboseLevel) -> [NoSubst Term VerboseLevel])
-> Maybe (NoSubst Term VerboseLevel) -> [NoSubst Term VerboseLevel]
forall a b. (a -> b) -> a -> b
$ Term
-> [(Term, NoSubst Term VerboseLevel)]
-> Maybe (NoSubst Term VerboseLevel)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Term
v [(Term, NoSubst Term VerboseLevel)]
recCandTerms ]

      let newRecCall = do
            -- Apply the recursive call to new metas
            (thisFnTerm, thisFnType, newMetas) <- VerboseLevel -> Term -> Type -> SM (Term, Type, [MetaId])
applyToMetas VerboseLevel
0 (Component -> Term
compTerm Component
thisFn) (Component -> Type
compType Component
thisFn)
            let argGoals = (MetaId -> Goal) -> [MetaId] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map MetaId -> Goal
Goal [MetaId]
newMetas
            comp <- newComponent newMetas (compCost thisFn) (compName thisFn) 0 thisFnTerm thisFnType
            return (comp, zip argGoals [0..])

          -- go :: Component -- ^ Recursive call function applied to meta-variables
          --   -> [(Goal, Int)] -- ^ Remaining parameters to try to fill
          --   -> [(Component, Int)] -- ^ Remaining argument candidates for the current parameter
          --   -> SM [Component]
          go Component
_thisFn [] [(Component, VerboseLevel)]
_args = [Component] -> ReaderT SearchOptions (TCMT IO) [Component]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
          go Component
thisFn ((Goal, VerboseLevel)
_ : [(Goal, VerboseLevel)]
goals) [] = Component
-> [(Goal, VerboseLevel)]
-> [(Component, VerboseLevel)]
-> ReaderT SearchOptions (TCMT IO) [Component]
go Component
thisFn [(Goal, VerboseLevel)]
goals [(Component, VerboseLevel)]
recCands
          go Component
thisFn ((Goal
goal, VerboseLevel
i) : [(Goal, VerboseLevel)]
goals) ((Component
arg, VerboseLevel
j) : [(Component, VerboseLevel)]
args) | VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
j = do
            ArgName
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
reportSMDoc ArgName
"mimer.components.rec" VerboseLevel
80 (ReaderT SearchOptions (TCMT IO) Doc
 -> ReaderT SearchOptions (TCMT IO) ())
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [ReaderT SearchOptions (TCMT IO) Doc]
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
              [ ReaderT SearchOptions (TCMT IO) Doc
"Trying to generate recursive call"
              , Term -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Component -> Term
compTerm Component
thisFn)
              , ReaderT SearchOptions (TCMT IO) Doc
"with" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Component -> Term
compTerm Component
arg)
              , ReaderT SearchOptions (TCMT IO) Doc
"for" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM (Goal -> MetaId
goalMeta Goal
goal) ]
            goalType <- MetaId -> ReaderT SearchOptions (TCMT IO) Type
forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
 MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext (Goal -> MetaId
goalMeta Goal
goal)
            state <- getTC
            tryRefineWith' goal goalType arg >>= \case
              Maybe ([MetaId], [MetaId])
Nothing -> do
                TCState -> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
state
                Component
-> [(Goal, VerboseLevel)]
-> [(Component, VerboseLevel)]
-> ReaderT SearchOptions (TCMT IO) [Component]
go Component
thisFn ((Goal
goal, VerboseLevel
i) (Goal, VerboseLevel)
-> [(Goal, VerboseLevel)] -> [(Goal, VerboseLevel)]
forall a. a -> [a] -> [a]
: [(Goal, VerboseLevel)]
goals) [(Component, VerboseLevel)]
args
              Just ([MetaId]
newMetas1, [MetaId]
newMetas2) -> do
                let newComp :: Component
newComp = Component
thisFn{compMetas = newMetas1 ++ newMetas2 ++ (compMetas thisFn \\ [goalMeta goal])}
                (thisFn', goals') <- ReaderT SearchOptions (TCMT IO) (Component, [(Goal, VerboseLevel)])
newRecCall
                (newComp:) <$> go thisFn' (drop (length goals' - length goals - 1) goals') args
          go Component
thisFn [(Goal, VerboseLevel)]
goals ((Component, VerboseLevel)
_ : [(Component, VerboseLevel)]
args) = Component
-> [(Goal, VerboseLevel)]
-> [(Component, VerboseLevel)]
-> ReaderT SearchOptions (TCMT IO) [Component]
go Component
thisFn [(Goal, VerboseLevel)]
goals [(Component, VerboseLevel)]
args
      (thisFn', argGoals) <- newRecCall
      comps <- go thisFn' argGoals recCands
      -- Compute costs for the calls:
      --  - costNewMeta/costNewHiddenMeta for each unsolved argument
      --  - zero for solved arguments
      --  - costLocal for the parameter we recurse on
      let callCost Component
comp = (VerboseLevel
costLocal VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+) (VerboseLevel -> VerboseLevel)
-> ([VerboseLevel] -> VerboseLevel)
-> [VerboseLevel]
-> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VerboseLevel] -> VerboseLevel
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([VerboseLevel] -> VerboseLevel)
-> ReaderT SearchOptions (TCMT IO) [VerboseLevel]
-> SM VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReaderT SearchOptions (TCMT IO) [VerboseLevel]
argCosts (Component -> Term
compTerm Component
comp)
          argCosts (Def QName
_ Elims
elims) = (Elim' Term -> SM VerboseLevel)
-> Elims -> ReaderT SearchOptions (TCMT IO) [VerboseLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim' Term -> SM VerboseLevel
argCost Elims
elims
          argCosts Term
_ = ReaderT SearchOptions (TCMT IO) [VerboseLevel]
forall a. HasCallStack => a
__IMPOSSIBLE__
          argCost (Apply Arg Term
arg) = Arg Term -> ReaderT SearchOptions (TCMT IO) (Arg Term)
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Arg Term
arg ReaderT SearchOptions (TCMT IO) (Arg Term)
-> (Arg Term -> VerboseLevel) -> SM VerboseLevel
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ case
            Arg ArgInfo
h MetaV{} | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
h -> VerboseLevel
costNewMeta
                          | Bool
otherwise -> VerboseLevel
costNewHiddenMeta
            Arg Term
_ -> VerboseLevel
0
          argCost Proj{}   = VerboseLevel -> SM VerboseLevel
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VerboseLevel
0
          argCost IApply{} = VerboseLevel -> SM VerboseLevel
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VerboseLevel
0
      mapM (\ Component
c -> (VerboseLevel -> Component -> Component
`addCost` Component
c) (VerboseLevel -> Component)
-> SM VerboseLevel -> ReaderT SearchOptions (TCMT IO) Component
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Component -> SM VerboseLevel
callCost Component
c) comps


-- TODO: Factor out `checkSolved`
tryDataRecord :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryDataRecord :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryDataRecord Goal
goal Type
goalType SearchBranch
branch = SearchBranch
-> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
  -- TODO: There is a `isRecord` function, which performs a similar case
  -- analysis as here, but it does not work for data types.
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
goalType of
    Def QName
qname Elims
elims -> Definition -> Defn
theDef (Definition -> Defn)
-> ReaderT SearchOptions (TCMT IO) Definition
-> ReaderT SearchOptions (TCMT IO) Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ReaderT SearchOptions (TCMT IO) Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qname ReaderT SearchOptions (TCMT IO) Defn
-> (Defn -> SM [SearchStepResult]) -> SM [SearchStepResult]
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      recordDefn :: Defn
recordDefn@Record{} -> do
        Defn -> SM [SearchStepResult]
tryRecord Defn
recordDefn
      dataDefn :: Defn
dataDefn@Datatype{} -> do
        Defn -> SM [SearchStepResult]
tryData Defn
dataDefn
      primitive :: Defn
primitive@Primitive{} -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      -- TODO: Better way of checking that type is Level
      d :: Defn
d@Axiom{}
        | QName -> ArgName
forall a. Pretty a => a -> ArgName
P.prettyShow QName
qname ArgName -> ArgName -> Bool
forall a. Eq a => a -> a -> Bool
== ArgName
"Agda.Primitive.Level" -> do
            tryLevel
        | Bool
otherwise -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      d :: Defn
d@DataOrRecSig{} -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      d :: Defn
d@Defn
GeneralizableVar -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      d :: Defn
d@AbstractDefn{} -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      d :: Defn
d@Function{} -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      d :: Defn
d@Constructor{} -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      d :: Defn
d@PrimitiveSort{} -> do
        [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    sort :: Term
sort@(Sort (Type Level
level)) -> do
      Level -> SM [SearchStepResult]
trySet Level
level
    Sort Sort' Term
sort -> do
      [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Term
_ -> [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  where
      -- TODO: Alternatively, the constructor can be accessed via `getRecordConstructor`
      -- TODO: There might be a neater way of applying the constructor to new metas
    tryRecord :: Defn -> SM [SearchStepResult]
    tryRecord :: Defn -> SM [SearchStepResult]
tryRecord Defn
recordDefn = do
      cost <- (SearchOptions -> VerboseLevel) -> SM VerboseLevel
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Costs -> VerboseLevel
costRecordCon (Costs -> VerboseLevel)
-> (SearchOptions -> Costs) -> SearchOptions -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> Costs
searchCosts) -- TODO: Use lenses for this?
      comp <- qnameToComponent cost $ conName $ recConHead recordDefn
      -- NOTE: at most 1
      newBranches <- maybeToList <$> tryRefineAddMetas goal goalType branch comp
      mapM checkSolved newBranches

    tryData :: Defn -> SM [SearchStepResult]
    tryData :: Defn -> SM [SearchStepResult]
tryData Defn
dataDefn = do
      cost <- (SearchOptions -> VerboseLevel) -> SM VerboseLevel
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Costs -> VerboseLevel
costDataCon (Costs -> VerboseLevel)
-> (SearchOptions -> Costs) -> SearchOptions -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> Costs
searchCosts)
      comps <- mapM (qnameToComponent cost) $ dataCons dataDefn
      newBranches <- mapM (tryRefineAddMetas goal goalType branch) comps
      -- TODO: Reduce overlap between e.g. tryLocals, this and tryRecord
      mapM checkSolved (catMaybes newBranches)

    tryLevel :: SM [SearchStepResult]
    tryLevel :: SM [SearchStepResult]
tryLevel = do
      levelHints <- (SearchOptions -> [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (BaseComponents -> [Component]
hintLevel (BaseComponents -> [Component])
-> (SearchOptions -> BaseComponents)
-> SearchOptions
-> [Component]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> BaseComponents
searchBaseComponents)
      newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) levelHints
      mapM checkSolved newBranches

    -- TODO: Add an extra filtering on the sort
    trySet :: Level -> SM [SearchStepResult]
    trySet :: Level -> SM [SearchStepResult]
trySet Level
level = do
      reducedLevel <- Level -> ReaderT SearchOptions (TCMT IO) Level
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Level
level
      cost <- asks (costSet . searchCosts)
      setCandidates <- case reducedLevel of
        (Max Integer
i [])
          | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 -> do
              comp <- [MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> ReaderT SearchOptions (TCMT IO) Component
forall (m :: * -> *).
MonadFresh VerboseLevel m =>
[MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> m Component
newComponent [] VerboseLevel
cost Maybe Name
forall a. Maybe a
Nothing VerboseLevel
0 (Sort' Term -> Term
Sort (Sort' Term -> Term) -> Sort' Term -> Term
forall a b. (a -> b) -> a -> b
$ Level -> Sort' Term
forall t. Level' t -> Sort' t
Type (Level -> Sort' Term) -> Level -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) []) Type
goalType
              return [(branch, comp)]
          | Bool
otherwise -> [(SearchBranch, Component)]
-> ReaderT SearchOptions (TCMT IO) [(SearchBranch, Component)]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        (Max Integer
i [PlusLevel' Term]
ps) -> do
              (metaId, metaTerm) <- Type -> SM (MetaId, Term)
createMeta (Type -> SM (MetaId, Term))
-> ReaderT SearchOptions (TCMT IO) Type -> SM (MetaId, Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ReaderT SearchOptions (TCMT IO) Type
forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
levelType
              comp <- newComponent [metaId] cost Nothing 0 (Sort $ Type $ Max (max 0 (i - 1)) [Plus 0 metaTerm]) goalType
              branch' <- updateBranch [metaId] branch
              return [(branch', comp)]
      reportSDoc "mimer.refine.set" 40 $
        "Trying" <+> prettyTCM (map snd setCandidates) <+> "for" <+> prettyTCM goalType
      newBranches <- catMaybes <$> mapM (\(SearchBranch
br,Component
c) -> Goal
-> Type
-> SearchBranch
-> Component
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
tryRefineWith Goal
goal Type
goalType SearchBranch
br Component
c) setCandidates
      components <- asks searchBaseComponents
      newBranches' <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch)
                      (concatMap ($ components)
                       [ hintDataTypes
                       , hintRecordTypes
                       , hintAxioms])
      mapM checkSolved (newBranches ++ newBranches')

-- | Type should already be reduced here
-- NOTE: Does not reset the state!
-- TODO: Make sure the type is always reduced
tryRefineWith :: Goal -> Type -> SearchBranch -> Component -> SM (Maybe SearchBranch)
tryRefineWith :: Goal
-> Type
-> SearchBranch
-> Component
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
tryRefineWith Goal
goal Type
goalType SearchBranch
branch Component
comp = SearchBranch
-> Goal
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
 -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch))
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
forall a b. (a -> b) -> a -> b
$ do

  ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr, LocalMetaStores)
forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy (Type -> Type -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
dumbUnifierErr (Component -> Type
compType Component
comp) Type
goalType) ReaderT SearchOptions (TCMT IO) (Maybe TCErr, LocalMetaStores)
-> ((Maybe TCErr, LocalMetaStores)
    -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch))
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    (Maybe TCErr
Nothing, LocalMetaStores
newMetaStore) -> do
      (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
updateStat MimerStats -> MimerStats
incRefineSuccess
      -- TODO: Why is newMetaIds not used here?
      newMetaIds <- MetaId -> Term -> Type -> SM [MetaId]
assignMeta (Goal -> MetaId
goalMeta Goal
goal) (Component -> Term
compTerm Component
comp) Type
goalType
      let newMetaIds' = Map MetaId MetaVariable -> [MetaId]
forall k a. Map k a -> [k]
Map.keys (LocalMetaStores -> Map MetaId MetaVariable
openMetas LocalMetaStores
newMetaStore)
      reportSDoc "mimer.refine" 60 $
        "Refine: assignMeta created new metas:" <+> prettyTCM newMetaIds

      reportSMDoc "mimer.refine" 50 $ "Refinement succeeded"

      mimerTrace 2 10 $ sep
        [ "Found refinement"
        , nest 2 $ sep [ prettyTCM (compTerm comp)
                       , ":" <+> prettyTCM (compType comp) ] ]
      -- Take the metas stored in the component and add them as sub-goals
      Just <$> updateBranchCost comp (newMetaIds' ++ compMetas comp) branch
    (Just TCErr
err, LocalMetaStores
_) -> do
      (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
updateStat MimerStats -> MimerStats
incRefineFail
      ArgName
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
reportSMDoc ArgName
"mimer.refine" VerboseLevel
50 (ReaderT SearchOptions (TCMT IO) Doc
 -> ReaderT SearchOptions (TCMT IO) ())
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ ReaderT SearchOptions (TCMT IO) Doc
"Refinement failed"

      VerboseLevel
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
mimerTrace VerboseLevel
2 VerboseLevel
60 (ReaderT SearchOptions (TCMT IO) Doc
 -> ReaderT SearchOptions (TCMT IO) ())
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [ReaderT SearchOptions (TCMT IO) Doc]
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ ReaderT SearchOptions (TCMT IO) Doc
"Failed refinement"
        , VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (ReaderT SearchOptions (TCMT IO) Doc
 -> ReaderT SearchOptions (TCMT IO) Doc)
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$ [ReaderT SearchOptions (TCMT IO) Doc]
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Component -> Term
compTerm Component
comp)
                       , ReaderT SearchOptions (TCMT IO) Doc
":" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Component -> Type
compType Component
comp) ]
        , VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (ReaderT SearchOptions (TCMT IO) Doc
 -> ReaderT SearchOptions (TCMT IO) Doc)
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$ TCErr -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err ]
      Maybe SearchBranch
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SearchBranch
forall a. Maybe a
Nothing

tryRefineWith' :: Goal -> Type -> Component -> SM (Maybe ([MetaId], [MetaId]))
tryRefineWith' :: Goal -> Type -> Component -> SM (Maybe ([MetaId], [MetaId]))
tryRefineWith' Goal
goal Type
goalType Component
comp = do
  SM Bool -> ReaderT SearchOptions (TCMT IO) (Bool, LocalMetaStores)
forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy (Type -> Type -> SM Bool
dumbUnifier (Component -> Type
compType Component
comp) Type
goalType) ReaderT SearchOptions (TCMT IO) (Bool, LocalMetaStores)
-> ((Bool, LocalMetaStores) -> SM (Maybe ([MetaId], [MetaId])))
-> SM (Maybe ([MetaId], [MetaId]))
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    (Bool
True, LocalMetaStores
newMetaStore) -> do
      newMetaIds <- MetaId -> Term -> Type -> SM [MetaId]
assignMeta (Goal -> MetaId
goalMeta Goal
goal) (Component -> Term
compTerm Component
comp) Type
goalType
      let newMetaIds' = Map MetaId MetaVariable -> [MetaId]
forall k a. Map k a -> [k]
Map.keys (LocalMetaStores -> Map MetaId MetaVariable
openMetas LocalMetaStores
newMetaStore)
      return $ Just (newMetaIds, newMetaIds')
    (Bool
False, LocalMetaStores
_) -> Maybe ([MetaId], [MetaId]) -> SM (Maybe ([MetaId], [MetaId]))
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([MetaId], [MetaId])
forall a. Maybe a
Nothing

-- TODO: Make policy for when state should be put
tryRefineAddMetas :: Goal -> Type -> SearchBranch -> Component -> SM (Maybe SearchBranch)
tryRefineAddMetas :: Goal
-> Type
-> SearchBranch
-> Component
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
tryRefineAddMetas Goal
goal Type
goalType SearchBranch
branch Component
comp = SearchBranch
-> Goal
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
 -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch))
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
forall a b. (a -> b) -> a -> b
$ do
  -- Apply the hint to new metas (generating @c@, @c ?@, @c ? ?@, etc.)
  -- TODO: Where is the best place to reduce the hint type?
  comp' <- Maybe VerboseLevel
-> Component -> ReaderT SearchOptions (TCMT IO) Component
applyToMetasG Maybe VerboseLevel
forall a. Maybe a
Nothing Component
comp
  branch' <- updateBranch [] branch
  tryRefineWith goal goalType branch' comp'

-- TODO: Make sure the type is reduced the first time this is called
-- TODO: Rewrite with Component?
-- NOTE: The new metas are in left-to-right order -- the opposite of the
-- order they should be solved in.
applyToMetas :: Nat -> Term -> Type -> SM (Term, Type, [MetaId])
applyToMetas :: VerboseLevel -> Term -> Type -> SM (Term, Type, [MetaId])
applyToMetas VerboseLevel
skip Term
term Type
typ = do
  ctx <- ReaderT SearchOptions (TCMT IO) Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
  case unEl typ of
    Pi Dom Type
dom Abs Type
abs -> do
      let domainType :: Type
domainType = Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom
      -- TODO: What exactly does the occur check do?
      (metaId', metaTerm) <- [Phase] -> SM (MetaId, Term) -> SM (MetaId, Term)
forall a. NFData a => [Phase] -> SM a -> SM a
bench [Phase
Bench.Free] (SM (MetaId, Term) -> SM (MetaId, Term))
-> SM (MetaId, Term) -> SM (MetaId, Term)
forall a b. (a -> b) -> a -> b
$ RunMetaOccursCheck -> Comparison -> Type -> SM (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck Comparison
CmpLeq Type
domainType
      let arg = Origin -> Arg Term -> Arg Term
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term
metaTerm Term -> Arg Type -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
dom
      newType <- bench [Bench.Reduce] $ reduce =<< piApplyM typ metaTerm -- TODO: Is this the best place to reduce?
      -- For records, the parameters are not included in the term
      let newTerm = if VerboseLevel
skip VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0 then Term
term else Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
term [Arg Term
arg]
      (term', typ', metas) <- applyToMetas (predNat skip) newTerm newType
      return (term', typ', metaId' : metas)
    Term
_ -> (Term, Type, [MetaId]) -> SM (Term, Type, [MetaId])
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
term, Type
typ, [])

normaliseSolution :: Term -> SM Term
normaliseSolution :: Term -> ReaderT SearchOptions (TCMT IO) Term
normaliseSolution Term
t = do
  norm <- (SearchOptions -> Rewrite)
-> ReaderT SearchOptions (TCMT IO) Rewrite
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> Rewrite
searchRewrite
  lift . normalForm norm =<< instantiateFull t

checkSolved :: SearchBranch -> SM SearchStepResult
checkSolved :: SearchBranch -> ReaderT SearchOptions (TCMT IO) SearchStepResult
checkSolved SearchBranch
branch = do
  topMetaId <- (SearchOptions -> MetaId) -> ReaderT SearchOptions (TCMT IO) MetaId
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> MetaId
searchTopMeta
  topMeta <- lookupLocalMeta topMetaId
  ii <- asks searchInteractionId
  withInteractionId ii $ withBranchState branch $ do
    metaArgs <- getMetaContextArgs topMeta
    inst <- normaliseSolution $ apply (MetaV topMetaId []) metaArgs
    case allMetas (:[]) inst of
      [] -> Expr -> SearchStepResult
ResultExpr (Expr -> SearchStepResult)
-> ReaderT SearchOptions (TCMT IO) Expr
-> ReaderT SearchOptions (TCMT IO) SearchStepResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReaderT SearchOptions (TCMT IO) (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
inst
      [MetaId]
metaIds -> do
        SearchStepResult
-> ReaderT SearchOptions (TCMT IO) SearchStepResult
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SearchStepResult
 -> ReaderT SearchOptions (TCMT IO) SearchStepResult)
-> SearchStepResult
-> ReaderT SearchOptions (TCMT IO) SearchStepResult
forall a b. (a -> b) -> a -> b
$ SearchBranch -> SearchStepResult
OpenBranch (SearchBranch -> SearchStepResult)
-> SearchBranch -> SearchStepResult
forall a b. (a -> b) -> a -> b
$ SearchBranch
branch{sbGoals = map Goal $ reverse metaIds}

setAt :: Int -> a -> [a] -> [a]
setAt :: forall a. VerboseLevel -> a -> [a] -> [a]
setAt VerboseLevel
i a
x [a]
xs = case VerboseLevel -> [a] -> ([a], [a])
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt VerboseLevel
i [a]
xs of
  ([a]
ls, a
_r:[a]
rs) -> [a]
ls [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
rs)
  ([a], [a])
_ -> ArgName -> [a]
forall a. HasCallStack => ArgName -> a
error ArgName
"setAt: index out of bounds"

updateBranch' :: Maybe Component -> [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch' :: Maybe Component -> [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch' Maybe Component
mComp [MetaId]
newMetaIds SearchBranch
branch = do
  state <- ReaderT SearchOptions (TCMT IO) TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
  let compsUsed = SearchBranch -> Map Name VerboseLevel
sbComponentsUsed SearchBranch
branch
  (deltaCost, compsUsed') <- case mComp of
        Maybe Component
Nothing -> (VerboseLevel, Map Name VerboseLevel)
-> ReaderT
     SearchOptions (TCMT IO) (VerboseLevel, Map Name VerboseLevel)
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseLevel
0, Map Name VerboseLevel
compsUsed)
        Just Component
comp -> do
          case Component -> Maybe Name
compName Component
comp of
            Maybe Name
Nothing -> (VerboseLevel, Map Name VerboseLevel)
-> ReaderT
     SearchOptions (TCMT IO) (VerboseLevel, Map Name VerboseLevel)
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Component -> VerboseLevel
compCost Component
comp, Map Name VerboseLevel
compsUsed)
            Just Name
name -> case Map Name VerboseLevel
compsUsed Map Name VerboseLevel -> Name -> Maybe VerboseLevel
forall k a. Ord k => Map k a -> k -> Maybe a
Map.!? Name
name of
              Maybe VerboseLevel
Nothing -> (VerboseLevel, Map Name VerboseLevel)
-> ReaderT
     SearchOptions (TCMT IO) (VerboseLevel, Map Name VerboseLevel)
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Component -> VerboseLevel
compCost Component
comp, Name
-> VerboseLevel -> Map Name VerboseLevel -> Map Name VerboseLevel
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
name VerboseLevel
1 Map Name VerboseLevel
compsUsed)
              Just VerboseLevel
uses -> do
                reuseCost <- (SearchOptions -> VerboseLevel -> VerboseLevel)
-> ReaderT SearchOptions (TCMT IO) (VerboseLevel -> VerboseLevel)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Costs -> VerboseLevel -> VerboseLevel
costCompReuse (Costs -> VerboseLevel -> VerboseLevel)
-> (SearchOptions -> Costs)
-> SearchOptions
-> VerboseLevel
-> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> Costs
searchCosts)
                return (compCost comp + reuseCost uses, Map.adjust succ name compsUsed)
  return branch{ sbTCState = state
               , sbGoals = map Goal newMetaIds ++ sbGoals branch
               , sbCost = sbCost branch + deltaCost
               , sbComponentsUsed = compsUsed'
               }

updateBranch :: [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch :: [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch = Maybe Component -> [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch' Maybe Component
forall a. Maybe a
Nothing

updateBranchCost :: Component -> [MetaId] -> SearchBranch -> SM SearchBranch
updateBranchCost :: Component -> [MetaId] -> SearchBranch -> SM SearchBranch
updateBranchCost Component
comp = Maybe Component -> [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch' (Component -> Maybe Component
forall a. a -> Maybe a
Just Component
comp)

assignMeta :: MetaId -> Term -> Type -> SM [MetaId]
assignMeta :: MetaId -> Term -> Type -> SM [MetaId]
assignMeta MetaId
metaId Term
term Type
metaType = [Phase] -> SM [MetaId] -> SM [MetaId]
forall a. NFData a => [Phase] -> SM a -> SM a
bench [Phase
Bench.CheckRHS] (SM [MetaId] -> SM [MetaId]) -> SM [MetaId] -> SM [MetaId]
forall a b. (a -> b) -> a -> b
$ do
  ((), newMetaStore) <- ReaderT SearchOptions (TCMT IO) ()
-> ReaderT SearchOptions (TCMT IO) ((), LocalMetaStores)
forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy (ReaderT SearchOptions (TCMT IO) ()
 -> ReaderT SearchOptions (TCMT IO) ((), LocalMetaStores))
-> ReaderT SearchOptions (TCMT IO) ()
-> ReaderT SearchOptions (TCMT IO) ((), LocalMetaStores)
forall a b. (a -> b) -> a -> b
$ do
    metaVar <- MetaId -> ReaderT SearchOptions (TCMT IO) MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
metaId
    metaArgs <- getMetaContextArgs metaVar

    reportSMDoc "mimer.assignMeta" 60 $ vcat
      [ "Assigning" <+> pretty term
      , nest 2 $ vcat [ "to" <+> pretty metaId <+> ":" <+> pretty metaType
                      , "in context" <+> (pretty =<< getContextTelescope)
                      ]
      ]

    assignV DirLeq metaId metaArgs term (AsTermsOf metaType) `catchError` \TCErr
err -> do
      ArgName
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
reportSMDoc ArgName
"mimer.assignMeta" VerboseLevel
30 (ReaderT SearchOptions (TCMT IO) Doc
 -> ReaderT SearchOptions (TCMT IO) ())
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [ReaderT SearchOptions (TCMT IO) Doc]
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ ReaderT SearchOptions (TCMT IO) Doc
"Got error from assignV:" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCErr -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err
        , VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (ReaderT SearchOptions (TCMT IO) Doc
 -> ReaderT SearchOptions (TCMT IO) Doc)
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$ [ReaderT SearchOptions (TCMT IO) Doc]
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ ReaderT SearchOptions (TCMT IO) Doc
"when trying to assign" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
term
          , ReaderT SearchOptions (TCMT IO) Doc
"to" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
metaId ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ReaderT SearchOptions (TCMT IO) Doc
":" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
metaType
          , ReaderT SearchOptions (TCMT IO) Doc
"in context" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (ReaderT SearchOptions (TCMT IO) Doc
 -> ReaderT SearchOptions (TCMT IO) Doc)
-> (Telescope -> ReaderT SearchOptions (TCMT IO) Doc)
-> Telescope
-> ReaderT SearchOptions (TCMT IO) Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> ReaderT SearchOptions (TCMT IO) Doc)
-> ReaderT SearchOptions (TCMT IO) Telescope
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ReaderT SearchOptions (TCMT IO) Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
          ]
        ]

  let newMetaIds = Map MetaId MetaVariable -> [MetaId]
forall k a. Map k a -> [k]
Map.keys (LocalMetaStores -> Map MetaId MetaVariable
openMetas LocalMetaStores
newMetaStore)
  return newMetaIds

dumbUnifier :: Type -> Type -> SM Bool
dumbUnifier :: Type -> Type -> SM Bool
dumbUnifier Type
t1 Type
t2 = Maybe TCErr -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe TCErr -> Bool)
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr) -> SM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Type -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
dumbUnifierErr Type
t1 Type
t2

dumbUnifierErr :: Type -> Type -> SM (Maybe TCErr)
dumbUnifierErr :: Type -> Type -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
dumbUnifierErr Type
t1 Type
t2 = [Phase]
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
forall a. NFData a => [Phase] -> SM a -> SM a
bench [Phase
Bench.UnifyIndices] (ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
 -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr))
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
forall a b. (a -> b) -> a -> b
$ do
  (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
updateStat MimerStats -> MimerStats
incTypeEqChecks
  ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (Maybe TCErr
forall a. Maybe a
Nothing Maybe TCErr
-> ReaderT SearchOptions (TCMT IO) ()
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
forall a b.
a
-> ReaderT SearchOptions (TCMT IO) b
-> ReaderT SearchOptions (TCMT IO) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type -> Type -> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
t2 Type
t1) ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
-> (TCErr -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr))
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
forall a.
ReaderT SearchOptions (TCMT IO) a
-> (TCErr -> ReaderT SearchOptions (TCMT IO) a)
-> ReaderT SearchOptions (TCMT IO) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
err -> do
    ArgName
-> VerboseLevel
-> TCMT IO Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"mimer.unify" VerboseLevel
80 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
-> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Unification failed with error:", VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCErr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err ]
    Maybe TCErr -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TCErr -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr))
-> Maybe TCErr -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
forall a b. (a -> b) -> a -> b
$ TCErr -> Maybe TCErr
forall a. a -> Maybe a
Just TCErr
err

-- Duplicate of a local definition in Agda.Interaction.BasicOps
showTCM :: (MonadPretty tcm, PrettyTCM a) => a -> tcm String
showTCM :: forall (tcm :: * -> *) a.
(MonadPretty tcm, PrettyTCM a) =>
a -> tcm ArgName
showTCM a
v = Doc -> ArgName
forall a. Doc a -> ArgName
P.render (Doc -> ArgName) -> tcm Doc -> tcm ArgName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> tcm Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
v

bench :: NFData a => [Bench.Phase] -> SM a -> SM a
bench :: forall a. NFData a => [Phase] -> SM a -> SM a
bench [Phase]
k SM a
ma = Account (BenchPhase (ReaderT SearchOptions (TCMT IO)))
-> SM a -> SM a
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
billTo (Phase
mimerAccount Phase -> [Phase] -> [Phase]
forall a. a -> [a] -> [a]
: [Phase]
k) SM a
ma
  where
    -- Dummy account to avoid updating Bench. Doesn't matter since this is only used interactively
    -- to debug Mimer performance.
    mimerAccount :: Phase
mimerAccount = Phase
Bench.Sort

-- Local variables:
-- getContext :: MonadTCEnv m => m [Dom (Name, Type)]
-- getContextArgs :: (Applicative m, MonadTCEnv m) => m Args
-- getContextTelescope :: (Applicative m, MonadTCEnv m) => m Telescope
-- getContextTerms :: (Applicative m, MonadTCEnv m) => m [Term]
getLocalVars :: Int -> Cost -> TCM [Component]
getLocalVars :: VerboseLevel -> VerboseLevel -> TCMT IO [Component]
getLocalVars VerboseLevel
localCxt VerboseLevel
cost = do
  typedTerms <- VerboseLevel -> TCM [(Term, Dom Type)]
getLocalVarTerms VerboseLevel
localCxt
  let varZeroDiscount (Var VerboseLevel
0 []) = a
1
      varZeroDiscount Term
_          = a
0
  mapM (\(Term
term, Dom Type
domTyp) -> [MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> TCMT IO Component
forall (m :: * -> *).
MonadFresh VerboseLevel m =>
[MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> m Component
newComponent [] (VerboseLevel
cost VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- Term -> VerboseLevel
forall {a}. Num a => Term -> a
varZeroDiscount Term
term) Maybe Name
noName VerboseLevel
0 Term
term (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
domTyp)) typedTerms

getLocalVarTerms :: Int -> TCM [(Term, Dom Type)]
getLocalVarTerms :: VerboseLevel -> TCM [(Term, Dom Type)]
getLocalVarTerms VerboseLevel
localCxt = do
  contextTerms <- TCMT IO [Term]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Term]
getContextTerms
  contextTypes <- flattenTel <$> getContextTelescope
  let inScope VerboseLevel
i ContextEntry
_ | VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
< VerboseLevel
localCxt = Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True   -- Ignore scope for variables we inserted ourselves
      inScope VerboseLevel
_ Dom{ unDom :: forall t e. Dom' t e -> e
unDom = (Name
name, Type
_) } = do
        x <- Name -> TCMT IO (ConOfAbs Name)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ Name
name
        pure $ C.isInScope x == C.InScope
  scope <- mapM (uncurry inScope) . reverse . zip [0..] =<< getContext
  return [ e | (True, e) <- zip scope $ zip contextTerms contextTypes ]



prettyBranch :: SearchBranch -> SM String
prettyBranch :: SearchBranch -> ReaderT SearchOptions (TCMT IO) ArgName
prettyBranch SearchBranch
branch = SearchBranch
-> ReaderT SearchOptions (TCMT IO) ArgName
-> ReaderT SearchOptions (TCMT IO) ArgName
forall a. SearchBranch -> SM a -> SM a
withBranchState SearchBranch
branch (ReaderT SearchOptions (TCMT IO) ArgName
 -> ReaderT SearchOptions (TCMT IO) ArgName)
-> ReaderT SearchOptions (TCMT IO) ArgName
-> ReaderT SearchOptions (TCMT IO) ArgName
forall a b. (a -> b) -> a -> b
$ do
    metaId <- (SearchOptions -> MetaId) -> ReaderT SearchOptions (TCMT IO) MetaId
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> MetaId
searchTopMeta
    P.render <$> "Branch" <> braces (sep $ punctuate ","
      [ "cost:" <+> pretty (sbCost branch)
      , "metas:" <+> prettyTCM (map goalMeta (sbGoals branch))
      , sep [ "instantiation:"
            , nest 2 $ pretty metaId <+> "=" <+> (prettyTCM =<< getMetaInstantiation metaId) ]
      , "used components:" <+> pretty (Map.toList $ sbComponentsUsed branch)
      ])


instance Pretty Goal where
  pretty :: Goal -> Doc
pretty Goal
goal = MetaId -> Doc
forall a. Pretty a => a -> Doc
P.pretty (MetaId -> Doc) -> MetaId -> Doc
forall a b. (a -> b) -> a -> b
$ Goal -> MetaId
goalMeta Goal
goal

instance Pretty SearchBranch where
  pretty :: SearchBranch -> Doc
pretty SearchBranch
branch = [(Doc, Doc)] -> Doc
keyValueList
    [ (Doc
"sbTCState", Doc
"[...]")
    , (Doc
"sbGoals", [Goal] -> Doc
forall a. Pretty a => a -> Doc
P.pretty ([Goal] -> Doc) -> [Goal] -> Doc
forall a b. (a -> b) -> a -> b
$ SearchBranch -> [Goal]
sbGoals SearchBranch
branch)
    , (Doc
"sbCost", VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ SearchBranch -> VerboseLevel
sbCost SearchBranch
branch)
    , (Doc
"sbComponentsUsed", Map Name VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Map Name VerboseLevel -> Doc) -> Map Name VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ SearchBranch -> Map Name VerboseLevel
sbComponentsUsed SearchBranch
branch)
    ]


instance PrettyTCM BaseComponents where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => BaseComponents -> m Doc
prettyTCM BaseComponents
comps = do
    let thisFn :: m Doc
thisFn = case BaseComponents -> Maybe Component
hintThisFn BaseComponents
comps of
          Maybe Component
Nothing -> m Doc
"(nothing)"
          Just Component
comp -> Component -> m Doc
forall {m :: * -> *}.
(Applicative m, IsString (m Doc)) =>
Component -> m Doc
prettyComp Component
comp
    [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ m Doc
"Base components:"
         , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
           [ m Doc -> [Component] -> m Doc
f m Doc
"hintFns" (BaseComponents -> [Component]
hintFns BaseComponents
comps)
           , m Doc -> [Component] -> m Doc
f m Doc
"hintDataTypes" (BaseComponents -> [Component]
hintDataTypes BaseComponents
comps)
           , m Doc -> [Component] -> m Doc
f m Doc
"hintRecordTypes" (BaseComponents -> [Component]
hintRecordTypes BaseComponents
comps)
           , m Doc -> [Component] -> m Doc
f m Doc
"hintAxioms" (BaseComponents -> [Component]
hintAxioms BaseComponents
comps)
           , m Doc -> [Component] -> m Doc
f m Doc
"hintLevel" (BaseComponents -> [Component]
hintLevel BaseComponents
comps)
           , m Doc -> [Component] -> m Doc
f m Doc
"hintProjections" (BaseComponents -> [Component]
hintProjections BaseComponents
comps)
           , m Doc
"hintThisFn:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
thisFn
           , (Open Component -> m Doc) -> m Doc -> [Open Component] -> m Doc
forall {m :: * -> *} {a}.
(Semigroup (m Doc), IsString (m Doc), Applicative m) =>
(a -> m Doc) -> m Doc -> [a] -> m Doc
g Open Component -> m Doc
forall {m :: * -> *}.
(Applicative m, IsString (m Doc)) =>
Open Component -> m Doc
prettyOpenComp m Doc
"hintLetVars" (BaseComponents -> [Open Component]
hintLetVars BaseComponents
comps)
           , m Doc
"hintRecVars: Open" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [(Term, VerboseLevel)] -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ((NoSubst Term VerboseLevel -> VerboseLevel)
-> (Term, NoSubst Term VerboseLevel) -> (Term, VerboseLevel)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd NoSubst Term VerboseLevel -> VerboseLevel
forall t a. NoSubst t a -> a
unNoSubst ((Term, NoSubst Term VerboseLevel) -> (Term, VerboseLevel))
-> [(Term, NoSubst Term VerboseLevel)] -> [(Term, VerboseLevel)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Open [(Term, NoSubst Term VerboseLevel)]
-> [(Term, NoSubst Term VerboseLevel)]
forall a. Open a -> a
openThing (BaseComponents -> Open [(Term, NoSubst Term VerboseLevel)]
hintRecVars BaseComponents
comps))
           , m Doc
"hintSplitVars: Open" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Open [Term] -> [Term]
forall a. Open a -> a
openThing (Open [Term] -> [Term]) -> Open [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ BaseComponents -> Open [Term]
hintSplitVars BaseComponents
comps)
           ]
         ]
    where
      prettyComp :: Component -> m Doc
prettyComp Component
comp = Term -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Component -> Term
compTerm Component
comp) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Component -> Type
compType Component
comp)
      prettyOpenComp :: Open Component -> m Doc
prettyOpenComp Open Component
openComp = m Doc
"Open" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (Component -> m Doc
forall {m :: * -> *}.
(Applicative m, IsString (m Doc)) =>
Component -> m Doc
prettyComp (Component -> m Doc) -> Component -> m Doc
forall a b. (a -> b) -> a -> b
$ Open Component -> Component
forall a. Open a -> a
openThing Open Component
openComp)
      prettyTCMComp :: Component -> m Doc
prettyTCMComp Component
comp = Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Component -> Term
compTerm Component
comp) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Component -> Type
compType Component
comp)
      f :: m Doc -> [Component] -> m Doc
f = (Component -> m Doc) -> m Doc -> [Component] -> m Doc
forall {m :: * -> *} {a}.
(Semigroup (m Doc), IsString (m Doc), Applicative m) =>
(a -> m Doc) -> m Doc -> [a] -> m Doc
g Component -> m Doc
forall {m :: * -> *}.
(MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc)) =>
Component -> m Doc
prettyTCMComp
      g :: (a -> m Doc) -> m Doc -> [a] -> m Doc
g a -> m Doc
p m Doc
n [] = m Doc
n m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
": []"
      g a -> m Doc
p m Doc
n [a]
xs = (m Doc
n m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
":") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$ VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (a -> m Doc) -> [a] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Doc
p [a]
xs)


-- -- TODO: Is it possible to derive the pretty instances?
instance Pretty BaseComponents where
  pretty :: BaseComponents -> Doc
pretty BaseComponents
comps = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat
      [ Doc -> [Component] -> Doc
forall {a}. Pretty a => Doc -> [a] -> Doc
f Doc
"hintFns" (BaseComponents -> [Component]
hintFns BaseComponents
comps)
      , Doc -> [Component] -> Doc
forall {a}. Pretty a => Doc -> [a] -> Doc
f Doc
"hintDataTypes" (BaseComponents -> [Component]
hintDataTypes BaseComponents
comps)
      , Doc -> [Component] -> Doc
forall {a}. Pretty a => Doc -> [a] -> Doc
f Doc
"hintRecordTypes" (BaseComponents -> [Component]
hintRecordTypes BaseComponents
comps)
      , Doc -> [Component] -> Doc
forall {a}. Pretty a => Doc -> [a] -> Doc
f Doc
"hintAxioms" (BaseComponents -> [Component]
hintAxioms BaseComponents
comps)
      , Doc -> [Component] -> Doc
forall {a}. Pretty a => Doc -> [a] -> Doc
f Doc
"hintLevel" (BaseComponents -> [Component]
hintLevel BaseComponents
comps)
      , Doc -> [Component] -> Doc
forall {a}. Pretty a => Doc -> [a] -> Doc
f Doc
"hintProjections" (BaseComponents -> [Component]
hintProjections BaseComponents
comps)
      ]
    where
      f :: Doc -> [a] -> Doc
f Doc
n [] = Doc
n Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Doc
": []"
      f Doc
n [a]
xs = (Doc
n Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Doc
":") Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.$$ VerboseLevel -> Doc -> Doc
forall a. VerboseLevel -> Doc a -> Doc a
P.nest VerboseLevel
2 ([a] -> Doc
forall a. Pretty a => a -> Doc
P.pretty [a]
xs)

instance Pretty SearchOptions where
  pretty :: SearchOptions -> Doc
pretty SearchOptions
opts = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat
    [ Doc
"searchBaseComponents:"
    , VerboseLevel -> Doc -> Doc
forall a. VerboseLevel -> Doc a -> Doc a
P.nest VerboseLevel
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ BaseComponents -> Doc
forall a. Pretty a => a -> Doc
P.pretty (BaseComponents -> Doc) -> BaseComponents -> Doc
forall a b. (a -> b) -> a -> b
$ SearchOptions -> BaseComponents
searchBaseComponents SearchOptions
opts
    , [(Doc, Doc)] -> Doc
keyValueList
      [ (Doc
"searchHintMode", HintMode -> Doc
forall a. Pretty a => a -> Doc
P.pretty (HintMode -> Doc) -> HintMode -> Doc
forall a b. (a -> b) -> a -> b
$ SearchOptions -> HintMode
searchHintMode SearchOptions
opts)
      , (Doc
"searchTimeout",  Integer -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Integer -> Doc) -> Integer -> Doc
forall a b. (a -> b) -> a -> b
$ SearchOptions -> Integer
searchTimeout SearchOptions
opts)
      , (Doc
"searchTopMeta",  MetaId -> Doc
forall a. Pretty a => a -> Doc
P.pretty (MetaId -> Doc) -> MetaId -> Doc
forall a b. (a -> b) -> a -> b
$ SearchOptions -> MetaId
searchTopMeta SearchOptions
opts)
      , (Doc
"searchTopEnv", Doc
"[...]")
      ]
    , Doc
"searchCosts:"
    , VerboseLevel -> Doc -> Doc
forall a. VerboseLevel -> Doc a -> Doc a
P.nest VerboseLevel
2 (Costs -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Costs -> Doc) -> Costs -> Doc
forall a b. (a -> b) -> a -> b
$ SearchOptions -> Costs
searchCosts SearchOptions
opts)
    ]

instance PrettyTCM SearchOptions where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => SearchOptions -> m Doc
prettyTCM SearchOptions
opts = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ m Doc
"searchBaseComponents:"
    , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ BaseComponents -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => BaseComponents -> m Doc
prettyTCM (BaseComponents -> m Doc) -> BaseComponents -> m Doc
forall a b. (a -> b) -> a -> b
$ SearchOptions -> BaseComponents
searchBaseComponents SearchOptions
opts
    , [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ m Doc
"searchHintMode:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> HintMode -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (SearchOptions -> HintMode
searchHintMode SearchOptions
opts)
      , m Doc
"searchTimeout:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Integer -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (SearchOptions -> Integer
searchTimeout SearchOptions
opts)
      , m Doc
"searchTopMeta:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM (SearchOptions -> MetaId
searchTopMeta SearchOptions
opts)
      , m Doc
"searchTopEnv: [...]"
      , m Doc
"searchTopCheckpoint:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> CheckpointId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CheckpointId -> m Doc
prettyTCM (SearchOptions -> CheckpointId
searchTopCheckpoint SearchOptions
opts)
      , m Doc
"searchInteractionId:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> InteractionId -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (SearchOptions -> InteractionId
searchInteractionId SearchOptions
opts)
      , m Doc
"searchFnName:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Maybe QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (SearchOptions -> Maybe QName
searchFnName SearchOptions
opts)
      , m Doc
"searchStats: [...]"
      ]
    , m Doc
"searchCosts:"
    , VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Costs -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Costs -> m Doc) -> Costs -> m Doc
forall a b. (a -> b) -> a -> b
$ SearchOptions -> Costs
searchCosts SearchOptions
opts
    ]

instance Pretty Component where
  pretty :: Component -> Doc
pretty Component
comp = Doc -> [(Doc, Doc)] -> Doc
haskellRecord Doc
"Component"
    [ (Doc
"compId", VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Component -> VerboseLevel
compId Component
comp)
    , (Doc
"compTerm", Term -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Term -> Doc) -> Term -> Doc
forall a b. (a -> b) -> a -> b
$ Component -> Term
compTerm Component
comp)
    , (Doc
"compType", Type -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ Component -> Type
compType Component
comp)
    , (Doc
"compMetas", [MetaId] -> Doc
forall a. Pretty a => a -> Doc
P.pretty ([MetaId] -> Doc) -> [MetaId] -> Doc
forall a b. (a -> b) -> a -> b
$ Component -> [MetaId]
compMetas Component
comp)
    , (Doc
"compCost", VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Component -> VerboseLevel
compCost Component
comp)
    ]

instance Pretty Costs where
  pretty :: Costs -> Doc
pretty Costs
costs = VerboseLevel -> [(ArgName, Doc)] -> Doc
P.align VerboseLevel
20 [(ArgName, Doc)]
entries
    where
      entries :: [(ArgName, Doc)]
entries =
        [ (ArgName
"costLocal:"         , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costLocal Costs
costs)
        , (ArgName
"costFn:"            , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costFn Costs
costs)
        , (ArgName
"costDataCon:"       , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costDataCon Costs
costs)
        , (ArgName
"costRecordCon:"     , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costRecordCon Costs
costs)
        , (ArgName
"costSpeculateProj:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costSpeculateProj Costs
costs)
        , (ArgName
"costProj:"          , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costProj Costs
costs)
        , (ArgName
"costAxiom:"         , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costAxiom Costs
costs)
        , (ArgName
"costLet:"           , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costLet Costs
costs)
        , (ArgName
"costLevel:"         , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costLevel Costs
costs)
        , (ArgName
"costSet:"           , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costSet Costs
costs)
        , (ArgName
"costRecCall:"       , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costRecCall Costs
costs)
        , (ArgName
"costNewMeta:"       , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costNewMeta Costs
costs)
        , (ArgName
"costNewHiddenMeta:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costNewHiddenMeta Costs
costs)
        , (ArgName
"costCompReuse:"     , Doc
"{function}")
        ]

instance PrettyTCM Component where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Component -> m Doc
prettyTCM Component{Bool
VerboseLevel
[MetaId]
Maybe Name
Type
Term
compId :: Component -> VerboseLevel
compName :: Component -> Maybe Name
compPars :: Component -> VerboseLevel
compTerm :: Component -> Term
compType :: Component -> Type
compRec :: Component -> Bool
compMetas :: Component -> [MetaId]
compCost :: Component -> VerboseLevel
compId :: VerboseLevel
compName :: Maybe Name
compPars :: VerboseLevel
compTerm :: Term
compType :: Type
compRec :: Bool
compMetas :: [MetaId]
compCost :: VerboseLevel
..} = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (VerboseLevel -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => VerboseLevel -> m Doc
prettyTCM VerboseLevel
compId) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
compTerm
          , m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
compType ]
    , m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
","
      [ m Doc
"cost:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseLevel -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => VerboseLevel -> m Doc
prettyTCM VerboseLevel
compCost
      , m Doc
"metas:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [MetaId] -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [MetaId] -> m Doc
prettyTCM [MetaId]
compMetas
      ]
    ]

instance PrettyTCM MimerResult where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => MimerResult -> m Doc
prettyTCM = \case
    MimerExpr ArgName
expr    -> ArgName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ArgName
expr
    MimerClauses QName
f [Clause]
cl -> m Doc
"MimerClauses" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
f m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"[..]" -- TODO: display the clauses
    MimerResult
MimerNoResult     -> m Doc
"MimerNoResult"
    MimerList [(VerboseLevel, ArgName)]
sols    -> m Doc
"MimerList" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [(VerboseLevel, ArgName)] -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [(VerboseLevel, ArgName)]
sols

concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM :: forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM a -> m [b]
f = ([[b]] -> [b]) -> m [[b]] -> m [b]
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[b]] -> [b]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (m [[b]] -> m [b]) -> ([a] -> m [[b]]) -> [a] -> m [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m [b]) -> [a] -> m [[b]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM a -> m [b]
f

reportSMDoc :: VerboseKey -> VerboseLevel -> SM Doc -> SM ()
reportSMDoc :: ArgName
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
reportSMDoc ArgName
vk VerboseLevel
vl ReaderT SearchOptions (TCMT IO) Doc
md = ArgName
-> VerboseLevel
-> TCMT IO Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
vk VerboseLevel
vl (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
-> (SearchOptions -> TCMT IO Doc)
-> SearchOptions
-> ReaderT SearchOptions (TCMT IO) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReaderT SearchOptions (TCMT IO) Doc -> SearchOptions -> TCMT IO Doc
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT SearchOptions (TCMT IO) Doc
md (SearchOptions -> ReaderT SearchOptions (TCMT IO) ())
-> ReaderT SearchOptions (TCMT IO) SearchOptions
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ReaderT SearchOptions (TCMT IO) SearchOptions
forall r (m :: * -> *). MonadReader r m => m r
ask

mimerTrace :: Int -> VerboseLevel -> SM Doc -> SM ()
mimerTrace :: VerboseLevel
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
mimerTrace VerboseLevel
ilvl VerboseLevel
vlvl ReaderT SearchOptions (TCMT IO) Doc
doc = ArgName
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
reportSMDoc ArgName
"mimer.trace" VerboseLevel
vlvl (ReaderT SearchOptions (TCMT IO) Doc
 -> ReaderT SearchOptions (TCMT IO) ())
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest (VerboseLevel
2 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
* VerboseLevel
ilvl) (ReaderT SearchOptions (TCMT IO) Doc
 -> ReaderT SearchOptions (TCMT IO) Doc)
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$ ReaderT SearchOptions (TCMT IO) Doc
"-" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ReaderT SearchOptions (TCMT IO) Doc
doc

haskellRecord :: Doc -> [(Doc, Doc)] -> Doc
haskellRecord :: Doc -> [(Doc, Doc)] -> Doc
haskellRecord Doc
name [(Doc, Doc)]
fields = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.sep [ Doc
name, VerboseLevel -> Doc -> Doc
forall a. VerboseLevel -> Doc a -> Doc a
P.nest VerboseLevel
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
P.braces ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
P.punctuate Doc
"," [ Doc -> VerboseLevel -> Doc -> Doc
forall a. Doc a -> VerboseLevel -> Doc a -> Doc a
P.hang (Doc
k Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> Doc
"=") VerboseLevel
2 Doc
v | (Doc
k, Doc
v) <- [(Doc, Doc)]
fields ]) ]

keyValueList :: [(Doc, Doc)] -> Doc
keyValueList :: [(Doc, Doc)] -> Doc
keyValueList [(Doc, Doc)]
kvs = Doc -> Doc
P.braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
P.punctuate Doc
"," [ Doc -> VerboseLevel -> Doc -> Doc
forall a. Doc a -> VerboseLevel -> Doc a -> Doc a
P.hang (Doc
k Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Doc
":") VerboseLevel
2 Doc
v | (Doc
k, Doc
v) <- [(Doc, Doc)]
kvs ]

writeTime :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCM m, MonadDebug m) => InteractionId -> Maybe CPUTime -> m ()
writeTime :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCM m,
 MonadDebug m) =>
InteractionId -> Maybe CPUTime -> m ()
writeTime InteractionId
ii Maybe CPUTime
mTime = do
  let time :: ArgName
time = case Maybe CPUTime
mTime of
        Maybe CPUTime
Nothing -> ArgName
"n/a"
        Just (CPUTime Integer
t) -> Integer -> ArgName
forall a. Show a => a -> ArgName
show Integer
t
  file <- Range -> SrcFile
rangeFile (Range -> SrcFile)
-> (InteractionPoint -> Range) -> InteractionPoint -> SrcFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoint -> Range
ipRange (InteractionPoint -> SrcFile) -> m InteractionPoint -> m SrcFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionId -> m InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
  case file of
    SrcFile
SMaybe.Nothing ->
      ArgName -> VerboseLevel -> ArgName -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> ArgName -> m ()
reportSLn ArgName
"mimer.stats" VerboseLevel
2 ArgName
"No file found for interaction id"
    SMaybe.Just RangeFile
file -> do
      let path :: ArgName
path = AbsolutePath -> ArgName
filePath (RangeFile -> AbsolutePath
rangeFilePath RangeFile
file) ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
".stats"
      IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ ArgName -> ArgName -> IO ()
appendFile ArgName
path (VerboseLevel -> ArgName
forall a. Show a => a -> ArgName
show (InteractionId -> VerboseLevel
interactionId InteractionId
ii) ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
time ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
"\n")

-- Hack to let you experiment with costs using verbosity flags.
customCosts :: TCM Costs
customCosts :: TCMT IO Costs
customCosts = do
  costLocal         <- ArgName -> TCM VerboseLevel
forall {m :: * -> *}. MonadDebug m => ArgName -> m VerboseLevel
cost ArgName
"local"
  costFn            <- cost "fn"
  costDataCon       <- cost "dataCon"
  costRecordCon     <- cost "recordCon"
  costSpeculateProj <- cost "speculateProj"
  costProj          <- cost "proj"
  costAxiom         <- cost "axiom"
  costLet           <- cost "let"
  costLevel         <- cost "level"
  costSet           <- cost "set"
  costRecCall       <- cost "recCall"
  costNewMeta       <- cost "newMeta"
  costNewHiddenMeta <- cost "newHiddenMeta"
  compReuse         <- cost "compReuse"
  let costCompReuse VerboseLevel
uses = VerboseLevel
compReuse VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
* VerboseLevel
uses VerboseLevel -> Integer -> VerboseLevel
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
2
  pure Costs{..}
  where
    cost :: ArgName -> m VerboseLevel
cost ArgName
key = ArgName -> m VerboseLevel
forall {m :: * -> *}. MonadDebug m => ArgName -> m VerboseLevel
getVerbosityLevel (ArgName
"mimer-cost." ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
key)

getVerbosityLevel :: MonadDebug m => VerboseKey -> m VerboseLevel
getVerbosityLevel :: forall {m :: * -> *}. MonadDebug m => ArgName -> m VerboseLevel
getVerbosityLevel ArgName
k = do
  t <- m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
  return $ case t of
    Verbosity
Strict.Nothing -> VerboseLevel
1
    Strict.Just Trie VerboseKeyItem VerboseLevel
t
      | Trie VerboseKeyItem VerboseLevel
t Trie VerboseKeyItem VerboseLevel
-> Trie VerboseKeyItem VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== [VerboseKeyItem]
-> VerboseLevel -> Trie VerboseKeyItem VerboseLevel
forall k v. [k] -> v -> Trie k v
Trie.singleton [] VerboseLevel
0 -> VerboseLevel
0
      | Bool
otherwise -> VerboseLevel -> [VerboseLevel] -> VerboseLevel
forall a. a -> [a] -> a
lastWithDefault VerboseLevel
0 ([VerboseLevel] -> VerboseLevel) -> [VerboseLevel] -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ [VerboseKeyItem]
-> Trie VerboseKeyItem VerboseLevel -> [VerboseLevel]
forall k v. Ord k => [k] -> Trie k v -> [v]
Trie.lookupPath [VerboseKeyItem]
ks Trie VerboseKeyItem VerboseLevel
t
  where ks :: [VerboseKeyItem]
ks = ArgName -> [VerboseKeyItem]
parseVerboseKey ArgName
k