Support printing rules in LaTeX

eo-phi-normalizer/app/Main.hs

@@ -53,6 +53,7 @@ import Language.EO.Phi.Report.Data (makeProgramReport, makeReport)
 import Language.EO.Phi.Report.Html (reportCSS, reportJS, toStringReport)
 import Language.EO.Phi.Rules.Common
 import Language.EO.Phi.Rules.Fast (fastYegorInsideOut, fastYegorInsideOutAsRule)
+import Language.EO.Phi.Rules.RunYegor (yegorRuleSet)
 import Language.EO.Phi.Rules.Yaml (RuleSet (rules, title), convertRuleNamed, parseRuleSetFromFile)
 import Language.EO.Phi.ToLaTeX
 import Main.Utf8
@@ -100,6 +101,13 @@ data CLI'MetricsPhi = CLI'MetricsPhi
   }
   deriving stock (Show)
 
+data CLI'PrintRules = CLI'PrintRules
+  { rulesPath :: Maybe String
+  , latex :: Bool
+  , compact :: Bool
+  }
+  deriving stock (Show)
+
 newtype CLI'Pipeline'Report = CLI'Pipeline'Report
   { configFile :: FilePath
   }
@@ -127,6 +135,7 @@ data CLI
   = CLI'TransformPhi' CLI'TransformPhi
   | CLI'DataizePhi' CLI'DataizePhi
   | CLI'MetricsPhi' CLI'MetricsPhi
+  | CLI'PrintRules' CLI'PrintRules
   | CLI'Pipeline' CLI'Pipeline
   deriving stock (Show)
 
@@ -189,6 +198,9 @@ jsonSwitch = switch (long "json" <> short 'j' <> help "Output JSON.")
 latexSwitch :: Parser Bool
 latexSwitch = switch (long "tex" <> help "Output LaTeX.")
 
+compactSwitch :: Parser Bool
+compactSwitch = switch (long "compact" <> short 'c' <> help "Print rules, either each on one line")
+
 asPackageSwitch :: Parser Bool
 asPackageSwitch = switch (long "as-package" <> help "Automatically inject (λ → Package) in the program if necessary, to dataize all fields.")
 
@@ -223,6 +235,7 @@ data CommandParser = CommandParser
   , dataize :: Parser CLI'DataizePhi
   , pipeline :: Parser CLI'Pipeline
   , pipeline' :: CommandParser'Pipeline
+  , printRules :: Parser CLI'PrintRules
   }
 
 commandParser :: CommandParser
@@ -234,7 +247,11 @@ commandParser =
     outputFile <- outputFileOption
     bindingsPath <- bindingsPathOption
     pure CLI'MetricsPhi{..}
-
+  printRules = do
+    rulesPath <- optional $ strOption (long "rules" <> short 'r' <> metavar.file <> help [fmt|{metavarName.file} with user-defined rules. If unspecified, yegor.yaml is rendered.|])
+    latex <- latexSwitch
+    compact <- compactSwitch
+    pure CLI'PrintRules{..}
   transform = do
     rulesPath <- optional $ strOption (long "rules" <> short 'r' <> metavar.file <> help [fmt|{metavarName.file} with user-defined rules. If unspecified, builtin set of rules is used.|])
     chain <- switch (long "chain" <> short 'c' <> help "Output transformation steps.")
@@ -296,6 +313,7 @@ data CommandParserInfo = CommandParserInfo
   { metrics :: ParserInfo CLI
   , transform :: ParserInfo CLI
   , dataize :: ParserInfo CLI
+  , printRules :: ParserInfo CLI
   , pipeline :: ParserInfo CLI
   , pipeline' :: CommandParserInfo'Pipeline
   }
