0 | module Text.ILex.Util
  1 |
  2 | import Data.ByteString
  3 | import Data.Linear.Ref1
  4 | import Derive.Prelude
  5 | import Syntax.T1
  6 | import Text.Bounds
  7 | import Text.ParseError
  8 | import Text.ILex.Parser
  9 | import Text.ILex.RExp
 10 |
 11 | %default total
 12 |
 13 | --------------------------------------------------------------------------------
 14 | -- Reading Numbers
 15 | --------------------------------------------------------------------------------
 16 |
 17 | export %inline
 18 | decimaldigit : Bits8 -> Integer
 19 | decimaldigit x = cast x - 48
 20 |
 21 | export
 22 | hexdigit : Bits8 -> Integer
 23 | hexdigit x =
 24 |   if      x <= byte_9 then cast x - cast byte_0
 25 |   else if x <= byte_F then 10 + cast x - cast byte_A
 26 |   else                     10 + cast x - cast byte_a
 27 |
 28 | parameters (bv : ByteVect n)
 29 |   export
 30 |   binaryBV : Integer -> (k : Nat) -> (x : Ix k n) => Integer
 31 |   binaryBV res 0     = res
 32 |   binaryBV res (S k) =
 33 |       case ix bv k of
 34 |         48 => binaryBV (res * 2) k
 35 |         _  => binaryBV (res * 2 + 1) k
 36 |
 37 |   export
 38 |   binarySepBV : Integer -> (k : Nat) -> (x : Ix k n) => Integer
 39 |   binarySepBV res 0     = res
 40 |   binarySepBV res (S k) =
 41 |       case ix bv k of
 42 |         48 => binarySepBV (res * 2) k
 43 |         49 => binarySepBV (res * 2 + 1) k
 44 |         _  => binarySepBV res k
 45 |
 46 |   export
 47 |   octalBV : Integer -> (k : Nat) -> (x : Ix k n) => Integer
 48 |   octalBV res 0     = res
 49 |   octalBV res (S k) = octalBV (res * 8 + decimaldigit (ix bv k)) k
 50 |
 51 |   export
 52 |   octalSepBV : Bits8 -> Integer -> (k : Nat) -> (x : Ix k n) => Integer
 53 |   octalSepBV sep res 0     = res
 54 |   octalSepBV sep res (S k) =
 55 |      let b := ix bv k
 56 |       in case prim__eq_Bits8 sep b of
 57 |            0 => octalSepBV sep (res * 8 + decimaldigit b) k
 58 |            _ => octalSepBV sep res k
 59 |
 60 |   export
 61 |   decimalBV : Integer -> (k : Nat) -> (x : Ix k n) => Integer
 62 |   decimalBV res 0     = res
 63 |   decimalBV res (S k) = decimalBV (res * 10 + decimaldigit (ix bv k)) k
 64 |
 65 |   export
 66 |   decimalSepBV : Bits8 -> Integer -> (k : Nat) -> (x : Ix k n) => Integer
 67 |   decimalSepBV sep res 0     = res
 68 |   decimalSepBV sep res (S k) =
 69 |      let b := ix bv k
 70 |       in case prim__eq_Bits8 sep b of
 71 |            0 => decimalSepBV sep (res * 10 + decimaldigit b) k
 72 |            _ => decimalSepBV sep res k
 73 |
 74 |   export
 75 |   hexadecimalBV : Integer -> (k : Nat) -> (x : Ix k n) => Integer
 76 |   hexadecimalBV res 0     = res
 77 |   hexadecimalBV res (S k) = hexadecimalBV (res * 16 + hexdigit (ix bv k)) k
 78 |
 79 |   export
 80 |   hexadecimalSepBV : Bits8 -> Integer -> (k : Nat) -> (x : Ix k n) => Integer
 81 |   hexadecimalSepBV sep res 0     = res
 82 |   hexadecimalSepBV sep res (S k) =
 83 |      let b := ix bv k
 84 |       in case prim__eq_Bits8 sep b of
 85 |            0 => hexadecimalSepBV sep (res * 16 + hexdigit b) k
 86 |            _ => hexadecimalSepBV sep res k
 87 |
 88 |   export
 89 |   integerBV : (k : Nat) -> (x : Ix k n) => Integer
 90 |   integerBV 0     = 0
 91 |   integerBV (S k) =
 92 |     case ix bv k of
 93 |       45 => negate $ decimalBV 0 k       -- '-'
 94 |       43 => decimalBV 0 k                -- '+'
 95 |       b  => decimalBV (decimaldigit b) k
 96 |
 97 | ||| Converts a string of binary digits to an integer
 98 | export %inline
 99 | binary : ByteString -> Integer
