Fix bitrotting in manual

Author: nick8325

Filter.hs

@@ -1,11 +1,9 @@
-#!/usr/bin/runhaskell
-
 {-# LANGUAGE RecordWildCards #-}
 import Text.Pandoc.JSON
 import Text.Pandoc
 import Tip.Core
 import Tip.Parser
-import Tip.Passes
+import Tip.Passes hiding (Mode)
 import qualified Tip.Pretty.SMT as SMT
 import qualified Tip.Pretty.Why3 as Why3
 import Control.Monad
@@ -28,7 +26,6 @@ tipBlock name classes attrs expr =
     (modes, passes) = go classes [] []
     go [] modes passes = (reverse modes, reverse passes)
     go ("no-datatypes":xs) modes passes = go xs (NoData:modes) passes
-    go ("no-check-sat":xs) modes passes = go xs (NoCheckSat:modes) passes
     go ("no-functions":xs) modes passes = go xs (NoFuns:modes) passes
     go ("no-properties":xs) modes passes = go xs (NoProp:modes) passes
     go ("why3":xs) modes passes = go xs (Why3:modes) passes
@@ -37,20 +34,19 @@ tipBlock name classes attrs expr =
         [(pass, "")] -> go xs modes (pass:passes)
         _ -> error ("Unknown pass " ++ x)
 
-data Mode = NoData | NoProp | NoFuns | NoCheckSat | Why3 deriving (Show, Eq)
+data Mode = NoData | NoProp | NoFuns | Why3 deriving (Show, Eq)
 
 pass :: StandardPass -> Theory Id -> Theory Id
-pass p = freshPass (runPass p)
+pass p thy =
+  case freshPass (runPass p) thy of
+    [thy'] -> thy'
 
 mode :: [Mode] -> Theory Id -> String
 mode ms thy@Theory{..}
   | Why3 `elem` ms       = show . Why3.ppTheory $ thy'
-  | NoCheckSat `elem` ms = out' thy'
   | otherwise = out thy'
   where
-    out  = show . SMT.ppTheory
-    out' = dropRev (length "(check-sat)") . show . SMT.ppTheory
-    dropRev n = reverse . drop n . reverse
+    out  = show . SMT.ppTheory (SMT.smtQuoted ++ SMT.tipKeywords ++ SMT.smtKeywords)
     thy' =
       thy {
         thy_datatypes = checking NoData thy_datatypes,

Makefile

@@ -8,6 +8,8 @@ clean:
 
 .PHONY: all clean
 
-%.html: %.md
-	pandoc $< -o $@ --standalone --filter ./Filter.hs --bibliography=bibfile.bib --template ./template.html
+%.html: %.md Filter
+	pandoc $< -o $@ --standalone --filter ./Filter --bibliography=bibfile.bib --template ./template.html
 
+Filter: Filter.hs
+	ghc --make -O $<

bnf.html

@@ -114,9 +114,6 @@ <h1>TIP BNF</h1>
 terminator FunDec &quot;&quot;;
 
 position token Symbol (letter|[&quot;~!@$%^&amp;*_+=&lt;&gt;.?/&quot;])(letter|digit|[&quot;~!@$%^&amp;*_-+=&lt;&gt;.?/&quot;])*;</code></pre>
-<div class="references">
-
-</div>
 </div>
 </body>
 </html>

format.html

@@ -1,11 +1,12 @@
-(declare-datatypes (a)
-  ((list (nil) (cons (head a) (tail (list a))))))
-(define-funs-rec
-  ((par (a) (append ((xs (list a)) (ys (list a))) (list a))))
-  ((match xs
-     (case nil (as nil (list a)))
-     (case (cons x xs) (cons x (as (append xs ys) (list a)))))))
-(assert-not
+(declare-datatype
+  list
   (par (a)
-    (forall ((xs (list a))) (= (append xs (as nil (list a))) xs))))
-(check-sat)
+    ((nil) (cons (head a) (tail (list a))))))
+(define-fun-rec
+  append (par (a) (((xs (list a)) (ys (list a))) (list a)))
+  (match xs
+    ((nil (_ nil a))
+     ((cons x xs) (cons x (append xs ys))))))
+(prove
+  (par (a)
+    (forall ((xs (list a))) (= (append xs (_ nil a)) xs))))

list.smt2

@@ -1,13 +1,14 @@
-(declare-datatypes (a)
-  ((list (nil) (cons (head a) (tail (list a))))))
-(define-funs-rec
-  ((par (a b) (map2 ((f (=> a b)) (xs (list a))) (list b))))
-  ((match xs
-     (case nil (as nil (list b)))
-     (case (cons y ys) (cons (@ f y) (as (map2 f ys) (list b)))))))
-(assert-not
+(declare-datatype
+  list
+  (par (a)
+    ((nil) (cons (head a) (tail (list a))))))
+(define-fun-rec
+  map (par (a b) (((f (=> a b)) (xs (list a))) (list b)))
+  (match xs
+     ((nil (_ nil b))
+      ((cons y ys) (cons (@ f y) (map f ys))))))
+(prove
   (par (a b c)
     (forall ((f (=> b c)) (g (=> a b)) (xs (list a)))
-      (= (map2 (lambda ((x a)) (@ f (@ g x))) xs)
-        (map2 f (map2 g xs))))))
-(check-sat)
+      (= (map (lambda ((x a)) (@ f (@ g x))) xs)
+        (map f (map g xs))))))

map.smt2

@@ -1,8 +1,7 @@
-(declare-datatypes () ((Nat (Zero) (Succ (pred Nat)))))
-(define-funs-rec
-  ((plus ((x Nat) (y Nat)) Nat))
-  ((match x
-     (case Zero y)
-     (case default (Succ (plus (pred x) y))))))
-(assert-not (forall ((n Nat) (m Nat)) (= (plus n m) (plus m n))))
-(check-sat)
+(declare-datatype Nat ((Zero) (Succ (pred Nat))))
+(define-fun-rec
+  plus ((x Nat) (y Nat)) Nat
+  (match x
+    ((Zero y)
+     (default (Succ (plus (pred x) y))))))
+(prove (forall ((n Nat) (m Nat)) (= (plus n m) (plus m n))))

nat-default.smt2

@@ -1,8 +1,7 @@
-(declare-datatypes () ((Nat (Zero) (Succ (pred Nat)))))
-(define-funs-rec
-  ((plus ((x Nat) (y Nat)) Nat))
-  ((match x
-     (case Zero y)
-     (case (Succ n) (Succ (plus n y))))))
-(assert-not (forall ((n Nat) (m Nat)) (= (plus n m) (plus m n))))
-(check-sat)
+(declare-datatype Nat ((Zero) (Succ (pred Nat))))
+(define-fun-rec
+  plus ((x Nat) (y Nat)) Nat
+  (match x
+    ((Zero y)
+     ((Succ n) (Succ (plus n y))))))
+(prove (forall ((n Nat) (m Nat)) (= (plus n m) (plus m n))))