{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}

-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
-- SPDX-License-Identifier: MIT

module LaTeX
  ( explainRules
  , explainMorphRules
  , explainDataizeRules
  , explainContextualizeRules
  , rewrittensToLatex
  , expressionToLaTeX
  , defaultLatexContext
  , defaultMeetLength
  , defaultMeetPopularity
  , LatexContext (..)
  , meetInExpressions
  , meetInExpression
  , conditionToLatex
  ) where

import AST
import Bytes (nonFiniteName)
import CST
import Canonizer (canonize, canonizeExpr)
import Data.Char (isAscii, ord)
import Data.List (intercalate, nub, zipWith4)
import Data.Maybe (isJust)
import qualified Data.Text as T
import Deps (Judgment (..))
import Encoding
import Lining
import Locator (locatedExpression)
import Margin (WithMargin, defaultMargin, withLines)
import Matcher
import Metas (lonely)
import Misc
import Render (Render (render))
import Replacer (replaceExpression)
import Rewriter (Rewritten, Rewrittens', stepHeaders)
import Sugar (SugarType (SWEET), ToSalty, withSugarType, withoutRho)
import Text.Printf (printf)
import Text.Read (readMaybe)
import qualified Yaml as Y

data LatexContext = LatexContext
  { LatexContext -> SugarType
_sugar :: SugarType
  , LatexContext -> LineFormat
_line :: LineFormat
  , LatexContext -> Int
_margin :: Int
  , LatexContext -> Bool
_nonumber :: Bool
  , LatexContext -> Bool
_compress :: Bool
  , LatexContext -> Bool
_canonize :: Bool
  , LatexContext -> Int
_meetPopularity :: Int
  , LatexContext -> Int
_meetLength :: Int
  , LatexContext -> Expression
_focus :: Expression
  , LatexContext -> Maybe String
_expression :: Maybe String
  , LatexContext -> Maybe String
_label :: Maybe String
  , LatexContext -> Maybe String
_meetPrefix :: Maybe String
  , LatexContext -> Bool
_headers :: Bool
  , LatexContext -> Bool
_hideRho :: Bool
  }

defaultLatexContext :: LatexContext
defaultLatexContext :: LatexContext
defaultLatexContext = SugarType
-> LineFormat
-> Int
-> Bool
-> Bool
-> Bool
-> Int
-> Int
-> Expression
-> Maybe String
-> Maybe String
-> Maybe String
-> Bool
-> Bool
-> LatexContext
LatexContext SugarType
SWEET LineFormat
SINGLELINE Int
defaultMargin Bool
False Bool
False Bool
False Int
defaultMeetPopularity Int
defaultMeetLength Expression
ExRoot Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Bool
False Bool
False

defaultMeetPopularity :: Int
defaultMeetPopularity :: Int
defaultMeetPopularity = Int
50

defaultMeetLength :: Int
defaultMeetLength :: Int
defaultMeetLength = Int
8

meetInExpression :: Expression -> Int -> Expression -> [Expression]
meetInExpression :: Expression -> Int -> Expression -> [Expression]
meetInExpression Expression
expr Int
len = Expression -> Expression -> [Expression]
meetIn Expression
expr
  where
    meetIn :: Expression -> Expression -> [Expression]
    meetIn :: Expression -> Expression -> [Expression]
meetIn (DataString Bytes
_) Expression
_ = []
    meetIn (DataNumber Bytes
_) Expression
_ = []
    meetIn (ExPhiMeet{}) Expression
_ = []
    meetIn (ExPhiAgain{}) Expression
_ = []
    meetIn Expression
ex Expression
target =
      let matched :: [Expression]
matched = if Expression -> Int
countNodes Expression
ex Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
len then (Subst -> Expression) -> [Subst] -> [Expression]
forall a b. (a -> b) -> [a] -> [b]
map (Expression -> Subst -> Expression
forall a b. a -> b -> a
const Expression
ex) (MatchExpressionFunc
matchExpression Expression
ex Expression
target) else []
       in [Expression]
matched [Expression] -> [Expression] -> [Expression]
forall a. [a] -> [a] -> [a]
++ case Expression
ex of
            ExDispatch Expression
ex' Attribute
_ -> Expression -> Expression -> [Expression]
meetIn Expression
ex' Expression
target
            ExApplication Expression
ex' Argument
arg -> Expression -> Expression -> [Expression]
meetIn Expression
ex' Expression
target [Expression] -> [Expression] -> [Expression]
forall a. [a] -> [a] -> [a]
++ Expression -> Expression -> [Expression]
meetIn (Argument -> Expression
argExpr Argument
arg) Expression
target
            ExFormation [Binding]
bds -> [Binding] -> Expression -> [Expression]
meetInBindings [Binding]
bds Expression
target
            Expression
_ -> []
    meetInBindings :: [Binding] -> Expression -> [Expression]
    meetInBindings :: [Binding] -> Expression -> [Expression]
meetInBindings [] Expression
_ = []
    meetInBindings (BiTau Attribute
_ Expression
ex : [Binding]
bds) Expression
target = Expression -> Expression -> [Expression]
meetIn Expression
ex Expression
target [Expression] -> [Expression] -> [Expression]
forall a. [a] -> [a] -> [a]
++ [Binding] -> Expression -> [Expression]
meetInBindings [Binding]
bds Expression
target
    meetInBindings (Binding
_ : [Binding]
bds) Expression
target = [Binding] -> Expression -> [Expression]
meetInBindings [Binding]
bds Expression
target
    argExpr :: Argument -> Expression
    argExpr :: Argument -> Expression
argExpr (ArTau Attribute
_ Expression
ex) = Expression
ex
    argExpr (ArAlpha Alpha
_ Expression
ex) = Expression
ex

meetInExpressions :: [Expression] -> LatexContext -> [Expression]
meetInExpressions :: [Expression] -> LatexContext -> [Expression]
meetInExpressions [Expression]
exprs LatexContext{Bool
Int
Maybe String
Expression
SugarType
LineFormat
_sugar :: LatexContext -> SugarType
_line :: LatexContext -> LineFormat
_margin :: LatexContext -> Int
_nonumber :: LatexContext -> Bool
_compress :: LatexContext -> Bool
_canonize :: LatexContext -> Bool
_meetPopularity :: LatexContext -> Int
_meetLength :: LatexContext -> Int
_focus :: LatexContext -> Expression
_expression :: LatexContext -> Maybe String
_label :: LatexContext -> Maybe String
_meetPrefix :: LatexContext -> Maybe String
_headers :: LatexContext -> Bool
_hideRho :: LatexContext -> Bool
_sugar :: SugarType
_line :: LineFormat
_margin :: Int
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe String
_label :: Maybe String
_meetPrefix :: Maybe String
_headers :: Bool
_hideRho :: Bool
..} = [Expression] -> Int -> [Expression]
go [Expression]
exprs Int
1
  where
    go :: [Expression] -> Int -> [Expression]
    go :: [Expression] -> Int -> [Expression]
go [] Int
_ = []
    go [Expression
single] Int
_ = [Expression
single]
    go (Expression
first : [Expression]
rest) Int
idx =
      let met :: [[Expression]]
met = (Expression -> [Expression]) -> [Expression] -> [[Expression]]
forall a b. (a -> b) -> [a] -> [b]
map (Expression -> Int -> Expression -> [Expression]
meetInExpression Expression
first Int
_meetLength) [Expression]
rest
          unique :: [Expression]
unique = [Expression] -> [Expression]
forall a. Eq a => [a] -> [a]
nub ([[Expression]] -> [Expression]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Expression]]
met)
          (Maybe Expression
frequent, Int
_) =
            ((Maybe Expression, Int) -> Expression -> (Maybe Expression, Int))
-> (Maybe Expression, Int)
-> [Expression]
-> (Maybe Expression, Int)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
              ( \(Maybe Expression
best, Int
count) Expression
cur ->
                  let len :: Int
len = [[Expression]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (([Expression] -> Bool) -> [[Expression]] -> [[Expression]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expression -> [Expression] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Expression
cur) [[Expression]]
met)
                   in if Int
len Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
count
                        then (Expression -> Maybe Expression
forall a. a -> Maybe a
Just Expression
cur, Int
len)
                        else (Maybe Expression
best, Int
count)
              )
              (Maybe Expression
forall a. Maybe a
Nothing, Int
0)
              [Expression]
unique
          next :: [Expression]
next = Expression
first Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: [Expression] -> Int -> [Expression]
go [Expression]
rest Int
idx
       in case Maybe Expression
frequent of
            Just Expression
expr ->
              case MatchExpressionFunc
matchExpression Expression
expr Expression
first of
                (Subst
_ : [Subst]
substs) ->
                  let met' :: [[Expression]]
met' = ([Expression] -> [Expression]) -> [[Expression]] -> [[Expression]]
forall a b. (a -> b) -> [a] -> [b]
map ((Expression -> Bool) -> [Expression] -> [Expression]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
expr)) [[Expression]]
met
                      withMeet :: Expression
withMeet = ReplaceExpressionFunc
replaceExpression (Expression
first, [Expression
expr], [Maybe String -> Int -> Expression -> Expression
ExPhiMeet Maybe String
_meetPrefix Int
idx])
                      withAgain :: Expression
withAgain = ReplaceExpressionFunc
replaceExpression (Expression
withMeet, (Subst -> Expression) -> [Subst] -> [Expression]
forall a b. (a -> b) -> [a] -> [b]
map (Expression -> Subst -> Expression
forall a b. a -> b -> a
const Expression
expr) [Subst]
substs, (Subst -> Expression -> Expression)
-> [Subst] -> [Expression -> Expression]
forall a b. (a -> b) -> [a] -> [b]
map ((Expression -> Expression) -> Subst -> Expression -> Expression
forall a b. a -> b -> a
const (Maybe String -> Int -> Expression -> Expression
ExPhiAgain Maybe String
_meetPrefix Int
idx)) [Subst]
substs)
                      rest' :: [Expression]
rest' = (Expression -> [Expression] -> Expression)
-> [Expression] -> [[Expression]] -> [Expression]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Expression
other [Expression]
exprs' -> ReplaceExpressionFunc
replaceExpression (Expression
other, [Expression]
exprs', (Expression -> Expression -> Expression)
-> [Expression] -> [Expression -> Expression]
forall a b. (a -> b) -> [a] -> [b]
map ((Expression -> Expression)
-> Expression -> Expression -> Expression
forall a b. a -> b -> a
const (Maybe String -> Int -> Expression -> Expression
ExPhiAgain Maybe String
_meetPrefix Int
idx)) [Expression]
exprs')) [Expression]
rest [[Expression]]
met'
                      found :: [[Expression]]
found = ([Expression] -> Bool) -> [[Expression]] -> [[Expression]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ([Expression] -> Bool) -> [Expression] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expression] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [[Expression]]
met'
                   in if [[Expression]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Expression]]
met' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 Bool -> Bool -> Bool
&& Int -> Double
toDouble ([[Expression]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Expression]]
found) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Int -> Double
toDouble ([[Expression]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Expression]]
met') Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
>= Double
popularity
                        then [Expression] -> Int -> [Expression]
go (Expression
withAgain Expression -> [Expression] -> [Expression]
forall a. a -> [a] -> [a]
: [Expression]
rest') (Int
idx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                        else [Expression]
next
                [] -> [Expression]
next
            Maybe Expression
_ -> [Expression]
next
    popularity :: Double
    popularity :: Double
popularity = Int -> Double
toDouble Int
_meetPopularity Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
100.0

renderToLatex :: (ToSalty a, ToASCII a, ToSingleLine a, ToLaTeX a, WithMargin a, Render a) => a -> LatexContext -> String
renderToLatex :: forall a.
(ToSalty a, ToASCII a, ToSingleLine a, ToLaTeX a, WithMargin a,
 Render a) =>
a -> LatexContext -> String
renderToLatex a
renderable LatexContext{Bool
Int
Maybe String
Expression
SugarType
LineFormat
_sugar :: LatexContext -> SugarType
_line :: LatexContext -> LineFormat
_margin :: LatexContext -> Int
_nonumber :: LatexContext -> Bool
_compress :: LatexContext -> Bool
_canonize :: LatexContext -> Bool
_meetPopularity :: LatexContext -> Int
_meetLength :: LatexContext -> Int
_focus :: LatexContext -> Expression
_expression :: LatexContext -> Maybe String
_label :: LatexContext -> Maybe String
_meetPrefix :: LatexContext -> Maybe String
_headers :: LatexContext -> Bool
_hideRho :: LatexContext -> Bool
_sugar :: SugarType
_line :: LineFormat
_margin :: Int
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe String
_label :: Maybe String
_meetPrefix :: Maybe String
_headers :: Bool
_hideRho :: Bool
..} = Text -> String
T.unpack (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ a -> Text
forall a. Render a => a -> Text
render (a -> a
forall a. ToLaTeX a => a -> a
toLaTeX (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ LineFormat -> Int -> a -> a
forall a.
(WithMargin a, ToSingleLine a) =>
LineFormat -> Int -> a -> a
withLines LineFormat
_line Int
_margin (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ Encoding -> a -> a
forall a. ToASCII a => Encoding -> a -> a
withEncoding Encoding
ASCII (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ SugarType -> a -> a
forall a. ToSalty a => SugarType -> a -> a
withSugarType SugarType
_sugar a
renderable)

phiquation :: LatexContext -> String
phiquation :: LatexContext -> String
phiquation LatexContext{_nonumber :: LatexContext -> Bool
_nonumber = Bool
True} = String
"phiquation*"
phiquation LatexContext{_nonumber :: LatexContext -> Bool
_nonumber = Bool
False} = String
"phiquation"

preamble :: LatexContext -> String
preamble :: LatexContext -> String
preamble ctx :: LatexContext
ctx@LatexContext{Bool
Int
Maybe String
Expression
SugarType
LineFormat
_sugar :: LatexContext -> SugarType
_line :: LatexContext -> LineFormat
_margin :: LatexContext -> Int
_nonumber :: LatexContext -> Bool
_compress :: LatexContext -> Bool
_canonize :: LatexContext -> Bool
_meetPopularity :: LatexContext -> Int
_meetLength :: LatexContext -> Int
_focus :: LatexContext -> Expression
_expression :: LatexContext -> Maybe String
_label :: LatexContext -> Maybe String
_meetPrefix :: LatexContext -> Maybe String
_headers :: LatexContext -> Bool
_hideRho :: LatexContext -> Bool
_sugar :: SugarType
_line :: LineFormat
_margin :: Int
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe String
_label :: Maybe String
_meetPrefix :: Maybe String
_headers :: Bool
_hideRho :: Bool
..} =
  [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ String -> String -> String
forall r. PrintfType r => String -> r
printf String
"\\begin{%s}\n" (LatexContext -> String
phiquation LatexContext
ctx)
    , String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"\\label{%s}\n") Maybe String
_label
    , String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"\\phiExpression{%s} " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
escaped) Maybe String
_expression
    ]

body :: [String] -> [(a, Maybe (Judgment, String))] -> (Int -> a -> String) -> String
body :: forall a.
[String]
-> [(a, Maybe (Judgment, String))]
-> (Int -> a -> String)
-> String
body [String]
comments [(a, Maybe (Judgment, String))]
printed Int -> a -> String
toLatex =
  String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate
    String
"\n"
    ( (Int
 -> String -> (a, Maybe (Judgment, String)) -> Judgment -> String)
-> [Int]
-> [String]
-> [(a, Maybe (Judgment, String))]
-> [Judgment]
-> [String]
forall a b c d e.
(a -> b -> c -> d -> e) -> [a] -> [b] -> [c] -> [d] -> [e]
zipWith4
        ( \Int
idx String
comment (a
item, Maybe (Judgment, String)
rule) Judgment
reached ->
            let item' :: String
item' = Int -> a -> String
toLatex (Int -> Int
baseTab Int
idx) a
item
                opening :: String
opening = if Int
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then String
item' else String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"  %s %s" (Judgment -> String
relation Judgment
reached) String
item'
             in String
comment
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
-> ((Judgment, String) -> String)
-> Maybe (Judgment, String)
-> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
                    String
opening
                    ( \(Judgment
judgment, String
name) ->
                        if Judgment
judgment Judgment -> [Judgment] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Judgment
Contextualization, Judgment
Evaluation]
                          then String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s %s" String
opening (Judgment -> String
relation Judgment
judgment)
                          else String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s %s[\\nameref{r:%s}]" String
opening (Judgment -> String
relation Judgment
judgment) (String -> String
escaped String
name)
                    )
                    Maybe (Judgment, String)
rule
        )
        [Int
0 ..]
        [String]
comments
        [(a, Maybe (Judgment, String))]
printed
        ([Maybe (Judgment, String)] -> [Judgment]
arrows (((a, Maybe (Judgment, String)) -> Maybe (Judgment, String))
-> [(a, Maybe (Judgment, String))] -> [Maybe (Judgment, String)]
forall a b. (a -> b) -> [a] -> [b]
map (a, Maybe (Judgment, String)) -> Maybe (Judgment, String)
forall a b. (a, b) -> b
snd [(a, Maybe (Judgment, String))]
printed))
    )
  where
    baseTab :: Int -> Int
    baseTab :: Int -> Int
baseTab Int
0 = Int
0
    baseTab Int
_ = Int
1

arrows :: [Maybe (Judgment, String)] -> [Judgment]
arrows :: [Maybe (Judgment, String)] -> [Judgment]
arrows = (Judgment -> Maybe (Judgment, String) -> Judgment)
-> Judgment -> [Maybe (Judgment, String)] -> [Judgment]
forall b a. (b -> a -> b) -> b -> [a] -> [b]
scanl (\Judgment
current Maybe (Judgment, String)
rule -> Judgment
-> ((Judgment, String) -> Judgment)
-> Maybe (Judgment, String)
-> Judgment
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Judgment
current (Judgment, String) -> Judgment
forall a b. (a, b) -> a
fst Maybe (Judgment, String)
rule) Judgment
Normalization

relation :: Judgment -> String
relation :: Judgment -> String
relation Judgment
Normalization = String
"\\phiNormalize"
relation Judgment
Morphing = String
"\\phiMorph"
relation Judgment
Dataization = String
"\\phiDataize"
relation Judgment
Evaluation = String
"\\phiEvaluate"
relation Judgment
Contextualization = String
"\\phiContextualize"

stepComments :: [Rewritten] -> LatexContext -> [String]
stepComments :: [Rewritten] -> LatexContext -> [String]
stepComments [Rewritten]
rewrittens LatexContext{_headers :: LatexContext -> Bool
_headers = Bool
enabled} =
  if Bool
enabled
    then (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%% %s\n") ([Rewritten] -> [String]
stepHeaders [Rewritten]
rewrittens)
    else (Rewritten -> String) -> [Rewritten] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Rewritten -> String
forall a b. a -> b -> a
const String
"") [Rewritten]
rewrittens

ending :: Bool -> Judgment -> LatexContext -> String
ending :: Bool -> Judgment -> LatexContext -> String
ending Bool
True Judgment
judgment LatexContext
ctx = String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
" %s\n  %s \\dots\n\\end{%s}" (Judgment -> String
relation Judgment
judgment) (Judgment -> String
relation Judgment
judgment) (LatexContext -> String
phiquation LatexContext
ctx)
ending Bool
False Judgment
_ LatexContext
ctx = LatexContext -> String
period LatexContext
ctx

period :: LatexContext -> String
period :: LatexContext -> String
period LatexContext
ctx = String -> String -> String
forall r. PrintfType r => String -> r
printf String
"{.}\n\\end{%s}" (LatexContext -> String
phiquation LatexContext
ctx)

compressedRewrittens :: [Rewritten] -> LatexContext -> [Rewritten]
compressedRewrittens :: [Rewritten] -> LatexContext -> [Rewritten]
compressedRewrittens [Rewritten]
rewrittens ctx :: LatexContext
ctx@LatexContext{Bool
Int
Maybe String
Expression
SugarType
LineFormat
_sugar :: LatexContext -> SugarType
_line :: LatexContext -> LineFormat
_margin :: LatexContext -> Int
_nonumber :: LatexContext -> Bool
_compress :: LatexContext -> Bool
_canonize :: LatexContext -> Bool
_meetPopularity :: LatexContext -> Int
_meetLength :: LatexContext -> Int
_focus :: LatexContext -> Expression
_expression :: LatexContext -> Maybe String
_label :: LatexContext -> Maybe String
_meetPrefix :: LatexContext -> Maybe String
_headers :: LatexContext -> Bool
_hideRho :: LatexContext -> Bool
_sugar :: SugarType
_line :: LineFormat
_margin :: Int
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe String
_label :: Maybe String
_meetPrefix :: Maybe String
_headers :: Bool
_hideRho :: Bool
..} =
  let ([Expression]
exprs, [Maybe (Judgment, String)]
rules) = [Rewritten] -> ([Expression], [Maybe (Judgment, String)])
forall a b. [(a, b)] -> ([a], [b])
unzip [Rewritten]
rewrittens
   in if Bool
_compress then [Expression] -> [Maybe (Judgment, String)] -> [Rewritten]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Expression] -> LatexContext -> [Expression]
meetInExpressions [Expression]
exprs LatexContext
ctx) [Maybe (Judgment, String)]
rules else [Rewritten]
rewrittens

