ClTests-Sublogic-ghci-script revision 9a4b469ca0a7f44a598e551a973c75195207db58
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa:l CommonLogic/ClTests.hs
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa:m +CommonLogic.Sublogic
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa-- extract pieces from abstract syntax:
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksalet Right txt = abstrSyntax "(and (P x) (Q P)))"
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksalet (Text [phr] _) = txt
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksalet (Sentence sen) = phr
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksalet (Bool_sent boolsen _) = sen
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksalet (Conjunction [atsen1, atsen2]) = boolsen
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksalet (Atom_sent (Atom ntP1 [Term_seq ntx]) _) = atsen1
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksalet (Atom_sent (Atom ntQ [Term_seq ntP2]) _) = atsen2
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa
9a4b469ca0a7f44a598e551a973c75195207db58Eugen Kuksa-- parsing error: Predicates *must* be used
9a4b469ca0a7f44a598e551a973c75195207db58Eugen Kuksalet (Left err) = abstrSyntax "(and (x) (y))"
9a4b469ca0a7f44a598e551a973c75195207db58Eugen Kuksaerr
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa
9a4b469ca0a7f44a598e551a973c75195207db58Eugen Kuksa-- first order
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksalet (Right txt1) = abstrSyntax "(and (P x) (Q y))"
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksaprd_text txt1
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksasublogic txt1
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa-- first order (quantified over some object x)
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa-- "(exists (x) (x))" cannot be parsed
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksalet (Right txt2) = abstrSyntax "(exists (x) (P x))"
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksaprd_text txt2
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksasublogic txt2
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa-- first order (some predicates used)
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa-- "(and (x), (Q x))" cannot be parsed
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksalet (Right txt3) = abstrSyntax "(and (P x) (Q (P x)))"
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksaprd_text txt3
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksasublogic txt3
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa-- full common logic: quantified (used predicate as object)
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksalet (Right txt4) = abstrSyntax "(and (P x) (Q P)))"
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksaprd_text txt4
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksasublogic txt4
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa-- full common logic: quantified over predicate P
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksalet (Right txt5) = abstrSyntax "(exists (P) (and (P x)))"
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksaprd_text txt5
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksasublogic txt5
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksa