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

open import Text.Parser.Types.Core using (Parameters)

module Text.Parser.Combinators.Numbers {l} {P : Parameters l} where

open import Data.Char.Base using (Char)
open import Data.Float.Base as Float using (Float; fromℕ; fromℤ)
open import Data.Integer.Base using (; -_; +_; _◃_)
open import Data.List.Base as List using ([]; _∷_)
open import Data.List.NonEmpty as List⁺ using (List⁺)
open import Data.List.Sized.Interface
open import Data.Maybe.Base using (Maybe; fromMaybe; maybe′)
open import Data.Nat.Base as  using (; _+_; _*_)
import Data.Nat.GeneralisedArithmetic
open import Data.Product as Product using (_×_; _,_; uncurry)
open import Data.Sign.Base using (Sign)
open import Data.Sum.Base using ([_,_]′)

open import Function.Base using (const; id; _$_; _∘′_; case_of_)
open import Category.Monad using (RawMonadPlus)

open import Relation.Unary
open import Relation.Binary.PropositionalEquality.Decidable using (DecidableEquality)
open import Data.Subset using (Subset; into)

open import Level.Bounded using (theSet; [_])
open import Text.Parser.Types P
open import Text.Parser.Combinators {P = P}
open Parameters P

module _ {{𝕄 : RawMonadPlus M}}
         {{𝕊 : Sized Tok Toks}}
         {{𝔻 : DecidableEquality (theSet Tok)}}
         {{ : Subset Char (theSet Tok)}} where

 private module  = Subset 

 decimalDigit : ∀[ Parser [  ] ]
 decimalDigit = alts $ List.map (uncurry $ λ v c  v <$ exact (ℂ.into c))
              $ (0 , '0')  (1 , '1')  (2 , '2')  (3 , '3')  (4 , '4')
               (5 , '5')  (6 , '6')  (7 , '7')  (8 , '8')  (9 , '9')  []

 hexadecimalDigit : ∀[ Parser [  ] ]
 hexadecimalDigit = decimalDigit <|> alts hex where
   hex = List.map (uncurry $ λ v c  v <$ exact (ℂ.into c))
       $ (10 , 'a')  (11 , 'b')  (12 , 'c')
        (13 , 'd')  (14 , 'e')  (15 , 'f')  []

 private
   natFromDigits : List⁺   
   natFromDigits = List⁺.foldl  ih v  ih * 10 + v) id

 sign : ∀[ Parser [ Sign ] ]
 sign = Sign.- <$ anyOf (List.map ℂ.into $ '-'  '−'  [])
    <|> Sign.+ <$ exact (ℂ.into '+')

 decimalℕ : ∀[ Parser [  ] ]
 decimalℕ = natFromDigits  <$> list⁺ decimalDigit

 decimalℤ : ∀[ Parser [  ] ]
 decimalℤ = uncurry convert <$> (sign <?&> decimalℕ) where
   convert : Maybe Sign    
   convert ms n = fromMaybe Sign.+ ms  n

 decimalFloat : ∀[ Parser [ Float ] ]
 decimalFloat = convert <$> rawDouble where

   fractional : ∀[ Parser [ List⁺  ] ]
   fractional = exact (ℂ.into '.') &> box (list⁺ decimalDigit)

   fromFractional : List⁺   Float
   fromFractional ds = fromℕ (natFromDigits ds)
               Float.÷ fromℕ (10 ℕ.^ List⁺.length ds)

   eNotation : ∀[ Parser [ Maybe Sign ×  ] ]
   eNotation = anyOf (ℂ.into 'E'  ℂ.into 'e'  [])
             &> box (sign <?&> decimalℕ)

   fromENotation : Maybe Sign ×   Float  Float
   fromENotation (ms , e) f = case fromMaybe Sign.+ ms of λ where
     Sign.-  f Float.÷ fromℕ (10 ℕ.^ e)
     Sign.+  f Float.* fromℕ (10 ℕ.^ e)

   rawDouble : ∀[ Parser [ ( × Maybe (List⁺ )) × Maybe (Maybe Sign × ) ] ]
   rawDouble = (decimalℤ <&?> box fractional) <&?> box eNotation

   convert : ( × Maybe (List⁺ )) × Maybe (Maybe Sign × )  Float
   convert ((int , mfrac) , menot)
     = maybe′ fromENotation id menot
     $ maybe′  m f  f Float.+ fromFractional m) id mfrac
     $ fromℤ int