Idris2Doc : Language.Reflection.Types

Language.Reflection.Types

(source)
Definitions
Res : Type -> Type
  Totality: total
  Visibility: public export
freshNames : String -> (n : Nat) -> Vect n Name
  Creates a sequence of argument names, using the given string as a prefix
  and appending names with their index in the sequence.
  
  It is at times necessary to provide a set of fresh names to
  for instance pattern matching on a data constructor making sure
  to not shadow already existing
  names. This function provides a pure way to do so without having
  to run this in the `Elab` monad.

  Totality: total
  Visibility: export
implicits : Foldable t => t Name -> List Arg
  Totality: total
  Visibility: public export
tryAll : Applicative f => ((v : a) -> f (p v)) -> (vs : Vect n a) -> f (All p vs)
  Tries to generate the given proofs for all values in the
  given vector over an applicative functor.

  Totality: total
  Visibility: public export
data MissingInfo : PiInfo TTImp -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Auto : MissingInfo AutoImplicit
  
Implicit : MissingInfo ImplicitArg
  
Deflt : MissingInfo (DefImplicit t)

  Hint: 
Uninhabited (MissingInfo ExplicitArg)
data AppArg : Arg -> Type
  An argument extracted from an applied function.
  
  We use these to match result types of data constructors against the
  arguments of the corresponding type constructor, so they
  are indexed by the corresponding argument.

  Totality: total
  Visibility: public export
  Constructors:
  
NamedApp : (n : Name) -> TTImp -> AppArg (MkArg c p (Just n) t)
  Named application: `foo {x = 12}`
  
AutoApp : TTImp -> AppArg (MkArg c AutoImplicit n t)
  Applying an unnamed auto implicit: `foo @{MyEq}`
  
Regular : TTImp -> AppArg (MkArg c ExplicitArg n t)
  Regular function application: `foo 12`.
  
Missing : MissingInfo p -> AppArg (MkArg c p n t)
  An implicit argument not given explicitly.
.ttimp : AppArg a -> TTImp
  Totality: total
  Visibility: public export
appArg : TTImp -> AppArg a -> TTImp
  Applies an argument to the given value.

  Totality: total
  Visibility: public export
0 AppArgs : Vect n Arg -> Type
  Sequence of applied arguments matching a list of function arguments.

  Totality: total
  Visibility: public export
getArg : (arg : Arg) -> TTImp -> Maybe (AppArg arg, TTImp)
  Tries to extract an applied argument from an expression,
  returning it together with the remainder of the expression.

  Totality: total
  Visibility: export
getArgs : (vs : Vect n Arg) -> TTImp -> Res (AppArgs vs, TTImp)
  Tries to unapply an expression and extract all
  applied function arguments.

  Totality: total
  Visibility: public export
record Con : (n : Nat) -> Vect n Arg -> Type
  Data constructor of a data type index over the list of arguments
  of the corresponding type constructor.

  Totality: total
  Visibility: public export
  Constructor: 
MkCon : Name -> (arty : Nat) -> Vect arty Arg -> AppArgs vs -> Con n vs

  Projections:
  
.args : ({rec:0} : Con n vs) -> Vect (arty {rec:0}) Arg
  
.arty : Con n vs -> Nat
  
.name : Con n vs -> Name
  
.typeArgs : Con n vs -> AppArgs vs

  Hint: 
Named (Con n vs)
.name : Con n vs -> Name
  Totality: total
  Visibility: public export
name : Con n vs -> Name
  Totality: total
  Visibility: public export
.arty : Con n vs -> Nat
  Totality: total
  Visibility: public export
arty : Con n vs -> Nat
  Totality: total
  Visibility: public export
.args : ({rec:0} : Con n vs) -> Vect (arty {rec:0}) Arg
  Totality: total
  Visibility: public export
args : ({rec:0} : Con n vs) -> Vect (arty {rec:0}) Arg
  Totality: total
  Visibility: public export
.typeArgs : Con n vs -> AppArgs vs
  Totality: total
  Visibility: public export
typeArgs : Con n vs -> AppArgs vs
  Totality: total
  Visibility: public export
isConstant : Con n vs -> Bool
  True if the given constructor has only erased arguments.

  Totality: total
  Visibility: public export
bindCon : (c : Con n vs) -> Vect (c .arty) Name -> TTImp
  Creates bindings for the explicit arguments of a data constructor
  using the given prefix plus an index for the name of each
  argument.
  
  This is useful for implementing functions which pattern match on a
  data constructor.

  Totality: total
  Visibility: export
applyCon : (c : Con n vs) -> Vect (c .arty) Name -> TTImp
  Applies a constructor to variables of the given name.

  Totality: total
  Visibility: export
getCon : Elaboration m => (vs : Vect n Arg) -> Name -> m (Con n vs)
  Tries to lookup a data constructor by name, based on the
  given list of arguments of the corresponding data constructor.

  Totality: total
  Visibility: export
record TypeInfo : Type
  Information about a data type
  
  @name : Name of the data type
          Note: There is no guarantee that the name will be fully
          qualified
  @args : Type arguments of the data type
  @cons : List of data constructors

  Totality: total
  Visibility: public export
  Constructor: 
MkTypeInfo : Name -> (arty : Nat) -> (args : Vect arty Arg) -> Vect arty Name -> List (Con arty args) -> TypeInfo

  Projections:
  
.argNames : ({rec:0} : TypeInfo) -> Vect (arty {rec:0}) Name
  
.args : ({rec:0} : TypeInfo) -> Vect (arty {rec:0}) Arg
  
.arty : TypeInfo -> Nat
  
.cons : ({rec:0} : TypeInfo) -> List (Con (arty {rec:0}) (args {rec:0}))
  
.name : TypeInfo -> Name

  Hints:
  
Elaborateable TypeInfo
  
Named TypeInfo
.name : TypeInfo -> Name
  Totality: total
  Visibility: public export
name : TypeInfo -> Name
  Totality: total
  Visibility: public export
.arty : TypeInfo -> Nat
  Totality: total
  Visibility: public export
arty : TypeInfo -> Nat
  Totality: total
  Visibility: public export
.args : ({rec:0} : TypeInfo) -> Vect (arty {rec:0}) Arg
  Totality: total
  Visibility: public export
args : ({rec:0} : TypeInfo) -> Vect (arty {rec:0}) Arg
  Totality: total
  Visibility: public export
.argNames : ({rec:0} : TypeInfo) -> Vect (arty {rec:0}) Name
  Totality: total
  Visibility: public export
argNames : ({rec:0} : TypeInfo) -> Vect (arty {rec:0}) Name
  Totality: total
  Visibility: public export
.cons : ({rec:0} : TypeInfo) -> List (Con (arty {rec:0}) (args {rec:0}))
  Totality: total
  Visibility: public export
cons : ({rec:0} : TypeInfo) -> List (Con (arty {rec:0}) (args {rec:0}))
  Totality: total
  Visibility: public export
namedArg : Arg -> Maybe Name
  Totality: total
  Visibility: public export
.explicitArgs : TypeInfo -> List Name
  Returns the names of explicit arguments of a type constructor.

  Totality: total
  Visibility: public export
.applied : TypeInfo -> TTImp
  Returns a type constructor
  applied to the names of its explicit arguments

  Totality: total
  Visibility: public export
.implicits : TypeInfo -> List Arg
  Returns a list of implicit arguments corresponding
  to the data type's implicit and explicit arguments.

  Totality: total
  Visibility: public export
isEnum : TypeInfo -> Bool
  True if the given type has only constant constructors and
  is therefore represented by a single unsigned integer at runtime.

  Totality: total
  Visibility: public export
