Quine's Method, HTML version

Our next goal will be more ambitious. Generating a proof seems almost easy compared to the complexity of rendering in something that resembles human-readable form. Our goal is to take an input file that contains a sequence of propositions in the ASCII format we developed for the propositional parsing lecture, like this:

a -> a
a -> b -> a
a -> (a -> b) -> b

And produce an HTML file that contains a formatted sequence of proofs, like this:

Propositional Tautologies

Proposition 1: $\proves\;{\alpha}\:\limplies\:{\alpha}$

Quine Alternatives:

$\Box$ Proposition 1

Proposition 2: $\proves\;{\alpha}\:\limplies\:{\beta}\:\limplies\:{\alpha}$

Quine Alternatives:

$\Box$ Proposition 2

Proposition 3: $\proves\;{\alpha}\:\limplies\:({\alpha}\:\limplies\:{\beta})\:\limplies\:{\beta}$

Quine Alternatives:

$\Box$ Proposition 3

There are a lot of moving parts:

Each one of these parts adds something essential to solving the problem, and each adds a few of its own quirks and complexity. But this is in a way representative of how programming has changed—these days, we're often called upon to produce solutions that rely on the complementary capabilities of a number of different systems, and somehow we have to get them all working together. For us, Haskell is our main tool, and provides much of the glue, but there's more to this than just Haskell.

Let's start with Blaze, a system that is superficially similar to the HTML module we wrote in Lecture 15. It's similar enough that I'm not going to dwell too much on the Blaze-specific parts of the code. But it's important to note that Blaze defines a basic Html type (note capitalization), and that this type is an instance of Monoid. We're going to use this heavily. Note also the home page for BlazeHtml, which includes tutorials, documentation, etc. Unfortunately, Blaze isn't part of the Haskell Platform, and so requires installation via cabal:

$ cabal sandbox init $ cabal install blaze-html

Let's start with the big picture:

