AS_BASIC_Propositional.der.hs revision 90c174bac60a72ffd81bc3bf5ae2dd9a61943b8b
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Luecke{- |
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik LueckeModule : $Header$
9eb6a481980d81a55898ba418fba72fc3c09d8c8Dominik LueckeDescription : Abstract syntax for propositional logic
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik LueckeCopyright : (c) Dominik Luecke, Uni Bremen 2007
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik LueckeLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Luecke
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : luecke@informatik.uni-bremen.de
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik LueckeStability : experimental
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik LueckePortability : portable
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Luecke
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik LueckeDefinition of abstract syntax for propositional logic
2af38fde95f93562f2124ec615fba0e509c8202eDominik Luecke-}
cf04ba46b9eb495d334466e24e082e391055ca7bDominik Luecke
2af38fde95f93562f2124ec615fba0e509c8202eDominik Luecke{-
2af38fde95f93562f2124ec615fba0e509c8202eDominik Luecke Ref.
2af38fde95f93562f2124ec615fba0e509c8202eDominik Luecke http://en.wikipedia.org/wiki/Propositional_logic
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Luecke-}
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Luecke
da955132262baab309a50fdffe228c9efe68251dCui Jianmodule Propositional.AS_BASIC_Propositional
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke (
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke FORMULA (..) -- datatype for Propositional Formulas
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke , is_True_atom -- True?
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke , is_False_atom -- False?
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
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke ) where
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Luecke
85f112f807210b70172aab985810a37dc6a85eb3Dominik Lueckeimport Common.Id as Id
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Lueckeimport Common.Doc
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Lueckeimport Common.DocUtils
85f112f807210b70172aab985810a37dc6a85eb3Dominik Lueckeimport Common.AS_Annotation as AS_Anno
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Luecke
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Luecke-- DrIFT command
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder{-! global: GetRange !-}
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Luecke
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke-- | predicates = propotions
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Lueckedata PRED_ITEM = Pred_item [Id.Token] Id.Range
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke deriving Show
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke
548f3850942936a8c6021185c8391dfcd3b03018Dominik Lueckenewtype BASIC_SPEC = Basic_spec [AS_Anno.Annoted (BASIC_ITEMS)]
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke deriving Show
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke
da955132262baab309a50fdffe228c9efe68251dCui Jiandata BASIC_ITEMS =
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke Pred_decl PRED_ITEM
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke | Axiom_items [AS_Anno.Annoted (FORMULA)]
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke -- pos: dots
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke deriving Show
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke-- | Datatype for propositional formulas
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckedata FORMULA = Negation FORMULA Id.Range
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke -- pos: not
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke | Conjunction [FORMULA] Id.Range
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke -- pos: "/\"s
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke | Disjunction [FORMULA] Id.Range
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke -- pos: "\/"s
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke | Implication FORMULA FORMULA Id.Range
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke -- pos: "=>"
a785627ef4d2e3c73d9e5b8f7352fc859b85dd2bDominik Luecke | Equivalence FORMULA FORMULA Id.Range
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke -- pos: "<=>"
b694e4b3f771a2f32042c9c505dd698bde969558Dominik Luecke | True_atom Id.Range
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke -- pos: "True"
b694e4b3f771a2f32042c9c505dd698bde969558Dominik Luecke | False_atom Id.Range
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke -- pos: "False
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke | Predication Id.Token
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke -- pos: Propositional Identifiers
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke deriving (Show, Eq, Ord)
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke-- | Value of the true atom
cf04ba46b9eb495d334466e24e082e391055ca7bDominik Luecke-- True is always true -P
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckeis_True_atom :: FORMULA -> Bool
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Lueckeis_True_atom (True_atom _) = True
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Lueckeis_True_atom _ = False
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Luecke
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke-- | Value of the false atom
da955132262baab309a50fdffe228c9efe68251dCui Jian-- and False if always false
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckeis_False_atom :: FORMULA -> Bool
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Lueckeis_False_atom (False_atom _) = False
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Lueckeis_False_atom _ = False
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckedata SYMB_ITEMS = Symb_items [SYMB] Id.Range
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke -- pos: SYMB_KIND, commas
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke deriving (Show, Eq)
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke
548f3850942936a8c6021185c8391dfcd3b03018Dominik Lueckenewtype SYMB = Symb_id Id.Token
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke -- pos: colon
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke deriving (Show, Eq)
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckedata SYMB_MAP_ITEMS = Symb_map_items [SYMB_OR_MAP] Id.Range
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke -- pos: SYMB_KIND, commas
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke deriving (Show, Eq)
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckedata SYMB_OR_MAP = Symb SYMB
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke | Symb_map SYMB SYMB Id.Range
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke -- pos: "|->"
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke deriving (Show, Eq)
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke-- All about pretty printing
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke-- we 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
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke-- Pretty printing for formulas
da955132262baab309a50fdffe228c9efe68251dCui JianprintFormula :: FORMULA -> Doc
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik LueckeprintFormula (Negation f _) = notDoc
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke <> lparen <> printFormula f <> rparen
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik LueckeprintFormula (Conjunction xs _) = parens $
da955132262baab309a50fdffe228c9efe68251dCui Jian sepByArbitrary andDoc
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke $ map printFormula xs
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik LueckeprintFormula (Disjunction xs _) = parens $
da955132262baab309a50fdffe228c9efe68251dCui Jian sepByArbitrary orDoc
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke $ map printFormula xs
da955132262baab309a50fdffe228c9efe68251dCui JianprintFormula (Implication x y _) = parens $ printFormula x <>
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke implies <> printFormula y
da955132262baab309a50fdffe228c9efe68251dCui JianprintFormula (Equivalence x y _) = parens $ printFormula x <>
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke equiv <> printFormula y
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik LueckeprintFormula (True_atom _) = text "True"
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik LueckeprintFormula (False_atom _) = text "False"
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik LueckeprintFormula (Predication x) = pretty x
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke-- Extended version of vcat
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik LueckesepByArbitrary :: Doc -> [Doc] -> Doc
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik LueckesepByArbitrary _ [] = text ""
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik LueckesepByArbitrary _ (x:[]) = x
da955132262baab309a50fdffe228c9efe68251dCui JiansepByArbitrary separator (x:xs) = x <> separator
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke <> (sepByArbitrary separator xs)
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke
e0d31c8d6d8ded93c599cbfa9ebc72a2bf1b0a55Dominik LueckeprintPredItem :: PRED_ITEM -> Doc
e0d31c8d6d8ded93c599cbfa9ebc72a2bf1b0a55Dominik LueckeprintPredItem (Pred_item xs _) = hsep $ map pretty xs
e0d31c8d6d8ded93c599cbfa9ebc72a2bf1b0a55Dominik Luecke
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintBasicSpec :: BASIC_SPEC -> Doc
e0d31c8d6d8ded93c599cbfa9ebc72a2bf1b0a55Dominik LueckeprintBasicSpec (Basic_spec xs) = hsep $ map pretty xs
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintBasicItems :: BASIC_ITEMS -> Doc
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik LueckeprintBasicItems (Axiom_items xs) = hsep $ map pretty xs
e0d31c8d6d8ded93c599cbfa9ebc72a2bf1b0a55Dominik LueckeprintBasicItems (Pred_decl x) = pretty x
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbol :: SYMB -> Doc
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik LueckeprintSymbol (Symb_id sym) = pretty sym
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbItems :: SYMB_ITEMS -> Doc
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbItems (Symb_items xs _) = hsep $ map pretty xs
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbOrMap :: SYMB_OR_MAP -> Doc
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbOrMap (Symb sym) = pretty sym
da955132262baab309a50fdffe228c9efe68251dCui JianprintSymbOrMap (Symb_map source dest _) = pretty source <> mapsto <> pretty dest
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbMapItems :: SYMB_MAP_ITEMS -> Doc
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbMapItems (Symb_map_items xs _) = hsep $ map pretty xs