phino 0.0.0.61 → 0.0.0.62
raw patch · 17 files changed
+222/−205 lines, 17 files
Files
- README.md +46/−57
- phino.cabal +1/−1
- resources/alpha.yaml +1/−1
- src/CST.hs +12/−10
- src/Condition.hs +2/−2
- src/Dataize.hs +1/−1
- src/Encoding.hs +6/−6
- src/LaTeX.hs +30/−15
- src/Lining.hs +5/−5
- src/Margin.hs +11/−11
- src/Render.hs +21/−13
- src/Rule.hs +2/−2
- src/Sugar.hs +7/−5
- src/Yaml.hs +3/−3
- test/CLISpec.hs +69/−69
- test/CSTSpec.hs +3/−2
- test/ConditionSpec.hs +2/−2
README.md view
@@ -29,7 +29,7 @@ ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.0.60+cabal install --overwrite-policy=always phino-0.0.0.61 phino --version ``` @@ -156,52 +156,24 @@ ```bash $ cat bytes.phi-{⟦- org ↦ ⟦- eolang ↦ ⟦- bytes ↦ ⟦- data ↦ ∅,- φ ↦ data- ⟧- ⟧- ⟧-⟧}+{⟦ bytes(data) ↦ ⟦ φ ↦ data ⟧ ⟧} $ cat number.phi {⟦- org ↦ ⟦- eolang ↦ ⟦- number ↦ ⟦- as-bytes ↦ ∅,- φ ↦ as-bytes,- plus(x) ↦ ⟦- λ ⤍ L_org_eolang_number_plus- ⟧- ⟧- ⟧+ number(as-bytes) ↦ ⟦+ φ ↦ as-bytes,+ plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧ ⟧}-$ cat foo.phi-{⟦- foo ↦ 5.plus(3)-⟧}-$ phino merge bytes.phi number.phi foo.phi --sweet+$ cat minus.phi+{⟦ number ↦ ⟦ minus(x) ↦ ⟦ λ ⤍ L_number_minus ⟧ ⟧ ⟧}+$ phino merge bytes.phi number.phi minus.phi --sweet {⟦- org ↦ ⟦- eolang ↦ ⟦- bytes ↦ ⟦- data ↦ ∅,- φ ↦ data- ⟧,- number ↦ ⟦- as-bytes ↦ ∅,- φ ↦ as-bytes,- plus(x) ↦ ⟦- λ ⤍ L_org_eolang_number_plus- ⟧- ⟧- ⟧- ⟧,- foo ↦ 5.plus(3)+ bytes(data) ↦ ⟦ φ ↦ data ⟧,+ number(as-bytes) ↦ ⟦+ φ ↦ as-bytes,+ plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧,+ minus(x) ↦ ⟦ λ ⤍ L_number_minus ⟧+ ⟧ ⟧} ``` @@ -216,18 +188,35 @@ d >> 68-65-6C-6C-6F ``` -## Explain (under development)+## Explain You can _explain_ rewriting rule by printing them in [LaTeX][latex] format: ```bash-$ phino explain --rule=my-rule.yaml-\documentclass{article}-\usepackage{amsmath}-\begin{document}-\rule{My custom rule}-\...-\end{document}+$ phino explain --normalize+\begin{tabular}{rl}+\trrule{ALPHA}+ { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_2 -> e ) }+ { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_1 -> e ) }+ { if $ \indexof{ \tau_2 } = |B_1| $ }+ { }+\trrule{COPY}+ { [[ B_1, \tau -> ?, B_2 ]] ( \tau -> e_1 ) }+ { [[ B_1, \tau -> e_3, B_2 ]] }+ { if $ \isnormal{ e_1 } $ }+ { where $ e_2 \coloneqq \scopeof{ e_1 } $ and $ e_3 \coloneqq \ctx{ e_1 }{ e_2 } $ }+\trrule{DC}+ { T ( \tau -> e ) }+ { T }+ { }+ { }+...+\trrule{STOP}+ { [[ B ]] . \tau }+ { T }+ { if $ \tau \notin B \;\text{and}\; @ \notin B \;\text{and}\; L \notin B $ }+ { }+\end{tabular} ``` For more details, use `phino [COMMAND] --help` option.@@ -278,7 +267,7 @@ Number: # comparable number = Integer # just regular integer- | ordinal: Attribute' # calculate index of alpha attribute+ | index: Attribute' # calculate index of alpha attribute | length: BiMeta' # calculate length of bindings by given meta binding Extension: # substitutions extension used to introduce new meta variables@@ -322,13 +311,13 @@ decimals accordingly. Uniqueness is guaranteed during one execution of `phino`. * `size` - accepts exactly one meta binding and returns size of it and- `Φ̇.number`.-* `tau` - accepts `Φ̇.string`, dataizes it and converts it to attribute.+ `Φ.number`.+* `tau` - accepts `Φ.string`, dataizes it and converts it to attribute. If dataized string can't be converted to attribute - an error is thrown.-* `string` - accepts `Φ̇.string` or `Φ̇.number` or attribute and converts it- to `Φ̇.string`.-* `number` - accepts `Φ̇.string` and converts it `Φ̇.number`-* `sum` - accepts list of `Φ̇.number` or `Φ̇.bytes` and returns sum of them as `Φ̇.number`+* `string` - accepts `Φ.string` or `Φ.number` or attribute and converts it+ to `Φ.string`.+* `number` - accepts `Φ.string` and converts it `Φ.number`+* `sum` - accepts list of `Φ.number` or `Φ.bytes` and returns sum of them as `Φ.number` * `join` - accepts list of bindings and returns list of joined bindings. Duplicated `ρ`, `Δ` and `λ` attributes are ignored, all other duplicated attributes are replaced with unique attributes using `random-tau` function.
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.0.61+version: 0.0.0.62 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
resources/alpha.yaml view
@@ -6,5 +6,5 @@ result: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒) when: eq:- - ordinal: 𝜏2+ - index: 𝜏2 - length: 𝐵1
src/CST.hs view
@@ -59,7 +59,7 @@ data TERMINATION = DEAD | T deriving (Eq, Show) -data SPACE = SPACE+data SPACE = SPACE | NO_SPACE deriving (Eq, Show) data EOL = EOL | NO_EOL@@ -105,7 +105,7 @@ deriving (Eq, Show) data PROGRAM- = PR_SWEET {lcb :: LCB, expr :: EXPRESSION, rcb :: RCB}+ = PR_SWEET {lcb :: LCB, expr :: EXPRESSION, rcb :: RCB, space :: SPACE} | PR_SALTY {global :: GLOBAL, arrow :: ARROW, expr :: EXPRESSION} deriving (Eq, Show) @@ -154,10 +154,10 @@ | EX_ATTR {attr :: ATTRIBUTE} -- sugar for $.x -> just x | EX_TERMINATION {termination :: TERMINATION} | EX_FORMATION {lsb :: LSB, eol :: EOL, tab :: TAB, binding :: BINDING, eol' :: EOL, tab' :: TAB, rsb :: RSB}- | EX_DISPATCH {expr :: EXPRESSION, attr :: ATTRIBUTE}- | EX_APPLICATION {expr :: EXPRESSION, eol :: EOL, tab :: TAB, tau :: APP_BINDING, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(a1 -> e1)- | EX_APPLICATION_TAUS {expr :: EXPRESSION, eol :: EOL, tab :: TAB, taus :: BINDING, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(a1 -> e1)(a2 -> e2)(...)- | EX_APPLICATION_EXPRS {expr :: EXPRESSION, eol :: EOL, tab :: TAB, args :: APP_ARG, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(e1, e2, ...)+ | EX_DISPATCH {expr :: EXPRESSION, space :: SPACE, attr :: ATTRIBUTE}+ | EX_APPLICATION {expr :: EXPRESSION, space :: SPACE, eol :: EOL, tab :: TAB, tau :: APP_BINDING, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(a1 -> e1)+ | EX_APPLICATION_TAUS {expr :: EXPRESSION, space :: SPACE, eol :: EOL, tab :: TAB, taus :: BINDING, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(a1 -> e1)(a2 -> e2)(...)+ | EX_APPLICATION_EXPRS {expr :: EXPRESSION, space :: SPACE, eol :: EOL, tab :: TAB, args :: APP_ARG, eol' :: EOL, tab' :: TAB, indent :: Int} -- e(e1, e2, ...) | EX_STRING {str :: String, tab :: TAB, rhos :: [Binding]} | EX_NUMBER {num :: Either Int Double, tab :: TAB, rhos :: [Binding]} | EX_META {meta :: META}@@ -198,7 +198,7 @@ deriving (Eq, Show) data NUMBER- = ORDINAL {attr :: ATTRIBUTE}+ = INDEX {attr :: ATTRIBUTE} | LENGTH {binding :: BINDING} | LITERAL {num :: Int} deriving (Eq, Show)@@ -267,7 +267,7 @@ toCST :: a -> (Int, EOL) -> b instance ToCST Program PROGRAM where- toCST (Program expr) ctx = PR_SWEET LCB (toCST expr ctx) RCB+ toCST (Program expr) ctx = PR_SWEET LCB (toCST expr ctx) RCB NO_SPACE instance ToCST Expression EXPRESSION where toCST ExGlobal _ = EX_GLOBAL Φ@@ -298,7 +298,7 @@ toCST (DataString bts) (tabs, _) = EX_STRING (btsToStr bts) (TAB tabs) [] toCST (DataNumber bts) (tabs, _) = EX_NUMBER (btsToNum bts) (TAB tabs) [] toCST (ExDispatch ExThis attr) ctx = EX_ATTR (toCST attr ctx)- toCST (ExDispatch expr attr) ctx = EX_DISPATCH (toCST expr ctx) (toCST attr ctx)+ toCST (ExDispatch expr attr) ctx = EX_DISPATCH (toCST expr ctx) NO_SPACE (toCST attr ctx) -- Since we convert AST to CST in sweet notation, here we're trying to get rid of unnecessary rho bindings -- in primitives (more details here: https://github.com/objectionary/phino/issues/451) -- If we find something similar to:@@ -322,6 +322,7 @@ then EX_APPLICATION_TAUS ex'+ NO_SPACE eol (TAB next) (toCST ts (next, eol) :: BINDING)@@ -331,6 +332,7 @@ else EX_APPLICATION_EXPRS ex'+ NO_SPACE eol (TAB next) (toCST exs (next, eol))@@ -482,7 +484,7 @@ toCST (Y.CmpNum num) _ = CMP_NUM (numberToCST num) instance ToCST Y.Number NUMBER where- toCST (Y.Ordinal attr) _ = ORDINAL (attributeToCST attr)+ toCST (Y.Index attr) _ = INDEX (attributeToCST attr) toCST (Y.Length binding) _ = LENGTH (bindingsToCST [binding]) toCST (Y.Literal num) _ = LITERAL num
src/Condition.hs view
@@ -49,10 +49,10 @@ number = choice [ do- _ <- symbol "ordinal" >> lparen+ _ <- symbol "index" >> lparen attr <- _attribute phiParser _ <- rparen- return (Y.Ordinal attr)+ return (Y.Index attr) , do _ <- symbol "length" >> lparen bd <- _binding phiParser
src/Dataize.hs view
@@ -154,7 +154,7 @@ then morph (ExTermination, seq) ctx -- PRIM else do prog' <- withLocatedExpression _locator expr _program- (rewrittens', _) <- rewrite prog' normalizationRules (switchContext ctx) -- NMZ todo+ (rewrittens', _) <- rewrite prog' normalizationRules (switchContext ctx) -- NMZ let seq' = reverse rewrittens' <> tail seq expr' <- locatedExpression _locator (fst (head seq')) morph (expr', seq') ctx
src/Encoding.hs view
@@ -19,7 +19,7 @@ instance ToASCII PROGRAM where toASCII PR_SALTY{..} = PR_SALTY Q ARROW' (toASCII expr)- toASCII PR_SWEET{..} = PR_SWEET lcb (toASCII expr) rcb+ toASCII PR_SWEET{..} = PR_SWEET lcb (toASCII expr) rcb space instance ToASCII EXPRESSION where toASCII EX_GLOBAL{} = EX_GLOBAL Q@@ -27,10 +27,10 @@ toASCII EX_ATTR{..} = EX_ATTR (toASCII attr) toASCII EX_TERMINATION{} = EX_TERMINATION T toASCII EX_FORMATION{..} = EX_FORMATION LSB' eol tab (toASCII binding) eol' tab' RSB'- toASCII EX_DISPATCH{..} = EX_DISPATCH (toASCII expr) (toASCII attr)- toASCII EX_APPLICATION{..} = EX_APPLICATION (toASCII expr) eol tab (toASCII tau) eol' tab' indent- toASCII EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toASCII expr) eol tab (toASCII taus) eol' tab' indent- toASCII EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toASCII expr) eol tab (toASCII args) eol' tab' indent+ toASCII EX_DISPATCH{..} = EX_DISPATCH (toASCII expr) space (toASCII attr)+ toASCII EX_APPLICATION{..} = EX_APPLICATION (toASCII expr) space eol tab (toASCII tau) eol' tab' indent+ toASCII EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toASCII expr) space eol tab (toASCII taus) eol' tab' indent+ toASCII EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toASCII expr) space eol tab (toASCII args) eol' tab' indent toASCII EX_META{..} = EX_META (META EXCL E' (rest meta)) toASCII EX_META_TAIL{..} = EX_META_TAIL (toASCII expr) meta toASCII EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toASCII expr)@@ -79,7 +79,7 @@ toASCII ST_ATTRIBUTES{..} = ST_ATTRIBUTES (map toASCII attrs) instance ToASCII NUMBER where- toASCII ORDINAL{..} = ORDINAL (toASCII attr)+ toASCII INDEX{..} = INDEX (toASCII attr) toASCII LENGTH{..} = LENGTH (toASCII binding) toASCII literal@LITERAL{} = literal
src/LaTeX.hs view
@@ -22,7 +22,7 @@ import AST import CST import Data.List (intercalate, nub)-import Data.Maybe (fromMaybe)+import Data.Maybe (fromMaybe, isJust) import Encoding import Lining import Locator (locatedExpression)@@ -34,6 +34,7 @@ import Rewriter (Rewritten, Rewrittens) import Sugar (SugarType (SWEET), ToSalty, withSugarType) import Text.Printf (printf)+import Text.Read (readMaybe) import qualified Yaml as Y data LatexContext = LatexContext@@ -201,24 +202,24 @@ toLaTeX :: a -> a instance ToLaTeX PROGRAM where- toLaTeX PR_SWEET{..} = PR_SWEET BIG_LCB (toLaTeX expr) BIG_RCB+ toLaTeX PR_SWEET{..} = PR_SWEET BIG_LCB (toLaTeX expr) BIG_RCB SPACE toLaTeX PR_SALTY{..} = PR_SALTY global arrow (toLaTeX expr) instance ToLaTeX EXPRESSION where toLaTeX EX_ATTR{..} = EX_ATTR (toLaTeX attr) toLaTeX EX_FORMATION{..} = EX_FORMATION lsb eol tab (toLaTeX binding) eol' tab' rsb- toLaTeX EX_APPLICATION{..} = EX_APPLICATION (toLaTeX expr) eol tab (toLaTeX tau) eol' tab' indent- toLaTeX EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toLaTeX expr) eol tab (toLaTeX taus) eol' tab' indent- toLaTeX EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toLaTeX expr) eol tab (toLaTeX args) eol' tab' indent- toLaTeX EX_DISPATCH{..} = EX_DISPATCH (toLaTeX expr) (toLaTeX attr)+ toLaTeX EX_APPLICATION{..} = EX_APPLICATION (toLaTeX expr) SPACE eol tab (toLaTeX tau) eol' tab' indent+ toLaTeX EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toLaTeX expr) SPACE eol tab (toLaTeX taus) eol' tab' indent+ toLaTeX EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toLaTeX expr) SPACE eol tab (toLaTeX args) eol' tab' indent+ toLaTeX EX_DISPATCH{..} = EX_DISPATCH (toLaTeX expr) SPACE (toLaTeX attr) toLaTeX EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toLaTeX expr) toLaTeX EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toLaTeX expr)- toLaTeX EX_META{..} = EX_META (META NO_EXCL E' (rest meta))+ toLaTeX EX_META{..} = EX_META (toLaTeX meta) toLaTeX expr = expr instance ToLaTeX ATTRIBUTE where toLaTeX AT_LABEL{..} = AT_LABEL (piped (toLaTeX label))- toLaTeX AT_META{..} = AT_META (META NO_EXCL TAU' (rest meta))+ toLaTeX AT_META{..} = AT_META (toLaTeX meta) toLaTeX AT_LAMBDA{} = AT_LAMBDA LAMBDA' toLaTeX AT_REST{} = AT_REST DOTS' toLaTeX attr = attr@@ -228,12 +229,12 @@ instance ToLaTeX BINDING where toLaTeX BI_PAIR{..} = BI_PAIR (toLaTeX pair) (toLaTeX bindings) tab- toLaTeX BI_META{..} = BI_META (META NO_EXCL B' (rest meta)) (toLaTeX bindings) tab+ toLaTeX BI_META{..} = BI_META (toLaTeX meta) (toLaTeX bindings) tab toLaTeX bd = bd instance ToLaTeX BINDINGS where toLaTeX BDS_PAIR{..} = BDS_PAIR eol tab (toLaTeX pair) (toLaTeX bindings)- toLaTeX BDS_META{..} = BDS_META eol tab (META NO_EXCL B' (rest meta)) (toLaTeX bindings)+ toLaTeX BDS_META{..} = BDS_META eol tab (toLaTeX meta) (toLaTeX bindings) toLaTeX bds = bds instance ToLaTeX PAIR where@@ -244,11 +245,25 @@ toLaTeX PA_TAU{..} = PA_TAU (toLaTeX attr) arrow (toLaTeX expr) toLaTeX PA_FORMATION{..} = PA_FORMATION (toLaTeX attr) (map toLaTeX voids) arrow (toLaTeX expr) toLaTeX PA_META_DELTA{..} = toLaTeX (PA_META_DELTA' meta)- toLaTeX PA_META_DELTA'{..} = PA_META_DELTA' (META NO_EXCL D' (rest meta))+ toLaTeX PA_META_DELTA'{..} = PA_META_DELTA' (toLaTeX meta) toLaTeX PA_META_LAMBDA{..} = toLaTeX (PA_META_LAMBDA' meta)- toLaTeX PA_META_LAMBDA'{..} = PA_META_LAMBDA' (META NO_EXCL F (rest meta))+ toLaTeX PA_META_LAMBDA'{..} = PA_META_LAMBDA' (toLaTeX meta) toLaTeX pair = pair +instance ToLaTeX META where+ toLaTeX META{..} =+ let idx = readMaybe rest :: Maybe Int+ rest' = if not (null rest) && length rest <= 2 && isJust idx then '_' : rest else rest+ in META NO_EXCL (toLaTeX hd) rest'++instance ToLaTeX META_HEAD where+ toLaTeX E = E'+ toLaTeX A = TAU'+ toLaTeX TAU = TAU'+ toLaTeX B = B'+ toLaTeX D = D'+ toLaTeX mh = mh+ instance ToLaTeX APP_ARG where toLaTeX APP_ARG{..} = APP_ARG (toLaTeX expr) (toLaTeX args) @@ -273,7 +288,7 @@ toLaTeX ST_ATTRIBUTES{..} = ST_ATTRIBUTES (map toLaTeX attrs) instance ToLaTeX NUMBER where- toLaTeX ORDINAL{..} = ORDINAL (toLaTeX attr)+ toLaTeX INDEX{..} = INDEX (toLaTeX attr) toLaTeX LENGTH{..} = LENGTH (toLaTeX binding) toLaTeX literal@LITERAL{} = literal @@ -316,12 +331,12 @@ conditionToLatex Nothing = "{ }" conditionToLatex (Just cond) = case conditionToCST cond of CO_EMPTY -> "{ }"- cond' -> braced ("if " <> renderToLatex cond' defaultLatexContext)+ cond' -> braced ("if $ " <> renderToLatex cond' defaultLatexContext <> " $") extraArgumentsToLatex :: Maybe [Y.Extra] -> String extraArgumentsToLatex Nothing = "{ }" extraArgumentsToLatex (Just extras) = let extras' = map ((`renderToLatex` defaultLatexContext) . extraToCST) extras- in braced ("where " <> intercalate "; " extras')+ in braced ("where " <> intercalate " and " extras') braced :: String -> String braced = printf "{ %s }" -- Join two maybe conditions into single one using Y.And if at least one is just.
src/Lining.hs view
@@ -20,15 +20,15 @@ instance ToSingleLine PROGRAM where toSingleLine PR_SALTY{..} = PR_SALTY global arrow (toSingleLine expr)- toSingleLine PR_SWEET{..} = PR_SWEET lcb (toSingleLine expr) rcb+ toSingleLine PR_SWEET{..} = PR_SWEET lcb (toSingleLine expr) rcb space instance ToSingleLine EXPRESSION where toSingleLine EX_FORMATION{lsb, binding = bd@BI_EMPTY{}, rsb} = EX_FORMATION lsb NO_EOL NO_TAB bd NO_EOL NO_TAB rsb toSingleLine EX_FORMATION{..} = EX_FORMATION lsb NO_EOL TAB' (toSingleLine binding) NO_EOL TAB' rsb- toSingleLine EX_DISPATCH{..} = EX_DISPATCH (toSingleLine expr) attr- toSingleLine EX_APPLICATION{..} = EX_APPLICATION (toSingleLine expr) NO_EOL TAB' (toSingleLine tau) NO_EOL TAB' indent- toSingleLine EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toSingleLine expr) NO_EOL TAB' (toSingleLine taus) NO_EOL TAB' indent- toSingleLine EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toSingleLine expr) NO_EOL TAB' (toSingleLine args) NO_EOL TAB' indent+ toSingleLine EX_DISPATCH{..} = EX_DISPATCH (toSingleLine expr) space attr+ toSingleLine EX_APPLICATION{..} = EX_APPLICATION (toSingleLine expr) space NO_EOL TAB' (toSingleLine tau) NO_EOL TAB' indent+ toSingleLine EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toSingleLine expr) space NO_EOL TAB' (toSingleLine taus) NO_EOL TAB' indent+ toSingleLine EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toSingleLine expr) space NO_EOL TAB' (toSingleLine args) NO_EOL TAB' indent toSingleLine EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toSingleLine expr) toSingleLine EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toSingleLine expr) toSingleLine expr = expr
src/Margin.hs view
@@ -21,7 +21,7 @@ withMargin' :: (Int, Int) -> a -> a instance WithMargin PROGRAM where- withMargin' (_, margin) PR_SWEET{..} = PR_SWEET lcb (withMargin' (2, margin) expr) rcb+ withMargin' (_, margin) PR_SWEET{..} = PR_SWEET lcb (withMargin' (2, margin) expr) rcb space withMargin' (_, margin) PR_SALTY{..} = let before = lengthOf global + lengthOf arrow + 2 -- 'Q -> ' in PR_SALTY global arrow (withMargin' (before, margin) expr)@@ -34,7 +34,7 @@ in if lengthOf single + extra <= margin then single else ex' withMargin' _ num@EX_NUMBER{} = num withMargin' _ str@EX_STRING{} = str- withMargin' cfg EX_DISPATCH{..} = EX_DISPATCH (withMargin' cfg expr) attr+ withMargin' cfg EX_DISPATCH{..} = EX_DISPATCH (withMargin' cfg expr) space attr withMargin' cfg EX_META_TAIL{..} = EX_META_TAIL (withMargin' cfg expr) meta withMargin' cfg EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (withMargin' cfg expr) withMargin' cfg EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (withMargin' cfg expr)@@ -47,9 +47,9 @@ singleArg = toSingleLine arg in if | lengthOf single + extra <= margin -> single- | lengthOf singleMain + extra <= margin -> EX_APPLICATION singleMain EOL tab arg EOL tab' indent- | lengthOf singleArg + extra' <= margin -> EX_APPLICATION main NO_EOL TAB' singleArg NO_EOL TAB' indent- | otherwise -> EX_APPLICATION main EOL tab arg EOL tab' indent+ | lengthOf singleMain + extra <= margin -> EX_APPLICATION singleMain space EOL tab arg EOL tab' indent+ | lengthOf singleArg + extra' <= margin -> EX_APPLICATION main space NO_EOL TAB' singleArg NO_EOL TAB' indent+ | otherwise -> EX_APPLICATION main space EOL tab arg EOL tab' indent withMargin' cfg@(extra, margin) ex@EX_APPLICATION_EXPRS{tab = tab@(TAB indt), ..} = let single = toSingleLine ex main = withMargin' cfg expr@@ -59,9 +59,9 @@ singleExprs = toSingleLine exprs in if | lengthOf single + extra <= margin -> single- | lengthOf singleMain + extra <= margin -> EX_APPLICATION_EXPRS singleMain EOL tab exprs EOL tab' indent- | lengthOf singleExprs + extra' <= margin -> EX_APPLICATION_EXPRS main NO_EOL TAB' singleExprs NO_EOL TAB' indent- | otherwise -> EX_APPLICATION_EXPRS main EOL tab exprs EOL tab' indent+ | lengthOf singleMain + extra <= margin -> EX_APPLICATION_EXPRS singleMain space EOL tab exprs EOL tab' indent+ | lengthOf singleExprs + extra' <= margin -> EX_APPLICATION_EXPRS main space NO_EOL TAB' singleExprs NO_EOL TAB' indent+ | otherwise -> EX_APPLICATION_EXPRS main space EOL tab exprs EOL tab' indent withMargin' cfg@(extra, margin) ex@EX_APPLICATION_TAUS{tab = tab@(TAB indt), ..} = let single = toSingleLine ex main = withMargin' cfg expr@@ -71,9 +71,9 @@ singleTaus = toSingleLine taus' in if | lengthOf single + extra <= margin -> single- | lengthOf singleMain + extra <= margin -> EX_APPLICATION_TAUS singleMain EOL tab taus' EOL tab' indent- | lengthOf singleTaus + extra' <= margin -> EX_APPLICATION_TAUS main NO_EOL TAB' singleTaus NO_EOL TAB' indent- | otherwise -> EX_APPLICATION_TAUS main EOL tab taus' EOL tab' indent+ | lengthOf singleMain + extra <= margin -> EX_APPLICATION_TAUS singleMain space EOL tab taus' EOL tab' indent+ | lengthOf singleTaus + extra' <= margin -> EX_APPLICATION_TAUS main space NO_EOL TAB' singleTaus NO_EOL TAB' indent+ | otherwise -> EX_APPLICATION_TAUS main space EOL tab taus' EOL tab' indent withMargin' _ ex = ex instance WithMargin APP_BINDING where
src/Render.hs view
@@ -77,7 +77,7 @@ instance Render LAMBDA where render LAMBDA = "λ"- render LAMBDA' = "\\lambda"+ render LAMBDA' = "L" instance Render GLOBAL where render Φ = "Φ"@@ -89,6 +89,7 @@ instance Render SPACE where render SPACE = " "+ render NO_SPACE = "" instance Render EOL where render EOL = "\n"@@ -134,7 +135,7 @@ render NO_TAB = "" instance Render PROGRAM where- render PR_SWEET{..} = render lcb <> render expr <> render rcb+ render PR_SWEET{..} = render lcb <> render space <> render expr <> render space <> render rcb render PR_SALTY{..} = render global <> render SPACE <> render arrow <> render SPACE <> render expr instance Render PAIR where@@ -177,10 +178,10 @@ render EX_ATTR{..} = render attr render EX_TERMINATION{..} = render termination render EX_FORMATION{..} = render lsb <> render eol <> render tab <> render binding <> render eol' <> render tab' <> render rsb- render EX_DISPATCH{..} = render expr <> "." <> render attr- render EX_APPLICATION{..} = render expr <> "(" <> render eol <> render tab <> render tau <> render eol' <> render tab' <> ")"- render EX_APPLICATION_TAUS{..} = render expr <> "(" <> render eol <> render tab <> render taus <> render eol' <> render tab' <> ")"- render EX_APPLICATION_EXPRS{..} = render expr <> "(" <> render eol <> render tab <> render args <> render eol' <> render tab' <> ")"+ render EX_DISPATCH{..} = render expr <> render space <> "." <> render space <> render attr+ render EX_APPLICATION{..} = render expr <> render space <> "(" <> render eol <> render tab <> render tau <> render eol' <> render tab' <> ")"+ render EX_APPLICATION_TAUS{..} = render expr <> render space <> "(" <> render eol <> render tab <> render taus <> render eol' <> render tab' <> ")"+ render EX_APPLICATION_EXPRS{..} = render expr <> render space <> "(" <> render eol <> render tab <> render args <> render eol' <> render tab' <> ")" render EX_STRING{..} = '"' : render str <> "\"" render EX_NUMBER{..} = either show show num render EX_META{..} = render meta@@ -210,12 +211,12 @@ render ST_ATTRIBUTES{..} = printf "[ %s ]" (intercalate ", " (map render attrs)) instance Render LOGIC_OPERATOR where- render AND = "and"- render OR = "or"+ render AND = "\\;\\text{and}\\;"+ render OR = "\\;\\text{or}\\;" instance Render NUMBER where- render ORDINAL{..} = renderFunc "ordinal" attr- render LENGTH{..} = renderFunc "length" binding+ render INDEX{..} = printf "\\indexof{ %s }" (render attr)+ render LENGTH{..} = printf "|%s|" (render binding) render LITERAL{..} = show num instance Render COMPARABLE where@@ -230,8 +231,13 @@ instance Render CONDITION where render CO_BELONGS{..} = render attr <> render SPACE <> render belongs <> render SPACE <> render set render CO_LOGIC{conditions = [cond]} = render cond- render CO_LOGIC{..} = printf "\\( %s \\)" (intercalate (printf " \\) %s \\( " (render operator)) (map render conditions))- render CO_NF{..} = renderFunc "NF" expr+ render CO_LOGIC{..} = intercalate (printf " %s " (render operator)) (map renderWrapped conditions)+ where+ renderWrapped :: CONDITION -> String+ renderWrapped CO_LOGIC{conditions = [cond]} = render cond+ renderWrapped cond@CO_LOGIC{} = printf "( %s )" (render cond)+ renderWrapped cond = render cond+ render CO_NF{..} = printf "\\isnormal{ %s }" (render expr) render CO_NOT{..} = renderFunc "not" condition render CO_COMPARE{..} = render left <> render SPACE <> render equal <> render SPACE <> render right render CO_MATCHES{..} = printf "matches( %s, %s )" regex (render expr)@@ -248,4 +254,6 @@ render ARG_BYTES{..} = render bytes instance Render EXTRA where- render EXTRA{..} = render meta <> " <- " <> printf "%s( %s )" func (intercalate ", " (map render args))+ render EXTRA{func = "contextualize", ..} = printf "$ %s \\coloneqq \\ctx{ %s }{ %s } $" (render meta) (render (head args)) (intercalate ", " (map render (tail args)))+ render EXTRA{func = "scope", ..} = printf "$ %s \\coloneqq \\scopeof{ %s } $" (render meta) (render (head args))+ render EXTRA{..} = printf "$ %s \\coloneqq %s( %s ) $" (render meta) func (intercalate ", " (map render args))
src/Rule.hs view
@@ -122,10 +122,10 @@ where -- Convert Number to Int numToInt :: Y.Number -> Subst -> Maybe Int- numToInt (Y.Ordinal (AtMeta meta)) (Subst mp) = case M.lookup meta mp of+ numToInt (Y.Index (AtMeta meta)) (Subst mp) = case M.lookup meta mp of Just (MvAttribute (AtAlpha idx)) -> Just idx _ -> Nothing- numToInt (Y.Ordinal (AtAlpha idx)) _ = Just idx+ numToInt (Y.Index (AtAlpha idx)) _ = Just idx numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of Just (MvBindings bds) -> Just (length bds) _ -> Nothing
src/Sugar.hs view
@@ -59,11 +59,11 @@ toSalty prog = prog instance ToSalty EXPRESSION where- toSalty EX_ATTR{..} = EX_DISPATCH (EX_XI XI) attr- toSalty EX_DISPATCH{..} = EX_DISPATCH (toSalty expr) attr+ toSalty EX_ATTR{..} = EX_DISPATCH (EX_XI XI) NO_SPACE attr+ toSalty EX_DISPATCH{..} = EX_DISPATCH (toSalty expr) space attr toSalty EX_FORMATION{lsb, binding = bd@BI_EMPTY{}, rsb} = EX_FORMATION lsb NO_EOL TAB' (toSalty (bdWithVoidRho bd)) NO_EOL TAB' rsb toSalty EX_FORMATION{..} = EX_FORMATION lsb eol tab (toSalty (bdWithVoidRho binding)) eol' tab' rsb- toSalty EX_APPLICATION{..} = EX_APPLICATION (toSalty expr) EOL (TAB indent) (toSalty tau) EOL (TAB (indent - 1)) indent+ toSalty EX_APPLICATION{..} = EX_APPLICATION (toSalty expr) space EOL (TAB indent) (toSalty tau) EOL (TAB (indent - 1)) indent toSalty EX_APPLICATION_TAUS{..} = foldl toApplication@@ -72,7 +72,7 @@ where toApplication :: EXPRESSION -> PAIR -> EXPRESSION toApplication exp pair =- EX_APPLICATION (toSalty exp) EOL (TAB indent) (APP_BINDING (toSalty pair)) EOL (TAB (indent - 1)) indent+ EX_APPLICATION (toSalty exp) space EOL (TAB indent) (APP_BINDING (toSalty pair)) EOL (TAB (indent - 1)) indent tauToPairs :: BINDING -> [PAIR] tauToPairs BI_PAIR{..} = pair : tausToPairs bindings tauToPairs BI_EMPTY{} = []@@ -81,7 +81,7 @@ tausToPairs BDS_EMPTY{} = [] tausToPairs BDS_PAIR{..} = pair : tausToPairs bindings tausToPairs (BDS_META _ _ mt _) = error $ "BDS_META " ++ show mt ++ " unexpected in tausToPairs"- toSalty EX_APPLICATION_EXPRS{..} = toSalty (EX_APPLICATION_TAUS expr EOL (TAB indent) (argToBinding args tab) EOL (TAB (indent - 1)) indent)+ toSalty EX_APPLICATION_EXPRS{..} = toSalty (EX_APPLICATION_TAUS expr space EOL (TAB indent) (argToBinding args tab) EOL (TAB (indent - 1)) indent) where argToBinding :: APP_ARG -> TAB -> BINDING argToBinding APP_ARG{..} =@@ -115,6 +115,7 @@ in toSalty ( EX_APPLICATION_TAUS base+ NO_SPACE EOL next ( BI_PAIR@@ -123,6 +124,7 @@ ARROW ( EX_APPLICATION_EXPRS bytes+ NO_SPACE EOL (TAB (indent + 2)) (APP_ARG data' AAS_EMPTY)
src/Yaml.hs view
@@ -54,9 +54,9 @@ instance FromJSON Number where parseJSON v = case v of Object o -> do- validateYamlObject o ["ordinal", "length"]+ validateYamlObject o ["index", "length"] asum- [ Ordinal <$> o .: "ordinal"+ [ Index <$> o .: "index" , Length <$> o .: "length" ] Number num -> pure (Literal (round num))@@ -132,7 +132,7 @@ } data Number- = Ordinal Attribute+ = Index Attribute | Length Binding | Literal Int deriving (Eq, Generic, Show)
test/CLISpec.hs view
@@ -359,15 +359,15 @@ ["rewrite", "--output=latex", "--sweet"] [ unlines [ "\\begin{phiquation}"- , "\\Big\\{[["- , " |x\\char95{}o| -> Q.|z|( |y| -> 5 ),"+ , "\\Big\\{ [["+ , " |x\\char95{}o| -> Q . |z| ( |y| -> 5 )," , " |q\\char36{}| -> T," , " |w| -> $," , " ^ -> Q," , " @ -> 1," , " |y| -> \"H$@^M\"," , " L> |Fu\\char95{}nc|"- , "]]\\Big\\}{.}"+ , "]] \\Big\\}{.}" , "\\end{phiquation}" ] ]@@ -378,7 +378,7 @@ ["rewrite", "--output=latex", "--sweet", "--nonumber", "--flat"] [ unlines [ "\\begin{phiquation*}"- , "\\Big\\{[[ |x| -> 5 ]]\\Big\\}{.}"+ , "\\Big\\{ [[ |x| -> 5 ]] \\Big\\}{.}" , "\\end{phiquation*}" ] ]@@ -389,7 +389,7 @@ ["rewrite", "--output=latex", "--sweet", "--flat", "--expression=foo"] [ unlines [ "\\begin{phiquation}"- , "\\phiExpression{foo} \\Big\\{[[ |x| -> 5 ]]\\Big\\}{.}"+ , "\\phiExpression{foo} \\Big\\{ [[ |x| -> 5 ]] \\Big\\}{.}" , "\\end{phiquation}" ] ]@@ -400,7 +400,7 @@ ["rewrite", "--output=latex", "--sweet", "--flat", "--label=foo"] [ unlines [ "\\begin{phiquation}\n\\label{foo}"- , "\\Big\\{[[ |x| -> 5 ]]\\Big\\}{.}"+ , "\\Big\\{ [[ |x| -> 5 ]] \\Big\\}{.}" , "\\end{phiquation}" ] ]@@ -457,9 +457,9 @@ ] [ unlines [ "\\begin{phiquation}"- , "\\Big\\{[[ |x| -> \"foo\" ]]\\Big\\} \\leadsto_{\\nameref{r:first}}"- , " \\leadsto \\Big\\{Q.|x|( |y| -> \"foo\" )\\Big\\} \\leadsto_{\\nameref{r:second}}"- , " \\leadsto \\Big\\{[[ |x| -> \"foo\" ]]\\Big\\}{.}"+ , "\\Big\\{ [[ |x| -> \"foo\" ]] \\Big\\} \\leadsto_{\\nameref{r:first}}"+ , " \\leadsto \\Big\\{ Q . |x| ( |y| -> \"foo\" ) \\Big\\} \\leadsto_{\\nameref{r:second}}"+ , " \\leadsto \\Big\\{ [[ |x| -> \"foo\" ]] \\Big\\}{.}" , "\\end{phiquation}" ] ]@@ -470,12 +470,12 @@ ["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress", "--meet-prefix=foo"] [ unlines [ "\\begin{phiquation}"- , "\\Big\\{[[ |x| -> ?, |y| -> |x| ]]( |x| -> \\phiMeet{foo:1}{ [[ D> 42- ]] } ).|y|\\Big\\} \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto \\Big\\{\\phiMeet{foo:2}{ [[ |x| -> \\phiAgain{foo:1}, |y| -> |x| ]] }.|y|\\Big\\} \\leadsto_{\\nameref{r:dot}}"- , " \\leadsto \\Big\\{\\phiAgain{foo:2}.|x|( ^ -> \\phiAgain{foo:2} )\\Big\\} \\leadsto_{\\nameref{r:dot}}"- , " \\leadsto \\Big\\{\\phiAgain{foo:1}( ^ -> \\phiAgain{foo:2}, ^ -> \\phiAgain{foo:2} )\\Big\\} \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{foo:2} ]]( ^ -> \\phiAgain{foo:2} )\\Big\\} \\leadsto_{\\nameref{r:stay}}"- , " \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{foo:2} ]]\\Big\\}{.}"+ , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phiMeet{foo:1}{ [[ D> 42- ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}"+ , " \\leadsto \\Big\\{ \\phiMeet{foo:2}{ [[ |x| -> \\phiAgain{foo:1}, |y| -> |x| ]] } . |y| \\Big\\} \\leadsto_{\\nameref{r:dot}}"+ , " \\leadsto \\Big\\{ \\phiAgain{foo:2} . |x| ( ^ -> \\phiAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}"+ , " \\leadsto \\Big\\{ \\phiAgain{foo:1} ( ^ -> \\phiAgain{foo:2}, ^ -> \\phiAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"+ , " \\leadsto \\Big\\{ [[ D> 42-, ^ -> \\phiAgain{foo:2} ]] ( ^ -> \\phiAgain{foo:2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"+ , " \\leadsto \\Big\\{ [[ D> 42-, ^ -> \\phiAgain{foo:2} ]] \\Big\\}{.}" , "\\end{phiquation}" ] ]@@ -486,12 +486,12 @@ ["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress"] [ unlines [ "\\begin{phiquation}"- , "\\Big\\{[[ |x| -> ?, |y| -> |x| ]]( |x| -> \\phiMeet{1}{ [[ D> 42- ]] } ).|y|\\Big\\} \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto \\Big\\{\\phiMeet{2}{ [[ |x| -> \\phiAgain{1}, |y| -> |x| ]] }.|y|\\Big\\} \\leadsto_{\\nameref{r:dot}}"- , " \\leadsto \\Big\\{\\phiAgain{2}.|x|( ^ -> \\phiAgain{2} )\\Big\\} \\leadsto_{\\nameref{r:dot}}"- , " \\leadsto \\Big\\{\\phiAgain{1}( ^ -> \\phiAgain{2}, ^ -> \\phiAgain{2} )\\Big\\} \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{2} ]]( ^ -> \\phiAgain{2} )\\Big\\} \\leadsto_{\\nameref{r:stay}}"- , " \\leadsto \\Big\\{[[ D> 42-, ^ -> \\phiAgain{2} ]]\\Big\\}{.}"+ , "\\Big\\{ [[ |x| -> ?, |y| -> |x| ]] ( |x| -> \\phiMeet{1}{ [[ D> 42- ]] } ) . |y| \\Big\\} \\leadsto_{\\nameref{r:copy}}"+ , " \\leadsto \\Big\\{ \\phiMeet{2}{ [[ |x| -> \\phiAgain{1}, |y| -> |x| ]] } . |y| \\Big\\} \\leadsto_{\\nameref{r:dot}}"+ , " \\leadsto \\Big\\{ \\phiAgain{2} . |x| ( ^ -> \\phiAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:dot}}"+ , " \\leadsto \\Big\\{ \\phiAgain{1} ( ^ -> \\phiAgain{2}, ^ -> \\phiAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"+ , " \\leadsto \\Big\\{ [[ D> 42-, ^ -> \\phiAgain{2} ]] ( ^ -> \\phiAgain{2} ) \\Big\\} \\leadsto_{\\nameref{r:stay}}"+ , " \\leadsto \\Big\\{ [[ D> 42-, ^ -> \\phiAgain{2} ]] \\Big\\}{.}" , "\\end{phiquation}" ] ]@@ -502,9 +502,9 @@ ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet"] [ unlines [ "\\begin{phiquation}"- , "\\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> \\phiMeet{1}{ [[ |t| -> 42 ]] } ]]( |y| -> \\phiAgain{1} ) ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto \\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> \\phiAgain{1}, |k| -> \\phiAgain{1} ]] ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:stop}}"- , " \\leadsto \\Big\\{[[ |ex| -> T ]]\\Big\\}{.}"+ , "\\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> \\phiMeet{1}{ [[ |t| -> 42 ]] } ]] ( |y| -> \\phiAgain{1} ) ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:copy}}"+ , " \\leadsto \\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> \\phiAgain{1}, |k| -> \\phiAgain{1} ]] ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:stop}}"+ , " \\leadsto \\Big\\{ [[ |ex| -> T ]] \\Big\\}{.}" , "\\end{phiquation}" ] ]@@ -515,9 +515,9 @@ ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet", "--meet-popularity=70"] [ unlines [ "\\begin{phiquation}"- , "\\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]]( |y| -> [[ |t| -> 42 ]] ) ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto \\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:stop}}"- , " \\leadsto \\Big\\{[[ |ex| -> T ]]\\Big\\}{.}"+ , "\\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:copy}}"+ , " \\leadsto \\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:stop}}"+ , " \\leadsto \\Big\\{ [[ |ex| -> T ]] \\Big\\}{.}" , "\\end{phiquation}" ] ]@@ -528,9 +528,9 @@ ["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet", "--meet-length=32"] [ unlines [ "\\begin{phiquation}"- , "\\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]]( |y| -> [[ |t| -> 42 ]] ) ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto \\Big\\{[[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]].|i| ]]\\Big\\} \\leadsto_{\\nameref{r:stop}}"- , " \\leadsto \\Big\\{[[ |ex| -> T ]]\\Big\\}{.}"+ , "\\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:copy}}"+ , " \\leadsto \\Big\\{ [[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| ]] \\Big\\} \\leadsto_{\\nameref{r:stop}}"+ , " \\leadsto \\Big\\{ [[ |ex| -> T ]] \\Big\\}{.}" , "\\end{phiquation}" ] ]@@ -541,8 +541,8 @@ ["rewrite", "--normalize", "--sequence", "--flat", "--output=latex", "--sweet", "--focus=Q.ex"] [ unlines [ "\\begin{phiquation}"- , "[[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]]( |y| -> [[ |t| -> 42 ]] ) ]].|i| \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]].|i| \\leadsto_{\\nameref{r:stop}}"+ , "[[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| \\leadsto_{\\nameref{r:copy}}"+ , " \\leadsto [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| \\leadsto_{\\nameref{r:stop}}" , " \\leadsto T{.}" , "\\end{phiquation}" ]@@ -565,8 +565,8 @@ ["rewrite", "--normalize", "--flat", "--sequence", "--output=latex", "--sweet", "--max-depth=1", "--max-cycles=1"] [ unlines [ "\\begin{phiquation}"- , "\\Big\\{[[ |x| -> |y|, |y| -> |x| ]].|x|\\Big\\} \\leadsto_{\\nameref{r:dot}}"- , " \\leadsto \\Big\\{[[ |x| -> |y|, |y| -> |x| ]].|y|( ^ -> [[ |x| -> |y|, |y| -> |x| ]] )\\Big\\} \\leadsto"+ , "\\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}"+ , " \\leadsto \\Big\\{ [[ |x| -> |y|, |y| -> |x| ]] . |y| ( ^ -> [[ |x| -> |y|, |y| -> |x| ]] ) \\Big\\} \\leadsto" , " \\leadsto \\dots" , "\\end{phiquation}" ]@@ -759,12 +759,12 @@ [ intercalate "\n" [ "\\begin{phiquation}"- , "\\Big\\{[[ @ -> [[ |x| -> [[ D> 01-, |y| -> ? ]]( |y| -> [[]] ) ]].|x| ]]\\Big\\} \\leadsto_{\\nameref{r:contextualize}}"- , " \\leadsto \\Big\\{[[ |x| -> [[ D> 01-, |y| -> ? ]]( |y| -> [[]] ) ]].|x|\\Big\\} \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto \\Big\\{[[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]].|x|\\Big\\} \\leadsto_{\\nameref{r:dot}}"- , " \\leadsto \\Big\\{[[ D> 01-, |y| -> [[]] ]]( ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] )\\Big\\} \\leadsto_{\\nameref{r:copy}}"- , " \\leadsto \\Big\\{[[ D> 01-, |y| -> [[]], ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]]\\Big\\} \\leadsto_{\\nameref{r:Mprim}}"- , " \\leadsto \\Big\\{[[ D> 01-, |y| -> [[]], ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]]\\Big\\}{.}"+ , "\\Big\\{ [[ @ -> [[ |x| -> [[ D> 01-, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| ]] \\Big\\} \\leadsto_{\\nameref{r:contextualize}}"+ , " \\leadsto \\Big\\{ [[ |x| -> [[ D> 01-, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:copy}}"+ , " \\leadsto \\Big\\{ [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] . |x| \\Big\\} \\leadsto_{\\nameref{r:dot}}"+ , " \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]] ]] ( ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ) \\Big\\} \\leadsto_{\\nameref{r:copy}}"+ , " \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\} \\leadsto_{\\nameref{r:Mprim}}"+ , " \\leadsto \\Big\\{ [[ D> 01-, |y| -> [[]], ^ -> [[ |x| -> [[ D> 01-, |y| -> [[]] ]] ]] ]] \\Big\\}{.}" , "\\end{phiquation}" , "01-" ]@@ -822,10 +822,10 @@ [ unlines [ "\\begin{tabular}{rl}" , "\\trrule{COPY}"- , " { [[ B1, \\tau -> ?, B2 ]]( \\tau -> e1 ) }"- , " { [[ B1, \\tau -> e3, B2 ]] }"- , " { if NF( e1 ) }"- , " { where e2 <- scope( e1 ); e3 <- contextualize( e1, e2 ) }"+ , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e_1 ) }"+ , " { [[ B_1, \\tau -> e_3, B_2 ]] }"+ , " { if $ \\isnormal{ e_1 } $ }"+ , " { where $ e_2 \\coloneqq \\scopeof{ e_1 } $ and $ e_3 \\coloneqq \\ctx{ e_1 }{ e_2 } $ }" , "\\end{tabular}" ] ]@@ -841,59 +841,59 @@ [ unlines [ "\\begin{tabular}{rl}" , "\\trrule{ALPHA}"- , " { [[ B1, \\tau1 -> ?, B2 ]]( \\tau2 -> e ) }"- , " { [[ B1, \\tau1 -> ?, B2 ]]( \\tau1 -> e ) }"- , " { if ordinal( \\tau2 ) = length( B1 ) }"+ , " { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_2 -> e ) }"+ , " { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> e ) }"+ , " { if $ \\indexof{ \\tau_2 } = |B_1| $ }" , " { }" , "\\trrule{COPY}"- , " { [[ B1, \\tau -> ?, B2 ]]( \\tau -> e1 ) }"- , " { [[ B1, \\tau -> e3, B2 ]] }"- , " { if NF( e1 ) }"- , " { where e2 <- scope( e1 ); e3 <- contextualize( e1, e2 ) }"+ , " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e_1 ) }"+ , " { [[ B_1, \\tau -> e_3, B_2 ]] }"+ , " { if $ \\isnormal{ e_1 } $ }"+ , " { where $ e_2 \\coloneqq \\scopeof{ e_1 } $ and $ e_3 \\coloneqq \\ctx{ e_1 }{ e_2 } $ }" , "\\trrule{DC}"- , " { T( \\tau -> e ) }"+ , " { T ( \\tau -> e ) }" , " { T }" , " { }" , " { }" , "\\trrule{DD}"- , " { T.\\tau }"+ , " { T . \\tau }" , " { T }" , " { }" , " { }" , "\\trrule{DOT}"- , " { [[ B1, \\tau -> e1, B2 ]].\\tau }"- , " { e2( ^ -> [[ B1, \\tau -> e1, B2 ]] ) }"- , " { if NF( e1 ) }"- , " { where e2 <- contextualize( e1, [[ B1, \\tau -> e1, B2 ]] ) }"+ , " { [[ B_1, \\tau -> e_1, B_2 ]] . \\tau }"+ , " { e_2 ( ^ -> [[ B_1, \\tau -> e_1, B_2 ]] ) }"+ , " { if $ \\isnormal{ e_1 } $ }"+ , " { where $ e_2 \\coloneqq \\ctx{ e_1 }{ [[ B_1, \\tau -> e_1, B_2 ]] } $ }" , "\\trrule{MISS}"- , " { [[ B ]]( \\tau -> e ) }"+ , " { [[ B ]] ( \\tau -> e ) }" , " { T }"- , " { if \\( \\tau \\notin B \\) and \\( \\tau \\notin [ ~0, ~1, \\dots ] \\) }"+ , " { if $ \\tau \\notin B \\;\\text{and}\\; \\tau \\notin [ ~0, ~1, \\dots ] $ }" , " { }" , "\\trrule{NULL}"- , " { [[ B1, \\tau -> ?, B2 ]].\\tau }"+ , " { [[ B_1, \\tau -> ?, B_2 ]] . \\tau }" , " { T }" , " { }" , " { }" , "\\trrule{OVER}"- , " { [[ B1, \\tau -> e1, B2 ]]( \\tau -> e2 ) }"+ , " { [[ B_1, \\tau -> e_1, B_2 ]] ( \\tau -> e_2 ) }" , " { T }"- , " { if \\tau \\not= ^ }"+ , " { if $ \\tau \\not= ^ $ }" , " { }" , "\\trrule{PHI}"- , " { [[ B ]].\\tau }"- , " { [[ B ]].@.\\tau }"- , " { if \\( @ \\in B \\) and \\( \\tau \\notin B \\) }"+ , " { [[ B ]] . \\tau }"+ , " { [[ B ]] . @ . \\tau }"+ , " { if $ @ \\in B \\;\\text{and}\\; \\tau \\notin B $ }" , " { }" , "\\trrule{STAY}"- , " { [[ B1, ^ -> e1, B2 ]]( ^ -> e2 ) }"- , " { [[ B1, ^ -> e1, B2 ]] }"+ , " { [[ B_1, ^ -> e_1, B_2 ]] ( ^ -> e_2 ) }"+ , " { [[ B_1, ^ -> e_1, B_2 ]] }" , " { }" , " { }" , "\\trrule{STOP}"- , " { [[ B ]].\\tau }"+ , " { [[ B ]] . \\tau }" , " { T }"- , " { if \\( \\tau \\notin B \\) and \\( @ \\notin B \\) and \\( \\lambda \\notin B \\) }"+ , " { if $ \\tau \\notin B \\;\\text{and}\\; @ \\notin B \\;\\text{and}\\; L \\notin B $ }" , " { }" , "\\end{tabular}" ]
test/CSTSpec.hs view
@@ -35,7 +35,7 @@ spec = do describe "builds valid CST" $ forM_- [ ("Q -> Q", PR_SWEET LCB (EX_GLOBAL Φ) RCB)+ [ ("Q -> Q", PR_SWEET LCB (EX_GLOBAL Φ) RCB NO_SPACE) , ( "{[[ x -> Q.y ]]}" , PR_SWEET@@ -44,12 +44,13 @@ LSB EOL (TAB 1)- (BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_DISPATCH (EX_GLOBAL Φ) (AT_LABEL "y"))) (BDS_EMPTY (TAB 1)) (TAB 1))+ (BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_DISPATCH (EX_GLOBAL Φ) NO_SPACE (AT_LABEL "y"))) (BDS_EMPTY (TAB 1)) (TAB 1)) EOL (TAB 0) RSB ) RCB+ NO_SPACE ) ] ( \(prog, cst) -> it prog $ do
test/ConditionSpec.hs view
@@ -18,7 +18,7 @@ , " not (in (!a1, !B)) " , "alpha(x)" , "eq(1, 1)"- , "or(eq(ordinal(a),1),eq(length(!B),-2),eq(!e1,!e2),eq(!a1,x),eq(Q.org.eolang,[[ x -> 2 ]]))"+ , "or(eq(index(a),1),eq(length(!B),-2),eq(!e1,!e2),eq(!a1,x),eq(Q.org.eolang,[[ x -> 2 ]]))" , "and(alpha(q),eq(-5,21))" , "nf([[ x -> !e ]].x)" , "xi(!e1)"@@ -34,7 +34,7 @@ , ("not(in(!a,!B))", Y.Not (Y.In (AtMeta "a") (BiMeta "B"))) , ("alpha(y)", Y.Alpha (AtLabel "y")) , ("eq(1,-2)", Y.Eq (Y.CmpNum (Y.Literal 1)) (Y.CmpNum (Y.Literal (-2))))- , ("eq(ordinal(z),length(!B1))", Y.Eq (Y.CmpNum (Y.Ordinal (AtLabel "z"))) (Y.CmpNum (Y.Length (BiMeta "B1"))))+ , ("eq(index(z),length(!B1))", Y.Eq (Y.CmpNum (Y.Index (AtLabel "z"))) (Y.CmpNum (Y.Length (BiMeta "B1")))) , ("eq(!a1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "a1")) (Y.CmpExpr (ExMeta "e2"))) , ("or(xi(!e1), nf(Q.x))", Y.Or [Y.Xi (ExMeta "e1"), Y.NF (ExDispatch ExGlobal (AtLabel "x"))]) , ("and(matches(\"hi\", !e),part-of(!e, !B))", Y.And [Y.Matches "hi" (ExMeta "e"), Y.PartOf (ExMeta "e") (BiMeta "B")])