This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
||| 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