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