mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 20:51:43 +03:00
Merge pull request #310 from chrrasmussen/replace-ffi-in-hex-function
Replace FFI implementation of 'hex' function with a plain Idris version
This commit is contained in:
commit
452eaaf2b9
@ -56,14 +56,8 @@ showRacketChar : Char -> String -> String
|
||||
showRacketChar '\\' = ("\\\\" ++)
|
||||
showRacketChar c
|
||||
= if c < chr 32 || c > chr 126
|
||||
then (("\\u" ++ pad (asHex (cast c))) ++)
|
||||
then (("\\u" ++ leftPad '0' 4 (asHex (cast c))) ++)
|
||||
else strCons c
|
||||
where
|
||||
pad : String -> String
|
||||
pad str
|
||||
= case isLTE (length str) 4 of
|
||||
Yes _ => pack (List.replicate (minus 4 (length str)) '0') ++ str
|
||||
No _ => str
|
||||
|
||||
showRacketString : List Char -> String -> String
|
||||
showRacketString [] = id
|
||||
|
@ -3,6 +3,7 @@ module Idris.IDEMode.Commands
|
||||
import Core.Core
|
||||
import Core.Name
|
||||
import public Idris.REPLOpts
|
||||
import Utils.Hex
|
||||
|
||||
import System.File
|
||||
|
||||
@ -253,21 +254,14 @@ export
|
||||
version : Int -> Int -> SExp
|
||||
version maj min = toSExp (SymbolAtom "protocol-version", maj, min)
|
||||
|
||||
%foreign "C:fprintf,libc 6"
|
||||
prim__printfHex : AnyPtr -> String -> Int -> PrimIO ()
|
||||
|
||||
hex : File -> Int -> IO ()
|
||||
hex (FHandle h) num
|
||||
= primIO $ prim__printfHex h "%06x" num
|
||||
|
||||
sendLine : File -> String -> IO ()
|
||||
sendLine f st =
|
||||
sendStr : File -> String -> IO ()
|
||||
sendStr f st =
|
||||
map (const ()) (fPutStr f st)
|
||||
|
||||
export
|
||||
send : SExpable a => File -> a -> Core ()
|
||||
send f resp
|
||||
= do let r = show (toSExp resp) ++ "\n"
|
||||
coreLift $ hex f (cast (length r))
|
||||
coreLift $ sendLine f r
|
||||
coreLift $ sendStr f $ leftPad '0' 6 (asHex (cast (length r)))
|
||||
coreLift $ sendStr f r
|
||||
coreLift $ fflush f
|
||||
|
@ -1,5 +1,6 @@
|
||||
module Utils.Hex
|
||||
|
||||
import Data.List
|
||||
import Data.Primitives.Views
|
||||
|
||||
%default total
|
||||
@ -26,13 +27,23 @@ hexDigit _ = 'X' -- TMP HACK: Ideally we'd have a bounds proof, generated below
|
||||
||| Convert a positive integer into a list of (lower case) hexadecimal characters
|
||||
export
|
||||
asHex : Int -> String
|
||||
asHex n = pack $ asHex' n []
|
||||
asHex n =
|
||||
if n > 0
|
||||
then pack $ asHex' n []
|
||||
else "0"
|
||||
where
|
||||
asHex' : Int -> List Char -> List Char
|
||||
asHex' 0 hex = hex
|
||||
asHex' n hex with (n `divides` 16)
|
||||
asHex' (16 * div + rem) hex | DivBy div rem _ =
|
||||
assert_total $ asHex' div (hexDigit rem :: hex)
|
||||
asHex' (assert_smaller n div) (hexDigit rem :: hex)
|
||||
|
||||
export
|
||||
leftPad : Char -> Nat -> String -> String
|
||||
leftPad paddingChar padToLength str =
|
||||
if length str < padToLength
|
||||
then pack (List.replicate (minus padToLength (length str)) paddingChar) ++ str
|
||||
else str
|
||||
|
||||
export
|
||||
fromHexDigit : Char -> Maybe Int
|
||||
|
Loading…
Reference in New Issue
Block a user