0 | module Text.WebIDL.Types.Numbers
  1 |
  2 | import Derive.Prelude
  3 |
  4 | %default total
  5 |
  6 | %language ElabReflection
  7 |
  8 | --------------------------------------------------------------------------------
  9 | --          IntLit
 10 | --------------------------------------------------------------------------------
 11 |
 12 | hexDigit : Integer -> Char
 13 | hexDigit n = if n < 10 then chr (48 + cast n) else chr (97 + cast (n - 10))
 14 |
 15 | digs :
 16 |      (base : Integer)
 17 |   -> {auto 0 _ : (base > 0) === True}
 18 |   -> List Char
 19 |   -> Integer
 20 |   -> String
 21 | digs b cs 0 = pack cs
 22 | digs b cs n = digs b (hexDigit (mod n b) :: cs) (assert_smaller n $ div n b)
 23 |
 24 | ||| An integer literal in hexadecimal, octal, or decimal representation.
 25 | ||| The code generator will use the same representation when
 26 | ||| generating code for constants and default values.
 27 | public export
 28 | data IntLit = Hex Nat | Oct Nat | I Integer
 29 |
 30 | %runElab derive "IntLit" [Show, Eq]
 31 |
 32 | export
 33 | Interpolation IntLit where
 34 |   interpolate (Hex 0) = "0x0"
 35 |   interpolate (Hex k) = "0x\{digs 16 [] $ cast k}"
 36 |   interpolate (Oct 0) = "0"
 37 |   interpolate (Oct k) = "0\{digs 8 [] $ cast k}" 
 38 |   interpolate (I i)   = show i
 39 |
 40 | --------------------------------------------------------------------------------
 41 | --          Floating Point Literals
 42 | --------------------------------------------------------------------------------
 43 |
 44 | ||| The sign of a floating point literal.
 45 | public export
 46 | data Signum = Plus | Minus
 47 |
 48 | %runElab derive "Signum" [Eq,Show]
 49 |
 50 | ||| A parsed floating point literal.
 51 | |||
 52 | ||| A floating point literal is either one of three
 53 | ||| special values (`NaN`, `Infinity`, or `-Infinity`)
 54 | ||| or a decimal floating point number (`NoExp`: dot is
 55 | ||| mandatory), or a float in scientific notation (`Exp`:
 56 | ||| dot is optional).
 57 | |||
 58 | ||| The main focus of this data type is one of
 59 | ||| preserving information. Encoding a `FloatLit` should
 60 | ||| yield (almost) exactly the same literal as the one
 61 | ||| encountered during parsin with two minor exceptions:
 62 | ||| a) The encoded literal will always use a lowercase 'e' as
 63 | ||| the delimiter for the exponent and b) in case of a
 64 | ||| positive exponent, there will not be a '+' in the
 65 | ||| encoded literal.
 66 | public export
 67 | data FloatLit : Type where
 68 |   ||| Floating point number in scientific notation.
 69 |   |||
 70 |   ||| Example: `-12.10e10`
 71 |   Exp :  (beforeDot : Integer)
 72 |       -> (afterDot  : Maybe Nat)
 73 |       -> (exp       : Integer)
 74 |       -> FloatLit
 75 |
 76 |   ||| Floating point number without exponent.
 77 |   |||
 78 |   ||| Example: `-12.1002`
 79 |   NoExp :  (beforeDot : Integer)
 80 |         -> (afterDot  : Nat)
 81 |         -> FloatLit
 82 |
 83 |   ||| Corresponds to the WebIDL keyword `Infinity`
 84 |   Infinity         : FloatLit
 85 |
 86 |   ||| Corresponds to the WebIDL keyword `-Infinity`
 87 |   NegativeInfinity : FloatLit
 88 |
 89 |   ||| Corresponds to the WebIDL keyword `NaN`
 90 |   NaN              : FloatLit
 91 |
 92 | %runElab derive "FloatLit" [Show,Eq]
 93 |
 94 | export
 95 | Interpolation FloatLit where
 96 |   interpolate (Exp bd (Just ad) ex) = "\{show bd}.\{show ad}e\{show ex}"
 97 |   interpolate (Exp bd Nothing ex)   = "\{show bd}e\{show ex}"
 98 |   interpolate (NoExp bd ad)         = "\{show bd}.\{show ad}"
 99 |   interpolate Infinity              = "Infinity"
100 |   interpolate NegativeInfinity      = "-Infinity"
101 |   interpolate NaN                   = "NaN"
102 |