ClTests-Sublogic-ghci-script revision 9a4b469ca0a7f44a598e551a973c75195207db58
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder:l CommonLogic/ClTests.hs
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian Maeder:m +CommonLogic.Sublogic
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- extract pieces from abstract syntax:
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederlet Right txt = abstrSyntax "(and (P x) (Q P)))"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederlet (Text [phr] _) = txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederlet (Sentence sen) = phr
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederlet (Bool_sent boolsen _) = sen
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maederlet (Conjunction [atsen1, atsen2]) = boolsen
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederlet (Atom_sent (Atom ntP1 [Term_seq ntx]) _) = atsen1
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maederlet (Atom_sent (Atom ntQ [Term_seq ntP2]) _) = atsen2
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder-- parsing error: Predicates *must* be used
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederlet (Left err) = abstrSyntax "(and (x) (y))"
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maedererr
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- first order
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maederlet (Right txt1) = abstrSyntax "(and (P x) (Q y))"
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederprd_text txt1
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichsublogic txt1
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder-- first order (quantified over some object x)
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich-- "(exists (x) (x))" cannot be parsed
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederlet (Right txt2) = abstrSyntax "(exists (x) (P x))"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederprd_text txt2
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maedersublogic txt2
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maeder
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder-- first order (some predicates used)
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder-- "(and (x), (Q x))" cannot be parsed
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maederlet (Right txt3) = abstrSyntax "(and (P x) (Q (P x)))"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederprd_text txt3
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maedersublogic txt3
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder-- full common logic: quantified (used predicate as object)
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederlet (Right txt4) = abstrSyntax "(and (P x) (Q P)))"
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederprd_text txt4
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroedersublogic txt4
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder-- full common logic: quantified over predicate P
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederlet (Right txt5) = abstrSyntax "(exists (P) (and (P x)))"
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederprd_text txt5
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroedersublogic txt5
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder