Language.Reflection.Refined

The content of this module is based on the
tutorial post about [refined primitives](../../Doc/Primitives.md).

Reexports

Definitions

refinedEq : String -> TTImp -> Name -> Elab ()

  Creates an `Eq` implementation for the given datatype
  by using the given accessor function.
  
  This is hardly useful on its own but convenient when
  combined with other interface implementors.
  
  In some occasions it is useful to have one or several
  phantom types for the refined type. Therefore, the exact
  type should be given as a `TTImp`.
  
  ```idris example
  record AtomicNr a where
    constructor MkAtomicNr
    value : Int
    0 inBounds : So (1 <= value && value <= 118)
  
  %runElab refinedEq "AtomicNr" `(AtomicNr a) `{{value}}
  ```

Totality: total
Visibility: export

refinedOrd : String -> TTImp -> Name -> Elab ()

  Creates an `Ord` implementation for the given datatype
  by using the given accessor function.
  
  This is hardly useful on its own but convenient when
  combined with other interface implementors.
  
  ```idris example
  record AtomicNr a where
    constructor MkAtomicNr
    value : Int
    0 inBounds : So (1 <= value && value <= 118)
  
  %runElab refinedOrd "AtomicNr" `(AtomicNr a) `{{value}}
  ```

Totality: total
Visibility: export

refinedShow : String -> TTImp -> Name -> Elab ()

  Creates a `Show` implementation for the given datatype
  by using the given accessor function.
  
  This is hardly useful on its own but convenient when
  combined with other interface implementors.
  
  ```idris example
  record AtomicNr a where
    constructor MkAtomicNr
    value : Int
    0 inBounds : So (1 <= value && value <= 118)
  
  %runElab refinedShow "AtomicNr" `(AtomicNr a) `{{value}}
  ```

Totality: total
Visibility: export

refinedEqOrdShow : String -> TTImp -> Name -> Elab ()

  Convenience function combining `refinedEq`, `refinedOrd`,
  and `refinedShow`.

Totality: total
Visibility: export

refinedIntegral : String -> TTImp -> Name -> Name -> TTImp -> Elab ()

  This creates `Eq`, `Ord`, and `Show` implementations as
  well as conversion functions for a refined integral number.
  
  Conversion functions are called `refine` and `fromInteger`
  and are put in their own namespace, named after the
  data type's name.
  
  ```idris example
  record AtomicNr a where
    constructor MkAtomicNr
    value : Int
    0 inBounds : So (1 <= value && value <= 118)
  
  %runElab refinedIntegral "AtomicNr"
                           `(AtomicNr a)
                           `{{MkAtomicNr}}
                           `{{value}}
                           `(Int)
  ```
  
  The above will result in the following declarations being generated:
  
  ```idris example
  Eq AtomicNr where
    (==) = (==) `on` value
  
  Ord AtomicNr where
    compare = compare `on` value
  
  Show AtomicNr where
    showPrec p = showPrec p . value
  
  namespace AtomicNr
    refine : Int -> Maybe AtomicNr
    refine = refineSo MkAtomicNr
  
    fromInteger :
         (v : Integer)
      -> {auto 0 _: IsJust (refine $ fromInteger v)}
      -> AtomicNr
    fromInteger v = fromJust (refine $ fromInteger v)
  ```

Totality: total
Visibility: export

refinedIntegralDflt : String -> TTImp -> Elab ()

Totality: total
Visibility: export

refinedInt : String -> Elab ()

  Specialized version of `refinedIntegral` for data types,
  which adhere to the following conventions:
  
   * If a data type's name is `Foo` its constructor is named `MkFoo`.
   * The field accessor of the wrapped Int is named `value`.
   * The proof of validity consists of a single zero quantity `So`.
  
  ```idris example
  record AtomicNr where
    constructor MkAtomicNr
    value : Int
    0 inBounds : So (1 <= value && value <= 118)
  
  %runElab refinedInt "AtomicNr"
  ```

Totality: total
Visibility: export

refinedBits8 : String -> Elab ()

  Specialized version of `refinedIntegral` for data types,
  which adhere to the following conventions:
  
   * If a data type's name is `Foo` its constructor is named `MkFoo`.
   * The field accessor of the wrapped Int is named `value`.
   * The proof of validity consists of a single zero quantity `So`.

Totality: total
Visibility: export

refinedBits16 : String -> Elab ()

  Specialized version of `refinedIntegral` for data types,
  which adhere to the following conventions:
  
   * If a data type's name is `Foo` its constructor is named `MkFoo`.
   * The field accessor of the wrapped Int is named `value`.
   * The proof of validity consists of a single zero quantity `So`.

Totality: total
Visibility: export

refinedBits32 : String -> Elab ()

  Specialized version of `refinedIntegral` for data types,
  which adhere to the following conventions:
  
   * If a data type's name is `Foo` its constructor is named `MkFoo`.
   * The field accessor of the wrapped Int is named `value`.
   * The proof of validity consists of a single zero quantity `So`.

Totality: total
Visibility: export

refinedBits64 : String -> Elab ()

  Specialized version of `refinedIntegral` for data types,
  which adhere to the following conventions:
  
   * If a data type's name is `Foo` its constructor is named `MkFoo`.
   * The field accessor of the wrapped Int is named `value`.
   * The proof of validity consists of a single zero quantity `So`.

Totality: total
Visibility: export

