0 | ||| Common types and utility funtions for the LSP server implementation.
  1 | |||
  2 | ||| (C) The Idris Community, 2021
  3 | module Language.LSP.Utils
  4 |
  5 | import Data.Bits
  6 | import Data.List
  7 | import Data.String
  8 | import Language.JSON
  9 | import Language.LSP.Message
 10 | import System.File
 11 | import System
 12 | import System.Info
 13 |
 14 | export
 15 | headerLineEnd : String
 16 | headerLineEnd = if isWindows then "\n" else "\r\n"
 17 |
 18 | ||| Reads a single header from an LSP message on the supplied file handle.
 19 | ||| Headers end with the string "\r\n".
 20 | export
 21 | fGetHeader : (handle : File) -> IO (Either FileError String)
 22 | fGetHeader handle = do
 23 |   False <- fEOF handle
 24 |     | True => exitWith (ExitFailure 1)
 25 |   Right l <- fGetLine handle
 26 |     | Left err => pure $ Left err
 27 |   -- TODO: reading up to a string should probably be handled directly by the FFI primitive
 28 |   --       or at least in a more efficient way in Idris2
 29 |   if isSuffixOf headerLineEnd l
 30 |      then pure $ Right l
 31 |      else (map (l ++)) <$> fGetHeader handle
 32 |
 33 | -- From Language.JSON.Data
 34 | private
 35 | b16ToHexString : Bits16 -> String
 36 | b16ToHexString n =
 37 |   case n of
 38 |     0 => "0"
 39 |     1 => "1"
 40 |     2 => "2"
 41 |     3 => "3"
 42 |     4 => "4"
 43 |     5 => "5"
 44 |     6 => "6"
 45 |     7 => "7"
 46 |     8 => "8"
 47 |     9 => "9"
 48 |     10 => "A"
 49 |     11 => "B"
 50 |     12 => "C"
 51 |     13 => "D"
 52 |     14 => "E"
 53 |     15 => "F"
 54 |     other => assert_total $
 55 |                b16ToHexString (n `shiftR` 4) ++
 56 |                b16ToHexString (n .&. 15)
 57 |
 58 | ||| Pad a string with leading zeros, if
 59 | ||| its length is less than 4, up to 4 symbols.
 60 | pad4 : String -> String
 61 | pad4 str =
 62 |   case length str of
 63 |     0 => "0000"
 64 |     1 => "000" ++ str
 65 |     2 => "00" ++ str
 66 |     3 => "0" ++ str
 67 |     _ => str
 68 |
 69 | ||| See https://en.wikipedia.org/wiki/UTF-16 for the algorithm.
 70 | ||| Returns the codepoint value represented as a hex string,
 71 | ||| if it encodes a symbol from the Basic Multilingual Plane.
 72 | ||| Otherwise, returns the 16-bit surrogate pair, every element of which
 73 | ||| is, in turn, represented as a hex string.
 74 | encodeCodepointH : Bits32 -> Either String (String, String)
 75 | encodeCodepointH x =
 76 |   case x <= 0xFFFF of
 77 |     -- Basic Multilingual Plane
 78 |     True => Left $ pad4 (b16ToHexString (cast x))
 79 |     --  One of the Supplementary Planes
 80 |     False =>
 81 |       let x' = x - 0x10000 in
 82 |       Right $
 83 |         ( pad4 (b16ToHexString (cast $ 0xD800 + (x' `shiftR` 10)))
 84 |         , pad4 (b16ToHexString (cast $ 0xDC00 + (x' .&. 0b1111111111))))
 85 |
 86 | ||| Encode an arbitrary unicode codepointby escaping it
 87 | ||| as defined in
 88 | ||| https://tools.ietf.org/id/draft-ietf-json-rfc4627bis-09.html#rfc.section.7
 89 | encodeCodepoint : Bits32 -> String
 90 | encodeCodepoint x =
 91 |   case encodeCodepointH x of
 92 |     Left w => "\\u" ++ w
 93 |     Right (w1, w2) => "\\u" ++ w1 ++ "\\u" ++ w2
 94 |
 95 | ||| Here we escape all wide characters (exceeding 8 bit width).
 96 | ||| JSON spec doesn't seem to require that,
 97 | ||| but at least some of the editors (e.g. Neovim) expect
 98 | ||| wide characters escaped, otherwise refusing to work.
 99 | private
100 | showChar : Char -> String
101 | showChar c =
102 |   case c of
103 |        '\b' => "\\b"
104 |        '\f' => "\\f"
105 |        '\n' => "\\n"
106 |        '\r' => "\\r"
107 |        '\t' => "\\t"
108 |        '\\' => "\\\\"
109 |        '"'  => "\\\""
110 |        c => if isControl c || c >= '\127'
111 |                then encodeCodepoint (cast $ ord c)
112 |                else singleton c
113 |
114 | private
115 | showString : String -> String
116 | showString x = "\"" ++ concatMap showChar (unpack x) ++ "\""
117 |
118 | export
119 | stringify : JSON -> String
120 | stringify JNull = "null"
121 | stringify (JBoolean x) = if x then "true" else "false"
122 | stringify (JNumber x) =
123 |   let s = show x
124 |    in if isSuffixOf ".0" s then substr 0 (length s `minus` 2) s else s
125 | stringify (JString x) = showString x
126 | stringify (JArray xs) = "[" ++ stringifyValues xs ++ "]"
127 |   where
128 |     stringifyValues : List JSON -> String
129 |     stringifyValues [] = ""
130 |     stringifyValues (x :: xs) =
131 |       stringify x ++ if isNil xs then "" else "," ++ stringifyValues xs
132 | stringify (JObject xs) = "{" ++ stringifyProps xs ++ "}"
133 |   where
134 |     stringifyProp : (String, JSON) -> String
135 |     stringifyProp (key, value) = showString key ++ ":" ++ stringify value
136 |
137 |     stringifyProps : List (String, JSON) -> String
138 |     stringifyProps [] = ""
139 |     stringifyProps (x :: xs) =
140 |       stringifyProp x ++ if isNil xs then "" else "," ++ stringifyProps xs
141 |
142 | export
143 | pathToURI : String -> URI
144 | pathToURI path =
145 |   MkURI { scheme    = "file"
146 |         , authority = Just (MkURIAuthority Nothing "" Nothing)
147 |         , path      = path
148 |         , query     = ""
149 |         , fragment  = ""
150 |         }
151 |
152 | export
153 | Show Position where
154 |   show (MkPosition line character) = "\{show line}:\{show character}"
155 |
156 | export
157 | Show Range where
158 |   show (MkRange start end) = "\{show start} -- \{show end}"
159 |
160 | export
161 | systemPathToURIPath : String -> String
162 | systemPathToURIPath p = if not isWindows then p else
163 |   let p1 = fastPack (map (\c => if c == '\\' then '/' else c) (fastUnpack p))
164 |   in case strUncons p1 of
165 |     Just ('/', _) => p1
166 |     _ => strCons '/' p1
167 |
168 | export
169 | uriPathToSystemPath : String -> String
170 | uriPathToSystemPath p = if not isWindows then p else
171 |   let p1 = case strUncons p of
172 |         Just ('/', tail) => tail
173 |         _ => p
174 |   in fastPack (map (\c => if c == '/' then '\\' else c) (fastUnpack p1))
175 |