To scasp

lib/haskell/natural4/app/Main.hs

@@ -57,7 +57,7 @@ import LS.XPile.Maude qualified as Maude
 import LS.XPile.NaturalLanguage (toNatLang)
 import LS.XPile.Org (toOrg)
 import LS.XPile.Petri (toPetri)
-import LS.XPile.Prolog (sfl4ToProlog)
+import LS.XPile.Prolog (rulesToProlog, rulesToSCasp)
 import LS.XPile.Purescript (translate2PS)
 import LS.XPile.SVG qualified as AAS
 import LS.XPile.Typescript (asTypescript)
@@ -172,7 +172,8 @@ main = do
 
   -- end of the section that deals with NLG
 
-  let (toprologFN,  asProlog)                 = (workuuid <> "/" <> "prolog",   show (sfl4ToProlog rules))
+  let (toprologFN,  asProlog)                 = (workuuid <> "/" <> "prolog",   rulesToProlog rules)
+      (toscaspFN,   asSCasp)                  = (workuuid <> "/" <> "scasp",    rulesToSCasp rules)
       (topetriFN,   (asPetri, asPetriErr))    = (workuuid <> "/" <> "petri",    xpLog $ toPetri rules)
       (toaasvgFN,   asaasvg)                  = (workuuid <> "/" <> "aasvg",    AAS.asAAsvg defaultAAVConfig l4i rules)
       (tocorel4FN,  (asCoreL4, asCoreL4Err))  = (workuuid <> "/" <> "corel4",   xpLog (sfl4ToCorel4 rules))
@@ -288,6 +289,7 @@ main = do
         (concatMap snd toWriteVue)
 
     when (SFL4.toprolog  opts) $ mywritefile  True toprologFN   iso8601 "pl"   asProlog
+    when (SFL4.toscasp   opts) $ mywritefile  True toscaspFN    iso8601 "pl"   asSCasp
     when (SFL4.topetri   opts) $ mywritefile2 True topetriFN    iso8601 "dot"  (commentIfError "//" asPetri) asPetriErr
     when (SFL4.tots      opts) $ mywritefile  True totsFN       iso8601 "ts"   asTSstr
     when (SFL4.tonl      opts) $ mywritefile  True toNL_FN      iso8601 "txt"  asNatLang
@@ -336,6 +338,7 @@ main = do
       pPrint $ groundrules rc rules
 
     when (SFL4.toProlog rc) $ pPrint asProlog
+    when (SFL4.toSCasp  rc) $ pPrint asSCasp
 
     when (SFL4.toTS rc) $ print $ asTypescript rules
 

lib/haskell/natural4/src/LS/Lib.hs

