------------------------------------------------------------------------
-- 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