canonizedRewrittens :: [Rewritten] -> LatexContext -> [Rewritten]
canonizedRewrittens :: [Rewritten] -> LatexContext -> [Rewritten]
canonizedRewrittens [Rewritten]
rewrittens LatexContext{_canonize :: LatexContext -> Bool
_canonize = Bool
shouldCanonize} =
  if Bool
shouldCanonize then [Rewritten] -> [Rewritten]
canonize [Rewritten]
rewrittens else [Rewritten]
rewrittens

canonizedExpressions :: [Expression] -> LatexContext -> [Expression]
canonizedExpressions :: [Expression] -> LatexContext -> [Expression]
canonizedExpressions [Expression]
exprs LatexContext{_canonize :: LatexContext -> Bool
_canonize = Bool
shouldCanonize} =
  if Bool
shouldCanonize then (Expression -> Expression) -> [Expression] -> [Expression]
forall a b. (a -> b) -> [a] -> [b]
map Expression -> Expression
canonizeExpr [Expression]
exprs else [Expression]
exprs

compressedExpressions :: [Expression] -> LatexContext -> [Expression]
compressedExpressions :: [Expression] -> LatexContext -> [Expression]
compressedExpressions [Expression]
exprs ctx :: LatexContext
ctx@LatexContext{Bool
Int
Maybe String
Expression
SugarType
LineFormat
_sugar :: LatexContext -> SugarType
_line :: LatexContext -> LineFormat
_margin :: LatexContext -> Int
_nonumber :: LatexContext -> Bool
_compress :: LatexContext -> Bool
_canonize :: LatexContext -> Bool
_meetPopularity :: LatexContext -> Int
_meetLength :: LatexContext -> Int
_focus :: LatexContext -> Expression
_expression :: LatexContext -> Maybe String
_label :: LatexContext -> Maybe String
_meetPrefix :: LatexContext -> Maybe String
_headers :: LatexContext -> Bool
_hideRho :: LatexContext -> Bool
_sugar :: SugarType
_line :: LineFormat
_margin :: Int
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe String
_label :: Maybe String
_meetPrefix :: Maybe String
_headers :: Bool
_hideRho :: Bool
..} =
  if Bool
_compress then [Expression] -> LatexContext -> [Expression]
meetInExpressions [Expression]
exprs LatexContext
ctx else [Expression]
exprs

rewrittensToLatex :: Rewrittens' -> LatexContext -> IO String
rewrittensToLatex :: Rewrittens' -> LatexContext -> IO String
rewrittensToLatex ([Rewritten]
rewrittens, Bool
exceeded) ctx :: LatexContext
ctx@LatexContext{_focus :: LatexContext -> Expression
_focus = Expression
ExRoot} =
  String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ LatexContext -> String
preamble LatexContext
ctx
        , [String] -> [Rewritten] -> (Int -> Expression -> String) -> String
forall a.
[String]
-> [(a, Maybe (Judgment, String))]
-> (Int -> a -> String)
-> String
body ([Rewritten] -> LatexContext -> [String]
stepComments [Rewritten]
rewrittens LatexContext
ctx) ([Rewritten] -> LatexContext -> [Rewritten]
canonizedRewrittens ([Rewritten] -> LatexContext -> [Rewritten]
compressedRewrittens [Rewritten]
rewrittens LatexContext
ctx) LatexContext
ctx) (\Int
tabs Expression
expr -> EXPRESSION -> LatexContext -> String
forall a.
(ToSalty a, ToASCII a, ToSingleLine a, ToLaTeX a, WithMargin a,
 Render a) =>
a -> LatexContext -> String
renderToLatex (LatexContext -> EXPRESSION -> EXPRESSION
shown LatexContext
ctx (Int -> Expression -> EXPRESSION
expressionToCSTFrom Int
tabs Expression
expr)) LatexContext
ctx)
        , Bool -> Judgment -> LatexContext -> String
ending Bool
exceeded ([Judgment] -> Judgment
forall a. HasCallStack => [a] -> a
last ([Maybe (Judgment, String)] -> [Judgment]
arrows ((Rewritten -> Maybe (Judgment, String))
-> [Rewritten] -> [Maybe (Judgment, String)]
forall a b. (a -> b) -> [a] -> [b]
map Rewritten -> Maybe (Judgment, String)
forall a b. (a, b) -> b
snd [Rewritten]
rewrittens))) LatexContext
ctx
        ]
    )
rewrittensToLatex ([Rewritten]
rewrittens, Bool
exceeded) ctx :: LatexContext
ctx@LatexContext{Bool
Int
Maybe String
Expression
SugarType
LineFormat
_sugar :: LatexContext -> SugarType
_line :: LatexContext -> LineFormat
_margin :: LatexContext -> Int
_nonumber :: LatexContext -> Bool
_compress :: LatexContext -> Bool
_canonize :: LatexContext -> Bool
_meetPopularity :: LatexContext -> Int
_meetLength :: LatexContext -> Int
_focus :: LatexContext -> Expression
_expression :: LatexContext -> Maybe String
_label :: LatexContext -> Maybe String
_meetPrefix :: LatexContext -> Maybe String
_headers :: LatexContext -> Bool
_hideRho :: LatexContext -> Bool
_sugar :: SugarType
_line :: LineFormat
_margin :: Int
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe String
_label :: Maybe String
_meetPrefix :: Maybe String
_headers :: Bool
_hideRho :: Bool
..} = do
  let ([Expression]
exprs, [Maybe (Judgment, String)]
rules) = [Rewritten] -> ([Expression], [Maybe (Judgment, String)])
forall a b. [(a, b)] -> ([a], [b])
unzip [Rewritten]
rewrittens
  [Expression]
focused <- (Expression -> IO Expression) -> [Expression] -> IO [Expression]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Expression -> Expression -> IO Expression
locatedExpression Expression
_focus) [Expression]
exprs
  String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ LatexContext -> String
preamble LatexContext
ctx
        , [String] -> [Rewritten] -> (Int -> Expression -> String) -> String
forall a.
[String]
-> [(a, Maybe (Judgment, String))]
-> (Int -> a -> String)
-> String
body ([Rewritten] -> LatexContext -> [String]
stepComments [Rewritten]
rewrittens LatexContext
ctx) ([Expression] -> [Maybe (Judgment, String)] -> [Rewritten]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Expression] -> LatexContext -> [Expression]
canonizedExpressions ([Expression] -> LatexContext -> [Expression]
compressedExpressions [Expression]
focused LatexContext
ctx) LatexContext
ctx) [Maybe (Judgment, String)]
rules) (\Int
tabs Expression
expr -> EXPRESSION -> LatexContext -> String
forall a.
(ToSalty a, ToASCII a, ToSingleLine a, ToLaTeX a, WithMargin a,
 Render a) =>
a -> LatexContext -> String
renderToLatex (LatexContext -> EXPRESSION -> EXPRESSION
shown LatexContext
ctx (Int -> Expression -> EXPRESSION
expressionToCSTFrom Int
tabs Expression
expr)) LatexContext
ctx)
        , Bool -> Judgment -> LatexContext -> String
ending Bool
exceeded ([Judgment] -> Judgment
forall a. HasCallStack => [a] -> a
last ([Maybe (Judgment, String)] -> [Judgment]
arrows ((Rewritten -> Maybe (Judgment, String))
-> [Rewritten] -> [Maybe (Judgment, String)]
forall a b. (a -> b) -> [a] -> [b]
map Rewritten -> Maybe (Judgment, String)
forall a b. (a, b) -> b
snd [Rewritten]
rewrittens))) LatexContext
ctx
        ]
    )

shown :: LatexContext -> EXPRESSION -> EXPRESSION
shown :: LatexContext -> EXPRESSION -> EXPRESSION
shown LatexContext{Bool
Int
Maybe String
Expression
SugarType
LineFormat
_sugar :: LatexContext -> SugarType
_line :: LatexContext -> LineFormat
_margin :: LatexContext -> Int
_nonumber :: LatexContext -> Bool
_compress :: LatexContext -> Bool
_canonize :: LatexContext -> Bool
_meetPopularity :: LatexContext -> Int
_meetLength :: LatexContext -> Int
_focus :: LatexContext -> Expression
_expression :: LatexContext -> Maybe String
_label :: LatexContext -> Maybe String
_meetPrefix :: LatexContext -> Maybe String
_headers :: LatexContext -> Bool
_hideRho :: LatexContext -> Bool
_sugar :: SugarType
_line :: LineFormat
_margin :: Int
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe String
_label :: Maybe String
_meetPrefix :: Maybe String
_headers :: Bool
_hideRho :: Bool
..}
  | Bool
_hideRho = SugarType -> EXPRESSION -> EXPRESSION
withoutRho SugarType
_sugar
  | Bool
otherwise = EXPRESSION -> EXPRESSION
forall a. a -> a
id

expressionToLaTeX :: Expression -> LatexContext -> String
expressionToLaTeX :: Expression -> LatexContext -> String
expressionToLaTeX Expression
ex LatexContext
ctx =
  [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ LatexContext -> String
preamble LatexContext
ctx
    , EXPRESSION -> LatexContext -> String
forall a.
(ToSalty a, ToASCII a, ToSingleLine a, ToLaTeX a, WithMargin a,
 Render a) =>
a -> LatexContext -> String
renderToLatex (LatexContext -> EXPRESSION -> EXPRESSION
shown LatexContext
ctx (Expression -> EXPRESSION
expressionToCST Expression
ex)) LatexContext
ctx
    , LatexContext -> String
period LatexContext
ctx
    ]

piped :: T.Text -> T.Text
piped :: Text -> Text
piped Text
str = Text
"|" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
forall a. ToLaTeX a => a -> a
toLaTeX Text
str Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"|"

class ToLaTeX a where
  toLaTeX :: a -> a

instance ToLaTeX EXPRESSION where
  toLaTeX :: EXPRESSION -> EXPRESSION
