{-# LANGUAGE DeriveDataTypeable #-} {- | Module : ./Propositional/AS_BASIC_Propositional.hs Description : Abstract syntax for propositional logic Copyright : (c) Dominik Luecke, Uni Bremen 2007 License : GPLv2 or higher, see LICENSE.txt Maintainer : luecke@informatik.uni-bremen.de Stability : experimental Portability : portable Definition of abstract syntax for propositional logic -} {- Ref. http://en.wikipedia.org/wiki/Propositional_logic -} module Propositional.AS_BASIC_Propositional ( FORMULA (..) -- datatype for Propositional Formulas , BASIC_ITEMS (..) -- Items of a Basic Spec , BASIC_SPEC (..) -- Basic Spec , SYMB_ITEMS (..) -- List of symbols , SYMB (..) -- Symbols , SYMB_MAP_ITEMS (..) -- Symbol map , SYMB_OR_MAP (..) -- Symbol or symbol map , PRED_ITEM (..) -- Predicates , isPrimForm ) where import Common.Id as Id import Common.Doc import Common.DocUtils import Common.Keywords import Common.AS_Annotation as AS_Anno import Data.Data -- DrIFT command {-! global: GetRange !-} -- | predicates = propotions data PRED_ITEM = Pred_item [Id.Token] Id.Range deriving (Show, Typeable, Data) newtype BASIC_SPEC = Basic_spec [AS_Anno.Annoted BASIC_ITEMS] deriving (Show, Typeable, Data) data BASIC_ITEMS = Pred_decl PRED_ITEM | Axiom_items [AS_Anno.Annoted FORMULA] -- pos: dots deriving (Show, Typeable, Data) -- | Datatype for propositional formulas data FORMULA = False_atom Id.Range -- pos: "False | True_atom Id.Range -- pos: "True" | Predication Id.Token -- pos: Propositional Identifiers | Negation FORMULA Id.Range -- pos: not | Conjunction [FORMULA] Id.Range -- pos: "/\"s | Disjunction [FORMULA] Id.Range -- pos: "\/"s | Implication FORMULA FORMULA Id.Range -- pos: "=>" | Equivalence FORMULA FORMULA Id.Range -- pos: "<=>" deriving (Show, Eq, Ord, Typeable, Data) data SYMB_ITEMS = Symb_items [SYMB] Id.Range -- pos: SYMB_KIND, commas deriving (Show, Eq, Ord, Typeable, Data) newtype SYMB = Symb_id Id.Token -- pos: colon deriving (Show, Eq, Ord, Typeable, Data) data SYMB_MAP_ITEMS = Symb_map_items [SYMB_OR_MAP] Id.Range -- pos: SYMB_KIND, commas deriving (Show, Eq, Ord, Typeable, Data) data SYMB_OR_MAP = Symb SYMB | Symb_map SYMB SYMB Id.Range -- pos: "|->" deriving (Show, Eq, Ord, Typeable, Data) {- All about pretty printing we chose the easy way here :) -} instance Pretty FORMULA where pretty = printFormula instance Pretty BASIC_SPEC where pretty = printBasicSpec instance Pretty SYMB where pretty = printSymbol instance Pretty SYMB_ITEMS where pretty = printSymbItems instance Pretty SYMB_MAP_ITEMS where pretty = printSymbMapItems instance Pretty BASIC_ITEMS where pretty = printBasicItems instance Pretty SYMB_OR_MAP where pretty = printSymbOrMap instance Pretty PRED_ITEM where pretty = printPredItem isPrimForm :: FORMULA -> Bool isPrimForm f = case f of True_atom _ -> True False_atom _ -> True Predication _ -> True Negation _ _ -> True _ -> False -- Pretty printing for formulas printFormula :: FORMULA -> Doc printFormula frm = let ppf p f = (if p f then id else parens) \$ printFormula f isJunctForm f = case f of Implication {} -> False Equivalence {} -> False _ -> True in case frm of False_atom _ -> text falseS True_atom _ -> text trueS Predication x -> pretty x Negation f _ -> notDoc <+> ppf isPrimForm f Conjunction xs _ -> sepByArbitrary andDoc \$ map (ppf isPrimForm) xs Disjunction xs _ -> sepByArbitrary orDoc \$ map (ppf isPrimForm) xs Implication x y _ -> ppf isJunctForm x <+> implies <+> ppf isJunctForm y Equivalence x y _ -> ppf isJunctForm x <+> equiv <+> ppf isJunctForm y sepByArbitrary :: Doc -> [Doc] -> Doc sepByArbitrary d = fsep . prepPunctuate (d <> space) printPredItem :: PRED_ITEM -> Doc printPredItem (Pred_item xs _) = fsep \$ map pretty xs printBasicSpec :: BASIC_SPEC -> Doc printBasicSpec (Basic_spec xs) = vcat \$ map pretty xs printBasicItems :: BASIC_ITEMS -> Doc printBasicItems (Axiom_items xs) = vcat \$ map pretty xs printBasicItems (Pred_decl x) = pretty x printSymbol :: SYMB -> Doc printSymbol (Symb_id sym) = pretty sym printSymbItems :: SYMB_ITEMS -> Doc printSymbItems (Symb_items xs _) = fsep \$ map pretty xs printSymbOrMap :: SYMB_OR_MAP -> Doc printSymbOrMap (Symb sym) = pretty sym printSymbOrMap (Symb_map source dest _) = pretty source <+> mapsto <+> pretty dest printSymbMapItems :: SYMB_MAP_ITEMS -> Doc printSymbMapItems (Symb_map_items xs _) = fsep \$ map pretty xs -- Generated by DrIFT, look but don't touch! instance GetRange PRED_ITEM where getRange = const nullRange rangeSpan x = case x of Pred_item a b -> joinRanges [rangeSpan a, rangeSpan b] instance GetRange BASIC_SPEC where getRange = const nullRange rangeSpan x = case x of Basic_spec a -> joinRanges [rangeSpan a] instance GetRange BASIC_ITEMS where getRange = const nullRange rangeSpan x = case x of Pred_decl a -> joinRanges [rangeSpan a] Axiom_items a -> joinRanges [rangeSpan a] instance GetRange FORMULA where getRange = const nullRange rangeSpan x = case x of False_atom a -> joinRanges [rangeSpan a] True_atom a -> joinRanges [rangeSpan a] Predication a -> joinRanges [rangeSpan a] Negation a b -> joinRanges [rangeSpan a, rangeSpan b] Conjunction a b -> joinRanges [rangeSpan a, rangeSpan b] Disjunction a b -> joinRanges [rangeSpan a, rangeSpan b] Implication a b c -> joinRanges [rangeSpan a, rangeSpan b, rangeSpan c] Equivalence a b c -> joinRanges [rangeSpan a, rangeSpan b, rangeSpan c] instance GetRange SYMB_ITEMS where getRange = const nullRange rangeSpan x = case x of Symb_items a b -> joinRanges [rangeSpan a, rangeSpan b] instance GetRange SYMB where getRange = const nullRange rangeSpan x = case x of Symb_id a -> joinRanges [rangeSpan a] instance GetRange SYMB_MAP_ITEMS where getRange = const nullRange rangeSpan x = case x of Symb_map_items a b -> joinRanges [rangeSpan a, rangeSpan b] instance GetRange SYMB_OR_MAP where getRange = const nullRange rangeSpan x = case x of Symb a -> joinRanges [rangeSpan a] Symb_map a b c -> joinRanges [rangeSpan a, rangeSpan b, rangeSpan c]