1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE DeriveDataTypeable #-}
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Propositional/AS_BASIC_Propositional.der.hs
9eb6a481980d81a55898ba418fba72fc3c09d8c8Dominik LueckeDescription : Abstract syntax for propositional logic
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik LueckeCopyright : (c) Dominik Luecke, Uni Bremen 2007
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : luecke@informatik.uni-bremen.de
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik LueckeStability : experimental
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik LueckePortability : portable
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik LueckeDefinition of abstract syntax for propositional logic
2af38fde95f93562f2124ec615fba0e509c8202eDominik Luecke http://en.wikipedia.org/wiki/Propositional_logic
6329255607e98810295820b38098229a5ddc5d3bChristian Maeder ( FORMULA (..) -- datatype for Propositional Formulas
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke , BASIC_ITEMS (..) -- Items of a Basic Spec
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke , BASIC_SPEC (..) -- Basic Spec
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke , SYMB_ITEMS (..) -- List of symbols
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke , SYMB (..) -- Symbols
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke , SYMB_MAP_ITEMS (..) -- Symbol map
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke , SYMB_OR_MAP (..) -- Symbol or symbol map
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke , PRED_ITEM (..) -- Predicates
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Luecke-- DrIFT command
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder{-! global: GetRange !-}
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke-- | predicates = propotions
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Lueckedata PRED_ITEM = Pred_item [Id.Token] Id.Range
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Typeable, Data)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedernewtype BASIC_SPEC = Basic_spec [AS_Anno.Annoted BASIC_ITEMS]
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Typeable, Data)
da955132262baab309a50fdffe228c9efe68251dCui Jiandata BASIC_ITEMS =
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke Pred_decl PRED_ITEM
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | Axiom_items [AS_Anno.Annoted FORMULA]
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Typeable, Data)
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke-- | Datatype for propositional formulas
ffb6099205b26594acf25e64efd338cee362a659Christian Maederdata FORMULA =
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder -- pos: "False
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder -- pos: "True"
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder -- pos: Propositional Identifiers
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder | Negation FORMULA Id.Range
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder | Conjunction [FORMULA] Id.Range
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder -- pos: "/\"s
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder | Disjunction [FORMULA] Id.Range
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder -- pos: "\/"s
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder | Implication FORMULA FORMULA Id.Range
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder | Equivalence FORMULA FORMULA Id.Range
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder -- pos: "<=>"
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckedata SYMB_ITEMS = Symb_items [SYMB] Id.Range
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke -- pos: SYMB_KIND, commas
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
548f3850942936a8c6021185c8391dfcd3b03018Dominik Lueckenewtype SYMB = Symb_id Id.Token
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke -- pos: colon
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckedata SYMB_MAP_ITEMS = Symb_map_items [SYMB_OR_MAP] Id.Range
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke -- pos: SYMB_KIND, commas
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckedata SYMB_OR_MAP = Symb SYMB
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke | Symb_map SYMB SYMB Id.Range
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke -- pos: "|->"
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- All about pretty printing
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederwe chose the easy way here :) -}
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckeinstance Pretty FORMULA where
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke pretty = printFormula
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckeinstance Pretty BASIC_SPEC where
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke pretty = printBasicSpec
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckeinstance Pretty SYMB where
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke pretty = printSymbol
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckeinstance Pretty SYMB_ITEMS where
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke pretty = printSymbItems
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckeinstance Pretty SYMB_MAP_ITEMS where
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke pretty = printSymbMapItems
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckeinstance Pretty BASIC_ITEMS where
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke pretty = printBasicItems
da955132262baab309a50fdffe228c9efe68251dCui Jianinstance Pretty SYMB_OR_MAP where
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke pretty = printSymbOrMap
e0d31c8d6d8ded93c599cbfa9ebc72a2bf1b0a55Dominik Lueckeinstance Pretty PRED_ITEM where
e0d31c8d6d8ded93c599cbfa9ebc72a2bf1b0a55Dominik Luecke pretty = printPredItem
97c9d39efee30883aa578294c46506ff8a9478c8Christian MaederisPrimForm :: FORMULA -> Bool
97c9d39efee30883aa578294c46506ff8a9478c8Christian MaederisPrimForm f = case f of
6329255607e98810295820b38098229a5ddc5d3bChristian Maeder True_atom _ -> True
6329255607e98810295820b38098229a5ddc5d3bChristian Maeder False_atom _ -> True
6329255607e98810295820b38098229a5ddc5d3bChristian Maeder Predication _ -> True
6329255607e98810295820b38098229a5ddc5d3bChristian Maeder Negation _ _ -> True
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder-- Pretty printing for formulas
97c9d39efee30883aa578294c46506ff8a9478c8Christian MaederprintFormula :: FORMULA -> Doc
97c9d39efee30883aa578294c46506ff8a9478c8Christian MaederprintFormula frm =
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder let ppf p f = (if p f then id else parens) $ printFormula f
3519b5ffec1455664eabfe9c36b8b4c08b42081aChristian Maeder isJunctForm f = case f of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Implication {} -> False
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Equivalence {} -> False
6329255607e98810295820b38098229a5ddc5d3bChristian Maeder in case frm of
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder False_atom _ -> text falseS
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder True_atom _ -> text trueS
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder Predication x -> pretty x
6329255607e98810295820b38098229a5ddc5d3bChristian Maeder Negation f _ -> notDoc <+> ppf isPrimForm f
3519b5ffec1455664eabfe9c36b8b4c08b42081aChristian Maeder Conjunction xs _ -> sepByArbitrary andDoc $ map (ppf isPrimForm) xs
3519b5ffec1455664eabfe9c36b8b4c08b42081aChristian Maeder Disjunction xs _ -> sepByArbitrary orDoc $ map (ppf isPrimForm) xs
3519b5ffec1455664eabfe9c36b8b4c08b42081aChristian Maeder Implication x y _ -> ppf isJunctForm x <+> implies <+> ppf isJunctForm y
3519b5ffec1455664eabfe9c36b8b4c08b42081aChristian Maeder Equivalence x y _ -> ppf isJunctForm x <+> equiv <+> ppf isJunctForm y
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik LueckesepByArbitrary :: Doc -> [Doc] -> Doc
6329255607e98810295820b38098229a5ddc5d3bChristian MaedersepByArbitrary d = fsep . prepPunctuate (d <> space)
e0d31c8d6d8ded93c599cbfa9ebc72a2bf1b0a55Dominik LueckeprintPredItem :: PRED_ITEM -> Doc
0fb1cdb3c2beb68346fdf420c2903a4285f990eacmaederprintPredItem (Pred_item xs _) =
0fb1cdb3c2beb68346fdf420c2903a4285f990eacmaeder keyword (propS ++ case xs of
0fb1cdb3c2beb68346fdf420c2903a4285f990eacmaeder _ -> "s") <+> ppWithCommas xs
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintBasicSpec :: BASIC_SPEC -> Doc
6329255607e98810295820b38098229a5ddc5d3bChristian MaederprintBasicSpec (Basic_spec xs) = vcat $ map pretty xs
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintBasicItems :: BASIC_ITEMS -> Doc
0fb1cdb3c2beb68346fdf420c2903a4285f990eacmaederprintBasicItems (Axiom_items xs) = vcat $ map (addBullet . pretty) xs
e0d31c8d6d8ded93c599cbfa9ebc72a2bf1b0a55Dominik LueckeprintBasicItems (Pred_decl x) = pretty x
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbol :: SYMB -> Doc
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik LueckeprintSymbol (Symb_id sym) = pretty sym
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbItems :: SYMB_ITEMS -> Doc
6329255607e98810295820b38098229a5ddc5d3bChristian MaederprintSymbItems (Symb_items xs _) = fsep $ map pretty xs
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbOrMap :: SYMB_OR_MAP -> Doc
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbOrMap (Symb sym) = pretty sym
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprintSymbOrMap (Symb_map source dest _) =
6329255607e98810295820b38098229a5ddc5d3bChristian Maeder pretty source <+> mapsto <+> pretty dest
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbMapItems :: SYMB_MAP_ITEMS -> Doc
6329255607e98810295820b38098229a5ddc5d3bChristian MaederprintSymbMapItems (Symb_map_items xs _) = fsep $ map pretty xs