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