{- |
Module      :  ./CommonLogic/Print_KIF.hs
Description :  Pretty Printer for KIF
Copyright   :  (c) Soeren Schulze, Uni Bremen 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  s.schulze@uni-bremen.de
Stability   :  provisional
Portability :  portable

Pretty Printer for KIF.  Partially based on "pretty" instances in AS_CommonLogic.
Note that the output does not perfectly match the input, as CommonLogic does
not have the concept of "free variables" (as opposed to variables bound by a
quantifier).  Thus, any free variables are converted into constants and lose
their '?' prefix.  When CommonLogic code is emitted as KIF, the comments in
commented sentences and terms get lost, and modules are inlined.
-}

module CommonLogic.Print_KIF where

import Common.Id as Id
import Common.Doc
import Common.DocUtils
import Common.Keywords
import CommonLogic.ModuleElimination
import qualified CommonLogic.AS_CommonLogic as AS
import qualified Common.AS_Annotation as AS_Anno
import qualified Data.Set as Set

printBasicSpec :: AS.BASIC_SPEC -> Doc
printBasicSpec :: BASIC_SPEC -> Doc
printBasicSpec (AS.Basic_spec xs :: [Annoted BASIC_ITEMS]
xs) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted BASIC_ITEMS -> Doc) -> [Annoted BASIC_ITEMS] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((BASIC_ITEMS -> Doc) -> Annoted BASIC_ITEMS -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted BASIC_ITEMS -> Doc
printBasicItems) [Annoted BASIC_ITEMS]
xs

printBasicItems :: AS.BASIC_ITEMS -> Doc
printBasicItems :: BASIC_ITEMS -> Doc
printBasicItems (AS.Axiom_items xs :: [Annoted TEXT_META]
xs) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted TEXT_META -> Doc) -> [Annoted TEXT_META] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((TEXT_META -> Doc) -> Annoted TEXT_META -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted TEXT_META -> Doc
printTextMeta) [Annoted TEXT_META]
xs

printTextMeta :: AS.TEXT_META -> Doc
printTextMeta :: TEXT_META -> Doc
printTextMeta tm :: TEXT_META
tm = TEXT -> Doc
printText (TEXT -> Doc) -> TEXT -> Doc
forall a b. (a -> b) -> a -> b
$ TEXT_META -> TEXT
AS.getText (TEXT_META -> TEXT) -> TEXT_META -> TEXT
forall a b. (a -> b) -> a -> b
$ TEXT_META -> TEXT_META
eliminateModules TEXT_META
tm

exportKIF :: [AS_Anno.Named AS.TEXT_META] -> Doc
exportKIF :: [Named TEXT_META] -> Doc
exportKIF xs :: [Named TEXT_META]
xs = [Doc] -> Doc
vsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Named TEXT_META -> Doc) -> [Named TEXT_META] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (TEXT_META -> Doc
printTextMeta (TEXT_META -> Doc)
-> (Named TEXT_META -> TEXT_META) -> Named TEXT_META -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named TEXT_META -> TEXT_META
forall s a. SenAttr s a -> s
AS_Anno.sentence) [Named TEXT_META]
xs

printText :: AS.TEXT -> Doc
printText :: TEXT -> Doc
printText s :: TEXT
s = case TEXT
s of
  AS.Text x :: [PHRASE]
x _ -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (PHRASE -> Doc) -> [PHRASE] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PHRASE -> Doc
printPhrase [PHRASE]
x
  AS.Named_text _ x :: TEXT
x _ -> TEXT -> Doc
printText TEXT
x

printPhrase :: AS.PHRASE -> Doc
printPhrase :: PHRASE -> Doc
printPhrase s :: PHRASE
s = case PHRASE
s of
  AS.Module _ -> [Char] -> Doc
forall a. HasCallStack => [Char] -> a
error "printPhrase: \"module\" found"
  AS.Sentence x :: SENTENCE
x -> Set [Char] -> SENTENCE -> Doc
printSentence Set [Char]
forall a. Set a
Set.empty SENTENCE
x
  AS.Importation _ -> [Char] -> Doc
forall a. HasCallStack => [Char] -> a
error "printPhrase: \"import\" found"
  AS.Comment_text _ t :: TEXT
t _ -> TEXT -> Doc
printText TEXT
t

printQuant :: AS.QUANT -> Doc
printQuant :: QUANT -> Doc
printQuant = QUANT -> Doc
AS.printQuant

printAndOr :: AS.AndOr -> Doc
printAndOr :: AndOr -> Doc
printAndOr = AndOr -> Doc
AS.printAndOr

printImplEq :: AS.ImplEq -> Doc
printImplEq :: ImplEq -> Doc
printImplEq s :: ImplEq
s = case ImplEq
s of
  AS.Implication -> [Char] -> Doc
text [Char]
implS
  AS.Biconditional -> [Char] -> Doc
text [Char]
equivS

getQuantVarName :: AS.NAME_OR_SEQMARK -> String
getQuantVarName :: NAME_OR_SEQMARK -> [Char]
getQuantVarName v :: NAME_OR_SEQMARK
v = [Char] -> [Char]
stripVar ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Token -> [Char]
tokStr (Token -> [Char]) -> Token -> [Char]
forall a b. (a -> b) -> a -> b
$ case NAME_OR_SEQMARK
v of
  AS.Name x :: Token
x -> Token
x
  AS.SeqMark x :: Token
x -> Token
x

{- The "bv" argument contains a set of variables that are bound by quantifiers.
These variables are prepended by a '?' sign when printed.
Sequence markers are always prepended by '@', without checking if they
are bounded. -}

printSentence :: Set.Set String -> AS.SENTENCE -> Doc
printSentence :: Set [Char] -> SENTENCE -> Doc
printSentence bv :: Set [Char]
bv s :: SENTENCE
s = case SENTENCE
s of
  AS.Quant_sent q :: QUANT
q vs :: [NAME_OR_SEQMARK]
vs is :: SENTENCE
is _ ->
    Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ QUANT -> Doc
printQuant QUANT
q Doc -> Doc -> Doc
<+> Doc -> Doc
parens ([Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (NAME_OR_SEQMARK -> Doc) -> [NAME_OR_SEQMARK] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Set [Char] -> NAME_OR_SEQMARK -> Doc
printNameOrSeqMark Set [Char]
bv') [NAME_OR_SEQMARK]
vs) Doc -> Doc -> Doc
<+>
    Set [Char] -> SENTENCE -> Doc
printSentence Set [Char]
bv' SENTENCE
is
    where bv' :: Set [Char]
bv' = Set [Char] -> Set [Char] -> Set [Char]
forall a. Ord a => Set a -> Set a -> Set a
Set.union ([[Char]] -> Set [Char]
forall a. Ord a => [a] -> Set a
Set.fromList ([[Char]] -> Set [Char]) -> [[Char]] -> Set [Char]
forall a b. (a -> b) -> a -> b
$ (NAME_OR_SEQMARK -> [Char]) -> [NAME_OR_SEQMARK] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map NAME_OR_SEQMARK -> [Char]
getQuantVarName [NAME_OR_SEQMARK]
vs) Set [Char]
bv
  AS.Bool_sent xs :: BOOL_SENT
xs _ -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Set [Char] -> BOOL_SENT -> Doc
printBoolSent Set [Char]
bv BOOL_SENT
xs
  AS.Atom_sent xs :: ATOM
xs _ -> Set [Char] -> ATOM -> Doc
printAtom Set [Char]
bv ATOM
xs
  AS.Comment_sent _ y :: SENTENCE
y _ -> Set [Char] -> SENTENCE -> Doc
printSentence Set [Char]
bv SENTENCE
y
  AS.Irregular_sent xs :: SENTENCE
xs _ -> Set [Char] -> SENTENCE -> Doc
printSentence Set [Char]
bv SENTENCE
xs

printBoolSent :: Set.Set String -> AS.BOOL_SENT -> Doc
printBoolSent :: Set [Char] -> BOOL_SENT -> Doc
printBoolSent bv :: Set [Char]
bv s :: BOOL_SENT
s = case BOOL_SENT
s of
  AS.Junction q :: AndOr
q xs :: [SENTENCE]
xs -> AndOr -> Doc
printAndOr AndOr
q Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((SENTENCE -> Doc) -> [SENTENCE] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Set [Char] -> SENTENCE -> Doc
printSentence Set [Char]
bv) [SENTENCE]
xs)
  AS.Negation xs :: SENTENCE
xs -> [Char] -> Doc
text [Char]
notS Doc -> Doc -> Doc
<+> Set [Char] -> SENTENCE -> Doc
printSentence Set [Char]
bv SENTENCE
xs
  AS.BinOp q :: ImplEq
