Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
||| Binary parsing, based on the stuff in Power of Pi
module Bin
import System
import Data.So
import Data.Vect
import Bytes
%default total
data BaseData : Type where
||| A byte
Byte : BaseData
||| n repetitions of some base data
NTimes : Nat -> BaseData -> BaseData
||| An ASCII Char
Ch : BaseData
||| Interpret the base data as a type
baseType : BaseData -> Type
baseType Byte = Bits8
baseType (NTimes n b) = Vect n (baseType b)
baseType Ch = Char
||| A tagged bit of code, to make things easier to read and debug
data Section : String -> Type -> Type where
MkSection : (lbl : String) -> (x : a) -> Section lbl a
mutual
||| Format specifiers, which combine base data
data Fmt : Type where
Part : String -> Fmt -> Fmt
Bad : String -> Fmt
End : Fmt
Base : BaseData -> Fmt
OneOf : Fmt -> Fmt -> Fmt
Many : Fmt -> Fmt
Skip : (fmt : Fmt) -> (rep : resultOf fmt) -> Fmt -> Fmt
(>>=) : (fmt : Fmt) -> (resultOf fmt -> Fmt) -> Fmt
||| Compute the type that corresponds to base data
resultOf : Fmt -> Type
resultOf (Part lbl fmt) = Section lbl (resultOf fmt)
resultOf (Bad _) = Void
resultOf End = ()
resultOf (Base b) = baseType b
resultOf (OneOf x y) = Either (resultOf x) (resultOf y)
resultOf (Many fmt) = List (resultOf fmt)
resultOf (Skip _ _ y) = resultOf y
resultOf (fmt >>= f) = (x : resultOf fmt ** resultOf (f x))
||| Match data that satisfies a predicate
satisfy : [static] String -> [static] (fmt : Fmt) -> (resultOf fmt -> Bool) -> Fmt
satisfy what fmt p =
do x <- fmt
if p x
then End
else Bad what
||| Match one particular byte
byte : Bits8 -> Fmt -> Fmt
byte b fmt = Skip (satisfy "byte" (Base Byte) (b ==))
(b ** rewrite primEqReflexive b in ()) fmt
where postulate primEqReflexive : (x : Bits8) -> prim__eqB8 x x = 1
||| Match one byte that's an ASCII space or newline
whitespace : Fmt
whitespace = satisfy "whitespace" (Base Byte) (\x => x == 0x0a || x == 0x20)
||| Match at least one whitespace byte
whitespaces : Fmt
whitespaces = Skip whitespace (0x20 ** ()) (Many whitespace)
||| Match at least one ASCII digit
digit : Fmt
digit = satisfy "digit" (Base Ch) isDigit
data Result : Fmt -> Type where
Failure : (msg : String) -> Result fmt
Success : resultOf fmt -> Int -> Result fmt
||| Read the base datatypes from a byte array
|||
||| @ b the format to read
||| @ i the pointer to start at
||| @ j the size of the array
covering
readBase : [static] (b : BaseData) -> (i : Int) -> ByteArray j -> IO (Maybe (baseType b, Int))
readBase Byte i arr with (choose $ inBounds i j)
readBase Byte i arr | Right x = return Nothing
readBase Byte i arr | Left ok = do byte <- read i arr ok
return (Just (byte, i+1))
readBase (NTimes n b) i arr = ntimes n i
where partial
ntimes : (n : Nat) -> Int -> IO (Maybe (Vect n (baseType b), Int))
ntimes Z i = return (Just ([], i))
ntimes (S k) i = do Just (x, i') <- readBase b i arr
| Nothing => return Nothing
Just (xs, i'') <- ntimes k i'
| Nothing => return Nothing
return $ Just (x::xs, i'')
readBase Ch i arr with (choose $ inBounds i j)
readBase Ch i arr | Right x = return Nothing
readBase Ch i arr | Left ok = do byte <- read i arr ok
return (Just (chr (prim__zextB8_Int byte), i+1))
||| Read from a byte array according to some format
|||
||| @ fmt the format to read
||| @ i the pointer to start at
||| @ j the size of the array
covering
readFmt : [static] (fmt : Fmt) -> (i : Int) -> ByteArray j -> IO (Result fmt)
readFmt (Part lbl fmt) i arr =
putStrLn lbl >>= \_ =>
case !(readFmt fmt i arr) of
Failure msg => return (Failure $ "In " ++ lbl ++ ": " ++ msg)
Success x i' => return (Success (MkSection lbl x) i')
readFmt (Bad msg) i arr = return (Failure $ "Couldn't get: " ++ msg)
readFmt End i arr = return (Success () i)
readFmt (Base b) i arr =
case !(readBase b i arr) of
Nothing => return (Failure "couldn't read base")
Just (elt, i') => return (Success elt i')
readFmt (OneOf fmt fmt') i arr =
case !(readFmt fmt i arr) of
Failure msg => case !(readFmt fmt' i arr) of
Failure msg' => return (Failure $ msg ++ msg')
Success res i' => return $ Success (Right res) i'
Success res i' => return $ Success (Left res) i'
readFmt (Many fmt) i arr =
case !(readFmt fmt i arr) of
Failure _ => return $ Success [] i
Success x i' =>
case !(readFmt (Many fmt) i' arr) of
Failure _ => return $ Success [x] i'
Success xs i'' => return $ Success (x::xs) i''
readFmt (Skip fmt _ fmt') i arr =
case !(readFmt fmt i arr) of
Failure msg => return $ Failure msg
Success _ i' =>
case !(readFmt fmt' i' arr) of
Failure msg => return $ Failure msg
Success res i'' => return $ Success res i''
readFmt (fmt >>= f) i arr =
case !(readFmt fmt i arr) of
Failure msg => return $ Failure msg
Success x i' => case !(readFmt (f x) i' arr) of
Failure msg => return $ Failure msg
Success y i'' => return $ Success (x ** y) i''
||| Read according to a format, starting with the beginning of the array
covering
readArray : [static] (fmt : Fmt) -> ByteArray j -> IO (Result fmt)
readArray fmt arr = readFmt fmt 0 arr
||| PPM raw images (no support for comments in the header yet)
ppm : Fmt
ppm = do Part "Magic" $ do
byte 0x50 $ byte 0x36 $ whitespaces
x <- Many digit
y <- Skip whitespaces [(0x20 ** ())] $ Many digit
let width = dimension $ map getWitness x
let height = dimension $ map getWitness y
maxColor <- Skip whitespaces [(0x20 ** ())] $ Many digit
let colspace = dimension $ map getWitness maxColor
Skip whitespace (0x20 ** ()) $
(Part "Image data:" $ Base $ NTimes width $ NTimes height $ NTimes 3 Byte)
End
where dimension : List Char -> Nat
dimension xs = fromInteger $ cast $ pack xs
||| Flip the contents of PPM image data
mirror : resultOf ppm -> resultOf ppm
mirror (magic ** (width ** (height ** (maxColor ** (MkSection "Image data:" pixels ** ()))))) =
(magic ** (width ** (height ** (maxColor ** (MkSection "Image data:" (reverse pixels) ** ())))))
||| Write base data to a byte array
covering -- TODO: make helper structurally recursive on format
writeBase : (b : BaseData) -> baseType b -> ByteArray k -> Int -> IO Int
writeBase {k} Byte x arr i with (choose $ inBounds i k)
writeBase {k} Byte x arr i | Right y = do putStrLn "Overflow1" ; exit 1; return (-100)
writeBase {k} Byte x arr i | Left ok = do write i x arr ok; return (i + 1)
writeBase (NTimes Z y) [] arr i = return i
writeBase (NTimes (S j) y) (x :: xs) arr i = do i' <- writeBase y x arr i
writeBase (NTimes j y) xs arr i'
writeBase {k} Ch x arr i with (choose $ inBounds i k)
writeBase {k = k} Ch x arr i | Right y = do putStrLn "Overflow2" ; exit 1; return (-100)
writeBase {k = k} Ch x arr i | Left ok =
do let byte = prim__truncInt_B8 $ prim__charToInt x
write i byte arr ok
return (i + 1)
||| Write formatted data to a byte array, starting at position 0
|||
||| @ fmt the format to follow
covering
writeArr : resultOf fmt -> ByteArray k -> IO ()
writeArr {k} res arr = do writeArr' _ res 0; return ()
where partial
writeArr' : (fmt : Fmt) -> resultOf fmt -> Int -> IO Int
writeArr' (Part _ fmt) (MkSection _ res) i = writeArr' fmt res i
writeArr' (Bad x) res i = absurd res
writeArr' End () i = return i
writeArr' (Base x) res i = writeBase x res arr i
writeArr' (OneOf fmt _) (Left x) i = writeArr' fmt x i
writeArr' (OneOf _ fmt) (Right x) i = writeArr' fmt x i
writeArr' (Many x) [] i = return i
writeArr' (Many x) (y :: xs) i = writeArr' x y i >>= writeArr' (Many x) xs
writeArr' (Skip x rep y) res i = writeArr' x rep i >>= writeArr' y res
writeArr' (fmt >>= f) (x ** y) i = do i' <- writeArr' fmt x i
writeArr' (f x) y i'
namespace Main
partial
main : IO ()
main = do putStrLn "Running"
Right (k ** image) <- slurp "me3.ppm"
| Left err => do putStrLn err; exit 1
putStrLn "Array slurped."
res <- readArray ppm image
putStrLn "Processed."
case res of
Failure msg => putStrLn $ "Failure: " ++ msg
Success res i => do putStrLn $ "Success at " ++ show i ++ "!"
arr' <- allocBytes (10 + k) (const 0)
writeArr (mirror res) arr'
dump "me3Flip.ppm" arr'
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.