module Agda.Mimer.Mimer
( MimerResult(..)
, mimer
)
where
import Control.DeepSeq (force, NFData(..))
import Control.Monad
import Control.Monad.Except (catchError)
import Control.Monad.Error.Class (MonadError)
import Control.Monad.Fail (MonadFail)
import Control.Monad.IO.Class (liftIO)
import Control.Monad.Reader (ReaderT(..), runReaderT, asks, ask, lift)
import Data.Function (on)
import Data.Functor ((<&>))
import Data.List (sortOn, intersect, transpose, (\\))
import qualified Data.List.NonEmpty as NonEmptyList (head)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Maybe (maybeToList, fromMaybe, maybe, isNothing)
import Data.PQueue.Min (MinQueue)
import qualified Data.PQueue.Min as Q
import GHC.Generics (Generic)
import qualified Text.PrettyPrint.Boxes as Box
import qualified Data.Text as Text
import qualified Agda.Benchmarking as Bench
import Agda.Interaction.MakeCase (makeCase, getClauseZipperForIP, recheckAbstractClause)
import Agda.Syntax.Abstract (Expr(AbsurdLam))
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Views as A
import Agda.Syntax.Abstract.Name (QName(..), Name(..))
import Agda.Syntax.Common (InteractionId(..), MetaId(..), ArgInfo(..), defaultArgInfo, Origin(..), ConOrigin(..), Hiding(..), setOrigin, NameId, Nat, namedThing, Arg(..), setHiding, getHiding, ProjOrigin(..), rangedThing, woThing, nameOf, visible)
import Agda.Syntax.Common.Pretty (Pretty)
import qualified Agda.Syntax.Common.Pretty as P
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Info (pattern UnificationMeta, exprNoRange)
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars (AllMetas(..))
import Agda.Syntax.Internal.Pattern (clausePerm)
import Agda.Syntax.Position (Range, rangeFile, rangeFilePath)
import qualified Agda.Syntax.Scope.Base as Scope
import Agda.Syntax.Translation.InternalToAbstract (reify, NamedClause(..))
import Agda.Syntax.Translation.AbstractToConcrete (abstractToConcrete_)
import Agda.TypeChecking.Constraints (noConstraints)
import Agda.TypeChecking.Conversion (equalType)
import qualified Agda.TypeChecking.Empty as Empty
import Agda.TypeChecking.Free (flexRigOccurrenceIn, freeVars)
import Agda.TypeChecking.Level (levelType)
import Agda.TypeChecking.MetaVars (newValueMeta)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records (isRecord, isRecursiveRecord)
import Agda.TypeChecking.Reduce (reduce, instantiateFull, instantiate)
import Agda.TypeChecking.Rules.LHS.Problem (AsBinding(..))
import Agda.TypeChecking.Rules.Term (lambdaAddContext)
import Agda.TypeChecking.Substitute.Class (apply, applyE, NoSubst(..))
import Agda.TypeChecking.Telescope (piApplyM, flattenTel, teleArgs)
import Agda.Utils.Benchmark (billTo)
import Agda.Utils.FileName (filePath)
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.Utils.Maybe (catMaybes)
import Agda.Utils.Monad (ifM)
import qualified Agda.Utils.Maybe.Strict as SMaybe
import Agda.Utils.Time (CPUTime(..), getCPUTime, fromMilliseconds)
import Agda.Utils.Tuple (mapFst, mapSnd)
import Agda.Utils.FileName (AbsolutePath(..))
import Agda.Mimer.Options
import System.IO.Unsafe (unsafePerformIO)
import Data.IORef (IORef, writeIORef, readIORef, newIORef, modifyIORef')
import qualified Agda.Utils.Maybe.Strict as Strict
import qualified Agda.Utils.Trie as Trie
import Agda.Interaction.Base (Rewrite(..))
import Agda.Interaction.BasicOps (normalForm)
import Agda.Interaction.Options.Base (parseVerboseKey)
import Agda.Utils.List (lastWithDefault)
data MimerResult
= MimerExpr String
| MimerClauses QName [A.Clause]
| MimerList [(Int, String)]
| MimerNoResult
deriving ((forall x. MimerResult -> Rep MimerResult x)
-> (forall x. Rep MimerResult x -> MimerResult)
-> Generic MimerResult
forall x. Rep MimerResult x -> MimerResult
forall x. MimerResult -> Rep MimerResult x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MimerResult -> Rep MimerResult x
from :: forall x. MimerResult -> Rep MimerResult x
$cto :: forall x. Rep MimerResult x -> MimerResult
to :: forall x. Rep MimerResult x -> MimerResult
Generic)
instance NFData MimerResult
mimer :: MonadTCM tcm
=> Rewrite
-> InteractionId
-> Range
-> String
-> tcm MimerResult
mimer :: forall (tcm :: * -> *).
MonadTCM tcm =>
Rewrite -> InteractionId -> Range -> ArgName -> tcm MimerResult
mimer Rewrite
norm InteractionId
ii Range
rng ArgName
argStr = TCM MimerResult -> tcm MimerResult
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM MimerResult -> tcm MimerResult)
-> TCM MimerResult -> tcm MimerResult
forall a b. (a -> b) -> a -> b
$ do
ArgName -> VerboseLevel -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"mimer.top" VerboseLevel
10 (TCMT IO Doc
"Running Mimer on interaction point" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> InteractionId -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty InteractionId
ii TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"with argument string" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> ArgName
forall a. Show a => a -> ArgName
show ArgName
argStr))
start <- IO CPUTime -> TCMT IO CPUTime
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO CPUTime -> TCMT IO CPUTime) -> IO CPUTime -> TCMT IO CPUTime
forall a b. (a -> b) -> a -> b
$ IO CPUTime
forall (m :: * -> *). MonadIO m => m CPUTime
getCPUTime
opts <- parseOptions ii rng argStr
reportS "mimer.top" 15 ("Mimer options: " ++ show opts)
oldState <- getTC
sols <- runSearch norm opts ii rng
putTC oldState
sol <- case drop (optSkip opts) $ zip [0..] sols of
[] -> do
ArgName -> VerboseLevel -> ArgName -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> ArgName -> m ()
reportSLn ArgName
"mimer.top" VerboseLevel
10 ArgName
"No solution found"
MimerResult -> TCM MimerResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MimerResult
MimerNoResult
[(VerboseLevel, MimerResult)]
sols' | Options -> Bool
optList Options
opts -> MimerResult -> TCM MimerResult
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MimerResult -> TCM MimerResult) -> MimerResult -> TCM MimerResult
forall a b. (a -> b) -> a -> b
$ [(VerboseLevel, ArgName)] -> MimerResult
MimerList [ (VerboseLevel
i, ArgName
s) | (VerboseLevel
i, MimerExpr ArgName
s) <- [(VerboseLevel, MimerResult)]
sols' ]
(VerboseLevel
_, MimerResult
sol) : [(VerboseLevel, MimerResult)]
_ -> do
ArgName -> VerboseLevel -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"mimer.top" VerboseLevel
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Solution:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MimerResult -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MimerResult -> m Doc
prettyTCM MimerResult
sol
MimerResult -> TCM MimerResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MimerResult
sol
putTC oldState
stop <- liftIO $ getCPUTime
let time = CPUTime
stop CPUTime -> CPUTime -> CPUTime
forall a. Num a => a -> a -> a
- CPUTime
start
reportSDoc "mimer.top" 10 ("Total elapsed time:" <+> pretty time)
verboseS "mimer.stats" 50 $ writeTime ii (if null sols then Nothing else Just time)
return sol
type SM a = ReaderT SearchOptions TCM a
data SearchBranch = SearchBranch
{ SearchBranch -> TCState
sbTCState :: TCState
, SearchBranch -> [Goal]
sbGoals :: [Goal]
, SearchBranch -> VerboseLevel
sbCost :: Int
, SearchBranch -> Map CheckpointId ComponentCache
sbCache :: Map CheckpointId ComponentCache
, SearchBranch -> Map Name VerboseLevel
sbComponentsUsed :: Map Name Int
}
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
instance Eq SearchBranch where
SearchBranch
sb1 == :: SearchBranch -> SearchBranch -> Bool
== SearchBranch
sb2 = SearchBranch -> VerboseLevel
sbCost SearchBranch
sb1 VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== SearchBranch -> VerboseLevel
sbCost SearchBranch
sb2 Bool -> Bool -> Bool
&& SearchBranch -> [Goal]
sbGoals SearchBranch
sb1 [Goal] -> [Goal] -> Bool
forall a. Eq a => a -> a -> Bool
== SearchBranch -> [Goal]
sbGoals SearchBranch
sb2
instance Ord SearchBranch where
compare :: SearchBranch -> SearchBranch -> Ordering
compare = VerboseLevel -> VerboseLevel -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (VerboseLevel -> VerboseLevel -> Ordering)
-> (SearchBranch -> VerboseLevel)
-> SearchBranch
-> SearchBranch
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` SearchBranch -> VerboseLevel
sbCost
type ComponentCache = Map Component (Maybe [Component])
data Goal = Goal
{ Goal -> MetaId
goalMeta :: MetaId
}
deriving ((forall x. Goal -> Rep Goal x)
-> (forall x. Rep Goal x -> Goal) -> Generic Goal
forall x. Rep Goal x -> Goal
forall x. Goal -> Rep Goal x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Goal -> Rep Goal x
from :: forall x. Goal -> Rep Goal x
$cto :: forall x. Rep Goal x -> Goal
to :: forall x. Rep Goal x -> Goal
Generic)
instance NFData Goal
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
data BaseComponents = BaseComponents
{ BaseComponents -> [Component]
hintFns :: [Component]
, BaseComponents -> [Component]
hintDataTypes :: [Component]
, BaseComponents -> [Component]
hintRecordTypes :: [Component]
, BaseComponents -> [Component]
hintAxioms :: [Component]
, BaseComponents -> [Component]
hintLevel :: [Component]
, BaseComponents -> [Component]
hintProjections :: [Component]
, BaseComponents -> Maybe Component
hintThisFn :: Maybe Component
, BaseComponents -> [Open Component]
hintLetVars :: [Open Component]
, BaseComponents -> Open [(Term, NoSubst Term VerboseLevel)]
hintRecVars :: Open [(Term, NoSubst Term Int)]
, BaseComponents -> Open [Term]
hintSplitVars :: Open [Term]
}
deriving ((forall x. BaseComponents -> Rep BaseComponents x)
-> (forall x. Rep BaseComponents x -> BaseComponents)
-> Generic BaseComponents
forall x. Rep BaseComponents x -> BaseComponents
forall x. BaseComponents -> Rep BaseComponents x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BaseComponents -> Rep BaseComponents x
from :: forall x. BaseComponents -> Rep BaseComponents x
$cto :: forall x. Rep BaseComponents x -> BaseComponents
to :: forall x. Rep BaseComponents x -> BaseComponents
Generic)
instance NFData BaseComponents
type CompId = Int
data Component = Component
{ Component -> VerboseLevel
compId :: CompId
, Component -> Maybe Name
compName :: Maybe Name
, Component -> VerboseLevel
compPars :: Nat
, Component -> Term
compTerm :: Term
, Component -> Type
compType :: Type
, Component -> Bool
compRec :: Bool
, Component -> [MetaId]
compMetas :: [MetaId]
, Component -> VerboseLevel
compCost :: Cost
}
deriving (Component -> Component -> Bool
(Component -> Component -> Bool)
-> (Component -> Component -> Bool) -> Eq Component
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Component -> Component -> Bool
== :: Component -> Component -> Bool
$c/= :: Component -> Component -> Bool
/= :: Component -> Component -> Bool
Eq, (forall x. Component -> Rep Component x)
-> (forall x. Rep Component x -> Component) -> Generic Component
forall x. Rep Component x -> Component
forall x. Component -> Rep Component x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Component -> Rep Component x
from :: forall x. Component -> Rep Component x
$cto :: forall x. Rep Component x -> Component
to :: forall x. Rep Component x -> Component
Generic)
instance NFData Component
instance Ord Component where
compare :: Component -> Component -> Ordering
compare = VerboseLevel -> VerboseLevel -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (VerboseLevel -> VerboseLevel -> Ordering)
-> (Component -> VerboseLevel)
-> Component
-> Component
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Component -> VerboseLevel
compId
data SearchStepResult
= ResultExpr Expr
| ResultClauses [A.Clause]
| OpenBranch SearchBranch
| NoSolution
deriving ((forall x. SearchStepResult -> Rep SearchStepResult x)
-> (forall x. Rep SearchStepResult x -> SearchStepResult)
-> Generic SearchStepResult
forall x. Rep SearchStepResult x -> SearchStepResult
forall x. SearchStepResult -> Rep SearchStepResult x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SearchStepResult -> Rep SearchStepResult x
from :: forall x. SearchStepResult -> Rep SearchStepResult x
$cto :: forall x. Rep SearchStepResult x -> SearchStepResult
to :: forall x. Rep SearchStepResult x -> SearchStepResult
Generic)
instance NFData SearchStepResult
data SearchOptions = SearchOptions
{ SearchOptions -> BaseComponents
searchBaseComponents :: BaseComponents
, SearchOptions -> HintMode
searchHintMode :: HintMode
, SearchOptions -> Integer
searchTimeout :: MilliSeconds
, SearchOptions -> Bool
searchGenProjectionsLocal :: Bool
, SearchOptions -> Bool
searchGenProjectionsLet :: Bool
, SearchOptions -> Bool
searchGenProjectionsExternal :: Bool
, SearchOptions -> Bool
searchGenProjectionsRec :: Bool
, SearchOptions -> Bool
searchSpeculateProjections :: Bool
, SearchOptions -> MetaId
searchTopMeta :: MetaId
, SearchOptions -> TCEnv
searchTopEnv :: TCEnv
, SearchOptions -> CheckpointId
searchTopCheckpoint :: CheckpointId
, SearchOptions -> InteractionId
searchInteractionId :: InteractionId
, SearchOptions -> Maybe QName
searchFnName :: Maybe QName
, SearchOptions -> Costs
searchCosts :: Costs
, SearchOptions -> IORef MimerStats
searchStats :: IORef MimerStats
, SearchOptions -> Rewrite
searchRewrite :: Rewrite
}
type Cost = Int
data Costs = Costs
{ Costs -> VerboseLevel
costLocal :: Cost
, Costs -> VerboseLevel
costFn :: Cost
, Costs -> VerboseLevel
costDataCon :: Cost
, Costs -> VerboseLevel
costRecordCon :: Cost
, Costs -> VerboseLevel
costSpeculateProj :: Cost
, Costs -> VerboseLevel
costProj :: Cost
, Costs -> VerboseLevel
costAxiom :: Cost
, Costs -> VerboseLevel
costLet :: Cost
, Costs -> VerboseLevel
costLevel :: Cost
, Costs -> VerboseLevel
costSet :: Cost
, Costs -> VerboseLevel
costRecCall :: Cost
, Costs -> VerboseLevel
costNewMeta :: Cost
, Costs -> VerboseLevel
costNewHiddenMeta :: Cost
, Costs -> VerboseLevel -> VerboseLevel
costCompReuse :: Nat -> Cost
}
noCost :: Cost
noCost :: VerboseLevel
noCost = VerboseLevel
0
defaultCosts :: Costs
defaultCosts :: Costs
defaultCosts = Costs
{ costLocal :: VerboseLevel
costLocal = VerboseLevel
3
, costFn :: VerboseLevel
costFn = VerboseLevel
10
, costDataCon :: VerboseLevel
costDataCon = VerboseLevel
3
, costRecordCon :: VerboseLevel
costRecordCon = VerboseLevel
3
, costSpeculateProj :: VerboseLevel
costSpeculateProj = VerboseLevel
20
, costProj :: VerboseLevel
costProj = VerboseLevel
3
, costAxiom :: VerboseLevel
costAxiom = VerboseLevel
10
, costLet :: VerboseLevel
costLet = VerboseLevel
5
, costLevel :: VerboseLevel
costLevel = VerboseLevel
3
, costSet :: VerboseLevel
costSet = VerboseLevel
10
, costRecCall :: VerboseLevel
costRecCall = VerboseLevel
8
, costNewMeta :: VerboseLevel
costNewMeta = VerboseLevel
10
, costNewHiddenMeta :: VerboseLevel
costNewHiddenMeta = VerboseLevel
1
, costCompReuse :: VerboseLevel -> VerboseLevel
costCompReuse = \VerboseLevel
uses -> VerboseLevel
10 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
* (VerboseLevel
uses VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1) VerboseLevel -> Integer -> VerboseLevel
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
2
}
predNat :: Nat -> Nat
predNat :: VerboseLevel -> VerboseLevel
predNat VerboseLevel
n | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0 = VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1
| VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
0 = VerboseLevel
0
| Bool
otherwise = ArgName -> VerboseLevel
forall a. HasCallStack => ArgName -> a
error ArgName
"predNat of negative value"
getRecordFields :: (HasConstInfo tcm, MonadTCM tcm) => QName -> tcm [QName]
getRecordFields :: forall (tcm :: * -> *).
(HasConstInfo tcm, MonadTCM tcm) =>
QName -> tcm [QName]
getRecordFields = (Definition -> [QName]) -> tcm Definition -> tcm [QName]
forall a b. (a -> b) -> tcm a -> tcm b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Dom' Term QName -> QName) -> [Dom' Term QName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term QName -> QName
forall t e. Dom' t e -> e
unDom ([Dom' Term QName] -> [QName])
-> (Definition -> [Dom' Term QName]) -> Definition -> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> [Dom' Term QName]
recFields (Defn -> [Dom' Term QName])
-> (Definition -> Defn) -> Definition -> [Dom' Term QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef) (tcm Definition -> tcm [QName])
-> (QName -> tcm Definition) -> QName -> tcm [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> tcm Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo
isEmptyType :: Type -> SM Bool
isEmptyType :: Type -> SM Bool
isEmptyType = TCM Bool -> SM Bool
forall a. TCM a -> ReaderT SearchOptions (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> SM Bool) -> (Type -> TCM Bool) -> Type -> SM Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TCM Bool
Empty.isEmptyType
getDomainType :: Type -> Type
getDomainType :: Type -> Type
getDomainType Type
typ = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
typ of
Pi Dom Type
dom Abs Type
_ -> Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom
Term
_ -> Type
forall a. HasCallStack => a
__IMPOSSIBLE__
allOpenMetas :: (AllMetas t, ReadTCState tcm) => t -> tcm [MetaId]
allOpenMetas :: forall t (tcm :: * -> *).
(AllMetas t, ReadTCState tcm) =>
t -> tcm [MetaId]
allOpenMetas t
t = do
openMetas <- tcm [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas
return $ allMetas (:[]) t `intersect` openMetas
getOpenComponent :: MonadTCM tcm => Open Component -> tcm Component
getOpenComponent :: forall (tcm :: * -> *).
MonadTCM tcm =>
Open Component -> tcm Component
getOpenComponent Open Component
openComp = do
let comp :: Component
comp = Open Component -> Component
forall a. Open a -> a
openThing Open Component
openComp
term <- Open Term -> tcm Term
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen (Open Term -> tcm Term) -> Open Term -> tcm Term
forall a b. (a -> b) -> a -> b
$ Component -> Term
compTerm (Component -> Term) -> Open Component -> Open Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Open Component
openComp
typ <- getOpen $ compType <$> openComp
when (not $ null $ compMetas comp) __IMPOSSIBLE__
return Component
{ compId = compId comp
, compName = compName comp
, compPars = compPars comp
, compTerm = term
, compType = typ
, compRec = compRec comp
, compMetas = compMetas comp
, compCost = compCost comp
}
mkComponent :: CompId -> [MetaId] -> Cost -> Maybe Name -> Nat -> Term -> Type -> Component
mkComponent :: VerboseLevel
-> [MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> Component
mkComponent VerboseLevel
cId [MetaId]
metaIds VerboseLevel
cost Maybe Name
mName VerboseLevel
pars Term
term Type
typ = Component
{ compId :: VerboseLevel
compId = VerboseLevel
cId
, compName :: Maybe Name
compName = Maybe Name
mName
, compPars :: VerboseLevel
compPars = VerboseLevel
pars
, compTerm :: Term
compTerm = Term
term
, compType :: Type
compType = Type
typ
, compRec :: Bool
compRec = Bool
False
, compMetas :: [MetaId]
compMetas = [MetaId]
metaIds
, compCost :: VerboseLevel
compCost = VerboseLevel
cost }
mkComponentQ :: CompId -> Cost -> QName -> Nat -> Term -> Type -> Component
mkComponentQ :: VerboseLevel
-> VerboseLevel
-> QName
-> VerboseLevel
-> Term
-> Type
-> Component
mkComponentQ VerboseLevel
cId VerboseLevel
cost QName
qname = VerboseLevel
-> [MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> Component
mkComponent VerboseLevel
cId [] VerboseLevel
cost (Name -> Maybe Name
forall a. a -> Maybe a
Just (Name -> Maybe Name) -> Name -> Maybe Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
qname)
noName :: Maybe Name
noName :: Maybe Name
noName = Maybe Name
forall a. Maybe a
Nothing
newComponent :: MonadFresh CompId m => [MetaId] -> Cost -> Maybe Name -> Nat -> Term -> Type -> m Component
newComponent :: forall (m :: * -> *).
MonadFresh VerboseLevel m =>
[MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> m Component
newComponent [MetaId]
metaIds VerboseLevel
cost Maybe Name
mName VerboseLevel
pars Term
term Type
typ = m VerboseLevel
forall i (m :: * -> *). MonadFresh i m => m i
fresh m VerboseLevel -> (VerboseLevel -> Component) -> m Component
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \VerboseLevel
cId -> VerboseLevel
-> [MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> Component
mkComponent VerboseLevel
cId [MetaId]
metaIds VerboseLevel
cost Maybe Name
mName VerboseLevel
pars Term
term Type
typ
newComponentQ :: MonadFresh CompId m => [MetaId] -> Cost -> QName -> Nat -> Term -> Type -> m Component
newComponentQ :: forall (m :: * -> *).
MonadFresh VerboseLevel m =>
[MetaId]
-> VerboseLevel
-> QName
-> VerboseLevel
-> Term
-> Type
-> m Component
newComponentQ [MetaId]
metaIds VerboseLevel
cost QName
qname VerboseLevel
pars Term
term Type
typ = m VerboseLevel
forall i (m :: * -> *). MonadFresh i m => m i
fresh m VerboseLevel -> (VerboseLevel -> Component) -> m Component
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \VerboseLevel
cId -> VerboseLevel
-> [MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> Component
mkComponent VerboseLevel
cId [MetaId]
metaIds VerboseLevel
cost (Name -> Maybe Name
forall a. a -> Maybe a
Just (Name -> Maybe Name) -> Name -> Maybe Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
qname) VerboseLevel
pars Term
term Type
typ
addCost :: Cost -> Component -> Component
addCost :: VerboseLevel -> Component -> Component
addCost VerboseLevel
cost Component
comp = Component
comp { compCost = cost + compCost comp }
addBranchGoals :: [Goal] -> SearchBranch -> SearchBranch
addBranchGoals :: [Goal] -> SearchBranch -> SearchBranch
addBranchGoals [Goal]
goals SearchBranch
branch = SearchBranch
branch {sbGoals = goals ++ sbGoals branch}
withBranchState :: SearchBranch -> SM a -> SM a
withBranchState :: forall a. SearchBranch -> SM a -> SM a
withBranchState SearchBranch
br SM a
ma = do
TCState -> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC (SearchBranch -> TCState
sbTCState SearchBranch
br)
SM a
ma
withBranchAndGoal :: SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal :: forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
br Goal
goal SM a
ma = Goal -> SM a -> SM a
forall a. Goal -> SM a -> SM a
inGoalEnv Goal
goal (SM a -> SM a) -> SM a -> SM a
forall a b. (a -> b) -> a -> b
$ SearchBranch -> SM a -> SM a
forall a. SearchBranch -> SM a -> SM a
withBranchState SearchBranch
br SM a
ma
inGoalEnv :: Goal -> SM a -> SM a
inGoalEnv :: forall a. Goal -> SM a -> SM a
inGoalEnv Goal
goal = MetaId
-> ReaderT SearchOptions (TCMT IO) a
-> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
ReadTCState m) =>
MetaId -> m a -> m a
withMetaId (Goal -> MetaId
goalMeta Goal
goal)
nextBranchMeta' :: SearchBranch -> SM (Goal, SearchBranch)
nextBranchMeta' :: SearchBranch -> SM (Goal, SearchBranch)
nextBranchMeta' = (Maybe (Goal, SearchBranch) -> (Goal, SearchBranch))
-> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch))
-> SM (Goal, SearchBranch)
forall a b.
(a -> b)
-> ReaderT SearchOptions (TCMT IO) a
-> ReaderT SearchOptions (TCMT IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Goal, SearchBranch)
-> Maybe (Goal, SearchBranch) -> (Goal, SearchBranch)
forall a. a -> Maybe a -> a
fromMaybe (Goal, SearchBranch)
forall a. HasCallStack => a
__IMPOSSIBLE__) (ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch))
-> SM (Goal, SearchBranch))
-> (SearchBranch
-> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch)))
-> SearchBranch
-> SM (Goal, SearchBranch)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchBranch
-> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch))
nextBranchMeta
nextBranchMeta :: SearchBranch -> SM (Maybe (Goal, SearchBranch))
nextBranchMeta :: SearchBranch
-> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch))
nextBranchMeta SearchBranch
branch = case SearchBranch -> [Goal]
sbGoals SearchBranch
branch of
[] -> Maybe (Goal, SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch))
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Goal, SearchBranch)
forall a. Maybe a
Nothing
(Goal
goal : [Goal]
goals) ->
Maybe (Goal, SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch))
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Goal, SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch)))
-> Maybe (Goal, SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe (Goal, SearchBranch))
forall a b. (a -> b) -> a -> b
$ (Goal, SearchBranch) -> Maybe (Goal, SearchBranch)
forall a. a -> Maybe a
Just (Goal
goal, SearchBranch
branch{sbGoals=goals})
getMetaInstantiation :: (MonadTCM tcm, PureTCM tcm, MonadDebug tcm, MonadInteractionPoints tcm, MonadFresh NameId tcm)
=> MetaId -> tcm (Maybe Expr)
getMetaInstantiation :: forall (tcm :: * -> *).
(MonadTCM tcm, PureTCM tcm, MonadDebug tcm,
MonadInteractionPoints tcm, MonadFresh NameId tcm) =>
MetaId -> tcm (Maybe Expr)
getMetaInstantiation = MetaId -> tcm (Maybe Term)
forall (tcm :: * -> *).
(MonadTCM tcm, MonadDebug tcm, ReadTCState tcm) =>
MetaId -> tcm (Maybe Term)
metaInstantiation (MetaId -> tcm (Maybe Term))
-> (Maybe Term -> tcm (Maybe Expr)) -> MetaId -> tcm (Maybe Expr)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Maybe Term -> tcm (Maybe Expr)
Maybe Term -> tcm (Maybe (ReifiesTo Term))
forall {m :: * -> *} {a}.
(InstantiateFull a, Reify a, PureTCM m, MonadInteractionPoints m,
MonadFresh NameId m) =>
Maybe a -> m (Maybe (ReifiesTo a))
go
where
go :: Maybe a -> m (Maybe (ReifiesTo a))
go Maybe a
Nothing = Maybe (ReifiesTo a) -> m (Maybe (ReifiesTo a))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (ReifiesTo a)
forall a. Maybe a
Nothing
go (Just a
term) = do
expr <- a -> m a
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull a
term m a -> (a -> m (ReifiesTo a)) -> m (ReifiesTo a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> m (ReifiesTo a)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => a -> m (ReifiesTo a)
reify
return $ Just expr
metaInstantiation :: (MonadTCM tcm, MonadDebug tcm, ReadTCState tcm) => MetaId -> tcm (Maybe Term)
metaInstantiation :: forall (tcm :: * -> *).
(MonadTCM tcm, MonadDebug tcm, ReadTCState tcm) =>
MetaId -> tcm (Maybe Term)
metaInstantiation MetaId
metaId = MetaId -> tcm MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
metaId tcm MetaVariable
-> (MetaVariable -> MetaInstantiation) -> tcm MetaInstantiation
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> MetaVariable -> MetaInstantiation
mvInstantiation tcm MetaInstantiation
-> (MetaInstantiation -> tcm (Maybe Term)) -> tcm (Maybe Term)
forall a b. tcm a -> (a -> tcm b) -> tcm b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
InstV Instantiation
inst -> Maybe Term -> tcm (Maybe Term)
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term -> tcm (Maybe Term)) -> Maybe Term -> tcm (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Instantiation -> Term
instBody Instantiation
inst
MetaInstantiation
_ -> Maybe Term -> tcm (Maybe Term)
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
forall a. Maybe a
Nothing
isTypeDatatype :: (MonadTCM tcm, MonadReduce tcm, HasConstInfo tcm) => Type -> tcm Bool
isTypeDatatype :: forall (tcm :: * -> *).
(MonadTCM tcm, MonadReduce tcm, HasConstInfo tcm) =>
Type -> tcm Bool
isTypeDatatype Type
typ = do
typ' <- Type -> tcm Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
typ
case unEl typ' of
Def QName
qname Elims
_ -> Definition -> Defn
theDef (Definition -> Defn) -> tcm Definition -> tcm Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> tcm Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qname tcm Defn -> (Defn -> tcm Bool) -> tcm Bool
forall a b. tcm a -> (a -> tcm b) -> tcm b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Datatype{} -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Defn
_ -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Term
_ -> Bool -> tcm Bool
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
collectComponents :: Options -> Costs -> InteractionId -> Maybe QName -> [QName] -> MetaId -> TCM BaseComponents
collectComponents :: Options
-> Costs
-> InteractionId
-> Maybe QName
-> [QName]
-> MetaId
-> TCM BaseComponents
collectComponents Options
opts Costs
costs InteractionId
ii Maybe QName
mDefName [QName]
whereNames MetaId
metaId = do
lhsVars' <- InteractionId -> TCMT IO (Open [(Term, Maybe VerboseLevel)])
forall (tcm :: * -> *).
(MonadFail tcm, ReadTCState tcm, MonadError TCErr tcm,
MonadTCM tcm, HasConstInfo tcm) =>
InteractionId -> tcm (Open [(Term, Maybe VerboseLevel)])
collectLHSVars InteractionId
ii
let recVars = Open [(Term, Maybe VerboseLevel)]
lhsVars' Open [(Term, Maybe VerboseLevel)]
-> ([(Term, Maybe VerboseLevel)]
-> [(Term, NoSubst Term VerboseLevel)])
-> Open [(Term, NoSubst Term VerboseLevel)]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ [(Term, Maybe VerboseLevel)]
vars -> [ (Term
tm, VerboseLevel -> NoSubst Term VerboseLevel
forall t a. a -> NoSubst t a
NoSubst VerboseLevel
i) | (Term
tm, Just VerboseLevel
i) <- [(Term, Maybe VerboseLevel)]
vars ]
lhsVars <- getOpen $ map fst <$> lhsVars'
typedLocals <- getLocalVarTerms 0
reportSDoc "mimer.components" 40 $ "All LHS variables:" <+> prettyTCM lhsVars <+> parens ("or" <+> pretty lhsVars)
let typedLhsVars = ((Term, Dom Type) -> Bool)
-> [(Term, Dom Type)] -> [(Term, Dom Type)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Term
term,Dom Type
typ) -> Term
term Term -> [Term] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Term]
lhsVars) [(Term, Dom Type)]
typedLocals
reportSDoc "mimer.components" 40 $
"LHS variables with types:" <+> prettyList (map prettyTCMTypedTerm typedLhsVars) <+> parens ("or"
<+> prettyList (map prettyTypedTerm typedLhsVars))
splitVarsTyped <- filterM (\(Term
term, Dom Type
typ) ->
((ArgInfo -> Hiding
argInfoHiding (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
typ) Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
NotHidden) Bool -> Bool -> Bool
&&) (Bool -> Bool) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM Bool
forall (tcm :: * -> *).
(MonadTCM tcm, MonadReduce tcm, HasConstInfo tcm) =>
Type -> tcm Bool
isTypeDatatype (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
typ))
typedLhsVars
reportSDoc "mimer.components" 40 $
"Splittable variables" <+> prettyList (map prettyTCMTypedTerm splitVarsTyped) <+> parens ("or"
<+> prettyList (map prettyTypedTerm splitVarsTyped))
splitVars <- makeOpen $ map fst splitVarsTyped
letVars <- getLetVars (costLet costs)
let components = BaseComponents
{ hintFns :: [Component]
hintFns = []
, hintDataTypes :: [Component]
hintDataTypes = []
, hintRecordTypes :: [Component]
hintRecordTypes = []
, hintProjections :: [Component]
hintProjections = []
, hintAxioms :: [Component]
hintAxioms = []
, hintLevel :: [Component]
hintLevel = []
, hintThisFn :: Maybe Component
hintThisFn = Maybe Component
forall a. Maybe a
Nothing
, hintRecVars :: Open [(Term, NoSubst Term VerboseLevel)]
hintRecVars = Open [(Term, NoSubst Term VerboseLevel)]
recVars
, hintLetVars :: [Open Component]
hintLetVars = [Open Component]
letVars
, hintSplitVars :: Open [Term]
hintSplitVars = Open [Term]
splitVars
}
metaVar <- lookupLocalMeta metaId
hintNames <- getEverythingInScope metaVar
components' <- foldM go components $ explicitHints ++ (hintNames \\ explicitHints)
return BaseComponents
{ hintFns = doSort $ hintFns components'
, hintDataTypes = doSort $ hintDataTypes components'
, hintRecordTypes = doSort $ hintRecordTypes components'
, hintProjections = doSort $ hintProjections components'
, hintAxioms = doSort $ hintAxioms components'
, hintLevel = doSort $ hintLevel components'
, hintThisFn = hintThisFn components'
, hintRecVars = recVars
, hintLetVars = letVars
, hintSplitVars = splitVars
}
where
hintMode :: HintMode
hintMode = Options -> HintMode
optHintMode Options
opts
explicitHints :: [QName]
explicitHints = Options -> [QName]
optExplicitHints Options
opts
doSort :: [Component] -> [Component]
doSort = (Component -> VerboseLevel) -> [Component] -> [Component]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Type -> VerboseLevel
arity (Type -> VerboseLevel)
-> (Component -> Type) -> Component -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Component -> Type
compType)
isNotMutual :: QName -> Defn -> Bool
isNotMutual QName
qname Defn
f = case Maybe QName
mDefName of
Maybe QName
Nothing -> Bool
True
Just QName
defName -> QName
defName QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
/= QName
qname Bool -> Bool -> Bool
&& ([QName] -> Bool) -> Maybe [QName] -> Maybe Bool
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((QName
defName QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`)) (Defn -> Maybe [QName]
funMutual Defn
f) Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
go :: BaseComponents -> QName -> TCM BaseComponents
go BaseComponents
comps QName
qname = do
info <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qname
typ <- typeOfConst qname
scope <- getScope
let addLevel = VerboseLevel -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
MonadTCM tcm) =>
VerboseLevel -> QName -> tcm Component
qnameToComponent (Costs -> VerboseLevel
costLevel Costs
costs) QName
qname TCMT IO Component
-> (Component -> BaseComponents) -> TCM BaseComponents
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Component
comp -> BaseComponents
comps{hintLevel = comp : hintLevel comps}
addAxiom = VerboseLevel -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
MonadTCM tcm) =>
VerboseLevel -> QName -> tcm Component
qnameToComponent (Costs -> VerboseLevel
costAxiom Costs
costs) QName
qname TCMT IO Component
-> (Component -> BaseComponents) -> TCM BaseComponents
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Component
comp -> BaseComponents
comps{hintAxioms = comp : hintAxioms comps}
addThisFn = VerboseLevel -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
MonadTCM tcm) =>
VerboseLevel -> QName -> tcm Component
qnameToComponent (Costs -> VerboseLevel
costRecCall Costs
costs) QName
qname TCMT IO Component
-> (Component -> BaseComponents) -> TCM BaseComponents
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Component
comp -> BaseComponents
comps{hintThisFn = Just comp{ compRec = True }}
addFn = VerboseLevel -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
MonadTCM tcm) =>
VerboseLevel -> QName -> tcm Component
qnameToComponent (Costs -> VerboseLevel
costFn Costs
costs) QName
qname TCMT IO Component
-> (Component -> BaseComponents) -> TCM BaseComponents
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Component
comp -> BaseComponents
comps{hintFns = comp : hintFns comps}
addData = VerboseLevel -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
MonadTCM tcm) =>
VerboseLevel -> QName -> tcm Component
qnameToComponent (Costs -> VerboseLevel
costSet Costs
costs) QName
qname TCMT IO Component
-> (Component -> BaseComponents) -> TCM BaseComponents
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Component
comp -> BaseComponents
comps{hintDataTypes = comp : hintDataTypes comps}
case theDef info of
Axiom{} | Type -> Bool
isToLevel Type
typ -> TCM BaseComponents
addLevel
| ScopeInfo -> Bool
shouldKeep ScopeInfo
scope -> TCM BaseComponents
addAxiom
| Bool
otherwise -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
DataOrRecSig{} -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
Defn
GeneralizableVar -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
AbstractDefn{} -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
f :: Defn
f@Function{}
| QName -> Maybe QName
forall a. a -> Maybe a
Just QName
qname Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mDefName -> TCM BaseComponents
addThisFn
| Type -> Bool
isToLevel Type
typ Bool -> Bool -> Bool
&& QName -> Defn -> Bool
isNotMutual QName
qname Defn
f -> TCM BaseComponents
addLevel
| QName -> Defn -> Bool
isNotMutual QName
qname Defn
f Bool -> Bool -> Bool
&& ScopeInfo -> Bool
shouldKeep ScopeInfo
scope -> TCM BaseComponents
addFn
| Bool
otherwise -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
Datatype{} -> TCM BaseComponents
addData
Record{} -> do
projections <- (QName -> TCMT IO Component) -> [QName] -> TCMT IO [Component]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (VerboseLevel -> QName -> TCMT IO Component
forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
MonadTCM tcm) =>
VerboseLevel -> QName -> tcm Component
qnameToComponent (Costs -> VerboseLevel
costSpeculateProj Costs
costs)) ([QName] -> TCMT IO [Component])
-> TCMT IO [QName] -> TCMT IO [Component]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO [QName]
forall (tcm :: * -> *).
(HasConstInfo tcm, MonadTCM tcm) =>
QName -> tcm [QName]
getRecordFields QName
qname
comp <- qnameToComponent (costSet costs) qname
return comps{ hintRecordTypes = comp : hintRecordTypes comps
, hintProjections = projections ++ hintProjections comps }
Constructor{} -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
Primitive{} | Type -> Bool
isToLevel Type
typ -> TCM BaseComponents
addLevel
| ScopeInfo -> Bool
shouldKeep ScopeInfo
scope -> TCM BaseComponents
addFn
| Bool
otherwise -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
PrimitiveSort{} -> BaseComponents -> TCM BaseComponents
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return BaseComponents
comps
where
shouldKeep :: ScopeInfo -> Bool
shouldKeep ScopeInfo
scope = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or
[ QName
qname QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
explicitHints
, QName
qname QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
whereNames
, case HintMode
hintMode of
HintMode
Unqualified -> QName -> ScopeInfo -> Bool
Scope.isNameInScopeUnqualified QName
qname ScopeInfo
scope
HintMode
AllModules -> Bool
True
HintMode
Module -> ModuleName -> Maybe ModuleName
forall a. a -> Maybe a
Just (QName -> ModuleName
qnameModule QName
qname) Maybe ModuleName -> Maybe ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe ModuleName
mThisModule
HintMode
NoHints -> Bool
False
]
mThisModule :: Maybe ModuleName
mThisModule = QName -> ModuleName
qnameModule (QName -> ModuleName) -> Maybe QName -> Maybe ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe QName
mDefName
isToLevel :: Type -> Bool
isToLevel :: Type -> Bool
isToLevel Type
typ = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
typ of
Pi Dom Type
_ Abs Type
abs -> Type -> Bool
isToLevel (Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
abs)
Def QName
qname Elims
_ -> QName -> ArgName
forall a. Pretty a => a -> ArgName
P.prettyShow QName
qname ArgName -> ArgName -> Bool
forall a. Eq a => a -> a -> Bool
== ArgName
builtinLevelName
Term
_ -> Bool
False
prettyTCMTypedTerm :: (PrettyTCM tm, PrettyTCM ty) => (tm, ty) -> TCM Doc
prettyTCMTypedTerm :: forall tm ty.
(PrettyTCM tm, PrettyTCM ty) =>
(tm, ty) -> TCMT IO Doc
prettyTCMTypedTerm (tm
term, ty
typ) = tm -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => tm -> m Doc
prettyTCM tm
term TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ty -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ty -> m Doc
prettyTCM ty
typ
prettyTypedTerm :: (a, a) -> m Doc
prettyTypedTerm (a
term, a
typ) = a -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
term m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
typ
qnameToComponent :: (HasConstInfo tcm, ReadTCState tcm, MonadFresh CompId tcm, MonadTCM tcm)
=> Cost -> QName -> tcm Component
qnameToComponent :: forall (tcm :: * -> *).
(HasConstInfo tcm, ReadTCState tcm, MonadFresh VerboseLevel tcm,
MonadTCM tcm) =>
VerboseLevel -> QName -> tcm Component
qnameToComponent VerboseLevel
cost QName
qname = do
info <- QName -> tcm Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qname
typ <- typeOfConst qname
mParams <- freeVarsToApply qname
let def = (QName -> Elims -> Term
Def QName
qname [] Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Args
mParams, VerboseLevel
0)
(term, pars) = case theDef info of
c :: Defn
c@Constructor{} -> (ConHead -> ConInfo -> Elims -> Term
Con (Defn -> ConHead
conSrcCon Defn
c) ConInfo
ConOCon [], Defn -> VerboseLevel
conPars Defn
c VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- Args -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Args
mParams)
Axiom{} -> (Term, VerboseLevel)
def
Defn
GeneralizableVar -> (Term, VerboseLevel)
def
Function{} -> (Term, VerboseLevel)
def
Datatype{} -> (Term, VerboseLevel)
def
Record{} -> (Term, VerboseLevel)
def
Primitive{} -> (Term, VerboseLevel)
def
PrimitiveSort{} -> (Term, VerboseLevel)
def
DataOrRecSig{} -> (Term, VerboseLevel)
forall a. HasCallStack => a
__IMPOSSIBLE__
AbstractDefn{} -> (Term, VerboseLevel)
forall a. HasCallStack => a
__IMPOSSIBLE__
newComponentQ [] cost qname pars term typ
getEverythingInScope :: MonadTCM tcm => MetaVariable -> tcm [QName]
getEverythingInScope :: forall (tcm :: * -> *). MonadTCM tcm => MetaVariable -> tcm [QName]
getEverythingInScope MetaVariable
metaVar = do
let scope :: ScopeInfo
scope = Closure Range -> ScopeInfo
forall a. Closure a -> ScopeInfo
clScope (Closure Range -> ScopeInfo) -> Closure Range -> ScopeInfo
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Closure Range
getMetaInfo MetaVariable
metaVar
let nameSpace :: NameSpace
nameSpace = ScopeInfo -> NameSpace
Scope.everythingInScope ScopeInfo
scope
names :: NamesInScope
names = NameSpace -> NamesInScope
Scope.nsNames NameSpace
nameSpace
validKind :: KindOfName -> Bool
validKind = \ case
KindOfName
Scope.PatternSynName -> Bool
False
KindOfName
Scope.GeneralizeName -> Bool
False
KindOfName
Scope.DisallowedGeneralizeName -> Bool
False
KindOfName
Scope.MacroName -> Bool
False
KindOfName
Scope.QuotableName -> Bool
False
KindOfName
Scope.ConName -> Bool
True
KindOfName
Scope.CoConName -> Bool
True
KindOfName
Scope.FldName -> Bool
True
KindOfName
Scope.DataName -> Bool
True
KindOfName
Scope.RecName -> Bool
True
KindOfName
Scope.FunName -> Bool
True
KindOfName
Scope.AxiomName -> Bool
True
KindOfName
Scope.PrimName -> Bool
True
KindOfName
Scope.OtherDefName -> Bool
True
qnames :: [QName]
qnames = (AbstractName -> QName) -> [AbstractName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map AbstractName -> QName
Scope.anameName
([AbstractName] -> [QName])
-> ([NonEmpty AbstractName] -> [AbstractName])
-> [NonEmpty AbstractName]
-> [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName -> Bool) -> [AbstractName] -> [AbstractName]
forall a. (a -> Bool) -> [a] -> [a]
filter (KindOfName -> Bool
validKind (KindOfName -> Bool)
-> (AbstractName -> KindOfName) -> AbstractName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
Scope.anameKind)
([AbstractName] -> [AbstractName])
-> ([NonEmpty AbstractName] -> [AbstractName])
-> [NonEmpty AbstractName]
-> [AbstractName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty AbstractName -> AbstractName)
-> [NonEmpty AbstractName] -> [AbstractName]
forall a b. (a -> b) -> [a] -> [b]
map NonEmpty AbstractName -> AbstractName
forall a. NonEmpty a -> a
NonEmptyList.head
([NonEmpty AbstractName] -> [QName])
-> [NonEmpty AbstractName] -> [QName]
forall a b. (a -> b) -> a -> b
$ NamesInScope -> [NonEmpty AbstractName]
forall k a. Map k a -> [a]
Map.elems NamesInScope
names
[QName] -> tcm [QName]
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return [QName]
qnames
getLetVars :: (MonadFresh CompId tcm, MonadTCM tcm, Monad tcm) => Cost -> tcm [Open Component]
getLetVars :: forall (tcm :: * -> *).
(MonadFresh VerboseLevel tcm, MonadTCM tcm, Monad tcm) =>
VerboseLevel -> tcm [Open Component]
getLetVars VerboseLevel
cost = do
bindings <- (TCEnv -> LetBindings) -> tcm LetBindings
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> LetBindings
envLetBindings
mapM makeComp $ Map.toAscList bindings
where
makeComp :: (Name, Open LetBinding) -> tcm (Open Component)
makeComp (Name
name, Open LetBinding
opn) = do
cId <- tcm VerboseLevel
forall i (m :: * -> *). MonadFresh i m => m i
fresh
return $ opn <&> \ (LetBinding Origin
_ Term
term Dom Type
typ) ->
VerboseLevel
-> [MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> Component
mkComponent VerboseLevel
cId [] VerboseLevel
cost (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
name) VerboseLevel
0 Term
term (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
typ)
builtinLevelName :: String
builtinLevelName :: ArgName
builtinLevelName = ArgName
"Agda.Primitive.Level"
collectLHSVars :: (MonadFail tcm, ReadTCState tcm, MonadError TCErr tcm, MonadTCM tcm, HasConstInfo tcm)
=> InteractionId -> tcm (Open [(Term, Maybe Int)])
collectLHSVars :: forall (tcm :: * -> *).
(MonadFail tcm, ReadTCState tcm, MonadError TCErr tcm,
MonadTCM tcm, HasConstInfo tcm) =>
InteractionId -> tcm (Open [(Term, Maybe VerboseLevel)])
collectLHSVars InteractionId
ii = do
ipc <- InteractionPoint -> IPClause
ipClause (InteractionPoint -> IPClause)
-> tcm InteractionPoint -> tcm IPClause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionId -> tcm InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
case ipc of
IPClause
IPNoClause -> [(Term, Maybe VerboseLevel)]
-> tcm (Open [(Term, Maybe VerboseLevel)])
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
a -> m (Open a)
makeOpen []
IPClause{ipcQName :: IPClause -> QName
ipcQName = QName
fnName, ipcClauseNo :: IPClause -> VerboseLevel
ipcClauseNo = VerboseLevel
clauseNr} -> do
info <- QName -> tcm Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
fnName
typ <- typeOfConst fnName
parCount <- liftTCM getCurrentModuleFreeVars
case theDef info of
fnDef :: Defn
fnDef@Function{} -> do
let clause :: Clause
clause = Defn -> [Clause]
funClauses Defn
fnDef [Clause] -> VerboseLevel -> Clause
forall a. HasCallStack => [a] -> VerboseLevel -> a
!! VerboseLevel
clauseNr
naps :: NAPs
naps = Clause -> NAPs
namedClausePats Clause
clause
iTel <- tcm Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
let cTel = Clause -> Telescope
clauseTel Clause
clause
let shift = [Arg ArgName] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length (Telescope -> [Arg ArgName]
forall a. TelToArgs a => a -> [Arg ArgName]
telToArgs Telescope
iTel) VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- [Arg ArgName] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length (Telescope -> [Arg ArgName]
forall a. TelToArgs a => a -> [Arg ArgName]
telToArgs Telescope
cTel)
reportSDoc "mimer" 60 $ vcat
[ "Tel:"
, nest 2 $ pretty iTel $$ prettyTCM iTel
, "CTel:"
, nest 2 $ pretty cTel $$ prettyTCM cTel
]
reportSDoc "mimer" 60 $ "Shift:" <+> pretty shift
makeOpen [ (Var (n + shift) [], (i - parCount) <$ guard underCon)
| (i, nap) <- zip [0..] naps
, (n, underCon) <- go False $ namedThing $ unArg nap
]
Defn
_ -> do
[(Term, Maybe VerboseLevel)]
-> tcm (Open [(Term, Maybe VerboseLevel)])
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
a -> m (Open a)
makeOpen []
where
go :: Bool -> DeBruijnPattern -> [(VerboseLevel, Bool)]
go Bool
isUnderCon = \case
VarP PatternInfo
patInf DBPatVar
x -> [(DBPatVar -> VerboseLevel
dbPatVarIndex DBPatVar
x, Bool
isUnderCon)]
DotP PatternInfo
patInf Term
t -> []
ConP ConHead
conHead ConPatternInfo
conPatInf NAPs
namedArgs -> (NamedArg DeBruijnPattern -> [(VerboseLevel, Bool)])
-> NAPs -> [(VerboseLevel, Bool)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool -> DeBruijnPattern -> [(VerboseLevel, Bool)]
go Bool
True (DeBruijnPattern -> [(VerboseLevel, Bool)])
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> [(VerboseLevel, Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern
forall e. Arg e -> e
unArg) NAPs
namedArgs
LitP{} -> []
ProjP{} -> []
IApplyP{} -> []
DefP{} -> []
declarationQnames :: A.Declaration -> [QName]
declarationQnames :: Declaration -> [QName]
declarationQnames Declaration
dec = [ QName
q | Scope.WithKind KindOfName
_ QName
q <- Declaration -> [KName]
forall m. Collection KName m => Declaration -> m
forall a m. (DeclaredNames a, Collection KName m) => a -> m
A.declaredNames Declaration
dec ]
data MimerStats = MimerStats
{ MimerStats -> VerboseLevel
statCompHit :: Nat
, MimerStats -> VerboseLevel
statCompGen :: Nat
, MimerStats -> VerboseLevel
statCompRegen :: Nat
, MimerStats -> VerboseLevel
statCompNoRegen :: Nat
, MimerStats -> VerboseLevel
statMetasCreated :: Nat
, MimerStats -> VerboseLevel
statTypeEqChecks :: Nat
, MimerStats -> VerboseLevel
statRefineSuccess :: Nat
, MimerStats -> VerboseLevel
statRefineFail :: Nat
} deriving (VerboseLevel -> MimerStats -> ArgName -> ArgName
[MimerStats] -> ArgName -> ArgName
MimerStats -> ArgName
(VerboseLevel -> MimerStats -> ArgName -> ArgName)
-> (MimerStats -> ArgName)
-> ([MimerStats] -> ArgName -> ArgName)
-> Show MimerStats
forall a.
(VerboseLevel -> a -> ArgName -> ArgName)
-> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
$cshowsPrec :: VerboseLevel -> MimerStats -> ArgName -> ArgName
showsPrec :: VerboseLevel -> MimerStats -> ArgName -> ArgName
$cshow :: MimerStats -> ArgName
show :: MimerStats -> ArgName
$cshowList :: [MimerStats] -> ArgName -> ArgName
showList :: [MimerStats] -> ArgName -> ArgName
Show, MimerStats -> MimerStats -> Bool
(MimerStats -> MimerStats -> Bool)
-> (MimerStats -> MimerStats -> Bool) -> Eq MimerStats
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MimerStats -> MimerStats -> Bool
== :: MimerStats -> MimerStats -> Bool
$c/= :: MimerStats -> MimerStats -> Bool
/= :: MimerStats -> MimerStats -> Bool
Eq, (forall x. MimerStats -> Rep MimerStats x)
-> (forall x. Rep MimerStats x -> MimerStats) -> Generic MimerStats
forall x. Rep MimerStats x -> MimerStats
forall x. MimerStats -> Rep MimerStats x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MimerStats -> Rep MimerStats x
from :: forall x. MimerStats -> Rep MimerStats x
$cto :: forall x. Rep MimerStats x -> MimerStats
to :: forall x. Rep MimerStats x -> MimerStats
Generic)
instance NFData MimerStats
emptyMimerStats :: MimerStats
emptyMimerStats :: MimerStats
emptyMimerStats = MimerStats
{ statCompHit :: VerboseLevel
statCompHit = VerboseLevel
0, statCompGen :: VerboseLevel
statCompGen = VerboseLevel
0, statCompRegen :: VerboseLevel
statCompRegen = VerboseLevel
0 , statCompNoRegen :: VerboseLevel
statCompNoRegen = VerboseLevel
0 , statMetasCreated :: VerboseLevel
statMetasCreated = VerboseLevel
0, statTypeEqChecks :: VerboseLevel
statTypeEqChecks = VerboseLevel
0, statRefineSuccess :: VerboseLevel
statRefineSuccess = VerboseLevel
0 , statRefineFail :: VerboseLevel
statRefineFail = VerboseLevel
0}
incCompHit, incCompGen, incCompRegen, incCompNoRegen, incMetasCreated, incTypeEqChecks, incRefineSuccess, incRefineFail :: MimerStats -> MimerStats
incCompHit :: MimerStats -> MimerStats
incCompHit MimerStats
stats = MimerStats
stats {statCompHit = succ $ statCompHit stats}
incCompGen :: MimerStats -> MimerStats
incCompGen MimerStats
stats = MimerStats
stats {statCompGen = succ $ statCompGen stats}
incCompRegen :: MimerStats -> MimerStats
incCompRegen MimerStats
stats = MimerStats
stats {statCompRegen = succ $ statCompRegen stats}
incCompNoRegen :: MimerStats -> MimerStats
incCompNoRegen MimerStats
stats = MimerStats
stats {statCompNoRegen = succ $ statCompNoRegen stats}
incMetasCreated :: MimerStats -> MimerStats
incMetasCreated MimerStats
stats = MimerStats
stats {statMetasCreated = succ $ statMetasCreated stats}
incTypeEqChecks :: MimerStats -> MimerStats
incTypeEqChecks MimerStats
stats = MimerStats
stats {statTypeEqChecks = succ $ statTypeEqChecks stats}
incRefineSuccess :: MimerStats -> MimerStats
incRefineSuccess MimerStats
stats = MimerStats
stats {statRefineSuccess = succ $ statRefineSuccess stats}
incRefineFail :: MimerStats -> MimerStats
incRefineFail MimerStats
stats = MimerStats
stats {statRefineFail = succ $ statRefineFail stats}
updateStat :: (MimerStats -> MimerStats) -> SM ()
updateStat :: (MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
updateStat MimerStats -> MimerStats
f = ArgName
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) ()
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> m () -> m ()
verboseS ArgName
"mimer.stats" VerboseLevel
10 (ReaderT SearchOptions (TCMT IO) ()
-> ReaderT SearchOptions (TCMT IO) ())
-> ReaderT SearchOptions (TCMT IO) ()
-> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ do
ref <- (SearchOptions -> IORef MimerStats)
-> ReaderT SearchOptions (TCMT IO) (IORef MimerStats)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> IORef MimerStats
searchStats
liftIO $ modifyIORef' ref f
runSearch :: Rewrite -> Options -> InteractionId -> Range -> TCM [MimerResult]
runSearch :: Rewrite -> Options -> InteractionId -> Range -> TCM [MimerResult]
runSearch Rewrite
norm Options
options InteractionId
ii Range
rng = InteractionId -> TCM [MimerResult] -> TCM [MimerResult]
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM [MimerResult] -> TCM [MimerResult])
-> TCM [MimerResult] -> TCM [MimerResult]
forall a b. (a -> b) -> a -> b
$ do
(mTheFunctionQName, whereNames) <- (InteractionPoint -> IPClause)
-> TCMT IO InteractionPoint -> TCMT IO IPClause
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap InteractionPoint -> IPClause
ipClause (InteractionId -> TCMT IO InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii) TCMT IO IPClause
-> (IPClause -> (Maybe QName, [QName]))
-> TCMT IO (Maybe QName, [QName])
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
clause :: IPClause
clause@IPClause{} -> ( QName -> Maybe QName
forall a. a -> Maybe a
Just (QName -> Maybe QName) -> QName -> Maybe QName
forall a b. (a -> b) -> a -> b
$ IPClause -> QName
ipcQName IPClause
clause
, case WhereDeclarations -> Maybe Declaration
A.whereDecls (WhereDeclarations -> Maybe Declaration)
-> WhereDeclarations -> Maybe Declaration
forall a b. (a -> b) -> a -> b
$ Clause' SpineLHS -> WhereDeclarations
forall lhs. Clause' lhs -> WhereDeclarations
A.clauseWhereDecls (Clause' SpineLHS -> WhereDeclarations)
-> Clause' SpineLHS -> WhereDeclarations
forall a b. (a -> b) -> a -> b
$ IPClause -> Clause' SpineLHS
ipcClause IPClause
clause of
Just Declaration
decl -> Declaration -> [QName]
declarationQnames Declaration
decl
Maybe Declaration
_ -> []
)
IPClause
IPNoClause -> (Maybe QName
forall a. Maybe a
Nothing, [])
reportSDoc "mimer.init" 15 $ "Interaction point in function:" <+> pretty mTheFunctionQName
reportSDoc "mimer.init" 25 $ "Names in where-block" <+> pretty whereNames
metaId <- lookupInteractionId ii
metaVar <- lookupLocalMeta metaId
setMetaOccursCheck metaId DontRunMetaOccursCheck
metaIds <- case mvInstantiation metaVar of
InstV Instantiation
inst -> do
metaIds <- Term -> TCMT IO [MetaId]
forall t (tcm :: * -> *).
(AllMetas t, ReadTCState tcm) =>
t -> tcm [MetaId]
allOpenMetas (Instantiation -> Term
instBody Instantiation
inst)
reportSDoc "mimer.init" 20 $ sep [ "Interaction point already instantiated:" <+> pretty (instBody inst)
, "with args" <+> pretty (instTel inst) ]
return metaIds
OpenMeta MetaKind
UnificationMeta -> do
ArgName -> VerboseLevel -> ArgName -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> ArgName -> m ()
reportSLn ArgName
"mimer.init" VerboseLevel
20 ArgName
"Interaction point not instantiated."
[MetaId] -> TCMT IO [MetaId]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [MetaId
metaId]
MetaInstantiation
_ -> TCMT IO [MetaId]
forall a. HasCallStack => a
__IMPOSSIBLE__
reportSDoc "mimer.init" 20 $ "Remaining meta-variables to solve:" <+> prettyTCM metaIds
reportSDoc "mimer.init" 20 $ "Meta var args" <+> (prettyTCM =<< getMetaContextArgs metaVar)
fnArgs1 <- withShowAllArguments' False $ getContextArgs >>= mapM prettyTCM
fnArgs2 <- withShowAllArguments' True $ getContextArgs >>= mapM prettyTCM
let bringScope = ((Doc, Doc) -> Doc) -> [(Doc, Doc)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc, Doc) -> Doc
forall a b. (a, b) -> b
snd ([(Doc, Doc)] -> [Doc]) -> [(Doc, Doc)] -> [Doc]
forall a b. (a -> b) -> a -> b
$ ((Doc, Doc) -> Bool) -> [(Doc, Doc)] -> [(Doc, Doc)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Doc -> Doc -> Bool) -> (Doc, Doc) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Doc -> Doc -> Bool
forall a. Eq a => a -> a -> Bool
(/=)) ([(Doc, Doc)] -> [(Doc, Doc)]) -> [(Doc, Doc)] -> [(Doc, Doc)]
forall a b. (a -> b) -> a -> b
$ [Doc] -> [Doc] -> [(Doc, Doc)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Doc]
fnArgs1 [Doc]
fnArgs2
bringScopeNoBraces = (Doc -> ArgName) -> [Doc] -> [ArgName]
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> Bool) -> ArgName -> ArgName
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> ArgName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Char
'{', Char
'}']) (ArgName -> ArgName) -> (Doc -> ArgName) -> Doc -> ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> ArgName
forall a. Doc a -> ArgName
P.render) [Doc]
bringScope
reportSDoc "mimer.temp" 20 $ vcat
[ "Things to bring into scope:"
, nest 2 $ vcat
[ "Context args (don't show):" <+> pretty fnArgs1
, "Context args (show all): " <+> pretty fnArgs2
, "To bring into scope: " <+> pretty bringScope
, "To bring into scope (str):" <+> pretty bringScopeNoBraces
]
]
case metaIds of
[] -> do
case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
metaVar of
InstV Instantiation
inst -> do
expr <- InteractionId -> TCMT IO Expr -> TCMT IO Expr
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCMT IO Expr -> TCMT IO Expr) -> TCMT IO Expr -> TCMT IO Expr
forall a b. (a -> b) -> a -> b
$ do
metaArgs <- MetaVariable -> TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVariable
metaVar
instantiateFull (apply (MetaV metaId []) metaArgs) >>= normalForm norm >>= reify
str <- P.render <$> prettyTCM expr
let sol = ArgName -> MimerResult
MimerExpr ArgName
str
reportSDoc "mimer.init" 10 $ "Goal already solved. Solution:" <+> text str
return [sol]
MetaInstantiation
_ -> TCM [MimerResult]
forall a. HasCallStack => a
__IMPOSSIBLE__
[MetaId]
_ -> do
costs <- TCM Bool -> TCMT IO Costs -> TCMT IO Costs -> TCMT IO Costs
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (ArgName -> VerboseLevel -> TCM Bool
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> m Bool
hasVerbosity ArgName
"mimer.cost.custom" VerboseLevel
10)
TCMT IO Costs
customCosts
(Costs -> TCMT IO Costs
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Costs
defaultCosts)
reportSDoc "mimer.cost.custom" 10 $ "Using costs:" $$ nest 2 (pretty costs)
components <- collectComponents options costs ii mTheFunctionQName whereNames metaId
let startGoals = (MetaId -> Goal) -> [MetaId] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map MetaId -> Goal
Goal [MetaId]
metaIds
state <- getTC
env <- askTC
let startBranch = SearchBranch
{ sbTCState :: TCState
sbTCState = TCState
state
, sbGoals :: [Goal]
sbGoals = [Goal]
startGoals
, sbCost :: VerboseLevel
sbCost = VerboseLevel
0
, sbCache :: Map CheckpointId ComponentCache
sbCache = Map CheckpointId ComponentCache
forall k a. Map k a
Map.empty
, sbComponentsUsed :: Map Name VerboseLevel
sbComponentsUsed = Map Name VerboseLevel
forall k a. Map k a
Map.empty
}
statsRef <- liftIO $ newIORef emptyMimerStats
checkpoint <- viewTC eCurrentCheckpoint
let searchOptions = SearchOptions
{ searchBaseComponents :: BaseComponents
searchBaseComponents = BaseComponents
components
, searchHintMode :: HintMode
searchHintMode = Options -> HintMode
optHintMode Options
options
, searchTimeout :: Integer
searchTimeout = Options -> Integer
optTimeout Options
options
, searchGenProjectionsLocal :: Bool
searchGenProjectionsLocal = Bool
True
, searchGenProjectionsLet :: Bool
searchGenProjectionsLet = Bool
True
, searchGenProjectionsExternal :: Bool
searchGenProjectionsExternal = Bool
False
, searchGenProjectionsRec :: Bool
searchGenProjectionsRec = Bool
True
, searchSpeculateProjections :: Bool
searchSpeculateProjections = Bool
True
, searchTopMeta :: MetaId
searchTopMeta = MetaId
metaId
, searchTopEnv :: TCEnv
searchTopEnv = TCEnv
env
, searchTopCheckpoint :: CheckpointId
searchTopCheckpoint = CheckpointId
checkpoint
, searchInteractionId :: InteractionId
searchInteractionId = InteractionId
ii
, searchFnName :: Maybe QName
searchFnName = Maybe QName
mTheFunctionQName
, searchCosts :: Costs
searchCosts = Costs
costs
, searchStats :: IORef MimerStats
searchStats = IORef MimerStats
statsRef
, searchRewrite :: Rewrite
searchRewrite = Rewrite
norm
}
reportSDoc "mimer.init" 20 $ "Using search options:" $$ nest 2 (prettyTCM searchOptions)
reportSDoc "mimer.init" 20 $ "Initial search branch:" $$ nest 2 (pretty startBranch)
flip runReaderT searchOptions $ bench [] $ do
timeout <- fromMilliseconds <$> asks searchTimeout
startTime <- liftIO getCPUTime
let go :: Int -> Int -> MinQueue SearchBranch -> SM ([MimerResult], Int)
go VerboseLevel
0 VerboseLevel
n MinQueue SearchBranch
_ = ([MimerResult], VerboseLevel) -> SM ([MimerResult], VerboseLevel)
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], VerboseLevel
n)
go VerboseLevel
need VerboseLevel
n MinQueue SearchBranch
branchQueue = case MinQueue SearchBranch
-> Maybe (SearchBranch, MinQueue SearchBranch)
forall a. Ord a => MinQueue a -> Maybe (a, MinQueue a)
Q.minView MinQueue SearchBranch
branchQueue of
Maybe (SearchBranch, MinQueue SearchBranch)
Nothing -> do
ArgName
-> VerboseLevel -> ArgName -> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> ArgName -> m ()
reportSLn ArgName
"mimer.search" VerboseLevel
30 (ArgName -> ReaderT SearchOptions (TCMT IO) ())
-> ArgName -> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ ArgName
"No remaining search branches."
([MimerResult], VerboseLevel) -> SM ([MimerResult], VerboseLevel)
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], VerboseLevel
n)
Just (SearchBranch
branch, MinQueue SearchBranch
branchQueue') -> do
time <- IO CPUTime -> ReaderT SearchOptions (TCMT IO) CPUTime
forall a. IO a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO CPUTime
forall (m :: * -> *). MonadIO m => m CPUTime
getCPUTime
mimerTrace 0 10 $ vcat
[ "Choosing branch"
, nest 2 $ sep
[ branchInstantiationDocCost branch <> ","
, nest 2 $ "metas:" <+> prettyTCM (map goalMeta $ sbGoals branch)
]
]
reportSDoc "mimer.search" 50 $ "Full branch:" <+> pretty branch
reportSMDoc "mimer.search" 50 $
"Instantiation of other branches:" <+> prettyList (map branchInstantiationDocCost $ Q.toAscList branchQueue')
let elapsed = CPUTime
time CPUTime -> CPUTime -> CPUTime
forall a. Num a => a -> a -> a
- CPUTime
startTime
if elapsed < timeout
then do
(newBranches, sols) <- refine branch >>= partitionStepResult
let branchQueue'' = (SearchBranch -> MinQueue SearchBranch -> MinQueue SearchBranch)
-> MinQueue SearchBranch -> [SearchBranch] -> MinQueue SearchBranch
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SearchBranch -> MinQueue SearchBranch -> MinQueue SearchBranch
forall a. Ord a => a -> MinQueue a -> MinQueue a
Q.insert MinQueue SearchBranch
branchQueue' [SearchBranch]
newBranches
reportSLn "mimer.search" 40 $ show (length sols) ++ " solutions found during cycle " ++ show (n + 1)
reportSMDoc "mimer.search" 45 $ "Solutions:" <+> prettyTCM sols
mimerTrace 0 40 $ vcat
[ "Cycle" <+> pretty (n + 1) <+> "branches"
, nest 2 $ vcat $ map branchInstantiationDocCost $ Q.toAscList branchQueue''
]
unless (null sols) $ mimerTrace 0 20 $ vcat
[ "Cycle" <+> pretty (n + 1) <+> "solutions"
, nest 2 $ vcat $ map prettyTCM sols
]
let sols' = VerboseLevel -> [MimerResult] -> [MimerResult]
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
need [MimerResult]
sols
mapFst (sols' ++) <$> go (need - length sols') (n + 1) branchQueue''
else do
reportSLn "mimer.search" 30 $ "Search time limit reached. Elapsed search time: " ++ show elapsed
return ([], n)
let numSolutions | Options -> Bool
optList Options
options = VerboseLevel
10 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ Options -> VerboseLevel
optSkip Options
options
| Bool
otherwise = VerboseLevel
1 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ Options -> VerboseLevel
optSkip Options
options
(sols, nrSteps) <- go numSolutions 0 $ Q.singleton startBranch
reportSLn "mimer.search" 20 $ "Search ended after " ++ show (nrSteps + 1) ++ " cycles"
reportSDoc "mimer.search" 15 $ "Solutions found: " <+> prettyList (map prettyTCM sols)
reportSMDoc "mimer.stats" 10 $ do
ref <- asks searchStats
stats <- liftIO $ readIORef ref
"Statistics:" <+> text (show stats)
return sols
tryComponents :: Goal -> Type -> SearchBranch -> [(Component, [Component])] -> SM [SearchStepResult]
tryComponents :: Goal
-> Type
-> SearchBranch
-> [(Component, [Component])]
-> SM [SearchStepResult]
tryComponents Goal
goal Type
goalType SearchBranch
branch [(Component, [Component])]
comps = SearchBranch
-> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
checkpoint <- Lens' TCEnv CheckpointId
-> ReaderT SearchOptions (TCMT IO) CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
Lens' TCEnv CheckpointId
eCurrentCheckpoint
let tryFor (Component
sourceComp, [Component]
comps') = do
let newCache :: ComponentCache
newCache = Component -> Maybe [Component] -> ComponentCache -> ComponentCache
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Component
sourceComp Maybe [Component]
forall a. Maybe a
Nothing (SearchBranch -> Map CheckpointId ComponentCache
sbCache SearchBranch
branch Map CheckpointId ComponentCache -> CheckpointId -> ComponentCache
forall k a. Ord k => Map k a -> k -> a
Map.! CheckpointId
checkpoint)
newBranches <- [Maybe SearchBranch] -> [SearchBranch]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe SearchBranch] -> [SearchBranch])
-> ReaderT SearchOptions (TCMT IO) [Maybe SearchBranch]
-> ReaderT SearchOptions (TCMT IO) [SearchBranch]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Component -> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch))
-> [Component]
-> ReaderT SearchOptions (TCMT IO) [Maybe SearchBranch]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Goal
-> Type
-> SearchBranch
-> Component
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
tryRefineWith Goal
goal Type
goalType SearchBranch
branch) [Component]
comps'
return $ map (\SearchBranch
br -> SearchBranch
br{sbCache = Map.insert checkpoint newCache (sbCache branch)}) newBranches
newBranches <- concatMapM tryFor comps
mapM checkSolved newBranches
prepareComponents :: Goal -> SearchBranch -> SM (SearchBranch, [(Component, [Component])])
prepareComponents :: Goal
-> SearchBranch -> SM (SearchBranch, [(Component, [Component])])
prepareComponents Goal
goal SearchBranch
branch = SearchBranch
-> Goal
-> SM (SearchBranch, [(Component, [Component])])
-> SM (SearchBranch, [(Component, [Component])])
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (SM (SearchBranch, [(Component, [Component])])
-> SM (SearchBranch, [(Component, [Component])]))
-> SM (SearchBranch, [(Component, [Component])])
-> SM (SearchBranch, [(Component, [Component])])
forall a b. (a -> b) -> a -> b
$ do
checkpoint <- Lens' TCEnv CheckpointId
-> ReaderT SearchOptions (TCMT IO) CheckpointId
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (CheckpointId -> f CheckpointId) -> TCEnv -> f TCEnv
Lens' TCEnv CheckpointId
eCurrentCheckpoint
comps <- case Map.lookup checkpoint (sbCache branch) of
Maybe ComponentCache
Nothing -> do
(MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
updateStat MimerStats -> MimerStats
incCompRegen
ArgName
-> VerboseLevel
-> TCMT IO Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"mimer.components" VerboseLevel
20 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
-> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"No cache found checkpoint:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> CheckpointId -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty CheckpointId
checkpoint
, VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"with context:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc)
-> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope) ]
comps <- ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
genComponents
reportSDoc "mimer.components" 20 $ "Generated" <+> pretty (sum $ map (length . snd) comps) <+> "components"
return comps
Just ComponentCache
cache -> ((Component, Maybe [Component])
-> ReaderT SearchOptions (TCMT IO) (Component, [Component]))
-> [(Component, Maybe [Component])]
-> ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Component, Maybe [Component])
-> ReaderT SearchOptions (TCMT IO) (Component, [Component])
prepare (ComponentCache -> [(Component, Maybe [Component])]
forall k a. Map k a -> [(k, a)]
Map.toAscList ComponentCache
cache)
let newCache = [(Component, Maybe [Component])] -> ComponentCache
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Component, Maybe [Component])] -> ComponentCache)
-> [(Component, Maybe [Component])] -> ComponentCache
forall a b. (a -> b) -> a -> b
$ ((Component, [Component]) -> (Component, Maybe [Component]))
-> [(Component, [Component])] -> [(Component, Maybe [Component])]
forall a b. (a -> b) -> [a] -> [b]
map (([Component] -> Maybe [Component])
-> (Component, [Component]) -> (Component, Maybe [Component])
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd [Component] -> Maybe [Component]
forall a. a -> Maybe a
Just) [(Component, [Component])]
comps
branch' <- updateBranch [] branch{sbCache = Map.insert checkpoint newCache (sbCache branch)}
return (branch', comps)
where
prepare :: (Component, Maybe [Component]) -> SM (Component, [Component])
prepare :: (Component, Maybe [Component])
-> ReaderT SearchOptions (TCMT IO) (Component, [Component])
prepare (Component
sourceComp, Just [Component]
comps) = do
(MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
updateStat MimerStats -> MimerStats
incCompNoRegen
(Component, [Component])
-> ReaderT SearchOptions (TCMT IO) (Component, [Component])
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Component
sourceComp, [Component]
comps)
prepare (Component
sourceComp, Maybe [Component]
Nothing) = do
(MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
updateStat MimerStats -> MimerStats
incCompRegen
(Component
sourceComp,) ([Component] -> (Component, [Component]))
-> ReaderT SearchOptions (TCMT IO) [Component]
-> ReaderT SearchOptions (TCMT IO) (Component, [Component])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Component -> ReaderT SearchOptions (TCMT IO) [Component]
genComponentsFrom Bool
True Component
sourceComp
localVarCount :: SM Int
localVarCount :: SM VerboseLevel
localVarCount = do
top <- (SearchOptions -> VerboseLevel) -> SM VerboseLevel
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((SearchOptions -> VerboseLevel) -> SM VerboseLevel)
-> (SearchOptions -> VerboseLevel) -> SM VerboseLevel
forall a b. (a -> b) -> a -> b
$ [ContextEntry] -> VerboseLevel
forall a. [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length ([ContextEntry] -> VerboseLevel)
-> (SearchOptions -> [ContextEntry])
-> SearchOptions
-> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> [ContextEntry]
envContext (TCEnv -> [ContextEntry])
-> (SearchOptions -> TCEnv) -> SearchOptions -> [ContextEntry]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> TCEnv
searchTopEnv
cur <- length <$> getContext
pure $ cur - top
genComponents :: SM [(Component, [Component])]
genComponents :: ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
genComponents = do
opts <- ReaderT SearchOptions (TCMT IO) SearchOptions
forall r (m :: * -> *). MonadReader r m => m r
ask
let comps = SearchOptions -> BaseComponents
searchBaseComponents SearchOptions
opts
n <- localVarCount
localVars <- lift (getLocalVars n (costLocal $ searchCosts opts))
>>= genAddSource (searchGenProjectionsLocal opts)
recCalls <- genAddSource (searchGenProjectionsRec opts) (maybeToList $ hintThisFn comps)
letVars <- mapM getOpenComponent (hintLetVars comps)
>>= genAddSource (searchGenProjectionsLet opts)
fns <- genAddSource (searchGenProjectionsExternal opts) (hintFns comps)
axioms <- genAddSource (searchGenProjectionsExternal opts) (hintAxioms comps)
return $ localVars ++ letVars ++ recCalls ++ fns ++ axioms
where
genAddSource :: Bool -> [Component] -> SM [(Component, [Component])]
genAddSource :: Bool
-> [Component]
-> ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
genAddSource Bool
genProj = (Component
-> ReaderT SearchOptions (TCMT IO) (Component, [Component]))
-> [Component]
-> ReaderT SearchOptions (TCMT IO) [(Component, [Component])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Component
comp -> (Component
comp,) ([Component] -> (Component, [Component]))
-> ReaderT SearchOptions (TCMT IO) [Component]
-> ReaderT SearchOptions (TCMT IO) (Component, [Component])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Component -> ReaderT SearchOptions (TCMT IO) [Component]
genComponentsFrom Bool
genProj Component
comp)
genComponentsFrom :: Bool
-> Component
-> SM [Component]
genComponentsFrom :: Bool -> Component -> ReaderT SearchOptions (TCMT IO) [Component]
genComponentsFrom Bool
appRecElims Component
origComp = do
comps <- if | Component -> Bool
compRec Component
origComp -> (Component -> ReaderT SearchOptions (TCMT IO) Component)
-> [Component] -> ReaderT SearchOptions (TCMT IO) [Component]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Maybe VerboseLevel
-> Component -> ReaderT SearchOptions (TCMT IO) Component
applyToMetasG Maybe VerboseLevel
forall a. Maybe a
Nothing) ([Component] -> ReaderT SearchOptions (TCMT IO) [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
-> ReaderT SearchOptions (TCMT IO) [Component]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Component -> ReaderT SearchOptions (TCMT IO) [Component]
genRecCalls Component
origComp
| Bool
otherwise -> (Component -> [Component] -> [Component]
forall a. a -> [a] -> [a]
:[]) (Component -> [Component])
-> ReaderT SearchOptions (TCMT IO) Component
-> ReaderT SearchOptions (TCMT IO) [Component]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe VerboseLevel
-> Component -> ReaderT SearchOptions (TCMT IO) Component
applyToMetasG Maybe VerboseLevel
forall a. Maybe a
Nothing Component
origComp
if appRecElims
then concat <$> mapM (applyProjections Set.empty) comps
else return comps
where
applyProjections :: Set QName -> Component -> SM [Component]
applyProjections :: Set QName
-> Component -> ReaderT SearchOptions (TCMT IO) [Component]
applyProjections Set QName
seenRecords Component
comp = do
projComps <- Type -> SM (Maybe (QName, Args, [QName], Bool))
getRecordInfo (Component -> Type
compType Component
comp) SM (Maybe (QName, Args, [QName], Bool))
-> (Maybe (QName, Args, [QName], Bool)
-> ReaderT SearchOptions (TCMT IO) [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe (QName, Args, [QName], Bool)
Nothing -> [Component] -> ReaderT SearchOptions (TCMT IO) [Component]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
Just (QName
recordName, Args
args, [QName]
fields, Bool
isRecursive)
| QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
recordName Set QName
seenRecords -> do
ArgName
-> VerboseLevel
-> TCMT IO Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"mimer.components" VerboseLevel
60 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
-> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Skipping projection because recursive record already seen:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
recordName
[Component] -> ReaderT SearchOptions (TCMT IO) [Component]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise -> do
let seenRecords' :: Set QName
seenRecords' = if Bool
isRecursive then QName -> Set QName -> Set QName
forall a. Ord a => a -> Set a -> Set a
Set.insert QName
recordName Set QName
seenRecords else Set QName
seenRecords
comps <- (QName -> ReaderT SearchOptions (TCMT IO) Component)
-> [QName] -> ReaderT SearchOptions (TCMT IO) [Component]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Args
-> Component -> QName -> ReaderT SearchOptions (TCMT IO) Component
applyProj Args
args Component
comp (QName -> ReaderT SearchOptions (TCMT IO) Component)
-> (Component -> ReaderT SearchOptions (TCMT IO) Component)
-> QName
-> ReaderT SearchOptions (TCMT IO) Component
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Maybe VerboseLevel
-> Component -> ReaderT SearchOptions (TCMT IO) Component
applyToMetasG Maybe VerboseLevel
forall a. Maybe a
Nothing) [QName]
fields
concatMapM (applyProjections seenRecords') comps
return $ comp : projComps
getRecordInfo :: Type
-> SM (Maybe ( QName
, Args
, [QName]
, Bool
))
getRecordInfo :: Type -> SM (Maybe (QName, Args, [QName], Bool))
getRecordInfo Type
typ = case Type -> Term
forall t a. Type'' t a -> a
unEl Type
typ of
Def QName
qname Elims
elims -> QName -> ReaderT SearchOptions (TCMT IO) (Maybe RecordData)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe RecordData)
isRecord QName
qname ReaderT SearchOptions (TCMT IO) (Maybe RecordData)
-> (Maybe RecordData -> SM (Maybe (QName, Args, [QName], Bool)))
-> SM (Maybe (QName, Args, [QName], Bool))
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe RecordData
Nothing -> Maybe (QName, Args, [QName], Bool)
-> SM (Maybe (QName, Args, [QName], Bool))
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Args, [QName], Bool)
forall a. Maybe a
Nothing
Just RecordData
defn -> do
fields <- QName -> ReaderT SearchOptions (TCMT IO) [QName]
forall (tcm :: * -> *).
(HasConstInfo tcm, MonadTCM tcm) =>
QName -> tcm [QName]
getRecordFields QName
qname
return $ Just (qname, argsFromElims elims, fields, recRecursive_ defn)
Term
_ -> Maybe (QName, Args, [QName], Bool)
-> SM (Maybe (QName, Args, [QName], Bool))
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Args, [QName], Bool)
forall a. Maybe a
Nothing
applyProj :: Args -> Component -> QName -> SM Component
applyProj :: Args
-> Component -> QName -> ReaderT SearchOptions (TCMT IO) Component
applyProj Args
recordArgs Component
comp' QName
qname = do
cost <- (SearchOptions -> VerboseLevel) -> SM VerboseLevel
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Costs -> VerboseLevel
costProj (Costs -> VerboseLevel)
-> (SearchOptions -> Costs) -> SearchOptions -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> Costs
searchCosts)
let newTerm = Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE (Component -> Term
compTerm Component
comp') [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
qname]
projType <- defType <$> getConstInfo qname
projTypeWithArgs <- piApplyM projType recordArgs
newType <- piApplyM projTypeWithArgs (compTerm comp')
newComponentQ (compMetas comp') (compCost comp' + cost) qname 0 newTerm newType
applyToMetasG
:: Maybe Nat
-> Component -> SM Component
applyToMetasG :: Maybe VerboseLevel
-> Component -> ReaderT SearchOptions (TCMT IO) Component
applyToMetasG (Just VerboseLevel
m) Component
comp | VerboseLevel
m VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
0 = Component -> ReaderT SearchOptions (TCMT IO) Component
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Component
comp
applyToMetasG Maybe VerboseLevel
maxArgs Component
comp = do
ctx <- ReaderT SearchOptions (TCMT IO) Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
compTyp <- reduce $ compType comp
case unEl compTyp of
Pi Dom Type
dom Abs Type
abs -> do
let domainType :: Type
domainType = Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom
(metaId, metaTerm) <- Type -> SM (MetaId, Term)
createMeta Type
domainType
let arg = Origin -> Arg Term -> Arg Term
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term
metaTerm Term -> Arg Type -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
dom
newType <- reduce =<< piApplyM (compType comp) metaTerm
let skip = Component -> VerboseLevel
compPars Component
comp
newTerm | VerboseLevel
skip VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0 = Component -> Term
compTerm Component
comp
| Bool
otherwise = Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply (Component -> Term
compTerm Component
comp) [Arg Term
arg]
cost <- asks $ (if getHiding arg == Hidden then costNewHiddenMeta else costNewMeta) . searchCosts
applyToMetasG (predNat <$> maxArgs)
comp{ compTerm = newTerm
, compType = newType
, compPars = predNat skip
, compMetas = metaId : compMetas comp
, compCost = cost + compCost comp
}
Term
_ ->
Component -> ReaderT SearchOptions (TCMT IO) Component
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Component
comp{compType = compTyp}
createMeta :: Type -> SM (MetaId, Term)
createMeta :: Type -> SM (MetaId, Term)
createMeta Type
typ = do
(metaId, metaTerm) <- RunMetaOccursCheck -> Comparison -> Type -> SM (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck Comparison
CmpLeq Type
typ
verboseS "mimer.stats" 20 $ updateStat incMetasCreated
reportSDoc "mimer.components" 80 $ do
"Created meta-variable (type in context):" <+> pretty metaTerm <+> ":" <+> (pretty =<< getMetaTypeInContext metaId)
return (metaId, metaTerm)
partitionStepResult :: [SearchStepResult] -> SM ([SearchBranch], [MimerResult])
partitionStepResult :: [SearchStepResult]
-> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
partitionStepResult [] = ([SearchBranch], [MimerResult])
-> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([],[])
partitionStepResult (SearchStepResult
x:[SearchStepResult]
xs) = do
let rest :: ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
rest = [SearchStepResult]
-> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
partitionStepResult [SearchStepResult]
xs
(brs',sols) <- ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
rest
case x of
SearchStepResult
NoSolution -> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
rest
OpenBranch SearchBranch
br -> ([SearchBranch], [MimerResult])
-> ReaderT SearchOptions (TCMT IO) ([SearchBranch], [MimerResult])
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SearchBranch
brSearchBranch -> [SearchBranch] -> [SearchBranch]
forall a. a -> [a] -> [a]
:[SearchBranch]
brs', [MimerResult]
sols)
ResultExpr Expr
exp -> do
str <- Doc -> ArgName
forall a. Doc a -> ArgName
P.render (Doc -> ArgName)
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ArgName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
exp
return $ (brs', MimerExpr str : sols)
ResultClauses [Clause]
cls -> do
f <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName)
-> ReaderT SearchOptions (TCMT IO) (Maybe QName)
-> ReaderT SearchOptions (TCMT IO) QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SearchOptions -> Maybe QName)
-> ReaderT SearchOptions (TCMT IO) (Maybe QName)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> Maybe QName
searchFnName
return $ (brs', MimerClauses f cls : sols)
topInstantiationDoc :: SM Doc
topInstantiationDoc :: ReaderT SearchOptions (TCMT IO) Doc
topInstantiationDoc = (SearchOptions -> MetaId) -> ReaderT SearchOptions (TCMT IO) MetaId
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> MetaId
searchTopMeta ReaderT SearchOptions (TCMT IO) MetaId
-> (MetaId -> ReaderT SearchOptions (TCMT IO) (Maybe Expr))
-> ReaderT SearchOptions (TCMT IO) (Maybe Expr)
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= MetaId -> ReaderT SearchOptions (TCMT IO) (Maybe Expr)
forall (tcm :: * -> *).
(MonadTCM tcm, PureTCM tcm, MonadDebug tcm,
MonadInteractionPoints tcm, MonadFresh NameId tcm) =>
MetaId -> tcm (Maybe Expr)
getMetaInstantiation ReaderT SearchOptions (TCMT IO) (Maybe Expr)
-> (Maybe Expr -> ReaderT SearchOptions (TCMT IO) Doc)
-> ReaderT SearchOptions (TCMT IO) Doc
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ReaderT SearchOptions (TCMT IO) Doc
-> (Expr -> ReaderT SearchOptions (TCMT IO) Doc)
-> Maybe Expr
-> ReaderT SearchOptions (TCMT IO) Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Doc -> ReaderT SearchOptions (TCMT IO) Doc
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
"(nothing)") Expr -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM
prettyGoalInst :: Goal -> SM Doc
prettyGoalInst :: Goal -> ReaderT SearchOptions (TCMT IO) Doc
prettyGoalInst Goal
goal = Goal
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall a. Goal -> SM a -> SM a
inGoalEnv Goal
goal (ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc)
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$ do
args <- (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Elims)
-> ReaderT SearchOptions (TCMT IO) Args
-> ReaderT SearchOptions (TCMT IO) Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT SearchOptions (TCMT IO) Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
prettyTCM =<< instantiate (MetaV (goalMeta goal) args)
branchInstantiationDocCost :: SearchBranch -> SM Doc
branchInstantiationDocCost :: SearchBranch -> ReaderT SearchOptions (TCMT IO) Doc
branchInstantiationDocCost SearchBranch
branch = SearchBranch -> ReaderT SearchOptions (TCMT IO) Doc
branchInstantiationDoc SearchBranch
branch ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (ReaderT SearchOptions (TCMT IO) Doc
"cost:" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseLevel -> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (SearchBranch -> VerboseLevel
sbCost SearchBranch
branch))
branchInstantiationDoc :: SearchBranch -> SM Doc
branchInstantiationDoc :: SearchBranch -> ReaderT SearchOptions (TCMT IO) Doc
branchInstantiationDoc SearchBranch
branch = SearchBranch
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall a. SearchBranch -> SM a -> SM a
withBranchState SearchBranch
branch ReaderT SearchOptions (TCMT IO) Doc
topInstantiationDoc
refine :: SearchBranch -> SM [SearchStepResult]
refine :: SearchBranch -> SM [SearchStepResult]
refine SearchBranch
branch = SearchBranch -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> SM a -> SM a
withBranchState SearchBranch
branch (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
(goal1, branch1) <- SearchBranch -> SM (Goal, SearchBranch)
nextBranchMeta' SearchBranch
branch
withBranchAndGoal branch1 goal1 $ do
goalType1 <- bench [Bench.Reduce] $ reduce =<< getMetaTypeInContext (goalMeta goal1)
mimerTrace 1 10 $ sep
[ "Refining goal"
, nest 2 $ prettyTCM (goalMeta goal1) <+> ":" <+> prettyTCM goalType1
, nest 2 $ "in context" <+> (inTopContext . prettyTCM =<< getContextTelescope)
]
reportSDoc "mimer.refine" 30 $ "Goal type:" <+> pretty goalType1
reportSDoc "mimer.refine" 30 $ "Goal context:" <+> (pretty =<< getContextTelescope)
tryLamAbs goal1 goalType1 branch1 >>= \case
Left Expr
expr -> do
ArgName
-> VerboseLevel
-> TCMT IO Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"mimer.refine" VerboseLevel
30 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
-> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Abstracted with absurd lambda. Result:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
expr
[SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Expr -> SearchStepResult
ResultExpr Expr
expr]
Right (Goal
goal2, Type
goalType2, SearchBranch
branch2) -> SearchBranch
-> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch2 Goal
goal2 (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
(branch3, components) <- Goal
-> SearchBranch -> SM (SearchBranch, [(Component, [Component])])
prepareComponents Goal
goal2 SearchBranch
branch2
withBranchAndGoal branch3 goal2 $ do
when (goalMeta goal2 /= goalMeta goal1) $ do
mimerTrace 1 10 $ sep
[ "Lambda refinement", nest 2 $ prettyGoalInst goal1 ]
mimerTrace 1 10 $ sep
[ "Refining goal"
, nest 2 $ prettyTCM (goalMeta goal2) <+> ":" <+> prettyTCM goalType2
, nest 2 $ "in context" <+> (inTopContext . prettyTCM =<< getContextTelescope)
]
mimerTrace 2 40 $ vcat
[ "Components:"
, nest 2 $ vcat $ map prettyTCM $ concatMap snd components
]
results1 <- tryComponents goal2 goalType2 branch3 components
results2 <- tryDataRecord goal2 goalType2 branch3
return $ results1 ++ results2
tryFns :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryFns :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryFns Goal
goal Type
goalType SearchBranch
branch = SearchBranch
-> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
ArgName
-> VerboseLevel
-> TCMT IO Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"mimer.refine.fn" VerboseLevel
50 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
-> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Trying functions"
fns <- (SearchOptions -> [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (BaseComponents -> [Component]
hintFns (BaseComponents -> [Component])
-> (SearchOptions -> BaseComponents)
-> SearchOptions
-> [Component]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> BaseComponents
searchBaseComponents)
newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) fns
mapM checkSolved newBranches
tryProjs :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryProjs :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryProjs Goal
goal Type
goalType SearchBranch
branch = SearchBranch
-> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
projs <- (SearchOptions -> [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (BaseComponents -> [Component]
hintProjections (BaseComponents -> [Component])
-> (SearchOptions -> BaseComponents)
-> SearchOptions
-> [Component]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> BaseComponents
searchBaseComponents)
newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) projs
mapM checkSolved newBranches
tryAxioms :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryAxioms :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryAxioms Goal
goal Type
goalType SearchBranch
branch = SearchBranch
-> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
axioms <- (SearchOptions -> [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (BaseComponents -> [Component]
hintAxioms (BaseComponents -> [Component])
-> (SearchOptions -> BaseComponents)
-> SearchOptions
-> [Component]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> BaseComponents
searchBaseComponents)
newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) axioms
mapM checkSolved newBranches
tryLet :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryLet :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryLet Goal
goal Type
goalType SearchBranch
branch = SearchBranch
-> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
letVars <- (SearchOptions -> [Open Component])
-> ReaderT SearchOptions (TCMT IO) [Open Component]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (BaseComponents -> [Open Component]
hintLetVars (BaseComponents -> [Open Component])
-> (SearchOptions -> BaseComponents)
-> SearchOptions
-> [Open Component]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> BaseComponents
searchBaseComponents) ReaderT SearchOptions (TCMT IO) [Open Component]
-> ([Open Component]
-> ReaderT SearchOptions (TCMT IO) [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Open Component -> ReaderT SearchOptions (TCMT IO) Component)
-> [Open Component] -> ReaderT SearchOptions (TCMT IO) [Component]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Open Component -> ReaderT SearchOptions (TCMT IO) Component
forall (tcm :: * -> *).
MonadTCM tcm =>
Open Component -> tcm Component
getOpenComponent
newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) letVars
mapM checkSolved newBranches
tryLamAbs :: Goal -> Type -> SearchBranch -> SM (Either Expr (Goal, Type, SearchBranch))
tryLamAbs :: Goal
-> Type
-> SearchBranch
-> SM (Either Expr (Goal, Type, SearchBranch))
tryLamAbs Goal
goal Type
goalType SearchBranch
branch =
case Type -> Term
forall t a. Type'' t a -> a
unEl Type
goalType of
Pi Dom Type
dom Abs Type
abs -> do
e <- Type -> SM Bool
isEmptyType (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom)
isEmptyType (unDom dom) >>= \case
Bool
True -> do
let argInf :: ArgInfo
argInf = ArgInfo
defaultArgInfo{argInfoOrigin = Inserted}
term :: Term
term = ArgInfo -> Abs Term -> Term
Lam ArgInfo
argInf Abs Term
absurdBody
newMetaIds <- MetaId -> Term -> Type -> SM [MetaId]
assignMeta (Goal -> MetaId
goalMeta Goal
goal) Term
term Type
goalType
unless (null newMetaIds) (__IMPOSSIBLE__)
return $ Left $ AbsurdLam exprNoRange NotHidden
Bool
False -> do
let bindName :: ArgName
bindName | ArgName -> Bool
forall a. IsNoName a => a -> Bool
isNoName (Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
abs) = ArgName
"z"
| Bool
otherwise = Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
abs
newName <- ArgName -> ReaderT SearchOptions (TCMT IO) Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *). MonadFresh NameId m => ArgName -> m Name
freshName_ ArgName
bindName
(metaId', bodyType, metaTerm, env) <- lambdaAddContext newName bindName dom $ do
goalType' <- getMetaTypeInContext (goalMeta goal)
bodyType <- bench [Bench.Reduce] $ reduce =<< piApplyM goalType' (Var 0 [])
(metaId', metaTerm) <- bench [Bench.Free] $ newValueMeta DontRunMetaOccursCheck CmpLeq bodyType
env <- askTC
return (metaId', bodyType, metaTerm, env)
let argInf = Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
dom
newAbs = Abs{absName :: ArgName
absName = ArgName
bindName, unAbs :: Term
unAbs = Term
metaTerm }
term = ArgInfo -> Abs Term -> Term
Lam ArgInfo
argInf Abs Term
newAbs
newMetaIds <- assignMeta (goalMeta goal) term goalType
withEnv env $ do
branch' <- updateBranch newMetaIds branch
tryLamAbs (Goal metaId') bodyType branch'
Term
_ -> do
branch' <- [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch [] SearchBranch
branch
return $ Right (goal, goalType, branch')
genRecCalls :: Component -> SM [Component]
genRecCalls :: Component -> ReaderT SearchOptions (TCMT IO) [Component]
genRecCalls Component
thisFn = do
(SearchOptions -> Open [(Term, NoSubst Term VerboseLevel)])
-> ReaderT
SearchOptions (TCMT IO) (Open [(Term, NoSubst Term VerboseLevel)])
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (BaseComponents -> Open [(Term, NoSubst Term VerboseLevel)]
hintRecVars (BaseComponents -> Open [(Term, NoSubst Term VerboseLevel)])
-> (SearchOptions -> BaseComponents)
-> SearchOptions
-> Open [(Term, NoSubst Term VerboseLevel)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> BaseComponents
searchBaseComponents) ReaderT
SearchOptions (TCMT IO) (Open [(Term, NoSubst Term VerboseLevel)])
-> (Open [(Term, NoSubst Term VerboseLevel)]
-> ReaderT
SearchOptions (TCMT IO) [(Term, NoSubst Term VerboseLevel)])
-> ReaderT
SearchOptions (TCMT IO) [(Term, NoSubst Term VerboseLevel)]
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Open [(Term, NoSubst Term VerboseLevel)]
-> ReaderT
SearchOptions (TCMT IO) [(Term, NoSubst Term VerboseLevel)]
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen ReaderT SearchOptions (TCMT IO) [(Term, NoSubst Term VerboseLevel)]
-> ([(Term, NoSubst Term VerboseLevel)]
-> ReaderT SearchOptions (TCMT IO) [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
[] -> [Component] -> ReaderT SearchOptions (TCMT IO) [Component]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
[(Term, NoSubst Term VerboseLevel)]
recCandTerms -> do
Costs{..} <- (SearchOptions -> Costs) -> ReaderT SearchOptions (TCMT IO) Costs
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> Costs
searchCosts
n <- localVarCount
localVars <- lift $ getLocalVars n costLocal
let recCands = [ (Component
t, VerboseLevel
i) | t :: Component
t@(Component -> Term
compTerm -> v :: Term
v@Var{}) <- [Component]
localVars, NoSubst VerboseLevel
i <- Maybe (NoSubst Term VerboseLevel) -> [NoSubst Term VerboseLevel]
forall a. Maybe a -> [a]
maybeToList (Maybe (NoSubst Term VerboseLevel) -> [NoSubst Term VerboseLevel])
-> Maybe (NoSubst Term VerboseLevel) -> [NoSubst Term VerboseLevel]
forall a b. (a -> b) -> a -> b
$ Term
-> [(Term, NoSubst Term VerboseLevel)]
-> Maybe (NoSubst Term VerboseLevel)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Term
v [(Term, NoSubst Term VerboseLevel)]
recCandTerms ]
let newRecCall = do
(thisFnTerm, thisFnType, newMetas) <- VerboseLevel -> Term -> Type -> SM (Term, Type, [MetaId])
applyToMetas VerboseLevel
0 (Component -> Term
compTerm Component
thisFn) (Component -> Type
compType Component
thisFn)
let argGoals = (MetaId -> Goal) -> [MetaId] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map MetaId -> Goal
Goal [MetaId]
newMetas
comp <- newComponent newMetas (compCost thisFn) (compName thisFn) 0 thisFnTerm thisFnType
return (comp, zip argGoals [0..])
go Component
_thisFn [] [(Component, VerboseLevel)]
_args = [Component] -> ReaderT SearchOptions (TCMT IO) [Component]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
go Component
thisFn ((Goal, VerboseLevel)
_ : [(Goal, VerboseLevel)]
goals) [] = Component
-> [(Goal, VerboseLevel)]
-> [(Component, VerboseLevel)]
-> ReaderT SearchOptions (TCMT IO) [Component]
go Component
thisFn [(Goal, VerboseLevel)]
goals [(Component, VerboseLevel)]
recCands
go Component
thisFn ((Goal
goal, VerboseLevel
i) : [(Goal, VerboseLevel)]
goals) ((Component
arg, VerboseLevel
j) : [(Component, VerboseLevel)]
args) | VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
j = do
ArgName
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
reportSMDoc ArgName
"mimer.components.rec" VerboseLevel
80 (ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ())
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [ReaderT SearchOptions (TCMT IO) Doc]
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ ReaderT SearchOptions (TCMT IO) Doc
"Trying to generate recursive call"
, Term -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Component -> Term
compTerm Component
thisFn)
, ReaderT SearchOptions (TCMT IO) Doc
"with" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Component -> Term
compTerm Component
arg)
, ReaderT SearchOptions (TCMT IO) Doc
"for" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM (Goal -> MetaId
goalMeta Goal
goal) ]
goalType <- MetaId -> ReaderT SearchOptions (TCMT IO) Type
forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext (Goal -> MetaId
goalMeta Goal
goal)
state <- getTC
tryRefineWith' goal goalType arg >>= \case
Maybe ([MetaId], [MetaId])
Nothing -> do
TCState -> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
state
Component
-> [(Goal, VerboseLevel)]
-> [(Component, VerboseLevel)]
-> ReaderT SearchOptions (TCMT IO) [Component]
go Component
thisFn ((Goal
goal, VerboseLevel
i) (Goal, VerboseLevel)
-> [(Goal, VerboseLevel)] -> [(Goal, VerboseLevel)]
forall a. a -> [a] -> [a]
: [(Goal, VerboseLevel)]
goals) [(Component, VerboseLevel)]
args
Just ([MetaId]
newMetas1, [MetaId]
newMetas2) -> do
let newComp :: Component
newComp = Component
thisFn{compMetas = newMetas1 ++ newMetas2 ++ (compMetas thisFn \\ [goalMeta goal])}
(thisFn', goals') <- ReaderT SearchOptions (TCMT IO) (Component, [(Goal, VerboseLevel)])
newRecCall
(newComp:) <$> go thisFn' (drop (length goals' - length goals - 1) goals') args
go Component
thisFn [(Goal, VerboseLevel)]
goals ((Component, VerboseLevel)
_ : [(Component, VerboseLevel)]
args) = Component
-> [(Goal, VerboseLevel)]
-> [(Component, VerboseLevel)]
-> ReaderT SearchOptions (TCMT IO) [Component]
go Component
thisFn [(Goal, VerboseLevel)]
goals [(Component, VerboseLevel)]
args
(thisFn', argGoals) <- newRecCall
comps <- go thisFn' argGoals recCands
let callCost Component
comp = (VerboseLevel
costLocal VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+) (VerboseLevel -> VerboseLevel)
-> ([VerboseLevel] -> VerboseLevel)
-> [VerboseLevel]
-> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VerboseLevel] -> VerboseLevel
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([VerboseLevel] -> VerboseLevel)
-> ReaderT SearchOptions (TCMT IO) [VerboseLevel]
-> SM VerboseLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReaderT SearchOptions (TCMT IO) [VerboseLevel]
argCosts (Component -> Term
compTerm Component
comp)
argCosts (Def QName
_ Elims
elims) = (Elim' Term -> SM VerboseLevel)
-> Elims -> ReaderT SearchOptions (TCMT IO) [VerboseLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim' Term -> SM VerboseLevel
argCost Elims
elims
argCosts Term
_ = ReaderT SearchOptions (TCMT IO) [VerboseLevel]
forall a. HasCallStack => a
__IMPOSSIBLE__
argCost (Apply Arg Term
arg) = Arg Term -> ReaderT SearchOptions (TCMT IO) (Arg Term)
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Arg Term
arg ReaderT SearchOptions (TCMT IO) (Arg Term)
-> (Arg Term -> VerboseLevel) -> SM VerboseLevel
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ case
Arg ArgInfo
h MetaV{} | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
h -> VerboseLevel
costNewMeta
| Bool
otherwise -> VerboseLevel
costNewHiddenMeta
Arg Term
_ -> VerboseLevel
0
argCost Proj{} = VerboseLevel -> SM VerboseLevel
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VerboseLevel
0
argCost IApply{} = VerboseLevel -> SM VerboseLevel
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VerboseLevel
0
mapM (\ Component
c -> (VerboseLevel -> Component -> Component
`addCost` Component
c) (VerboseLevel -> Component)
-> SM VerboseLevel -> ReaderT SearchOptions (TCMT IO) Component
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Component -> SM VerboseLevel
callCost Component
c) comps
tryDataRecord :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryDataRecord :: Goal -> Type -> SearchBranch -> SM [SearchStepResult]
tryDataRecord Goal
goal Type
goalType SearchBranch
branch = SearchBranch
-> Goal -> SM [SearchStepResult] -> SM [SearchStepResult]
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (SM [SearchStepResult] -> SM [SearchStepResult])
-> SM [SearchStepResult] -> SM [SearchStepResult]
forall a b. (a -> b) -> a -> b
$ do
case Type -> Term
forall t a. Type'' t a -> a
unEl Type
goalType of
Def QName
qname Elims
elims -> Definition -> Defn
theDef (Definition -> Defn)
-> ReaderT SearchOptions (TCMT IO) Definition
-> ReaderT SearchOptions (TCMT IO) Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ReaderT SearchOptions (TCMT IO) Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qname ReaderT SearchOptions (TCMT IO) Defn
-> (Defn -> SM [SearchStepResult]) -> SM [SearchStepResult]
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
recordDefn :: Defn
recordDefn@Record{} -> do
Defn -> SM [SearchStepResult]
tryRecord Defn
recordDefn
dataDefn :: Defn
dataDefn@Datatype{} -> do
Defn -> SM [SearchStepResult]
tryData Defn
dataDefn
primitive :: Defn
primitive@Primitive{} -> do
[SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
d :: Defn
d@Axiom{}
| QName -> ArgName
forall a. Pretty a => a -> ArgName
P.prettyShow QName
qname ArgName -> ArgName -> Bool
forall a. Eq a => a -> a -> Bool
== ArgName
"Agda.Primitive.Level" -> do
tryLevel
| Bool
otherwise -> do
[SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
d :: Defn
d@DataOrRecSig{} -> do
[SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
d :: Defn
d@Defn
GeneralizableVar -> do
[SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
d :: Defn
d@AbstractDefn{} -> do
[SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
d :: Defn
d@Function{} -> do
[SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
d :: Defn
d@Constructor{} -> do
[SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
d :: Defn
d@PrimitiveSort{} -> do
[SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
sort :: Term
sort@(Sort (Type Level
level)) -> do
Level -> SM [SearchStepResult]
trySet Level
level
Sort Sort' Term
sort -> do
[SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
Term
_ -> [SearchStepResult] -> SM [SearchStepResult]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
where
tryRecord :: Defn -> SM [SearchStepResult]
tryRecord :: Defn -> SM [SearchStepResult]
tryRecord Defn
recordDefn = do
cost <- (SearchOptions -> VerboseLevel) -> SM VerboseLevel
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Costs -> VerboseLevel
costRecordCon (Costs -> VerboseLevel)
-> (SearchOptions -> Costs) -> SearchOptions -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> Costs
searchCosts)
comp <- qnameToComponent cost $ conName $ recConHead recordDefn
newBranches <- maybeToList <$> tryRefineAddMetas goal goalType branch comp
mapM checkSolved newBranches
tryData :: Defn -> SM [SearchStepResult]
tryData :: Defn -> SM [SearchStepResult]
tryData Defn
dataDefn = do
cost <- (SearchOptions -> VerboseLevel) -> SM VerboseLevel
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Costs -> VerboseLevel
costDataCon (Costs -> VerboseLevel)
-> (SearchOptions -> Costs) -> SearchOptions -> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> Costs
searchCosts)
comps <- mapM (qnameToComponent cost) $ dataCons dataDefn
newBranches <- mapM (tryRefineAddMetas goal goalType branch) comps
mapM checkSolved (catMaybes newBranches)
tryLevel :: SM [SearchStepResult]
tryLevel :: SM [SearchStepResult]
tryLevel = do
levelHints <- (SearchOptions -> [Component])
-> ReaderT SearchOptions (TCMT IO) [Component]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (BaseComponents -> [Component]
hintLevel (BaseComponents -> [Component])
-> (SearchOptions -> BaseComponents)
-> SearchOptions
-> [Component]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> BaseComponents
searchBaseComponents)
newBranches <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch) levelHints
mapM checkSolved newBranches
trySet :: Level -> SM [SearchStepResult]
trySet :: Level -> SM [SearchStepResult]
trySet Level
level = do
reducedLevel <- Level -> ReaderT SearchOptions (TCMT IO) Level
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Level
level
cost <- asks (costSet . searchCosts)
setCandidates <- case reducedLevel of
(Max Integer
i [])
| Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 -> do
comp <- [MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> ReaderT SearchOptions (TCMT IO) Component
forall (m :: * -> *).
MonadFresh VerboseLevel m =>
[MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> m Component
newComponent [] VerboseLevel
cost Maybe Name
forall a. Maybe a
Nothing VerboseLevel
0 (Sort' Term -> Term
Sort (Sort' Term -> Term) -> Sort' Term -> Term
forall a b. (a -> b) -> a -> b
$ Level -> Sort' Term
forall t. Level' t -> Sort' t
Type (Level -> Sort' Term) -> Level -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) []) Type
goalType
return [(branch, comp)]
| Bool
otherwise -> [(SearchBranch, Component)]
-> ReaderT SearchOptions (TCMT IO) [(SearchBranch, Component)]
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
(Max Integer
i [PlusLevel' Term]
ps) -> do
(metaId, metaTerm) <- Type -> SM (MetaId, Term)
createMeta (Type -> SM (MetaId, Term))
-> ReaderT SearchOptions (TCMT IO) Type -> SM (MetaId, Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ReaderT SearchOptions (TCMT IO) Type
forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
levelType
comp <- newComponent [metaId] cost Nothing 0 (Sort $ Type $ Max (max 0 (i - 1)) [Plus 0 metaTerm]) goalType
branch' <- updateBranch [metaId] branch
return [(branch', comp)]
reportSDoc "mimer.refine.set" 40 $
"Trying" <+> prettyTCM (map snd setCandidates) <+> "for" <+> prettyTCM goalType
newBranches <- catMaybes <$> mapM (\(SearchBranch
br,Component
c) -> Goal
-> Type
-> SearchBranch
-> Component
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
tryRefineWith Goal
goal Type
goalType SearchBranch
br Component
c) setCandidates
components <- asks searchBaseComponents
newBranches' <- catMaybes <$> mapM (tryRefineAddMetas goal goalType branch)
(concatMap ($ components)
[ hintDataTypes
, hintRecordTypes
, hintAxioms])
mapM checkSolved (newBranches ++ newBranches')
tryRefineWith :: Goal -> Type -> SearchBranch -> Component -> SM (Maybe SearchBranch)
tryRefineWith :: Goal
-> Type
-> SearchBranch
-> Component
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
tryRefineWith Goal
goal Type
goalType SearchBranch
branch Component
comp = SearchBranch
-> Goal
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch))
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
forall a b. (a -> b) -> a -> b
$ do
ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr, LocalMetaStores)
forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy (Type -> Type -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
dumbUnifierErr (Component -> Type
compType Component
comp) Type
goalType) ReaderT SearchOptions (TCMT IO) (Maybe TCErr, LocalMetaStores)
-> ((Maybe TCErr, LocalMetaStores)
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch))
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
(Maybe TCErr
Nothing, LocalMetaStores
newMetaStore) -> do
(MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
updateStat MimerStats -> MimerStats
incRefineSuccess
newMetaIds <- MetaId -> Term -> Type -> SM [MetaId]
assignMeta (Goal -> MetaId
goalMeta Goal
goal) (Component -> Term
compTerm Component
comp) Type
goalType
let newMetaIds' = Map MetaId MetaVariable -> [MetaId]
forall k a. Map k a -> [k]
Map.keys (LocalMetaStores -> Map MetaId MetaVariable
openMetas LocalMetaStores
newMetaStore)
reportSDoc "mimer.refine" 60 $
"Refine: assignMeta created new metas:" <+> prettyTCM newMetaIds
reportSMDoc "mimer.refine" 50 $ "Refinement succeeded"
mimerTrace 2 10 $ sep
[ "Found refinement"
, nest 2 $ sep [ prettyTCM (compTerm comp)
, ":" <+> prettyTCM (compType comp) ] ]
Just <$> updateBranchCost comp (newMetaIds' ++ compMetas comp) branch
(Just TCErr
err, LocalMetaStores
_) -> do
(MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
updateStat MimerStats -> MimerStats
incRefineFail
ArgName
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
reportSMDoc ArgName
"mimer.refine" VerboseLevel
50 (ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ())
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ ReaderT SearchOptions (TCMT IO) Doc
"Refinement failed"
VerboseLevel
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
mimerTrace VerboseLevel
2 VerboseLevel
60 (ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ())
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [ReaderT SearchOptions (TCMT IO) Doc]
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ ReaderT SearchOptions (TCMT IO) Doc
"Failed refinement"
, VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc)
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$ [ReaderT SearchOptions (TCMT IO) Doc]
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Component -> Term
compTerm Component
comp)
, ReaderT SearchOptions (TCMT IO) Doc
":" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Component -> Type
compType Component
comp) ]
, VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc)
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$ TCErr -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err ]
Maybe SearchBranch
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SearchBranch
forall a. Maybe a
Nothing
tryRefineWith' :: Goal -> Type -> Component -> SM (Maybe ([MetaId], [MetaId]))
tryRefineWith' :: Goal -> Type -> Component -> SM (Maybe ([MetaId], [MetaId]))
tryRefineWith' Goal
goal Type
goalType Component
comp = do
SM Bool -> ReaderT SearchOptions (TCMT IO) (Bool, LocalMetaStores)
forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy (Type -> Type -> SM Bool
dumbUnifier (Component -> Type
compType Component
comp) Type
goalType) ReaderT SearchOptions (TCMT IO) (Bool, LocalMetaStores)
-> ((Bool, LocalMetaStores) -> SM (Maybe ([MetaId], [MetaId])))
-> SM (Maybe ([MetaId], [MetaId]))
forall a b.
ReaderT SearchOptions (TCMT IO) a
-> (a -> ReaderT SearchOptions (TCMT IO) b)
-> ReaderT SearchOptions (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
(Bool
True, LocalMetaStores
newMetaStore) -> do
newMetaIds <- MetaId -> Term -> Type -> SM [MetaId]
assignMeta (Goal -> MetaId
goalMeta Goal
goal) (Component -> Term
compTerm Component
comp) Type
goalType
let newMetaIds' = Map MetaId MetaVariable -> [MetaId]
forall k a. Map k a -> [k]
Map.keys (LocalMetaStores -> Map MetaId MetaVariable
openMetas LocalMetaStores
newMetaStore)
return $ Just (newMetaIds, newMetaIds')
(Bool
False, LocalMetaStores
_) -> Maybe ([MetaId], [MetaId]) -> SM (Maybe ([MetaId], [MetaId]))
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([MetaId], [MetaId])
forall a. Maybe a
Nothing
tryRefineAddMetas :: Goal -> Type -> SearchBranch -> Component -> SM (Maybe SearchBranch)
tryRefineAddMetas :: Goal
-> Type
-> SearchBranch
-> Component
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
tryRefineAddMetas Goal
goal Type
goalType SearchBranch
branch Component
comp = SearchBranch
-> Goal
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
forall a. SearchBranch -> Goal -> SM a -> SM a
withBranchAndGoal SearchBranch
branch Goal
goal (ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch))
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
-> ReaderT SearchOptions (TCMT IO) (Maybe SearchBranch)
forall a b. (a -> b) -> a -> b
$ do
comp' <- Maybe VerboseLevel
-> Component -> ReaderT SearchOptions (TCMT IO) Component
applyToMetasG Maybe VerboseLevel
forall a. Maybe a
Nothing Component
comp
branch' <- updateBranch [] branch
tryRefineWith goal goalType branch' comp'
applyToMetas :: Nat -> Term -> Type -> SM (Term, Type, [MetaId])
applyToMetas :: VerboseLevel -> Term -> Type -> SM (Term, Type, [MetaId])
applyToMetas VerboseLevel
skip Term
term Type
typ = do
ctx <- ReaderT SearchOptions (TCMT IO) Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
case unEl typ of
Pi Dom Type
dom Abs Type
abs -> do
let domainType :: Type
domainType = Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom
(metaId', metaTerm) <- [Phase] -> SM (MetaId, Term) -> SM (MetaId, Term)
forall a. NFData a => [Phase] -> SM a -> SM a
bench [Phase
Bench.Free] (SM (MetaId, Term) -> SM (MetaId, Term))
-> SM (MetaId, Term) -> SM (MetaId, Term)
forall a b. (a -> b) -> a -> b
$ RunMetaOccursCheck -> Comparison -> Type -> SM (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck Comparison
CmpLeq Type
domainType
let arg = Origin -> Arg Term -> Arg Term
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term
metaTerm Term -> Arg Type -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
dom
newType <- bench [Bench.Reduce] $ reduce =<< piApplyM typ metaTerm
let newTerm = if VerboseLevel
skip VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0 then Term
term else Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
term [Arg Term
arg]
(term', typ', metas) <- applyToMetas (predNat skip) newTerm newType
return (term', typ', metaId' : metas)
Term
_ -> (Term, Type, [MetaId]) -> SM (Term, Type, [MetaId])
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
term, Type
typ, [])
normaliseSolution :: Term -> SM Term
normaliseSolution :: Term -> ReaderT SearchOptions (TCMT IO) Term
normaliseSolution Term
t = do
norm <- (SearchOptions -> Rewrite)
-> ReaderT SearchOptions (TCMT IO) Rewrite
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> Rewrite
searchRewrite
lift . normalForm norm =<< instantiateFull t
checkSolved :: SearchBranch -> SM SearchStepResult
checkSolved :: SearchBranch -> ReaderT SearchOptions (TCMT IO) SearchStepResult
checkSolved SearchBranch
branch = do
topMetaId <- (SearchOptions -> MetaId) -> ReaderT SearchOptions (TCMT IO) MetaId
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> MetaId
searchTopMeta
topMeta <- lookupLocalMeta topMetaId
ii <- asks searchInteractionId
withInteractionId ii $ withBranchState branch $ do
metaArgs <- getMetaContextArgs topMeta
inst <- normaliseSolution $ apply (MetaV topMetaId []) metaArgs
case allMetas (:[]) inst of
[] -> Expr -> SearchStepResult
ResultExpr (Expr -> SearchStepResult)
-> ReaderT SearchOptions (TCMT IO) Expr
-> ReaderT SearchOptions (TCMT IO) SearchStepResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ReaderT SearchOptions (TCMT IO) (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
inst
[MetaId]
metaIds -> do
SearchStepResult
-> ReaderT SearchOptions (TCMT IO) SearchStepResult
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SearchStepResult
-> ReaderT SearchOptions (TCMT IO) SearchStepResult)
-> SearchStepResult
-> ReaderT SearchOptions (TCMT IO) SearchStepResult
forall a b. (a -> b) -> a -> b
$ SearchBranch -> SearchStepResult
OpenBranch (SearchBranch -> SearchStepResult)
-> SearchBranch -> SearchStepResult
forall a b. (a -> b) -> a -> b
$ SearchBranch
branch{sbGoals = map Goal $ reverse metaIds}
setAt :: Int -> a -> [a] -> [a]
setAt :: forall a. VerboseLevel -> a -> [a] -> [a]
setAt VerboseLevel
i a
x [a]
xs = case VerboseLevel -> [a] -> ([a], [a])
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt VerboseLevel
i [a]
xs of
([a]
ls, a
_r:[a]
rs) -> [a]
ls [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
rs)
([a], [a])
_ -> ArgName -> [a]
forall a. HasCallStack => ArgName -> a
error ArgName
"setAt: index out of bounds"
updateBranch' :: Maybe Component -> [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch' :: Maybe Component -> [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch' Maybe Component
mComp [MetaId]
newMetaIds SearchBranch
branch = do
state <- ReaderT SearchOptions (TCMT IO) TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
let compsUsed = SearchBranch -> Map Name VerboseLevel
sbComponentsUsed SearchBranch
branch
(deltaCost, compsUsed') <- case mComp of
Maybe Component
Nothing -> (VerboseLevel, Map Name VerboseLevel)
-> ReaderT
SearchOptions (TCMT IO) (VerboseLevel, Map Name VerboseLevel)
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseLevel
0, Map Name VerboseLevel
compsUsed)
Just Component
comp -> do
case Component -> Maybe Name
compName Component
comp of
Maybe Name
Nothing -> (VerboseLevel, Map Name VerboseLevel)
-> ReaderT
SearchOptions (TCMT IO) (VerboseLevel, Map Name VerboseLevel)
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Component -> VerboseLevel
compCost Component
comp, Map Name VerboseLevel
compsUsed)
Just Name
name -> case Map Name VerboseLevel
compsUsed Map Name VerboseLevel -> Name -> Maybe VerboseLevel
forall k a. Ord k => Map k a -> k -> Maybe a
Map.!? Name
name of
Maybe VerboseLevel
Nothing -> (VerboseLevel, Map Name VerboseLevel)
-> ReaderT
SearchOptions (TCMT IO) (VerboseLevel, Map Name VerboseLevel)
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Component -> VerboseLevel
compCost Component
comp, Name
-> VerboseLevel -> Map Name VerboseLevel -> Map Name VerboseLevel
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
name VerboseLevel
1 Map Name VerboseLevel
compsUsed)
Just VerboseLevel
uses -> do
reuseCost <- (SearchOptions -> VerboseLevel -> VerboseLevel)
-> ReaderT SearchOptions (TCMT IO) (VerboseLevel -> VerboseLevel)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Costs -> VerboseLevel -> VerboseLevel
costCompReuse (Costs -> VerboseLevel -> VerboseLevel)
-> (SearchOptions -> Costs)
-> SearchOptions
-> VerboseLevel
-> VerboseLevel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SearchOptions -> Costs
searchCosts)
return (compCost comp + reuseCost uses, Map.adjust succ name compsUsed)
return branch{ sbTCState = state
, sbGoals = map Goal newMetaIds ++ sbGoals branch
, sbCost = sbCost branch + deltaCost
, sbComponentsUsed = compsUsed'
}
updateBranch :: [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch :: [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch = Maybe Component -> [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch' Maybe Component
forall a. Maybe a
Nothing
updateBranchCost :: Component -> [MetaId] -> SearchBranch -> SM SearchBranch
updateBranchCost :: Component -> [MetaId] -> SearchBranch -> SM SearchBranch
updateBranchCost Component
comp = Maybe Component -> [MetaId] -> SearchBranch -> SM SearchBranch
updateBranch' (Component -> Maybe Component
forall a. a -> Maybe a
Just Component
comp)
assignMeta :: MetaId -> Term -> Type -> SM [MetaId]
assignMeta :: MetaId -> Term -> Type -> SM [MetaId]
assignMeta MetaId
metaId Term
term Type
metaType = [Phase] -> SM [MetaId] -> SM [MetaId]
forall a. NFData a => [Phase] -> SM a -> SM a
bench [Phase
Bench.CheckRHS] (SM [MetaId] -> SM [MetaId]) -> SM [MetaId] -> SM [MetaId]
forall a b. (a -> b) -> a -> b
$ do
((), newMetaStore) <- ReaderT SearchOptions (TCMT IO) ()
-> ReaderT SearchOptions (TCMT IO) ((), LocalMetaStores)
forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy (ReaderT SearchOptions (TCMT IO) ()
-> ReaderT SearchOptions (TCMT IO) ((), LocalMetaStores))
-> ReaderT SearchOptions (TCMT IO) ()
-> ReaderT SearchOptions (TCMT IO) ((), LocalMetaStores)
forall a b. (a -> b) -> a -> b
$ do
metaVar <- MetaId -> ReaderT SearchOptions (TCMT IO) MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
metaId
metaArgs <- getMetaContextArgs metaVar
reportSMDoc "mimer.assignMeta" 60 $ vcat
[ "Assigning" <+> pretty term
, nest 2 $ vcat [ "to" <+> pretty metaId <+> ":" <+> pretty metaType
, "in context" <+> (pretty =<< getContextTelescope)
]
]
assignV DirLeq metaId metaArgs term (AsTermsOf metaType) `catchError` \TCErr
err -> do
ArgName
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
reportSMDoc ArgName
"mimer.assignMeta" VerboseLevel
30 (ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ())
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [ReaderT SearchOptions (TCMT IO) Doc]
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ ReaderT SearchOptions (TCMT IO) Doc
"Got error from assignV:" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCErr -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err
, VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc)
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$ [ReaderT SearchOptions (TCMT IO) Doc]
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ ReaderT SearchOptions (TCMT IO) Doc
"when trying to assign" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
term
, ReaderT SearchOptions (TCMT IO) Doc
"to" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
metaId ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ReaderT SearchOptions (TCMT IO) Doc
":" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
metaType
, ReaderT SearchOptions (TCMT IO) Doc
"in context" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc)
-> (Telescope -> ReaderT SearchOptions (TCMT IO) Doc)
-> Telescope
-> ReaderT SearchOptions (TCMT IO) Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> ReaderT SearchOptions (TCMT IO) Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> ReaderT SearchOptions (TCMT IO) Doc)
-> ReaderT SearchOptions (TCMT IO) Telescope
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ReaderT SearchOptions (TCMT IO) Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
]
]
let newMetaIds = Map MetaId MetaVariable -> [MetaId]
forall k a. Map k a -> [k]
Map.keys (LocalMetaStores -> Map MetaId MetaVariable
openMetas LocalMetaStores
newMetaStore)
return newMetaIds
dumbUnifier :: Type -> Type -> SM Bool
dumbUnifier :: Type -> Type -> SM Bool
dumbUnifier Type
t1 Type
t2 = Maybe TCErr -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe TCErr -> Bool)
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr) -> SM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Type -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
dumbUnifierErr Type
t1 Type
t2
dumbUnifierErr :: Type -> Type -> SM (Maybe TCErr)
dumbUnifierErr :: Type -> Type -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
dumbUnifierErr Type
t1 Type
t2 = [Phase]
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
forall a. NFData a => [Phase] -> SM a -> SM a
bench [Phase
Bench.UnifyIndices] (ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr))
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
forall a b. (a -> b) -> a -> b
$ do
(MimerStats -> MimerStats) -> ReaderT SearchOptions (TCMT IO) ()
updateStat MimerStats -> MimerStats
incTypeEqChecks
ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m a -> m a
noConstraints (Maybe TCErr
forall a. Maybe a
Nothing Maybe TCErr
-> ReaderT SearchOptions (TCMT IO) ()
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
forall a b.
a
-> ReaderT SearchOptions (TCMT IO) b
-> ReaderT SearchOptions (TCMT IO) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type -> Type -> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
t2 Type
t1) ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
-> (TCErr -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr))
-> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
forall a.
ReaderT SearchOptions (TCMT IO) a
-> (TCErr -> ReaderT SearchOptions (TCMT IO) a)
-> ReaderT SearchOptions (TCMT IO) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
err -> do
ArgName
-> VerboseLevel
-> TCMT IO Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
"mimer.unify" VerboseLevel
80 (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
-> TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Unification failed with error:", VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCErr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err ]
Maybe TCErr -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
forall a. a -> ReaderT SearchOptions (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TCErr -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr))
-> Maybe TCErr -> ReaderT SearchOptions (TCMT IO) (Maybe TCErr)
forall a b. (a -> b) -> a -> b
$ TCErr -> Maybe TCErr
forall a. a -> Maybe a
Just TCErr
err
showTCM :: (MonadPretty tcm, PrettyTCM a) => a -> tcm String
showTCM :: forall (tcm :: * -> *) a.
(MonadPretty tcm, PrettyTCM a) =>
a -> tcm ArgName
showTCM a
v = Doc -> ArgName
forall a. Doc a -> ArgName
P.render (Doc -> ArgName) -> tcm Doc -> tcm ArgName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> tcm Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
v
bench :: NFData a => [Bench.Phase] -> SM a -> SM a
bench :: forall a. NFData a => [Phase] -> SM a -> SM a
bench [Phase]
k SM a
ma = Account (BenchPhase (ReaderT SearchOptions (TCMT IO)))
-> SM a -> SM a
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
billTo (Phase
mimerAccount Phase -> [Phase] -> [Phase]
forall a. a -> [a] -> [a]
: [Phase]
k) SM a
ma
where
mimerAccount :: Phase
mimerAccount = Phase
Bench.Sort
getLocalVars :: Int -> Cost -> TCM [Component]
getLocalVars :: VerboseLevel -> VerboseLevel -> TCMT IO [Component]
getLocalVars VerboseLevel
localCxt VerboseLevel
cost = do
typedTerms <- VerboseLevel -> TCM [(Term, Dom Type)]
getLocalVarTerms VerboseLevel
localCxt
let varZeroDiscount (Var VerboseLevel
0 []) = a
1
varZeroDiscount Term
_ = a
0
mapM (\(Term
term, Dom Type
domTyp) -> [MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> TCMT IO Component
forall (m :: * -> *).
MonadFresh VerboseLevel m =>
[MetaId]
-> VerboseLevel
-> Maybe Name
-> VerboseLevel
-> Term
-> Type
-> m Component
newComponent [] (VerboseLevel
cost VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- Term -> VerboseLevel
forall {a}. Num a => Term -> a
varZeroDiscount Term
term) Maybe Name
noName VerboseLevel
0 Term
term (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
domTyp)) typedTerms
getLocalVarTerms :: Int -> TCM [(Term, Dom Type)]
getLocalVarTerms :: VerboseLevel -> TCM [(Term, Dom Type)]
getLocalVarTerms VerboseLevel
localCxt = do
contextTerms <- TCMT IO [Term]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Term]
getContextTerms
contextTypes <- flattenTel <$> getContextTelescope
let inScope VerboseLevel
i ContextEntry
_ | VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
< VerboseLevel
localCxt = Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
inScope VerboseLevel
_ Dom{ unDom :: forall t e. Dom' t e -> e
unDom = (Name
name, Type
_) } = do
x <- Name -> TCMT IO (ConOfAbs Name)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ Name
name
pure $ C.isInScope x == C.InScope
scope <- mapM (uncurry inScope) . reverse . zip [0..] =<< getContext
return [ e | (True, e) <- zip scope $ zip contextTerms contextTypes ]
prettyBranch :: SearchBranch -> SM String
prettyBranch :: SearchBranch -> ReaderT SearchOptions (TCMT IO) ArgName
prettyBranch SearchBranch
branch = SearchBranch
-> ReaderT SearchOptions (TCMT IO) ArgName
-> ReaderT SearchOptions (TCMT IO) ArgName
forall a. SearchBranch -> SM a -> SM a
withBranchState SearchBranch
branch (ReaderT SearchOptions (TCMT IO) ArgName
-> ReaderT SearchOptions (TCMT IO) ArgName)
-> ReaderT SearchOptions (TCMT IO) ArgName
-> ReaderT SearchOptions (TCMT IO) ArgName
forall a b. (a -> b) -> a -> b
$ do
metaId <- (SearchOptions -> MetaId) -> ReaderT SearchOptions (TCMT IO) MetaId
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SearchOptions -> MetaId
searchTopMeta
P.render <$> "Branch" <> braces (sep $ punctuate ","
[ "cost:" <+> pretty (sbCost branch)
, "metas:" <+> prettyTCM (map goalMeta (sbGoals branch))
, sep [ "instantiation:"
, nest 2 $ pretty metaId <+> "=" <+> (prettyTCM =<< getMetaInstantiation metaId) ]
, "used components:" <+> pretty (Map.toList $ sbComponentsUsed branch)
])
instance Pretty Goal where
pretty :: Goal -> Doc
pretty Goal
goal = MetaId -> Doc
forall a. Pretty a => a -> Doc
P.pretty (MetaId -> Doc) -> MetaId -> Doc
forall a b. (a -> b) -> a -> b
$ Goal -> MetaId
goalMeta Goal
goal
instance Pretty SearchBranch where
pretty :: SearchBranch -> Doc
pretty SearchBranch
branch = [(Doc, Doc)] -> Doc
keyValueList
[ (Doc
"sbTCState", Doc
"[...]")
, (Doc
"sbGoals", [Goal] -> Doc
forall a. Pretty a => a -> Doc
P.pretty ([Goal] -> Doc) -> [Goal] -> Doc
forall a b. (a -> b) -> a -> b
$ SearchBranch -> [Goal]
sbGoals SearchBranch
branch)
, (Doc
"sbCost", VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ SearchBranch -> VerboseLevel
sbCost SearchBranch
branch)
, (Doc
"sbComponentsUsed", Map Name VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Map Name VerboseLevel -> Doc) -> Map Name VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ SearchBranch -> Map Name VerboseLevel
sbComponentsUsed SearchBranch
branch)
]
instance PrettyTCM BaseComponents where
prettyTCM :: forall (m :: * -> *). MonadPretty m => BaseComponents -> m Doc
prettyTCM BaseComponents
comps = do
let thisFn :: m Doc
thisFn = case BaseComponents -> Maybe Component
hintThisFn BaseComponents
comps of
Maybe Component
Nothing -> m Doc
"(nothing)"
Just Component
comp -> Component -> m Doc
forall {m :: * -> *}.
(Applicative m, IsString (m Doc)) =>
Component -> m Doc
prettyComp Component
comp
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ m Doc
"Base components:"
, VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ m Doc -> [Component] -> m Doc
f m Doc
"hintFns" (BaseComponents -> [Component]
hintFns BaseComponents
comps)
, m Doc -> [Component] -> m Doc
f m Doc
"hintDataTypes" (BaseComponents -> [Component]
hintDataTypes BaseComponents
comps)
, m Doc -> [Component] -> m Doc
f m Doc
"hintRecordTypes" (BaseComponents -> [Component]
hintRecordTypes BaseComponents
comps)
, m Doc -> [Component] -> m Doc
f m Doc
"hintAxioms" (BaseComponents -> [Component]
hintAxioms BaseComponents
comps)
, m Doc -> [Component] -> m Doc
f m Doc
"hintLevel" (BaseComponents -> [Component]
hintLevel BaseComponents
comps)
, m Doc -> [Component] -> m Doc
f m Doc
"hintProjections" (BaseComponents -> [Component]
hintProjections BaseComponents
comps)
, m Doc
"hintThisFn:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
thisFn
, (Open Component -> m Doc) -> m Doc -> [Open Component] -> m Doc
forall {m :: * -> *} {a}.
(Semigroup (m Doc), IsString (m Doc), Applicative m) =>
(a -> m Doc) -> m Doc -> [a] -> m Doc
g Open Component -> m Doc
forall {m :: * -> *}.
(Applicative m, IsString (m Doc)) =>
Open Component -> m Doc
prettyOpenComp m Doc
"hintLetVars" (BaseComponents -> [Open Component]
hintLetVars BaseComponents
comps)
, m Doc
"hintRecVars: Open" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [(Term, VerboseLevel)] -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ((NoSubst Term VerboseLevel -> VerboseLevel)
-> (Term, NoSubst Term VerboseLevel) -> (Term, VerboseLevel)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd NoSubst Term VerboseLevel -> VerboseLevel
forall t a. NoSubst t a -> a
unNoSubst ((Term, NoSubst Term VerboseLevel) -> (Term, VerboseLevel))
-> [(Term, NoSubst Term VerboseLevel)] -> [(Term, VerboseLevel)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Open [(Term, NoSubst Term VerboseLevel)]
-> [(Term, NoSubst Term VerboseLevel)]
forall a. Open a -> a
openThing (BaseComponents -> Open [(Term, NoSubst Term VerboseLevel)]
hintRecVars BaseComponents
comps))
, m Doc
"hintSplitVars: Open" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Open [Term] -> [Term]
forall a. Open a -> a
openThing (Open [Term] -> [Term]) -> Open [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ BaseComponents -> Open [Term]
hintSplitVars BaseComponents
comps)
]
]
where
prettyComp :: Component -> m Doc
prettyComp Component
comp = Term -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Component -> Term
compTerm Component
comp) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Component -> Type
compType Component
comp)
prettyOpenComp :: Open Component -> m Doc
prettyOpenComp Open Component
openComp = m Doc
"Open" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (Component -> m Doc
forall {m :: * -> *}.
(Applicative m, IsString (m Doc)) =>
Component -> m Doc
prettyComp (Component -> m Doc) -> Component -> m Doc
forall a b. (a -> b) -> a -> b
$ Open Component -> Component
forall a. Open a -> a
openThing Open Component
openComp)
prettyTCMComp :: Component -> m Doc
prettyTCMComp Component
comp = Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Component -> Term
compTerm Component
comp) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Component -> Type
compType Component
comp)
f :: m Doc -> [Component] -> m Doc
f = (Component -> m Doc) -> m Doc -> [Component] -> m Doc
forall {m :: * -> *} {a}.
(Semigroup (m Doc), IsString (m Doc), Applicative m) =>
(a -> m Doc) -> m Doc -> [a] -> m Doc
g Component -> m Doc
forall {m :: * -> *}.
(MonadFresh NameId m, MonadInteractionPoints m,
MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
Semigroup (m Doc)) =>
Component -> m Doc
prettyTCMComp
g :: (a -> m Doc) -> m Doc -> [a] -> m Doc
g a -> m Doc
p m Doc
n [] = m Doc
n m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
": []"
g a -> m Doc
p m Doc
n [a]
xs = (m Doc
n m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
":") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$ VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (a -> m Doc) -> [a] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Doc
p [a]
xs)
instance Pretty BaseComponents where
pretty :: BaseComponents -> Doc
pretty BaseComponents
comps = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat
[ Doc -> [Component] -> Doc
forall {a}. Pretty a => Doc -> [a] -> Doc
f Doc
"hintFns" (BaseComponents -> [Component]
hintFns BaseComponents
comps)
, Doc -> [Component] -> Doc
forall {a}. Pretty a => Doc -> [a] -> Doc
f Doc
"hintDataTypes" (BaseComponents -> [Component]
hintDataTypes BaseComponents
comps)
, Doc -> [Component] -> Doc
forall {a}. Pretty a => Doc -> [a] -> Doc
f Doc
"hintRecordTypes" (BaseComponents -> [Component]
hintRecordTypes BaseComponents
comps)
, Doc -> [Component] -> Doc
forall {a}. Pretty a => Doc -> [a] -> Doc
f Doc
"hintAxioms" (BaseComponents -> [Component]
hintAxioms BaseComponents
comps)
, Doc -> [Component] -> Doc
forall {a}. Pretty a => Doc -> [a] -> Doc
f Doc
"hintLevel" (BaseComponents -> [Component]
hintLevel BaseComponents
comps)
, Doc -> [Component] -> Doc
forall {a}. Pretty a => Doc -> [a] -> Doc
f Doc
"hintProjections" (BaseComponents -> [Component]
hintProjections BaseComponents
comps)
]
where
f :: Doc -> [a] -> Doc
f Doc
n [] = Doc
n Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Doc
": []"
f Doc
n [a]
xs = (Doc
n Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Doc
":") Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.$$ VerboseLevel -> Doc -> Doc
forall a. VerboseLevel -> Doc a -> Doc a
P.nest VerboseLevel
2 ([a] -> Doc
forall a. Pretty a => a -> Doc
P.pretty [a]
xs)
instance Pretty SearchOptions where
pretty :: SearchOptions -> Doc
pretty SearchOptions
opts = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat
[ Doc
"searchBaseComponents:"
, VerboseLevel -> Doc -> Doc
forall a. VerboseLevel -> Doc a -> Doc a
P.nest VerboseLevel
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ BaseComponents -> Doc
forall a. Pretty a => a -> Doc
P.pretty (BaseComponents -> Doc) -> BaseComponents -> Doc
forall a b. (a -> b) -> a -> b
$ SearchOptions -> BaseComponents
searchBaseComponents SearchOptions
opts
, [(Doc, Doc)] -> Doc
keyValueList
[ (Doc
"searchHintMode", HintMode -> Doc
forall a. Pretty a => a -> Doc
P.pretty (HintMode -> Doc) -> HintMode -> Doc
forall a b. (a -> b) -> a -> b
$ SearchOptions -> HintMode
searchHintMode SearchOptions
opts)
, (Doc
"searchTimeout", Integer -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Integer -> Doc) -> Integer -> Doc
forall a b. (a -> b) -> a -> b
$ SearchOptions -> Integer
searchTimeout SearchOptions
opts)
, (Doc
"searchTopMeta", MetaId -> Doc
forall a. Pretty a => a -> Doc
P.pretty (MetaId -> Doc) -> MetaId -> Doc
forall a b. (a -> b) -> a -> b
$ SearchOptions -> MetaId
searchTopMeta SearchOptions
opts)
, (Doc
"searchTopEnv", Doc
"[...]")
]
, Doc
"searchCosts:"
, VerboseLevel -> Doc -> Doc
forall a. VerboseLevel -> Doc a -> Doc a
P.nest VerboseLevel
2 (Costs -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Costs -> Doc) -> Costs -> Doc
forall a b. (a -> b) -> a -> b
$ SearchOptions -> Costs
searchCosts SearchOptions
opts)
]
instance PrettyTCM SearchOptions where
prettyTCM :: forall (m :: * -> *). MonadPretty m => SearchOptions -> m Doc
prettyTCM SearchOptions
opts = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ m Doc
"searchBaseComponents:"
, VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ BaseComponents -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => BaseComponents -> m Doc
prettyTCM (BaseComponents -> m Doc) -> BaseComponents -> m Doc
forall a b. (a -> b) -> a -> b
$ SearchOptions -> BaseComponents
searchBaseComponents SearchOptions
opts
, [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ m Doc
"searchHintMode:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> HintMode -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (SearchOptions -> HintMode
searchHintMode SearchOptions
opts)
, m Doc
"searchTimeout:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Integer -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (SearchOptions -> Integer
searchTimeout SearchOptions
opts)
, m Doc
"searchTopMeta:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM (SearchOptions -> MetaId
searchTopMeta SearchOptions
opts)
, m Doc
"searchTopEnv: [...]"
, m Doc
"searchTopCheckpoint:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> CheckpointId -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CheckpointId -> m Doc
prettyTCM (SearchOptions -> CheckpointId
searchTopCheckpoint SearchOptions
opts)
, m Doc
"searchInteractionId:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> InteractionId -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (SearchOptions -> InteractionId
searchInteractionId SearchOptions
opts)
, m Doc
"searchFnName:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Maybe QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (SearchOptions -> Maybe QName
searchFnName SearchOptions
opts)
, m Doc
"searchStats: [...]"
]
, m Doc
"searchCosts:"
, VerboseLevel -> m Doc -> m Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Costs -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Costs -> m Doc) -> Costs -> m Doc
forall a b. (a -> b) -> a -> b
$ SearchOptions -> Costs
searchCosts SearchOptions
opts
]
instance Pretty Component where
pretty :: Component -> Doc
pretty Component
comp = Doc -> [(Doc, Doc)] -> Doc
haskellRecord Doc
"Component"
[ (Doc
"compId", VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Component -> VerboseLevel
compId Component
comp)
, (Doc
"compTerm", Term -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Term -> Doc) -> Term -> Doc
forall a b. (a -> b) -> a -> b
$ Component -> Term
compTerm Component
comp)
, (Doc
"compType", Type -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ Component -> Type
compType Component
comp)
, (Doc
"compMetas", [MetaId] -> Doc
forall a. Pretty a => a -> Doc
P.pretty ([MetaId] -> Doc) -> [MetaId] -> Doc
forall a b. (a -> b) -> a -> b
$ Component -> [MetaId]
compMetas Component
comp)
, (Doc
"compCost", VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Component -> VerboseLevel
compCost Component
comp)
]
instance Pretty Costs where
pretty :: Costs -> Doc
pretty Costs
costs = VerboseLevel -> [(ArgName, Doc)] -> Doc
P.align VerboseLevel
20 [(ArgName, Doc)]
entries
where
entries :: [(ArgName, Doc)]
entries =
[ (ArgName
"costLocal:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costLocal Costs
costs)
, (ArgName
"costFn:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costFn Costs
costs)
, (ArgName
"costDataCon:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costDataCon Costs
costs)
, (ArgName
"costRecordCon:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costRecordCon Costs
costs)
, (ArgName
"costSpeculateProj:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costSpeculateProj Costs
costs)
, (ArgName
"costProj:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costProj Costs
costs)
, (ArgName
"costAxiom:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costAxiom Costs
costs)
, (ArgName
"costLet:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costLet Costs
costs)
, (ArgName
"costLevel:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costLevel Costs
costs)
, (ArgName
"costSet:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costSet Costs
costs)
, (ArgName
"costRecCall:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costRecCall Costs
costs)
, (ArgName
"costNewMeta:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costNewMeta Costs
costs)
, (ArgName
"costNewHiddenMeta:" , VerboseLevel -> Doc
forall a. Pretty a => a -> Doc
P.pretty (VerboseLevel -> Doc) -> VerboseLevel -> Doc
forall a b. (a -> b) -> a -> b
$ Costs -> VerboseLevel
costNewHiddenMeta Costs
costs)
, (ArgName
"costCompReuse:" , Doc
"{function}")
]
instance PrettyTCM Component where
prettyTCM :: forall (m :: * -> *). MonadPretty m => Component -> m Doc
prettyTCM Component{Bool
VerboseLevel
[MetaId]
Maybe Name
Type
Term
compId :: Component -> VerboseLevel
compName :: Component -> Maybe Name
compPars :: Component -> VerboseLevel
compTerm :: Component -> Term
compType :: Component -> Type
compRec :: Component -> Bool
compMetas :: Component -> [MetaId]
compCost :: Component -> VerboseLevel
compId :: VerboseLevel
compName :: Maybe Name
compPars :: VerboseLevel
compTerm :: Term
compType :: Type
compRec :: Bool
compMetas :: [MetaId]
compCost :: VerboseLevel
..} = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (VerboseLevel -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => VerboseLevel -> m Doc
prettyTCM VerboseLevel
compId) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
compTerm
, m Doc
":" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
compType ]
, m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
","
[ m Doc
"cost:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseLevel -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => VerboseLevel -> m Doc
prettyTCM VerboseLevel
compCost
, m Doc
"metas:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [MetaId] -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [MetaId] -> m Doc
prettyTCM [MetaId]
compMetas
]
]
instance PrettyTCM MimerResult where
prettyTCM :: forall (m :: * -> *). MonadPretty m => MimerResult -> m Doc
prettyTCM = \case
MimerExpr ArgName
expr -> ArgName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ArgName
expr
MimerClauses QName
f [Clause]
cl -> m Doc
"MimerClauses" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
f m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"[..]"
MimerResult
MimerNoResult -> m Doc
"MimerNoResult"
MimerList [(VerboseLevel, ArgName)]
sols -> m Doc
"MimerList" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [(VerboseLevel, ArgName)] -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [(VerboseLevel, ArgName)]
sols
concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM :: forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM a -> m [b]
f = ([[b]] -> [b]) -> m [[b]] -> m [b]
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[b]] -> [b]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (m [[b]] -> m [b]) -> ([a] -> m [[b]]) -> [a] -> m [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m [b]) -> [a] -> m [[b]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM a -> m [b]
f
reportSMDoc :: VerboseKey -> VerboseLevel -> SM Doc -> SM ()
reportSMDoc :: ArgName
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
reportSMDoc ArgName
vk VerboseLevel
vl ReaderT SearchOptions (TCMT IO) Doc
md = ArgName
-> VerboseLevel
-> TCMT IO Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc ArgName
vk VerboseLevel
vl (TCMT IO Doc -> ReaderT SearchOptions (TCMT IO) ())
-> (SearchOptions -> TCMT IO Doc)
-> SearchOptions
-> ReaderT SearchOptions (TCMT IO) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReaderT SearchOptions (TCMT IO) Doc -> SearchOptions -> TCMT IO Doc
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT SearchOptions (TCMT IO) Doc
md (SearchOptions -> ReaderT SearchOptions (TCMT IO) ())
-> ReaderT SearchOptions (TCMT IO) SearchOptions
-> ReaderT SearchOptions (TCMT IO) ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ReaderT SearchOptions (TCMT IO) SearchOptions
forall r (m :: * -> *). MonadReader r m => m r
ask
mimerTrace :: Int -> VerboseLevel -> SM Doc -> SM ()
mimerTrace :: VerboseLevel
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
mimerTrace VerboseLevel
ilvl VerboseLevel
vlvl ReaderT SearchOptions (TCMT IO) Doc
doc = ArgName
-> VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
reportSMDoc ArgName
"mimer.trace" VerboseLevel
vlvl (ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ())
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ VerboseLevel
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest (VerboseLevel
2 VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
* VerboseLevel
ilvl) (ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc)
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$ ReaderT SearchOptions (TCMT IO) Doc
"-" ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
-> ReaderT SearchOptions (TCMT IO) Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ReaderT SearchOptions (TCMT IO) Doc
doc
haskellRecord :: Doc -> [(Doc, Doc)] -> Doc
haskellRecord :: Doc -> [(Doc, Doc)] -> Doc
haskellRecord Doc
name [(Doc, Doc)]
fields = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.sep [ Doc
name, VerboseLevel -> Doc -> Doc
forall a. VerboseLevel -> Doc a -> Doc a
P.nest VerboseLevel
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
P.braces ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
P.punctuate Doc
"," [ Doc -> VerboseLevel -> Doc -> Doc
forall a. Doc a -> VerboseLevel -> Doc a -> Doc a
P.hang (Doc
k Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> Doc
"=") VerboseLevel
2 Doc
v | (Doc
k, Doc
v) <- [(Doc, Doc)]
fields ]) ]
keyValueList :: [(Doc, Doc)] -> Doc
keyValueList :: [(Doc, Doc)] -> Doc
keyValueList [(Doc, Doc)]
kvs = Doc -> Doc
P.braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
P.punctuate Doc
"," [ Doc -> VerboseLevel -> Doc -> Doc
forall a. Doc a -> VerboseLevel -> Doc a -> Doc a
P.hang (Doc
k Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Doc
":") VerboseLevel
2 Doc
v | (Doc
k, Doc
v) <- [(Doc, Doc)]
kvs ]
writeTime :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCM m, MonadDebug m) => InteractionId -> Maybe CPUTime -> m ()
writeTime :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCM m,
MonadDebug m) =>
InteractionId -> Maybe CPUTime -> m ()
writeTime InteractionId
ii Maybe CPUTime
mTime = do
let time :: ArgName
time = case Maybe CPUTime
mTime of
Maybe CPUTime
Nothing -> ArgName
"n/a"
Just (CPUTime Integer
t) -> Integer -> ArgName
forall a. Show a => a -> ArgName
show Integer
t
file <- Range -> SrcFile
rangeFile (Range -> SrcFile)
-> (InteractionPoint -> Range) -> InteractionPoint -> SrcFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoint -> Range
ipRange (InteractionPoint -> SrcFile) -> m InteractionPoint -> m SrcFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionId -> m InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
case file of
SrcFile
SMaybe.Nothing ->
ArgName -> VerboseLevel -> ArgName -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> ArgName -> m ()
reportSLn ArgName
"mimer.stats" VerboseLevel
2 ArgName
"No file found for interaction id"
SMaybe.Just RangeFile
file -> do
let path :: ArgName
path = AbsolutePath -> ArgName
filePath (RangeFile -> AbsolutePath
rangeFilePath RangeFile
file) ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
".stats"
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ ArgName -> ArgName -> IO ()
appendFile ArgName
path (VerboseLevel -> ArgName
forall a. Show a => a -> ArgName
show (InteractionId -> VerboseLevel
interactionId InteractionId
ii) ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
time ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
"\n")
customCosts :: TCM Costs
customCosts :: TCMT IO Costs
customCosts = do
costLocal <- ArgName -> TCM VerboseLevel
forall {m :: * -> *}. MonadDebug m => ArgName -> m VerboseLevel
cost ArgName
"local"
costFn <- cost "fn"
costDataCon <- cost "dataCon"
costRecordCon <- cost "recordCon"
costSpeculateProj <- cost "speculateProj"
costProj <- cost "proj"
costAxiom <- cost "axiom"
costLet <- cost "let"
costLevel <- cost "level"
costSet <- cost "set"
costRecCall <- cost "recCall"
costNewMeta <- cost "newMeta"
costNewHiddenMeta <- cost "newHiddenMeta"
compReuse <- cost "compReuse"
let costCompReuse VerboseLevel
uses = VerboseLevel
compReuse VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
* VerboseLevel
uses VerboseLevel -> Integer -> VerboseLevel
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
2
pure Costs{..}
where
cost :: ArgName -> m VerboseLevel
cost ArgName
key = ArgName -> m VerboseLevel
forall {m :: * -> *}. MonadDebug m => ArgName -> m VerboseLevel
getVerbosityLevel (ArgName
"mimer-cost." ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
key)
getVerbosityLevel :: MonadDebug m => VerboseKey -> m VerboseLevel
getVerbosityLevel :: forall {m :: * -> *}. MonadDebug m => ArgName -> m VerboseLevel
getVerbosityLevel ArgName
k = do
t <- m Verbosity
forall (m :: * -> *). MonadDebug m => m Verbosity
getVerbosity
return $ case t of
Verbosity
Strict.Nothing -> VerboseLevel
1
Strict.Just Trie VerboseKeyItem VerboseLevel
t
| Trie VerboseKeyItem VerboseLevel
t Trie VerboseKeyItem VerboseLevel
-> Trie VerboseKeyItem VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== [VerboseKeyItem]
-> VerboseLevel -> Trie VerboseKeyItem VerboseLevel
forall k v. [k] -> v -> Trie k v
Trie.singleton [] VerboseLevel
0 -> VerboseLevel
0
| Bool
otherwise -> VerboseLevel -> [VerboseLevel] -> VerboseLevel
forall a. a -> [a] -> a
lastWithDefault VerboseLevel
0 ([VerboseLevel] -> VerboseLevel) -> [VerboseLevel] -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ [VerboseKeyItem]
-> Trie VerboseKeyItem VerboseLevel -> [VerboseLevel]
forall k v. Ord k => [k] -> Trie k v -> [v]
Trie.lookupPath [VerboseKeyItem]
ks Trie VerboseKeyItem VerboseLevel
t
where ks :: [VerboseKeyItem]
ks = ArgName -> [VerboseKeyItem]
parseVerboseKey ArgName
k