q x :: SENTENCE
x y :: SENTENCE
y -> ImplEq -> Doc
printImplEq ImplEq
q Doc -> Doc -> Doc
<+> Set [Char] -> SENTENCE -> Doc
printSentence Set [Char]
bv SENTENCE
x Doc -> Doc -> Doc
<+> Set [Char] -> SENTENCE -> Doc
printSentence Set [Char]
bv SENTENCE
y

printAtom :: Set.Set String -> AS.ATOM -> Doc
printAtom :: Set [Char] -> ATOM -> Doc
printAtom bv :: Set [Char]
bv s :: ATOM
s = case ATOM
s of
  AS.Equation a :: TERM
a b :: TERM
b -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
equals Doc -> Doc -> Doc
<+> Set [Char] -> TERM -> Doc
printTerm Set [Char]
bv TERM
a Doc -> Doc -> Doc
<+> Set [Char] -> TERM -> Doc
printTerm Set [Char]
bv TERM
b
  AS.Atom t :: TERM
t [] -> Set [Char] -> TERM -> Doc
printTerm Set [Char]
bv TERM
t
  AS.Atom t :: TERM
t ts :: [TERM_SEQ]
ts -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Set [Char] -> TERM -> Doc
printTerm Set [Char]
bv TERM
t Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep ((TERM_SEQ -> Doc) -> [TERM_SEQ] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Set [Char] -> TERM_SEQ -> Doc
printTermSeq Set [Char]
bv) [TERM_SEQ]
ts)

stripVar :: String -> String
stripVar :: [Char] -> [Char]
stripVar = (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> [Char] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "?@.")

printName :: Set.Set String -> AS.NAME -> Doc
printName :: Set [Char] -> Token -> Doc
printName bv :: Set [Char]
bv name :: Token
name = [Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ if [Char] -> Set [Char] -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member [Char]
cleanName Set [Char]
bv
                           then '?' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char]
cleanName
                           else [Char]
cleanName
  where cleanName :: [Char]
cleanName = [Char] -> [Char]
stripVar ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Token -> [Char]
tokStr Token
name

printRowVar :: Token -> Doc
printRowVar :: Token -> Doc
printRowVar name :: Token
name = [Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ '@' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char]
stripVar (Token -> [Char]
tokStr Token
name)

printTerm :: Set.Set String -> AS.TERM -> Doc
printTerm :: Set [Char] -> TERM -> Doc
printTerm bv :: Set [Char]
bv s :: TERM
s = case TERM
s of
  AS.Name_term a :: Token
a -> Set [Char] -> Token -> Doc
printName Set [Char]
bv Token
a
  AS.Funct_term t :: TERM
t ts :: [TERM_SEQ]
ts _ -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Set [Char] -> TERM -> Doc
printTerm Set [Char]
bv TERM
t
                          Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep ((TERM_SEQ -> Doc) -> [TERM_SEQ] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Set [Char] -> TERM_SEQ -> Doc
printTermSeq Set [Char]
bv) [TERM_SEQ]
ts)
  AS.Comment_term t :: TERM
t _ _ -> Set [Char] -> TERM -> Doc
printTerm Set [Char]
bv TERM
t
  AS.That_term sent :: SENTENCE
sent _ -> Set [Char] -> SENTENCE -> Doc
printSentence Set [Char]
bv SENTENCE
sent

printTermSeq :: Set.Set String -> AS.TERM_SEQ -> Doc
printTermSeq :: Set [Char] -> TERM_SEQ -> Doc
printTermSeq bv :: Set [Char]
bv s :: TERM_SEQ
s = case TERM_SEQ
s of
  AS.Term_seq t :: TERM
t -> Set [Char] -> TERM -> Doc
printTerm Set [Char]
bv TERM
t
  AS.Seq_marks m :: Token
m -> Token -> Doc
printRowVar Token
m

printNameOrSeqMark :: Set.Set String -> AS.NAME_OR_SEQMARK -> Doc
printNameOrSeqMark :: Set [Char] -> NAME_OR_SEQMARK -> Doc
printNameOrSeqMark bv :: Set [Char]
bv s :: NAME_OR_SEQMARK
s = case NAME_OR_SEQMARK
s of
  AS.Name x :: Token
x -> Set [Char] -> Token -> Doc
printName Set [Char]
bv Token
x
  AS.SeqMark x :: Token
x -> Token -> Doc
printRowVar Token
x