module Prim.Literals where

Primitive: Overloaded literalsπŸ”—

We define the records Number, Negative and String to allow overloading of the numeric literals.

record Number {a} (A : Type a) : Type (lsuc a) where
  field
    Constraint : Nat β†’ Type a
    fromNat : βˆ€ n β†’ {{_ : Constraint n}} β†’ A

open Number {{...}} public using (fromNat)

record Negative {a} (A : Type a) : Type (lsuc a) where
  field
    Constraint : Nat β†’ Type a
    fromNeg : βˆ€ n β†’ {{_ : Constraint n}} β†’ A

open Negative {{...}} public using (fromNeg)

{-# BUILTIN FROMNAT fromNat #-}
{-# DISPLAY Number.fromNat _ n = fromNat n #-}
{-# BUILTIN FROMNEG fromNeg #-}
{-# DISPLAY Negative.fromNeg _ n = fromNeg n #-}

postulate String : Type
{-# BUILTIN STRING String #-}

record IsString {a} (A : Type a) : Type (lsuc a) where
  field
    Constraint : String β†’ Type a
    fromString : (s : String) {{_ : Constraint s}} β†’ A

open IsString {{...}} public using (fromString)

{-# BUILTIN FROMSTRING fromString #-}
{-# DISPLAY Number.fromNat _ n = fromNat n #-}
{-# DISPLAY IsString.fromString _ s = fromString s #-}
{-# DISPLAY Negative.fromNeg _ n = fromNeg n #-}

instance
  Number-Nat : Number Nat
  Number-Nat .Number.Constraint _ = ⊀
  Number-Nat .Number.fromNat n = n

  IsString-String : IsString String
  IsString-String .IsString.Constraint _ = ⊀
  IsString-String .IsString.fromString s = s