toLaTeX EX_ATTR{ATTRIBUTE
attr :: ATTRIBUTE
$sel:attr:EX_GLOBAL :: EXPRESSION -> ATTRIBUTE
..} = ATTRIBUTE -> EXPRESSION
EX_ATTR (ATTRIBUTE -> ATTRIBUTE
forall a. ToLaTeX a => a -> a
toLaTeX ATTRIBUTE
attr)
  toLaTeX EX_FORMATION{BINDING
TAB
EOL
RSB
LSB
lsb :: LSB
eol :: EOL
tab :: TAB
binding :: BINDING
eol' :: EOL
tab' :: TAB
rsb :: RSB
$sel:lsb:EX_GLOBAL :: EXPRESSION -> LSB
$sel:eol:EX_GLOBAL :: EXPRESSION -> EOL
$sel:tab:EX_GLOBAL :: EXPRESSION -> TAB
$sel:binding:EX_GLOBAL :: EXPRESSION -> BINDING
$sel:eol':EX_GLOBAL :: EXPRESSION -> EOL
$sel:tab':EX_GLOBAL :: EXPRESSION -> TAB
$sel:rsb:EX_GLOBAL :: EXPRESSION -> RSB
..} = LSB -> EOL -> TAB -> BINDING -> EOL -> TAB -> RSB -> EXPRESSION
EX_FORMATION LSB
lsb EOL
eol TAB
tab (BINDING -> BINDING
forall a. ToLaTeX a => a -> a
toLaTeX BINDING
binding) EOL
eol' TAB
tab' RSB
rsb
  toLaTeX EX_APPLICATION{Int
EXPRESSION
APP_ARGUMENT
TAB
EOL
SPACE
$sel:eol:EX_GLOBAL :: EXPRESSION -> EOL
$sel:tab:EX_GLOBAL :: EXPRESSION -> TAB
$sel:eol':EX_GLOBAL :: EXPRESSION -> EOL
$sel:tab':EX_GLOBAL :: EXPRESSION -> TAB
expr :: EXPRESSION
space :: SPACE
eol :: EOL
tab :: TAB
argument :: APP_ARGUMENT
eol' :: EOL
tab' :: TAB
indent :: Int
$sel:expr:EX_GLOBAL :: EXPRESSION -> EXPRESSION
$sel:space:EX_GLOBAL :: EXPRESSION -> SPACE
$sel:argument:EX_GLOBAL :: EXPRESSION -> APP_ARGUMENT
$sel:indent:EX_GLOBAL :: EXPRESSION -> Int
..} = EXPRESSION
-> SPACE
-> EOL
-> TAB
-> APP_ARGUMENT
-> EOL
-> TAB
-> Int
-> EXPRESSION
EX_APPLICATION (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr) SPACE
SPACE EOL
eol TAB
tab (APP_ARGUMENT -> APP_ARGUMENT
forall a. ToLaTeX a => a -> a
toLaTeX APP_ARGUMENT
argument) EOL
eol' TAB
tab' Int
indent
  toLaTeX EX_DISPATCH{ATTRIBUTE
EXPRESSION
SPACE
$sel:attr:EX_GLOBAL :: EXPRESSION -> ATTRIBUTE
$sel:expr:EX_GLOBAL :: EXPRESSION -> EXPRESSION
$sel:space:EX_GLOBAL :: EXPRESSION -> SPACE
expr :: EXPRESSION
space :: SPACE
attr :: ATTRIBUTE
..} = EXPRESSION -> SPACE -> ATTRIBUTE -> EXPRESSION
EX_DISPATCH (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr) SPACE
SPACE (ATTRIBUTE -> ATTRIBUTE
forall a. ToLaTeX a => a -> a
toLaTeX ATTRIBUTE
attr)
  toLaTeX EX_PHI_MEET{Int
Maybe String
EXPRESSION
$sel:expr:EX_GLOBAL :: EXPRESSION -> EXPRESSION
prefix :: Maybe String
idx :: Int
expr :: EXPRESSION
$sel:prefix:EX_GLOBAL :: EXPRESSION -> Maybe String
$sel:idx:EX_GLOBAL :: EXPRESSION -> Int
..} = Maybe String -> Int -> EXPRESSION -> EXPRESSION
EX_PHI_MEET Maybe String
prefix Int
idx (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr)
  toLaTeX EX_PHI_AGAIN{Int
Maybe String
EXPRESSION
$sel:expr:EX_GLOBAL :: EXPRESSION -> EXPRESSION
$sel:prefix:EX_GLOBAL :: EXPRESSION -> Maybe String
$sel:idx:EX_GLOBAL :: EXPRESSION -> Int
prefix :: Maybe String
idx :: Int
expr :: EXPRESSION
..} = Maybe String -> Int -> EXPRESSION -> EXPRESSION
EX_PHI_AGAIN Maybe String
prefix Int
idx (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr)
  toLaTeX EX_META{META
meta :: META
$sel:meta:EX_GLOBAL :: EXPRESSION -> META
..} = META -> EXPRESSION
EX_META (META -> META
forall a. ToLaTeX a => a -> a
toLaTeX META
meta)
  toLaTeX EX_XI{} = XI -> EXPRESSION
EX_XI XI
XI'
  toLaTeX EX_NONFINITE{[Argument]
NonFinite
TAB
GLOBAL
$sel:tab:EX_GLOBAL :: EXPRESSION -> TAB
global :: GLOBAL
nonfinite :: NonFinite
tab :: TAB
rhos :: [Argument]
$sel:global:EX_GLOBAL :: EXPRESSION -> GLOBAL
$sel:rhos:EX_GLOBAL :: EXPRESSION -> [Argument]
$sel:nonfinite:EX_GLOBAL :: EXPRESSION -> NonFinite
..} = EXPRESSION -> SPACE -> ATTRIBUTE -> EXPRESSION
EX_DISPATCH (GLOBAL -> EXPRESSION
EX_GLOBAL GLOBAL
global) SPACE
SPACE (ATTRIBUTE -> ATTRIBUTE
forall a. ToLaTeX a => a -> a
toLaTeX (Text -> ATTRIBUTE
AT_LABEL (NonFinite -> Text
nonFiniteName NonFinite
nonfinite)))
  toLaTeX EX_BYTES{BYTES
bytes :: BYTES
$sel:bytes:EX_GLOBAL :: EXPRESSION -> BYTES
..} = BYTES -> EXPRESSION
EX_BYTES (BYTES -> BYTES
forall a. ToLaTeX a => a -> a
toLaTeX BYTES
bytes)
  toLaTeX EX_SINGLE{EXPRESSION
PAIR
SPACE
$sel:space:EX_GLOBAL :: EXPRESSION -> SPACE
pair :: PAIR
space :: SPACE
formation :: EXPRESSION
$sel:pair:EX_GLOBAL :: EXPRESSION -> PAIR
$sel:formation:EX_GLOBAL :: EXPRESSION -> EXPRESSION
..} = PAIR -> SPACE -> EXPRESSION -> EXPRESSION
EX_SINGLE (PAIR -> PAIR
forall a. ToLaTeX a => a -> a
toLaTeX PAIR
pair) SPACE
SPACE (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
formation)
  toLaTeX EX_STRING{String
[Argument]
TAB
$sel:tab:EX_GLOBAL :: EXPRESSION -> TAB
$sel:rhos:EX_GLOBAL :: EXPRESSION -> [Argument]
str :: String
tab :: TAB
rhos :: [Argument]
$sel:str:EX_GLOBAL :: EXPRESSION -> String
..} = String -> TAB -> [Argument] -> EXPRESSION
EX_STRING (Text -> String
T.unpack (Text -> Text
forall a. ToLaTeX a => a -> a
toLaTeX (String -> Text
T.pack String
str))) TAB
tab [Argument]
rhos
  toLaTeX num :: EXPRESSION
num@EX_NUMBER{} = ATTRIBUTE -> EXPRESSION
EX_ATTR (ATTRIBUTE -> ATTRIBUTE
forall a. ToLaTeX a => a -> a
toLaTeX (Text -> ATTRIBUTE
AT_LABEL (EXPRESSION -> Text
forall a. Render a => a -> Text
render EXPRESSION
num)))
  toLaTeX EXPRESSION
expr = EXPRESSION
expr

instance ToLaTeX ATTRIBUTE where
  toLaTeX :: ATTRIBUTE -> ATTRIBUTE
toLaTeX AT_LABEL{Text
label :: Text
$sel:label:AT_LABEL :: ATTRIBUTE -> Text
..} = Text -> ATTRIBUTE
AT_LABEL (Text -> Text
piped Text
label)
  toLaTeX AT_META{META
meta :: META
$sel:meta:AT_LABEL :: ATTRIBUTE -> META
..} = META -> ATTRIBUTE
AT_META (META -> META
forall a. ToLaTeX a => a -> a
toLaTeX META
meta)
  toLaTeX AT_LAMBDA{} = LAMBDA -> ATTRIBUTE
AT_LAMBDA LAMBDA
LAMBDA'
  toLaTeX AT_DELTA{} = DELTA -> ATTRIBUTE
AT_DELTA DELTA
DELTA'
  toLaTeX AT_REST{} = DOTS -> ATTRIBUTE
AT_REST DOTS
DOTS'
  toLaTeX AT_RHO{} = RHO -> ATTRIBUTE
AT_RHO RHO
RHO'
  toLaTeX ATTRIBUTE
attr = ATTRIBUTE
attr

instance ToLaTeX APP_BINDING where
  toLaTeX :: APP_BINDING -> APP_BINDING
toLaTeX APP_BINDING{PAIR
pair :: PAIR
$sel:pair:APP_BINDING :: APP_BINDING -> PAIR
..} = PAIR -> APP_BINDING
APP_BINDING (PAIR -> PAIR
forall a. ToLaTeX a => a -> a
toLaTeX PAIR
pair)

instance ToLaTeX BINDING where
  toLaTeX :: BINDING -> BINDING
toLaTeX BI_PAIR{BINDINGS
PAIR
TAB
pair :: PAIR
bindings :: BINDINGS
tab :: TAB
$sel:pair:BI_PAIR :: BINDING -> PAIR
$sel:bindings:BI_PAIR :: BINDING -> BINDINGS
$sel:tab:BI_PAIR :: BINDING -> TAB
..} = PAIR -> BINDINGS -> TAB -> BINDING
BI_PAIR (PAIR -> PAIR
forall a. ToLaTeX a => a -> a
toLaTeX PAIR
pair) (BINDINGS -> BINDINGS
forall a. ToLaTeX a => a -> a
toLaTeX BINDINGS
bindings) TAB
tab
  toLaTeX BI_META{BINDINGS
TAB
META
$sel:bindings:BI_PAIR :: BINDING -> BINDINGS
$sel:tab:BI_PAIR :: BINDING -> TAB
meta :: META
bindings :: BINDINGS
tab :: TAB
$sel:meta:BI_PAIR :: BINDING -> META
..} = META -> BINDINGS -> TAB -> BINDING
BI_META (META -> META
forall a. ToLaTeX a => a -> a
toLaTeX META
meta) (BINDINGS -> BINDINGS
forall a. ToLaTeX a => a -> a
toLaTeX BINDINGS
bindings) TAB
tab
  toLaTeX BINDING
bd = BINDING
bd

