phino 0.0.82 → 0.0.83

raw patch · 20 files changed

+92/−71 lines, 20 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +6/−5
• phino.cabal +1/−1
• resources/morphing.yaml +3/−3
• resources/normalize/alpha.yaml +3/−3
• resources/normalize/dca.yaml +1/−1
• src/AST.hs +1/−1
• src/Builder.hs +1/−1
• src/CST.hs +6/−9
• src/Condition.hs +1/−5
• src/Encoding.hs +2/−2
• src/LaTeX.hs +16/−6
• src/Matcher.hs +2/−2
• src/Parser.hs +16/−8
• src/Printer.hs +1/−1
• src/Render.hs +4/−4
• src/Rule.hs +2/−3
• src/Yaml.hs +8/−6
• test/CLISpec.hs +12/−6
• test/ConditionSpec.hs +4/−4
• test/ParserSpec.hs +2/−0

@@ -214,9 +214,9 @@ $ phino explain --normalize \begin{tabular}{rl} \trrule{alpha}-  { [[ B_1, \tau_1 -> ?, B_2 ]] ( \eta -> e ) }-  { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_1 -> e ) }-  { if $ \indexof{ \eta } = \vert \overline{ B_1 } \vert $ }+  { [[ B_1, \tau -> ?, B_2 ]] ( \alpha_{i} -> e ) }+  { [[ B_1, \tau -> ?, B_2 ]] ( \tau -> e ) }+  { if $ i = \vert \overline{ B_1 } \vert $ }   { } \trrule{dc}   { T ( \tau -> e ) }@@ -318,7 +318,7 @@  Number:                  # comparable number   = Integer              # just regular integer-  | index: Alpha'        # calculate index of alpha+  | IndexMeta'           # 𝑖 (or !i), the index captured by an α𝑖 argument   | length: BiMeta'      # calculate length of bindings by given meta binding  Extension:               # substitutions extension used to introduce new meta variables@@ -377,7 +377,8 @@ This is the list of supported meta variables:  * `!a` || `𝜏` - attribute-* `!h` || `𝜂` - alpha, the positional index of an application argument+* `!i` || `𝑖` - the index of a positional (α) application argument,+                captured by writing `α𝑖` * `!e` || `𝑒` - any expression * `!n` || `𝑛` - any expression that is already in normal form (behaves like                 `!e`/`𝑒`, but only binds a sub-expression in NF, so no explicit

@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.82+version: 0.0.83 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>

@@ -50,8 +50,8 @@       normalize: '𝑒1(𝜏 ↦ 𝑒)'  - name: applicationa-  description: '𝕄(n(η ↦ e)) ⟿ 𝕄(𝒩(𝕄(n)(η ↦ e)))'-  match: '𝑛(𝜂 ↦ 𝑒)'+  description: '𝕄(n(α_i ↦ e)) ⟿ 𝕄(𝒩(𝕄(n)(α_i ↦ e)))'+  match: '𝑛(α𝑖 ↦ 𝑒)'   where:     - meta: 𝑒1       function: morph@@ -59,7 +59,7 @@         - 𝑛   then:     morph:-      normalize: '𝑒1(𝜂 ↦ 𝑒)'+      normalize: '𝑒1(α𝑖 ↦ 𝑒)'  - name: root   description: '𝕄(Φ) ⟿ 𝕄(𝒩(e)) where e := global(), unless e is Φ'

@@ -2,9 +2,9 @@ # SPDX-License-Identifier: MIT --- name: alpha-pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜂 ↦ 𝑒)-result: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒)+pattern: ⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧(α𝑖 ↦ 𝑒)+result: ⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧(𝜏 ↦ 𝑒) when:   eq:-    - index: 𝜂+    - 𝑖     - domain: 𝐵1

@@ -2,5 +2,5 @@ # SPDX-License-Identifier: MIT --- name: dca-pattern: ⊥(𝜂 ↦ 𝑒)+pattern: ⊥(α𝑖 ↦ 𝑒) result: ⊥