@@ -87,6 +87,7 @@ data Opts w = Opts { demo :: w ::: Bool <!> "False"
                    , workdir   :: w ::: String <!> ""  <?> "workdir to save all the output files to"
                    , uuiddir   :: w ::: String <!> "no-uuid"  <?> "uuid prefix to follow the workdir"
                    , toprolog  :: w ::: Bool   <!> "True"  <?> "prolog-like syntax representing the predicate logic"
+                   , toscasp   :: w ::: Bool   <!> "True"  <?> "sCasp-like syntax representing the predicate logic"
                    , tonative  :: w ::: Bool   <!> "True"  <?> "native Haskell data structure of the AST"
                    , topetri   :: w ::: Bool   <!> "True"  <?> "a petri-net Dot file of the state graph"
                    , toaasvg   :: w ::: Bool   <!> "True"  <?> "an anyall SVG of the decision trees"
@@ -157,6 +158,7 @@ getConfig o = do
         , toBabyL4  = only o == "babyl4" || only o == "corel4"
         , toASP     = only o == "asp"
         , toProlog  = only o == "prolog"
+        , toSCasp   = only o == "scasp"
         , toUppaal  = only o == "uppaal"
         , toGrounds = only o == "grounds"
         , toChecklist = only o == "checklist"

lib/haskell/natural4/src/LS/Types.hs

@@ -571,6 +571,7 @@ data RunConfig = RC { debug     :: Bool
                     , toBabyL4  :: Bool
                     , toASP     :: Bool
                     , toProlog  :: Bool
+                    , toSCasp   :: Bool
                     , toUppaal  :: Bool
                     , toHTML    :: Bool
                     , saveAKA   :: Bool
@@ -596,6 +597,7 @@ defaultRC = RC
         , toBabyL4 = False
         , toASP    = False
         , toProlog = False
+        , toSCasp  = False
         , toUppaal = False
         , saveAKA = False
         , wantNotRules = False

lib/haskell/natural4/src/LS/XPile/Prolog.hs

@@ -8,12 +8,35 @@ to Prolog.
 For more information see also `RelationalPredicates`.
 -}
 
+{-|
+TODO: Move the following into a README once the transpiler toolchain
+is operational.
+
+The transpiler comes in two versions: for Prolog and for sCasp.
+For a generation of valid sCasp to work, some very strong assumptions
+about Spreadsheet / csv files have been made, and if these 
+are not respected, the compiler produces garbage without mercy and warnings:
+* Each argument of a predicate has to be written in a separate CSV cell, 
+  and so has the predicate itself
+* However, arguments can be composite, e.g. function and arguments.
+* Also comparison operators have to be written in a separate cell. 
+For available comparison operators, see function showLPspecialSCasp
+* Assignment of a numerical value to a variable has to be written with IS:
+  var IS val   which is rendered as var #= val in sCasp
+* Equating two terms (triggerin unification in sCasp / Prolog) has to be written = .
+  Attention, in a spreadsheet, the symbol = has to be preceeded by a simple quote to be accepted.
+  term1 = term2 is rendered as term1 = term2 in sCasp
+  The tokens == and === are synonymes of = and are also rendered as term1 = term2 in sCasp
+-}
+
 module LS.XPile.Prolog where
 
-import AnyAll (BoolStruct (All, Any, Leaf, Not))
+import AnyAll (BoolStruct (All, Any, Leaf, Not), Dot (xPos))
 import Data.List.NonEmpty as NE (NonEmpty (..), toList)
 import Data.Map qualified as Map
 import Data.Text qualified as Text
+import Prettyprinter
+import Prettyprinter.Render.Text (putDoc)
 import LS.Rule as SFL4
   ( Rule (Hornlike, TypeDecl, clauses, enums, has, name, super),
   )
@@ -26,7 +49,7 @@ import LS.Types as SFL4
     MTExpr (..),
     ParamText,
     ParamType (TList0, TList1, TOne, TOptional),
-    RPRel,
+    RPRel (RPeq),
     RelationalPredicate (..),
     TypeSig (..),
     mt2text,
@@ -35,7 +58,63 @@ import LS.Types as SFL4
     rel2txt,
     untypePT,
   )
-import Language.Prolog (Clause (Clause), Term (Struct), var)
+import Language.Prolog (Clause (Clause), Term (Struct, Var, Wildcard, Cut), Atom, var)
+import Data.Functor.Classes (showsBinary1)
+
+
+-- Document generation for Logic Programs 
+-- Currently supported: Prolog and SCasp
+
+data TranslationMode = Prolog | SCasp
+class ShowLP x where
+    showLP :: TranslationMode -> x -> Doc ann
+
+instance ShowLP Clause where
+  -- showLP t c = pretty (show c)
+  showLP t (Clause lhs []) =
+    showLP t lhs <> pretty ("." :: Text.Text)
+  showLP t (Clause lhs rhs) =
+    showLP t lhs <>
+    pretty (":-" :: Text.Text) <>
+    nest 4
+      (vsep (punctuate comma (map (showLP t) rhs)) <>
+      pretty ("." :: Text.Text))
+  showLP t c = pretty (show c)
+
+instance ShowLP Term where
+  showLP SCasp trm@(Struct atom terms) =
+    if showLPIsSpecial atom
+    then showLPspecialSCasp atom terms
+    else pretty (show trm)
+  showLP t trm = pretty (show trm)
+
+showLPIsSpecial :: Atom -> Bool
+showLPIsSpecial "IS" = True
+showLPIsSpecial "<" = True
+showLPIsSpecial "=<" = True
+showLPIsSpecial "<=" = True
+showLPIsSpecial ">" = True
+showLPIsSpecial ">=" = True
+showLPIsSpecial "=" = True
+showLPIsSpecial "==" = True
+showLPIsSpecial _ = False
+
+
+showLPspecialSCasp :: Atom -> [Term] -> Doc ann
+showLPspecialSCasp "IS" = showBinaryInfixSCasp "#="
+showLPspecialSCasp "<"  = showBinaryInfixSCasp "#<"
+showLPspecialSCasp "=<" = showBinaryInfixSCasp "#=<"
+showLPspecialSCasp "<=" = showBinaryInfixSCasp "#=<"
+showLPspecialSCasp ">"  = showBinaryInfixSCasp "#>"
+showLPspecialSCasp ">=" = showBinaryInfixSCasp "#>="
+showLPspecialSCasp "="  = showBinaryInfixSCasp "=" -- non arithmetic equality
+showLPspecialSCasp "==" = showBinaryInfixSCasp "#="
+
+showBinaryInfixSCasp :: Text.Text -> [Term] -> Doc ann
+showBinaryInfixSCasp sym (trm1:trm2:trms) =
+  pretty (show trm1) <>
+  pretty (sym :: Text.Text) <>
+  pretty (show trm2)
 
 prologExamples :: [Clause]
 prologExamples =
