Proof-of-concept EDSL for writing PostScript with static stack effects.

PostScript.idr

module Main

data Literal : Type where
    float : Float -> Literal

-- A PostScript program which takes a stack of one size to a stack of
-- another size.
-- (PostScript m n) takes a stack of size m and returns a stack of size n.
data PostScript : Nat -> Nat -> Type where
    nop : PostScript n n
    literal : Literal -> PostScript m n -> PostScript m (S n)
    -- User-defined words with some explicit stack postcondition.
    -- Introduces potential unsoundness.
    word : String -> PostScript m n -> PostScript m n'

    -- Given a true branch, false branch, and some code to emit a boolean on the top of the stack,
    -- produce an if-else. Note that both branches must have the same stack effect.
    ifelse : PostScript n p -> PostScript n p -> PostScript m (S n) -> PostScript m p


-- Emit the program
emit : PostScript m n -> IO ()
emit nop = return ()
emit (literal (float n) s) = do
    emit s
    print n
emit (word name s) = do
    emit s
    putStrLn name
emit (ifelse trueCase falseCase s) = do
    emit s
    putStrLn "{"
    emit trueCase
    putStrLn "}"
    putStrLn "{"
    emit falseCase
    putStrLn "}"
    putStrLn "ifelse"


-- Command sequencing
infixr 1 ?.
(?.) : (a -> b) -> (b -> c) -> a -> c
(?.) = flip (.)

ifthen : PostScript n n -> PostScript m (S n) -> PostScript m n
ifthen trueCase s = ifelse trueCase nop s

dup : PostScript m n -> PostScript m (S n)
dup = word "dup"

pop : PostScript m (S n) -> PostScript m n
pop = word "pop"

moveto : PostScript m (S (S n)) -> PostScript m n
moveto = word "moveto"

lineto : PostScript m (S (S n)) -> PostScript m n
lineto = word "lineto"

stroke : PostScript m n -> PostScript m n
stroke = word "stroke"

greater : PostScript m (S (S n)) -> PostScript m (S n)
greater = word "gt"

and : PostScript m (S (S n)) -> PostScript m (S n)
and = word "and"

-- Convenience: make a literal from a float
lf : Float -> PostScript m n -> PostScript m (S n)
lf = literal . float

lineTo : Float -> Float -> PostScript 0 0
lineTo x y = lf x ?. lf 0 ?. greater ?.
             lf y ?. lf 0 ?. greater ?. and ?.
             ifthen -- Check if both x and y are positive
                (lf 50 ?. lf 50 ?. -- If so, draw a line. Otherwise do nothing.
                 moveto ?.
                 lf x ?. lf y ?.
                 lineto ?.
                 stroke $ nop) $ nop

main : IO ()
main = emit $ lineTo 200 200