@@ -77,7 +77,7 @@  instance Show Alpha where   show (Alpha idx) = 'α' : show idx-  show (AlMeta meta) = '!' : T.unpack meta+  show (AlMeta meta) = 'α' : '!' : T.unpack meta  -- A cheap, fixed-size digest of an expression, used for fast (dirty) equality -- checks during loop detection. Equal expressions always produce the same

@@ -71,7 +71,7 @@  buildAlpha :: Alpha -> Subst -> Built Alpha buildAlpha (AlMeta meta) (Subst mp) = case Map.lookup meta mp of-  Just (MvAlpha alpha) -> Right alpha+  Just (MvIndex idx) -> Right (Alpha idx)   _ -> Left (metaMsg meta) buildAlpha a _ = Right a 

@@ -86,9 +86,8 @@   | A -- a   | TAU -- 𝜏   | TAU' -- \tau-  | ETA -- 𝜂-  | ETA' -- \eta-  | H -- h+  | I -- 𝑖+  | I' -- i   | B -- 𝐵   | B' -- B   | D -- δ@@ -175,6 +174,7 @@ data ATTRIBUTE   = AT_LABEL {label :: T.Text}   | AT_ALPHA {alpha :: ALPHA, idx :: Int}+  | AT_ALPHA_META {alpha :: ALPHA, meta :: META}   | AT_RHO {rho :: RHO}   | AT_PHI {phi :: PHI}   | AT_LAMBDA {lambda :: LAMBDA}@@ -204,7 +204,7 @@   deriving (Eq, Show)  data NUMBER-  = INDEX {attr :: ATTRIBUTE}+  = IDX_META {meta :: META}   | LENGTH {binding :: BINDING}   | DOMAIN {binding :: BINDING}   | LITERAL {num :: Int}@@ -262,9 +262,6 @@ attributeToCST :: Attribute -> ATTRIBUTE attributeToCST = toCST' -alphaToCST :: Alpha -> ATTRIBUTE-alphaToCST = toCST'- bindingsToCST :: [Binding] -> BINDING bindingsToCST = toCST' @@ -514,7 +511,7 @@  instance ToCST Alpha ATTRIBUTE where   toCST (Alpha idx) _ = AT_ALPHA ALPHA idx-  toCST (AlMeta mt) _ = AT_META (META NO_EXCL ETA (metaTail mt))+  toCST (AlMeta mt) _ = AT_ALPHA_META ALPHA (META NO_EXCL I (metaTail mt))  instance ToCST Y.Condition CONDITION where   toCST (Y.Not (Y.In attr binding)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_BINDING (bindingsToCST [binding]))@@ -541,7 +538,7 @@   toCST (Y.CmpNum num) _ = CMP_NUM (numberToCST num)  instance ToCST Y.Number NUMBER where-  toCST (Y.Index alpha) _ = INDEX (alphaToCST alpha)+  toCST (Y.MetaIndex mt) _ = IDX_META (META NO_EXCL I (metaTail mt))   toCST (Y.Length binding) _ = LENGTH (bindingsToCST [binding])   toCST (Y.Domain binding) _ = DOMAIN (bindingsToCST [binding])   toCST (Y.Literal num) _ = LITERAL num