100 | binary (BS n bv) = binaryBV bv 0 n
101 |
102 | ||| Converts a string of binary digits containing optional
103 | ||| separators to an integer `0010_0011_1110_0011.
104 | |||
105 | ||| Such integer literals are supported by Idris as well as TOML,
106 | ||| for instance:
107 | export %inline
108 | binarySep : ByteString -> Integer
109 | binarySep (BS n bv) = binarySepBV bv 0 n
110 |
111 | ||| Converts a string of octal digits to an integer
112 | export %inline
113 | octal : ByteString -> Integer
114 | octal (BS n bv) = octalBV bv 0 n
115 |
116 | ||| Converts a string of octal digits containing optional
117 | ||| separators to an integer `077_334`.
118 | |||
119 | ||| Such integer literals are supported by Idris as well as TOML,
120 | ||| for instance:
121 | export %inline
122 | octalSep : Bits8 -> ByteString -> Integer
123 | octalSep sep (BS n bv) = octalSepBV bv sep 0 n
124 |
125 | ||| Converts a string of decimal digits to an integer
126 | export %inline
127 | decimal : ByteString -> Integer
128 | decimal (BS n bv) = decimalBV bv 0 n
129 |
130 | ||| Converts a string of decimal digits containing optional
131 | ||| separators to an integer `177_934`.
132 | |||
133 | ||| Such integer literals are supported by Idris as well as TOML,
134 | ||| for instance:
135 | export %inline
136 | decimalSep : Bits8 -> ByteString -> Integer
137 | decimalSep sep (BS n bv) = decimalSepBV bv sep 0 n
138 |
139 | ||| Converts a string of decimal digits to an integer
140 | export %inline
141 | hexadecimal : ByteString -> Integer
142 | hexadecimal (BS n bv) = hexadecimalBV bv 0 n
143 |
144 | ||| Converts a string of decimal digits containing optional
145 | ||| separators to an integer `177_934`.
146 | |||
147 | ||| Such integer literals are supported by Idris as well as TOML,
148 | ||| for instance:
149 | export %inline
150 | hexadecimalSep : Bits8 -> ByteString -> Integer
151 | hexadecimalSep sep (BS n bv) = hexadecimalSepBV bv sep 0 n
152 |
153 | ||| Converts an integer literal with optional sign prefix
154 | ||| to an integer.
155 | export %inline
156 | integer : ByteString -> Integer
157 | integer (BS n bv) = integerBV bv n
158 |
159 | --------------------------------------------------------------------------------
160 | -- Operator Precedence
161 | --------------------------------------------------------------------------------
162 |
163 | ||| Utility for combining a snoc-list of expressions combined
164 | ||| via left-binding operators of different fixity into a single
165 | ||| expression.
166 | export
167 | mergeL : Ord o => (o -> e -> e -> e) -> SnocList (e,o) -> e -> e
168 | mergeL merge sp y =
169 |   case sp <>> [] of
170 |     []        => y
171 |     (x,ox)::t => go [<] x ox t y
172 |
173 |   where
174 |     app : SnocList (e,o) -> e -> o -> List (e,o) -> e -> e
175 |
176 |     go : SnocList (e,o) -> e -> o -> List (e,o) -> e -> e
177 |     go sx x ox []        z =
178 |       case sx of
179 |         [<]        => merge ox x z
180 |         sp:<(w,ow) => go sp w ow [] (merge ox x z)
181 |
182 |     go sx x ox ((y,oy) :: xs) z =
183 |       case compare ox oy of
184 |         LT => go (sx:<(x,ox)) y oy xs z
185 |         EQ => go sx (merge ox x y) oy xs z
186 |         GT => app sx (merge ox x y) oy xs z
187 |
188 |     app [<]                x ox xs z = go [<] x ox xs z
189 |     app outer@(sp:<(w,ow)) x ox xs z =
190 |       case compare ow ox of
191 |         LT => go outer x ox xs z
192 |         _  => app sp (merge ow w x) ox xs z
193 |
194 | ||| Utility for converting a snoc list into a list.
195 | |||
196 | ||| This is useful when streaming chunks of data and emitting
197 | ||| all the accumulated values of a single chunk.
198 | export
199 | maybeList : SnocList a -> Maybe (List a)
200 | maybeList [<] = Nothing
201 | maybeList sx  = Just (sx <>> [])
202 |
203 | ||| Concatenates the strings accumulated in a snoc list.
204 | |||
205 | ||| This is a utility often used when lexing or parsing
206 | ||| string literals that support various kinds of escape
207 | ||| sequences.
208 | export
209 | snocPack : SnocList String -> String
210 | snocPack [<]  = ""
211 | snocPack [<s] = s
212 | snocPack ss   = fastConcat $ ss <>> []
213 |