{- |
Module      :  ./CASL/ToDoc.hs
Description :  pretty printing data types of BASIC_SPEC
Copyright   :  (c) Christian Maeder and Uni Bremen 2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

Pretty printing data types of 'BASIC_SPEC'
-}

module CASL.ToDoc
    ( printBASIC_SPEC
    , printFormula
    , printTerm
    , printTheoryFormula
    , pluralS_symb_list
    , pluralS
    , appendS
    , isJunct
    , printInfix
    , ListCheck (..)
    , recoverType
    , printALTERNATIVE
    , typeString
    , printVarDecl
    , printVarDeclL
    , printVarDecls
    , printOptArgDecls
    , printSortItem
    , printOpItem
    , printPredItem
    , printPredHead
    , printRecord
    , printAttr
    , printAnnotedBulletFormulas
    , FormExtension (..)
    , isQuant
    ) where

import Common.Id
import Common.Keywords
import Common.Doc
import Common.DocUtils
import Common.AS_Annotation

import CASL.AS_Basic_CASL
import CASL.Fold

instance (Pretty b, Pretty s, FormExtension f) => Pretty (BASIC_SPEC b s f)
  where pretty :: BASIC_SPEC b s f -> Doc
pretty = (b -> Doc) -> (s -> Doc) -> BASIC_SPEC b s f -> Doc
forall f b s.
FormExtension f =>
(b -> Doc) -> (s -> Doc) -> BASIC_SPEC b s f -> Doc
printBASIC_SPEC b -> Doc
forall a. Pretty a => a -> Doc
pretty s -> Doc
forall a. Pretty a => a -> Doc
pretty

printBASIC_SPEC :: FormExtension f => (b -> Doc) -> (s -> Doc)
                -> BASIC_SPEC b s f -> Doc
printBASIC_SPEC :: (b -> Doc) -> (s -> Doc) -> BASIC_SPEC b s f -> Doc
printBASIC_SPEC fB :: b -> Doc
fB fS :: s -> Doc
fS (Basic_spec l :: [Annoted (BASIC_ITEMS b s f)]
l) = case [Annoted (BASIC_ITEMS b s f)]
l of
    [] -> Doc -> Doc
specBraces Doc
empty
    _ -> [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted (BASIC_ITEMS b s f) -> Doc)
-> [Annoted (BASIC_ITEMS b s f)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((BASIC_ITEMS b s f -> Doc) -> Annoted (BASIC_ITEMS b s f) -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted ((b -> Doc) -> (s -> Doc) -> BASIC_ITEMS b s f -> Doc
forall f b s.
FormExtension f =>
(b -> Doc) -> (s -> Doc) -> BASIC_ITEMS b s f -> Doc
printBASIC_ITEMS b -> Doc
fB s -> Doc
fS)) [Annoted (BASIC_ITEMS b s f)]
l

instance (Pretty b, Pretty s, FormExtension f) => Pretty (BASIC_ITEMS b s f)
  where pretty :: BASIC_ITEMS b s f -> Doc
pretty = (b -> Doc) -> (s -> Doc) -> BASIC_ITEMS b s f -> Doc
forall f b s.
FormExtension f =>
(b -> Doc) -> (s -> Doc) -> BASIC_ITEMS b s f -> Doc
printBASIC_ITEMS b -> Doc
forall a. Pretty a => a -> Doc
pretty s -> Doc
forall a. Pretty a => a -> Doc
pretty

typeString :: SortsKind -> [Annoted DATATYPE_DECL] -> String
typeString :: SortsKind -> [Annoted DATATYPE_DECL] -> String
typeString sk :: SortsKind
sk l :: [Annoted DATATYPE_DECL]
l = (case SortsKind
sk of
    NonEmptySorts -> String
typeS
    PossiblyEmptySorts -> String
etypeS) String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Annoted DATATYPE_DECL] -> String
forall a. [a] -> String
appendS [Annoted DATATYPE_DECL]
l

printBASIC_ITEMS :: FormExtension f => (b -> Doc) -> (s -> Doc)
                 -> BASIC_ITEMS b s f -> Doc
printBASIC_ITEMS :: (b -> Doc) -> (s -> Doc) -> BASIC_ITEMS b s f -> Doc
printBASIC_ITEMS fB :: b -> Doc
fB fS :: s -> Doc
fS sis :: BASIC_ITEMS b s f
sis = case BASIC_ITEMS b s f
sis of
    Sig_items s :: SIG_ITEMS s f
s -> (s -> Doc) -> SIG_ITEMS s f -> Doc
forall f s. FormExtension f => (s -> Doc) -> SIG_ITEMS s f -> Doc
printSIG_ITEMS s -> Doc
fS SIG_ITEMS s f
s
    Free_datatype sk :: SortsKind
sk l :: [Annoted DATATYPE_DECL]
l _ -> [Doc] -> Doc
sep [String -> Doc
keyword String
freeS Doc -> Doc -> Doc
<+> String -> Doc
keyword (SortsKind -> [Annoted DATATYPE_DECL] -> String
typeString SortsKind
sk [Annoted DATATYPE_DECL]
l),
                                 (DATATYPE_DECL -> Doc) -> [Annoted DATATYPE_DECL] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos DATATYPE_DECL -> Doc
printDATATYPE_DECL [Annoted DATATYPE_DECL]
l]
    Sort_gen l :: [Annoted (SIG_ITEMS s f)]
