NatLiteral.agda

module NatLiteral where

open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Unit

record Literal (A : Set) : Set₁ where
  field
    bounds    : ℕ → Set
    inBounds? : (n : ℕ) → Dec (bounds n)
    fromNat   : (n : ℕ) → {inBounds : True (inBounds? n)} → A
open Literal {{...}} public

instance
  NatLiteral : Literal ℕ
  bounds    {{NatLiteral}} _ = ⊤
  inBounds? {{NatLiteral}} _ = yes tt
  fromNat   {{NatLiteral}} n = n

open import Data.Fin as Fin using (Fin)
instance
  FinLiteral : ∀ n → Literal (Fin n)
  bounds    {{FinLiteral m}} n = n ℕ.< m
  inBounds? {{FinLiteral m}} n = suc n ℕ.≤? m
  fromNat   {{FinLiteral m}} n {inBounds} = Fin.#_ n {m} {inBounds}

open import Data.Bool as Bool using (Bool)
instance
  BoolLiteral : Literal Bool
  bounds    {{BoolLiteral}} n = n ℕ.≤  1
  inBounds? {{BoolLiteral}} n = n ℕ.≤? 1
  fromNat   {{BoolLiteral}} 0 = Bool.false
  fromNat   {{BoolLiteral}} 1 = Bool.true
  fromNat   {{BoolLiteral}} (suc (suc _)) {inBounds = ()}

open import Data.Integer as ℤ using (ℤ)
instance
  IntLiteral : Literal ℤ
  bounds    {{IntLiteral}} _ = ⊤
  inBounds? {{IntLiteral}} _ = yes tt
  fromNat   {{IntLiteral}} n = ℤ.+ n

open import Data.Rational as ℚ using (ℚ)
import Data.Nat.Coprimality as Coprimality

instance
  RationalLiteral : Literal ℚ
  bounds    {{RationalLiteral}} _ = ⊤
  inBounds? {{RationalLiteral}} _ = yes tt
  fromNat   {{RationalLiteral}} n =
    ℚ._÷_
      (ℤ.+ n)
      (suc zero)
      { coprime = fromCoprimeWitness (Coprimality.sym (Coprimality.1-coprimeTo n)) }
    where
    fromCoprimeWitness : ∀ {n m}
                       → Coprimality.Coprime n m
                       → True (Coprimality.coprime? n m)
    fromCoprimeWitness = fromWitness

{-# BUILTIN FROMNAT fromNat #-}