Fields

• sbTCState :: TCState
   
• sbGoals :: [Goal]
   
• sbCost :: Int
   
• sbCache :: Map CheckpointId ComponentCache
   
• sbComponentsUsed :: Map Name Int

  Number of times each component has been used

Fields

• goalMeta :: MetaId
   

Fields

• hintFns :: [Component]
   
• hintDataTypes :: [Component]
   
• hintRecordTypes :: [Component]
   
• hintAxioms :: [Component]

  Excluding those producing Level

• hintLevel :: [Component]

  A definition in a where clause

• hintProjections :: [Component]

  Variables that are candidates for arguments to recursive calls

• hintThisFn :: Maybe Component
   
• hintLetVars :: [Open Component]
   
• hintRecVars :: Open [(Term, NoSubst Term Int)]

  Variable terms and which argument they come from

Fields

• compId :: CompId

  Unique id for the component. Used for the cache.

• compName :: Maybe Name

  Used for keeping track of how many times a component has been used

• compPars :: Nat

  How many arguments should be dropped (e.g. constructor parameters)

• compTerm :: Term
   
• compType :: Type
   
• compRec :: Bool

  Is this a recursive call

• compMetas :: [MetaId]
   
• compCost :: Cost
   

Fields

• searchBaseComponents :: BaseComponents
   
• searchHintMode :: HintMode
   
• searchTimeout :: MilliSeconds
   
• searchGenProjectionsLocal :: Bool
   
• searchGenProjectionsLet :: Bool
   
• searchGenProjectionsExternal :: Bool
   
• searchGenProjectionsRec :: Bool
   
• searchSpeculateProjections :: Bool
   
• searchTopMeta :: MetaId
   
• searchTopEnv :: TCEnv
   
• searchTopCheckpoint :: CheckpointId
   
• searchInteractionId :: InteractionId
   
• searchFnName :: Maybe QName
   
• searchCosts :: Costs
   
• searchStats :: IORef MimerStats
   
• searchRewrite :: Rewrite
   
• searchBuiltinFlat :: Maybe QName
   

Fields

• costLocal :: Cost
   
• costFn :: Cost
   
• costDataCon :: Cost
   
• costRecordCon :: Cost
   
• costSpeculateProj :: Cost
   
• costProj :: Cost
   
• costAxiom :: Cost
   
• costLet :: Cost
   
• costLevel :: Cost
   
• costSet :: Cost
   
• costRecCall :: Cost
   
• costNewMeta :: Cost

  Cost of a new meta-variable appearing in a non-implicit position

• costNewHiddenMeta :: Cost

  Cost of a new meta-variable appearing in an implicit position

• costCompReuse :: Nat -> Cost

  Cost of reusing a component n times. Only counted when n>1.

Fields

• statCompHit :: !Int

  Could make use of an already generated component

• statCompGen :: !Int

  Could use a generator for a component

• statCompRegen :: !Int

  Had to regenerate the cache (new context)

• statCompNoRegen :: !Int

  Did not have to regenerate the cache

• statMetasCreated :: !Int

  Total number of meta-variables created explicitly (not through unification)

• statTypeEqChecks :: !Int

  Number of times type equality is tested (with unification)

• statRefineSuccess :: !Int

  Number of times a refinement has been successful

• statRefineFail :: !Int

  Number of times a refinement has failed