:l CommonLogic/ClTests.hs

:m +CommonLogic.Sublogic

-- extract pieces from abstract syntax:

let Right txt = abstrSyntax "(and (P x) (Q P)))"

let (Text [phr] _) = txt

let (Sentence sen) = phr

let (Bool_sent boolsen _) = sen

let (Conjunction [atsen1, atsen2]) = boolsen

let (Atom_sent (Atom ntP1 [Term_seq ntx]) _) = atsen1

let (Atom_sent (Atom ntQ [Term_seq ntP2]) _) = atsen2

-- parsing error: Predicates *must* be used

let (Right txt0) = abstrSyntax "(and (x) (y))"

err

-- first order

let (Right txt1) = abstrSyntax "(and (P x) (Q y))"

prd_text txt1

sublogic txt1

-- first order (quantified over some object x)

-- "(exists (x) (x))" cannot be parsed

let (Right txt2) = abstrSyntax "(exists (x) (P x))"

prd_text txt2

sublogic txt2

-- first order (some predicates used)

-- "(and (x), (Q x))" cannot be parsed

let (Right txt3) = abstrSyntax "(and (P x) (Q (P x)))"

prd_text txt3

sublogic txt3

-- full common logic: quantified (used predicate as object)

let (Right txt4) = abstrSyntax "(and (P x) (Q P)))"

prd_text txt4

sublogic txt4

-- full common logic: quantified over predicate P

let (Right txt5) = abstrSyntax "(exists (P) (and (P x)))"

prd_text txt5

sublogic txt5

-- module elimination

let (Right mt) = abstrSyntax "(cl-module D (forall (x) (and (P x) (Q x))))"

let (Text [Module (Mod _ (Text [Sentence sen] _) _)] _) = mt

let d = mkSimpleId "D"

let sen_new = rq_sentence sen [d]

let (Right mt') = abstrSyntax "(forall (x) (if (and (D x)) (and (P x) (Q x))))"

let (Text [Sentence sen'] _) = mt'

sen_new == sen'

--TODO: analyze multiple modules in a text

abstrSyntax "(cl-module D (P x)) (cl-module E (Q x)) (cl-module Fa (cl-module Fb (forall (z) (R z))))"