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

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

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

instance Pretty SearchBranch where
  pretty :: SearchBranch -> Doc Aspects
pretty SearchBranch
branch = [(Doc Aspects, Doc Aspects)] -> Doc Aspects
keyValueList
    [ (Doc Aspects
"sbTCState", Doc Aspects
"[...]")
    , (Doc Aspects
"sbGoals", [Goal] -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
P.pretty ([Goal] -> Doc Aspects) -> [Goal] -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ SearchBranch -> [Goal]
sbGoals SearchBranch
branch)
    , (Doc Aspects
"sbCost", Int -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
P.pretty (Int -> Doc Aspects) -> Int -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ SearchBranch -> Int
sbCost SearchBranch
branch)
    , (Doc Aspects
"sbComponentsUsed", Map Name Int -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
P.pretty (Map Name Int -> Doc Aspects) -> Map Name Int -> Doc Aspects
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 Aspects)
prettyTCM BaseComponents
comps = do
    let thisFn :: m (Doc Aspects)
thisFn = case BaseComponents -> Maybe Component
hintThisFn BaseComponents
comps of
          Maybe Component
Nothing -> m (Doc Aspects)
"(nothing)"
          Just Component
comp -> Component -> m (Doc Aspects)
forall {m :: * -> *}.
(Applicative m, IsString (m (Doc Aspects))) =>
Component -> m (Doc Aspects)
prettyComp Component
comp
    [m (Doc Aspects)] -> m (Doc Aspects)
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m (Doc Aspects)) -> m (Doc Aspects)
vcat [ m (Doc Aspects)
"Base components:"
         , Int -> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *).
Functor m =>
Int -> m (Doc Aspects) -> m (Doc Aspects)
nest Int
2 (m (Doc Aspects) -> m (Doc Aspects))
-> m (Doc Aspects) -> m (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ [m (Doc Aspects)] -> m (Doc Aspects)
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m (Doc Aspects)) -> m (Doc Aspects)
vcat
           [ m (Doc Aspects) -> [Component] -> m (Doc Aspects)
f m (Doc Aspects)
"hintFns" (BaseComponents -> [Component]
hintFns BaseComponents
comps)
           , m (Doc Aspects) -> [Component] -> m (Doc Aspects)
f m (Doc Aspects)
"hintDataTypes" (BaseComponents -> [Component]
hintDataTypes BaseComponents
comps)
           , m (Doc Aspects) -> [Component] -> m (Doc Aspects)
f m (Doc Aspects)
"hintRecordTypes" (BaseComponents -> [Component]
hintRecordTypes BaseComponents
comps)
           , m (Doc Aspects) -> [Component] -> m (Doc Aspects)
f m (Doc Aspects)
"hintAxioms" (BaseComponents -> [Component]
hintAxioms BaseComponents
comps)
           , m (Doc Aspects) -> [Component] -> m (Doc Aspects)
f m (Doc Aspects)
"hintLevel" (BaseComponents -> [Component]
hintLevel BaseComponents
comps)
           , m (Doc Aspects) -> [Component] -> m (Doc Aspects)
f m (Doc Aspects)
"hintProjections" (BaseComponents -> [Component]
hintProjections BaseComponents
comps)
           , m (Doc Aspects)
"hintThisFn:" m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
<+> m (Doc Aspects)
thisFn
           , (Open Component -> m (Doc Aspects))
-> m (Doc Aspects) -> [Open Component] -> m (Doc Aspects)
forall {m :: * -> *} {t}.
(Semigroup (m (Doc Aspects)), IsString (m (Doc Aspects)),
 Applicative m) =>
(t -> m (Doc Aspects)) -> m (Doc Aspects) -> [t] -> m (Doc Aspects)
g Open Component -> m (Doc Aspects)
forall {m :: * -> *}.
(Applicative m, IsString (m (Doc Aspects))) =>
Open Component -> m (Doc Aspects)
prettyOpenComp m (Doc Aspects)
"hintLetVars" (BaseComponents -> [Open Component]
hintLetVars BaseComponents
comps)
           , m (Doc Aspects)
"hintRecVars: Open" m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
<+> [(Term, Int)] -> m (Doc Aspects)
forall (m :: * -> *) a.
(Applicative m, Pretty a) =>
a -> m (Doc Aspects)
pretty ((NoSubst Term Int -> Int)
-> (Term, NoSubst Term Int) -> (Term, Int)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second 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 Aspects)
prettyComp Component
comp = Term -> m (Doc Aspects)
forall (m :: * -> *) a.
(Applicative m, Pretty a) =>
a -> m (Doc Aspects)
pretty (Component -> Term
compTerm Component
comp) m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
<+> m (Doc Aspects)
":" m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
<+> Type -> m (Doc Aspects)
forall (m :: * -> *) a.
(Applicative m, Pretty a) =>
a -> m (Doc Aspects)
pretty (Component -> Type
compType Component
comp)
      prettyOpenComp :: Open Component -> m (Doc Aspects)
prettyOpenComp Open Component
openComp = m (Doc Aspects)
"Open" m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
<+> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *).
Functor m =>
m (Doc Aspects) -> m (Doc Aspects)
parens (Component -> m (Doc Aspects)
forall {m :: * -> *}.
(Applicative m, IsString (m (Doc Aspects))) =>
Component -> m (Doc Aspects)
prettyComp (Component -> m (Doc Aspects)) -> Component -> m (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ Open Component -> Component
forall a. Open a -> a
openThing Open Component
openComp)
      prettyTCMComp :: Component -> m (Doc Aspects)
prettyTCMComp Component
comp = Term -> m (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *). MonadPretty m => Term -> m (Doc Aspects)
prettyTCM (Component -> Term
compTerm Component
comp) m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
<+> m (Doc Aspects)
":" m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
<+> Type -> m (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *). MonadPretty m => Type -> m (Doc Aspects)
prettyTCM (Component -> Type
compType Component
comp)
      f :: m (Doc Aspects) -> [Component] -> m (Doc Aspects)
f = (Component -> m (Doc Aspects))
-> m (Doc Aspects) -> [Component] -> m (Doc Aspects)
forall {m :: * -> *} {t}.
(Semigroup (m (Doc Aspects)), IsString (m (Doc Aspects)),
 Applicative m) =>
(t -> m (Doc Aspects)) -> m (Doc Aspects) -> [t] -> m (Doc Aspects)
g Component -> m (Doc Aspects)
forall {m :: * -> *}.
(MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m (Doc Aspects)),
 Null (m (Doc Aspects)), Semigroup (m (Doc Aspects))) =>
