module GeneratePatterns where

main :: IO ()

main = mapM_ print genPatterns

toNFrm :: [[Named a]] -> Named a

toNFrm = head . head

{- The perl script will use the following subtitutions:

"°!modalAx" =>

"inlineAxioms Modal \"modality empty\\n"++

"pred p,q:()\\n"++

". ",

"°!caslAx" =>

"inlineAxioms CASL \"sort world \\n"++

"pred rel : world * world\\n"++

"forall w1 : world \\n. "

Further it generates a case expression, where the Modalformula forms

the pattern and the CASL formula is embedded in a call to addTerm.

as variables for modal formulas only 'p','q' and 'r' are recognized.

-}

genPatterns :: [(Named ModalFORMULA,Named CASLFORMULA)]

genPatterns = map (\ (x,y) -> (toNFrm x, toNFrm y))

snip><Patterns

[([°!modalAx"[](p=>q) => (([]p) => []q)"],

[[Nothing]]),

([°!modalAx"[] p => <> p"],

[°!caslAx"exists w2 : world . rel(w1,w2) %(Serial_D)%"]),

([°!modalAx"[] p => p"],

[°!caslAx"rel(w1,w1) %(Reflexive_M)%"]),

([°!modalAx"[] p => [][] p "],

[°!caslAx"forall w2,w3: world . (rel(w1,w2) /\\ rel(w2,w3)) => rel(w1,w3) %(Transitive_4)%"]),

([°!modalAx" p => []<> p "],

[°!caslAx"forall w2:world . rel(w1,w2) => rel(w2,w1) %(Symmetric_B)%"]),

([°!modalAx"<> p => []<> p"],

[°!caslAx"forall w2,w3:world . (rel(w1,w2) /\\ rel(w1,w3)) => rel(w2,w3) %(Euclidean_5)%"])

]

snip>/<Patterns