module Agda.Mimer.Types where

import Control.DeepSeq (NFData)
import Data.Function (on)
import Data.Map (Map)
import Data.List qualified as List
import GHC.Generics (Generic)
import Data.IORef (IORef)

import Agda.Syntax.Abstract (Expr)
import Agda.Syntax.Common.Pretty qualified as P
import Agda.Syntax.Common.Pretty (Pretty)
import Agda.Syntax.Common (InteractionId, Nat)
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad (TCState, CheckpointId, Open, TCEnv, openThing)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute (NoSubst(..))
import Agda.Interaction.Base (Rewrite(..))
import Agda.Utils.Tuple (mapSnd)
import Agda.Utils.Impossible

import Agda.Mimer.Options

------------------------------------------------------------------------
-- * Results
------------------------------------------------------------------------

data MimerResult
  = MimerExpr String -- ^ Returns 'String' rather than 'Expr' because the give action expects a string.
  | 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

isNoResult :: MimerResult -> Bool
isNoResult :: MimerResult -> Bool
isNoResult MimerResult
MimerNoResult = Bool
True
isNoResult MimerResult
_             = Bool
False

data SearchStepResult
  = ResultExpr Expr
  | 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

------------------------------------------------------------------------
-- * Search branches
------------------------------------------------------------------------

