ClTests-Sublogic-ghci-script revision ead7fb0fe5492f65c8e47eaa9d5105bffde163f2
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
9a4b469ca0a7f44a598e551a973c75195207db58Eugen Kuksa-- parsing error: Predicates *must* be used
ead7fb0fe5492f65c8e47eaa9d5105bffde163f2Eugen Kuksalet (Right txt0) = abstrSyntax "(and (x) (y))"
9a4b469ca0a7f44a598e551a973c75195207db58Eugen Kuksa-- first order
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksalet (Right txt1) = abstrSyntax "(and (P x) (Q y))"
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksaprd_text txt1
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksasublogic txt1
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-- 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-- 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-- full common logic: quantified over predicate P
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksalet (Right txt5) = abstrSyntax "(exists (P) (and (P x)))"
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksaprd_text txt5
bdbe06eab641ea31682220252b728d421e4c028eEugen Kuksasublogic txt5
d53747c386354ff7db8629dfdf20f44a7c4d715dEugen Kuksa-- module elimination
d53747c386354ff7db8629dfdf20f44a7c4d715dEugen Kuksalet (Right mt) = abstrSyntax "(cl-module D (forall (x) (and (P x) (Q x))))"
d53747c386354ff7db8629dfdf20f44a7c4d715dEugen Kuksalet (Text [Module (Mod _ (Text [Sentence sen] _) _)] _) = mt
d53747c386354ff7db8629dfdf20f44a7c4d715dEugen Kuksalet d = mkSimpleId "D"
d53747c386354ff7db8629dfdf20f44a7c4d715dEugen Kuksalet sen_new = rq_sentence sen [d]
d53747c386354ff7db8629dfdf20f44a7c4d715dEugen Kuksalet (Right mt') = abstrSyntax "(forall (x) (if (and (D x)) (and (P x) (Q x))))"
d53747c386354ff7db8629dfdf20f44a7c4d715dEugen Kuksalet (Text [Sentence sen'] _) = mt'
d53747c386354ff7db8629dfdf20f44a7c4d715dEugen Kuksasen_new == sen'
d53747c386354ff7db8629dfdf20f44a7c4d715dEugen Kuksa--TODO: analyze multiple modules in a text
ead7fb0fe5492f65c8e47eaa9d5105bffde163f2Eugen KuksaabstrSyntax "(cl-module D (P x)) (cl-module E (Q x)) (cl-module Fa (cl-module Fb (forall (z) (R z))))"