Deriving.Common

Definitions

data IsFreeOf : Name -> TTImp -> Type

  IsFreeOf is parametrised by
  @ x  the name of the type variable that the functioral action will change
  @ ty the type that does not contain any mention of x

Totality: total
Visibility: export
Constructor: 

TrustMeFO : IsFreeOf a x

  For now we do not bother keeping precise track of the proof that a type
  is free of x

assert_IsFreeOf : IsFreeOf x ty

  We may need to manufacture proofs and so we provide the `assert` escape hatch.

Totality: total
Visibility: export

isFreeOf : (x : Name) -> (ty : TTImp) -> Maybe (IsFreeOf x ty)

  Testing function deciding whether the given term is free of a particular
  variable.

Totality: total
Visibility: export

record IsType : Type

Totality: total
Visibility: public export
Constructor: 

MkIsType : Name -> List (Argument Name, Nat) -> List (Name, TTImp) -> IsType

Projections:

.dataConstructors : IsType -> List (Name, TTImp)

.parameterNames : IsType -> List (Argument Name, Nat)

.typeConstructor : IsType -> Name

.typeConstructor : IsType -> Name

Totality: total
Visibility: public export

typeConstructor : IsType -> Name

Totality: total
Visibility: public export

.parameterNames : IsType -> List (Argument Name, Nat)

Totality: total
Visibility: public export

parameterNames : IsType -> List (Argument Name, Nat)

Totality: total
Visibility: public export

.dataConstructors : IsType -> List (Name, TTImp)

Totality: total
Visibility: public export

dataConstructors : IsType -> List (Name, TTImp)

Totality: total
Visibility: public export

isType : Elaboration m => TTImp -> m IsType

Totality: total
Visibility: export

record ConstructorView : Type

Totality: total
Visibility: public export
Constructor: 

MkConstructorView : SnocList (Name, Nat) -> List (Count, Argument TTImp) -> ConstructorView

Projections:

.conArgTypes : ConstructorView -> List (Count, Argument TTImp)

.params : ConstructorView -> SnocList (Name, Nat)

.params : ConstructorView -> SnocList (Name, Nat)

Totality: total
Visibility: public export

params : ConstructorView -> SnocList (Name, Nat)

Totality: total
Visibility: public export

.conArgTypes : ConstructorView -> List (Count, Argument TTImp)

Totality: total
Visibility: public export

conArgTypes : ConstructorView -> List (Count, Argument TTImp)

Totality: total
Visibility: public export

constructorView : TTImp -> Maybe ConstructorView

Totality: total
Visibility: export

withParams : FC -> (Nat -> Maybe TTImp) -> List (Argument Name, Nat) -> TTImp -> TTImp

Totality: total
Visibility: export

data HasType : Name -> TTImp -> Type

  Type of proofs that something has a given type

Totality: total
Visibility: export
Constructor: 

TrustMeHT : HasType nm ty

hasType : Elaboration m => (nm : Name) -> m (Maybe (ty : TTImp ** HasType nm ty))

Totality: total
Visibility: export

data IsProvable : TTImp -> Type

  Type of proofs that a type is inhabited

Totality: total
Visibility: export
Constructor: 

TrustMeIP : IsProvable ty

isProvable : Elaboration m => (ty : TTImp) -> m (Maybe (IsProvable ty))

Totality: total
Visibility: export

data HasImplementation : (a -> Type) -> TTImp -> Type

  Type of proofs that a type satisfies a constraint.
  Internally it's vacuous. We don't export the constructor so
  that users cannot manufacture buggy proofs.

Totality: total
Visibility: export
Constructor: 

TrustMeHI : HasImplementation intf t

assert_hasImplementation : HasImplementation intf t

  We may need to manufacture proofs and so we provide the `assert` escape hatch.

Totality: total
Visibility: export

hasImplementation : Elaboration m => (intf : (a -> Type)) -> (t : TTImp) -> m (Maybe (HasImplementation intf t))

  Given
  @ intf an interface (e.g. `Functor`, or `Bifunctor`)
  @ t    a term corresponding to a (possibly partially applied) type constructor
  check whether Idris2 can find a proof that t satisfies the interface.

Totality: total
Visibility: export

optionallyEta : FC -> Maybe TTImp -> (TTImp -> TTImp) -> TTImp

  Optionally eta-expand if there is no argument available

Totality: total
Visibility: export

apply : FC -> TTImp -> List TTImp -> TTImp

  We often apply multiple arguments, this makes things simpler

Totality: total
Visibility: export

cleanup : TTImp -> TTImp

  Use unqualified names (useful for more compact printing)

Totality: total
Visibility: export

freshName : List Name -> String -> String

  Create fresh names

Totality: total
Visibility: export