Text.ILex.Derive

Reexports

Definitions

deriveParserState : Elaboration m => Name -> Name -> List Name -> (() `m`)

  Given names for the number of states (`size`), the
  parser state (`state`), and the distinct parser states,
  this will compute the actual number of states and define
  a constant for each state.
  
  For instance, `deriveParserState "SZ" "ST" ["SIni", "Str", "Err", "Done"]`
  will generate the following definitions:
  
  ```idris
  public export
  SZ : Bits32
  SZ = 4
  
  public export
  0 ST : Type
  ST = Index SZ
  
  export
  SIni : ST
  SIni = I 0
  
  export
  Str : ST
  Str = I 1
  
  export
  Err : ST
  Err = I 2
  
  export
  Done : ST
  Done = I 3
  
  export
  showST : ST -> String
  showST (I 0) = "SIni"
  showST (I 1) = "Str"
  showST (I 2) = "Err"
  showST (I 3) = "Done"
  showST _     = "impossible"
  ```

Totality: total
Visibility: export

HasPosition : List Name -> ParamTypeInfo -> Res (List TopLevel)

  Derives an implementation of `HasPosition` for a record type with the
  following fields:
  
  ```idris
  line_      : Ref q Nat
  col_       : Ref q Nat
  positions_ : Ref q Nat
  ```

Totality: total
Visibility: export

HasBytes : List Name -> ParamTypeInfo -> Res (List TopLevel)

  Derives an implementation of `HasBytes` for a record type with the
  following field:
  
  ```idris
  bytes_     : Ref q ByteString
  ```

Totality: total
Visibility: export

HasStringLits : List Name -> ParamTypeInfo -> Res (List TopLevel)

  Derives an implementation of `HasStringLits` for a record type with the
  following field:
  
  ```idris
  strings_     : Ref q (SnocList String)
  ```

Totality: total
Visibility: export

HasError : List Name -> ParamTypeInfo -> Res (List TopLevel)

  Derives an implementation of `HasError` for a record type with the
  following field:
  
  ```idris
  error_     : Ref q (Maybe $ BoundedErr e)
  ```
  
  The error type `e` can be freely chosen (it can also be a parameter) and
  will be determined when deriving the implementation.

Totality: total
Visibility: export

HasStack : List Name -> ParamTypeInfo -> Res (List TopLevel)

  Derives an implementation of `HasStack` for a record type with the
  following field:
  
  ```idris
  stack_     : Ref q a
  ```
  
  The stack type `a` can be freely chosen (it can also be a parameter) and
  will be determined when deriving the implementation.

Totality: total
Visibility: export

FullStack : List Name -> ParamTypeInfo -> Res (List TopLevel)

  Derives implementations of the following interfaces for a suitable
  record type: `HasPosition`, `HasBytes`, `HasStringLits`, `HasError`, and
  `HasStack`.

Totality: total
Visibility: export