------------------------------------------------------------------------
-- The Agda standard library
--
-- Format strings for Printf and Scanf
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Text.Format where

open import Data.Maybe.Base
open import Text.Format.Generic

-- Formatted types
open import Data.Char.Base using (Char)
open import Data.Integer.Base using (ℤ)
open import Data.Float.Base using (Float)
open import Data.Nat.Base using (ℕ)
open import Data.String.Base using (String)

------------------------------------------------------------------------
-- Basic types

data ArgChunk : Set where
  ℕArg ℤArg FloatArg CharArg StringArg : ArgChunk

------------------------------------------------------------------------
-- Semantics

ArgType : (fmt : ArgChunk) → Set
ArgType ℕArg      = ℕ
ArgType ℤArg      = ℤ
ArgType FloatArg  = Float
ArgType CharArg   = Char
ArgType StringArg = String

lexArg : Char → Maybe ArgChunk
lexArg 'd' = just ℤArg
lexArg 'i' = just ℤArg
lexArg 'u' = just ℕArg
lexArg 'f' = just FloatArg
lexArg 'c' = just CharArg
lexArg 's' = just StringArg
lexArg _   = nothing

formatSpec : FormatSpec
formatSpec .FormatSpec.ArgChunk = ArgChunk
formatSpec .FormatSpec.ArgType  = ArgType
formatSpec .FormatSpec.lexArg   = lexArg

open Format formatSpec public

pattern `ℕ      = Arg ℕArg
pattern `ℤ      = Arg ℤArg
pattern `Float  = Arg FloatArg
pattern `Char   = Arg CharArg
pattern `String = Arg StringArg