module PrSequent where import PrelSequent import Sequent -- printing sequent calculus. AR 4/4/1999 -- 14/4 -- printing in ASCII prSequent :: Sequent -> String prSequent (ant,suc) = prTList ", " (map (prFormula 1) ant) +++ "=>" +++ prTList ", " (map (prFormula 1) (reverse suc)) prFormula n f = case f of Scheme i terms -> i ++ prArgList (map prTerm terms) Predic p [x,y] | infixPredicate p -> prTerm x +++ p +++ prTerm y Predic p terms -> p ++ prArgList (map prTerm terms) Falsum -> "_|_" Neg a -> "~" +++ prf 3 a Conj a b -> parIf 2 (prf 3 a +++ "&" +++ prf 3 b) Disj a b -> parIf 2 (prf 3 a +++ "v" +++ prf 3 b) Impl a b -> parIf 1 (prf 2 a +++ "->" +++ prf 2 b) Univ x a -> "(" ++ "/A" ++ x ++ ")" ++ prf 3 a Exist x a -> "(" ++ "/E" ++ x ++ ")" ++ prf 3 a where parIf k s = if n > k then "(" ++ s ++ ")" else s prf = prFormula prTerm t = case t of Var x -> x Meta c -> c NewMeta c -> c Apply f [x,y] | infixFunction f -> prTerm x +++ f +++ prTerm y Apply f tt -> f ++ prArgList (map prTerm tt) prProof = prProofNodes False prProofNodes sh tree = foldr1 lined (map prLine layers) ++ prParams where --- layers = [[prSeqn sh n s | ((n,s),_) <- nodesOfProof tree, length n == ht-k] | k <- [0 .. ht-1]] prSeqn sh n s = (if sh then ((concat (map show n))+++) else id) (prSequent s) ht = htProof tree prLine ss = foldr1 (\x y -> x ++ " " ++ y) ss lined x y = x ++++ replicate (length x) '-' ++++ y prParams = let pp = paramsOfProof tree in case pp of [] -> "" _ -> "\n\nParameters" +++ foldr1 (+++) pp --------- prGoals goals = foldr (++++) "" (map prGoal goals) where prGoal (Left (ints,sequent)) = prGoalId ints +++ "=" +++ prSequent sequent prGoal (Right par) = par +++ "=" +++ "?" prGoalId n = foldl1 (++) (map show n) -- works for 1..9 only --------------------------------------------------- -- printing in LaTeX -- printing proof trees as LaTeX files prLatexProof proof = prLatexFile ("\$" ++++ prProof proof ++++ "\$") where prProof (Goal seq) = makeLatex (prSequent seq ++ "^{??}") prProof (Param c) = makeLatex (c +++ "= ?") prProof (Proof ident seq []) = "\\infer{" ++++ makeLatex (prSequent seq) ++++ "}{" ++ makeLatex ident ++ "}" -- makeLatex (prSequent seq ++ "^{" ++ ident ++"}") -- axiom without line prProof (Proof ident seq proofs) = "\\infer[{\\scriptstyle" +++ makeLatex ident ++ "}]{" ++++ makeLatex (prSequent seq) ++++ "}{" ++++ prTList "\n & \n" (map prProof proofs) ++++ "}" prLatexFormula n f = makeLatex (prFormula n f) prLatexFile string = "\\documentstyle[proof]{article}" ++++ "\\setlength{\\parskip}{2mm}" ++++ "\\setlength{\\parindent}{0mm}" ++++ --- "\\newcommand{\\discharge}[2]{\\stackrel {#1. \\ }{[ #2 ]}}" ++++ -- JvP's "\\newcommand{\\discharge}[2]{\\begin{array}[b]{c} #1 \\\\ #2 \\end{array}}" ++++ "\\begin{document}" ++++ string ++++ "\\end{document}" makeLatex s = case s of '_':'|':'_':t -> "\\bot" +++ makeLatex t '~' :t -> "\\sim" +++ makeLatex t '&' :t -> "\\&" +++ makeLatex t ' ':'v':' ':t -> " \\vee" +++ makeLatex t '-':'>' :t -> "\\supset" +++ makeLatex t '=':'>' :t -> "\\Rightarrow" +++ makeLatex t '/':'A' :t -> "\\forall" +++ makeLatex t '/':'E' :t -> "\\exists" +++ makeLatex t 'G':'a':'m':'m':'a':t -> "\\Gamma" +++ makeLatex t 'D':'e':'l':'t':'a':t -> "\\Delta" +++ makeLatex t '#' :t -> "\\#" +++ makeLatex t c :t -> c : makeLatex t [] -> [] -- auxiliary operations prTList t ss = case ss of [] -> "" [s] -> s s:ss -> s ++ t ++ prTList t ss prArgList tt = case tt of [] -> "" _ -> "(" ++ prTList "," tt ++ ")"