instance ToLaTeX BINDINGS where
  toLaTeX :: BINDINGS -> BINDINGS
toLaTeX BDS_PAIR{BINDINGS
PAIR
TAB
EOL
eol :: EOL
tab :: TAB
pair :: PAIR
bindings :: BINDINGS
$sel:eol:BDS_PAIR :: BINDINGS -> EOL
$sel:tab:BDS_PAIR :: BINDINGS -> TAB
$sel:pair:BDS_PAIR :: BINDINGS -> PAIR
$sel:bindings:BDS_PAIR :: BINDINGS -> BINDINGS
..} = EOL -> TAB -> PAIR -> BINDINGS -> BINDINGS
BDS_PAIR EOL
eol TAB
tab (PAIR -> PAIR
forall a. ToLaTeX a => a -> a
toLaTeX PAIR
pair) (BINDINGS -> BINDINGS
forall a. ToLaTeX a => a -> a
toLaTeX BINDINGS
bindings)
  toLaTeX BDS_META{BINDINGS
TAB
META
EOL
$sel:eol:BDS_PAIR :: BINDINGS -> EOL
$sel:tab:BDS_PAIR :: BINDINGS -> TAB
$sel:bindings:BDS_PAIR :: BINDINGS -> BINDINGS
eol :: EOL
tab :: TAB
meta :: META
bindings :: BINDINGS
$sel:meta:BDS_PAIR :: BINDINGS -> META
..} = EOL -> TAB -> META -> BINDINGS -> BINDINGS
BDS_META EOL
eol TAB
tab (META -> META
forall a. ToLaTeX a => a -> a
toLaTeX META
meta) (BINDINGS -> BINDINGS
forall a. ToLaTeX a => a -> a
toLaTeX BINDINGS
bindings)
  toLaTeX BINDINGS
bds = BINDINGS
bds

instance ToLaTeX PAIR where
  toLaTeX :: PAIR -> PAIR
toLaTeX PA_DELTA{BYTES
bytes :: BYTES
$sel:bytes:PA_TAU :: PAIR -> BYTES
..} = PAIR -> PAIR
forall a. ToLaTeX a => a -> a
toLaTeX (BYTES -> PAIR
PA_DELTA' BYTES
bytes)
  toLaTeX PA_DELTA'{BYTES
$sel:bytes:PA_TAU :: PAIR -> BYTES
bytes :: BYTES
..} = BYTES -> PAIR
PA_DELTA' (BYTES -> BYTES
forall a. ToLaTeX a => a -> a
toLaTeX BYTES
bytes)
  toLaTeX PA_LAMBDA{Text
func :: Text
$sel:func:PA_TAU :: PAIR -> Text
..} = Text -> PAIR
PA_LAMBDA' (Text -> Text
piped Text
func)
  toLaTeX PA_LAMBDA'{Text
$sel:func:PA_TAU :: PAIR -> Text
func :: Text
..} = Text -> PAIR
PA_LAMBDA' (Text -> Text
piped Text
func)
  toLaTeX PA_VOID{ATTRIBUTE
VOID
ARROW
attr :: ATTRIBUTE
arrow :: ARROW
void :: VOID
$sel:attr:PA_TAU :: PAIR -> ATTRIBUTE
$sel:arrow:PA_TAU :: PAIR -> ARROW
$sel:void:PA_TAU :: PAIR -> VOID
..} = ATTRIBUTE -> ARROW -> VOID -> PAIR
PA_VOID (ATTRIBUTE -> ATTRIBUTE
forall a. ToLaTeX a => a -> a
toLaTeX ATTRIBUTE
attr) ARROW
arrow VOID
void
  toLaTeX PA_TAU{ATTRIBUTE
EXPRESSION
ARROW
$sel:attr:PA_TAU :: PAIR -> ATTRIBUTE
$sel:arrow:PA_TAU :: PAIR -> ARROW
attr :: ATTRIBUTE
arrow :: ARROW
expr :: EXPRESSION
$sel:expr:PA_TAU :: PAIR -> EXPRESSION
..} = ATTRIBUTE -> ARROW -> EXPRESSION -> PAIR
PA_TAU (ATTRIBUTE -> ATTRIBUTE
forall a. ToLaTeX a => a -> a
toLaTeX ATTRIBUTE
attr) ARROW
arrow (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr)
  toLaTeX PA_ALPHA{EXPRESSION
ALPHA
ARROW
$sel:arrow:PA_TAU :: PAIR -> ARROW
$sel:expr:PA_TAU :: PAIR -> EXPRESSION
alpha :: ALPHA
arrow :: ARROW
expr :: EXPRESSION
$sel:alpha:PA_TAU :: PAIR -> ALPHA
..} =
    let subscript :: Text
subscript = case ALPHA
alpha of
          AL_IDX ALPHA'
_ Int
n -> Int -> Text
forall a. Render a => a -> Text
render Int
n
          AL_META ALPHA'
_ META
mt -> META_HEAD -> Text
forall a. Render a => a -> Text
render (META -> META_HEAD
hd META
mt) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> META -> Text
rest META
mt
     in ATTRIBUTE -> ARROW -> EXPRESSION -> PAIR
PA_TAU (Text -> ATTRIBUTE
AT_LABEL (Text
"\\phiTerminal{\\alpha_{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
subscript Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}}")) ARROW
arrow (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr)
  toLaTeX PA_FORMATION{[ATTRIBUTE]
ATTRIBUTE
EXPRESSION
ARROW
$sel:attr:PA_TAU :: PAIR -> ATTRIBUTE
$sel:arrow:PA_TAU :: PAIR -> ARROW
$sel:expr:PA_TAU :: PAIR -> EXPRESSION
attr :: ATTRIBUTE
voids :: [ATTRIBUTE]
arrow :: ARROW
expr :: EXPRESSION
$sel:voids:PA_TAU :: PAIR -> [ATTRIBUTE]
..} = ATTRIBUTE -> [ATTRIBUTE] -> ARROW -> EXPRESSION -> PAIR
PA_FORMATION (ATTRIBUTE -> ATTRIBUTE
forall a. ToLaTeX a => a -> a
toLaTeX ATTRIBUTE
attr) ((ATTRIBUTE -> ATTRIBUTE) -> [ATTRIBUTE] -> [ATTRIBUTE]
forall a b. (a -> b) -> [a] -> [b]
map ATTRIBUTE -> ATTRIBUTE
forall a. ToLaTeX a => a -> a
toLaTeX [ATTRIBUTE]
voids) ARROW
arrow (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr)
  toLaTeX PA_META_DELTA{META
meta :: META
$sel:meta:PA_TAU :: PAIR -> META
..} = PAIR -> PAIR
forall a. ToLaTeX a => a -> a
toLaTeX (META -> PAIR
PA_META_DELTA' META
meta)
  toLaTeX PA_META_DELTA'{META
$sel:meta:PA_TAU :: PAIR -> META
meta :: META
..} = META -> PAIR
PA_META_DELTA' (META -> META
forall a. ToLaTeX a => a -> a
toLaTeX META
meta)
  toLaTeX PA_META_LAMBDA{META
$sel:meta:PA_TAU :: PAIR -> META
meta :: META
..} = PAIR -> PAIR
forall a. ToLaTeX a => a -> a
toLaTeX (META -> PAIR
PA_META_LAMBDA' META
meta)
  toLaTeX PA_META_LAMBDA'{META
$sel:meta:PA_TAU :: PAIR -> META
meta :: META
..} = META -> PAIR
PA_META_LAMBDA' (META -> META
forall a. ToLaTeX a => a -> a
toLaTeX META
meta)
  toLaTeX folded :: PAIR
folded@PA_FOLDED{} = PAIR
folded

instance ToLaTeX META where
  toLaTeX :: META -> META
toLaTeX META{Text
EXCLAMATION
META_HEAD
$sel:hd:META :: META -> META_HEAD
$sel:rest:META :: META -> Text
excl :: EXCLAMATION
hd :: META_HEAD
rest :: Text
$sel:excl:META :: META -> EXCLAMATION
..} =
    let idx :: Maybe Int
idx = String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe (Text -> String
T.unpack Text
rest) :: Maybe Int
        rest' :: Text
rest'
          | Text -> Int
T.length Text
rest Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Maybe Int -> Bool
forall a. Maybe a -> Bool
isJust Maybe Int
idx = Char -> Text -> Text
T.cons Char
'_' Text
rest
          | Text -> Int
T.length Text
rest Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 Bool -> Bool -> Bool
&& Maybe Int -> Bool
forall a. Maybe a -> Bool
isJust Maybe Int
idx = Text
"_{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
rest Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"
          | Bool
otherwise = Text
rest
     in EXCLAMATION -> META_HEAD -> Text -> META
META EXCLAMATION
NO_EXCL (META_HEAD -> META_HEAD
forall a. ToLaTeX a => a -> a
toLaTeX META_HEAD
hd) Text
rest'

instance ToLaTeX META_HEAD where
  toLaTeX :: META_HEAD -> META_HEAD
toLaTeX META_HEAD
E = META_HEAD
E'
  toLaTeX META_HEAD
N = META_HEAD
N'
  toLaTeX META_HEAD
K = META_HEAD
K'
  toLaTeX META_HEAD
A = META_HEAD
TAU'
  toLaTeX META_HEAD
TAU = META_HEAD
TAU'
  toLaTeX META_HEAD
B = META_HEAD
B'
  toLaTeX META_HEAD
D = META_HEAD
D'
  toLaTeX META_HEAD
D'' = META_HEAD
D'
  toLaTeX META_HEAD
F = META_HEAD
F''
  toLaTeX META_HEAD
F' = META_HEAD
F''
  toLaTeX META_HEAD
S = META_HEAD
S''
  toLaTeX META_HEAD
S' = META_HEAD
S''
  toLaTeX META_HEAD
mh = META_HEAD
mh

instance ToLaTeX BYTES where
  toLaTeX :: BYTES -> BYTES
toLaTeX (BT_META META
meta) = META -> BYTES
BT_META (META -> META
forall a. ToLaTeX a => a -> a
toLaTeX META
meta)
  toLaTeX BYTES
bts = BYTES -> BYTES
BT_PIPED BYTES
bts

instance ToLaTeX APP_ARGUMENT where
  toLaTeX :: APP_ARGUMENT -> APP_ARGUMENT
toLaTeX (AA_TAU APP_BINDING
tau) = APP_BINDING -> APP_ARGUMENT
AA_TAU (APP_BINDING -> APP_BINDING
forall a. ToLaTeX a => a -> a
toLaTeX APP_BINDING
tau)
  toLaTeX (AA_TAUS BINDING
taus) = BINDING -> APP_ARGUMENT
AA_TAUS (BINDING -> BINDING
forall a. ToLaTeX a => a -> a
toLaTeX BINDING
taus)
  toLaTeX (AA_EXPRS APP_ARG
args) = APP_ARG -> APP_ARGUMENT
AA_EXPRS (APP_ARG -> APP_ARG
forall a. ToLaTeX a => a -> a
toLaTeX APP_ARG
args)

