Idris2Doc : Core.UnifyState

Core.UnifyState

(source)
Definitions
data Constraint : Type
  Totality: possibly not terminating due to call to $resolved17706
  Visibility: public export
  Constructors:
  
MkConstraint : FC -> Bool -> Env Term vars -> NF vars -> NF vars -> Constraint
  
Resolved : Constraint
data PolyConstraint : Type
  Totality: possibly not terminating due to call to $resolved17706
  Visibility: public export
  Constructor: 
MkPolyConstraint : FC -> Env Term vars -> Term vars -> NF vars -> NF vars -> PolyConstraint
data DelayReason : Type
  Totality: total
  Visibility: public export
  Constructors:
  
CaseBlock : DelayReason
  
Ambiguity : DelayReason
  
RecordUpdate : DelayReason
  
Rewrite : DelayReason
  
LazyDelay : DelayReason

  Hints:
  
Eq DelayReason
  
Ord DelayReason
record UState : Type
  Totality: possibly not terminating due to calls to $resolved20207, $resolved20201
  Visibility: public export
  Constructor: 
MkUState : IntMap (FC, Name) -> IntMap (FC, Name) -> IntMap (FC, Name) -> IntMap (FC, Name) -> IntMap Constraint -> IntMap () -> List PolyConstraint -> List (Name, (DotReason, Constraint)) -> Int -> Int -> List (DelayReason, (Int, (NameMap (), Core ClosedTerm))) -> Bool -> UState

  Projections:
  
.constraints : UState -> IntMap Constraint
  
.currentHoles : UState -> IntMap (FC, Name)
  
.delayedElab : UState -> List (DelayReason, (Int, (NameMap (), Core ClosedTerm)))
  
.delayedHoles : UState -> IntMap (FC, Name)
  
.dotConstraints : UState -> List (Name, (DotReason, Constraint))
  
.guesses : UState -> IntMap (FC, Name)
  
.holes : UState -> IntMap (FC, Name)
  
.logging : UState -> Bool
  
.nextConstraint : UState -> Int
  
.nextName : UState -> Int
  
.noSolve : UState -> IntMap ()
  
.polyConstraints : UState -> List PolyConstraint
.holes : UState -> IntMap (FC, Name)
  Visibility: public export
holes : UState -> IntMap (FC, Name)
  Visibility: public export
.guesses : UState -> IntMap (FC, Name)
  Visibility: public export
guesses : UState -> IntMap (FC, Name)
  Visibility: public export
.currentHoles : UState -> IntMap (FC, Name)
  Visibility: public export
currentHoles : UState -> IntMap (FC, Name)
  Visibility: public export
.delayedHoles : UState -> IntMap (FC, Name)
  Visibility: public export
delayedHoles : UState -> IntMap (FC, Name)
  Visibility: public export
.constraints : UState -> IntMap Constraint
  Visibility: public export
constraints : UState -> IntMap Constraint
  Visibility: public export
.noSolve : UState -> IntMap ()
  Visibility: public export
noSolve : UState -> IntMap ()
  Visibility: public export
.polyConstraints : UState -> List PolyConstraint
  Visibility: public export
polyConstraints : UState -> List PolyConstraint
  Visibility: public export
.dotConstraints : UState -> List (Name, (DotReason, Constraint))
  Visibility: public export
dotConstraints : UState -> List (Name, (DotReason, Constraint))
  Visibility: public export
.nextName : UState -> Int
  Visibility: public export
nextName : UState -> Int
  Visibility: public export
.nextConstraint : UState -> Int
  Visibility: public export
nextConstraint : UState -> Int
  Visibility: public export
.delayedElab : UState -> List (DelayReason, (Int, (NameMap (), Core ClosedTerm)))
  Visibility: public export
delayedElab : UState -> List (DelayReason, (Int, (NameMap (), Core ClosedTerm)))
  Visibility: public export
.logging : UState -> Bool
  Visibility: public export
logging : UState -> Bool
  Visibility: public export
initUState : UState
  Visibility: export
data UST : Type
  Totality: total
  Visibility: export
resetNextVar : Ref UST UState => Core ()
  Visibility: export
genName : Ref Ctxt Defs => Ref UST UState => String -> Core Name
  Visibility: export
genMVName : Ref Ctxt Defs => Ref UST UState => Name -> Core Name
  Visibility: export
genVarName : Ref Ctxt Defs => Ref UST UState => String -> Core Name
  Visibility: export
