AS_BASIC_Propositional.der.hs revision 90c174bac60a72ffd81bc3bf5ae2dd9a61943b8b
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
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
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
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
1fb884d0af74a8b911f5de1cf2b68e33676c088bDominik Luecke-- DrIFT command
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder{-! global: GetRange !-}
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke-- | predicates = propotions
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Lueckedata PRED_ITEM = Pred_item [Id.Token] Id.Range
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke deriving Show
548f3850942936a8c6021185c8391dfcd3b03018Dominik Lueckenewtype BASIC_SPEC = Basic_spec [AS_Anno.Annoted (BASIC_ITEMS)]
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke deriving Show
da955132262baab309a50fdffe228c9efe68251dCui Jiandata BASIC_ITEMS =
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke Pred_decl PRED_ITEM
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke | Axiom_items [AS_Anno.Annoted (FORMULA)]
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik Luecke deriving Show
59917a4f0a6a20f5a20bcab1f2a0a0774db56807Dominik Luecke-- | Datatype for propositional formulas
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckedata FORMULA = Negation FORMULA Id.Range
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
a785627ef4d2e3c73d9e5b8f7352fc859b85dd2bDominik Luecke | Equivalence FORMULA FORMULA Id.Range
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke -- pos: "<=>"
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke -- pos: "True"
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke -- pos: "False
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke -- pos: Propositional Identifiers
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke deriving (Show, Eq, Ord)
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
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
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Lueckedata SYMB_ITEMS = Symb_items [SYMB] Id.Range
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke -- pos: SYMB_KIND, commas
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke deriving (Show, Eq)
548f3850942936a8c6021185c8391dfcd3b03018Dominik Lueckenewtype SYMB = Symb_id Id.Token
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke -- pos: colon
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke deriving (Show, Eq)
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 Lueckedata SYMB_OR_MAP = Symb SYMB
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke | Symb_map SYMB SYMB Id.Range
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke -- pos: "|->"
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik Luecke deriving (Show, Eq)
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
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-- 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)
e0d31c8d6d8ded93c599cbfa9ebc72a2bf1b0a55Dominik LueckeprintPredItem :: PRED_ITEM -> Doc
e0d31c8d6d8ded93c599cbfa9ebc72a2bf1b0a55Dominik LueckeprintPredItem (Pred_item xs _) = hsep $ map pretty xs
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintBasicSpec :: BASIC_SPEC -> Doc
e0d31c8d6d8ded93c599cbfa9ebc72a2bf1b0a55Dominik LueckeprintBasicSpec (Basic_spec xs) = hsep $ map pretty xs
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintBasicItems :: BASIC_ITEMS -> Doc
1d677cafe64269a9c961396b85b5b50c126f58d8Dominik LueckeprintBasicItems (Axiom_items xs) = hsep $ map 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
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbItems (Symb_items xs _) = hsep $ map pretty xs
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbOrMap :: SYMB_OR_MAP -> Doc
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbOrMap (Symb sym) = pretty sym
da955132262baab309a50fdffe228c9efe68251dCui JianprintSymbOrMap (Symb_map source dest _) = pretty source <> mapsto <> pretty dest
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbMapItems :: SYMB_MAP_ITEMS -> Doc
8b6e542715e576ffbf6ae13634c85f3445036e77Dominik LueckeprintSymbMapItems (Symb_map_items xs _) = hsep $ map pretty xs