Martin Escardo 12th September 2024

This file provides an interface to implement automatic converscxion of
decimal literals to types other than just the natural numbers.

See https://agda.readthedocs.io/en/latest/language/literal-overloading.html

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Notation.Decimal where

open import MLTT.Universes
open import MLTT.NaturalNumbers

record Decimal {𝓀 π“₯ : Universe} (A : 𝓀 Μ‡ ) : 𝓀 βŠ” π“₯ ⁺ Μ‡ where
  field
    constraint : β„• β†’ π“₯ Μ‡
    fromβ„• : (n : β„•) {{_ : constraint n}} β†’ A

open Decimal {{...}} public using (fromβ„•)

{-# BUILTIN FROMNAT fromβ„• #-}
{-# DISPLAY Decimal.fromβ„• _ n = fromβ„• n #-}

record Negative {𝓀 π“₯ : Universe} (A : 𝓀 Μ‡ ) : 𝓀 βŠ” π“₯ ⁺ Μ‡ where
  field
    constraint : β„• β†’ π“₯ Μ‡
    fromNeg : (n : β„•) {{_ : constraint n}} β†’ A

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

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

data No-Constraint : 𝓀₀ Μ‡ where
 no-constraint : No-Constraint

instance
 really-no-constraint : No-Constraint
 really-no-constraint = no-constraint

make-decimal-with-no-constraint
 : {A : 𝓀 Μ‡ }
 β†’ ((n : β„•)  {{_ : No-Constraint}} β†’ A)
 β†’ Decimal A
make-decimal-with-no-constraint f =
 record {
   constraint = Ξ» _ β†’ No-Constraint
 ; fromβ„• = f
 }

make-negative-with-no-constraint
 : {A : 𝓀 Μ‡ }
 β†’ ((n : β„•)  {{_ : No-Constraint}} β†’ A)
 β†’ Negative A
make-negative-with-no-constraint f =
 record {
   constraint = Ξ» _ β†’ No-Constraint
 ; fromNeg = f
 }

\end{code}

The natural place for this would be MLTT.NaturalNumbers, but then we
would get a circular dependency.

\begin{code}

instance
 Decimal-β„•-to-β„• : Decimal β„•
 Decimal-β„•-to-β„• = make-decimal-with-no-constraint (Ξ» n β†’ n)

\end{code}