refinedInt8 : String -> Elab ()

  Specialized version of `refinedIntegral` for data types,
  which adhere to the following conventions:
  
   * If a data type's name is `Foo` its constructor is named `MkFoo`.
   * The field accessor of the wrapped Int is named `value`.
   * The proof of validity consists of a single zero quantity `So`.

Totality: total
Visibility: export

refinedInt16 : String -> Elab ()

  Specialized version of `refinedIntegral` for data types,
  which adhere to the following conventions:
  
   * If a data type's name is `Foo` its constructor is named `MkFoo`.
   * The field accessor of the wrapped Int is named `value`.
   * The proof of validity consists of a single zero quantity `So`.

Totality: total
Visibility: export

refinedInt32 : String -> Elab ()

  Specialized version of `refinedIntegral` for data types,
  which adhere to the following conventions:
  
   * If a data type's name is `Foo` its constructor is named `MkFoo`.
   * The field accessor of the wrapped Int is named `value`.
   * The proof of validity consists of a single zero quantity `So`.

Totality: total
Visibility: export

refinedInt64 : String -> Elab ()

  Specialized version of `refinedIntegral` for data types,
  which adhere to the following conventions:
  
   * If a data type's name is `Foo` its constructor is named `MkFoo`.
   * The field accessor of the wrapped Int is named `value`.
   * The proof of validity consists of a single zero quantity `So`.

Totality: total
Visibility: export

refinedFloating : String -> TTImp -> Name -> Name -> Elab ()

  This creates `Eq`, `Ord`, and `Show` implementations as
  well as conversion functions for a refined floating point
  number.
  
  Conversion functions are called `refine` and `fromDouble`
  and are put in their own namespace, named after the
  data type's name.
  
  ```idris example
  record Abundance a where
    constructor MkAbundance
    value : Double
    0 inBounds : So (0 < value && value <= 1)
  
  %runElab refinedFloating "Abundance" `(Abundance a) `{{MkAbundance}} `{{value}}
  ```
  
  The above will result in the following declarations being generated:
  
  ```idris example
  Eq Abundance where
    (==) = (==) `on` value
  
  Ord Abundance where
    compare = compare `on` value
  
  Show Abundance where
    showPrec p = showPrec p . value
  
  namespace Abundance
    refine : Double -> Maybe Abundance
    refine = refineSo MkAbundance
  
    fromDouble :  (v : Double)
               -> {auto 0 _: IsJust (refine v)}
               -> Abundance
    fromDouble v = fromJust (refine v)
  ```

Totality: total
Visibility: export

refinedDouble : String -> Elab ()

  Convenience version of `refinedFloating` for data types,
  which adhere to the following conventions:
  
   * If a data type's name is `Foo` its constructor is named `MkFoo`.
   * The field accessor of the wrapped Int is named `value`.
   * The proof of validity consists of a single zero quantity `So`.

Totality: total
Visibility: export

refinedText : String -> TTImp -> Name -> Name -> Elab ()

  This creates `Eq`, `Ord`, and `Show` implementations as
  well as conversion functions for a refined string value.
  
  Conversion functions are called `refine` and `fromString`
  and are put in their own namespace, named after the
  data type's name.
  
  ```idris example
  record Html a where
    constructor MkHtml
    value : String
    0 inBounds : So (isValidHtml value)
  
  %runElab refinedText "Html" `(Html a) `{{MkHtml}} `{{value}}
  ```
  
  The above will result in the following declarations being generated:
  
  ```idris example
  Eq Html where
    (==) = (==) `on` value
  
  Ord Html where
    compare = compare `on` value
  
  Show Html where
    showPrec p = showPrec p . value
  
  namespace Html
    refine : String -> Maybe Html
    refine = refineSo MkHtml
  
    fromString :  (v : String)
               -> {auto 0 _: IsJust (refine v)}
               -> Html
    fromString v = fromJust (refine v)
  ```

Totality: total
Visibility: export

refinedString : String -> Elab ()

  Convenience version of `refinedText` for data types,
  which adhere to the following conventions:
  
   * If a data type's name is `Foo` its constructor is named `MkFoo`.
   * The field accessor of the wrapped Int is named `value`.
   * The proof of validity consists of a single zero quantity `So`.

Totality: total
Visibility: export

refinedCharacter : String -> TTImp -> Name -> Name -> Elab ()

  This creates `Eq`, `Ord`, and `Show` implementations as
  well as conversion functions for a refined charater.
  
  Conversion functions are called `refine` and `fromChar`
  and are put in their own namespace, named after the
  data type's name.
  
  ```idris example
  record Digit a where
    constructor MkDigit
    value : Char
    0 inBounds : So (isDigit value)
  
  %runElab refinedText "Digit" `(Digit a) `{{MkDigit}} `{{value}}
  ```
  
  The above will result in the following declarations being generated:
  
  ```idris example
  Eq Digit where
    (==) = (==) `on` value
  
  Ord Digit where
    compare = compare `on` value
  
  Show Digit where
    showPrec p = showPrec p . value
  
  namespace Digit
    refine : Char -> Maybe Digit
    refine = refineSo MkDigit
  
    fromChar :  (v : Char)
             -> {auto 0 _: IsJust (refine v)}
             -> Digit
    fromChar v = fromJust (refine v)
  ```

Totality: total
Visibility: export

refinedChar : String -> Elab ()

  Convenience version of `refinedCharacter` for data types,
  which adhere to the following conventions:
  
   * If a data type's name is `Foo` its constructor is named `MkFoo`.
   * The field accessor of the wrapped Char is named `value`.
   * The proof of validity consists of a single zero quantity `So`.

Totality: total
Visibility: export