Idris2Doc : Language.Reflection.Unify.Interface

Language.Reflection.Unify.Interface

(source)
Definitions
record UnificationTask : Type
  Unification task

  Totality: total
  Visibility: public export
  Constructor: 
MkUniTask : (lhsFreeVars : Vect lfv Arg) -> {auto 0 _ : All IsNamedArg lhsFreeVars} -> TTImp -> (rhsFreeVars : Vect rfv Arg) -> {auto 0 _ : All IsNamedArg rhsFreeVars} -> TTImp -> UnificationTask

  Projections:
  
.lfv : UnificationTask -> Nat
  Amount of left-hand-side free variables
  
0 .lhsAreNamed : ({rec:0} : UnificationTask) -> All IsNamedArg (lhsFreeVars {rec:0})
  
.lhsExpr : UnificationTask -> TTImp
  Left-hand-side expression
  
.lhsFreeVars : ({rec:0} : UnificationTask) -> Vect (lfv {rec:0}) Arg
  Left-hand-side free variables
  
.rfv : UnificationTask -> Nat
  Amount of right-hand-side free variables
  
0 .rhsAreNamed : ({rec:0} : UnificationTask) -> All IsNamedArg (rhsFreeVars {rec:0})
  
.rhsExpr : UnificationTask -> TTImp
  Right-hand-side expression
  
.rhsFreeVars : ({rec:0} : UnificationTask) -> Vect (rfv {rec:0}) Arg
  Right-hand-side free variables

  Hint: 
Show UnificationTask
.lfv : UnificationTask -> Nat
  Amount of left-hand-side free variables

  Totality: total
  Visibility: public export
lfv : UnificationTask -> Nat
  Amount of left-hand-side free variables

  Totality: total
  Visibility: public export
.lhsFreeVars : ({rec:0} : UnificationTask) -> Vect (lfv {rec:0}) Arg
  Left-hand-side free variables

  Totality: total
  Visibility: public export
lhsFreeVars : ({rec:0} : UnificationTask) -> Vect (lfv {rec:0}) Arg
  Left-hand-side free variables

  Totality: total
  Visibility: public export
0 .lhsAreNamed : ({rec:0} : UnificationTask) -> All IsNamedArg (lhsFreeVars {rec:0})
  Totality: total
  Visibility: public export
0 lhsAreNamed : ({rec:0} : UnificationTask) -> All IsNamedArg (lhsFreeVars {rec:0})
  Totality: total
  Visibility: public export
.lhsExpr : UnificationTask -> TTImp
  Left-hand-side expression

  Totality: total
  Visibility: public export
lhsExpr : UnificationTask -> TTImp
  Left-hand-side expression

  Totality: total
  Visibility: public export
.rfv : UnificationTask -> Nat
  Amount of right-hand-side free variables

  Totality: total
  Visibility: public export
rfv : UnificationTask -> Nat
  Amount of right-hand-side free variables

  Totality: total
  Visibility: public export
.rhsFreeVars : ({rec:0} : UnificationTask) -> Vect (rfv {rec:0}) Arg
  Right-hand-side free variables

  Totality: total
  Visibility: public export
rhsFreeVars : ({rec:0} : UnificationTask) -> Vect (rfv {rec:0}) Arg
  Right-hand-side free variables

  Totality: total
  Visibility: public export
0 .rhsAreNamed : ({rec:0} : UnificationTask) -> All IsNamedArg (rhsFreeVars {rec:0})
  Totality: total
  Visibility: public export
0 rhsAreNamed : ({rec:0} : UnificationTask) -> All IsNamedArg (rhsFreeVars {rec:0})
  Totality: total
  Visibility: public export
.rhsExpr : UnificationTask -> TTImp
  Right-hand-side expression

  Totality: total
  Visibility: public export
rhsExpr : UnificationTask -> TTImp
  Right-hand-side expression

  Totality: total
  Visibility: public export
sUT : Show UnificationTask
  Totality: total
  Visibility: export