instance ToLaTeX APP_ARG where
  toLaTeX :: APP_ARG -> APP_ARG
toLaTeX APP_ARG{EXPRESSION
APP_ARGS
expr :: EXPRESSION
args :: APP_ARGS
$sel:expr:APP_ARG :: APP_ARG -> EXPRESSION
$sel:args:APP_ARG :: APP_ARG -> APP_ARGS
..} = EXPRESSION -> APP_ARGS -> APP_ARG
APP_ARG (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr) (APP_ARGS -> APP_ARGS
forall a. ToLaTeX a => a -> a
toLaTeX APP_ARGS
args)

instance ToLaTeX APP_ARGS where
  toLaTeX :: APP_ARGS -> APP_ARGS
toLaTeX AAS_EXPR{EXPRESSION
APP_ARGS
TAB
EOL
eol :: EOL
tab :: TAB
expr :: EXPRESSION
args :: APP_ARGS
$sel:eol:AAS_EXPR :: APP_ARGS -> EOL
$sel:tab:AAS_EXPR :: APP_ARGS -> TAB
$sel:expr:AAS_EXPR :: APP_ARGS -> EXPRESSION
$sel:args:AAS_EXPR :: APP_ARGS -> APP_ARGS
..} = EOL -> TAB -> EXPRESSION -> APP_ARGS -> APP_ARGS
AAS_EXPR EOL
eol TAB
tab (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr) (APP_ARGS -> APP_ARGS
forall a. ToLaTeX a => a -> a
toLaTeX APP_ARGS
args)
  toLaTeX APP_ARGS
args = APP_ARGS
args

instance ToLaTeX T.Text where
  toLaTeX :: Text -> Text
toLaTeX = (Char -> Text) -> Text -> Text
T.concatMap Char -> Text
escape
    where
      escape :: Char -> Text
escape Char
'#' = Text
"\\char35{}"
      escape Char
'$' = Text
"\\char36{}"
      escape Char
'%' = Text
"\\char37{}"
      escape Char
'&' = Text
"\\char38{}"
      escape Char
'@' = Text
"\\char64{}"
      escape Char
'^' = Text
"\\char94{}"
      escape Char
'\\' = Text
"\\char92{}"
      escape Char
'_' = Text
"\\char95{}"
      escape Char
'{' = Text
"\\char123{}"
      escape Char
'}' = Text
"\\char125{}"
      escape Char
'~' = Text
"\\char126{}"
      escape Char
'ρ' = RHO -> Text
forall a. Render a => a -> Text
render RHO
RHO'
      escape Char
'ξ' = XI -> Text
forall a. Render a => a -> Text
render XI
XI'
      escape Char
'φ' = Text
"\\phiTerminal{\\varphi}"
      escape Char
ch
        | Char -> Bool
isAscii Char
ch = Char -> Text
T.singleton Char
ch
        | Bool
otherwise = String -> Text
T.pack (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"[U+%04X]" (Char -> Int
ord Char
ch))

instance ToLaTeX SET where
  toLaTeX :: SET -> SET
toLaTeX ST_BINDING{BINDING
binding :: BINDING
$sel:binding:ST_BINDING :: SET -> BINDING
..} = BINDING -> SET
ST_BINDING (BINDING -> BINDING
forall a. ToLaTeX a => a -> a
toLaTeX BINDING
binding)
  toLaTeX ST_ATTRIBUTES{[ATTRIBUTE]
attrs :: [ATTRIBUTE]
$sel:attrs:ST_BINDING :: SET -> [ATTRIBUTE]
..} = [ATTRIBUTE] -> SET
ST_ATTRIBUTES ((ATTRIBUTE -> ATTRIBUTE) -> [ATTRIBUTE] -> [ATTRIBUTE]
forall a b. (a -> b) -> [a] -> [b]
map ATTRIBUTE -> ATTRIBUTE
forall a. ToLaTeX a => a -> a
toLaTeX [ATTRIBUTE]
attrs)

instance ToLaTeX NUMBER where
  toLaTeX :: NUMBER -> NUMBER
toLaTeX IDX_META{META
meta :: META
$sel:meta:IDX_META :: NUMBER -> META
..} = META -> NUMBER
IDX_META (META -> META
forall a. ToLaTeX a => a -> a
toLaTeX META
meta)
  toLaTeX LENGTH{BINDING
binding :: BINDING
$sel:binding:IDX_META :: NUMBER -> BINDING
..} = BINDING -> NUMBER
LENGTH (BINDING -> BINDING
forall a. ToLaTeX a => a -> a
toLaTeX BINDING
binding)
  toLaTeX DOMAIN{BINDING
$sel:binding:IDX_META :: NUMBER -> BINDING
binding :: BINDING
..} = BINDING -> NUMBER
DOMAIN (BINDING -> BINDING
forall a. ToLaTeX a => a -> a
toLaTeX BINDING
binding)
  toLaTeX literal :: NUMBER
literal@LITERAL{} = NUMBER
literal

instance ToLaTeX COMPARABLE where
  toLaTeX :: COMPARABLE -> COMPARABLE
toLaTeX CMP_EXPR{EXPRESSION
expr :: EXPRESSION
$sel:expr:CMP_ATTR :: COMPARABLE -> EXPRESSION
..} = EXPRESSION -> COMPARABLE
CMP_EXPR (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr)
  toLaTeX CMP_ATTR{ATTRIBUTE
attr :: ATTRIBUTE
$sel:attr:CMP_ATTR :: COMPARABLE -> ATTRIBUTE
..} = ATTRIBUTE -> COMPARABLE
CMP_ATTR (ATTRIBUTE -> ATTRIBUTE
forall a. ToLaTeX a => a -> a
toLaTeX ATTRIBUTE
attr)
  toLaTeX CMP_NUM{NUMBER
num :: NUMBER
$sel:num:CMP_ATTR :: COMPARABLE -> NUMBER
..} = NUMBER -> COMPARABLE
CMP_NUM (NUMBER -> NUMBER
forall a. ToLaTeX a => a -> a
toLaTeX NUMBER
num)

instance ToLaTeX CONDITION where
  toLaTeX :: CONDITION -> CONDITION
toLaTeX CO_BELONGS{SET
BELONGING
ATTRIBUTE
attr :: ATTRIBUTE
belongs :: BELONGING
set :: SET
$sel:attr:CO_EMPTY :: CONDITION -> ATTRIBUTE
$sel:belongs:CO_EMPTY :: CONDITION -> BELONGING
$sel:set:CO_EMPTY :: CONDITION -> SET
..} = ATTRIBUTE -> BELONGING -> SET -> CONDITION
CO_BELONGS (ATTRIBUTE -> ATTRIBUTE
forall a. ToLaTeX a => a -> a
toLaTeX ATTRIBUTE
attr) BELONGING
belongs (SET -> SET
forall a. ToLaTeX a => a -> a
toLaTeX SET
set)
  toLaTeX CO_LOGIC{[CONDITION]
LOGIC_OPERATOR
conditions :: [CONDITION]
operator :: LOGIC_OPERATOR
$sel:conditions:CO_EMPTY :: CONDITION -> [CONDITION]
$sel:operator:CO_EMPTY :: CONDITION -> LOGIC_OPERATOR
..} = [CONDITION] -> LOGIC_OPERATOR -> CONDITION
CO_LOGIC ((CONDITION -> CONDITION) -> [CONDITION] -> [CONDITION]
forall a b. (a -> b) -> [a] -> [b]
map CONDITION -> CONDITION
forall a. ToLaTeX a => a -> a
toLaTeX [CONDITION]
conditions) LOGIC_OPERATOR
operator
  toLaTeX CO_NF{EXPRESSION
expr :: EXPRESSION
$sel:expr:CO_EMPTY :: CONDITION -> EXPRESSION
..} = EXPRESSION -> CONDITION
CO_NF (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr)
  toLaTeX CO_ABSOLUTE{BELONGING
EXPRESSION
$sel:belongs:CO_EMPTY :: CONDITION -> BELONGING
$sel:expr:CO_EMPTY :: CONDITION -> EXPRESSION
expr :: EXPRESSION
belongs :: BELONGING
..} = EXPRESSION -> BELONGING -> CONDITION
CO_ABSOLUTE (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr) BELONGING
belongs
  toLaTeX CO_NOT{CONDITION
condition :: CONDITION
$sel:condition:CO_EMPTY :: CONDITION -> CONDITION
..} = CONDITION -> CONDITION
CO_NOT (CONDITION -> CONDITION
forall a. ToLaTeX a => a -> a
toLaTeX CONDITION
condition)
  toLaTeX CO_COMPARE{COMPARABLE
EQUAL
left :: COMPARABLE
equal :: EQUAL
right :: COMPARABLE
$sel:left:CO_EMPTY :: CONDITION -> COMPARABLE
$sel:equal:CO_EMPTY :: CONDITION -> EQUAL
$sel:right:CO_EMPTY :: CONDITION -> COMPARABLE
..} = COMPARABLE -> EQUAL -> COMPARABLE -> CONDITION
CO_COMPARE (COMPARABLE -> COMPARABLE
forall a. ToLaTeX a => a -> a
toLaTeX COMPARABLE
left) EQUAL
equal (COMPARABLE -> COMPARABLE
forall a. ToLaTeX a => a -> a
toLaTeX COMPARABLE
right)
  toLaTeX CO_MATCHES{String
EXPRESSION
$sel:expr:CO_EMPTY :: CONDITION -> EXPRESSION
regex :: String
expr :: EXPRESSION
$sel:regex:CO_EMPTY :: CONDITION -> String
..} = String -> EXPRESSION -> CONDITION
CO_MATCHES (Text -> String
T.unpack (Text -> Text
forall a. ToLaTeX a => a -> a
toLaTeX (String -> Text
T.pack String
regex))) (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr)
  toLaTeX CO_PART_OF{EXPRESSION
BINDING
$sel:expr:CO_EMPTY :: CONDITION -> EXPRESSION
expr :: EXPRESSION
binding :: BINDING
$sel:binding:CO_EMPTY :: CONDITION -> BINDING
..} = EXPRESSION -> BINDING -> CONDITION
CO_PART_OF (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr) (BINDING -> BINDING
forall a. ToLaTeX a => a -> a
toLaTeX BINDING
binding)
  toLaTeX CO_DISJOINT{[ATTRIBUTE]
[BINDING]
attrs :: [ATTRIBUTE]
groups :: [BINDING]
$sel:attrs:CO_EMPTY :: CONDITION -> [ATTRIBUTE]
$sel:groups:CO_EMPTY :: CONDITION -> [BINDING]
..} = [ATTRIBUTE] -> [BINDING] -> CONDITION
CO_DISJOINT ((ATTRIBUTE -> ATTRIBUTE) -> [ATTRIBUTE] -> [ATTRIBUTE]
forall a b. (a -> b) -> [a] -> [b]
map ATTRIBUTE -> ATTRIBUTE
forall a. ToLaTeX a => a -> a
toLaTeX [ATTRIBUTE]
attrs) ((BINDING -> BINDING) -> [BINDING] -> [BINDING]
forall a b. (a -> b) -> [a] -> [b]
map BINDING -> BINDING
forall a. ToLaTeX a => a -> a
toLaTeX [BINDING]
groups)
  toLaTeX CO_SUBSET{[ATTRIBUTE]
[BINDING]
BELONGING
$sel:belongs:CO_EMPTY :: CONDITION -> BELONGING
$sel:attrs:CO_EMPTY :: CONDITION -> [ATTRIBUTE]
$sel:groups:CO_EMPTY :: CONDITION -> [BINDING]
attrs :: [ATTRIBUTE]
belongs :: BELONGING
groups :: [BINDING]
..} = [ATTRIBUTE] -> BELONGING -> [BINDING] -> CONDITION
CO_SUBSET ((ATTRIBUTE -> ATTRIBUTE) -> [ATTRIBUTE] -> [ATTRIBUTE]
forall a b. (a -> b) -> [a] -> [b]
map ATTRIBUTE -> ATTRIBUTE
forall a. ToLaTeX a => a -> a
toLaTeX [ATTRIBUTE]
attrs) BELONGING
belongs ((BINDING -> BINDING) -> [BINDING] -> [BINDING]
forall a b. (a -> b) -> [a] -> [b]
map BINDING -> BINDING
forall a. ToLaTeX a => a -> a
toLaTeX [BINDING]
groups)
  toLaTeX CO_FORMATION{EXPRESSION
$sel:expr:CO_EMPTY :: CONDITION -> EXPRESSION
expr :: EXPRESSION
..} = EXPRESSION -> CONDITION
CO_FORMATION (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr)
  toLaTeX CONDITION
