0 | module Text.Molfile.Parser.KeyVal
  1 |
  2 | import Derive.Prelude
  3 | import Syntax.T1
  4 | import Text.ILex
  5 | import Text.ILex.Derive
  6 | import Text.Molfile.Parser.Util
  7 | import Text.Molfile.Types
  8 |
  9 | %default total
 10 | %language ElabReflection
 11 |
 12 | public export
 13 | data KV : Nat -> Type where
 14 |   S : String  -> KV n
 15 |   I : Integer -> KV n
 16 |   L : List (KV 0) -> KV (S n)
 17 |   P : String -> KV 1 -> KV 2
 18 |
 19 | %runElab deriveIndexed "KV" [Show]
 20 |
 21 | w1 : KV n -> KV 2
 22 | w1 (S s)   = S s
 23 | w1 (I i)   = I i
 24 | w1 (L xs)  = L xs
 25 | w1 (P s x) = P s x
 26 |
 27 | w0 : KV 0 -> KV 1
 28 | w0 (S s) = S s
 29 | w0 (I i) = I i
 30 |
 31 | public export
 32 | 0 KeyVal : Type
 33 | KeyVal = KV 2
 34 |
 35 | export
 36 | toString : KV n -> Maybe String
 37 | toString (S s) = Just s
 38 | toString _     = Nothing
 39 |
 40 | export
 41 | toNat : KV n -> Maybe Nat
 42 | toNat (I i) = if i >= 0 then Just (cast i) else Nothing
 43 | toNat _     = Nothing
 44 |
 45 | export
 46 | toNats : KV n -> Maybe (List Nat)
 47 | toNats (L xs) = traverse toNat xs
 48 | toNats _      = Nothing
 49 |
 50 | export
 51 | lookupVal : String -> List KeyVal -> Maybe (KV 1)
 52 | lookupVal s []            = Nothing
 53 | lookupVal s (P k v :: xs) = if s == k then Just v else lookupVal s xs
 54 | lookupVal s (_     :: xs) = lookupVal s xs
 55 |
 56 | --------------------------------------------------------------------------------
 57 | --          Parser State
 58 | --------------------------------------------------------------------------------
 59 |
 60 | %runElab deriveParserState "KSz" "KST"
 61 |   ["KIni","Entry","KVal","InStr","LStart","LVal","LEnd","KErr","KDone"]
 62 |
 63 | data Part : Type where
 64 |   VS : SnocList KeyVal -> Part
 65 |   VK : SnocList KeyVal -> String -> Part
 66 |   VO : SnocList KeyVal -> Nat -> SnocList (KV 0) -> Part
 67 |   VL : SnocList KeyVal -> String -> Nat -> SnocList (KV 0) -> Part
 68 |
 69 | public export
 70 | 0 SK : Type -> Type
 71 | SK = Stack MolErr Part KSz
 72 |
 73 | --------------------------------------------------------------------------------
 74 | -- Transformations
 75 | --------------------------------------------------------------------------------
 76 |
 77 | parameters {auto sk : SK q}
 78 |   part : KV 0 -> Part -> F1 q KST
 79 |   part p (VS sx)      = putStackAs (VS $ sx:<w1 p) Entry
 80 |   part p (VK sx s)    = putStackAs (VS $ sx:<P s (w0 p)) Entry
 81 |   part p (VO sx k sp) =
 82 |     case pred k of
 83 |       0 => putStackAs (VS $ sx:<(L $ sp<>>[p])) LEnd
 84 |       x => putStackAs (VO sx x (sp:<p)) LVal
 85 |   part p (VL sx s k sp) =
 86 |     case pred k of
 87 |       0 => putStackAs (VS $ sx:<P s (L $ sp<>>[p])) LEnd
 88 |       x => putStackAs (VL sx s x (sp:<p)) LVal
 89 |
 90 |   key : String -> Part -> F1 q KST
 91 |   key s (VS sx) = putStackAs (VK sx s) KVal
 92 |   key s _       = pure KErr -- impossible
 93 |
 94 |   %inline
 95 |   onPrim : KV 0 -> F1 q KST
 96 |   onPrim v = getStack >>= part v
 97 |
 98 |   %inline
 99 |   onKey : ByteString -> F1 q KST