record FVData : Type
  Free variable output data

  Totality: total
  Visibility: public export
  Constructor: 
MkFVData : Name -> String -> Count -> PiInfo TTImp -> TTImp -> Maybe TTImp -> FVData

  Projections:
  
.holeName : FVData -> String
  Free variable hole name
  
.name : FVData -> Name
  Free variable name
  
.piInfo : FVData -> PiInfo TTImp
  Free variable PiInfo
  
.rig : FVData -> Count
  Free variable count
  
.type : FVData -> TTImp
  Free variable type
  
.value : FVData -> Maybe TTImp
  Free variable value

  Hints:
  
Eq FVData
  
Interpolation FVData
  
Show FVData
.name : FVData -> Name
  Free variable name

  Totality: total
  Visibility: public export
name : FVData -> Name
  Free variable name

  Totality: total
  Visibility: public export
.holeName : FVData -> String
  Free variable hole name

  Totality: total
  Visibility: public export
holeName : FVData -> String
  Free variable hole name

  Totality: total
  Visibility: public export
.rig : FVData -> Count
  Free variable count

  Totality: total
  Visibility: public export
rig : FVData -> Count
  Free variable count

  Totality: total
  Visibility: public export
.piInfo : FVData -> PiInfo TTImp
  Free variable PiInfo

  Totality: total
  Visibility: public export
piInfo : FVData -> PiInfo TTImp
  Free variable PiInfo

  Totality: total
  Visibility: public export
.type : FVData -> TTImp
  Free variable type

  Totality: total
  Visibility: public export
type : FVData -> TTImp
  Free variable type

  Totality: total
  Visibility: public export
.value : FVData -> Maybe TTImp
  Free variable value

  Totality: total
  Visibility: public export
value : FVData -> Maybe TTImp
  Free variable value

  Totality: total
  Visibility: public export
sFVData : Show FVData
  Totality: total
  Visibility: export
makeFVData : (String, (Arg, (Name, (TTImp, Maybe TTImp)))) -> FVData
  Make FVData out of most its components and an argument

  Totality: total
  Visibility: export
record FVDeps : Nat -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkFVDeps : FinSet freeVars -> FinSet freeVars -> FinSet freeVars -> FVDeps freeVars

  Projections:
  
.piInfoDeps : FVDeps freeVars -> FinSet freeVars
  
.typeDeps : FVDeps freeVars -> FinSet freeVars
  
.valueDeps : FVDeps freeVars -> FinSet freeVars

  Hints:
  
Eq (FVDeps freeVars)
  
Show (FVDeps freeVars)
.typeDeps : FVDeps freeVars -> FinSet freeVars
  Totality: total
  Visibility: public export
typeDeps : FVDeps freeVars -> FinSet freeVars
  Totality: total
  Visibility: public export
.valueDeps : FVDeps freeVars -> FinSet freeVars
  Totality: total
  Visibility: public export
valueDeps : FVDeps freeVars -> FinSet freeVars
  Totality: total
  Visibility: public export
.piInfoDeps : FVDeps freeVars -> FinSet freeVars
  Totality: total
  Visibility: public export
piInfoDeps : FVDeps freeVars -> FinSet freeVars
  Totality: total
  Visibility: public export
mergeDeps : FVDeps fv -> FinSet fv
  Totality: total
  Visibility: export
removeDeps : FinSet fv -> FVDeps fv -> FVDeps fv
  Totality: total
  Visibility: export
record DependencyGraph : Type
  Free variable depenfdency graph

  Totality: total
  Visibility: public export
  Constructor: 
MkDG : (freeVars : Nat) -> Vect freeVars FVData -> Vect freeVars (FVDeps freeVars) -> FinSet freeVars -> SortedMap Name (Fin freeVars) -> SortedMap String (Fin freeVars) -> DependencyGraph

  Projections:
  
.empties : ({rec:0} : DependencyGraph) -> FinSet (freeVars {rec:0})
  The set of all i: (Fin freeVars), where (index i fvData).value = None
  
.freeVars : DependencyGraph -> Nat
  Free variable amount
  
