0 | module Text.Molfile.SData
 1 |
 2 | import Data.ByteString
 3 | import Derive.Prelude
 4 | import Derive.Refined
 5 | import public Data.Nat
 6 | import public Data.String
 7 | import public Data.Refined
 8 | import public Data.Refined.Integer
 9 | import public Data.Refined.String
10 |
11 | %default total
12 | %language ElabReflection
13 |
14 | public export
15 | IsHeaderChar : Char -> Bool
16 | IsHeaderChar '>' = False
17 | IsHeaderChar '<' = False
18 | IsHeaderChar c   = not (isControl c)
19 |
20 | public export
21 | 0 IsHeader : String -> Type
22 | IsHeader = Len (<= 70) && Str (All $ Holds IsHeaderChar)
23 |
24 | ||| Header of a SDF data entry. This is put in angles (`<>`) in an SD file.
25 | public export
26 | record SDHeader where
27 |   constructor SDH
28 |   value : String
29 |   {auto 0 prf : IsHeader value}
30 |
31 | export %inline
32 | Interpolation SDHeader where
33 |   interpolate = value
34 |
35 | namespace SDHeader
36 |   %runElab derive "SDHeader" [Show,Eq,Ord,RefinedString]
37 |
38 | export
39 | readHeader : ByteString -> SDHeader
40 | readHeader bs =
41 |   case break (60 ==) bs of -- '<'
42 |     (_, BS 0 _)      => ""
43 |     (_, BS (S k) bv) =>
44 |       fromMaybe "" $ refineSDHeader (toString . BV.takeWhile (62 /=) $ tail bv)
45 |
46 | ||| Encodes a value header by replacing spaces with underscores and
47 | ||| dropping some other invalid characters such as angles.
48 | export
49 | encodeHeader : String -> Maybe SDHeader
50 | encodeHeader = refineSDHeader . convert [<] . unpack
51 |   where
52 |     convert : SnocList Char -> List Char -> String
53 |     convert sc [] = pack $ sc <>> []
54 |     convert sc (' '::t) = convert (sc :< '_') t
55 |     convert sc (h::t)   =
56 |       if isAlphaNum h then convert (sc:<h) t else convert sc t
57 |
58 | public export
59 | 0 IsValue : String -> Type
60 | IsValue = Str (All Printable)
61 |
62 | ||| Value of an SDF data entry. This follows after the header (see
63 | ||| `SDHeader`) and may span across several lines, each of which must not
64 | ||| be longer than 200 characters.
65 | public export
66 | record SDValue where
67 |   constructor SDV
68 |   value : String
69 |   {auto 0 prf : IsValue value}
70 |
71 | export %inline
72 | Interpolation SDValue where
73 |   interpolate = value
74 |
75 | namespace SDValue
76 |   %runElab derive "SDValue" [Show,Eq,Ord,RefinedString]
77 |
78 | ||| A data entry in an SD file consisting of the data header and value.
79 | public export
80 | record StructureData where
81 |   constructor SD
82 |   header : SDHeader
83 |   value  : SDValue
84 |
85 | %runElab derive "StructureData" [Show,Eq]
86 |
87 | ||| Tries to convert a name-value pair to a piece of
88 | ||| SD-data.
89 | |||
90 | ||| While the values is refined as it is, we try to encode the
91 | ||| header in such a way that it does not contain any invalid
92 | ||| characters.
93 | export
94 | encodeStructureData : (name,value : String) -> Maybe StructureData
95 | encodeStructureData n v = [| SD (encodeHeader n) (refineSDValue v) |]
96 |