100 |   onKey v = getStack >>= key (toUpper $ toString $ dropEnd 1 v)
101 |
102 |   startList : ByteString -> F1 q KST
103 |   startList bs =
104 |    let n := cast {to = Nat} $ decimal bs
105 |     in getStack >>= \case
106 |          VS sx   => putStackAs (VO sx   n [<]) LVal
107 |          VK sx s => putStackAs (VL sx s n [<]) LVal
108 |          _       => pure KErr -- impossible
109 |
110 | --------------------------------------------------------------------------------
111 | -- Lexers
112 | --------------------------------------------------------------------------------
113 |
114 | ||| the "M  V30" line prefix
115 | public export
116 | mv30 : RExp True
117 | mv30 = like "M  V30"
118 |
119 | ||| Remainder of a (possibly mutli-line) entry of values and key-value pairs.
120 | export
121 | keyValRest : RExp True
122 | keyValRest = dots >> star ('-' >> newline >> mv30 >> dots) >> newline
123 |
124 | ||| Recognizes some tokens, dropping any optional white space around them.
125 | export %inline
126 | spaced : HasBytes s => HasPosition s => Index r -> Steps q r s -> DFA q r s
127 | spaced x ss = dfa $ conv' (plus ' ') x :: ss
128 |
129 | size : RExp True
130 | size = posdigit >> star digit
131 |
132 | -- according to the spec (sic):
133 | --   >> Strings that contain blank spaces or start
134 | --   >> with left parenthesis or double quote, must be surrounded by
135 | --   >> double quotes
136 | --
137 | -- to distinguish a string from a key, an unquoted string must not contain
138 | -- an equals sign.
139 | unquoted : RExp True
140 | unquoted = start >> star uqc
141 |   where
142 |     uqc, start : RExp True
143 |     uqc   = dot && not ' ' && not ')' && not '='
144 |     start = uqc && not '"' && not '('
145 |
146 | splitted : KST -> Steps q KSz SK -> DFA q KSz SK
147 | splitted x ss =
148 |   spaced x $
149 |     [ linecol' 1 6 ('-' >> newline >> mv30) x
150 |     , newline' newline KDone
151 |     ] ++ ss
152 |
153 | val : KST -> Steps q KSz SK -> DFA q KSz SK
154 | val x ss =
155 |   splitted x $
156 |     [ conv integer (onPrim . I . decimal)
157 |     , read unquoted (onPrim . S)
158 |     , copen' '"' InStr
159 |     ] ++ ss
160 |
161 | toplevel : KST -> DFA q KSz SK
162 | toplevel x =
163 |   val x
164 |     [ conv (plus alphaNum >> '=') onKey
165 |     , copen' '(' LStart
166 |     ]
167 |
168 | str : DFA q KSz SK
169 | str =
170 |   dfa
171 |     [ read (plus $ dot && not '"' && not '-') (pushStr InStr)
172 |     , cexpr "\"\"" (pushStr InStr "\"")
173 |     , cexpr '-'    (pushStr InStr "-")
174 |     , linecol' 1 7 ('-' >> newline >> mv30 >> ' ') InStr
175 |     , linecol' 1 6 ('-' >> newline >> mv30)  InStr
176 |     , ccloseStr '"' (onPrim . S)
177 |     ]
178 |
179 | --------------------------------------------------------------------------------
180 | -- Parser
181 | --------------------------------------------------------------------------------
182 |
183 | kvTrans : Lex1 q KSz SK
184 | kvTrans =
185 |   lex1
186 |     [ E KIni   $ dfa [cexpr' mv30 KeyVal.Entry]
187 |     , E Entry     $ toplevel Entry
188 |     , E KVal   $ toplevel KVal
189 |     , E LVal   $ val LVal []
190 |     , E LStart $ splitted LStart [conv size startList]
191 |     , E LEnd   $ splitted LEnd [cclose ')' (pure Entry)]
192 |     , E InStr    str
193 |     ]
194 |
195 | kvErr : Arr32 KSz (SK q -> F1 q (BoundedErr MolErr))
196 | kvErr =
197 |   arr32 KSz (unexpected [])
198 |     [ E InStr  $ unclosedIfEOI "\"" []
199 |     , E LStart $ unclosedIfEOI "(" []
200 |     , E LVal   $ unclosedIfEOI "(" []
201 |     , E LEnd   $ unclosedIfEOI "(" [")"]
202 |     ]
203 |
204 | kvEOI : KST -> SK q -> F1 q (Either (BoundedErr MolErr) (List KeyVal))
205 | kvEOI sk s t =
206 |   case sk == KDone || sk == Entry of
207 |     False => arrFail SK kvErr sk s t
208 |     True  => case getStack t of
209 |       VS vs # t => Right (vs <>> []) # t
210 |       _     # t => Right [] # t -- impossible
211 |
212 | kv : P1 q (BoundedErr MolErr) (List KeyVal)
213 | kv = P KIni (init (VS [<])) kvTrans noChunk kvErr kvEOI
214 |
215 | ||| Parses V3000 key-value pairs from a (possibly multiline) bytestring.
216 | export %inline
217 | keyVals : ByteString -> Either (BoundedErr MolErr) (List KeyVal)
218 | keyVals = runBytes kv
219 |
220 | test : String -> IO ()
221 | test s =
222 |   either
223 |     (putStrLn . interpolate)
224 |     (traverse_ printLn)
225 |     (parseString kv Virtual s)
226 |
227 | ml : String
228 | ml =
229 |   """
230 |   M  V30 FOO=12 BAR="quux" BAZ="this is a -
231 |   M  V30 test" AND=(7 1 2 3 4 5   -
232 |   M  V30 six "se=ven") im="not yet done"
233 |   """
234 |
235 | sup : String
236 | sup =
237 |   """
238 |   M  V30 1 SUP 0 LABEL=a0 ATOMS=(1 1)\n
239 |   """
240 |