@@ -49,11 +49,6 @@ number =   choice     [ do-        _ <- symbol "index" >> lparen-        alpha <- _alpha phiParser-        _ <- rparen-        return (Y.Index alpha)-    , do         _ <- symbol "length" >> lparen         bd <- _binding phiParser         _ <- rparen@@ -63,6 +58,7 @@         bd <- _binding phiParser         _ <- rparen         return (Y.Domain bd)+    , Y.MetaIndex <$> _indexMeta phiParser     , do         sign <- optional (choice [char '-', char '+'])         unsigned <- lexeme L.decimal

@@ -70,9 +70,9 @@  instance ToASCII ATTRIBUTE where   toASCII AT_ALPHA{..} = AT_ALPHA ALPHA' idx+  toASCII AT_ALPHA_META{..} = AT_ALPHA_META ALPHA' (META EXCL I' (rest meta))   toASCII AT_PHI{} = AT_PHI AT   toASCII AT_RHO{} = AT_RHO CARET-  toASCII AT_META{meta = META{hd = ETA, ..}} = AT_META (META EXCL H rest)   toASCII AT_META{..} = AT_META (META EXCL A (rest meta))   toASCII attr = attr @@ -81,7 +81,7 @@   toASCII ST_ATTRIBUTES{..} = ST_ATTRIBUTES (map toASCII attrs)  instance ToASCII NUMBER where-  toASCII INDEX{..} = INDEX (toASCII attr)+  toASCII IDX_META{..} = IDX_META (META EXCL I' (rest meta))   toASCII LENGTH{..} = LENGTH (toASCII binding)   toASCII DOMAIN{..} = DOMAIN (toASCII binding)   toASCII literal@LITERAL{} = literal

@@ -167,6 +167,17 @@   let (progs, rules) = unzip rewrittens    in if _compress then zip (meetInPrograms progs ctx) rules else rewrittens +-- Compress a sequence of focused sub-expressions the way 'compressedRewrittens'+-- compresses whole programs: each expression is wrapped as a program so the+-- meet machinery factors recurring sub-expressions out across the sequence.+-- Focusing happens before this, so the meet never replaces a program root the+-- focus must still descend through.+compressedExpressions :: [Expression] -> LatexContext -> [Expression]+compressedExpressions exprs ctx@LatexContext{..} =+  if _compress then map unwrap (meetInPrograms (map Program exprs) ctx) else exprs+  where+    unwrap (Program expr) = expr+ rewrittensToLatex :: Rewrittens' -> LatexContext -> IO String rewrittensToLatex (rewrittens, exceeded) ctx@LatexContext{_focus = ExRoot} =   pure@@ -177,12 +188,12 @@         ]     ) rewrittensToLatex (rewrittens, exceeded) ctx@LatexContext{..} = do-  let (progs, rules) = unzip (compressedRewrittens rewrittens ctx)-  exprs <- mapM (locatedExpression _focus) progs+  let (progs, rules) = unzip rewrittens+  focused <- mapM (locatedExpression _focus) progs   pure     ( concat         [ preamble ctx-        , body (zip exprs rules) (\expr -> renderToLatex (expressionToCST expr) ctx)+        , body (zip (compressedExpressions focused ctx) rules) (\expr -> renderToLatex (expressionToCST expr) ctx)         , ending exceeded ctx         ]     )@@ -227,6 +238,7 @@  instance ToLaTeX ATTRIBUTE where   toLaTeX AT_LABEL{..} = AT_LABEL (piped label)+  toLaTeX AT_ALPHA_META{..} = AT_LABEL ("\\alpha_{" <> render (hd meta) <> rest meta <> "}")   toLaTeX AT_META{..} = AT_META (toLaTeX meta)   toLaTeX AT_LAMBDA{} = AT_LAMBDA LAMBDA'   toLaTeX AT_DELTA{} = AT_DELTA DELTA'@@ -271,8 +283,6 @@   toLaTeX K = K'   toLaTeX A = TAU'   toLaTeX TAU = TAU'-  toLaTeX ETA = ETA'-  toLaTeX H = ETA'   toLaTeX B = B'   toLaTeX D = D'   toLaTeX mh = mh@@ -302,7 +312,7 @@   toLaTeX ST_ATTRIBUTES{..} = ST_ATTRIBUTES (map toLaTeX attrs)  instance ToLaTeX NUMBER where-  toLaTeX INDEX{..} = INDEX (toLaTeX attr)+  toLaTeX IDX_META{..} = IDX_META (toLaTeX meta)   toLaTeX LENGTH{..} = LENGTH (toLaTeX binding)   toLaTeX DOMAIN{..} = DOMAIN (toLaTeX binding)   toLaTeX literal@LITERAL{} = literal

@@ -15,7 +15,7 @@ -- The right part of substitution data MetaValue   = MvAttribute Attribute -- !a-  | MvAlpha Alpha -- !h+  | MvIndex Int -- α𝑖   | MvBytes Bytes -- !b   | MvBindings [Binding] -- !B   | MvFunction Text -- !F@@ -62,7 +62,7 @@   | otherwise = []  matchAlpha :: Alpha -> Alpha -> [Subst]-matchAlpha (AlMeta meta) tgt = [substSingle meta (MvAlpha tgt)]+matchAlpha (AlMeta meta) (Alpha idx) = [substSingle meta (MvIndex idx)] matchAlpha ptn tgt   | ptn == tgt = [substEmpty]   | otherwise = []

@@ -13,6 +13,7 @@   , parseAttribute   , parseAttributeThrows   , parseAlpha+  , parseIndexMeta   , parseNumber   , parseNumberThrows   , parseBinding@@ -49,13 +50,14 @@ data PhiParser = PhiParser   { _attribute :: Parser Attribute   , _alpha :: Parser Alpha+  , _indexMeta :: Parser T.Text   , _binding :: Parser Binding   , _expression :: Parser Expression   , _string :: Parser String   }  phiParser :: PhiParser-phiParser = PhiParser attribute alpha binding expression quotedStr+phiParser = PhiParser attribute alpha indexMeta binding expression quotedStr  instance Show ParserException where   show CouldNotParseProgram{..} = printf "Couldn't parse given phi program, cause: %s" message@@ -132,7 +134,7 @@   choice     [ meta ch     , do-        _ <- symbol uni+        _ <- string uni         suf <- metaSuffix         return (T.pack (ch : suf))     ]@@ -330,16 +332,19 @@     ]     <?> "attribute" +-- index meta: !i, 𝑖+indexMeta :: Parser T.Text+indexMeta = meta' 'i' "𝑖"+ -- alpha -- 1. index: ~0, α0--- 2. meta: !h, 𝜂+-- 2. meta: α𝑖, ~!i alpha :: Parser Alpha-alpha =+alpha = do+  _ <- choice [symbol "~", symbol "α"]   choice-    [ do-        _ <- choice [symbol "~", symbol "α"]-        Alpha <$> lexeme L.decimal-    , AlMeta <$> meta' 'h' "𝜂"+    [ Alpha <$> lexeme L.decimal+    , AlMeta <$> indexMeta     ]     <?> "alpha" @@ -498,6 +503,9 @@  parseAlpha :: String -> Either String Alpha parseAlpha = parse' "alpha" alpha++parseIndexMeta :: String -> Either String T.Text+parseIndexMeta = parse' "index meta" indexMeta  parseAttributeThrows :: String -> IO Attribute parseAttributeThrows attr = case parseAttribute attr of

