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