Text.Show.Value

Definitions

record VName : Type

  A name.

Totality: total
Visibility: public export
Constructor: 

MkName : String -> VName

Projection: 

.unName : VName -> String

Hints:

Cast (SnocList Char) VName

Eq VName

FromString VName

Interpolation VName

Monoid VName

Ord VName

Pretty VName

Semigroup VName

Show VName

.unName : VName -> String

Totality: total
Visibility: public export

unName : VName -> String

Totality: total
Visibility: public export

data Value : Type

  Generic Idris values.
  The `String` in the literals is the text for the literals "as is".
  
  A chain of infix constructors means that they appeared in the input string
  without parentheses, i.e
  
  `1 :+: 2 :*: 3` is represented with `InfixCons 1 [(":+:",2),(":*:",3)]`, whereas
  
  `1 :+: (2 :*: 3)` is represented with `InfixCons 1 [(":+:",InfixCons 2 [(":*:",3)])]`.

Totality: total
Visibility: public export
Constructors:

Con : VName -> List Value -> Value

InfixCons : Value -> List (VName, Value) -> Value

Rec : VName -> List (VName, Value) -> Value

Tuple : Value -> Value -> List Value -> Value

Lst : List Value -> Value

Neg : Value -> Value

Natural : String -> Value

Dbl : String -> Value

Chr : String -> Value

Str : String -> Value

Hints:

Eq Value

Show Value

binOp : VName -> Value -> Value -> Value

  Displays an applied binary operator.
  If the same operator appears several times in a row,
  this is treated as a list of infix constructors.

Totality: total
Visibility: public export

hideCon : Bool -> (VName -> Bool) -> Value -> Value

  Hide constructors matching the given predicate.
  If the hidden value is in a record, we also hide
  the corresponding record field.
  
  If the boolean flag is true, then we also hide
  constructors all of whose fields were hidden.

Totality: total
Visibility: export

data Token : Type

Totality: total
Visibility: public export
Constructors:

Lit : Value -> Token

Id : VName -> Token

Op : VName -> Token

Symbol : Char -> Token

EOI : Token

Hints:

Eq Token

Interpolation Token

Show Token

data Err : Type

Totality: total
Visibility: public export
Constructor: 

ExpectedId : Err

Hints:

Eq Err

Interpolation Err

Show Err

0 PSErr : Type

Totality: total
Visibility: public export

fromChar : Char -> Token

Totality: total
Visibility: public export

tokens : String -> Either (Bounded PSErr) (List (Bounded Token))

Totality: total
Visibility: export

parseValueE : String -> Either (ParseError Err) Value

Totality: total
Visibility: export

parseValue : String -> Maybe Value

Totality: total
Visibility: export