@@ -306,6 +324,7 @@ commandParserInfo =
     { metrics = info (CLI'MetricsPhi' <$> commandParser.metrics) (progDesc "Collect metrics for a PHI program.")
     , transform = info (CLI'TransformPhi' <$> commandParser.transform) (progDesc "Transform a PHI program.")
     , dataize = info (CLI'DataizePhi' <$> commandParser.dataize) (progDesc "Dataize a PHI program.")
+    , printRules = info (CLI'PrintRules' <$> commandParser.printRules) (progDesc "Print rules in LaTeX format.")
     , pipeline = info (CLI'Pipeline' <$> commandParser.pipeline) (progDesc "Run pipeline-related commands.")
     , pipeline' =
         CommandParserInfo'Pipeline
@@ -325,6 +344,7 @@ data CommandNames = CommandNames
   { transform :: String
   , metrics :: String
   , dataize :: String
+  , printRules :: String
   , pipeline :: String
   , pipeline' :: CommandNames'Pipeline
   }
@@ -335,6 +355,7 @@ commandNames =
     { transform = "transform"
     , metrics = "metrics"
     , dataize = "dataize"
+    , printRules = "print-rules"
     , pipeline = "pipeline"
     , pipeline' =
         CommandNames'Pipeline
@@ -351,6 +372,7 @@ cli =
         <> command commandNames.metrics commandParserInfo.metrics
         <> command commandNames.dataize commandParserInfo.dataize
         <> command commandNames.pipeline commandParserInfo.pipeline
+        <> command commandNames.printRules commandParserInfo.printRules
     )
 
 cliOpts :: ParserInfo CLI
@@ -508,6 +530,11 @@ main = withUtf8 do
       -- logStrLn "Computing metrics"
       metrics <- getMetrics bindingsPath inputFile
       logStrLn $ encodeToJSONString metrics
+    CLI'PrintRules' CLI'PrintRules{..} -> do
+      (logStrLn, _) <- getLoggers Nothing
+      rules <- rules <$> maybe (return yegorRuleSet) parseRuleSetFromFile rulesPath
+      let toLatex' = if compact then rulesToLatexCompact else toLatex
+      logStrLn $ show $ toLatex' rules
     CLI'TransformPhi' CLI'TransformPhi{..} -> do
       program' <- getProgram inputFile
       deps <- mapM (getProgram . Just) dependencies

eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs

@@ -1,6 +1,8 @@
 {-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
 
 module Language.EO.Phi.ToLaTeX where
 
@@ -9,6 +11,7 @@ import Data.List (intersperse)
 import Data.String (IsString)
 import Data.Text qualified as T
 import Language.EO.Phi
+import Language.EO.Phi.Rules.Yaml
 import Text.Regex (mkRegex, subRegex)
 
 newtype LaTeX = LaTeX {unLaTeX :: String}
@@ -31,16 +34,16 @@ instance ToLatex Attribute where
   toLatex Rho = "^"
   toLatex (Alpha (AlphaIndex a)) = LaTeX ("\\alpha_" ++ tail a)
   toLatex (Label (LabelId l)) = LaTeX l
-  toLatex (MetaAttr _) = error "rendering MetaBindings in LaTex format"
+  toLatex (MetaAttr (LabelMetaId l)) = LaTeX l
 
 instance ToLatex Binding where
   toLatex (AlphaBinding attr obj) = toLatex attr <> " -> " <> toLatex obj
   toLatex (EmptyBinding attr) = toLatex attr <> " -> ?"
   toLatex (DeltaBinding (Bytes bytes)) = "D> " <> LaTeX bytes
   toLatex DeltaEmptyBinding = "D> ?"
   toLatex (LambdaBinding (Function fn)) = "L> " <> LaTeX fn
-  toLatex (MetaBindings _) = error "rendering MetaBindings in LaTex format"
-  toLatex (MetaDeltaBinding _) = error "rendering MetaDeltaBinding in LaTex format"
+  toLatex (MetaBindings (BindingsMetaId x)) = LaTeX x
+  toLatex (MetaDeltaBinding (BytesMetaId x)) = "D> " <> LaTeX x
 
 instance ToLatex Object where
   toLatex (Formation bindings) =
@@ -50,20 +53,99 @@ instance ToLatex Object where
   toLatex (ObjectDispatch obj attr) =
     toLatex obj <> "." <> toLatex attr
   toLatex GlobalObject = "Q"
-  toLatex ThisObject = "$"
+  toLatex ThisObject = "\\xi"
   toLatex Termination = "\\dead"
-  toLatex (MetaObject _) = error "rendering MetaObject in LaTex format"
+  toLatex (MetaObject (ObjectMetaId metaId)) = LaTeX metaId
   toLatex MetaTailContext{} = error "rendering MetaTailContext in LaTex format"
   toLatex (MetaFunction _ _) = error "rendering MetaFunction in LaTex format"
-  toLatex (MetaSubstThis _ _) = error "rendering MetaSubstThis in LaTex format"
+  toLatex (MetaSubstThis obj1 obj2) = LaTeX "\\mathbb{S}(" <> toLatex obj1 <> ", " <> toLatex obj2 <> ")"
 
 removeOrgEolang :: String -> String
 removeOrgEolang = T.unpack . T.replace "Q.org.eolang" "QQ" . T.pack
 
+substituteTau :: String -> String
+substituteTau = T.unpack . T.replace "τ" "\\tau" . T.pack
+
+removeExclamationsMarks :: String -> String
+removeExclamationsMarks = filter (/= '!')
+
 removeAlpha :: String -> String
 removeAlpha s = subRegex (mkRegex "\\\\alpha_([0-9]+) ->") s "\\1->"
 
 -- >>> toLatex ("{ ⟦ α0 ↦ ξ, α1 ↦ Φ.org.eolang.bytes( Δ ⤍ 00- ) ⟧ }" :: Program)
 -- \Big\{ [[ 0-> $, 1-> QQ.bytes( D> 00- ) ]] \Big\}
 latexToString :: LaTeX -> String
-latexToString = removeAlpha . removeOrgEolang . unLaTeX
+latexToString = removeExclamationsMarks . substituteTau . removeAlpha . removeOrgEolang . unLaTeX
+
+inMathMode :: LaTeX -> LaTeX
+inMathMode = (" $ " <>) . (<> " $ ")
+
+-- it's ok without separators here because rules have zero or one constraint from the context
+instance ToLatex RuleContext where
+  toLatex RuleContext{..} =
+    maybe mempty (\x -> inMathMode $ toLatex GlobalObject <> " -> " <> toLatex x) global_object
+      <> maybe mempty (\x -> (inMathMode $ toLatex x) <> " is the scope of the redex") current_object
+      <> maybe mempty (\x -> toLatex x <> " is the current attribute") current_attribute
+
+instance ToLatex RuleAttribute where
+  toLatex (ObjectAttr a) = toLatex a
+  toLatex DeltaAttr = "\\Delta"
+  toLatex LambdaAttr = "\\lambda"
+
+instance ToLatex Condition where
+  toLatex (IsNF nf) = inMathMode $ toLatex nf <> "\\in\\mathcal{N}"
+  toLatex (IsNFInsideFormation nf_inside_formation) =
+    (inMathMode $ toLatex nf_inside_formation) <> " is nf inside formation"
+  toLatex (PresentAttrs (AttrsInBindings attrs bindings)) =
+    inMathMode $ fold (intersperse ", " (map toLatex attrs)) <> " \\in " <> foldMap toLatex bindings
+  toLatex (AbsentAttrs (AttrsInBindings attrs bindings)) =
+    inMathMode $ fold (intersperse ", " (map toLatex attrs)) <> " \\notin " <> foldMap toLatex bindings
+  toLatex (AttrNotEqual (attr1, attr2)) =
+    inMathMode $ toLatex attr1 <> " \\neq " <> toLatex attr2
+  toLatex (ApplyInSubformations apply_in_subformations) =
+    if not apply_in_subformations then LaTeX "not in subformations" else mempty
+  toLatex (ApplyInAbstractSubformations apply_in_abstract_subformations) =
+    if not apply_in_abstract_subformations then LaTeX "not in subformations" else mempty
+
+isNonEmptyContext :: Maybe RuleContext -> Bool
+isNonEmptyContext Nothing = False
+isNonEmptyContext (Just (RuleContext Nothing Nothing Nothing)) = False
+isNonEmptyContext _ = True
+
+-- Renders all conditions on separate lines
+instance ToLatex Rule where
+  toLatex (Rule name _ context _ pattern result _ when _) =
+    "\\rrule{"
+      <> LaTeX name
+      <> "}: &"
+      <> inMathMode (toLatex pattern)
+      <> "\\(\\trans\\)"
+      <> inMathMode (toLatex result)
+      <> (if not (null when) || isNonEmptyContext context then "\\\\\\text {if }" else mempty)
+      <> maybe mempty (\c -> "&" <> toLatex c <> "\\\\") context
+      <> fold (intersperse ",\\\\" (map (("&" <>) . toLatex) when))
+
+instance ToLatex [Rule] where
+  toLatex rules =
+    "\\begin{figure*}\n\\begin{tabular}{rl}\n  "
+      <> fold (intersperse "\\\\\\\\\n  " (map toLatex rules))
+      <> "\n\\end{tabular}\n\\end{figure*}"
+
+-- Renders all conditions in one line
+ruleToLatexCompact :: Rule -> LaTeX
+ruleToLatexCompact (Rule name _ context _ pattern result _ when _) =
+  "\\rrule{"
+    <> LaTeX name
+    <> "}: "
+    <> inMathMode (toLatex pattern)
+    <> "\\(\\trans\\)"
+    <> inMathMode (toLatex result)
+    <> (if not (null when) || isNonEmptyContext context then "\\quad\\text {if }" else "")
+    <> maybe mempty (\c -> toLatex c <> ", ") context
+    <> fold (intersperse ", " (map toLatex when))
+
+rulesToLatexCompact :: [Rule] -> LaTeX
+rulesToLatexCompact rules =
+  "\\begin{figure*}\n  "
+    <> fold (intersperse "\\\\\\vspace*{0.5em}\n  " (map ruleToLatexCompact rules))
+    <> "\n\\end{figure*}"