isNil : Con n vs -> Bool
  True if the given constructor has name `Nil` and no explicit arguments.

  Totality: total
  Visibility: public export
isCons : Con n vs -> Bool
  True if the given constructor has name `(::)` and
  exactly two explicit arguments.

  Totality: total
  Visibility: public export
isLin : Con n vs -> Bool
  True if the given constructor has name `Lin` and no explicit arguments.

  Totality: total
  Visibility: public export
isSnoc : Con n vs -> Bool
  True if the given constructor has name `(:<)` and
  exactly two explicit arguments.

  Totality: total
  Visibility: public export
isNewtype : TypeInfo -> Bool
  True if the given type has a single constructor with a single
  unerased argument.

  Totality: total
  Visibility: public export
isListLike : TypeInfo -> Bool
  True, if the given type has exactly one
  `Nil` constructor with no explicit
  argument and a `(::)` constructor with two explicit arguments.

  Totality: total
  Visibility: public export
isSnocListLike : TypeInfo -> Bool
  True, if the given type has exactly one
  `Lin` constructor with no explicit
  argument and a `(:<)` constructor with two explicit arguments.

  Totality: total
  Visibility: public export
isErased : TypeInfo -> Bool
  True if the given type has a single constructor with only erased
  arguments. Such a value will have a trivial runtime representation.

  Totality: total
  Visibility: public export
getInfo' : Elaboration m => Name -> m TypeInfo
  Tries to get information about the data type specified
  by name. The name need not be fully qualified, but
  needs to be unambiguous.

  Totality: total
  Visibility: export
getInfo : Name -> Elab TypeInfo
  macro version of `getInfo'`

  Totality: total
  Visibility: export
singleCon : Name -> Elab Name
  Tries to get the name of the sole constructor
  of data type specified by name. Fails, if
  the name is not unambiguous, or if the data type
  in question has not exactly one constructor.

  Totality: total
  Visibility: export
data ParamTag : Nat -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
I : ParamTag 0
  
P : ParamTag 1
data ParamPattern : Nat -> Nat -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Nil : ParamPattern 0 0
  
(::) : ParamTag k -> ParamPattern m n -> ParamPattern (S m) (k + n)
paramsOnly : (k : Nat) -> ParamPattern k k
  Totality: total
  Visibility: public export
indicesOnly : (k : Nat) -> ParamPattern k 0
  Totality: total
  Visibility: public export
extractParams : ParamPattern n k -> Vect n a -> Vect k a
  Totality: total
  Visibility: public export
data PArg : Nat -> Type
  Constructor argument type in a parameterized data type
  with `n` parameters.

  Totality: total
  Visibility: public export
  Constructors:
  
PPar : Fin n -> PArg n
  
PVar : Name -> PArg n
  
PLam : Count -> PiInfo TTImp -> Maybe Name -> PArg n -> PArg n -> PArg n
  
PApp : PArg n -> PArg n -> PArg n
  
PNamedApp : PArg n -> Name -> PArg n -> PArg n
  
PAutoApp : PArg n -> PArg n -> PArg n
  
PWithApp : PArg n -> PArg n -> PArg n
  
PSearch : Nat -> PArg n
  
PPrim : Constant -> PArg n
  
PDelayed : LazyReason -> PArg n -> PArg n
  
PType : PArg n
  
PHole : String -> PArg n

  Hint: 
Eq (PArg n)
pvar : Named a => Vect n a -> List Name -> Name -> PArg n
  Checks if the given name corresponds to a parameter, in
  which case it must be present in the given vector of names.

  Totality: total
  Visibility: public export
parg : Named a => Vect n a -> List Name -> TTImp -> Res (PArg n)
  Tries to convert a `TTImp` to an argument of a
  parameterized constructor using the given vector of parameter names.

  Totality: total
  Visibility: public export