data SearchBranch = SearchBranch
  { SearchBranch -> TCState
sbTCState :: TCState
  , SearchBranch -> [Goal]
sbGoals :: [Goal]
  , SearchBranch -> Int
sbCost :: Int
  , SearchBranch -> Map CheckpointId ComponentCache
sbCache :: Map CheckpointId ComponentCache
  , SearchBranch -> Map Name Int
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 -> Int
sbCost SearchBranch
sb1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== SearchBranch -> Int
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 = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (SearchBranch -> Int)
-> SearchBranch
-> SearchBranch
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` SearchBranch -> Int
sbCost

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

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

-- | Take the first goal off a search branch.
--   Precondition: the set of goals is non-empty.
nextGoal :: SearchBranch -> (Goal, SearchBranch)
nextGoal :: SearchBranch -> (Goal, SearchBranch)
nextGoal SearchBranch
branch =
  case SearchBranch -> [Goal]
sbGoals SearchBranch
branch of
    [] -> (Goal, SearchBranch)
forall a. HasCallStack => a
__IMPOSSIBLE__
    Goal
goal : [Goal]
goals -> (Goal
goal, SearchBranch
branch{ sbGoals = goals })

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

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

-- | 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 Int)]
hintRecVars :: Open [(Term, NoSubst Term Int)] -- ^ Variable terms and which argument they come from
  }
  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 -> Int
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 -> Int
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 -> Int
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 = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (Component -> Int) -> Component -> Component -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Component -> Int
compId

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

mkComponentQ :: CompId -> Cost -> QName -> Nat -> Term -> Type -> Component
mkComponentQ :: Int -> Int -> QName -> Int -> Term -> Type -> Component
mkComponentQ Int
cId Int
cost QName
qname = Int
-> [MetaId]
-> Int
-> Maybe Name
-> Int
-> Term
-> Type
-> Component
mkComponent Int
cId [] Int
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

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

replaceCompMeta :: MetaId -> [MetaId] -> Component -> Component
replaceCompMeta :: MetaId -> [MetaId] -> Component -> Component
replaceCompMeta MetaId
old [MetaId]
new Component
c = Component
c{ compMetas = new ++ List.delete old (compMetas c) }

------------------------------------------------------------------------
-- * SearchOptions
------------------------------------------------------------------------

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
  , SearchOptions -> Maybe QName
searchBuiltinFlat :: Maybe QName
      -- Cache BUILTIN_FLAT for issue #7662 workaround
  }

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

noCost :: Cost
noCost :: Int
noCost = Int
0

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

------------------------------------------------------------------------
-- * Measure performance
------------------------------------------------------------------------

data MimerStats = MimerStats
  { MimerStats -> Int
statCompHit       :: !Int -- ^ Could make use of an already generated component
  , MimerStats -> Int
statCompGen       :: !Int -- ^ Could use a generator for a component
  , MimerStats -> Int
statCompRegen     :: !Int -- ^ Had to regenerate the cache (new context)
  , MimerStats -> Int
statCompNoRegen   :: !Int -- ^ Did not have to regenerate the cache
  , MimerStats -> Int
statMetasCreated  :: !Int -- ^ Total number of meta-variables created explicitly (not through unification)
  , MimerStats -> Int
statTypeEqChecks  :: !Int -- ^ Number of times type equality is tested (with unification)
  , MimerStats -> Int
statRefineSuccess :: !Int -- ^ Number of times a refinement has been successful
  , MimerStats -> Int
statRefineFail    :: !Int -- ^ Number of times a refinement has failed
  } deriving (Int -> MimerStats -> ShowS
[MimerStats] -> ShowS
MimerStats -> String
(Int -> MimerStats -> ShowS)
-> (MimerStats -> String)
-> ([MimerStats] -> ShowS)
-> Show MimerStats
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MimerStats -> ShowS
showsPrec :: Int -> MimerStats -> ShowS
$cshow :: MimerStats -> String
show :: MimerStats -> String
$cshowList :: [MimerStats] -> ShowS
showList :: [MimerStats] -> ShowS
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 :: Int
statCompHit = Int
0, statCompGen :: Int
statCompGen = Int
0, statCompRegen :: Int
statCompRegen = Int
0 , statCompNoRegen :: Int
statCompNoRegen = Int
0 , statMetasCreated :: Int
statMetasCreated = Int
0, statTypeEqChecks :: Int
statTypeEqChecks = Int
0, statRefineSuccess :: Int
statRefineSuccess = Int
0 , statRefineFail :: Int
statRefineFail = Int
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}

------------------------------------------------------------------------
-- * Pretty printing
------------------------------------------------------------------------

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, Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
P.nest Int
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 -> Int -> Doc -> Doc
forall a. Doc a -> Int -> Doc a -> Doc a
P.hang (Doc
k Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> Doc
"=") Int
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 -> Int -> Doc -> Doc
forall a. Doc a -> Int -> Doc a -> Doc a
P.hang (Doc
k Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Doc
":") Int
2 Doc
v | (Doc
k, Doc
v) <- [(Doc, Doc)]
kvs ]

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", Int -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Int -> Doc) -> Int -> Doc
forall a b. (a -> b) -> a -> b
$ SearchBranch -> Int
sbCost SearchBranch
branch)
    , (Doc
"sbComponentsUsed", Map Name Int -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Map Name Int -> Doc) -> Map Name Int -> Doc
forall a b. (a -> b) -> a -> b
$ SearchBranch -> Map Name Int
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:"
         , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
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, Int)] -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ((NoSubst Term Int -> Int)
-> (Term, NoSubst Term Int) -> (Term, Int)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd NoSubst Term Int -> Int
forall t a. NoSubst t a -> a
unNoSubst ((Term, NoSubst Term Int) -> (Term, Int))
-> [(Term, NoSubst Term Int)] -> [(Term, Int)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Open [(Term, NoSubst Term Int)] -> [(Term, NoSubst Term Int)]
forall a. Open a -> a
openThing (BaseComponents -> Open [(Term, NoSubst Term Int)]
hintRecVars 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
$+$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
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)

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.$$ Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
P.nest Int
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:"
    , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
P.nest Int
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:"
    , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
P.nest Int
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:"
    , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
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:"
    , Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
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", Int -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Int -> Doc) -> Int -> Doc
forall a b. (a -> b) -> a -> b
$ Component -> Int
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", Int -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Int -> Doc) -> Int -> Doc
forall a b. (a -> b) -> a -> b
$ Component -> Int
compCost Component
comp)
    ]

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

instance PrettyTCM Component where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => Component -> m Doc
prettyTCM Component{Bool
Int
[MetaId]
Maybe Name
Type
Term
compId :: Component -> Int
compName :: Component -> Maybe Name
compPars :: Component -> Int
compTerm :: Component -> Term
compType :: Component -> Type
compRec :: Component -> Bool
compMetas :: Component -> [MetaId]
compCost :: Component -> Int
compId :: Int
compName :: Maybe Name
compPars :: Int
compTerm :: Term
compType :: Type
compRec :: Bool
compMetas :: [MetaId]
compCost :: Int
..} = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (Int -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM Int
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
<+> Int -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM Int
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 String
expr    -> String -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty String
expr
    MimerResult
MimerNoResult     -> m Doc
"MimerNoResult"
    MimerList [(Int, String)]
sols    -> m Doc
"MimerList" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [(Int, String)] -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [(Int, String)]
sols