{-# LANGUAGE OverloadedStrings #-} module Main where ... main :: IO () main = do args <- getArgs case args of [infile,outfile] -> do input <- readFile infile let fmlas = map read . lines $ input writeFile outfile $ renderHtml $ page fmlas _ -> usage

This is like other things we've seen, the only really new thing here the use of the {-# LANGUAGE OverloadedStrings #-} compiler directive. This allows us to use ordinary string literals to initialize things that aren't actually strings by making them instances of the IsString type class from Data.String, and this simplifies writing Blaze code. The big moving part here is page, which produces the basic template of the HTML page we're writing:

page :: [Proposition] -> Html page tautologies = docTypeHtml $ do H.head $ do title "Propositional Tautologies" script ! type_ "text/javascript" ! src MathJax $ "" script ! type_ "text/x-MathJax-config" $ config H.style ! type_ "text/css" $ css body $ do h1 "Propositional Tautologies" execQuineState $ mapM_ makeSection (zip [1..] (map getProp tautologies)) where MathJax = "http://cdn.MathJax.org/MathJax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML" config = toHtml $ unlines [ "MathJax.Hub.Config({" , " tex2jax: {" , " inlineMath: [['$','$'], ['\\(','\\)']]" , " }," , " TeX: {" , " Macros: {" , " limplies: \"{\\\\rightarrow}\"," , " ltrue: \"{\\\\top}\"," , " lfalse: \"{\\\\bot}\"," , " proves: \"{\\\\vdash}\"}" , " } " , "});" ] css = "h1,h2,p.box { color: maroon }"

There basic structure of the page is an <html> element, which contains <head> and <body> elements. The <head> element contains a <title> element, a couple of <script> elements, each of which is related to the MathJax system, and a <style> that contains CSS. The (!) operator is used by Blaze to set a attribute on a tag. Note that the argument to <title> isn't actually a String, it's an Html, and that's the OverloadedStrings directive at work. Without this, we'd have to write title $ toHtml "Tautologies" here, and a few thousand other places. The definitions inside config are actually in JSON (JavaScript Object Notation), and the bindings in Macros describe LaTeX definitions, rendered in JavaScript, re-encoded in Haskell. Thus, we are defining \limplies to be {\rightarrow}, but this gets put inside a JavaScript string, and becomes "{\\rightarrow}, as JavaScript using backslash to quote backslash, and then this string has to be expressed within a Haskell string, becoming "\"{\\\\rightarrow}\"". And so describing one backslash through these layers requires four. It's enough to make a person long for Python's raw strings. As for breaking out the CSS content into a separate definition, it hardly seems necessary with the modest amount of styling we're doing now, but every web developer knows that to the writing of CSS there is no end.

You're also to be forgiven for thinking there must be a better way to describe multi-line strings than via unlines, as this sort of thing is cumbersome to write and maintain. There are a few, but the most flexible approach is through Template Haskell's Quasi-quoters, and that's a complication too many for the code here.

The heavy work here is done by the makeSection function, which returns a monadic result:

type QuineState = WriterT Html (State [(Int,Prop String)]) execQuineState :: QuineState a -> Html execQuineState qs = evalState (execWriterT qs) [] makeSection :: (Int,Prop String) -> QuineState () makeSection (idx,prop) = do tauts <- get case quineAnalyze tauts prop of Left r -> tell $ refutationToHtml idx prop r Right r -> do tell $ proofToHtml idx prop r modify (++[(idx,prop)])

This is one of those cases where the code is easier to follow than the types. A QuineState describes a value that's in a layered monad that combines Writer Html, for accumulating Html written across calls to makeSection, with State [(Int,Prop String], which holds a growing list of integer/tautology pairs, representing tautologies proved in previous sections. But it's easy to see the moving parts in action: refutationToHtml and proofToHtml produce Html values, which get logged via calls to tell. In the case where we prove a proposition, we add it to the state, for downstream calls to makeSection to use.

The refutationToHtml produces a representation of a refuting valuation, as well as a reduction sequence that begins by substituting the refuting valuation into the proposition, and the subsequent simplification of this form to $\lfalse$.

refutationToHtml :: (Show a) => a -> Prop String -> Refutation String -> Html refutationToHtml idx prop (Refutation valuation) = do h2 . toHtml $ "Refutable " ++ show idx ++ ": " ++ showTeX prop p "Refuting valuation" ul $ mapM_ (li . toHtml . (\(k,v) -> "$" ++ greek k ++ "$ := " ++ showBool v)) (Map.toList valuation) p "Reduction" ul $ mapM_ (li . toHtml . showTeX) (simplifyInSteps (substitute (Map.map Boolean valuation) prop)) p "Reduced to ${\\lfalse}$."

Note here the calls to toHtml, which we can't avoid when we're building String arguments ourselves, instead of using String literals. The functions showTeX renders a Prop String as a String containing LaTeX, greek produces a TeX representation of a lower-case letter in the Greek alphabet (given a lowercase Roman letter in the range ["a".."w"]), following the standard conventions of Mathematics, and showBool produces a String containing a LaTeX representation of a boolean value.

propToTeX :: (a -> String) -> Prop a -> String propToTeX litf = prec 0 where prec _ (Boolean True) = "{\\ltrue}" prec _ (Boolean False) = "{\\lfalse}" prec _ (Var v) = litf v prec _ (Not p) = "{\\lnot}" ++ prec 3 p prec i (And s t) = paren 2 i $ prec 2 s ++ "\\,\\land\\," ++ prec 2 t prec i (Or s t) = paren 1 i $ prec 1 s ++ "\\,\\lor\\," ++ prec 1 t prec i (Implies s t) = paren 0 i $ prec 1 s ++ "\\:\\limplies\\:" ++ prec 0 t paren cutoff prec str | prec > cutoff = "(" ++ str ++ ")" | otherwise = str greek a = fromJust $ lookup a [("a","{\\alpha}"),("b","{\\beta}"),("c","{\\gamma}"), ("d","{\\delta}"),("e","{\\epsilon}"),("f","{\\zeta}"), ("g","{\\eta}"),("h","{\\theta}"), ("i","{\\iota}"), ("j","{\\kappa}"),("k","{\\lambda}"),("l","{\\mu}"), ("m","{\\nu}"),("n","{\\xi}"),("o","{\\omicron}"), ("p","{\\pi}"),("q","{\\rho}"),("r","{\\sigma}"),("s","{\\tau}"), ("t","{\\upsilon}"),("u","{\\phi}"),("v","{\\chi}"), ("w","{\\psi}"),("x","{\\omega}")] showTeX :: Prop String -> String showTeX p = "$" ++ propToTeX greek p ++ "$" showBool :: Bool -> String showBool True = "${\\ltrue}$" showBool False = "${\\lfalse}$"

There are all kinds of TeX subtleties apparent here. Various commands in TeX, as already mentioned, begin with a backslash, which we'll need to quote in Haskell strings. But we don't want a command to be inadvertently merged with following text, so we'll usually protect bare commands by putting them inside of set-braces, which TeX uses for grouping, thus, e.g., "{\\ltrue}". But the logical connectives are symbols that TeX doesn't associate with any specific role, so we'll provide a bit of extra space around $\land$ and $\lor$, and a bit more around an $\limplies$. This involves using TeX math-mode spacing commands, \, and \;, properly quoted within Haskell strings.

The basic structure of the propToTeX function is familiar—we've seen such output code before. It's regrettable to have to re-write it. The greek function just does a big table lookup, while showTeX is basically a shortcut for putting the results of propToTeX inside of dollar signs, which is how we're indicating TeX in HTML to MathJax.

This leaves the function proofToHtml, which is surprising subtle:

proofToHtml :: Int -> Prop String -> Proof String -> Html proofToHtml idx prop proof = do h2 . toHtml $ "Proposition " ++ show idx ++ ": " ++ " $\\proves\\;" ++ propToTeX greek prop ++ "$" format proof where format proof = case proof of Node props var trueb falseb -> do simplifyToHtml props let prop = last props p "Quine Alternatives:" ul $ do li $ showBranch True trueb li $ showBranch False falseb where showBranch bool branch = do p . toHtml $ showTeX prop ++ " [$" ++ greek var ++ "$:=" ++ showBool bool ++ "]" format branch Leaf props -> do simplifyToHtml props p "Reduced to ${\\ltrue}$." Reference props cite pattern map -> do simplifyToHtml props let prop = last props p . toHtml $ "Instance of Proposition " ++ show cite ++ ": " ++ showTeX pattern ++ "."

The hard part of the problem is that writing out the description of what you're trying to prove happens one level higher in the Proof than you'd expect, because that's where the necessary information is. And there's the distinction between describing the root (which is at the <h2> level), and subsequent nodes (which are inside <li>'s). This subtlety aside, the code is fairly straightforward. Note that simplification sequences are produced using simplifyToHtml:

simplifyToHtml :: [Prop String] -> Html simplifyToHtml props = when (length props > 1) $ do p "Simplification" ul $ mapM_ (li . toHtml . showTeX) props

Note here the use of when, as this ensures that only non-trivial simplifications are printed.

Code