Core.Name

Reexports

Definitions

data UserName : Type

  A username has some structure

Totality: total
Visibility: public export
Constructors:

Basic : String -> UserName

Field : String -> UserName

Underscore : UserName

Hints:

Eq UserName

Ord UserName

Pretty Void UserName

Show UserName

mkUserName : String -> UserName

  A smart constructor taking a string and parsing it as the appropriate
  username

Totality: total
Visibility: export

data Name : Type

  Name helps us track a name's structure as well as its origin:
  was it user-provided or machine-manufactured? For what reason?

Totality: total
Visibility: public export
Constructors:

NS : Namespace -> Name -> Name

UN : UserName -> Name

MN : String -> Int -> Name

PV : Name -> Int -> Name

DN : String -> Name -> Name

Nested : (Int, Int) -> Name -> Name

CaseBlock : String -> Int -> Name

WithBlock : String -> Int -> Name

Resolved : Int -> Name

Hints:

Eq Name

FreelyEmbeddable (IsVar x k)

FreelyEmbeddable Var

FreelyEmbeddable (NVar nm)

GenWeaken Var

GenWeaken (NVar nm)

HasNames (PatInfo n vars)

HasNames (NamedPats todo vars)

HasNames (PatClause todo vars)

HasNames (Int, (FC, Name))

HasNames (Name, Bool)

HasNames (Name, List a)

HasNames (Name, Transform)

HasNames (Name, (Name, Bool))

HasNames Name

Hashable Name

IsScoped Var

Ord Name

Pretty IdrisSyntax (NamedPats todo vars)

Pretty IdrisSyntax (PatClause todo vars)

Pretty Void Name

SExpable Name

Show (ArgType ns)

Show (PatInfo n vars)

Show (NamedPats todo vars)

Show (PatClause todo vars)

Show (Partitions ps)

Show (Group todo vars)

Show (ScoredPats ps ns)

Show (NHead free)

Show (NF free)

Show (Lifted vs)

Show (LiftedConAlt vs)

Show (LiftedConstAlt vs)

Show (CaseTree vars)

Show (CaseAlt vars)

Show (CExp vars)

Show (Term vars)

Show Name

Strengthen Var

Strengthen (NVar nm)

StripNamespace Name

TTC Name

TTC (Binder (Term vars))

TTC (Term vars)

TTC (CaseTree vars)

TTC (CaseAlt vars)

TTC (Env Term vars)

TTC (CExp vars)

TTC (CConAlt vars)

TTC (CConstAlt vars)

Weaken (PatInfo p)

Weaken (NamedPats todo)

Weaken Var

Weaken (NVar nm)

mkNamespacedName : Maybe Namespace -> UserName -> Name

Totality: total
Visibility: export

matches : Name -> Name -> Bool

  `matches a b` checks that the name `a` matches `b` assuming
  the name roots are already known to be matching.
  For instance, both `reverse` and `List.reverse` match the fully
  qualified name `Data.List.reverse`.

Totality: total
Visibility: export

asName : ModuleIdent -> Namespace -> Name -> Name

Totality: total
Visibility: export

userNameRoot : Name -> Maybe UserName

Totality: total
Visibility: export

isOpChar : Char -> Bool

Totality: total
Visibility: export

isOpUserName : UserName -> Bool

  Test whether a user name begins with an operator symbol.

Totality: total
Visibility: export

isOpName : Name -> Bool

  Test whether a name begins with an operator symbol.

Totality: total
Visibility: export

isUnderscoreName : Name -> Bool

Totality: total
Visibility: export

isPatternVariable : UserName -> Bool

Totality: total
Visibility: export

isUserName : Name -> Bool

Totality: total
Visibility: export

isSourceName : Name -> Bool

  True iff name can be traced back to a source name.
  Used to determine whether it needs semantic highlighting.

Totality: total
Visibility: export

isRF : Name -> Maybe (Namespace, String)

Totality: total
Visibility: export

isUN : Name -> Maybe (Namespace, UserName)

Totality: total
Visibility: export

isBasic : UserName -> Maybe String

Totality: total
Visibility: export

isField : UserName -> Maybe String

Totality: total
Visibility: export

caseFn : Name -> Bool

Totality: total
Visibility: export

displayUserName : UserName -> String

Totality: total
Visibility: export

nameRoot : Name -> String

Totality: total
Visibility: export

displayName : Name -> (Maybe Namespace, String)

Totality: total
Visibility: export

splitNS : Name -> (Namespace, Name)

Totality: total
Visibility: export

dropNS : Name -> Name

Totality: total
Visibility: export

dropAllNS : Name -> Name

Totality: total
Visibility: export

mbApplyNS : Maybe Namespace -> Name -> Name

Totality: total
Visibility: export

isUnsafeBuiltin : Name -> Bool

Totality: total
Visibility: export

isPrettyOp : Bool -> Name -> Bool

  Will it be an operation once prettily displayed?
  The first boolean states whether the operator is prefixed.

Totality: total
Visibility: export

prettyOp : Bool -> Name -> Doc Void

Visibility: export

userNameEq : (x : UserName) -> (y : UserName) -> Maybe (x = y)

Totality: total
Visibility: export

nameEq : (x : Name) -> (y : Name) -> Maybe (x = y)

Totality: total
Visibility: export

namesEq : (xs : List Name) -> (ys : List Name) -> Maybe (xs = ys)

Totality: total
Visibility: export

next : Name -> Name

  Generate the next machine name

Totality: total
Visibility: export

closeMatch : Name -> Name -> IO Bool

  Check if the test closely match the reference.
  We only check for namespaces and user-defined names.

Totality: total
Visibility: export