.fvData : ({rec:0} : DependencyGraph) -> Vect (freeVars {rec:0}) FVData
  Free variable data
  
.fvDeps : ({rec:0} : DependencyGraph) -> Vect (freeVars {rec:0}) (FVDeps (freeVars {rec:0}))
  Free variable dependency matrix
  
.holeToId : ({rec:0} : DependencyGraph) -> SortedMap String (Fin (freeVars {rec:0}))
  For all i : (Fin freeVars); (lookup (index i fvData).holeName holeToId) = i
  
.nameToId : ({rec:0} : DependencyGraph) -> SortedMap Name (Fin (freeVars {rec:0}))
  For all i : (Fin freeVars); (lookup (index i fvData).name nameToId) = i

  Hints:
  
Eq DependencyGraph
  
Show DependencyGraph
.freeVars : DependencyGraph -> Nat
  Free variable amount

  Totality: total
  Visibility: public export
freeVars : DependencyGraph -> Nat
  Free variable amount

  Totality: total
  Visibility: public export
.fvData : ({rec:0} : DependencyGraph) -> Vect (freeVars {rec:0}) FVData
  Free variable data

  Totality: total
  Visibility: public export
fvData : ({rec:0} : DependencyGraph) -> Vect (freeVars {rec:0}) FVData
  Free variable data

  Totality: total
  Visibility: public export
.fvDeps : ({rec:0} : DependencyGraph) -> Vect (freeVars {rec:0}) (FVDeps (freeVars {rec:0}))
  Free variable dependency matrix

  Totality: total
  Visibility: public export
fvDeps : ({rec:0} : DependencyGraph) -> Vect (freeVars {rec:0}) (FVDeps (freeVars {rec:0}))
  Free variable dependency matrix

  Totality: total
  Visibility: public export
.empties : ({rec:0} : DependencyGraph) -> FinSet (freeVars {rec:0})
  The set of all i: (Fin freeVars), where (index i fvData).value = None

  Totality: total
  Visibility: public export
empties : ({rec:0} : DependencyGraph) -> FinSet (freeVars {rec:0})
  The set of all i: (Fin freeVars), where (index i fvData).value = None

  Totality: total
  Visibility: public export
.nameToId : ({rec:0} : DependencyGraph) -> SortedMap Name (Fin (freeVars {rec:0}))
  For all i : (Fin freeVars); (lookup (index i fvData).name nameToId) = i

  Totality: total
  Visibility: public export
nameToId : ({rec:0} : DependencyGraph) -> SortedMap Name (Fin (freeVars {rec:0}))
  For all i : (Fin freeVars); (lookup (index i fvData).name nameToId) = i

  Totality: total
  Visibility: public export
.holeToId : ({rec:0} : DependencyGraph) -> SortedMap String (Fin (freeVars {rec:0}))
  For all i : (Fin freeVars); (lookup (index i fvData).holeName holeToId) = i

  Totality: total
  Visibility: public export
holeToId : ({rec:0} : DependencyGraph) -> SortedMap String (Fin (freeVars {rec:0}))
  For all i : (Fin freeVars); (lookup (index i fvData).holeName holeToId) = i

  Totality: total
  Visibility: public export
record UnificationResult : Type
  Unification result

  Totality: total
  Visibility: public export
  Constructor: 
MkUR : UnificationTask -> (uniDg : DependencyGraph) -> SortedMap Name TTImp -> SortedMap Name TTImp -> SortedMap Name TTImp -> List (Fin (uniDg .freeVars)) -> UnificationResult

  Projections:
  
.fullResult : UnificationResult -> SortedMap Name TTImp
  All free variable values
  
.lhsResult : UnificationResult -> SortedMap Name TTImp
  LHS free variable (polymorphic constructor argument) values
  
.order : ({rec:0} : UnificationResult) -> List (Fin ((uniDg {rec:0}) .freeVars))
  Order of dependency of free variables without values
  (specialised constructor arguments)
  
