{-
# ConfigHOL for beautifHOL, a HOL prettyprinter
# Based on the paper found at http://www.cs.indiana.edu/~lepike/pub_pages/pphol.html
# Lee Pike <lee-pike-@-gma-il-.com> (remove dashes)
# Jan 5, 2009
# Copyright 2008
# This file is part of beautifHOL.
# BSD3.
-}
module ConfigHOL where
-- Maximum lenght of a term before splitting it across lines.
maxArgLen :: Int
maxArgLen = 10
-- Output strings. Listed here as a list of strings for easy manipulation. DO
-- NOT CHANGE THE ORDER OF THE LIST! Most of the operators are obvious; ones
-- that are not are commented.
opStr :: [String]
opStr =
[ "true", "false", "=", "and", "or", "not", "implies", "forall", "exists"
, " " -- the space separator (" " for ASCII pretty-printing)
, "\n" -- the line-break operator
, "." -- the separator between variables after a quantifier and the sentence
, "," -- the separator between arguments to a function or predicate or let definitions
, "\n" -- prelude
, "\n" -- postlude
, "|" -- String to separate labels from the formula
, "if", "then", "else"
, "let", "in " -- complete HACK because the prter inserts spcs and these
-- are 1 spc apart. Okay for two.
]
------------
--
-- Below, the only thing to edit is to manually set some of the tab lengths for
-- the above operators if your output strings are to be comiled (e.g., for LaTeX
-- output, you might want to set the tab for forall to be 1 (rather than the
-- length of '\forall').
--
------------
trueStr, falseStr, eqStr, andStr, orStr, negStr, impStr, forallStr, existsStr :: String
spaceStr, brkStr, quantVarsMark, argSepStr, preStr, postStr, labelSepStr :: String
ifStr, thenStr, elseStr, letStr, inStr :: String
eqTab, andTab, orTab, negTab, impTab, forallTab, existsTab, ifTab, letTab :: Int
trueStr = opStr !! 0 --"true"
falseStr = opStr !! 1 --"false"
eqStr = opStr !! 2 --"="
andStr = opStr !! 3 --"and"
orStr = opStr !! 4 --"or"
negStr = opStr !! 5 --"not"
impStr = opStr !! 6 --"implies"
forallStr = opStr !! 7 --"forall"
existsStr = opStr !! 8 --"exists"
spaceStr = opStr !! 9 --" "
brkChar :: Char
brkChar = head $ opStr !! 10 --'\n'
brkStr = [brkChar]
quantVarsMark = opStr !! 11 --"."
argSepStr = opStr !! 12 --","
preStr = opStr !! 13
postStr = opStr !! 14
labelSepStr = opStr !! 15
ifStr = opStr !! 16
thenStr = opStr !! 17
elseStr = opStr !! 18
letStr = opStr !! 19
inStr = opStr !! 20
eqTab = length eqStr
andTab = length andStr
orTab = length orStr
negTab = length negStr
impTab = length impStr
forallTab = length forallStr
existsTab = length existsStr
ifTab = max (length ifStr) $ max (length thenStr) (length elseStr)
letTab = max (length letStr) (length inStr)
-- get filepath
-- check that the dir and file exist
-- open the file
-- parse it
-- return errors on bad parsing
-- set the constants
-- close the file