diff --git a/lib/haskell/natural4/app/Main.hs b/lib/haskell/natural4/app/Main.hs index 736b6e49f..451495293 100644 --- a/lib/haskell/natural4/app/Main.hs +++ b/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 diff --git a/lib/haskell/natural4/src/LS/Lib.hs b/lib/haskell/natural4/src/LS/Lib.hs index e29fc5de0..e8a7599e5 100644 --- a/lib/haskell/natural4/src/LS/Lib.hs +++ b/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" diff --git a/lib/haskell/natural4/src/LS/Types.hs b/lib/haskell/natural4/src/LS/Types.hs index 0be3833fa..e5036344e 100644 --- a/lib/haskell/natural4/src/LS/Types.hs +++ b/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 diff --git a/lib/haskell/natural4/src/LS/XPile/Prolog.hs b/lib/haskell/natural4/src/LS/XPile/Prolog.hs index 958b46da9..7e89d7b0d 100644 --- a/lib/haskell/natural4/src/LS/XPile/Prolog.hs +++ b/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