instance (Pretty b, Pretty s, FormExtension f) => Pretty (BASIC_SPEC b s f)
where pretty = printBASIC_SPEC pretty pretty
printBASIC_SPEC :: FormExtension f => (b -> Doc) -> (s -> Doc)
-> BASIC_SPEC b s f -> Doc
printBASIC_SPEC fB fS (Basic_spec l) = case l of
_ -> vcat $ map (printAnnoted (printBASIC_ITEMS fB fS)) l
instance (Pretty b, Pretty s, FormExtension f) => Pretty (BASIC_ITEMS b s f)
where pretty = printBASIC_ITEMS pretty pretty
typeString :: SortsKind -> [Annoted DATATYPE_DECL] -> String
typeString sk l = (case sk of
PossiblyEmptySorts -> etypeS) ++ appendS l
printBASIC_ITEMS :: FormExtension f => (b -> Doc) -> (s -> Doc)
-> BASIC_ITEMS b s f -> Doc
printBASIC_ITEMS fB fS sis = case sis of
Sig_items s -> printSIG_ITEMS fS s
Free_datatype sk l _ -> sep [keyword freeS <+> keyword (typeString sk l),
semiAnnos printDATATYPE_DECL l]
Sort_gen l _ -> case l of
[Annoted (Datatype_items sk l' _) _ las ras] ->
(if null las then id else (printAnnotationList las $+$))
$ (if null ras then id else ($+$ printAnnotationList ras))
$ sep [keyword generatedS <+> keyword (typeString sk l'),
semiAnnos printDATATYPE_DECL l']
_ -> sep [keyword generatedS, specBraces $ vcat $ map
(printAnnoted $ printSIG_ITEMS fS) l]
Var_items l _ -> topSigKey (varS ++ pluralS l) <+> printVarDecls l
Local_var_axioms l f _ ->
fsep [fsep $ forallDoc : printVarDeclL l
, printAnnotedBulletFormulas f]
Axiom_items f _ -> printAnnotedBulletFormulas f
Ext_BASIC_ITEMS b -> fB b
printAnnotedBulletFormulas :: FormExtension f => [Annoted (FORMULA f)] -> Doc
printAnnotedBulletFormulas l = vcat $ case l of
_ -> let pp = addBullet . printFormula in
map (printAnnoted pp) (init l)
++ [printSemiAnno pp False $ last l] -- use True for HasCASL
instance (Pretty s, FormExtension f) => Pretty (SIG_ITEMS s f) where
pretty = printSIG_ITEMS pretty
printSIG_ITEMS :: FormExtension f => (s -> Doc) -> SIG_ITEMS s f -> Doc
printSIG_ITEMS fS sis = case sis of
Sort_items sk l _ -> topSigKey ((case sk of
PossiblyEmptySorts -> esortS) ++ pluralS l) <+>
semiAnnos printSortItem l
Op_items l _ -> topSigKey (opS ++ pluralS l) <+>
if null l then empty else if case item $ last l of
Op_decl _ _ a@(_ : _) _ -> case last a of
Unit_op_attr {} -> False -- use True for HasCASL
Op_defn {} -> False -- use True for HasCASL
then vcat $ map (printSemiAnno pp True) l else semiAnnos pp l
Pred_items l _ -> topSigKey (predS ++ pluralS l) <+>
let pp = printPredItem in
if null l then empty else if case item $ last l of
then vcat $ map (printSemiAnno pp True) l else semiAnnos pp l
Datatype_items sk l _ -> topSigKey (typeString sk l) <+>
semiAnnos printDATATYPE_DECL l
printDATATYPE_DECL :: DATATYPE_DECL -> Doc
printDATATYPE_DECL (Datatype_decl s a r) =
let pa = printAnnoted printALTERNATIVE in case a of
[] -> printDATATYPE_DECL (Datatype_decl s [emptyAnno $ Subsorts [s] r] r)
h : t -> sep [idLabelDoc s, colon <> colon <> sep
instance Pretty DATATYPE_DECL where
pretty = printDATATYPE_DECL
printCOMPONENTS :: COMPONENTS -> Doc
printCOMPONENTS c = case c of
Cons_select k l s _ -> fsep $ punctuate comma (map idLabelDoc l)
Partial -> colon <> quMarkD, idDoc s]
instance Pretty COMPONENTS where
printALTERNATIVE :: ALTERNATIVE -> Doc
printALTERNATIVE a = case a of
Alt_construct k n l _ -> case l of
parens ( sep $ punctuate semi $ map printCOMPONENTS l)
Subsorts l _ -> fsep $ text (sortS ++ pluralS l)
: punctuate comma (map idDoc l)
instance Pretty ALTERNATIVE where
pretty = printALTERNATIVE
printSortItem :: FormExtension f => SORT_ITEM f -> Doc
printSortItem si = case si of
Sort_decl sl _ -> sepByCommas $ map idLabelDoc sl
fsep $ punctuate comma (map idDoc sl) ++ [less, idDoc sup]
Subsort_defn s v sup af _ -> fsep [idLabelDoc s, equals,
specBraces $ fsep [sidDoc v, colon <+> idDoc sup,
printAnnoted (addBullet . printFormula) af]]
Iso_decl sl _ -> fsep $ punctuate (space <> equals) $ map idDoc sl
instance FormExtension f => Pretty (SORT_ITEM f) where
printQuant :: QUANTIFIER -> Doc
Unique_existential -> unique
printSortedVars :: [VAR] -> SORT -> Doc
fsep $ punctuate comma (map sidDoc l) ++ [colon <+> idDoc s]
printVarDeclL :: [VAR_DECL] -> [Doc]
printVarDeclL = punctuate semi . map printVarDecl
printVarDecls :: [VAR_DECL] -> Doc
printVarDecls = fsep . printVarDeclL
printVarDecl :: VAR_DECL -> Doc
printVarDecl (Var_decl l s _) = printSortedVars l s
printArgDecls :: [VAR_DECL] -> Doc
printArgDecls = parens . printVarDecls
printPredHead :: PRED_HEAD -> Doc
printPredHead (Pred_head l _) = printArgDecls l
printPredItem :: FormExtension f => PRED_ITEM f -> Doc
printPredItem p = case p of
Pred_decl l t _ -> fsep $ punctuate comma (map idLabelDoc l)
++ [colon <+> printPredType t]
sep [ cat [idLabelDoc i, printPredHead h]
, equiv <+> printAnnoted printFormula f]
instance FormExtension f => Pretty (PRED_ITEM f) where
printAttr :: FormExtension f => OP_ATTR f -> Doc
Assoc_op_attr -> text assocS
Comm_op_attr -> text commS
Idem_op_attr -> text idemS
Unit_op_attr t -> text unitS <+> printTerm t
instance FormExtension f => Pretty (OP_ATTR f) where
printOpHead :: OP_HEAD -> Doc
printOpHead (Op_head k l mr _) =
sep $ (if null l then [] else [printArgDecls l]) ++ case mr of
Partial -> text colonQuMark) <+> idDoc r]
instance Pretty OP_HEAD where
printOpItem :: FormExtension f => OP_ITEM f -> Doc
printOpItem p = case p of
Op_decl l t a _ -> fsep $ punctuate comma (map idLabelDoc l)
++ [colon <> (if null a then id else (<> comma)) (printOpType t)]
++ punctuate comma (map printAttr a)
Op_defn i h@(Op_head _ l _ _) t _ ->
sep [ (if null l then sep else cat) [idLabelDoc i, printOpHead h]
, equals <+> printAnnoted printTerm t]
instance FormExtension f => Pretty (OP_ITEM f) where
instance Pretty VAR_DECL where
printOpType :: OP_TYPE -> Doc
printOpType (Op_type p l r _) =
Partial -> quMarkD <+> idDoc r
Total -> space <> idDoc r
(punctuate (space <> cross) (map idDoc l)
instance Pretty OP_TYPE where
printOpSymb :: OP_SYMB -> Doc
printOpSymb o = case o of
Qual_op_name i t _ -> fsep [text opS, idDoc i, colon <> printOpType t]
instance Pretty OP_SYMB where
printPredType :: PRED_TYPE -> Doc
printPredType (Pred_type l _) = case l of
_ -> fsep $ punctuate (space <> cross) $ map idDoc l
instance Pretty PRED_TYPE where
printPredSymb :: PRED_SYMB -> Doc
printPredSymb p = case p of
parens $ fsep [text predS, idDoc i, colon <+> printPredType t]
instance Pretty PRED_SYMB where
instance Pretty SYMB_ITEMS where
printSymbItems :: SYMB_ITEMS -> Doc
printSymbItems (Symb_items k l _) =
print_kind_text k l <+> sepByCommas (map printSymb l)
instance Pretty SYMB where
Qual_id i t _ -> fsep [idDoc i, colon <> printType t]
instance Pretty TYPE where
O_type ot -> printOpType ot
P_type pt -> space <> printPredType pt
A_type s -> space <> idDoc s
print_kind_text :: SYMB_KIND -> [a] -> Doc
print_kind_text k l = case k of
_ -> keyword (pluralS_symb_list k l)
pluralS_symb_list :: SYMB_KIND -> [a] -> String
pluralS_symb_list k l = (case k of
Implicit -> error "pluralS_symb_list"
Preds_kind -> predS) ++ appendS l
instance Pretty SYMB_OR_MAP where
printSymbOrMap :: SYMB_OR_MAP -> Doc
printSymbOrMap som = case som of
Symb_map s t _ -> fsep [printSymb s, mapsto <+> printSymb t]
instance Pretty SYMB_KIND where
printSymbKind :: SYMB_KIND -> Doc
printSymbKind sk = print_kind_text sk [()]
instance Pretty SYMB_MAP_ITEMS where
pretty = printSymbMapItems
printSymbMapItems :: SYMB_MAP_ITEMS -> Doc
printSymbMapItems (Symb_map_items k l _) =
print_kind_text k l <+> sepByCommas (map printSymbOrMap 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
printInfix b join l s r =
join $ if b then [l, s <+> r] else [l <+> s, r]
class (GetRange f, Pretty f) => FormExtension f where
isQuantifierLike :: f -> Bool
isQuantifierLike _ = False
instance FormExtension ()
printRecord :: FormExtension f => Record f Doc Doc
{ foldQuantification = \ _ q l r _ ->
fsep $ printQuant q : printVarDeclL l
, foldConjunction = \ o l _ -> case o of
Conjunction ol@(_ : _) _ -> fsep $ prepPunctuate (andDoc <> space)
$ zipWith (mkJunctDoc True) (init ol) (init l) ++
[mkJunctDoc False (last ol) (last l)]
, foldDisjunction = \ o l _ -> case o of
Disjunction ol@(_ : _) _ -> fsep $ prepPunctuate (orDoc <> space)
$ zipWith (mkJunctDoc True) (init ol) (init l) ++
[mkJunctDoc False (last ol) (last l)]
, foldImplication = \ o l r _ _ ->
let Implication oL oR b _ = o
nl = if isAnyImpl oL || b && isQuant oL
nr = if isImpl b oR || not b && isQuant oR
in if b then printInfix True sep nl implies nr
else printInfix True sep nr (text ifS) nl
, foldEquivalence = \ o l r _ -> case o of
Equivalence oL oR _ -> printInfix True sep
(if isQuant oL then parens l else mkEquivDoc oL l)
, foldNegation = \ orig r _ -> case orig of
Negation o _ -> hsep [notDoc, mkJunctDoc False o r]
, foldTrue_atom = \ _ _ -> text trueS
, foldFalse_atom = \ _ _ -> text falseS
, foldPredication = \ o p l _ -> case (p, o) of
(Pred_name i, Predication _ ol _) -> predIdApplDoc i $ zipConds ol l
_ -> if null l then printPredSymb p else
fcat [printPredSymb p, parens $ sepByCommas l]
, foldDefinedness = \ _ r _ -> hsep [text defS, r]
, foldExistl_equation = \ _ l r _ -> printInfix True sep l exequal r
, foldStrong_equation = \ _ l r _ -> printInfix True sep l equals r
, foldMembership = \ _ r t _ -> fsep [r, inDoc, idDoc t]
, foldMixfix_formula = \ _ r -> r
, foldSort_gen_ax = \ o _ _ ->
let Sort_gen_ax constrs b = o
genAx = sep [ keyword generatedS <+> keyword (typeS ++ appendS l)
, semiAnnos printDATATYPE_DECL l]
in if b then text "%% free" $+$ genAx else genAx
, foldQuantOp = \ _ o n r -> fsep
, printOpSymb $ Qual_op_name o n nullRange
, foldQuantPred = \ _ p n r -> fsep
, printPredSymb $ Qual_pred_name p n nullRange
, foldExtFORMULA = const pretty
, foldQual_var = \ _ v s _ ->
parens $ fsep [text varS, sidDoc v, colon <+> idDoc s]
, foldApplication = \ orig o l _ -> case (o, orig) of
(Op_name i, Application _ ol _) -> idApplDoc i $ zipConds ol l
_ -> let d = parens $ printOpSymb o in
if null l then d else fcat [d, parens $ sepByCommas l]
, foldSorted_term = \ _ r t _ -> fsep [idApplDoc typeId [r], idDoc t]
, foldCast = \ _ r t _ ->
fsep [idApplDoc (mkId [placeTok, mkSimpleId asS]) [r], idDoc t]
, foldConditional = \ o l f r _ -> case o of
Conditional ol _ _ _ -> fsep [if isCond ol then parens l else l,
text whenS <+> f, text elseS <+> r]
, foldMixfix_qual_pred = const printPredSymb
, foldMixfix_term = \ o l -> case o of
Mixfix_term [_, Mixfix_parenthesized _ _] -> fcat l
, foldMixfix_token = const sidDoc
, foldMixfix_sorted_term = \ _ s _ -> colon <+> idDoc s
, foldMixfix_cast = \ _ s _ -> text asS <+> idDoc s
, foldMixfix_parenthesized = \ _ l _ -> parens $ sepByCommas l
, foldMixfix_bracketed = \ _ l _ -> brackets $ sepByCommas l
, foldMixfix_braced = \ _ l _ -> specBraces $ sepByCommas l
, foldExtTERM = const pretty }
recoverType :: [Constraint] -> [Annoted DATATYPE_DECL]
map (\ c -> let s = newSort c in emptyAnno $ Datatype_decl s
(map (\ (o, _) -> case o of
Qual_op_name i (Op_type fk args _ ps) r ->
let qs = appRange ps r in emptyAnno $ case args of
[_] | isInjName i -> Subsorts args qs
_ -> Alt_construct fk i (map Sort args) qs
zipConds :: [TERM f] -> [Doc] -> [Doc]
zipConds = zipWith (\ o d -> if isCond o then parens d else d)
printFormula :: FormExtension f => FORMULA f -> Doc
printFormula = foldFormula printRecord
instance FormExtension f => Pretty (FORMULA f) where
printTerm :: FormExtension f => TERM f -> Doc
printTerm = foldTerm printRecord
instance FormExtension f => Pretty (TERM f) where
isQuant :: FormExtension f => FORMULA f -> Bool
Quantification _ _ _ _ -> True
ExtFORMULA ef -> isQuantifierLike ef
Conjunction l _ -> case l of
Disjunction l _ -> case l of
Implication a b impl _ -> isQuant $ if impl then b else a
Equivalence _ b _ -> isQuant b
Negation a _ -> isQuant a
isEquiv :: FORMULA f -> Bool
Equivalence _ _ _ -> True
isAnyImpl :: FORMULA f -> Bool
isAnyImpl f = isImpl True f || isImpl False f
isJunct :: FORMULA f -> Bool
mkJunctDoc :: FormExtension f => Bool -> FORMULA f -> Doc -> Doc
mkJunctDoc b f = if isJunct f || b && isQuant f then parens else id
mkEquivDoc :: FORMULA f -> Doc -> Doc
mkEquivDoc f = if isEquiv f then parens else id
isImpl :: Bool -> FORMULA f -> Bool
Implication _ _ b _ -> a /= b
Conditional _ _ _ _ -> True
-- | a helper class for calculating the pluralS of
e.g. ops
instance ListCheck Token where
instance ListCheck Id where
instance ListCheck a => ListCheck [a] where
innerList = concatMap innerList
-- | an instance of ListCheck for Annoted stuff
instance ListCheck a => ListCheck (Annoted a) where
innerList = innerList . item
{- | pluralS checks nested lists via the class ListCheck to decide
if a plural s should be appended. -}
pluralS :: ListCheck a => a -> String
pluralS = appendS . innerList
appendS l = if isSingle l then "" else "s"
-- instances of ListCheck for various data types of AS_Basic_CASL
instance ListCheck (SORT_ITEM f) where
innerList (Sort_decl l _) = innerList l
innerList (Subsort_decl l _ _) = innerList l
innerList (Subsort_defn _ _ _ _ _) = [()]
innerList (Iso_decl l _) = innerList $ drop 1 l
-- assume last sort is known
instance ListCheck (OP_ITEM f) where
innerList (Op_decl l _ _ _) = innerList l
innerList (Op_defn _ _ _ _) = [()]
instance ListCheck (PRED_ITEM f) where
innerList (Pred_decl l _ _) = innerList l
innerList (Pred_defn _ _ _ _) = [()]
instance ListCheck VAR_DECL where
innerList (Var_decl l _ _) = innerList l
-- | print a formula as a sentence
printTheoryFormula :: FormExtension f => Named (FORMULA f) -> Doc
printTheoryFormula f = printAnnoted
Quantification Universal _ _ _ -> id
_ -> (bullet <+>)) . pretty) $ fromLabelledSen f