@@ -44,13 +123,23 @@ prologExamples =
 
 type Analysis = Map.Map Text.Text Text.Text
 
-sfl4ToProlog :: [SFL4.Rule] -> [Clause]
-sfl4ToProlog rs =
+rulesToProlog :: [SFL4.Rule] -> String
+rulesToProlog rs = show (vsep (map (showLP Prolog) (sfl4ToLogProg rs)))
+
+rulesToSCasp :: [SFL4.Rule] -> String
+rulesToSCasp rs = show (vsep (map (showLP SCasp) (sfl4ToLogProg rs)))
+
+-- Translation of rules to generic logic programming clauses
+sfl4ToLogProg :: [SFL4.Rule] -> [Clause]
+sfl4ToLogProg rs =
   let
     analysis = analyze rs :: Analysis
   in
     concatMap (rule2clause analysis) rs
 
+-- TODO: not clear what the "Analysis" is good for. 
+-- The corresponding parameter seems to be ignored in all called functions.
+-- Also see the comment in the "analyze" function further below.
 rule2clause :: Analysis -> SFL4.Rule -> [Clause]
 rule2clause st cr@Hornlike {} = hornlike2clauses st (mt2text $ name cr) (clauses cr)
 rule2clause st td@TypeDecl { enums = Just ens }    = clpEnums st (mt2text $ name td) ens
@@ -99,7 +188,7 @@ showtype (SimpleType TList1    tt) = "nonEmptyList(" <> tt <> ")"
 showtype (InlineEnum pt        tt) = showtype (SimpleType pt (inEnums (fmap mtexpr2text <$> untypePT tt)))
 
 inEnums :: NonEmpty (NonEmpty Text.Text) -> Text.Text
-inEnums pt = "enums(" <> Text.unwords [ h | (h :| _) <- NE.toList pt ] <> ")"          
+inEnums pt = "enums(" <> Text.unwords [ h | (h :| _) <- NE.toList pt ] <> ")"
              -- we gonna need the same writer magic to append top-level output.
              -- in future, run clpEnums
              -- for now, just blurt it out
@@ -167,8 +256,13 @@ rp2goal (RPBoolStructR lhs_ _rel bsr) = Struct (Text.unpack $ mt2text lhs_) <$>
 rp2goal (RPConstraint mt1 rel mt2) = pure $ Struct (rel2f rel) $ (varmt <$> mt1) ++ (varmt <$> mt2)
 rp2goal (RPnary      rprel rps) = pure $ Struct (rel2f rprel) (concatMap rp2goal rps)
 
+-- The equality token RPeq has three external appearances: =, ==, ===
+-- whose difference is not clear.
+-- Here, they are mapped to =, so that the symbol can be used as 
+-- Prolog's "unifiable". TODO: a bad hack.
 rel2f :: RPRel -> String
-rel2f = Text.unpack . rel2txt
+rel2f RPeq = "="
+rel2f r = Text.unpack (rel2txt r)
 
 analyze :: [SFL4.Rule] -> Analysis
 analyze _rs = Map.fromList [("enumPrimaryKey", "1")] -- sorry, gonna have to read and show this all the time, slightly lame