l _ -> case [Annoted (SIG_ITEMS s f)]
l of
         [Annoted (Datatype_items sk :: SortsKind
sk l' :: [Annoted DATATYPE_DECL]
l' _) _ las :: [Annotation]
las ras :: [Annotation]
ras] ->
             (if [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annotation]
las then Doc -> Doc
forall a. a -> a
id else ([Annotation] -> Doc
printAnnotationList [Annotation]
las Doc -> Doc -> Doc
$+$))
             (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (if [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annotation]
ras then Doc -> Doc
forall a. a -> a
id else (Doc -> Doc -> Doc
$+$ [Annotation] -> Doc
printAnnotationList [Annotation]
ras))
             (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [String -> Doc
keyword String
generatedS Doc -> Doc -> Doc
<+> String -> Doc
keyword (SortsKind -> [Annoted DATATYPE_DECL] -> String
typeString SortsKind
sk [Annoted DATATYPE_DECL]
l'),
                    (DATATYPE_DECL -> Doc) -> [Annoted DATATYPE_DECL] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos DATATYPE_DECL -> Doc
printDATATYPE_DECL [Annoted DATATYPE_DECL]
l']
         _ -> [Doc] -> Doc
sep [String -> Doc
keyword String
generatedS, Doc -> Doc
specBraces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted (SIG_ITEMS s f) -> Doc)
-> [Annoted (SIG_ITEMS s f)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map
              ((SIG_ITEMS s f -> Doc) -> Annoted (SIG_ITEMS s f) -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted ((SIG_ITEMS s f -> Doc) -> Annoted (SIG_ITEMS s f) -> Doc)
-> (SIG_ITEMS s f -> Doc) -> Annoted (SIG_ITEMS s f) -> Doc
forall a b. (a -> b) -> a -> b
$ (s -> Doc) -> SIG_ITEMS s f -> Doc
forall f s. FormExtension f => (s -> Doc) -> SIG_ITEMS s f -> Doc
printSIG_ITEMS s -> Doc
fS) [Annoted (SIG_ITEMS s f)]
l]
    Var_items l :: [VAR_DECL]
l _ -> String -> Doc
topSigKey (String
varS String -> String -> String
forall a. [a] -> [a] -> [a]
++ [VAR_DECL] -> String
forall a. ListCheck a => a -> String
pluralS [VAR_DECL]
l) Doc -> Doc -> Doc
<+> [VAR_DECL] -> Doc
printVarDecls [VAR_DECL]
l
    Local_var_axioms l :: [VAR_DECL]
l f :: [Annoted (FORMULA f)]
f _ ->
            [Doc] -> Doc
fsep [[Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
forallDoc Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [VAR_DECL] -> [Doc]
printVarDeclL [VAR_DECL]
l
                 , [Annoted (FORMULA f)] -> Doc
forall f. FormExtension f => [Annoted (FORMULA f)] -> Doc
printAnnotedBulletFormulas [Annoted (FORMULA f)]
f]
    Axiom_items f :: [Annoted (FORMULA f)]
f _ -> [Annoted (FORMULA f)] -> Doc
forall f. FormExtension f => [Annoted (FORMULA f)] -> Doc
printAnnotedBulletFormulas [Annoted (FORMULA f)]
f
    Ext_BASIC_ITEMS b :: b
b -> b -> Doc
fB b
b

printAnnotedBulletFormulas :: FormExtension f => [Annoted (FORMULA f)] -> Doc
printAnnotedBulletFormulas :: [Annoted (FORMULA f)] -> Doc
printAnnotedBulletFormulas l :: [Annoted (FORMULA f)]
l = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ case [Annoted (FORMULA f)]
l of
    [] -> []
    _ -> let pp :: FORMULA f -> Doc
pp = Doc -> Doc
addBullet (Doc -> Doc) -> (FORMULA f -> Doc) -> FORMULA f -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> Doc
forall f. FormExtension f => FORMULA f -> Doc
printFormula in
         (Annoted (FORMULA f) -> Doc) -> [Annoted (FORMULA f)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f -> Doc) -> Annoted (FORMULA f) -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted FORMULA f -> Doc
pp) ([Annoted (FORMULA f)] -> [Annoted (FORMULA f)]
forall a. [a] -> [a]
init [Annoted (FORMULA f)]
l)
         [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [(FORMULA f -> Doc) -> Bool -> Annoted (FORMULA f) -> Doc
forall a. (a -> Doc) -> Bool -> Annoted a -> Doc
printSemiAnno FORMULA f -> Doc
pp Bool
False (Annoted (FORMULA f) -> Doc) -> Annoted (FORMULA f) -> Doc
forall a b. (a -> b) -> a -> b
$ [Annoted (FORMULA f)] -> Annoted (FORMULA f)
forall a. [a] -> a
last [Annoted (FORMULA f)]
l] -- use True for HasCASL

instance (Pretty s, FormExtension f) => Pretty (SIG_ITEMS s f) where
    pretty :: SIG_ITEMS s f -> Doc
pretty = (s -> Doc) -> SIG_ITEMS s f -> Doc
forall f s. FormExtension f => (s -> Doc) -> SIG_ITEMS s f -> Doc
printSIG_ITEMS s -> Doc
forall a. Pretty a => a -> Doc
pretty

printSIG_ITEMS :: FormExtension f => (s -> Doc) -> SIG_ITEMS s f -> Doc
printSIG_ITEMS :: (s -> Doc) -> SIG_ITEMS s f -> Doc
printSIG_ITEMS fS :: s -> Doc
fS sis :: SIG_ITEMS s f
sis = case SIG_ITEMS s f
sis of
    Sort_items sk :: SortsKind
sk l :: [Annoted (SORT_ITEM f)]
l _ -> String -> Doc
topSigKey ((case SortsKind
sk of
        NonEmptySorts -> String
sortS
        PossiblyEmptySorts -> String
esortS) String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Annoted (SORT_ITEM f)] -> String
forall a. ListCheck a => a -> String
pluralS [Annoted (SORT_ITEM f)]
l) Doc -> Doc -> Doc
<+>
         (SORT_ITEM f -> Doc) -> [Annoted (SORT_ITEM f)] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos SORT_ITEM f -> Doc
forall f. FormExtension f => SORT_ITEM f -> Doc
printSortItem [Annoted (SORT_ITEM f)]
l
    Op_items l :: [Annoted (OP_ITEM f)]
l _ -> String -> Doc
topSigKey (String
opS String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Annoted (OP_ITEM f)] -> String
forall a. ListCheck a => a -> String
pluralS [Annoted (OP_ITEM f)]
l) Doc -> Doc -> Doc
<+>
        let pp :: OP_ITEM f -> Doc
pp = OP_ITEM f -> Doc
forall f. FormExtension f => OP_ITEM f -> Doc
printOpItem in
        if [Annoted (OP_ITEM f)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted (OP_ITEM f)]
l then Doc
empty else if case Annoted (OP_ITEM f) -> OP_ITEM f
forall a. Annoted a -> a
item (Annoted (OP_ITEM f) -> OP_ITEM f)
-> Annoted (OP_ITEM f) -> OP_ITEM f
forall a b. (a -> b) -> a -> b
$ [Annoted (OP_ITEM f)] -> Annoted (OP_ITEM f)
forall a. [a] -> a
last [Annoted (OP_ITEM f)]
l of
            Op_decl _ _ a :: [OP_ATTR f]
a@(_ : _) _ -> case [OP_ATTR f] -> OP_ATTR f
forall a. [a] -> a
last [OP_ATTR f]
a of
                Unit_op_attr {} -> Bool
False  -- use True for HasCASL
                _ -> Bool
False
            Op_defn {} -> Bool
False  -- use True for HasCASL
            _ -> Bool
False
        then [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted (OP_ITEM f) -> Doc) -> [Annoted (OP_ITEM f)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((OP_ITEM f -> Doc) -> Bool -> Annoted (OP_ITEM f) -> Doc
forall a. (a -> Doc) -> Bool -> Annoted a -> Doc
printSemiAnno OP_ITEM f -> Doc
pp Bool
True) [Annoted (OP_ITEM f)]
l else (OP_ITEM f -> Doc) -> [Annoted (OP_ITEM f)] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos OP_ITEM f -> Doc
pp [Annoted (OP_ITEM f)]
l
    Pred_items l :: [Annoted (PRED_ITEM f)]
l _ -> String -> Doc
topSigKey (String
predS String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Annoted (PRED_ITEM f)] -> String
forall a. ListCheck a => a -> String
pluralS [Annoted (PRED_ITEM f)]
l) Doc -> Doc -> Doc
<+>
        let pp :: PRED_ITEM f -> Doc
pp = PRED_ITEM f -> Doc
forall f. FormExtension f => PRED_ITEM f -> Doc
printPredItem in
        if [Annoted (PRED_ITEM f)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted (PRED_ITEM f)]
l then Doc
empty else if case Annoted (PRED_ITEM f) -> PRED_ITEM f
forall a. Annoted a -> a
item (Annoted (PRED_ITEM f) -> PRED_ITEM f)
-> Annoted (PRED_ITEM f) -> PRED_ITEM f
forall a b. (a -> b) -> a -> b
$ [Annoted (PRED_ITEM f)] -> Annoted (PRED_ITEM f)
forall a. [a] -> a
last [Annoted (PRED_ITEM f)]
l of
            Pred_defn {} -> Bool
True
            _ -> Bool
False
        then [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Annoted (PRED_ITEM f) -> Doc) -> [Annoted (PRED_ITEM f)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((PRED_ITEM f -> Doc) -> Bool -> Annoted (PRED_ITEM f) -> Doc
forall a. (a -> Doc) -> Bool -> Annoted a -> Doc
printSemiAnno PRED_ITEM f -> Doc
pp Bool
True) [Annoted (PRED_ITEM f)]
l else (PRED_ITEM f -> Doc) -> [Annoted (PRED_ITEM f)] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos PRED_ITEM f -> Doc
pp [Annoted (PRED_ITEM f)]
l
    Datatype_items sk :: SortsKind
sk l :: [Annoted DATATYPE_DECL]
l _ -> String -> Doc
topSigKey (SortsKind -> [Annoted DATATYPE_DECL] -> String
typeString SortsKind
sk [Annoted DATATYPE_DECL]
l) Doc -> Doc -> Doc
<+>
             (DATATYPE_DECL -> Doc) -> [Annoted DATATYPE_DECL] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos DATATYPE_DECL -> Doc
printDATATYPE_DECL [Annoted DATATYPE_DECL]
l
    Ext_SIG_ITEMS s :: s
s -> s -> Doc
fS s
s

printDATATYPE_DECL :: DATATYPE_DECL -> Doc
printDATATYPE_DECL :: DATATYPE_DECL -> Doc
printDATATYPE_DECL (Datatype_decl s :: SORT
s a :: [Annoted ALTERNATIVE]
a r :: Range
r) =
    let pa :: Annoted ALTERNATIVE -> Doc
pa = (ALTERNATIVE -> Doc) -> Annoted ALTERNATIVE -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted ALTERNATIVE -> Doc
printALTERNATIVE in case [Annoted ALTERNATIVE]
a of
    [] -> DATATYPE_DECL -> Doc
printDATATYPE_DECL (SORT -> [Annoted ALTERNATIVE] -> Range -> DATATYPE_DECL
Datatype_decl SORT
s [ALTERNATIVE -> Annoted ALTERNATIVE
forall a. a -> Annoted a
emptyAnno (ALTERNATIVE -> Annoted ALTERNATIVE)
-> ALTERNATIVE -> Annoted ALTERNATIVE
forall a b. (a -> b) -> a -> b
$ [SORT] -> Range -> ALTERNATIVE
Subsorts [SORT
s] Range
r] Range
r)
    h :: Annoted ALTERNATIVE
h : t :: [Annoted ALTERNATIVE]
t -> [Doc] -> Doc
sep [SORT -> Doc
idLabelDoc SORT
s, Doc
colon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
sep
                      ((Doc
equals Doc -> Doc -> Doc
<+> Annoted ALTERNATIVE -> Doc
pa Annoted ALTERNATIVE
h) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
                       (Annoted ALTERNATIVE -> Doc) -> [Annoted ALTERNATIVE] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc
bar Doc -> Doc -> Doc
<+>) (Doc -> Doc)
-> (Annoted ALTERNATIVE -> Doc) -> Annoted ALTERNATIVE -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted ALTERNATIVE -> Doc
pa) [Annoted ALTERNATIVE]
t)]

instance Pretty DATATYPE_DECL where
    pretty :: DATATYPE_DECL -> Doc
pretty = DATATYPE_DECL -> Doc
printDATATYPE_DECL

printCOMPONENTS :: COMPONENTS -> Doc
printCOMPONENTS :: COMPONENTS -> Doc
printCOMPONENTS c :: COMPONENTS
c = case COMPONENTS
c of
    Cons_select k :: OpKind
k l :: [SORT]
l s :: SORT
s _ -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((SORT -> Doc) -> [SORT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Doc
idLabelDoc [SORT]
l)
           [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [case OpKind
k of
           Total -> Doc
colon
           Partial -> Doc
colon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
quMarkD, SORT -> Doc
idDoc SORT
s]
    Sort s :: SORT
s -> SORT -> Doc
idDoc SORT
s

instance Pretty COMPONENTS where
    pretty :: COMPONENTS -> Doc
pretty = COMPONENTS -> Doc
printCOMPONENTS

printALTERNATIVE :: ALTERNATIVE -> Doc
printALTERNATIVE :: ALTERNATIVE -> Doc
printALTERNATIVE a :: ALTERNATIVE
a = case ALTERNATIVE
a of
  Alt_construct k :: OpKind
k n :: SORT
n l :: [COMPONENTS]
l _ -> case [COMPONENTS]
l of
    [] -> SORT -> Doc
idLabelDoc SORT
n
    _ -> SORT -> Doc
idLabelDoc SORT
n Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
       Doc -> Doc
parens ( [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
semi ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (COMPONENTS -> Doc) -> [COMPONENTS] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map COMPONENTS -> Doc
printCOMPONENTS [COMPONENTS]
l)
       Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> case OpKind
k of
               Total -> Doc
empty
               Partial -> Doc
quMarkD
  Subsorts l :: [SORT]
l _ -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String
sortS String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SORT] -> String
forall a. ListCheck a => a -> String
pluralS [SORT]
l)
                            Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((SORT -> Doc) -> [SORT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Doc
idDoc [SORT]
l)

instance Pretty ALTERNATIVE where
    pretty :: ALTERNATIVE -> Doc
pretty = ALTERNATIVE -> Doc
printALTERNATIVE

printSortItem :: FormExtension f => SORT_ITEM f -> Doc
printSortItem :: SORT_ITEM f -> Doc
printSortItem si :: SORT_ITEM f
si = case SORT_ITEM f
si of
    Sort_decl sl :: [SORT]
sl _ -> [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (SORT -> Doc) -> [SORT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Doc
idLabelDoc [SORT]
sl
    Subsort_decl sl :: [SORT]
sl sup :: SORT
sup _ ->
        [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((SORT -> Doc) -> [SORT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Doc
idDoc [SORT]
sl) [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
less, SORT -> Doc
idDoc SORT
sup]
    Subsort_defn s :: SORT
s v :: VAR
v sup :: SORT
sup af :: Annoted (FORMULA f)
af _ -> [Doc] -> Doc
fsep [SORT -> Doc
idLabelDoc SORT
s, Doc
equals,
              Doc -> Doc
specBraces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep [VAR -> Doc
sidDoc VAR
v, Doc
colon Doc -> Doc -> Doc
<+> SORT -> Doc
idDoc SORT
sup,
                             (FORMULA f -> Doc) -> Annoted (FORMULA f) -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted (Doc -> Doc
addBullet (Doc -> Doc) -> (FORMULA f -> Doc) -> FORMULA f -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> Doc
forall f. FormExtension f => FORMULA f -> Doc
printFormula) Annoted (FORMULA f)
af]]
    Iso_decl sl :: [SORT]
sl _ -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate (Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
equals) ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (SORT -> Doc) -> [SORT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Doc
idDoc [SORT]
sl

instance FormExtension f => Pretty (SORT_ITEM f) where
    pretty :: SORT_ITEM f -> Doc
pretty = SORT_ITEM f -> Doc
forall f. FormExtension f => SORT_ITEM f -> Doc
printSortItem

printQuant :: QUANTIFIER -> Doc
printQuant :: QUANTIFIER -> Doc
printQuant q :: QUANTIFIER
q = case QUANTIFIER
q of
    Universal -> Doc
forallDoc
    Existential -> Doc
exists
    Unique_existential -> Doc
unique

printSortedVars :: [VAR] -> SORT -> Doc
printSortedVars :: [VAR] -> SORT -> Doc
printSortedVars l :: [VAR]
l s :: SORT
s =
    [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((VAR -> Doc) -> [VAR] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map VAR -> Doc
sidDoc [VAR]
l) [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
colon Doc -> Doc -> Doc
<+> SORT -> Doc
idDoc SORT
s]

printVarDeclL :: [VAR_DECL] -> [Doc]
printVarDeclL :: [VAR_DECL] -> [Doc]
printVarDeclL = Doc -> [Doc] -> [Doc]
punctuate Doc
semi ([Doc] -> [Doc]) -> ([VAR_DECL] -> [Doc]) -> [VAR_DECL] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VAR_DECL -> Doc) -> [VAR_DECL] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> Doc
printVarDecl

printVarDecls :: [VAR_DECL] -> Doc
printVarDecls :: [VAR_DECL] -> Doc
printVarDecls = [Doc] -> Doc
fsep ([Doc] -> Doc) -> ([VAR_DECL] -> [Doc]) -> [VAR_DECL] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VAR_DECL] -> [Doc]
printVarDeclL

printVarDecl :: VAR_DECL -> Doc
printVarDecl :: VAR_DECL -> Doc
printVarDecl (Var_decl l :: [VAR]
l s :: SORT
s _) = [VAR] -> SORT -> Doc
printSortedVars [VAR]
l SORT
s

printArgDecls :: [VAR_DECL] -> Doc
printArgDecls :: [VAR_DECL] -> Doc
printArgDecls = Doc -> Doc
parens (Doc -> Doc) -> ([VAR_DECL] -> Doc) -> [VAR_DECL] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VAR_DECL] -> Doc
printVarDecls

printOptArgDecls :: [VAR_DECL] -> Doc
printOptArgDecls :: [VAR_DECL] -> Doc
printOptArgDecls vs :: [VAR_DECL]
vs = if [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
vs then Doc
empty else [VAR_DECL] -> Doc
printArgDecls [VAR_DECL]
vs

printPredHead :: PRED_HEAD -> Doc
printPredHead :: PRED_HEAD -> Doc
printPredHead (Pred_head l :: [VAR_DECL]
l _) = [VAR_DECL] -> Doc
printArgDecls [VAR_DECL]
l

printPredItem :: FormExtension f => PRED_ITEM f -> Doc
printPredItem :: PRED_ITEM f -> Doc
printPredItem p :: PRED_ITEM f
p = case PRED_ITEM f
p of
    Pred_decl l :: [SORT]
l t :: PRED_TYPE
t _ -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((SORT -> Doc) -> [SORT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Doc
idLabelDoc [SORT]
l)
        [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
colon Doc -> Doc -> Doc
<+> PRED_TYPE -> Doc
printPredType PRED_TYPE
t]
    Pred_defn i :: SORT
i h :: PRED_HEAD
h f :: Annoted (FORMULA f)
f _ ->
        [Doc] -> Doc
sep [ [Doc] -> Doc
cat [SORT -> Doc
idLabelDoc SORT
i, PRED_HEAD -> Doc
printPredHead PRED_HEAD
h]
           , Doc
equiv Doc -> Doc -> Doc
<+> (FORMULA f -> Doc) -> Annoted (FORMULA f) -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted FORMULA f -> Doc
forall f. FormExtension f => FORMULA f -> Doc
printFormula Annoted (FORMULA f)
f]

instance FormExtension f => Pretty (PRED_ITEM f) where
    pretty :: PRED_ITEM f -> Doc
pretty = PRED_ITEM f -> Doc
forall f. FormExtension f => PRED_ITEM f -> Doc
printPredItem

printAttr :: FormExtension f => OP_ATTR f -> Doc
printAttr :: OP_ATTR f -> Doc
printAttr a :: OP_ATTR f
a = case OP_ATTR f
a of
    Assoc_op_attr -> String -> Doc
text String
assocS
    Comm_op_attr -> String -> Doc
text String
commS
    Idem_op_attr -> String -> Doc
text String
idemS
    Unit_op_attr t :: TERM f
t -> String -> Doc
text String
unitS Doc -> Doc -> Doc
<+> TERM f -> Doc
forall f. FormExtension f => TERM f -> Doc
printTerm TERM f
t

instance FormExtension f => Pretty (OP_ATTR f) where
    pretty :: OP_ATTR f -> Doc
pretty = OP_ATTR f -> Doc
forall f. FormExtension f => OP_ATTR f -> Doc
printAttr

printOpHead :: OP_HEAD -> Doc
printOpHead :: OP_HEAD -> Doc
printOpHead (Op_head k :: OpKind
k l :: [VAR_DECL]
l mr :: Maybe SORT
mr _) =
    [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> Doc
printOptArgDecls [VAR_DECL]
l Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: case Maybe SORT
mr of
      Nothing -> []
      Just r :: SORT
r -> [(case OpKind
k of
             Total -> Doc
colon
             Partial -> String -> Doc
text String
colonQuMark) Doc -> Doc -> Doc
<+> SORT -> Doc
idDoc SORT
r]

instance Pretty OP_HEAD where
    pretty :: OP_HEAD -> Doc
pretty = OP_HEAD -> Doc
printOpHead

printOpItem :: FormExtension f => OP_ITEM f -> Doc
printOpItem :: OP_ITEM f -> Doc
printOpItem p :: OP_ITEM f
p = case OP_ITEM f
p of
    Op_decl l :: [SORT]
l t :: OP_TYPE
t a :: [OP_ATTR f]
a _ -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((SORT -> Doc) -> [SORT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Doc
idLabelDoc [SORT]
l)
        [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
colon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (if [OP_ATTR f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [OP_ATTR f]
a then Doc -> Doc
forall a. a -> a
id else (Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma)) (OP_TYPE -> Doc
printOpType OP_TYPE
t)]
        [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((OP_ATTR f -> Doc) -> [OP_ATTR f] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map OP_ATTR f -> Doc
forall f. FormExtension f => OP_ATTR f -> Doc
printAttr [OP_ATTR f]
a)
    Op_defn i :: SORT
i h :: OP_HEAD
h@(Op_head _ l :: [VAR_DECL]
l _ _) t :: Annoted (TERM f)
t _ ->
        [Doc] -> Doc
sep [ (if [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
l then [Doc] -> Doc
sep else [Doc] -> Doc
cat) [SORT -> Doc
idLabelDoc SORT
i, OP_HEAD -> Doc
printOpHead OP_HEAD
h]
            , Doc
equals Doc -> Doc -> Doc
<+> (TERM f -> Doc) -> Annoted (TERM f) -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted TERM f -> Doc
forall f. FormExtension f => TERM f -> Doc
printTerm Annoted (TERM f)
t]

instance FormExtension f => Pretty (OP_ITEM f) where
    pretty :: OP_ITEM f -> Doc
pretty = OP_ITEM f -> Doc
forall f. FormExtension f => OP_ITEM f -> Doc
printOpItem

instance Pretty VAR_DECL where
    pretty :: VAR_DECL -> Doc
pretty = VAR_DECL -> Doc
printVarDecl

printOpType :: OP_TYPE -> Doc
printOpType :: OP_TYPE -> Doc
printOpType (Op_type p :: OpKind
p l :: [SORT]
l r :: SORT
r _) =
    case [SORT]
l of
      [] -> case OpKind
p of
          Partial -> Doc
quMarkD Doc -> Doc -> Doc
<+> SORT -> Doc
idDoc SORT
r
          Total -> Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> SORT -> Doc
idDoc SORT
r
      _ -> Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
fsep
             (Doc -> [Doc] -> [Doc]
punctuate (Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
cross) ((SORT -> Doc) -> [SORT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Doc
idDoc [SORT]
l)
             [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [case OpKind
p of
                Partial -> Doc
pfun
                Total -> Doc
funArrow,
                 SORT -> Doc
idDoc SORT
r])

instance Pretty OP_TYPE where
    pretty :: OP_TYPE -> Doc
pretty = OP_TYPE -> Doc
printOpType

printOpSymb :: OP_SYMB -> Doc
printOpSymb :: OP_SYMB -> Doc
printOpSymb o :: OP_SYMB
o = case OP_SYMB
o of
    Op_name i :: SORT
i -> SORT -> Doc
idDoc SORT
i
    Qual_op_name i :: SORT
i t :: OP_TYPE
t _ -> [Doc] -> Doc
fsep [String -> Doc
text String
opS, SORT -> Doc
idDoc SORT
i, Doc
colon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> OP_TYPE -> Doc
printOpType OP_TYPE
t]

instance Pretty OP_SYMB where
    pretty :: OP_SYMB -> Doc
pretty = OP_SYMB -> Doc
printOpSymb

printPredType :: PRED_TYPE -> Doc
printPredType :: PRED_TYPE -> Doc
printPredType (Pred_type l :: [SORT]
l _) = case [SORT]
l of
    [] -> Doc -> Doc
parens Doc
empty
    _ -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate (Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
cross) ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (SORT -> Doc) -> [SORT] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Doc
idDoc [SORT]
l

instance Pretty PRED_TYPE where
    pretty :: PRED_TYPE -> Doc
pretty = PRED_TYPE -> Doc
printPredType

printPredSymb :: PRED_SYMB -> Doc
printPredSymb :: PRED_SYMB -> Doc
printPredSymb p :: PRED_SYMB
p = case PRED_SYMB
p of
    Pred_name i :: SORT
i -> SORT -> Doc
idDoc SORT
i
    Qual_pred_name i :: SORT
i t :: PRED_TYPE
t _ ->
        Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep [String -> Doc
text String
predS, SORT -> Doc
idDoc SORT
i, Doc
colon Doc -> Doc -> Doc
<+> PRED_TYPE -> Doc
printPredType PRED_TYPE
t]

instance Pretty PRED_SYMB where
    pretty :: PRED_SYMB -> Doc
pretty = PRED_SYMB -> Doc
printPredSymb

instance Pretty SYMB_ITEMS where
    pretty :: SYMB_ITEMS -> Doc
pretty = SYMB_ITEMS -> Doc
printSymbItems

printSymbItems :: SYMB_ITEMS -> Doc
printSymbItems :: SYMB_ITEMS -> Doc
printSymbItems (Symb_items k :: SYMB_KIND
k l :: [SYMB]
l _) =
    SYMB_KIND -> [SYMB] -> Doc
forall a. SYMB_KIND -> [a] -> Doc
print_kind_text SYMB_KIND
k [SYMB]
l Doc -> Doc -> Doc
<+> [Doc] -> Doc
sepByCommas ((SYMB -> Doc) -> [SYMB] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SYMB -> Doc
printSymb [SYMB]
l)

instance Pretty SYMB where
    pretty :: SYMB -> Doc
pretty = SYMB -> Doc
printSymb

printSymb :: SYMB -> Doc
printSymb :: SYMB -> Doc
printSymb s :: SYMB
s = case SYMB
s of
    Symb_id i :: SORT
i -> SORT -> Doc
idDoc SORT
i
    Qual_id i :: SORT
i t :: TYPE
t _ -> [Doc] -> Doc
fsep [SORT -> Doc
idDoc SORT
i, Doc
colon Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> TYPE -> Doc
printType TYPE
t]

instance Pretty TYPE where
    pretty :: TYPE -> Doc
pretty = TYPE -> Doc
printType

printType :: TYPE -> Doc
printType :: TYPE -> Doc
printType t :: TYPE
t = case TYPE
t of
    O_type ot :: OP_TYPE
ot -> OP_TYPE -> Doc
printOpType OP_TYPE
ot
    P_type pt :: PRED_TYPE
pt -> Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> PRED_TYPE -> Doc
printPredType PRED_TYPE
pt
    A_type s :: SORT
s -> Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> SORT -> Doc
idDoc SORT
s

print_kind_text :: SYMB_KIND -> [a] -> Doc
print_kind_text :: SYMB_KIND -> [a] -> Doc
print_kind_text k :: SYMB_KIND
k l :: [a]
l = case SYMB_KIND
k of
    Implicit -> Doc
empty
    _ -> String -> Doc
keyword (SYMB_KIND -> [a] -> String
forall a. SYMB_KIND -> [a] -> String
pluralS_symb_list SYMB_KIND
k [a]
l)

pluralS_symb_list :: SYMB_KIND -> [a] -> String
pluralS_symb_list :: SYMB_KIND -> [a] -> String
pluralS_symb_list k :: SYMB_KIND
k l :: [a]
l = (case SYMB_KIND
k of
    Implicit -> String -> String
forall a. HasCallStack => String -> a
error "pluralS_symb_list"
    Sorts_kind -> String
sortS
    Ops_kind -> String
opS
    Preds_kind -> String
predS) String -> String -> String
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. [a] -> String
appendS [a]
l

instance Pretty SYMB_OR_MAP where
    pretty :: SYMB_OR_MAP -> Doc
pretty = SYMB_OR_MAP -> Doc
printSymbOrMap

printSymbOrMap :: SYMB_OR_MAP -> Doc
printSymbOrMap :: SYMB_OR_MAP -> Doc
printSymbOrMap som :: SYMB_OR_MAP
som = case SYMB_OR_MAP
som of
    Symb s :: SYMB
s -> SYMB -> Doc
printSymb SYMB
s
    Symb_map s :: SYMB
s t :: SYMB
t _ -> [Doc] -> Doc
fsep [SYMB -> Doc
printSymb SYMB
s, Doc
mapsto Doc -> Doc -> Doc
<+> SYMB -> Doc
printSymb SYMB
t]

instance Pretty SYMB_KIND where
    pretty :: SYMB_KIND -> Doc
pretty = SYMB_KIND -> Doc
printSymbKind

printSymbKind :: SYMB_KIND -> Doc
printSymbKind :: SYMB_KIND -> Doc
printSymbKind sk :: SYMB_KIND
sk = SYMB_KIND -> [()] -> Doc
forall a. SYMB_KIND -> [a] -> Doc
print_kind_text SYMB_KIND
sk [()]

instance Pretty SYMB_MAP_ITEMS where
    pretty :: SYMB_MAP_ITEMS -> Doc
pretty = SYMB_MAP_ITEMS -> Doc
printSymbMapItems

printSymbMapItems :: SYMB_MAP_ITEMS -> Doc
printSymbMapItems :: SYMB_MAP_ITEMS -> Doc
printSymbMapItems (Symb_map_items k :: SYMB_KIND
k l :: [SYMB_OR_MAP]
l _) =
    SYMB_KIND -> [SYMB_OR_MAP] -> Doc
forall a. SYMB_KIND -> [a] -> Doc
print_kind_text SYMB_KIND
k [SYMB_OR_MAP]
l Doc -> Doc -> Doc
<+> [Doc] -> Doc
sepByCommas ((SYMB_OR_MAP -> Doc) -> [SYMB_OR_MAP] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map SYMB_OR_MAP -> Doc
printSymbOrMap [SYMB_OR_MAP]
l)

-- possibly use "printInfix False vcat"
printInfix :: Bool -- ^ attach separator to right argument?
           -> ([Doc] -> Doc) -- ^ combinator for two docs
           -> Doc -> Doc -> Doc -- ^ left, separator and right arguments
           -> Doc
printInfix :: Bool -> ([Doc] -> Doc) -> Doc -> Doc -> Doc -> Doc
printInfix b :: Bool
b join :: [Doc] -> Doc
join l :: Doc
l s :: Doc
s r :: Doc
r =
     [Doc] -> Doc
join ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ if Bool
b then [Doc
l, Doc
s Doc -> Doc -> Doc
<+> Doc
r] else [Doc
l Doc -> Doc -> Doc
<+> Doc
s, Doc
r]

class (GetRange f, Pretty f) => FormExtension f where
  isQuantifierLike :: f -> Bool
  isQuantifierLike _ = Bool
False
  prefixExt :: f -> Doc -> Doc
  prefixExt _ = (Doc
bullet Doc -> Doc -> Doc
<+>)

instance FormExtension ()

printRecord :: FormExtension f => Record f Doc Doc
printRecord :: Record f Doc Doc
printRecord = Record :: forall f a b.
(FORMULA f -> QUANTIFIER -> [VAR_DECL] -> a -> Range -> a)
-> (FORMULA f -> Junctor -> [a] -> Range -> a)
-> (FORMULA f -> a -> Relation -> a -> Range -> a)
-> (FORMULA f -> a -> Range -> a)
-> (FORMULA f -> Bool -> Range -> a)
-> (FORMULA f -> PRED_SYMB -> [b] -> Range -> a)
-> (FORMULA f -> b -> Range -> a)
-> (FORMULA f -> b -> Equality -> b -> Range -> a)
-> (FORMULA f -> b -> SORT -> Range -> a)
-> (FORMULA f -> b -> a)
-> (FORMULA f -> [Constraint] -> Bool -> a)
-> (FORMULA f -> SORT -> OP_TYPE -> a -> a)
-> (FORMULA f -> SORT -> PRED_TYPE -> a -> a)
-> (FORMULA f -> f -> a)
-> (TERM f -> VAR -> SORT -> Range -> b)
-> (TERM f -> OP_SYMB -> [b] -> Range -> b)
-> (TERM f -> b -> SORT -> Range -> b)
-> (TERM f -> b -> SORT -> Range -> b)
-> (TERM f -> b -> a -> b -> Range -> b)
-> (TERM f -> PRED_SYMB -> b)
-> (TERM f -> [b] -> b)
-> (TERM f -> VAR -> b)
-> (TERM f -> SORT -> Range -> b)
-> (TERM f -> SORT -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> f -> b)
-> Record f a b
Record
    { foldQuantification :: FORMULA f -> QUANTIFIER -> [VAR_DECL] -> Doc -> Range -> Doc
foldQuantification = \ _ q :: QUANTIFIER
q l :: [VAR_DECL]
l r :: Doc
r _ ->
          [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ QUANTIFIER -> Doc
printQuant QUANTIFIER
q Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [VAR_DECL] -> [Doc]
printVarDeclL [VAR_DECL]
l
                                [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> Doc
addBullet Doc
r]
    , foldJunction :: FORMULA f -> Junctor -> [Doc] -> Range -> Doc
foldJunction = \ o :: FORMULA f
o j :: Junctor
j l :: [Doc]
l _ ->
        let (n :: String
n, p :: Doc
p) = case Junctor
j of
                  Con -> (String
trueS, Doc
andDoc)
                  Dis -> (String
falseS, Doc
orDoc)
        in case FORMULA f
o of
          Junction _ ol :: [FORMULA f]
ol@(_ : _) _ -> [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
prepPunctuate (Doc
p Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
space)
               ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (FORMULA f -> Doc -> Doc) -> [FORMULA f] -> [Doc] -> [Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Bool -> FORMULA f -> Doc -> Doc
forall f. FormExtension f => Bool -> FORMULA f -> Doc -> Doc
mkJunctDoc Bool
True) ([FORMULA f] -> [FORMULA f]
forall a. [a] -> [a]
init [FORMULA f]
ol) ([Doc] -> [Doc]
forall a. [a] -> [a]
init [Doc]
l) [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
                 [Bool -> FORMULA f -> Doc -> Doc
forall f. FormExtension f => Bool -> FORMULA f -> Doc -> Doc
mkJunctDoc Bool
False ([FORMULA f] -> FORMULA f
forall a. [a] -> a
last [FORMULA f]
ol) ([Doc] -> Doc
forall a. [a] -> a
last [Doc]
l)]
          _ -> String -> Doc
text String
n
    , foldRelation :: FORMULA f -> Doc -> Relation -> Doc -> Range -> Doc
foldRelation = \ o :: FORMULA f
o l :: Doc
l c :: Relation
c r :: Doc
r _ ->
          let Relation oL :: FORMULA f
oL _ oR :: FORMULA f
oR _ = FORMULA f
o
              b :: Bool
b = Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
Implication
              nl :: Doc
nl = if FORMULA f -> Bool
forall f. FORMULA f -> Bool
isAnyImpl FORMULA f
oL Bool -> Bool -> Bool
|| Bool
b Bool -> Bool -> Bool
&& FORMULA f -> Bool
forall f. FormExtension f => FORMULA f -> Bool
isQuant FORMULA f
oL
                   then Doc -> Doc
parens Doc
l else Doc
l
              nr :: Doc
nr = if Relation -> FORMULA f -> Bool
forall f. Relation -> FORMULA f -> Bool
isImpl Relation
c FORMULA f
oR Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
b Bool -> Bool -> Bool
&& FORMULA f -> Bool
forall f. FormExtension f => FORMULA f -> Bool
isQuant FORMULA f
oR
                   then Doc -> Doc
parens Doc
r else Doc
r
          in case Relation
c of
               Implication -> Bool -> ([Doc] -> Doc) -> Doc -> Doc -> Doc -> Doc
printInfix Bool
True [Doc] -> Doc
sep Doc
nl Doc
implies Doc
nr
               RevImpl -> Bool -> ([Doc] -> Doc) -> Doc -> Doc -> Doc -> Doc
printInfix Bool
True [Doc] -> Doc
sep Doc
nr (String -> Doc
text String
ifS) Doc
nl
               Equivalence -> Bool -> ([Doc] -> Doc) -> Doc -> Doc -> Doc -> Doc
printInfix Bool
True [Doc] -> Doc
sep
                 (if FORMULA f -> Bool
forall f. FormExtension f => FORMULA f -> Bool
isQuant FORMULA f
oL then Doc -> Doc
parens Doc
l else FORMULA f -> Doc -> Doc
forall f. FORMULA f -> Doc -> Doc
mkEquivDoc FORMULA f
oL Doc
l)
                 Doc
equiv (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Doc -> Doc
forall f. FORMULA f -> Doc -> Doc
mkEquivDoc FORMULA f
oR Doc
r
    , foldNegation :: FORMULA f -> Doc -> Range -> Doc
foldNegation = \ orig :: FORMULA f
orig r :: Doc
r _ -> case FORMULA f
orig of
          Negation o :: FORMULA f
o _ -> [Doc] -> Doc
hsep [Doc
notDoc, Bool -> FORMULA f -> Doc -> Doc
forall f. FormExtension f => Bool -> FORMULA f -> Doc -> Doc
mkJunctDoc Bool
False FORMULA f
o Doc
r]
          _ -> String -> Doc
forall a. HasCallStack => String -> a
error "CASL.ToDoc.printRecord.foldNegation"
    , foldAtom :: FORMULA f -> Bool -> Range -> Doc
foldAtom = \ _ b :: Bool
b _ -> String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ if Bool
b then String
trueS else String
falseS
    , foldPredication :: FORMULA f -> PRED_SYMB -> [Doc] -> Range -> Doc
foldPredication = \ o :: FORMULA f
o p :: PRED_SYMB
p l :: [Doc]
l _ -> case (PRED_SYMB
p, FORMULA f
o) of
          (Pred_name i :: SORT
i, Predication _ ol :: [TERM f]
ol _) -> SORT -> [Doc] -> Doc
predIdApplDoc SORT
i ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [TERM f] -> [Doc] -> [Doc]
forall f. [TERM f] -> [Doc] -> [Doc]
zipConds [TERM f]
ol [Doc]
l
          _ -> if [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
l then PRED_SYMB -> Doc
printPredSymb PRED_SYMB
p else
              [Doc] -> Doc
fcat [PRED_SYMB -> Doc
printPredSymb PRED_SYMB
p, Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sepByCommas [Doc]
l]
    , foldDefinedness :: FORMULA f -> Doc -> Range -> Doc
foldDefinedness = \ _ r :: Doc
r _ -> [Doc] -> Doc
hsep [String -> Doc
text String
defS, Doc
r]
    , foldEquation :: FORMULA f -> Doc -> Equality -> Doc -> Range -> Doc
foldEquation = \ _ l :: Doc
l e :: Equality
e r :: Doc
r _ -> Bool -> ([Doc] -> Doc) -> Doc -> Doc -> Doc -> Doc
printInfix Bool
True [Doc] -> Doc
sep Doc
l (case Equality
e of
        Existl -> Doc
exequal
        Strong -> Doc
equals) Doc
r
    , foldMembership :: FORMULA f -> Doc -> SORT -> Range -> Doc
foldMembership = \ _ r :: Doc
r t :: SORT
t _ -> [Doc] -> Doc
fsep [Doc
r, Doc
inDoc, SORT -> Doc
idDoc SORT
t]
    , foldMixfix_formula :: FORMULA f -> Doc -> Doc
foldMixfix_formula = \ _ r :: Doc
r -> Doc
r
    , foldSort_gen_ax :: FORMULA f -> [Constraint] -> Bool -> Doc
foldSort_gen_ax = \ o :: FORMULA f
o _ _ ->
        let Sort_gen_ax constrs :: [Constraint]
constrs b :: Bool
b = FORMULA f
o
            l :: [Annoted DATATYPE_DECL]
l = [Constraint] -> [Annoted DATATYPE_DECL]
recoverType [Constraint]
constrs
            genAx :: Doc
genAx = [Doc] -> Doc
sep [ String -> Doc
keyword String
generatedS Doc -> Doc -> Doc
<+> String -> Doc
keyword (String
typeS String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Annoted DATATYPE_DECL] -> String
forall a. [a] -> String
appendS [Annoted DATATYPE_DECL]
l)
                        , (DATATYPE_DECL -> Doc) -> [Annoted DATATYPE_DECL] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos DATATYPE_DECL -> Doc
printDATATYPE_DECL [Annoted DATATYPE_DECL]
l]
        in if Bool
b then String -> Doc
text "%% free" Doc -> Doc -> Doc
$+$ Doc
genAx else Doc
genAx
    , foldQuantOp :: FORMULA f -> SORT -> OP_TYPE -> Doc -> Doc
foldQuantOp = \ _ o :: SORT
o n :: OP_TYPE
n r :: Doc
r -> [Doc] -> Doc
fsep
        [ Doc
forallDoc
        , Doc -> Doc
parens (Doc -> Doc) -> (OP_SYMB -> Doc) -> OP_SYMB -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OP_SYMB -> Doc
printOpSymb (OP_SYMB -> Doc) -> OP_SYMB -> Doc
forall a b. (a -> b) -> a -> b
$ SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
o OP_TYPE
n
        , Doc -> Doc
addBullet Doc
r ]
    , foldQuantPred :: FORMULA f -> SORT -> PRED_TYPE -> Doc -> Doc
foldQuantPred = \ _ p :: SORT
p n :: PRED_TYPE
n r :: Doc
r -> [Doc] -> Doc
fsep
        [ Doc
forallDoc
        , PRED_SYMB -> Doc
printPredSymb (PRED_SYMB -> Doc) -> PRED_SYMB -> Doc
forall a b. (a -> b) -> a -> b
$ SORT -> PRED_TYPE -> PRED_SYMB
mkQualPred SORT
p PRED_TYPE
n
        , Doc -> Doc
addBullet Doc
r ]
    , foldExtFORMULA :: FORMULA f -> f -> Doc
foldExtFORMULA = (f -> Doc) -> FORMULA f -> f -> Doc
forall a b. a -> b -> a
const f -> Doc
forall a. Pretty a => a -> Doc
pretty
    , foldQual_var :: TERM f -> VAR -> SORT -> Range -> Doc
foldQual_var = \ _ v :: VAR
v s :: SORT
s _ ->
          Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep [String -> Doc
text String
varS, VAR -> Doc
sidDoc VAR
v, Doc
colon Doc -> Doc -> Doc
<+> SORT -> Doc
idDoc SORT
s]
    , foldApplication :: TERM f -> OP_SYMB -> [Doc] -> Range -> Doc
foldApplication = \ orig :: TERM f
orig o :: OP_SYMB
o l :: [Doc]
l _ -> case (OP_SYMB
o, TERM f
orig) of
          (Op_name i :: SORT
i, Application _ ol :: [TERM f]
ol _) -> SORT -> [Doc] -> Doc
idApplDoc SORT
i ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [TERM f] -> [Doc] -> [Doc]
forall f. [TERM f] -> [Doc] -> [Doc]
zipConds [TERM f]
ol [Doc]
l
          _ -> let d :: Doc
d = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> Doc
printOpSymb OP_SYMB
o in
              if [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
l then Doc
d else [Doc] -> Doc
fcat [Doc
d, Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sepByCommas [Doc]
l]
    , foldSorted_term :: TERM f -> Doc -> SORT -> Range -> Doc
foldSorted_term = \ _ r :: Doc
r t :: SORT
t _ -> [Doc] -> Doc
fsep [SORT -> [Doc] -> Doc
idApplDoc SORT
typeId [Doc
r], SORT -> Doc
idDoc SORT
t]
    , foldCast :: TERM f -> Doc -> SORT -> Range -> Doc
foldCast = \ _ r :: Doc
r t :: SORT
t _ ->
          [Doc] -> Doc
fsep [SORT -> [Doc] -> Doc
idApplDoc ([VAR] -> SORT
mkId [VAR
placeTok, String -> VAR
mkSimpleId String
asS]) [Doc
r], SORT -> Doc
idDoc SORT
t]
    , foldConditional :: TERM f -> Doc -> Doc -> Doc -> Range -> Doc
foldConditional = \ o :: TERM f
o l :: Doc
l f :: Doc
f r :: Doc
r _ -> case TERM f
o of
          Conditional ol :: TERM f
ol _ _ _ -> [Doc] -> Doc
fsep [if TERM f -> Bool
forall f. TERM f -> Bool
isCond TERM f
ol then Doc -> Doc
parens Doc
l else Doc
l,
                String -> Doc
text String
whenS Doc -> Doc -> Doc
<+> Doc
f, String -> Doc
text String
elseS Doc -> Doc -> Doc
<+> Doc
r]
          _ -> String -> Doc
forall a. HasCallStack => String -> a
error "CASL.ToDoc.printRecord.foldConditional"
    , foldMixfix_qual_pred :: TERM f -> PRED_SYMB -> Doc
foldMixfix_qual_pred = (PRED_SYMB -> Doc) -> TERM f -> PRED_SYMB -> Doc
forall a b. a -> b -> a
const PRED_SYMB -> Doc
printPredSymb
    , foldMixfix_term :: TERM f -> [Doc] -> Doc
foldMixfix_term = \ o :: TERM f
o l :: [Doc]
l -> case TERM f
o of
          Mixfix_term [_, Mixfix_parenthesized _ _] -> [Doc] -> Doc
fcat [Doc]
l
          _ -> [Doc] -> Doc
fsep [Doc]
l
    , foldMixfix_token :: TERM f -> VAR -> Doc
foldMixfix_token = (VAR -> Doc) -> TERM f -> VAR -> Doc
forall a b. a -> b -> a
const VAR -> Doc
sidDoc
    , foldMixfix_sorted_term :: TERM f -> SORT -> Range -> Doc
foldMixfix_sorted_term = \ _ s :: SORT
s _ -> Doc
colon Doc -> Doc -> Doc
<+> SORT -> Doc
idDoc SORT
s
    , foldMixfix_cast :: TERM f -> SORT -> Range -> Doc
foldMixfix_cast = \ _ s :: SORT
s _ -> String -> Doc
text String
asS Doc -> Doc -> Doc
<+> SORT -> Doc
idDoc SORT
s
    , foldMixfix_parenthesized :: TERM f -> [Doc] -> Range -> Doc
foldMixfix_parenthesized = \ _ l :: [Doc]
l _ -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sepByCommas [Doc]
l
    , foldMixfix_bracketed :: TERM f -> [Doc] -> Range -> Doc
foldMixfix_bracketed = \ _ l :: [Doc]
l _ -> Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sepByCommas [Doc]
l
    , foldMixfix_braced :: TERM f -> [Doc] -> Range -> Doc
foldMixfix_braced = \ _ l :: [Doc]
l _ -> Doc -> Doc
specBraces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sepByCommas [Doc]
l
    , foldExtTERM :: TERM f -> f -> Doc
foldExtTERM = (f -> Doc) -> TERM f -> f -> Doc
forall a b. a -> b -> a
const f -> Doc
forall a. Pretty a => a -> Doc
pretty }

recoverType :: [Constraint] -> [Annoted DATATYPE_DECL]
recoverType :: [Constraint] -> [Annoted DATATYPE_DECL]
recoverType =
  (Constraint -> Annoted DATATYPE_DECL)
-> [Constraint] -> [Annoted DATATYPE_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: Constraint
c -> let s :: SORT
s = Constraint -> SORT
newSort Constraint
c in DATATYPE_DECL -> Annoted DATATYPE_DECL
forall a. a -> Annoted a
emptyAnno (DATATYPE_DECL -> Annoted DATATYPE_DECL)
-> DATATYPE_DECL -> Annoted DATATYPE_DECL
forall a b. (a -> b) -> a -> b
$ SORT -> [Annoted ALTERNATIVE] -> Range -> DATATYPE_DECL
Datatype_decl SORT
s
      (((OP_SYMB, [Int]) -> Annoted ALTERNATIVE)
-> [(OP_SYMB, [Int])] -> [Annoted ALTERNATIVE]
forall a b. (a -> b) -> [a] -> [b]
map (\ (o :: OP_SYMB
o, _) -> case OP_SYMB
o of
      Qual_op_name i :: SORT
i (Op_type fk :: OpKind
fk args :: [SORT]
args _ ps :: Range
ps) r :: Range
r ->
          let qs :: Range
qs = Range -> Range -> Range
appRange Range
ps Range
r in ALTERNATIVE -> Annoted ALTERNATIVE
forall a. a -> Annoted a
emptyAnno (ALTERNATIVE -> Annoted ALTERNATIVE)
-> ALTERNATIVE -> Annoted ALTERNATIVE
forall a b. (a -> b) -> a -> b
$ case [SORT]
args of
            [_] | SORT -> Bool
isInjName SORT
i -> [SORT] -> Range -> ALTERNATIVE
Subsorts [SORT]
args Range
qs
            _ -> OpKind -> SORT -> [COMPONENTS] -> Range -> ALTERNATIVE
Alt_construct OpKind
fk SORT
i ((SORT -> COMPONENTS) -> [SORT] -> [COMPONENTS]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> COMPONENTS
Sort [SORT]
args) Range
qs
      _ -> String -> Annoted ALTERNATIVE
forall a. HasCallStack => String -> a
error "CASL.recoverType") ([(OP_SYMB, [Int])] -> [Annoted ALTERNATIVE])
-> [(OP_SYMB, [Int])] -> [Annoted ALTERNATIVE]
forall a b. (a -> b) -> a -> b
$ Constraint -> [(OP_SYMB, [Int])]
opSymbs Constraint
c) Range
nullRange)

zipConds :: [TERM f] -> [Doc] -> [Doc]
zipConds :: [TERM f] -> [Doc] -> [Doc]
zipConds = (TERM f -> Doc -> Doc) -> [TERM f] -> [Doc] -> [Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ o :: TERM f
o d :: Doc
d -> if TERM f -> Bool
forall f. TERM f -> Bool
isCond TERM f
o then Doc -> Doc
parens Doc
d else Doc
d)

printFormula :: FormExtension f => FORMULA f -> Doc
printFormula :: FORMULA f -> Doc
printFormula = Record f Doc Doc -> FORMULA f -> Doc
forall f a b. Record f a b -> FORMULA f -> a
foldFormula Record f Doc Doc
forall f. FormExtension f => Record f Doc Doc
printRecord

instance FormExtension f => Pretty (FORMULA f) where
    pretty :: FORMULA f -> Doc
pretty = FORMULA f -> Doc
forall f. FormExtension f => FORMULA f -> Doc
printFormula

printTerm :: FormExtension f => TERM f -> Doc
printTerm :: TERM f -> Doc
printTerm = Record f Doc Doc -> TERM f -> Doc
forall f a b. Record f a b -> TERM f -> b
foldTerm Record f Doc Doc
forall f. FormExtension f => Record f Doc Doc
printRecord

instance FormExtension f => Pretty (TERM f) where
    pretty :: TERM f -> Doc
pretty = TERM f -> Doc
forall f. FormExtension f => TERM f -> Doc
printTerm

isQuant :: FormExtension f => FORMULA f -> Bool
isQuant :: FORMULA f -> Bool
isQuant f :: FORMULA f
f = case FORMULA f
f of
    Quantification {} -> Bool
True
    ExtFORMULA ef :: f
ef -> f -> Bool
forall f. FormExtension f => f -> Bool
isQuantifierLike f
ef
    Junction _ l :: [FORMULA f]
l _ -> case [FORMULA f]
l of
        [] -> Bool
False
        _ -> FORMULA f -> Bool
forall f. FormExtension f => FORMULA f -> Bool
isQuant (FORMULA f -> Bool) -> FORMULA f -> Bool
forall a b. (a -> b) -> a -> b
$ [FORMULA f] -> FORMULA f
forall a. [a] -> a
last [FORMULA f]
l
    Relation a :: FORMULA f
a c :: Relation
c b :: FORMULA f
b _ -> FORMULA f -> Bool
forall f. FormExtension f => FORMULA f -> Bool
isQuant (FORMULA f -> Bool) -> FORMULA f -> Bool
forall a b. (a -> b) -> a -> b
$ if Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
RevImpl then FORMULA f
a else FORMULA f
b
    Negation a :: FORMULA f
a _ -> FORMULA f -> Bool
forall f. FormExtension f => FORMULA f -> Bool
isQuant FORMULA f
a
    _ -> Bool
False

isEquiv :: FORMULA f -> Bool
isEquiv :: FORMULA f -> Bool
isEquiv f :: FORMULA f
f = case FORMULA f
f of
    Relation _ c :: Relation
c _ _ -> Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
Equivalence
    _ -> Bool
False

isAnyImpl :: FORMULA f -> Bool
isAnyImpl :: FORMULA f -> Bool
isAnyImpl f :: FORMULA f
f = Relation -> FORMULA f -> Bool
forall f. Relation -> FORMULA f -> Bool
isImpl Relation
Implication FORMULA f
f Bool -> Bool -> Bool
|| Relation -> FORMULA f -> Bool
forall f. Relation -> FORMULA f -> Bool
isImpl Relation
RevImpl FORMULA f
f

isJunct :: FORMULA f -> Bool
isJunct :: FORMULA f -> Bool
isJunct f :: FORMULA f
f = case FORMULA f
f of
    Junction {} -> Bool
True
    _ -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
isAnyImpl FORMULA f
f

-- true for non-final
mkJunctDoc :: FormExtension f => Bool -> FORMULA f -> Doc -> Doc
mkJunctDoc :: Bool -> FORMULA f -> Doc -> Doc
mkJunctDoc b :: Bool
b f :: FORMULA f
f = if FORMULA f -> Bool
forall f. FORMULA f -> Bool
isJunct FORMULA f
f Bool -> Bool -> Bool
|| Bool
b Bool -> Bool -> Bool
&& FORMULA f -> Bool
forall f. FormExtension f => FORMULA f -> Bool
isQuant FORMULA f
f then Doc -> Doc
parens else Doc -> Doc
forall a. a -> a
id

mkEquivDoc :: FORMULA f -> Doc -> Doc
mkEquivDoc :: FORMULA f -> Doc -> Doc
mkEquivDoc f :: FORMULA f
f = if FORMULA f -> Bool
forall f. FORMULA f -> Bool
isEquiv FORMULA f
f then Doc -> Doc
parens else Doc -> Doc
forall a. a -> a
id

isImpl :: Relation -> FORMULA f -> Bool
isImpl :: Relation -> FORMULA f -> Bool
isImpl a :: Relation
a f :: FORMULA f
f = case FORMULA f
f of
    Relation _ c :: Relation
c _ _ -> Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
Equivalence Bool -> Bool -> Bool
|| Relation
a Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
/= Relation
c
    _ -> Bool
False

isCond :: TERM f -> Bool
isCond :: TERM f -> Bool
isCond t :: TERM f
t = case TERM f
t of
    Conditional {} -> Bool
True
    _ -> Bool
False

-- | a helper class for calculating the pluralS of e.g. ops
class ListCheck a where
    innerList :: a -> [()]

instance ListCheck Token where
    innerList :: VAR -> [()]
innerList _ = [()]

instance ListCheck Id where
    innerList :: SORT -> [()]
innerList _ = [()]

instance ListCheck a => ListCheck [a] where
    innerList :: [a] -> [()]
innerList = (a -> [()]) -> [a] -> [()]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap a -> [()]
forall a. ListCheck a => a -> [()]
innerList

-- | an instance of ListCheck for Annoted stuff
instance ListCheck a => ListCheck (Annoted a) where
    innerList :: Annoted a -> [()]
innerList = a -> [()]
forall a. ListCheck a => a -> [()]
innerList (a -> [()]) -> (Annoted a -> a) -> Annoted a -> [()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted a -> a
forall a. Annoted a -> a
item

{- | pluralS checks nested lists via the class ListCheck to decide
if a plural s should be appended. -}
pluralS :: ListCheck a => a -> String
pluralS :: a -> String
pluralS = [()] -> String
forall a. [a] -> String
appendS ([()] -> String) -> (a -> [()]) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [()]
forall a. ListCheck a => a -> [()]
innerList

appendS :: [a] -> String
appendS :: [a] -> String
appendS l :: [a]
l = if [a] -> Bool
forall a. [a] -> Bool
isSingle [a]
l then "" else "s"

-- instances of ListCheck for various data types of AS_Basic_CASL

instance ListCheck (SORT_ITEM f) where
    innerList :: SORT_ITEM f -> [()]
innerList (Sort_decl l :: [SORT]
l _) = [SORT] -> [()]
forall a. ListCheck a => a -> [()]
innerList [SORT]
l
    innerList (Subsort_decl l :: [SORT]
l _ _) = [SORT] -> [()]
forall a. ListCheck a => a -> [()]
innerList [SORT]
l
    innerList (Subsort_defn {}) = [()]
    innerList (Iso_decl l :: [SORT]
l _) = [SORT] -> [()]
forall a. ListCheck a => a -> [()]
innerList ([SORT] -> [()]) -> [SORT] -> [()]
forall a b. (a -> b) -> a -> b
$ Int -> [SORT] -> [SORT]
forall a. Int -> [a] -> [a]
drop 1 [SORT]
l
      -- assume last sort is known

instance ListCheck (OP_ITEM f) where
    innerList :: OP_ITEM f -> [()]
innerList (Op_decl l :: [SORT]
l _ _ _) = [SORT] -> [()]
forall a. ListCheck a => a -> [()]
innerList [SORT]
l
    innerList (Op_defn {}) = [()]

instance ListCheck (PRED_ITEM f) where
    innerList :: PRED_ITEM f -> [()]
innerList (Pred_decl l :: [SORT]
l _ _) = [SORT] -> [()]
forall a. ListCheck a => a -> [()]
innerList [SORT]
l
    innerList (Pred_defn {}) = [()]

instance ListCheck VAR_DECL where
    innerList :: VAR_DECL -> [()]
innerList (Var_decl l :: [VAR]
l _ _) = [VAR] -> [()]
forall a. ListCheck a => a -> [()]
innerList [VAR]
l

-- | print a formula as a sentence
printTheoryFormula :: FormExtension f => Named (FORMULA f) -> Doc
printTheoryFormula :: Named (FORMULA f) -> Doc
printTheoryFormula f :: Named (FORMULA f)
f = (FORMULA f -> Doc) -> Annoted (FORMULA f) -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted
    ((case Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence Named (FORMULA f)
f of
    Quantification Universal _ _ _ -> Doc -> Doc
forall a. a -> a
id
    Sort_gen_ax _ _ -> Doc -> Doc
forall a. a -> a
id
    ExtFORMULA e :: f
e -> f -> Doc -> Doc
forall f. FormExtension f => f -> Doc -> Doc
prefixExt f
e
    _ -> (Doc
bullet Doc -> Doc -> Doc
<+>)) (Doc -> Doc) -> (FORMULA f -> Doc) -> FORMULA f -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> Doc
forall a. Pretty a => a -> Doc
pretty) (Annoted (FORMULA f) -> Doc) -> Annoted (FORMULA f) -> Doc
forall a b. (a -> b) -> a -> b
$ Named (FORMULA f) -> Annoted (FORMULA f)
forall s. Named s -> Annoted s
fromLabelledSen Named (FORMULA f)
f