CO_EMPTY = CONDITION
CO_EMPTY

instance ToLaTeX EXTRA_ARG where
  toLaTeX :: EXTRA_ARG -> EXTRA_ARG
toLaTeX ARG_ATTR{ATTRIBUTE
attr :: ATTRIBUTE
$sel:attr:ARG_EXPR :: EXTRA_ARG -> ATTRIBUTE
..} = ATTRIBUTE -> EXTRA_ARG
ARG_ATTR (ATTRIBUTE -> ATTRIBUTE
forall a. ToLaTeX a => a -> a
toLaTeX ATTRIBUTE
attr)
  toLaTeX ARG_EXPR{EXPRESSION
expr :: EXPRESSION
$sel:expr:ARG_EXPR :: EXTRA_ARG -> EXPRESSION
..} = EXPRESSION -> EXTRA_ARG
ARG_EXPR (EXPRESSION -> EXPRESSION
forall a. ToLaTeX a => a -> a
toLaTeX EXPRESSION
expr)
  toLaTeX ARG_BINDING{BINDING
binding :: BINDING
$sel:binding:ARG_EXPR :: EXTRA_ARG -> BINDING
..} = BINDING -> EXTRA_ARG
ARG_BINDING (BINDING -> BINDING
forall a. ToLaTeX a => a -> a
toLaTeX BINDING
binding)
  toLaTeX bts :: EXTRA_ARG
bts@ARG_BYTES{} = EXTRA_ARG
bts

instance ToLaTeX EXTRA where
  toLaTeX :: EXTRA -> EXTRA
toLaTeX EXTRA{String
[EXTRA_ARG]
EXTRA_ARG
meta :: EXTRA_ARG
func :: String
args :: [EXTRA_ARG]
$sel:meta:EXTRA :: EXTRA -> EXTRA_ARG
$sel:func:EXTRA :: EXTRA -> String
$sel:args:EXTRA :: EXTRA -> [EXTRA_ARG]
..} = EXTRA_ARG -> String -> [EXTRA_ARG] -> EXTRA
EXTRA (EXTRA_ARG -> EXTRA_ARG
forall a. ToLaTeX a => a -> a
toLaTeX EXTRA_ARG
meta) String
func ((EXTRA_ARG -> EXTRA_ARG) -> [EXTRA_ARG] -> [EXTRA_ARG]
forall a b. (a -> b) -> [a] -> [b]
map EXTRA_ARG -> EXTRA_ARG
forall a. ToLaTeX a => a -> a
toLaTeX [EXTRA_ARG]
args)

explainRule :: Y.Rule -> String
explainRule :: Rule -> String
explainRule Rule
rule =
  String
-> Maybe String
-> String
-> String
-> String
-> Maybe Condition
-> Maybe [Extra]
-> String
trrule
    String
"\\phinoNormalizationRule"
    Rule
rule.label
    Rule
rule.name
    (EXPRESSION -> LatexContext -> String
forall a.
(ToSalty a, ToASCII a, ToSingleLine a, ToLaTeX a, WithMargin a,
 Render a) =>
a -> LatexContext -> String
renderToLatex (Expression -> EXPRESSION
expressionToCST Rule
rule.pattern) LatexContext
defaultLatexContext)
    (EXPRESSION -> LatexContext -> String
forall a.
(ToSalty a, ToASCII a, ToSingleLine a, ToLaTeX a, WithMargin a,
 Render a) =>
a -> LatexContext -> String
renderToLatex (Expression -> EXPRESSION
expressionToCST Rule
rule.result) LatexContext
defaultLatexContext)
    (Maybe Condition -> Maybe Condition -> Maybe Condition
joinedConditions Rule
rule.when Rule
rule.having)
    Rule
rule.where_
  where
    joinedConditions :: Maybe Y.Condition -> Maybe Y.Condition -> Maybe Y.Condition
    joinedConditions :: Maybe Condition -> Maybe Condition -> Maybe Condition
joinedConditions Maybe Condition
Nothing Maybe Condition
Nothing = Maybe Condition
forall a. Maybe a
Nothing
    joinedConditions first :: Maybe Condition
first@(Just Condition
_) Maybe Condition
Nothing = Maybe Condition
first
    joinedConditions Maybe Condition
Nothing second :: Maybe Condition
second@(Just Condition
_) = Maybe Condition
second
    joinedConditions (Just Condition
first) (Just Condition
second) = Condition -> Maybe Condition
forall a. a -> Maybe a
Just ([Condition] -> Condition
Y.And [Condition
first, Condition
second])

explainMorphRule :: Y.MorphRule -> String
explainMorphRule :: MorphRule -> String
explainMorphRule MorphRule
rule =
  String
-> String
-> Maybe String
-> Maybe Condition
-> [String]
-> String
-> String
inference
    String
"phinoMorphingInference"
    MorphRule
rule.name
    MorphRule
rule.label
    MorphRule
rule.when
    [String]
premises
    (String -> String -> String -> String -> String -> String
phinoMorph (Expression -> String
renderExpr MorphRule
rule.match) (Expression -> String
renderExpr MorphRule
rule.ematch) (Int -> Int -> String
conclusionStateName Int
final Int
1) (Int -> Int -> String
conclusionStateName Int
final Int
final) (Expression -> String
renderExpr MorphRule
rule.nresult))
  where
    ([String]
premises, Int
final) = [Premise] -> ([String], Int)
premisesToLatex MorphRule
rule.premises

explainDataizeRule :: Y.DataizeRule -> String
explainDataizeRule :: DataizeRule -> String
explainDataizeRule DataizeRule
rule =
  String
-> String
-> Maybe String
-> Maybe Condition
-> [String]
-> String
-> String
inference
    String
"phinoDataizationInference"
    DataizeRule
rule.name
    DataizeRule
rule.label
    DataizeRule
rule.when
    [String]
premises
    (String -> String -> String -> String -> String -> String
phinoDataize (Expression -> String
renderExpr DataizeRule
rule.match) (Expression -> String
renderExpr DataizeRule
rule.ematch) (Int -> Int -> String
conclusionStateName Int
final Int
1) (Int -> Int -> String
conclusionStateName Int
final Int
final) (Bytes -> String
renderBytes DataizeRule
rule.dresult))
  where
    ([String]
premises, Int
final) = [Premise] -> ([String], Int)
premisesToLatex DataizeRule
rule.premises

explainContextualizeRule :: Y.ContextualizeRule -> String
explainContextualizeRule :: ContextualizeRule -> String
explainContextualizeRule ContextualizeRule
rule =
  String
-> String
-> Maybe String
-> Maybe Condition
-> [String]
-> String
-> String
inference
    String
"phinoContextualizationInference"
    ContextualizeRule
rule.name
    ContextualizeRule
rule.label
    Maybe Condition
forall a. Maybe a
Nothing
    (([String], Int) -> [String]
forall a b. (a, b) -> a
fst ([Premise] -> ([String], Int)
premisesToLatex ContextualizeRule
rule.premises))
    (String -> String -> String -> String
phinoContextualize (Expression -> String
renderExpr ContextualizeRule
rule.match) (Expression -> String
renderExpr ContextualizeRule
rule.cmatch) (Expression -> String
renderExpr ContextualizeRule
rule.cresult))

stateName :: Int -> String
stateName :: Int -> String
stateName Int
n = String
"s_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n

conclusionStateName :: Int -> Int -> String
conclusionStateName :: Int -> Int -> String
conclusionStateName Int
final Int
index
  | Int
final Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = String
"s"
  | Bool
otherwise = Int -> String
stateName Int
index

premisesToLatex :: [Y.Premise] -> ([String], Int)
premisesToLatex :: [Premise] -> ([String], Int)
premisesToLatex = Int -> [Premise] -> ([String], Int)
go Int
1
  where
    go :: Int -> [Y.Premise] -> ([String], Int)
    go :: Int -> [Premise] -> ([String], Int)
go Int
index [] = ([], Int
index)
    go Int
index (Premise
premise : [Premise]
rest) = (String
rendered String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
more, Int
final)
      where
        (String
rendered, Int
next) = Int -> Premise -> (String, Int)
premiseToLatex Int
index Premise
premise
        ([String]
more, Int
final) = Int -> [Premise] -> ([String], Int)
go Int
next [Premise]
rest