ttimp : Vect n Name -> PArg n -> TTImp
  Converts an argument of a parameterized data type to the
  corresponding `TTImp` expression.

  Totality: total
  Visibility: public export
paramArgs : PArg n -> List (PArg n)
  Extracts the sub-expressions from an argument's type
  where the outermost value is a parameter.
  
  Example:
  If `f`, `a`, and `b` are parameters, this will extract
  `[f Int, f a, b]` from `Maybe (Pair (f Int, Pair (f a, b)))`

  Totality: total
  Visibility: public export
paramNames : ParamPattern n k -> AppArgs vs -> Res (Vect k Name)
  Totality: total
  Visibility: public export
data ConArg : Nat -> Type
  Argument of a data constructor of a parameterized data type.

  Totality: total
  Visibility: public export
  Constructors:
  
ParamArg : Fin n -> TTImp -> ConArg n
  
CArg : Maybe Name -> Count -> PiInfo TTImp -> PArg n -> ConArg n
isExplicit : ConArg n -> Bool
  Totality: total
  Visibility: public export
conArg : Vect n Name -> Arg -> Res (ConArg n)
  Totality: total
  Visibility: public export
paramArgs : ConArg n -> List (PArg n)
  Totality: total
  Visibility: public export
record ParamCon : Nat -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkParamCon : Name -> (arty : Nat) -> Vect arty (ConArg n) -> ParamCon n

  Projections:
  
.args : ({rec:0} : ParamCon n) -> Vect (arty {rec:0}) (ConArg n)
  
.arty : ParamCon n -> Nat
  
.name : ParamCon n -> Name

  Hint: 
Named (ParamCon n)
.name : ParamCon n -> Name
  Totality: total
  Visibility: public export
name : ParamCon n -> Name
  Totality: total
  Visibility: public export
.arty : ParamCon n -> Nat
  Totality: total
  Visibility: public export
arty : ParamCon n -> Nat
  Totality: total
  Visibility: public export
.args : ({rec:0} : ParamCon n) -> Vect (arty {rec:0}) (ConArg n)
  Totality: total
  Visibility: public export
args : ({rec:0} : ParamCon n) -> Vect (arty {rec:0}) (ConArg n)
  Totality: total
  Visibility: public export
paramArgs : ParamCon n -> List (PArg n)
  Totality: total
  Visibility: public export
paramCon : ParamPattern n k -> Con n vs -> Res (ParamCon k)
  Totality: total
  Visibility: public export
record ParamTypeInfo : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkParamTypeInfo : (info : TypeInfo) -> ParamPattern (info .arty) numParams -> Vect numParams Name -> List (ParamCon numParams) -> List (PArg numParams) -> ParamTypeInfo

  Projections:
  
.applied : ParamTypeInfo -> TTImp
  Returns the type constructor of a parameterized
  data type applied to its parameters
  
.cons : ({rec:0} : ParamTypeInfo) -> List (ParamCon (numParams {rec:0}))
  List of data constructors
  
.implicits : ParamTypeInfo -> List Arg
  Returns a list of implicit arguments corresponding
  to the data type's arguments.
  
.info : ParamTypeInfo -> TypeInfo
  Underlying type info
  
0 .numParams : ParamTypeInfo -> Nat
  
.paramNames : ({rec:0} : ParamTypeInfo) -> Vect (numParams {rec:0}) Name
  Name of parameters
  
.pargs : ({rec:0} : ParamTypeInfo) -> List (PArg (numParams {rec:0}))
  List of types appearing in constructor arguments, where the
  the outermost applied type is one of the parameters. We use this
  to generate the constraints necessary to implement interfaces such
  as `Eq` or `Ord`.
  
  For instance, in case of a constructor argument `Either (f a) (b, f Nat)`
  with `f`, `a`, and `b` being parameters, this list will contain
  the encoded forms of `f a`, `f Nat`, and `b`.
  
