Language.TOML.Processing

Definitions

data ValueTy : Type

Totality: total
Visibility: public export
Constructors:

TString : ValueTy

TInteger : ValueTy

TFloat : ValueTy

TBoolean : ValueTy

TEnum : List String -> ValueTy

TArray : ValueTy -> ValueTy

TTable : TableTy -> ValueTy

record FieldTy : Type

Totality: total
Visibility: public export
Constructor: 

MkFieldTy : String -> Bool -> ValueTy -> FieldTy

Projections:

.name : FieldTy -> String

.optional : FieldTy -> Bool

.ty : FieldTy -> ValueTy

.name : FieldTy -> String

Visibility: public export

name : FieldTy -> String

Visibility: public export

.optional : FieldTy -> Bool

Visibility: public export

optional : FieldTy -> Bool

Visibility: public export

.ty : FieldTy -> ValueTy

Visibility: public export

ty : FieldTy -> ValueTy

Visibility: public export

data TableTy : Type

Totality: total
Visibility: public export
Constructors:

Emp : TableTy

Ext : (ft : FieldTy) -> (FieldOf ft -> TableTy) -> TableTy

And : FieldTy -> TableTy -> TableTy

Visibility: public export
Fixity Declaration: infixr operator, level 2

ValueOf : ValueTy -> Type

Visibility: public export

FieldOf : FieldTy -> Type

Visibility: public export

data TableOf : TableTy -> Type

Totality: total
Visibility: public export
Constructors:

Nil : TableOf Emp

(::) : (x : FieldOf ft) -> TableOf (f x) -> TableOf (Ext ft f)

data ValueError : Type

Totality: total
Visibility: public export
Constructors:

ExpectedType : ValueTy -> ValueError

InsideArray : ValueError -> ValueError

InsideTable : TableError -> ValueError

BadEnumVal : String -> ValueError

data TableError : Type

Totality: total
Visibility: public export
Constructors:

FieldError : String -> ValueError -> TableError

ExpectedField : String -> TableError

UnexpectedFields : List String -> TableError

processTable : (ty : TableTy) -> Table -> Either TableError (TableOf ty)

Visibility: public export

processValue : (ty : ValueTy) -> Value -> Either ValueError (ValueOf ty)

Visibility: public export