Deriving.DepTyCheck.Gen.Signature

Reexports

import public Data.DPair
import public Data.Fin
import public Data.List.Ex
import public Data.SortedMap
import public Data.SortedMap.Dependent
import public Data.SortedMap.Extra
import public Data.SortedSet
import public Deriving.DepTyCheck.Util.ArgsPerm
import public Deriving.DepTyCheck.Util.Primitives
import public Language.Reflection.Compat
import public Language.Reflection.Expr
import public Language.Reflection.Logging

Definitions

record GenSignature : Type

Totality: total
Visibility: public export
Constructor:

MkGenSignature : (targetType : TypeInfo) -> {auto 0 _ : AllTyArgsNamed targetType} -> SortedSet (Fin ((targetType .args) .length)) -> GenSignature

Projections:

.givenParams : ({rec:0} : GenSignature) -> SortedSet (Fin (((targetType {rec:0}) .args) .length))
.targetType : GenSignature -> TypeInfo
0 .targetTypeCorrect : ({rec:0} : GenSignature) -> AllTyArgsNamed (targetType {rec:0})

Hints:

DeriveBodyForType => ClosuringContext m => Elaboration m => SortedMap GenSignature (ExternalGenSignature, Name) => DerivationClosure m
Eq GenSignature
LogPosition GenSignature
Ord GenSignature

.targetType : GenSignature -> TypeInfo

Totality: total
Visibility: public export

targetType : GenSignature -> TypeInfo

Totality: total
Visibility: public export

0 .targetTypeCorrect : ({rec:0} : GenSignature) -> AllTyArgsNamed (targetType {rec:0})

Totality: total
Visibility: public export

0 targetTypeCorrect : ({rec:0} : GenSignature) -> AllTyArgsNamed (targetType {rec:0})

Totality: total
Visibility: public export

.givenParams : ({rec:0} : GenSignature) -> SortedSet (Fin (((targetType {rec:0}) .args) .length))

Totality: total
Visibility: public export

givenParams : ({rec:0} : GenSignature) -> SortedSet (Fin (((targetType {rec:0}) .args) .length))

Totality: total
Visibility: public export

characteristics : GenSignature -> (String, List Nat)

Totality: total
Visibility: export

showGivens : GenSignature -> String

Totality: total
Visibility: export

.generatedParams : (sig : GenSignature) -> SortedSet (Fin (((sig .targetType) .args) .length))

Totality: total
Visibility: public export

dependeesOfGivens : (sig : GenSignature) -> FinSet (((sig .targetType) .args) .length)

  Set of type arguments for which there exists a given argument depending on it

Totality: total
Visibility: export

canonicSig : GenSignature -> TTImp

Totality: total
Visibility: export

callCanonic : (0 sig : GenSignature) -> Name -> TTImp -> Vect ((sig .givenParams) .size) TTImp -> TTImp

Totality: total
Visibility: export

data ArgExplicitness : Type

Totality: total
Visibility: public export
Constructors:

ExplicitArg : ArgExplicitness
ImplicitArg : ArgExplicitness

Hint:

Eq ArgExplicitness

.toTT : ArgExplicitness -> PiInfo a

Totality: total
Visibility: public export

record ExternalGenSignature : Type

Totality: total
Visibility: public export
Constructor:

MkExternalGenSignature : (targetType : TypeInfo) -> {auto 0 _ : AllTyArgsNamed targetType} -> (givenParams : SortedMap (Fin ((targetType .args) .length)) (ArgExplicitness, Name)) -> Vect (givenParams .size) (Fin (givenParams .size)) -> Vect gendParamsCnt (Fin gendParamsCnt) -> ExternalGenSignature

Projections:

.gendOrder : ({rec:0} : ExternalGenSignature) -> Vect (gendParamsCnt {rec:0}) (Fin (gendParamsCnt {rec:0}))
.gendParamsCnt : ExternalGenSignature -> Nat
.givenParams : ({rec:0} : ExternalGenSignature) -> SortedMap (Fin (((targetType {rec:0}) .args) .length)) (ArgExplicitness, Name)
.givensOrder : ({rec:0} : ExternalGenSignature) -> Vect ((givenParams {rec:0}) .size) (Fin ((givenParams {rec:0}) .size))
.targetType : ExternalGenSignature -> TypeInfo
0 .targetTypeCorrect : ({rec:0} : ExternalGenSignature) -> AllTyArgsNamed (targetType {rec:0})

Hints:

DeriveBodyForType => ClosuringContext m => Elaboration m => SortedMap GenSignature (ExternalGenSignature, Name) => DerivationClosure m
Eq ExternalGenSignature
Ord ExternalGenSignature

.targetType : ExternalGenSignature -> TypeInfo

Totality: total
Visibility: public export

targetType : ExternalGenSignature -> TypeInfo

Totality: total
Visibility: public export

0 .targetTypeCorrect : ({rec:0} : ExternalGenSignature) -> AllTyArgsNamed (targetType {rec:0})

Totality: total
Visibility: public export

0 targetTypeCorrect : ({rec:0} : ExternalGenSignature) -> AllTyArgsNamed (targetType {rec:0})

Totality: total
Visibility: public export

.givenParams : ({rec:0} : ExternalGenSignature) -> SortedMap (Fin (((targetType {rec:0}) .args) .length)) (ArgExplicitness, Name)

Totality: total
Visibility: public export

givenParams : ({rec:0} : ExternalGenSignature) -> SortedMap (Fin (((targetType {rec:0}) .args) .length)) (ArgExplicitness, Name)

Totality: total
Visibility: public export

.givensOrder : ({rec:0} : ExternalGenSignature) -> Vect ((givenParams {rec:0}) .size) (Fin ((givenParams {rec:0}) .size))

Totality: total
Visibility: public export

givensOrder : ({rec:0} : ExternalGenSignature) -> Vect ((givenParams {rec:0}) .size) (Fin ((givenParams {rec:0}) .size))

Totality: total
Visibility: public export

.gendParamsCnt : ExternalGenSignature -> Nat

Totality: total
Visibility: public export

gendParamsCnt : ExternalGenSignature -> Nat

Totality: total
Visibility: public export

.gendOrder : ({rec:0} : ExternalGenSignature) -> Vect (gendParamsCnt {rec:0}) (Fin (gendParamsCnt {rec:0}))

Totality: total
Visibility: public export

gendOrder : ({rec:0} : ExternalGenSignature) -> Vect (gendParamsCnt {rec:0}) (Fin (gendParamsCnt {rec:0}))

Totality: total
Visibility: public export

characteristics : ExternalGenSignature -> (String, List Nat)

Totality: total
Visibility: export

callExternalGen : (sig : ExternalGenSignature) -> Name -> TTImp -> Vect ((sig .givenParams) .size) TTImp -> TTImp

Totality: total
Visibility: export

internalise : (extSig : ExternalGenSignature) -> Subset GenSignature (\sig => (sig .givenParams) .size = (extSig .givenParams) .size)

Totality: total
Visibility: export