.rhsResult : UnificationResult -> SortedMap Name TTImp
  RHS free variable (specialised type argument) values
  
.task : UnificationResult -> UnificationTask
  Task given to the unifier
  
.uniDg : UnificationResult -> DependencyGraph
  Dependency graph returned by the unifier

  Hints:
  
Cast (Either (Maybe UnificationError) UnificationResult) UnificationVerdict
  
Show UnificationResult
.task : UnificationResult -> UnificationTask
  Task given to the unifier

  Totality: total
  Visibility: public export
task : UnificationResult -> UnificationTask
  Task given to the unifier

  Totality: total
  Visibility: public export
.uniDg : UnificationResult -> DependencyGraph
  Dependency graph returned by the unifier

  Totality: total
  Visibility: public export
uniDg : UnificationResult -> DependencyGraph
  Dependency graph returned by the unifier

  Totality: total
  Visibility: public export
.lhsResult : UnificationResult -> SortedMap Name TTImp
  LHS free variable (polymorphic constructor argument) values

  Totality: total
  Visibility: public export
lhsResult : UnificationResult -> SortedMap Name TTImp
  LHS free variable (polymorphic constructor argument) values

  Totality: total
  Visibility: public export
.rhsResult : UnificationResult -> SortedMap Name TTImp
  RHS free variable (specialised type argument) values

  Totality: total
  Visibility: public export
rhsResult : UnificationResult -> SortedMap Name TTImp
  RHS free variable (specialised type argument) values

  Totality: total
  Visibility: public export
.fullResult : UnificationResult -> SortedMap Name TTImp
  All free variable values

  Totality: total
  Visibility: public export
fullResult : UnificationResult -> SortedMap Name TTImp
  All free variable values

  Totality: total
  Visibility: public export
.order : ({rec:0} : UnificationResult) -> List (Fin ((uniDg {rec:0}) .freeVars))
  Order of dependency of free variables without values
  (specialised constructor arguments)

  Totality: total
  Visibility: public export
order : ({rec:0} : UnificationResult) -> List (Fin ((uniDg {rec:0}) .freeVars))
  Order of dependency of free variables without values
  (specialised constructor arguments)

  Totality: total
  Visibility: public export
data UnificationError : Type
  Totality: total
  Visibility: public export
  Constructors:
  
CatastrophicError : UnificationError
  
InternalError : String -> UnificationError
  
TargetTypeError : TTImp -> UnificationError
  
ExtractionError : TTImp -> UnificationError
  
NoUnificationError : UnificationError

  Hints:
  
Cast (Either (Maybe UnificationError) UnificationResult) UnificationVerdict
  
Eq UnificationError
  
Show UnificationError
sUE : Show UnificationError
  Totality: total
  Visibility: export
data UnificationVerdict : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Success : UnificationResult -> UnificationVerdict
  
Undecided : UnificationVerdict
  
Fail : UnificationError -> UnificationVerdict

  Hints:
  
Cast (Either (Maybe UnificationError) UnificationResult) UnificationVerdict
  
Show UnificationVerdict
sUV : Show UnificationVerdict
  Totality: total
  Visibility: export
isSuccess : UnificationVerdict -> Bool
  Totality: total
  Visibility: export
isUndecided : UnificationVerdict -> Bool
  Totality: total
  Visibility: export
isFail : UnificationVerdict -> Bool
  Totality: total
  Visibility: export
interface CanUnify : (Type -> Type) -> Type
  Parameters: m
Constructor: 
MkCanUnify

Methods:
  
unify : UnificationTask -> m UnificationVerdict

Implementation: 
Monad m => MonadTrans t => CanUnify m => CanUnify (t m)
unify : CanUnify m => UnificationTask -> m UnificationVerdict
  Totality: total
  Visibility: public export
finalizeDG : Monad m => UnificationTask -> DependencyGraph -> m UnificationResult
  Calculate UnificationResult (var-to-value mappings and empty leaf dependency order)
  
  The function is monadic due to over-normalisation during elaborator script execution causing bad derivator performance

  Totality: total
  Visibility: export