@@ -91,7 +91,7 @@  printMetaValue :: MetaValue -> PrintConfig -> String printMetaValue (MvAttribute att) (_, encoding, _, _) = printAttribute' att encoding-printMetaValue (MvAlpha index) (_, encoding, _, _) = printAlpha' index encoding+printMetaValue (MvIndex index) _ = show index printMetaValue (MvExpression ex) config = printExpression' ex config printMetaValue (MvBytes bts) _ = printBytes bts printMetaValue (MvBindings bds) config = printExpression' (ExFormation bds) config

@@ -120,9 +120,8 @@   render A = "a"   render TAU = "𝜏"   render TAU' = "\\tau"-  render ETA = "𝜂"-  render ETA' = "\\eta"-  render H = "h"+  render I = "𝑖"+  render I' = "i"   render B = "𝐵"   render B' = "B"   render D = "δ"@@ -207,6 +206,7 @@ instance Render ATTRIBUTE where   render AT_LABEL{..} = render label   render AT_ALPHA{..} = render alpha <> render idx+  render AT_ALPHA_META{..} = render alpha <> render meta   render AT_RHO{..} = render rho   render AT_PHI{..} = render phi   render AT_LAMBDA{..} = render lambda@@ -227,7 +227,7 @@   render OR = "\\;\\text{or}\\;"  instance Render NUMBER where-  render INDEX{..} = "\\indexof{ " <> render attr <> " }"+  render IDX_META{..} = render meta   render LENGTH{..} = "\\vert " <> render binding <> " \\vert"   render DOMAIN{..} = "\\vert \\overline{ " <> render binding <> " } \\vert"   render LITERAL{..} = T.pack (show num)