.pattern : ({rec:0} : ParamTypeInfo) -> ParamPattern ((info {rec:0}) .arty) (numParams {rec:0})
  Information about which type arguments are parameters and
  which are indices

  Hint: 
Named ParamTypeInfo
.info : ParamTypeInfo -> TypeInfo
  Underlying type info

  Totality: total
  Visibility: public export
info : ParamTypeInfo -> TypeInfo
  Underlying type info

  Totality: total
  Visibility: public export
.pattern : ({rec:0} : ParamTypeInfo) -> ParamPattern ((info {rec:0}) .arty) (numParams {rec:0})
  Information about which type arguments are parameters and
  which are indices

  Totality: total
  Visibility: public export
pattern : ({rec:0} : ParamTypeInfo) -> ParamPattern ((info {rec:0}) .arty) (numParams {rec:0})
  Information about which type arguments are parameters and
  which are indices

  Totality: total
  Visibility: public export
.paramNames : ({rec:0} : ParamTypeInfo) -> Vect (numParams {rec:0}) Name
  Name of parameters

  Totality: total
  Visibility: public export
paramNames : ({rec:0} : ParamTypeInfo) -> Vect (numParams {rec:0}) Name
  Name of parameters

  Totality: total
  Visibility: public export
.cons : ({rec:0} : ParamTypeInfo) -> List (ParamCon (numParams {rec:0}))
  List of data constructors

  Totality: total
  Visibility: public export
cons : ({rec:0} : ParamTypeInfo) -> List (ParamCon (numParams {rec:0}))
  List of data constructors

  Totality: total
  Visibility: public export
.pargs : ({rec:0} : ParamTypeInfo) -> List (PArg (numParams {rec:0}))
  List of types appearing in constructor arguments, where the
  the outermost applied type is one of the parameters. We use this
  to generate the constraints necessary to implement interfaces such
  as `Eq` or `Ord`.
  
  For instance, in case of a constructor argument `Either (f a) (b, f Nat)`
  with `f`, `a`, and `b` being parameters, this list will contain
  the encoded forms of `f a`, `f Nat`, and `b`.

  Totality: total
  Visibility: public export
pargs : ({rec:0} : ParamTypeInfo) -> List (PArg (numParams {rec:0}))
  List of types appearing in constructor arguments, where the
  the outermost applied type is one of the parameters. We use this
  to generate the constraints necessary to implement interfaces such
  as `Eq` or `Ord`.
  
  For instance, in case of a constructor argument `Either (f a) (b, f Nat)`
  with `f`, `a`, and `b` being parameters, this list will contain
  the encoded forms of `f a`, `f Nat`, and `b`.

  Totality: total
  Visibility: public export
paramType : (ti : TypeInfo) -> ParamPattern (ti .arty) k -> Res ParamTypeInfo
  Totality: total
  Visibility: public export
constraints : ParamTypeInfo -> Name -> List Arg
  Returns the constraints required to implement the given interface
  for the given parameterized data types.
  
  The interface must be of type `Type -> Type`.

  Totality: total
  Visibility: export
.applied : ParamTypeInfo -> TTImp
  Returns the type constructor of a parameterized
  data type applied to its parameters

  Totality: total
  Visibility: public export
.implicits : ParamTypeInfo -> List Arg
  Returns a list of implicit arguments corresponding
  to the data type's arguments.

  Totality: total
  Visibility: public export
allImplicits : ParamTypeInfo -> Name -> List Arg
  Short-hand for `p.implicits ++ constraints iname p`.

  Totality: total
  Visibility: public export
getParamInfo' : Elaboration m => Name -> m ParamTypeInfo
  Returns information about a parameterized data type
  specified by the given (probably not fully qualified) name
  and a strategy for distinguishing between type parameters
  and indices.

  Totality: total
  Visibility: export
getParamInfo : Name -> Elab ParamTypeInfo
  macro version of `getParamInfo`.

  Totality: total
  Visibility: export