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.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

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 }

deleteCompMeta :: MetaId -> Component -> Component
deleteCompMeta :: MetaId -> Component -> Component
deleteCompMeta MetaId
old Component
c = Component
c{ compMetas = 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
<> 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
<> Doc
": []"
      f Doc
n [a]
xs = (Doc
n Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> 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