@@ -117,10 +117,9 @@   where     -- Convert Number to Int     numToInt :: Y.Number -> Subst -> Maybe Int-    numToInt (Y.Index (AlMeta meta)) (Subst mp) = case M.lookup meta mp of-      Just (MvAlpha (Alpha idx)) -> Just idx+    numToInt (Y.MetaIndex meta) (Subst mp) = case M.lookup meta mp of+      Just (MvIndex idx) -> Just idx       _ -> Nothing-    numToInt (Y.Index (Alpha idx)) _ = Just idx     numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of       Just (MvBindings bds) -> Just (length bds)       _ -> Nothing

@@ -15,7 +15,7 @@ import Data.Aeson import qualified Data.ByteString as BS import Data.FileEmbed (embedDir, embedFile)-import Data.Text (unpack)+import Data.Text (Text, unpack) import Data.Yaml (Parser) import qualified Data.Yaml as Yaml import GHC.Generics (Generic)@@ -58,15 +58,17 @@ instance FromJSON Number where   parseJSON v = case v of     Object o -> do-      validateYamlObject o ["index", "length", "domain"]+      validateYamlObject o ["length", "domain"]       asum-        [ Index <$> o .: "index"-        , Length <$> o .: "length"+        [ Length <$> o .: "length"         , Domain <$> o .: "domain"         ]     Number num -> pure (Literal (round num))+    String txt -> case parseIndexMeta (unpack txt) of+      Right mt -> pure (MetaIndex mt)+      Left err -> fail err     _ ->-      fail "Expected a numerable expression (object or number)"+      fail "Expected a numerable expression (object, number or index meta)"  instance FromJSON Comparable where   parseJSON v =@@ -149,7 +151,7 @@         }  data Number-  = Index Alpha+  = MetaIndex Text   | Length Binding   | Domain Binding   | Literal Int

@@ -874,6 +874,12 @@               ]           ] +    it "focuses a compressed sequence whose meet replaces a step root" $+      withStdin "{[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]}" $+        testCLISucceeded+          ["dataize", "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--hide=Q.bytes", "--hide=Q.number", "--locator=Q.@", "--focus=Q.@", "--meet-length=5", "--meet-popularity=1"]+          ["\\phiMeet{dataization:1}{ [[ @ -> |c| . |plus| ( 32 ), |c| -> 25 ]] } \\leadsto_{\\nameref{r:contextualize}}"]+     it "dataizes with --locator" $       withStdin "{[[ ex -> [[ @ -> Q.x ]], x -> [[ D> 42- ]] ]]}" $         testCLISucceeded ["dataize", "--locator=Q.ex"] ["42-"]@@ -945,9 +951,9 @@         [ unlines             [ "\\begin{tabular}{rl}"             , "\\trrule{alpha}"-            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\eta -> e ) }"-            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> e ) }"-            , "  { if $ \\indexof{ \\eta } = \\vert \\overline{ B_1 } \\vert $ }"+            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\alpha_{i} -> e ) }"+            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e ) }"+            , "  { if $ i = \\vert \\overline{ B_1 } \\vert $ }"             , "  { }"             , "\\trrule{copy}"             , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"@@ -960,7 +966,7 @@             , "  { }"             , "  { }"             , "\\trrule{dca}"-            , "  { T ( \\eta -> e ) }"+            , "  { T ( \\alpha_{i} -> e ) }"             , "  { T }"             , "  { }"             , "  { }"@@ -1034,8 +1040,8 @@             , "  { }"             , "  { where $ e_1 \\coloneqq morph( n ) $ }"             , "\\trrule{applicationa}"-            , "  { \\mathbb{M}( n ( \\eta -> e ) ) }"-            , "  { \\mathbb{M}( \\mathcal{N}( e_1 ( \\eta -> e ) ) ) }"+            , "  { \\mathbb{M}( n ( \\alpha_{i} -> e ) ) }"+            , "  { \\mathbb{M}( \\mathcal{N}( e_1 ( \\alpha_{i} -> e ) ) ) }"             , "  { }"             , "  { where $ e_1 \\coloneqq morph( n ) $ }"             , "\\trrule{root}"