premiseToLatex :: Int -> Y.Premise -> (String, Int)
premiseToLatex :: Int -> Premise -> (String, Int)
premiseToLatex Int
index Premise
premise = case Premise
premise.operation of
  Y.OpMorph Expression
arg Expression
universe -> (String -> String -> String -> String -> String -> String
phinoMorph (Expression -> String
renderExpr Expression
arg) (Expression -> String
renderExpr Expression
universe) (Int -> String
stateName Int
index) (Int -> String
stateName (Int
index Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) (Expression -> String
renderExpr (Text -> Expression
ExMeta Premise
premise.result)), Int
index Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
  Y.OpDataize Expression
arg Expression
universe -> (String -> String -> String -> String -> String -> String
phinoDataize (Expression -> String
renderExpr Expression
arg) (Expression -> String
renderExpr Expression
universe) (Int -> String
stateName Int
index) (Int -> String
stateName (Int
index Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) (Bytes -> String
renderBytes (Text -> Bytes
BtMeta Premise
premise.result)), Int
index Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
  Y.OpNormalize Expression
arg -> (String -> String -> String
phinoNormalize (Expression -> String
renderExpr Expression
arg) (Expression -> String
renderExpr (Text -> Expression
ExMeta Premise
premise.result)), Int
index)
  Y.OpEvaluate Expression
arg Expression
evalUniverse -> (String -> String -> String -> String -> String -> String
phinoEvaluate (Expression -> String
renderExpr Expression
arg) (Expression -> String
renderExpr Expression
evalUniverse) (Int -> String
stateName Int
index) (Int -> String
stateName (Int
index Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) (Expression -> String
renderExpr (Text -> Expression
ExMeta Premise
premise.result)), Int
index Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
  Y.OpContextualize Expression
arg Expression
context -> (String -> String -> String -> String
phinoContextualize (Expression -> String
renderExpr Expression
arg) (Expression -> String
renderExpr Expression
context) (Expression -> String
renderExpr (Text -> Expression
ExMeta Premise
premise.result)), Int
index)

inference :: String -> String -> Maybe String -> Maybe Y.Condition -> [String] -> String -> String
inference :: String
-> String
-> Maybe String
-> Maybe Condition
-> [String]
-> String
-> String
inference String
env String
name Maybe String
label Maybe Condition
cond [String]
premises String
conclusion =
  String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
    [String
"\\begin{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
env String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}", String
"  \\phinoName{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
escaped String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"]
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String] -> (String -> [String]) -> Maybe String -> [String]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\String
symbol -> [String
"  \\phinoLabel{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
symbol String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"]) Maybe String
label
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String] -> (String -> [String]) -> Maybe String -> [String]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\String
rendered -> [String
"  \\phinoCondition{ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rendered String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" }"]) (Maybe Condition -> Maybe String
conditionInLatex Maybe Condition
cond)
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\String
premise -> String
"  \\phinoPremise{ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
premise String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" }") [String]
premises
      [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"  \\phinoConclusion{ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
conclusion String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" }", String
"\\end{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
env String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"]

escaped :: String -> String
escaped :: String -> String
escaped = Text -> String
T.unpack (Text -> String) -> (String -> Text) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
forall a. ToLaTeX a => a -> a
toLaTeX (Text -> Text) -> (String -> Text) -> String -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack

renderExpr :: Expression -> String
renderExpr :: Expression -> String
renderExpr Expression
expr = EXPRESSION -> LatexContext -> String
forall a.
(ToSalty a, ToASCII a, ToSingleLine a, ToLaTeX a, WithMargin a,
 Render a) =>
a -> LatexContext -> String
renderToLatex (Expression -> EXPRESSION
expressionToCST Expression
expr) LatexContext
defaultLatexContext

renderBytes :: Bytes -> String
renderBytes :: Bytes -> String
renderBytes Bytes
bytes = Text -> String
T.unpack (BYTES -> Text
forall a. Render a => a -> Text
render (BYTES -> BYTES
forall a. ToLaTeX a => a -> a
toLaTeX (Bytes -> BYTES
forall a b. ToCST a b => a -> b
toCST' Bytes
bytes :: BYTES)))

trrule :: String -> Maybe String -> String -> String -> String -> Maybe Y.Condition -> Maybe [Y.Extra] -> String
trrule :: String
-> Maybe String
-> String
-> String
-> String
-> Maybe Condition
-> Maybe [Extra]
-> String
trrule String
macro Maybe String
label String
name String
lhs String
rhs Maybe Condition
cond Maybe [Extra]
extras =
  String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate
    String
"\n  "
    [ String
macro String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
labelArg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
escaped String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"
    , String -> String
braced String
lhs
    , String -> String
braced String
rhs
    , Maybe Condition -> String
conditionToLatex Maybe Condition
cond
    , Maybe [Extra] -> String
extraArgumentsToLatex Maybe [Extra]
extras
    ]
  where
    labelArg :: String
labelArg = String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (\String
symbol -> String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
symbol String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]") Maybe String
label

phinoMorph :: String -> String -> String -> String -> String -> String
phinoMorph :: String -> String -> String -> String -> String -> String
phinoMorph String
input String
univ String
sIn String
sOut String
output = String -> String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"\\phinoMorph{ %s }{ %s }{ %s }{ %s }{ %s }" String
input String
univ String
sIn String
output String
sOut

phinoDataize :: String -> String -> String -> String -> String -> String
phinoDataize :: String -> String -> String -> String -> String -> String
phinoDataize String
input String
univ String
sIn String
sOut String
output = String -> String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"\\phinoDataize{ %s }{ %s }{ %s }{ %s }{ %s }" String
input String
univ String
sIn String
output String
sOut

phinoNormalize :: String -> String -> String
phinoNormalize :: String -> String -> String
phinoNormalize String
input = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"\\phinoNormalize{ %s }{ %s }" String
input

phinoEvaluate :: String -> String -> String -> String -> String -> String
phinoEvaluate :: String -> String -> String -> String -> String -> String
phinoEvaluate String
input String
univ String
sIn String
sOut String
output = String -> String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"\\phinoEvaluate{ %s }{ %s }{ %s }{ %s }{ %s }" String
input String
univ String
sIn String
output String
sOut

phinoContextualize :: String -> String -> String -> String
phinoContextualize :: String -> String -> String -> String
phinoContextualize String
input String
context = String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"\\phinoContextualize{ %s }{ %s }{ %s }" String
input String
context

conditionInLatex :: Maybe Y.Condition -> Maybe String
conditionInLatex :: Maybe Condition -> Maybe String
conditionInLatex Maybe Condition
Nothing = Maybe String
forall a. Maybe a
Nothing
conditionInLatex (Just Condition
cond) = case Condition -> CONDITION
conditionToCST Condition
cond of
  CONDITION
CO_EMPTY -> Maybe String
forall a. Maybe a
Nothing
  CONDITION
cond' -> String -> Maybe String
forall a. a -> Maybe a
Just (CONDITION -> LatexContext -> String
forall a.
(ToSalty a, ToASCII a, ToSingleLine a, ToLaTeX a, WithMargin a,
 Render a) =>
a -> LatexContext -> String
renderToLatex CONDITION
cond' LatexContext
defaultLatexContext)

braced :: String -> String
braced :: String -> String
braced = String -> String -> String
forall r. PrintfType r => String -> r
printf String
"{ %s }"

conditionToLatex :: Maybe Y.Condition -> String
conditionToLatex :: Maybe Condition -> String
conditionToLatex Maybe Condition
Nothing = String
"{ }"
conditionToLatex (Just Condition
cond) = case Condition -> CONDITION
conditionToCST Condition
cond of
  CONDITION
CO_EMPTY -> String
"{ }"
  CONDITION
cond' -> String -> String
braced (CONDITION -> LatexContext -> String
forall a.
(ToSalty a, ToASCII a, ToSingleLine a, ToLaTeX a, WithMargin a,
 Render a) =>
a -> LatexContext -> String
renderToLatex CONDITION
cond' LatexContext
defaultLatexContext)

extraArgumentsToLatex :: Maybe [Y.Extra] -> String
extraArgumentsToLatex :: Maybe [Extra] -> String
extraArgumentsToLatex Maybe [Extra]
Nothing = String
"{ }"
extraArgumentsToLatex (Just [Extra]
extras) =
  let extras' :: [String]
extras' = (Extra -> String) -> [Extra] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((EXTRA -> LatexContext -> String
forall a.
(ToSalty a, ToASCII a, ToSingleLine a, ToLaTeX a, WithMargin a,
 Render a) =>
a -> LatexContext -> String
`renderToLatex` LatexContext
defaultLatexContext) (EXTRA -> String) -> (Extra -> EXTRA) -> Extra -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Extra -> EXTRA
extraToCST) [Extra]
extras
   in String -> String
braced (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate (String
" " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack (LOGIC_OPERATOR -> Text
forall a. Render a => a -> Text
render LOGIC_OPERATOR
AND) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" ") [String]
extras')

explainRules :: [Y.Rule] -> String
explainRules :: [Rule] -> String
explainRules = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> ([Rule] -> [String]) -> [Rule] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rule -> String) -> [Rule] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Rule -> String
explainRule (Rule -> String) -> (Rule -> Rule) -> Rule -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rule -> Rule
forall a. Metas a => a -> a
lonely)

explainMorphRules :: [Y.MorphRule] -> String
explainMorphRules :: [MorphRule] -> String
explainMorphRules = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String)
-> ([MorphRule] -> [String]) -> [MorphRule] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MorphRule -> String) -> [MorphRule] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (MorphRule -> String
explainMorphRule (MorphRule -> String)
-> (MorphRule -> MorphRule) -> MorphRule -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MorphRule -> MorphRule
forall a. Metas a => a -> a
lonely)

explainDataizeRules :: [Y.DataizeRule] -> String
explainDataizeRules :: [DataizeRule] -> String
explainDataizeRules = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String)
-> ([DataizeRule] -> [String]) -> [DataizeRule] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataizeRule -> String) -> [DataizeRule] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (DataizeRule -> String
explainDataizeRule (DataizeRule -> String)
-> (DataizeRule -> DataizeRule) -> DataizeRule -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataizeRule -> DataizeRule
forall a. Metas a => a -> a
lonely)

explainContextualizeRules :: [Y.ContextualizeRule] -> String
explainContextualizeRules :: [ContextualizeRule] -> String
explainContextualizeRules = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String)
-> ([ContextualizeRule] -> [String])
-> [ContextualizeRule]
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ContextualizeRule -> String) -> [ContextualizeRule] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ContextualizeRule -> String
explainContextualizeRule (ContextualizeRule -> String)
-> (ContextualizeRule -> ContextualizeRule)
-> ContextualizeRule
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextualizeRule -> ContextualizeRule
forall a. Metas a => a -> a
lonely)