Component -> m (Doc Aspects)
prettyTCMComp
      g :: (t -> m (Doc Aspects)) -> m (Doc Aspects) -> [t] -> m (Doc Aspects)
g t -> m (Doc Aspects)
p m (Doc Aspects)
n [] = m (Doc Aspects)
n m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
forall a. Semigroup a => a -> a -> a
<> m (Doc Aspects)
": []"
      g t -> m (Doc Aspects)
p m (Doc Aspects)
n [t]
xs = (m (Doc Aspects)
n m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
forall a. Semigroup a => a -> a -> a
<> m (Doc Aspects)
":") m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
$+$ Int -> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *).
Functor m =>
Int -> m (Doc Aspects) -> m (Doc Aspects)
nest Int
2 ([m (Doc Aspects)] -> m (Doc Aspects)
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m (Doc Aspects)) -> m (Doc Aspects)
vcat ([m (Doc Aspects)] -> m (Doc Aspects))
-> [m (Doc Aspects)] -> m (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ (t -> m (Doc Aspects)) -> [t] -> [m (Doc Aspects)]
forall a b. (a -> b) -> [a] -> [b]
map t -> m (Doc Aspects)
p [t]
xs)

instance Pretty BaseComponents where
  pretty :: BaseComponents -> Doc Aspects
pretty BaseComponents
comps = [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
P.vcat
      [ Doc Aspects -> [Component] -> Doc Aspects
forall {a}. Pretty a => Doc Aspects -> [a] -> Doc Aspects
f Doc Aspects
"hintFns" (BaseComponents -> [Component]
hintFns BaseComponents
comps)
      , Doc Aspects -> [Component] -> Doc Aspects
forall {a}. Pretty a => Doc Aspects -> [a] -> Doc Aspects
f Doc Aspects
"hintDataTypes" (BaseComponents -> [Component]
hintDataTypes BaseComponents
comps)
      , Doc Aspects -> [Component] -> Doc Aspects
forall {a}. Pretty a => Doc Aspects -> [a] -> Doc Aspects
f Doc Aspects
"hintRecordTypes" (BaseComponents -> [Component]
hintRecordTypes BaseComponents
comps)
      , Doc Aspects -> [Component] -> Doc Aspects
forall {a}. Pretty a => Doc Aspects -> [a] -> Doc Aspects
f Doc Aspects
"hintAxioms" (BaseComponents -> [Component]
hintAxioms BaseComponents
comps)
      , Doc Aspects -> [Component] -> Doc Aspects
forall {a}. Pretty a => Doc Aspects -> [a] -> Doc Aspects
f Doc Aspects
"hintLevel" (BaseComponents -> [Component]
hintLevel BaseComponents
comps)
      , Doc Aspects -> [Component] -> Doc Aspects
forall {a}. Pretty a => Doc Aspects -> [a] -> Doc Aspects
f Doc Aspects
"hintProjections" (BaseComponents -> [Component]
hintProjections BaseComponents
comps)
      ]
    where
      f :: Doc Aspects -> [a] -> Doc Aspects
f Doc Aspects
n [] = Doc Aspects
n Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Semigroup a => a -> a -> a
<> Doc Aspects
": []"
      f Doc Aspects
n [a]
xs = (Doc Aspects
n Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Semigroup a => a -> a -> a
<> Doc Aspects
":") Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
P.$$ Int -> Doc Aspects -> Doc Aspects
forall a. Int -> Doc a -> Doc a
P.nest Int
2 ([a] -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
P.pretty [a]
xs)

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

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

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

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

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

instance PrettyTCM MimerResult where
  prettyTCM :: forall (m :: * -> *).
MonadPretty m =>
MimerResult -> m (Doc Aspects)
prettyTCM = \case
    MimerExpr String
expr    -> String -> m (Doc Aspects)
forall (m :: * -> *) a.
(Applicative m, Pretty a) =>
a -> m (Doc Aspects)
pretty String
expr
    MimerResult
MimerNoResult     -> m (Doc Aspects)
"MimerNoResult"
    MimerList [(Int, String)]
sols    -> m (Doc Aspects)
"MimerList" m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
<+> [(Int, String)] -> m (Doc Aspects)
forall (m :: * -> *) a.
(Applicative m, Pretty a) =>
a -> m (Doc Aspects)
pretty [(Int, String)]
sols