@@ -5,7 +5,7 @@  module ConditionSpec where -import AST (Alpha (AlMeta, Alpha), Attribute (AtLabel, AtMeta), Binding (BiMeta), Expression (ExDispatch, ExMeta, ExRoot))+import AST (Attribute (AtLabel, AtMeta), Binding (BiMeta), Expression (ExDispatch, ExMeta, ExRoot)) import Condition import Control.Monad (forM_) import Data.Either (isLeft, isRight)@@ -19,7 +19,7 @@       [ "in (!a, !B)"       , " not   (in (!a1,   !B))   "       , "eq(1, 1)"-      , "or(eq(index(~0),1),eq(length(!B),-2),eq(!e1,!e2),eq(!a1,x),eq(Q.org.eolang,[[ x -> 2 ]]))"+      , "or(eq(!i,1),eq(length(!B),-2),eq(!e1,!e2),eq(!a1,x),eq(Q.org.eolang,[[ x -> 2 ]]))"       , "nf([[ x -> !e ]].x)"       , "absolute(!e1)"       , "matches(\"hello(\\\"\\u0000)\", !e)"@@ -32,8 +32,8 @@       [ ("in(!a, !B)", Y.In (AtMeta "a") (BiMeta "B"))       , ("not(in(!a,!B))", Y.Not (Y.In (AtMeta "a") (BiMeta "B")))       , ("eq(1,-2)", Y.Eq (Y.CmpNum (Y.Literal 1)) (Y.CmpNum (Y.Literal (-2))))-      , ("eq(index(α0),length(!B1))", Y.Eq (Y.CmpNum (Y.Index (Alpha 0))) (Y.CmpNum (Y.Length (BiMeta "B1"))))-      , ("eq(index(!h),domain(!B1))", Y.Eq (Y.CmpNum (Y.Index (AlMeta "h"))) (Y.CmpNum (Y.Domain (BiMeta "B1"))))+      , ("eq(!i,length(!B1))", Y.Eq (Y.CmpNum (Y.MetaIndex "i")) (Y.CmpNum (Y.Length (BiMeta "B1"))))+      , ("eq(!i2,domain(!B1))", Y.Eq (Y.CmpNum (Y.MetaIndex "i2")) (Y.CmpNum (Y.Domain (BiMeta "B1"))))       , ("eq(!a1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "a1")) (Y.CmpExpr (ExMeta "e2")))       , ("or(absolute(!e1), nf(Q.x))", Y.Or [Y.Absolute (ExMeta "e1"), Y.NF (ExDispatch ExRoot (AtLabel "x"))])       , ("and(matches(\"hi\", !e),part-of(!e, !B))", Y.And [Y.Matches "hi" (ExMeta "e"), Y.PartOf (ExMeta "e") (BiMeta "B")])

@@ -207,6 +207,8 @@       , "[[ x -> \"\\uD835\\uDF11\"]]"       , "[[ x ↦ \"This plugin has \\x01\\x01\" ]]"       , "[[ !afoo -> !e1Some, !a-BAR -> !e_123someW, !Bhi123 ]]"+      , "[[ !B ]](α𝑖 -> !e)"+      , "[[ 𝜏 -> !e, 𝐵 ]]"       ]       (\expr -> it expr (parseExpression expr `shouldSatisfy` isRight))