genCaseName : Ref Ctxt Defs => Ref UST UState => String -> Core Name
  Visibility: export
genWithName : Ref Ctxt Defs => Ref UST UState => String -> Core Name
  Visibility: export
removeHole : Ref UST UState => Int -> Core ()
  Visibility: export
removeHoleName : Ref Ctxt Defs => Ref UST UState => Name -> Core ()
  Visibility: export
addNoSolve : Ref UST UState => Int -> Core ()
  Visibility: export
removeNoSolve : Ref UST UState => Int -> Core ()
  Visibility: export
saveHoles : Ref UST UState => Core (IntMap (FC, Name))
  Visibility: export
restoreHoles : Ref UST UState => IntMap (FC, Name) -> Core ()
  Visibility: export
removeGuess : Ref UST UState => Int -> Core ()
  Visibility: export
getHoles : Ref UST UState => Core (IntMap (FC, Name))
  Visibility: export
getGuesses : Ref UST UState => Core (IntMap (FC, Name))
  Visibility: export
getCurrentHoles : Ref UST UState => Core (IntMap (FC, Name))
  Visibility: export
isHole : Ref UST UState => Int -> Core Bool
  Visibility: export
isCurrentHole : Ref UST UState => Int -> Core Bool
  Visibility: export
setConstraint : Ref UST UState => Int -> Constraint -> Core ()
  Visibility: export
deleteConstraint : Ref UST UState => Int -> Core ()
  Visibility: export
addConstraint : Ref UST UState => Ref Ctxt Defs => Constraint -> Core Int
  Visibility: export
addDot : Ref Ctxt Defs => Ref UST UState => FC -> Env Term vars -> Name -> Term vars -> DotReason -> Term vars -> Core ()
  Visibility: export
addPolyConstraint : Ref UST UState => FC -> Env Term vars -> Term vars -> NF vars -> NF vars -> Core ()
  Visibility: export
applyTo : FC -> Term vars -> Env Term vars -> Term vars
  Visibility: export
applyToFull : FC -> Term vars -> Env Term vars -> Term vars
  Visibility: export
applyToSub : FC -> Term vars -> Env Term vars -> Thin smaller vars -> Term vars
  Visibility: export
applyToOthers : FC -> Term vars -> Env Term vars -> Thin smaller vars -> Term vars
  Visibility: export
newMetaLets : Ref Ctxt Defs => Ref UST UState => FC -> RigCount -> Env Term vars -> Name -> Term vars -> Def -> Bool -> Bool -> Core (Int, Term vars)
  Visibility: export
newMeta : Ref Ctxt Defs => Ref UST UState => FC -> RigCount -> Env Term vars -> Name -> Term vars -> Def -> Bool -> Core (Int, Term vars)
  Visibility: export
newConstant : Ref UST UState => Ref Ctxt Defs => FC -> RigCount -> Env Term vars -> Term vars -> Term vars -> List Int -> Core (Term vars)
  Visibility: export
newSearch : Ref Ctxt Defs => Ref UST UState => FC -> RigCount -> Nat -> Name -> Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
  Visibility: export
newDelayed : Ref UST UState => Ref Ctxt Defs => FC -> RigCount -> Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
  Visibility: export
tryErrorUnify : Ref Ctxt Defs => Ref UST UState => {default False _ : Bool} -> Core a -> Core (Either Error a)
  Visibility: export
tryUnify : Ref Ctxt Defs => Ref UST UState => Core a -> Core a -> Core a
  Visibility: export
handleUnify : Ref Ctxt Defs => Ref UST UState => {default False _ : Bool} -> Core a -> (Error -> Core a) -> Core a
  Visibility: export
addDelayedHoleName : Ref UST UState => (Int, (FC, Name)) -> Core ()
  Visibility: export
checkDelayedHoles : Ref UST UState => Core (Maybe Error)
  Visibility: export
checkUserHolesAfter : Ref UST UState => Ref Ctxt Defs => Int -> Bool -> Core ()
  Visibility: export
checkUserHoles : Ref UST UState => Ref Ctxt Defs => Bool -> Core ()
  Visibility: export
checkNoGuards : Ref UST UState => Ref Ctxt Defs => Core ()
  Visibility: export
dumpHole : Ref UST UState => Ref Ctxt Defs => LogTopic -> Nat -> Int -> Core ()
  Visibility: export
dumpConstraints : Ref UST UState => Ref Ctxt Defs => LogTopic -> Nat -> Bool -> Core ()
  Visibility: export