{-
# 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