diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,36 @@ ## [Unreleased] +## [0.8.0.0] — 2026-08-02 + +### Added + +- `TOpaqueLit` and `opaqueLit` preserve exact concrete, replay, pure-analysis, + and symbolic literal semantics while deliberately rendering the stored value + as ``. +- `MermaidUpdateMode`, `topologyMermaidOptions`, and `toTopologyMermaid` make + complete updates, compact written-slot summaries, and Keiki 0.7-compatible + topology output explicit policies. +- Options-aware Mermaid entry points now cover composite, nested, three-way, + alternative, feedback, and labeled diagrams. Backend-level regression tests + pin semantic-label escaping through the documentation site's + `beautiful-mermaid` renderer. + +### Changed + +- **Breaking:** `TLit` and `lit` now require `Show` so renderers derive ordinary + literal text from the executable value. Exhaustive `Term` matches must handle + `TOpaqueLit`; values without `Show`, secrets, and deliberately redacted values + use `opaqueLit`. +- **Breaking:** `toMermaid` and every no-options shape renderer now default to + readable guards, complete register assignments, multiline labels, and no + semantic truncation. Use `toTopologyMermaid` or an options-aware shape + renderer with `topologyMermaidOptions` for the previous compact bytes. +- **Breaking:** `MermaidOptions` removes `showWrittenSlots` and + `showGuardSummary`. Set `updateMode = MermaidUpdateWrittenSlots` and + `guardMode = MermaidGuardStructuralSummary` respectively. + + ## [0.7.0.0] — 2026-08-01 ### Added diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -56,7 +56,8 @@ - per-vertex projections (the "B-presentation" view), - checked sequential composition (`composeChecked`) plus `alternative` and `feedback1`, - profunctor / `Category` / `Strong` / `Choice` / `Arrow` instances, -- Mermaid and Markdown renderers for documentation, +- behavior-readable Mermaid and Markdown renderers, with explicit compact + topology output, - eager builder validation, default-on replay-safety checks, and optional single-valuedness checks via SBV + z3. @@ -66,9 +67,9 @@ ## Status -Pre-1.0, prepared for the initial `0.1.0.0` Hackage release. The -planned v0.1 surface is implemented and validated against in-tree tests -plus the downstream `jitsurei` worked-example package. +Pre-1.0 and released under the Haskell PVP. The current surface is validated +against the in-tree suites plus the downstream `jitsurei` worked-example +package; see [`CHANGELOG.md`](CHANGELOG.md) for release history and migrations. The core package is intentionally codec-free. JSON support lives in [`keiki-codec-json`](keiki-codec-json/README.md), and downstream codec @@ -117,6 +118,12 @@ Forward decisions, structured replay, `Acceptor`s, and the per-vertex view all operate from this one declaration. See the downstream `jitsurei` package for the full worked aggregates the test suite drives. + +The primary `toMermaid emailDelivery` diagram is derived from the same edge AST +and shows its command, event constructor, complete register assignments, and +guard. Use `toTopologyMermaid emailDelivery` when only shape is intended. +Ordinary `lit` values appear in readable diagrams; model a value with +`opaqueLit` when it lacks `Show` or must remain redacted. ## Repository documentation diff --git a/keiki.cabal b/keiki.cabal --- a/keiki.cabal +++ b/keiki.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: keiki -version: 0.7.0.0 +version: 0.8.0.0 synopsis: Pure core for symbolic-register transducer event sourcing. description: A Haskell library for the pure core of event sourcing, workflow diff --git a/src/Keiki/Composition.hs b/src/Keiki/Composition.hs --- a/src/Keiki/Composition.hs +++ b/src/Keiki/Composition.hs @@ -248,12 +248,13 @@ weakenL (SIdx i) = SIdx (weakenL @_ @rs2 i) -- | Walk a 'Term' and weaken every register read across an rs2 --- suffix. 'TInpCtorField' / 'TLit' do not touch the register file, +-- suffix. 'TInpCtorField', 'TLit', and 'TOpaqueLit' do not touch the register file, -- so they pass through unchanged. weakenLTerm :: forall rs1 rs2 ci ifs r. Term rs1 ci ifs r -> Term (Append rs1 rs2) ci ifs r weakenLTerm (TLit r) = TLit r +weakenLTerm (TOpaqueLit r) = TOpaqueLit r weakenLTerm (TReg ix) = TReg (weakenL @rs1 @rs2 ix) weakenLTerm (TInpCtorField ic ix) = TInpCtorField ic ix weakenLTerm (TApp1 f t) = TApp1 f (weakenLTerm @rs1 @rs2 t) @@ -331,6 +332,7 @@ (WeakenR rs1) => Term rs2 ci ifs r -> Term (Append rs1 rs2) ci ifs r weakenRTerm (TLit r) = TLit r +weakenRTerm (TOpaqueLit r) = TOpaqueLit r weakenRTerm (TReg ix) = TReg (weakenR @rs1 ix) weakenRTerm (TInpCtorField ic ix) = TInpCtorField ic ix weakenRTerm (TApp1 f t) = TApp1 f (weakenRTerm @rs1 @rs2 t) @@ -466,12 +468,13 @@ -- Structural walkers see an opaque 'TApp1' over a harmless literal, so a -- constructor-mismatched composite edge cannot crash validation or rendering. poisonTerm :: String -> Term rs ci ifs r -poisonTerm message = TApp1 (\() -> error message) (TLit ()) +poisonTerm message = TApp1 (\() -> error message) (TOpaqueLit ()) -- | Detect a field read for a constructor other than the mid constructor -- produced by the t1 output currently being substituted. termHasCtorMismatch :: String -> Term rs ci ifs r -> Bool termHasCtorMismatch _ (TLit _) = False +termHasCtorMismatch _ (TOpaqueLit _) = False termHasCtorMismatch _ (TReg _) = False termHasCtorMismatch expected (TInpCtorField ic _) = icName ic /= expected termHasCtorMismatch expected (TApp1 _ term) = termHasCtorMismatch expected term @@ -500,6 +503,7 @@ OutTerm rs1 ci1 mid -> Term (Append rs1 rs2) ci1 ifsR r substTerm (TLit r) _o1 = TLit r +substTerm (TOpaqueLit r) _o1 = TOpaqueLit r substTerm (TReg ix2) _o1 = TReg (weakenR @rs1 ix2) substTerm (TInpCtorField ic2 ix2) o1 = substInputField @rs1 @rs2 ic2 ix2 o1 @@ -593,7 +597,9 @@ projectThroughTermWithStatus witness (TInpCtorField ic ix) = (TFieldProj witness (PBInp ic ix), ProjectionPreserved) projectThroughTermWithStatus witness (TLit owner) = - (TLit (fieldWitnessGet witness owner), ProjectionFolded) + (TOpaqueLit (fieldWitnessGet witness owner), ProjectionFolded) +projectThroughTermWithStatus witness (TOpaqueLit owner) = + (TOpaqueLit (fieldWitnessGet witness owner), ProjectionFolded) projectThroughTermWithStatus witness ownerTerm = (TApp1 (fieldWitnessGet witness) ownerTerm, ProjectionLowered) @@ -805,12 +811,13 @@ -- | Lift a 'Term' from the left side's input alphabet to -- @Either ci1 ci2@. Walks the AST and adjusts every 'TInpCtorField' --- to read through 'leftInCtor'. 'TLit' / 'TReg' don't depend on +-- to read through 'leftInCtor'. Literals and 'TReg' don't depend on -- @ci@ and pass through unchanged. liftLTermAlt :: forall rs ci1 ci2 ifs r. Term rs ci1 ifs r -> Term rs (Either ci1 ci2) ifs r liftLTermAlt (TLit r) = TLit r +liftLTermAlt (TOpaqueLit r) = TOpaqueLit r liftLTermAlt (TReg ix) = TReg ix liftLTermAlt (TInpCtorField ic ix) = TInpCtorField (leftInCtor ic) ix liftLTermAlt (TApp1 f t) = TApp1 f (liftLTermAlt @rs @ci1 @ci2 t) @@ -829,6 +836,7 @@ forall rs ci1 ci2 ifs r. Term rs ci2 ifs r -> Term rs (Either ci1 ci2) ifs r liftRTermAlt (TLit r) = TLit r +liftRTermAlt (TOpaqueLit r) = TOpaqueLit r liftRTermAlt (TReg ix) = TReg ix liftRTermAlt (TInpCtorField ic ix) = TInpCtorField (rightInCtor ic) ix liftRTermAlt (TApp1 f t) = TApp1 f (liftRTermAlt @rs @ci1 @ci2 t) @@ -1104,6 +1112,7 @@ Term rs ci ifs r -> Term rs ci ifs r applyEnvTerm _ (TLit r) = TLit r +applyEnvTerm _ (TOpaqueLit r) = TOpaqueLit r applyEnvTerm env (TReg ix) = maybe (TReg ix) id (lookupPending ix env) applyEnvTerm _ (TInpCtorField ic ix) = TInpCtorField ic ix applyEnvTerm env (TApp1 f term) = TApp1 f (applyEnvTerm env term) @@ -1251,6 +1260,7 @@ termExpectedReads :: Term rs ci ifs r -> [(String, Int)] termExpectedReads (TLit _) = [] +termExpectedReads (TOpaqueLit _) = [] termExpectedReads (TReg _) = [] termExpectedReads (TInpCtorField ic ix) = [(icName ic, indexInt ix)] termExpectedReads (TApp1 _ term) = termExpectedReads term @@ -1341,6 +1351,7 @@ goTerm :: forall ifs r. Term rs2 mid ifs r -> [ComposeAlignmentWarning s1 s2] goTerm (TLit _) = [] + goTerm (TOpaqueLit _) = [] goTerm (TReg _) = [] goTerm (TInpCtorField _ _) = [] goTerm (TApp1 _ term) = goTerm term @@ -1393,6 +1404,7 @@ goTerm :: forall ifs r. Term rs ci ifs r -> [ComposeAlignmentWarning s1 s2] goTerm (TLit _) = [] + goTerm (TOpaqueLit _) = [] goTerm (TReg _) = [] goTerm (TInpCtorField _ _) = [] goTerm (TApp1 _ term) = goTerm term diff --git a/src/Keiki/Core.hs b/src/Keiki/Core.hs --- a/src/Keiki/Core.hs +++ b/src/Keiki/Core.hs @@ -119,6 +119,7 @@ regProj, inpProj, lit, + opaqueLit, tadd, tsub, tmul, @@ -536,7 +537,7 @@ -- The @ifs :: [Slot]@ parameter is the /input field schema/ this term -- may project from: it is pinned by 'TInpCtorField' (whose 'Index' is -- into @ifs@) and left free by terms that do not read an input field --- ('TLit', 'TReg'). Threading @ifs@ through the AST is what lets an +-- ('TLit', 'TOpaqueLit', 'TReg'). Threading @ifs@ through the AST is what lets an -- 'OutFields' (and hence an 'OPack') guarantee /by construction/ that -- every top-level input projection reads the same constructor schema as -- the 'OPack''s 'InCtor' — so 'solveOutput' recovers a command field @@ -545,7 +546,12 @@ -- existentially hide @ifs@, so it never leaks into the 'Edge' / -- 'SymTransducer' surface. See @docs/research/tinpproj-design.md@. data Term (rs :: [Slot]) (ci :: Type) (ifs :: [Slot]) (r :: Type) where - TLit :: r -> Term rs ci ifs r + -- | An ordinary literal. The 'Show' dictionary is presentation evidence + -- retained for renderers; evaluation and proof paths use only the value. + TLit :: (Show r) => r -> Term rs ci ifs r + -- | A display-opaque literal. It has the same concrete and symbolic meaning + -- as 'TLit' but renderers deliberately do not expose its value. + TOpaqueLit :: r -> Term rs ci ifs r TReg :: Index rs r -> Term rs ci ifs r -- | Structural input projection: read field @ix@ of the input -- constructor described by @ic@. The 'InCtor' value names the @@ -1032,10 +1038,16 @@ Term rs ci ifs (FieldResult projection) inpProj witness ic ix = TFieldProj witness (PBInp ic ix) --- | A constant 'Term'. -lit :: r -> Term rs ci ifs r +-- | A readable constant 'Term'. Renderers derive its text from 'show'; use +-- 'opaqueLit' when the value has no 'Show' instance or must remain redacted. +lit :: (Show r) => r -> Term rs ci ifs r lit = TLit +-- | A display-opaque constant 'Term'. This changes presentation only: concrete +-- evaluation and symbolic translation still treat the stored value exactly. +opaqueLit :: r -> Term rs ci ifs r +opaqueLit = TOpaqueLit + -- | Structural arithmetic smart constructors. @tadd@\/@tsub@\/@tmul@ -- build a 'TArith' over @+@\/@-@\/@*@. The operand type must be numeric -- ('Num') and 'Typeable'; the SBV translator reads them structurally @@ -1137,6 +1149,7 @@ -- | Evaluate a 'Term' against a register file and an input symbol. evalTerm :: Term rs ci ifs r -> RegFile rs -> ci -> r evalTerm (TLit r) _ _ = r +evalTerm (TOpaqueLit r) _ _ = r evalTerm (TReg ix) regs _ = regs ! ix evalTerm (TInpCtorField ic ix) _ ci = case icMatch ic ci of Just rf -> rf ! ix @@ -2022,7 +2035,8 @@ -- == Recompute-and-verify (EP-47) -- -- The command is recovered from the /invertible/ fields alone --- (@TLit@\/@TReg@\/@TInpCtorField@); /derived/ fields (@TArith@\/@TApp1@\/ +-- (@TLit@\/@TOpaqueLit@\/@TReg@\/@TInpCtorField@); /derived/ fields +-- (@TArith@\/@TApp1@\/ -- @TApp2@) are skipped during recovery by 'gatherInpEntries'. After the -- command is rebuilt, the observed field tuple is rebuilt with each -- /derived/ field recomputed forward (via 'recomputeDerivedFields') and @@ -2067,7 +2081,7 @@ -- | Rebuild an observed output-field tuple, recomputing each /derived/ -- field ('TApp1'\/'TApp2'\/'TArith') forward via 'evalTerm' against the -- recovered command and the pre-update registers, while leaving every --- /invertible/ field ('TLit'\/'TReg'\/'TInpCtorField') at its observed +-- /invertible/ field ('TLit'\/'TOpaqueLit'\/'TReg'\/'TInpCtorField') at its observed -- value. Used by 'solveOutput' (EP-47 recompute-and-verify): comparing the -- rebuilt event to the observed one (via 'Eq' on @co@) then verifies -- exactly the derived fields. Invertible fields are deliberately /not/ @@ -2091,7 +2105,7 @@ -- | Walk an 'OutFields' HList in lockstep with an observed-fields -- tuple, gathering '(Index, value)' pairs for the named 'InCtor' from --- the /invertible/ fields. 'TLit'\/'TReg' contribute nothing; a +-- the /invertible/ fields. 'TLit'\/'TOpaqueLit'\/'TReg' contribute nothing; a -- 'TInpCtorField' for the matching 'InCtor' contributes its -- '(Index, value)' pair. Since EP-47 the /derived/ fields -- ('TArith'\/'TApp1'\/'TApp2') are /skipped/ (they contribute no @@ -2127,6 +2141,7 @@ where stepOne :: forall f. Term rs ci ifs f -> f -> InCtor ci ifs -> Maybe [ByIndex ifs] stepOne (TLit _) _val _ = Just [] + stepOne (TOpaqueLit _) _val _ = Just [] stepOne (TReg _) _val _ = Just [] stepOne (TInpCtorField ic2 ix) val ic1 | icName ic1 == icName ic2 = Just [ByIndex ix val] @@ -2322,6 +2337,7 @@ -- | Does the 'Term' read the input symbol via 'TInpCtorField'? termReadsInput :: Term rs ci ifs r -> Bool termReadsInput (TLit _) = False +termReadsInput (TOpaqueLit _) = False termReadsInput (TReg _) = False termReadsInput (TInpCtorField _ _) = True termReadsInput (TApp1 _ t) = termReadsInput t @@ -2338,6 +2354,7 @@ where termHasInpCtorField :: Term rs ci ifs r -> Bool termHasInpCtorField (TLit _) = False + termHasInpCtorField (TOpaqueLit _) = False termHasInpCtorField (TReg _) = False termHasInpCtorField (TInpCtorField _ _) = True termHasInpCtorField (TApp1 _ t') = termHasInpCtorField t' @@ -2710,6 +2727,7 @@ -- deliberately falls back to a fresh domain-valid value. termHasOpaqueFallback :: forall rs ci ifs r. Term rs ci ifs r -> Bool termHasOpaqueFallback (TLit _) = False +termHasOpaqueFallback (TOpaqueLit _) = False termHasOpaqueFallback (TReg _) = False termHasOpaqueFallback (TInpCtorField _ _) = False termHasOpaqueFallback (TApp1 _ _) = True @@ -2774,6 +2792,7 @@ termProjectionInfos :: Term rs ci ifs r -> [ProjectionInfo] termProjectionInfos (TLit _) = [] +termProjectionInfos (TOpaqueLit _) = [] termProjectionInfos (TReg _) = [] termProjectionInfos (TInpCtorField _ _) = [] termProjectionInfos (TApp1 _ term) = termProjectionInfos term @@ -2905,6 +2924,7 @@ termInCtorNames :: Term rs ci ifs r -> [String] termInCtorNames (TLit _) = [] +termInCtorNames (TOpaqueLit _) = [] termInCtorNames (TReg _) = [] termInCtorNames (TInpCtorField ic _) = [icName ic] termInCtorNames (TApp1 _ t) = termInCtorNames t @@ -3094,8 +3114,9 @@ -- -- This structural check intentionally over-approximates ambiguity. It cannot -- prove semantic guard disjointness over recovered values or registers; it --- cannot compare differing 'TLit' values because 'TLit' carries no 'Eq' or --- 'Typeable' evidence; and it does not predict derived-field verification in +-- cannot compare differing literal values without the 'Eq' or 'Typeable' +-- evidence supplied by a predicate constructor; and it does not predict +-- derived-field verification in -- 'solveOutput'. It ignores tail events because replay equality-checks rather -- than inverts them. Different head constructor names are safe under the -- documented honesty law of 'wcMatch'. Literal-'PBot' guards are exempt because @@ -3311,17 +3332,27 @@ Term rs ci ifs1 r -> Term rs ci ifs2 r -> PureFragment -pureEquality (TLit a) (TLit b) - | a == b = PureKnown emptyPureGuard - | otherwise = PureUnsatisfiable -pureEquality variable (TLit literalValue) - | Just name <- pureVariable variable = +pureEquality left right + | Just a <- termLiteralValue left, + Just b <- termLiteralValue right, + a == b = + PureKnown emptyPureGuard + | Just _ <- termLiteralValue left, + Just _ <- termLiteralValue right = + PureUnsatisfiable + | Just literalValue <- termLiteralValue right, + Just name <- pureVariable left = knownComparison name PureEq literalValue (== literalValue) -pureEquality (TLit literalValue) variable - | Just name <- pureVariable variable = + | Just literalValue <- termLiteralValue left, + Just name <- pureVariable right = knownComparison name PureEq literalValue (== literalValue) -pureEquality _ _ = PureUnknown + | otherwise = PureUnknown +termLiteralValue :: Term rs ci ifs r -> Maybe r +termLiteralValue (TLit value) = Just value +termLiteralValue (TOpaqueLit value) = Just value +termLiteralValue _ = Nothing + pureOrdering :: forall rs ci ifs1 ifs2 r. (Ord r, Typeable r) => @@ -3329,26 +3360,31 @@ Term rs ci ifs1 r -> Term rs ci ifs2 r -> PureFragment -pureOrdering relation (TLit a) (TLit b) - | applyPureCmp relation a b = PureKnown emptyPureGuard - | otherwise = PureUnsatisfiable -pureOrdering relation variable (TLit literalValue) - | Just name <- pureVariable variable = +pureOrdering relation left right + | Just a <- termLiteralValue left, + Just b <- termLiteralValue right, + applyPureCmp relation a b = + PureKnown emptyPureGuard + | Just _ <- termLiteralValue left, + Just _ <- termLiteralValue right = + PureUnsatisfiable + | Just literalValue <- termLiteralValue right, + Just name <- pureVariable left = let normalized = pureRelation relation in knownComparison name normalized literalValue (\value -> applyPureRelation normalized value literalValue) -pureOrdering relation (TLit literalValue) variable - | Just name <- pureVariable variable = + | Just literalValue <- termLiteralValue left, + Just name <- pureVariable right = let normalized = flipPureRelation (pureRelation relation) in knownComparison name normalized literalValue (\value -> applyPureRelation normalized value literalValue) -pureOrdering _ _ _ = PureUnknown + | otherwise = PureUnknown knownComparison :: (Typeable r) => diff --git a/src/Keiki/Profunctor.hs b/src/Keiki/Profunctor.hs --- a/src/Keiki/Profunctor.hs +++ b/src/Keiki/Profunctor.hs @@ -762,6 +762,7 @@ Term rs ci ifs a -> Term rs (ci, c) ('("snd", c) ': ifs) a goTerm (TLit r) = TLit r + goTerm (TOpaqueLit r) = TOpaqueLit r goTerm (TReg ix) = TReg ix goTerm (TInpCtorField _ ix) = TInpCtorField cic (SIdx ix) goTerm (TApp1 h a) = TApp1 h (goTerm a) @@ -956,6 +957,7 @@ where go :: forall a. Term rs ci ifs a -> Term rs ci' ifs a go (TLit r) = TLit r + go (TOpaqueLit r) = TOpaqueLit r go (TReg ix) = TReg ix go (TInpCtorField ic ix) = TInpCtorField (contraInCtor f ic) ix go (TApp1 h a) = TApp1 h (go a) @@ -971,6 +973,7 @@ where go :: forall a. Term rs ci ifs a -> Term rs ci' ifs a go (TLit r) = TLit r + go (TOpaqueLit r) = TOpaqueLit r go (TReg ix) = TReg ix go (TInpCtorField ic ix) = TInpCtorField (contraMaybeInCtor f ic) ix go (TApp1 h a) = TApp1 h (go a) diff --git a/src/Keiki/Render/Inspector.hs b/src/Keiki/Render/Inspector.hs --- a/src/Keiki/Render/Inspector.hs +++ b/src/Keiki/Render/Inspector.hs @@ -1,7 +1,7 @@ -- | A Markdown edge-detail renderer for 'SymTransducer', a sibling to --- the Mermaid topology renderer in "Keiki.Render.Mermaid". Where --- 'Keiki.Render.Mermaid.toMermaid' shows the /shape/ of a workflow (one --- line per edge), this renderer lays out every edge in /full/: its +-- the behavioral Mermaid renderer in "Keiki.Render.Mermaid". Where +-- 'Keiki.Render.Mermaid.toMermaid' keeps executable behavior compact in +-- one transition label, this renderer expands every edge's metadata: its -- source and target states, its 0-based edge index, the input -- (command) constructor, the output (event) constructor(s), the guard -- predicate (structural and/or domain-readable), the register slots it diff --git a/src/Keiki/Render/Mermaid.hs b/src/Keiki/Render/Mermaid.hs --- a/src/Keiki/Render/Mermaid.hs +++ b/src/Keiki/Render/Mermaid.hs @@ -8,8 +8,8 @@ -- -- The rendered output is a @stateDiagram-v2@ block as 'Data.Text.Text'. -- It can be pasted into a Markdown file or Notion page; GitHub renders --- Mermaid blocks inline so PR reviewers see the topology diff alongside --- the source diff. +-- Mermaid blocks inline so PR reviewers see executable guard and update +-- semantics alongside the topology and source diff. -- -- The renderer is specialised to @phi ~ 'HsPred' rs ci@ — extracting -- the input-constructor name from an edge guard requires walking the @@ -24,13 +24,20 @@ -- for the initiative motivation. module Keiki.Render.Mermaid ( toMermaid, + toTopologyMermaid, toMermaidAlternative, toMermaidAlternativeWith, + toMermaidAlternativeWithOptions, toMermaidComposite, + toMermaidCompositeWith, toMermaidCompositeNested, + toMermaidCompositeNestedWith, toMermaidCompose3, + toMermaidCompose3With, toMermaidCompose3Nested, + toMermaidCompose3NestedWith, toMermaidFeedback1, + toMermaidFeedback1With, toMermaidAtlas, toMermaidAtlasWith, MermaidSection (..), @@ -42,11 +49,13 @@ toMermaidWithLabels, MermaidOptions (..), MermaidGuardMode (..), + MermaidUpdateMode (..), MermaidLabelLayout (..), MermaidOutputLayout (..), MermaidStateLabels (..), duplicateStateIds, defaultMermaidOptions, + topologyMermaidOptions, vertexLabel, compositeLabel, compose3Label, @@ -73,7 +82,7 @@ ) import Keiki.Generics (Append) import Keiki.Internal.Slots (indexNName) -import Keiki.Render.Pretty (prettyPred) +import Keiki.Render.Pretty (prettyPred, prettyUpdate) -- | How an edge's guard predicate is rendered into the @[g: …]@ -- segment. @@ -81,7 +90,7 @@ -- * 'MermaidGuardHidden' — no guard segment at all. -- * 'MermaidGuardStructuralSummary' — the structural constructor-tag -- walk produced by 'guardSummary', e.g. @PAnd PInCtor PEq@. This is --- the legacy rendering that the 'showGuardSummary' flag selects. +-- the compact structural alternative to readable guards. -- * 'MermaidGuardPretty' — the domain-readable rendering produced by -- 'Keiki.Render.Pretty.prettyPred', e.g. -- @(ConfirmAccount && ConfirmAccount.confirmCode == confirmCode)@. @@ -91,6 +100,19 @@ | MermaidGuardPretty deriving stock (Eq, Show) +-- | How an edge's register update is rendered. +-- +-- * 'MermaidUpdateHidden' — no update segment at all. +-- * 'MermaidUpdateWrittenSlots' — only the names of written slots, +-- retained as a compact compatibility option. +-- * 'MermaidUpdatePretty' — the complete update produced by +-- 'Keiki.Render.Pretty.prettyUpdate', including right-hand terms. +data MermaidUpdateMode + = MermaidUpdateHidden + | MermaidUpdateWrittenSlots + | MermaidUpdatePretty + deriving stock (Eq, Show) + -- | How dense edge labels are laid out. -- -- * 'MermaidLabelInline' — the current single-line @[seg; seg]@ form. @@ -116,32 +138,18 @@ | MermaidOutputCounted deriving stock (Eq, Show) --- | Rendering options for the structural edge-summary suffix. All --- fields default to the no-suffix setting in 'defaultMermaidOptions', so --- the default rendering is byte-identical to 'toMermaid'. +-- | Rendering options for edge semantics and layout. -- --- The record is extended /additively/: new fields are appended with a --- default that reproduces the existing behaviour, and existing fields --- are never removed or reordered. The legacy 'showGuardSummary' flag and --- the newer 'guardMode' field are reconciled by 'renderGuardSegment' (an --- explicit 'guardMode' wins; otherwise 'showGuardSummary' is honoured as --- the legacy spelling of 'MermaidGuardStructuralSummary'). +-- 'defaultMermaidOptions' is the readable primary policy: complete guards +-- and updates, multiline labels, and no semantic truncation. +-- 'topologyMermaidOptions' is the explicit compact compatibility policy and +-- reproduces Keiki 0.7's topology-only bytes. data MermaidOptions = MermaidOptions - { -- | When 'True', append the update's written-slot names, e.g. - -- @[w: email; confirmCode; registeredAt]@. - showWrittenSlots :: Bool, - -- | When 'True', append a structural guard summary listing the - -- guard's constructor / comparison tags, e.g. @[g: PAnd PInCtor PEq]@. - -- This is the legacy spelling of @'guardMode' = 'MermaidGuardStructuralSummary'@; - -- it is honoured only when 'guardMode' is left at its default - -- ('MermaidGuardHidden'). - showGuardSummary :: Bool, - -- | How the guard segment is rendered. When set to anything other - -- than 'MermaidGuardHidden', it takes precedence over the legacy - -- 'showGuardSummary' flag. Defaults to 'MermaidGuardHidden'. + { -- | How the guard segment is rendered. guardMode :: MermaidGuardMode, - -- | Inline (default, byte-identical) or multiline @
@ layout - -- of an edge label's segments. Defaults to 'MermaidLabelInline'. + -- | How the register-update segment is rendered. + updateMode :: MermaidUpdateMode, + -- | Inline bracketed segments or multiline @
@ layout. labelLayout :: MermaidLabelLayout, -- | When @'Just' k@ and an edge writes @n > k@ slots, show the -- first @k@ then a single @+{n-k} more@ token. 'Nothing' (the @@ -157,14 +165,26 @@ outputLayout :: MermaidOutputLayout } --- | The default: no summary suffix. @'toMermaid' t@ equals --- @'toMermaidWith' 'defaultMermaidOptions' t@. +-- | The readable primary policy used by every no-options renderer. defaultMermaidOptions :: MermaidOptions defaultMermaidOptions = MermaidOptions - { showWrittenSlots = False, - showGuardSummary = False, - guardMode = MermaidGuardHidden, + { guardMode = MermaidGuardPretty, + updateMode = MermaidUpdatePretty, + labelLayout = MermaidLabelMultiline, + maxInlineWrittenSlots = Nothing, + maxInlineGuardWidth = Nothing, + outputLayout = MermaidOutputSemicolon + } + +-- | Keiki 0.7's compact topology-only policy. This is intentionally a +-- separate named value rather than an implicit default so callers make the +-- loss of business semantics explicit. +topologyMermaidOptions :: MermaidOptions +topologyMermaidOptions = + MermaidOptions + { guardMode = MermaidGuardHidden, + updateMode = MermaidUpdateHidden, labelLayout = MermaidLabelInline, maxInlineWrittenSlots = Nothing, maxInlineGuardWidth = Nothing, @@ -178,22 +198,27 @@ -- 'show'. The output begins with @stateDiagram-v2@, followed by an -- initial-state line (@[*] --> @), one line per outgoing -- edge of every vertex, and a final-state line (@ --> [*]@) --- for every vertex where 'isFinal' returns 'True'. Edge labels follow --- the format described by 'edgeLabel'. +-- for every vertex where 'isFinal' returns 'True'. The readable default +-- adds complete update and guard segments on renderer-owned @
@ lines; +-- use 'toTopologyMermaid' for the compact 'edgeLabel' form. toMermaid :: (Enum s, Bounded s, Show s) => SymTransducer (HsPred rs ci) rs s ci co -> Text toMermaid = toMermaidWith defaultMermaidOptions --- | Like 'toMermaid', but takes 'MermaidOptions' controlling the --- structural edge-summary suffix. @'toMermaidWith' 'defaultMermaidOptions'@ --- is byte-identical to 'toMermaid'. With 'showWrittenSlots' and/or --- 'showGuardSummary' enabled, each edge label gains a compact bracketed --- suffix, e.g. @… [w: email; confirmCode; registeredAt; g: PAnd PInCtor PTop]@. --- --- Only the single-transducer path is annotated; the composite renderers --- ('toMermaidComposite' and relatives) keep the guard-free default. +-- | Render only topology using Keiki 0.7's compact label policy. Use this +-- when guards and register assignments are intentionally out of scope. +toTopologyMermaid :: + (Enum s, Bounded s, Show s) => + SymTransducer (HsPred rs ci) rs s ci co -> + Text +toTopologyMermaid = toMermaidWith topologyMermaidOptions + +-- | Like 'toMermaid', but takes the complete edge-semantics and layout +-- policy explicitly. @'toMermaidWith' 'defaultMermaidOptions'@ is +-- byte-identical to 'toMermaid'; use 'topologyMermaidOptions' for the +-- Keiki 0.7 topology-only form. toMermaidWith :: (Enum s, Bounded s, Show s) => MermaidOptions -> @@ -267,8 +292,8 @@ -- Uses the **flat cross-product** shape: each composite vertex -- @'Composite' a b@ becomes a single Mermaid identifier -- @_@. The structure is otherwise identical to --- 'toMermaid' — same initial / final / edge emission rules, same --- 'edgeLabel' format. See EP-31's Decision Log +-- 'toMermaid' — same initial / final / edge emission rules and readable +-- semantics policy. See EP-31's Decision Log -- (@docs/plans/31-mermaid-rendering-for-composite-symtransducers.md@) -- for why the flat shape was chosen over Mermaid's nested-subgraph -- syntax (Shape B in the plan). @@ -282,8 +307,23 @@ ) => SymTransducer (HsPred rs ci) rs (Composite s1 s2) ci co -> Text -toMermaidComposite = renderTopology compositeLabel +toMermaidComposite = toMermaidCompositeWith defaultMermaidOptions +-- | Options-aware variant of 'toMermaidComposite'. +toMermaidCompositeWith :: + ( Enum s1, + Bounded s1, + Show s1, + Enum s2, + Bounded s2, + Show s2 + ) => + MermaidOptions -> + SymTransducer (HsPred rs ci) rs (Composite s1 s2) ci co -> + Text +toMermaidCompositeWith opts = + renderTopologyWith opts compositeLabel compositeLabel + -- | Render a right-associative 3-deep -- @t1 \`'Keiki.Composition.compose'\` (t2 \`'Keiki.Composition.compose'\` t3)@ -- composite (vertex type @'Composite' s1 ('Composite' s2 s3)@) to a @@ -292,8 +332,8 @@ -- Each composite vertex becomes a single Mermaid identifier -- @\_\_\@ via 'compose3Label'. The -- structure is otherwise identical to 'toMermaid' / --- 'toMermaidComposite' — same initial / final / edge emission rules, --- same 'edgeLabel' format. See EP-35's plan +-- 'toMermaidComposite' — same initial / final / edge emission rules and +-- readable semantics policy. See EP-35's plan -- (@docs/plans/35-mermaid-renderer-for-right-associative-3-deep-compose-composites.md@) -- for the rationale and for the comparison against the -- nested-subgraph variant 'toMermaidCompose3Nested'. @@ -316,8 +356,32 @@ ci co -> Text -toMermaidCompose3 = renderTopology compose3Label +toMermaidCompose3 = toMermaidCompose3With defaultMermaidOptions +-- | Options-aware variant of 'toMermaidCompose3'. +toMermaidCompose3With :: + forall rs s1 s2 s3 ci co. + ( Enum s1, + Bounded s1, + Show s1, + Enum s2, + Bounded s2, + Show s2, + Enum s3, + Bounded s3, + Show s3 + ) => + MermaidOptions -> + SymTransducer + (HsPred rs ci) + rs + (Composite s1 (Composite s2 s3)) + ci + co -> + Text +toMermaidCompose3With opts = + renderTopologyWith opts compose3Label compose3Label + -- | Render a composite 'SymTransducer' (a 'Keiki.Composition.compose' -- result, vertex type @'Composite' s1 s2@) using the **nested-subgraph** -- shape (Shape B): each outer @s1@ vertex hosts a @@ -359,7 +423,23 @@ ) => SymTransducer (HsPred rs ci) rs (Composite s1 s2) ci co -> Text -toMermaidCompositeNested t = +toMermaidCompositeNested = + toMermaidCompositeNestedWith defaultMermaidOptions + +-- | Options-aware variant of 'toMermaidCompositeNested'. +toMermaidCompositeNestedWith :: + forall rs s1 s2 ci co. + ( Enum s1, + Bounded s1, + Show s1, + Enum s2, + Bounded s2, + Show s2 + ) => + MermaidOptions -> + SymTransducer (HsPred rs ci) rs (Composite s1 s2) ci co -> + Text +toMermaidCompositeNestedWith opts t = let outers = [minBound .. maxBound] :: [s1] inners = [minBound .. maxBound] :: [s2] composites = [minBound .. maxBound] :: [Composite s1 s2] @@ -390,7 +470,7 @@ <> arrow <> compositeLabel (target e) <> colon - <> edgeLabel e + <> edgeLabelWith opts e | s <- composites, e <- edgesOut t s ] @@ -448,7 +528,31 @@ ci co -> Text -toMermaidCompose3Nested t = +toMermaidCompose3Nested = + toMermaidCompose3NestedWith defaultMermaidOptions + +-- | Options-aware variant of 'toMermaidCompose3Nested'. +toMermaidCompose3NestedWith :: + forall rs s1 s2 s3 ci co. + ( Enum s1, + Bounded s1, + Show s1, + Enum s2, + Bounded s2, + Show s2, + Enum s3, + Bounded s3, + Show s3 + ) => + MermaidOptions -> + SymTransducer + (HsPred rs ci) + rs + (Composite s1 (Composite s2 s3)) + ci + co -> + Text +toMermaidCompose3NestedWith opts t = let outers = [minBound .. maxBound] :: [s1] inners = [minBound .. maxBound] :: [Composite s2 s3] composites = [minBound .. maxBound] :: [Composite s1 (Composite s2 s3)] @@ -479,7 +583,7 @@ <> arrow <> compose3Label (target e) <> colon - <> edgeLabel e + <> edgeLabelWith opts e | s <- composites, e <- edgesOut t s ] @@ -516,10 +620,11 @@ -- 'toMermaidAlternativeWith' to override (e.g. for domain-specific -- naming such as @EmailArm@ / @PingerArm@). -- --- Edge labels are the standard @\ / \@ format --- ('edgeLabel'). Because 'Keiki.Composition' lifters preserve --- @icName@ and @wcName@ verbatim, the label reads naturally even --- though the runtime input is @'Left' …@ / @'Right' …@. +-- Edge labels use the same readable guard/update policy as 'toMermaid'. +-- Because 'Keiki.Composition' lifters preserve @icName@ and @wcName@ +-- verbatim, the base label reads naturally even though the runtime input is +-- @'Left' …@ / @'Right' …@. Use 'toMermaidAlternativeWithOptions' with +-- 'topologyMermaidOptions' for the historical compact form. -- -- See @docs/plans/33-shape-aware-mermaid-renderers-for-alternative-and-feedback1-composites.md@ -- for the full design record. @@ -535,7 +640,10 @@ SymTransducer (HsPred rs2 ci2) rs2 s2 ci2 co2 -> Text toMermaidAlternative = - toMermaidAlternativeWith (T.pack "LeftArm") (T.pack "RightArm") + toMermaidAlternativeWithOptions + defaultMermaidOptions + (T.pack "LeftArm") + (T.pack "RightArm") -- | The arm-name-overridable variant of 'toMermaidAlternative'. The -- two 'Text' arguments name the left and right @state … { … }@ @@ -560,7 +668,27 @@ SymTransducer (HsPred rs1 ci1) rs1 s1 ci1 co1 -> SymTransducer (HsPred rs2 ci2) rs2 s2 ci2 co2 -> Text -toMermaidAlternativeWith leftName rightName t1 t2 = +toMermaidAlternativeWith = + toMermaidAlternativeWithOptions defaultMermaidOptions + +-- | Options-aware, arm-name-overridable variant of +-- 'toMermaidAlternative'. +toMermaidAlternativeWithOptions :: + forall rs1 rs2 s1 s2 ci1 ci2 co1 co2. + ( Enum s1, + Bounded s1, + Show s1, + Enum s2, + Bounded s2, + Show s2 + ) => + MermaidOptions -> + Text -> + Text -> + SymTransducer (HsPred rs1 ci1) rs1 s1 ci1 co1 -> + SymTransducer (HsPred rs2 ci2) rs2 s2 ci2 co2 -> + Text +toMermaidAlternativeWithOptions opts leftName rightName t1 t2 = let ind = T.pack " " ind2 = T.pack " " arrow = T.pack " --> " @@ -587,7 +715,7 @@ <> arrow <> vertexLabel (target e) <> colon - <> edgeLabel e + <> edgeLabelWith opts e | s <- [minBound .. maxBound], e <- edgesOut t s ] @@ -645,8 +773,28 @@ SymTransducer (HsPred rs1 ci) rs1 s1 ci co -> SymTransducer (HsPred rs2 co) rs2 s2 co ci -> Text -toMermaidFeedback1 t f = renderTopology feedback1Label (feedback1 t f) +toMermaidFeedback1 = toMermaidFeedback1With defaultMermaidOptions +-- | Options-aware variant of 'toMermaidFeedback1'. +toMermaidFeedback1With :: + ( Enum s1, + Bounded s1, + Show s1, + Enum s2, + Bounded s2, + Show s2, + WeakenR rs1, + WeakenR rs2, + Disjoint (Names rs2) (Names rs1), + Disjoint (Names rs1) (Names (Append rs2 rs1)) + ) => + MermaidOptions -> + SymTransducer (HsPred rs1 ci) rs1 s1 ci co -> + SymTransducer (HsPred rs2 co) rs2 s2 co ci -> + Text +toMermaidFeedback1With opts t f = + renderTopologyWith opts feedback1Label feedback1Label (feedback1 t f) + -- | The Mermaid identifier for a 'feedback1' composite vertex. -- @\_\_\@. Like -- 'compositeLabel', joined with underscores so the result still @@ -685,25 +833,9 @@ <> T.pack "_" <> T.pack (show c) --- | The shared rendering core: walk @[minBound .. maxBound]@, emit --- the @stateDiagram-v2@ header, the initial-state line, one line per --- outgoing edge, and one final-state line per vertex where --- 'isFinal' fires. The vertex-label function is the only piece that --- varies between 'toMermaid' (single transducer) and --- 'toMermaidComposite' (composite); factoring it out keeps the --- rendering logic in one place. -renderTopology :: - (Enum s, Bounded s) => - (s -> Text) -> - SymTransducer (HsPred rs ci) rs s ci co -> - Text -renderTopology label = renderTopologyWith defaultMermaidOptions label label - --- | The options-aware rendering core. Identical to 'renderTopology' --- except the per-edge line calls 'edgeLabelWith' so the structural --- summary suffix appears when 'MermaidOptions' requests it. With --- 'defaultMermaidOptions' the output is byte-identical to the original --- 'renderTopology', which is what keeps 'toMermaid' guard-free. +-- | The shared options-aware rendering core: walk +-- @[minBound .. maxBound]@ and render every transition with +-- 'edgeLabelWith'. renderTopologyWith :: (Enum s, Bounded s) => MermaidOptions -> @@ -827,7 +959,7 @@ many -> Just (render layout (Prelude.map wcN many)) where wcN :: OutTerm rs ci co -> Text - wcN (OPack _ wc _) = T.pack (wcName wc) + wcN (OPack _ wc _) = escapeSemanticText (T.pack (wcName wc)) render :: MermaidOutputLayout -> [Text] -> Text render MermaidOutputSemicolon ns | length ns == 2 = T.intercalate (T.pack "; ") ns @@ -852,16 +984,13 @@ Edge (HsPred rs ci) rs ci co s -> Text edgeLabelWithLayout layout e = - let inp = maybe (T.pack "?") id (edgeInputName e) + let inp = escapeSemanticText (maybe (T.pack "?") id (edgeInputName e)) out = maybe (T.pack "\x03B5") id (edgeOutputNameWith layout e) in inp <> T.pack " / " <> out --- | The options-aware edge label: 'edgeLabel' plus an optional --- structural suffix @[w: …; g: …]@. When neither flag is set this is --- exactly 'edgeLabel' (no trailing space, no brackets), which is what --- keeps the 'toMermaid' default byte-identical. The written-slots part --- is omitted entirely when the edge writes nothing (an empty @w:@ would --- be noise); the guard part renders the full structural tag walk. +-- | The options-aware edge label. Semantic text is escaped before this +-- function inserts its own @
@ layout separators, so user/domain text +-- cannot create extra label lines. edgeLabelWith :: MermaidOptions -> Edge (HsPred rs ci) rs ci co s -> @@ -874,15 +1003,13 @@ -- the output rendering; guard /text/ is produced by -- 'renderGuardSegment' (EP-61's chokepoint). let base = edgeLabelWithLayout (outputLayout opts) e - ws = if showWrittenSlots opts then writtenSlots u else [] - wPart = - case truncateSlots (maxInlineWrittenSlots opts) ws of - [] -> [] - xs -> [T.pack "w: " <> T.intercalate (T.pack "; ") xs] + uPart = case renderUpdateSegment opts u of + Just t -> [t] + Nothing -> [] gPart = case renderGuardSegment opts g of Just t -> [T.pack "g: " <> truncateGuard (maxInlineGuardWidth opts) t] Nothing -> [] - parts = wPart ++ gPart + parts = uPart ++ gPart in case labelLayout opts of MermaidLabelInline -> if null parts @@ -920,28 +1047,61 @@ writtenSlots (USet ix _) = [T.pack (indexNName ix)] writtenSlots (UCombine a b) = writtenSlots a ++ writtenSlots b +-- | Produce the update segment text for an edge. Pretty mode retains the +-- complete right-hand expressions; written-slot mode is the compact legacy +-- summary and may use its dedicated truncation option. +renderUpdateSegment :: MermaidOptions -> Update rs w ci -> Maybe Text +renderUpdateSegment opts u = + case updateMode opts of + MermaidUpdateHidden -> Nothing + MermaidUpdateWrittenSlots -> + case truncateSlots + (maxInlineWrittenSlots opts) + (Prelude.map escapeSemanticText (writtenSlots u)) of + [] -> Nothing + xs -> Just (T.pack "w: " <> T.intercalate (T.pack "; ") xs) + MermaidUpdatePretty -> + Just (T.pack "u: " <> escapeSemanticText (prettyUpdate u)) + -- | Produce the guard segment text for an edge, or 'Nothing' when no --- guard segment should appear. The effective mode reconciles the legacy --- 'showGuardSummary' flag with the new 'guardMode': an explicit --- 'guardMode' (anything other than 'MermaidGuardHidden') wins; otherwise --- 'showGuardSummary' is honoured as the legacy spelling of --- 'MermaidGuardStructuralSummary'. --- --- This is the single chokepoint for guard /text/ production. A sibling --- renderer that changes how edge-label /segments are laid out/ (inline --- vs. multiline) wraps the assembly of segments and leaves this --- function's text untouched. +-- guard segment should appear. Semantic text is escaped here, before label +-- layout is assembled. renderGuardSegment :: MermaidOptions -> HsPred rs ci -> Maybe Text renderGuardSegment opts g = - case effectiveMode of + escapeSemanticText <$> case guardMode opts of MermaidGuardHidden -> Nothing MermaidGuardStructuralSummary -> Just (guardSummary g) MermaidGuardPretty -> Just (prettyPred g) + +-- | Escape domain-derived label text exactly once into a visible, +-- non-structural alphabet. The documentation backend decodes XML entities +-- before parsing Mermaid and also turns both @
@ spellings and literal +-- @\\n@ into line breaks, so entity encoding alone cannot isolate semantic +-- text. Full-width punctuation keeps the value recognizable while preventing +-- parser control. XML entities retain punctuation that the backend can safely +-- decode, full-width angle brackets keep break-tag-like input inert, and +-- control pictures make raw line endings visible rather than structural. +-- Renderer-owned ASCII @
@ is inserted only after this pass. The known +-- opaque marker @@ is encoded as entities because it cannot be a break +-- tag and should remain visually exact. +escapeSemanticText :: Text -> Text +escapeSemanticText = + T.intercalate (T.pack "<lit>") + . Prelude.map (T.concatMap escapeChar) + . T.splitOn (T.pack "") where - effectiveMode - | guardMode opts /= MermaidGuardHidden = guardMode opts - | showGuardSummary opts = MermaidGuardStructuralSummary - | otherwise = MermaidGuardHidden + escapeChar '\r' = T.pack "\x240D" + escapeChar '\n' = T.pack "\x240A" + escapeChar '\\' = T.pack "\xFF3C" + escapeChar '\'' = T.pack "'" + escapeChar '"' = T.pack """ + escapeChar '&' = T.pack "&" + escapeChar '<' = T.pack "\xFF1C" + escapeChar '>' = T.pack "\xFF1E" + escapeChar '|' = T.pack "|" + escapeChar '{' = T.pack "{" + escapeChar '}' = T.pack "}" + escapeChar c = T.singleton c -- | A structural, total summary of a guard predicate: its constructor -- tags in left-to-right (prefix) order, with 'PCmp' carrying its 'Cmp' diff --git a/src/Keiki/Render/Pretty.hs b/src/Keiki/Render/Pretty.hs --- a/src/Keiki/Render/Pretty.hs +++ b/src/Keiki/Render/Pretty.hs @@ -2,14 +2,14 @@ -- | Pure, domain-readable pretty-printer for keiki's predicate, term, -- and update syntax trees ('HsPred', 'Term', 'Update'). Produces --- 'Data.Text.Text'. No solver, no IO. Shared by the Mermaid topology +-- 'Data.Text.Text'. No solver, no IO. Shared by the Mermaid behavioral -- renderer ('Keiki.Render.Mermaid') and the sibling edge-inspector / -- multiline-label renderers. -- --- Two things are provably unprintable and are marked, not dropped: --- applied opaque Haskell functions render as @(...)@; literal --- values render as @@ (a 'TLit' carries an unconstrained type --- with no 'Show'). +-- Two things are deliberately marked rather than invented: applied opaque +-- Haskell functions render as @(...)@, and explicit display-opaque literal +-- values render as @@. Ordinary 'TLit' values use their retained 'Show' +-- evidence. module Keiki.Render.Pretty ( indexName, prettyTerm, @@ -44,11 +44,12 @@ -- | Render a 'Term' as domain-readable 'Text'. Register reads render by -- slot name, input-field reads as @ctor.field@, arithmetic structurally --- with @+ - *@. Opaque applied functions render @(...)@; literal --- values render @@ (a 'TLit' carries an unconstrained type with no --- 'Show'). +-- with @+ - *@. Opaque applied functions render @(...)@. Ordinary +-- literals use their value's 'Show' instance; explicit opaque literals render +-- as @@. prettyTerm :: Term rs ci ifs r -> Text -prettyTerm (TLit _) = T.pack "" +prettyTerm (TLit value) = T.pack (show value) +prettyTerm (TOpaqueLit _) = T.pack "" prettyTerm (TReg ix) = T.pack (indexName ix) prettyTerm (TInpCtorField ic ix) = T.pack (icName ic) <> T.pack "." <> T.pack (indexName ix) diff --git a/src/Keiki/Symbolic.hs b/src/Keiki/Symbolic.hs --- a/src/Keiki/Symbolic.hs +++ b/src/Keiki/Symbolic.hs @@ -576,7 +576,7 @@ -- | Translate a 'Term rs ci r' to an SBV expression of the carrier's -- representation type. Requires 'Sym' evidence for @r@. -- --- The translation is /structural/ for 'TLit', 'TReg', +-- The translation is /structural/ for 'TLit', 'TOpaqueLit', 'TReg', -- 'TInpCtorField', and (since EP-43) 'TArith': a 'TArith' over a type -- whose 'SymRep' is SBV-numeric (a 'discoverSymNum' hit) emits a real -- @+@ \/ @-@ \/ @*@ over the translated operands, so a guard over a @@ -624,6 +624,7 @@ Term rs ci ifs r -> SBV.Symbolic (SBV.SBV (SymRep r)) translateTermSym _env (TLit r) = pure (symLit r) +translateTermSym _env (TOpaqueLit r) = pure (symLit r) translateTermSym env (TReg ix) = memoFree @r env (RegVar (indexName ix)) translateTermSym env (TInpCtorField ic ix) = @@ -1045,6 +1046,7 @@ Term rs ci ifs r -> [TranslationReportEvent] termReportEvents _root _context (TLit _) = [] +termReportEvents _root _context (TOpaqueLit _) = [] termReportEvents _root _context (TReg ix) = [DirectOwnerReadEvent (registerBaseDescriptor @r ix)] termReportEvents _root _context (TInpCtorField ic ix) = diff --git a/test/Keiki/CompositionAlignmentSpec.hs b/test/Keiki/CompositionAlignmentSpec.hs --- a/test/Keiki/CompositionAlignmentSpec.hs +++ b/test/Keiki/CompositionAlignmentSpec.hs @@ -1,12 +1,14 @@ module Keiki.CompositionAlignmentSpec (spec) where import Data.Proxy (Proxy (..)) +import Data.Text qualified as T import Keiki.Composition import Keiki.Core import Keiki.FieldProjSpec qualified as FieldProj import Keiki.Fixtures.ComposeStateful import Keiki.Fixtures.CounterPipeline import Keiki.Profunctor (rmapCo) +import Keiki.Render.Pretty (prettyPred, prettyTerm) import Test.Hspec type Payload1 = '[ '("payload", Int)] @@ -218,6 +220,7 @@ inputTerm = TInpCtorField projectionSourceCtor #doc passThrough = projectionSource inputTerm literalOwner = projectionSource (TLit matchingDoc) + opaqueOwner = projectionSource (opaqueLit matchingDoc) computedOwner = projectionSource (TApp1 id inputTerm) it "preserves a stable input-field owner through checked composition" $ do @@ -226,15 +229,39 @@ Left warnings -> expectationFailure ("stable projection warned: " <> show warnings) Right pipeline -> opaqueGuardWarnings pipeline `shouldBe` [] - it "constant-folds a literal owner without introducing opacity" $ do - let pipeline = compose literalOwner projectionSink - opaqueGuardWarnings pipeline `shouldBe` [] - case stepEither - pipeline - (initial pipeline, initialRegs pipeline) - (ProjectionSourceCmd (FieldProj.DocInfo "ignored" "" [])) of - Left failure -> expectationFailure ("literal-folded pipeline failed: " <> show failure) - Right _ -> pure () + it "constant-folds a literal owner with display opacity but exact semantics" $ do + case composeChecked literalOwner projectionSink of + Left warnings -> expectationFailure ("literal fold failed checked composition: " <> show warnings) + Right pipeline -> do + opaqueGuardWarnings pipeline `shouldBe` [] + case edgesOut pipeline (initial pipeline) of + [edge] -> + prettyPred (guard edge) + `shouldSatisfy` T.isInfixOf (T.pack "") + _ -> expectationFailure "literal-folded pipeline no longer has one edge" + case stepEither + pipeline + (initial pipeline, initialRegs pipeline) + (ProjectionSourceCmd (FieldProj.DocInfo "ignored" "" [])) of + Left failure -> expectationFailure ("literal-folded pipeline failed: " <> show failure) + Right _ -> pure () + + it "preserves literal display evidence through positional substitution" $ do + let midRead = TInpCtorField projectionMidCtor #doc + case edgesOut literalOwner (initial literalOwner) of + [Edge {output = [out]}] -> do + let substituted = + substTerm @'[] @'[] midRead out :: + Term '[] ProjectionSourceCmd ProjectionSourceFields FieldProj.DocInfo + prettyTerm substituted `shouldBe` T.pack (show matchingDoc) + _ -> expectationFailure "readable literal source no longer has one output" + case edgesOut opaqueOwner (initial opaqueOwner) of + [Edge {output = [out]}] -> do + let substituted = + substTerm @'[] @'[] midRead out :: + Term '[] ProjectionSourceCmd ProjectionSourceFields FieldProj.DocInfo + prettyTerm substituted `shouldBe` T.pack "" + _ -> expectationFailure "opaque literal source no longer has one output" it "keeps raw composition forward-correct but rejects a computed owner at the checked boundary" $ do let pipeline = compose computedOwner projectionSink diff --git a/test/Keiki/CoreSpec.hs b/test/Keiki/CoreSpec.hs --- a/test/Keiki/CoreSpec.hs +++ b/test/Keiki/CoreSpec.hs @@ -8,6 +8,142 @@ -- | A two-constructor input symbol used by the 'TInpCtorField' tests. data TinyCmd = TinyFoo Int Int | TinyBar Int deriving (Eq, Show) +-- EP-84 guarantee-ledger fixtures. 'NoShowValue' proves the term language can +-- still carry a value with no display dictionary. 'ThrowingShowValue' carries +-- a dictionary whose method is bottom, so execution and replay tests detect +-- any accidental renderer observation on a semantic path. +data NoShowValue = NoShowValue Int deriving (Eq) + +data NoShowEvent = NoShowEvent NoShowValue deriving (Eq) + +data ThrowingShowValue = ThrowingShowValue Int deriving (Eq) + +instance Show ThrowingShowValue where + show _ = error "EP-84: semantic execution forced Show" + +data LiteralLedgerEvent = LiteralLedgerEvent ThrowingShowValue deriving (Eq) + +data LiteralLedgerVertex = LiteralLedgerStart | LiteralLedgerDone + deriving stock (Eq, Ord, Show, Enum, Bounded) + +type LiteralLedgerRegs = '[ '("payload", ThrowingShowValue)] + +literalLedgerInCtor :: InCtor () '[] +literalLedgerInCtor = + InCtor + { icName = "LiteralLedgerCommand", + icMatch = \() -> Just RNil, + icBuild = \RNil -> () + } + +literalLedgerWireCtor :: WireCtor LiteralLedgerEvent (ThrowingShowValue, ()) +literalLedgerWireCtor = + WireCtor + { wcName = "LiteralLedgerEvent", + wcMatch = \(LiteralLedgerEvent value) -> Just (value, ()), + wcBuild = \(value, ()) -> LiteralLedgerEvent value + } + +literalLedgerValue :: ThrowingShowValue +literalLedgerValue = ThrowingShowValue 41 + +literalLedgerTransducerWith :: + Term LiteralLedgerRegs () '[] ThrowingShowValue -> + SymTransducer + (HsPred LiteralLedgerRegs ()) + LiteralLedgerRegs + LiteralLedgerVertex + () + LiteralLedgerEvent +literalLedgerTransducerWith literalTerm = + SymTransducer + { edgesOut = \case + LiteralLedgerStart -> + [ Edge + { guard = PEq literalTerm literalTerm, + update = + USet + (#payload :: IndexN "payload" LiteralLedgerRegs ThrowingShowValue) + literalTerm, + output = + [ pack + literalLedgerInCtor + literalLedgerWireCtor + (OFCons literalTerm OFNil) + ], + target = LiteralLedgerDone, + mode = Live + } + ] + LiteralLedgerDone -> [], + initial = LiteralLedgerStart, + initialRegs = + RCons (Proxy @"payload") (ThrowingShowValue 0) RNil, + isFinal = (== LiteralLedgerDone) + } + +literalLedgerTransducer :: + SymTransducer + (HsPred LiteralLedgerRegs ()) + LiteralLedgerRegs + LiteralLedgerVertex + () + LiteralLedgerEvent +literalLedgerTransducer = literalLedgerTransducerWith (lit literalLedgerValue) + +opaqueLiteralLedgerTransducer :: + SymTransducer + (HsPred LiteralLedgerRegs ()) + LiteralLedgerRegs + LiteralLedgerVertex + () + LiteralLedgerEvent +opaqueLiteralLedgerTransducer = + literalLedgerTransducerWith (opaqueLit literalLedgerValue) + +type NoShowRegs = '[ '("payload", NoShowValue)] + +noShowWireCtor :: WireCtor NoShowEvent (NoShowValue, ()) +noShowWireCtor = + WireCtor + { wcName = "NoShowEvent", + wcMatch = \(NoShowEvent value) -> Just (value, ()), + wcBuild = \(value, ()) -> NoShowEvent value + } + +noShowTransducer :: + SymTransducer + (HsPred NoShowRegs ()) + NoShowRegs + LiteralLedgerVertex + () + NoShowEvent +noShowTransducer = + SymTransducer + { edgesOut = \case + LiteralLedgerStart -> + [ Edge + { guard = PTop, + update = + USet + (#payload :: IndexN "payload" NoShowRegs NoShowValue) + (opaqueLit (NoShowValue 7)), + output = + [ pack + literalLedgerInCtor + noShowWireCtor + (OFCons (opaqueLit (NoShowValue 7)) OFNil) + ], + target = LiteralLedgerDone, + mode = Live + } + ] + LiteralLedgerDone -> [], + initial = LiteralLedgerStart, + initialRegs = RCons (Proxy @"payload") (NoShowValue 0) RNil, + isFinal = (== LiteralLedgerDone) + } + type SnapshotRegs = '[ '("x", Int), '("y", Int) @@ -85,6 +221,88 @@ spec :: Spec spec = do + describe "EP-84 literal semantic guarantee ledger" $ do + it "evaluates a display-opaque value with no Show instance" $ + case evalTerm (opaqueLit (NoShowValue 7)) RNil () of + NoShowValue 7 -> pure () + _ -> expectationFailure "literal evaluation changed the no-Show value" + + it "updates, emits, and replays a value with no Show instance" $ do + case step + noShowTransducer + (initial noShowTransducer, initialRegs noShowTransducer) + () of + Just + ( LiteralLedgerDone, + RCons _ (NoShowValue 7) RNil, + [NoShowEvent (NoShowValue 7)] + ) -> pure () + _ -> expectationFailure "no-Show literal step changed its value" + case reconstitute noShowTransducer [NoShowEvent (NoShowValue 7)] of + Just (LiteralLedgerDone, RCons _ (NoShowValue 7) RNil) -> pure () + _ -> expectationFailure "no-Show literal replay changed its value" + + it "evaluates, compares, updates, and emits without forcing Show" $ do + evalPred + (PEq (lit literalLedgerValue) (lit literalLedgerValue) :: HsPred '[] ()) + RNil + () + `shouldBe` True + case step + literalLedgerTransducer + (initial literalLedgerTransducer, initialRegs literalLedgerTransducer) + () of + Just + ( LiteralLedgerDone, + RCons _ (ThrowingShowValue 41) RNil, + [LiteralLedgerEvent (ThrowingShowValue 41)] + ) -> pure () + _ -> expectationFailure "literal step changed state, registers, or output" + + it "solves and replays the emitted literal without forcing Show" $ do + let observed = LiteralLedgerEvent literalLedgerValue + case edgesOut literalLedgerTransducer LiteralLedgerStart of + [Edge {output = [out]}] -> solveOutput out (initialRegs literalLedgerTransducer) observed `shouldBe` Just () + _ -> expectationFailure "literal ledger fixture no longer has one output" + case reconstitute literalLedgerTransducer [observed] of + Just + ( LiteralLedgerDone, + RCons _ (ThrowingShowValue 41) RNil + ) -> pure () + _ -> expectationFailure "literal replay changed state or registers" + + it "retains the clean validation classification" $ + validateTransducer defaultValidationOptions literalLedgerTransducer + `shouldBe` [] + + it "gives readable and display-opaque literals identical step and replay results" $ do + let readableStep = + step + literalLedgerTransducer + (initial literalLedgerTransducer, initialRegs literalLedgerTransducer) + () + opaqueStep = + step + opaqueLiteralLedgerTransducer + (initial opaqueLiteralLedgerTransducer, initialRegs opaqueLiteralLedgerTransducer) + () + case (readableStep, opaqueStep) of + ( Just (LiteralLedgerDone, RCons _ (ThrowingShowValue 41) RNil, [LiteralLedgerEvent (ThrowingShowValue 41)]), + Just (LiteralLedgerDone, RCons _ (ThrowingShowValue 41) RNil, [LiteralLedgerEvent (ThrowingShowValue 41)]) + ) -> pure () + _ -> expectationFailure "readable and opaque literal steps diverged" + let observed = [LiteralLedgerEvent literalLedgerValue] + case ( reconstitute literalLedgerTransducer observed, + reconstitute opaqueLiteralLedgerTransducer observed + ) of + ( Just (LiteralLedgerDone, RCons _ (ThrowingShowValue 41) RNil), + Just (LiteralLedgerDone, RCons _ (ThrowingShowValue 41) RNil) + ) -> pure () + _ -> expectationFailure "readable and opaque literal replay diverged" + + it "does not classify display opacity as an opaque semantic guard" $ + opaqueGuardWarnings opaqueLiteralLedgerTransducer `shouldBe` [] + describe "evalTerm" $ do it "evaluates TLit" $ evalTerm (TLit (42 :: Int)) RNil () `shouldBe` 42 diff --git a/test/Keiki/Render/MermaidSpec.hs b/test/Keiki/Render/MermaidSpec.hs --- a/test/Keiki/Render/MermaidSpec.hs +++ b/test/Keiki/Render/MermaidSpec.hs @@ -30,6 +30,7 @@ -- nested) and the synthetic three-toy fixture. module Keiki.Render.MermaidSpec (spec) where +import Data.Proxy (Proxy (..)) import Data.Text (Text) import Data.Text qualified as T import Keiki.Composition (Composite, compose) @@ -41,13 +42,16 @@ EdgeMode (..), HsPred (..), InCtor (..), + IndexN (..), OutFields (..), RegFile (..), SymTransducer (..), Update (..), WireCtor (..), + opaqueLit, pack, ) +import Keiki.Fixtures.CounterPipeline (stageB) import Keiki.Fixtures.EmailDelivery (emailDelivery) import Keiki.Fixtures.UserRegistration (Vertex (..), userReg) import Keiki.Render.Mermaid @@ -60,57 +64,112 @@ MermaidSection (..), MermaidSectionKind (..), MermaidStateLabels (..), + MermaidUpdateMode (..), defaultMermaidAtlasOptions, defaultMermaidOptions, duplicateStateIds, toMermaid, toMermaidAlternative, + toMermaidAlternativeWithOptions, toMermaidAtlas, toMermaidAtlasWith, toMermaidCompose3, toMermaidCompose3Nested, + toMermaidCompose3NestedWith, + toMermaidCompose3With, toMermaidComposite, toMermaidCompositeNested, + toMermaidCompositeNestedWith, + toMermaidCompositeWith, toMermaidFeedback1, + toMermaidFeedback1With, toMermaidWith, toMermaidWithLabels, + toTopologyMermaid, + topologyMermaidOptions, vertexLabel, ) +import Keiki.Render.Validate + ( MermaidValidationOptions (..), + defaultMermaidValidationOptions, + validateMermaidDiagram, + ) import Test.Hspec spec :: Spec spec = do - describe "toMermaid (single SymTransducer)" $ + describe "toMermaid (readable single SymTransducer)" $ it "renders userReg to the canonical stateDiagram-v2 block" $ - toMermaid userReg `shouldBe` userRegCanonical + toMermaid userReg `shouldBe` userRegReadableCanonical - describe "toMermaidComposite (composite SymTransducer)" $ - it "renders the AlertSource ⨾ EmailDelivery pipeline" $ + describe "toMermaid (complete business expressions, EP-84)" $ + it "shows update right-hand expressions and ordinary literal values" $ do + let diagram = toMermaid stageB + diagram `shouldSatisfy` T.isInfixOf (T.pack "u: regB := (regB + MsgB.payload)") + diagram `shouldSatisfy` T.isInfixOf (T.pack "g: (MsgB && regB ＞= 0)") + diagram `shouldNotSatisfy` T.isInfixOf (T.pack "") + + describe "toMermaid (explicit display opacity, EP-84)" $ + it "shows opaqueLit as while topology mode hides the expression" $ do + toMermaid opaqueValue + `shouldSatisfy` T.isInfixOf (T.pack "u: secret := <lit>") + toTopologyMermaid opaqueValue + `shouldNotSatisfy` T.isInfixOf (T.pack "lit") + + describe "toTopologyMermaid (0.7 compatibility)" $ + it "renders userReg to the prior topology-only block exactly" $ + toTopologyMermaid userReg `shouldBe` userRegCanonical + + describe "toMermaidComposite (composite SymTransducer)" $ do + it "renders readable semantics for the AlertSource ⨾ EmailDelivery pipeline" $ toMermaidComposite (compose alertSource emailDelivery) + `shouldSatisfy` hasReadableSemantics + it "reproduces the 0.7 topology with explicit options" $ + toMermaidCompositeWith topologyMermaidOptions (compose alertSource emailDelivery) `shouldBe` alertEmailCompositeCanonical - describe "toMermaidCompositeNested (composite SymTransducer)" $ - it "renders the AlertSource ⨾ EmailDelivery pipeline in nested form" $ + describe "toMermaidCompositeNested (composite SymTransducer)" $ do + it "renders readable semantics in nested form" $ toMermaidCompositeNested (compose alertSource emailDelivery) + `shouldSatisfy` hasReadableSemantics + it "reproduces the 0.7 nested topology with explicit options" $ + toMermaidCompositeNestedWith topologyMermaidOptions (compose alertSource emailDelivery) `shouldBe` alertEmailCompositeNestedCanonical - describe "toMermaidAlternative (alternative composite)" $ - it "renders alternative emailDelivery pinger as parallel arms" $ + describe "toMermaidAlternative (alternative composite)" $ do + it "renders readable semantics for both parallel arms" $ toMermaidAlternative emailDelivery pinger + `shouldSatisfy` hasReadableSemantics + it "reproduces the 0.7 parallel-arm topology with explicit options" $ + toMermaidAlternativeWithOptions + topologyMermaidOptions + (T.pack "LeftArm") + (T.pack "RightArm") + emailDelivery + pinger `shouldBe` emailPingerAltCanonical - describe "toMermaidFeedback1 (feedback1 composite)" $ - it "renders feedback1 toggleAgg togglePolicy as flat 3-deep cross-product" $ + describe "toMermaidFeedback1 (feedback1 composite)" $ do + it "renders readable feedback semantics" $ toMermaidFeedback1 toggleAgg togglePolicy + `shouldSatisfy` hasReadableSemantics + it "reproduces the 0.7 flat feedback topology with explicit options" $ + toMermaidFeedback1With topologyMermaidOptions toggleAgg togglePolicy `shouldBe` toggleFeedback1Canonical - describe "toMermaidCompose3 (right-associative 3-deep compose)" $ - it "renders the toy1 ⨾ (toy2 ⨾ toy3) flat block" $ - toMermaidCompose3 toy3deep `shouldBe` toy3deepFlatCanonical + describe "toMermaidCompose3 (right-associative 3-deep compose)" $ do + it "renders readable semantics in the flat block" $ + toMermaidCompose3 toy3deep `shouldSatisfy` hasReadableSemantics + it "reproduces the 0.7 flat topology with explicit options" $ + toMermaidCompose3With topologyMermaidOptions toy3deep + `shouldBe` toy3deepFlatCanonical - describe "toMermaidCompose3Nested (right-associative 3-deep compose)" $ - it "renders the toy1 ⨾ (toy2 ⨾ toy3) one-level nested block" $ - toMermaidCompose3Nested toy3deep `shouldBe` toy3deepNestedCanonical + describe "toMermaidCompose3Nested (right-associative 3-deep compose)" $ do + it "renders readable semantics in the one-level nested block" $ + toMermaidCompose3Nested toy3deep `shouldSatisfy` hasReadableSemantics + it "reproduces the 0.7 nested topology with explicit options" $ + toMermaidCompose3NestedWith topologyMermaidOptions toy3deep + `shouldBe` toy3deepNestedCanonical -- EP-50 M3: the default must stay byte-identical to today (the -- guard-free pedagogy in deriving-lifecycle-transitions.md depends on @@ -124,23 +183,27 @@ describe "toMermaidWith (annotated edge summary)" $ it "renders userReg with written-slot and guard-summary suffixes" $ toMermaidWith - (defaultMermaidOptions {showWrittenSlots = True, showGuardSummary = True}) + ( topologyMermaidOptions + { updateMode = MermaidUpdateWrittenSlots, + guardMode = MermaidGuardStructuralSummary + } + ) userReg `shouldBe` userRegAnnotatedCanonical describe "toMermaidWith (MermaidGuardPretty, EP-61)" $ it "renders userReg guards in domain-readable form" $ toMermaidWith - (defaultMermaidOptions {guardMode = MermaidGuardPretty}) + (topologyMermaidOptions {guardMode = MermaidGuardPretty}) userReg `shouldBe` userRegPrettyGuardCanonical describe "toMermaidWith (multiline label layout, EP-63)" $ it "renders userReg labels with
-separated segments" $ toMermaidWith - ( defaultMermaidOptions - { showWrittenSlots = True, - showGuardSummary = True, + ( topologyMermaidOptions + { updateMode = MermaidUpdateWrittenSlots, + guardMode = MermaidGuardStructuralSummary, labelLayout = MermaidLabelMultiline } ) @@ -150,8 +213,8 @@ describe "toMermaidWith (written-slot truncation, EP-63)" $ it "truncates a long written-slot list with +N more" $ toMermaidWith - ( defaultMermaidOptions - { showWrittenSlots = True, + ( topologyMermaidOptions + { updateMode = MermaidUpdateWrittenSlots, maxInlineWrittenSlots = Just 2 } ) @@ -161,8 +224,8 @@ describe "toMermaidWith (guard-width truncation, EP-63)" $ it "truncates an over-long guard segment with an ellipsis" $ toMermaidWith - ( defaultMermaidOptions - { showGuardSummary = True, + ( topologyMermaidOptions + { guardMode = MermaidGuardStructuralSummary, maxInlineGuardWidth = Just 10 } ) @@ -171,25 +234,36 @@ describe "toMermaidWith (MermaidOutputSemicolon default, EP-63)" $ it "renders multiEvt with the length-based default output layout" $ - toMermaid multiEvt `shouldBe` multiEvtSemicolonCanonical + toTopologyMermaid multiEvt `shouldBe` multiEvtSemicolonCanonical describe "toMermaidWith (MermaidOutputMultiline, EP-63)" $ it "renders every multi-event edge one event per line" $ toMermaidWith - (defaultMermaidOptions {outputLayout = MermaidOutputMultiline}) + (topologyMermaidOptions {outputLayout = MermaidOutputMultiline}) multiEvt `shouldBe` multiEvtMultilineCanonical describe "toMermaidWith (MermaidOutputCounted, EP-63)" $ it "renders multi-event edges as an N events count" $ toMermaidWith - (defaultMermaidOptions {outputLayout = MermaidOutputCounted}) + (topologyMermaidOptions {outputLayout = MermaidOutputCounted}) multiEvt `shouldBe` multiEvtCountedCanonical + describe "semantic-label escaping (EP-84)" $ do + it "escapes every backend control spelling before inserting layout" $ + toMermaid specialChars `shouldBe` specialCharsCanonical + it "preserves the diagram and transition line counts" $ do + length (T.lines (toMermaid specialChars)) `shouldBe` 4 + T.count (T.pack " --> ") (toMermaid specialChars) `shouldBe` 3 + T.count (T.pack "
") (toMermaid specialChars) `shouldBe` 2 + it "passes suspicious-character validation without disabling that check" $ + validateMermaidDiagram semanticValidationOptions (toMermaid specialChars) + `shouldBe` [] + describe "toMermaidWithLabels (stable ASCII ids, spaced display labels, EP-64)" $ it "renders userReg with friendly labels and stable ids" $ - toMermaidWithLabels defaultMermaidOptions userRegLabels userReg + toMermaidWithLabels topologyMermaidOptions userRegLabels userReg `shouldBe` userRegLabeledCanonical describe "toMermaidWithLabels (id == display is byte-identical, EP-64)" $ @@ -210,8 +284,8 @@ describe "toMermaidAtlas (multi-diagram document)" $ it "assembles two labelled diagrams into one document" $ toMermaidAtlas - [ (T.pack "User registration", toMermaid userReg), - (T.pack "Alert \x2A3E Email", toMermaidComposite (compose alertSource emailDelivery)) + [ (T.pack "User registration", toTopologyMermaid userReg), + (T.pack "Alert \x2A3E Email", toMermaidCompositeWith topologyMermaidOptions (compose alertSource emailDelivery)) ] `shouldBe` atlasCanonical @@ -228,19 +302,38 @@ (T.pack "incident-command") (T.pack "Incident Command") AggregateDiagram - (toMermaid userReg), + (toTopologyMermaid userReg), MermaidSection (T.pack "dispatch") (T.pack "Dispatch") ProcessManagerDiagram - (toMermaidComposite (compose alertSource emailDelivery)) + (toMermaidCompositeWith topologyMermaidOptions (compose alertSource emailDelivery)) ] `shouldBe` typedAtlasCanonical --- | The canonical Mermaid block for @userReg@, mirrored verbatim from --- the aggregate's diagram in @docs/guide/diagrams/user-registration.md@. --- Stored inline (not in an external fixture file) so a formatting change --- requires touching this file alongside the producer change. +hasReadableSemantics :: Text -> Bool +hasReadableSemantics diagram = + T.pack "
u: " `T.isInfixOf` diagram + && T.pack "
g: " `T.isInfixOf` diagram + +-- | The readable-primary golden. Unlike the Keiki 0.7 topology golden below, +-- every transition includes the complete update and guard expression. +userRegReadableCanonical :: Text +userRegReadableCanonical = + T.intercalate + (T.pack "\n") + [ "stateDiagram-v2", + " [*] --> PotentialCustomer", + " PotentialCustomer --> RequiresConfirmation : StartRegistration / RegistrationStarted; ConfirmationEmailSent
u: registeredAt := StartRegistration.at, confirmCode := StartRegistration.confirmCode, email := StartRegistration.email, (keep)
g: StartRegistration", + " RequiresConfirmation --> Confirmed : ConfirmAccount / AccountConfirmed
u: confirmedAt := ConfirmAccount.at, (keep)
g: (ConfirmAccount && ConfirmAccount.confirmCode == confirmCode)", + " RequiresConfirmation --> RequiresConfirmation : ResendConfirmation / ConfirmationResent
u: registeredAt := ResendConfirmation.at, confirmCode := ResendConfirmation.code, (keep)
g: ResendConfirmation", + " RequiresConfirmation --> Deleted : FulfillGDPRRequest / AccountDeleted
u: deletedAt := FulfillGDPRRequest.at, (keep)
g: FulfillGDPRRequest", + " Confirmed --> Deleted : FulfillGDPRRequest / AccountDeleted
u: deletedAt := FulfillGDPRRequest.at, (keep)
g: FulfillGDPRRequest", + " Deleted --> [*]" + ] + +-- | The Keiki 0.7 topology-only block for @userReg@, retained as the +-- compatibility golden for 'toTopologyMermaid'. userRegCanonical :: Text userRegCanonical = unlinesNoTrail @@ -259,8 +352,8 @@ where unlinesNoTrail = T.intercalate (T.pack "\n") --- | EP-50: the canonical block for @userReg@ rendered with both summary --- flags on (@MermaidOptions True True@). Differs from 'userRegCanonical' +-- | EP-50: the canonical block for @userReg@ rendered with written-slot +-- and structural-guard modes. Differs from 'userRegCanonical' -- only by the bracketed @[w: …; g: …]@ suffixes. Captured verbatim from -- the renderer (the slot order is the @UCombine@ nesting order, and each -- guard is the actual 'HsPred' shape @onCmd@ produced — a bare 'PInCtor' @@ -280,8 +373,8 @@ ] -- | EP-61: the canonical block for @userReg@ rendered with --- @guardMode = MermaidGuardPretty@ and 'showWrittenSlots' left at its --- default 'False', so each label carries only a domain-readable +-- @guardMode = MermaidGuardPretty@ and updates hidden, so each label carries +-- only a domain-readable -- @[g: …]@ segment. Differs from 'userRegAnnotatedCanonical' by -- rendering real names — @ConfirmAccount@, @confirmCode@ — instead of -- the structural constructor-tag walk (@PAnd PInCtor PEq@). Captured @@ -293,14 +386,14 @@ [ "stateDiagram-v2", " [*] --> PotentialCustomer", " PotentialCustomer --> RequiresConfirmation : StartRegistration / RegistrationStarted; ConfirmationEmailSent [g: StartRegistration]", - " RequiresConfirmation --> Confirmed : ConfirmAccount / AccountConfirmed [g: (ConfirmAccount && ConfirmAccount.confirmCode == confirmCode)]", + " RequiresConfirmation --> Confirmed : ConfirmAccount / AccountConfirmed [g: (ConfirmAccount && ConfirmAccount.confirmCode == confirmCode)]", " RequiresConfirmation --> RequiresConfirmation : ResendConfirmation / ConfirmationResent [g: ResendConfirmation]", " RequiresConfirmation --> Deleted : FulfillGDPRRequest / AccountDeleted [g: FulfillGDPRRequest]", " Confirmed --> Deleted : FulfillGDPRRequest / AccountDeleted [g: FulfillGDPRRequest]", " Deleted --> [*]" ] --- | EP-63: @userReg@ rendered with both summary flags on and +-- | EP-63: @userReg@ rendered with written-slot and structural-guard modes and -- @labelLayout = MermaidLabelMultiline@. Same per-edge content as -- 'userRegAnnotatedCanonical', but the bracketed inline suffix is replaced -- by @
@-separated segments: the @command / event@ base on the first @@ -322,7 +415,7 @@ " Deleted --> [*]" ] --- | EP-63: @userReg@ rendered with @showWrittenSlots = True@ and +-- | EP-63: @userReg@ rendered with @updateMode = MermaidUpdateWrittenSlots@ and -- @maxInlineWrittenSlots = Just 2@. The only edge writing more than two -- slots is @StartRegistration@ (three slots), which truncates to the first -- two followed by a single @+1 more@ token; every other edge writes two or @@ -341,7 +434,7 @@ " Deleted --> [*]" ] --- | EP-63: @userReg@ rendered with @showGuardSummary = True@ and +-- | EP-63: @userReg@ rendered with structural guard summaries and -- @maxInlineGuardWidth = Just 10@. The only guard whose structural text -- exceeds ten characters is @ConfirmAccount@'s @PAnd PInCtor PEq@ (length -- 16), truncated to the first ten characters plus the ellipsis @…@. The @@ -749,6 +842,124 @@ " T1A_T2A_T3A --> T1B_T2B_T3B : Tick / Tick", " T1B_T2B_T3B --> [*]" ] + +-- * Semantic-label escaping fixture (EP-84) ------------------------- + +type SecretRegs = '[ '("secret", Int)] + +data SecretCmd = SetSecret + +data SecretEvt = SecretSet + +data SecretState = SecretState + deriving (Eq, Show, Enum, Bounded) + +secretInCtor :: InCtor SecretCmd '[] +secretInCtor = + InCtor + { icName = "SetSecret", + icMatch = \SetSecret -> Just RNil, + icBuild = \RNil -> SetSecret + } + +secretWireCtor :: WireCtor SecretEvt () +secretWireCtor = + WireCtor + { wcName = "SecretSet", + wcMatch = \SecretSet -> Just (), + wcBuild = \() -> SecretSet + } + +opaqueValue :: + SymTransducer + (HsPred SecretRegs SecretCmd) + SecretRegs + SecretState + SecretCmd + SecretEvt +opaqueValue = + SymTransducer + { edgesOut = \SecretState -> + [ Edge + { guard = PInCtor secretInCtor, + update = USet IZ (opaqueLit (7 :: Int)), + output = [pack secretInCtor secretWireCtor OFNil], + target = SecretState, + mode = Live + } + ], + initial = SecretState, + initialRegs = RCons (Proxy @"secret") 0 RNil, + isFinal = const True + } + +data SpecialCmd = SpecialCmd + +data SpecialEvt = SpecialEvt + +data SpecialState = SpecialStart | SpecialDone + deriving (Eq, Show, Enum, Bounded) + +specialName :: String +specialName = + "Command \"quote\" 'apostrophe'


<br> | {value}\r\n\\n" + +specialInCtor :: InCtor SpecialCmd '[] +specialInCtor = + InCtor + { icName = specialName, + icMatch = \SpecialCmd -> Just RNil, + icBuild = \RNil -> SpecialCmd + } + +specialWireCtor :: WireCtor SpecialEvt () +specialWireCtor = + WireCtor + { wcName = "Event", + wcMatch = \SpecialEvt -> Just (), + wcBuild = \() -> SpecialEvt + } + +specialChars :: + SymTransducer + (HsPred '[] SpecialCmd) + '[] + SpecialState + SpecialCmd + SpecialEvt +specialChars = + SymTransducer + { edgesOut = \case + SpecialStart -> + [ Edge + { guard = PInCtor specialInCtor, + update = UKeep, + output = [pack specialInCtor specialWireCtor OFNil], + target = SpecialDone, + mode = Live + } + ] + SpecialDone -> [], + initial = SpecialStart, + initialRegs = RNil, + isFinal = (== SpecialDone) + } + +specialCharsCanonical :: Text +specialCharsCanonical = + T.intercalate + (T.pack "\n") + [ "stateDiagram-v2", + " [*] --> SpecialStart", + " SpecialStart --> SpecialDone : Command "quote" 'apostrophe' ＜br＞ ＜br/＞ ＜br /＞ &lt;br&gt; | {value}␍␊＼n / Event
u: (keep)
g: Command "quote" 'apostrophe' ＜br＞ ＜br/＞ ＜br /＞ &lt;br&gt; | {value}␍␊＼n", + " SpecialDone --> [*]" + ] + +semanticValidationOptions :: MermaidValidationOptions +semanticValidationOptions = + defaultMermaidValidationOptions + { maxLabelLength = Nothing + } -- * Multi-event output fixture (EP-63 M2) ----------------------------- diff --git a/test/Keiki/Render/PrettySpec.hs b/test/Keiki/Render/PrettySpec.hs --- a/test/Keiki/Render/PrettySpec.hs +++ b/test/Keiki/Render/PrettySpec.hs @@ -15,6 +15,7 @@ Term (..), Update (..), inpProj, + opaqueLit, regProj, ) import Keiki.FieldProjSpec qualified as FieldProj @@ -66,8 +67,11 @@ it "renders an input-field read as ctor.field" $ prettyTerm (TInpCtorField inCtorDeposit amountIx :: Term Regs Cmd DepFields Int) `shouldBe` T.pack "Deposit.amount" - it "renders a literal opaquely as " $ + it "renders an ordinary literal from its value" $ prettyTerm (TLit (42 :: Int) :: Term Regs Cmd '[] Int) + `shouldBe` T.pack "42" + it "renders an explicit display-opaque literal as " $ + prettyTerm (opaqueLit (42 :: Int) :: Term Regs Cmd '[] Int) `shouldBe` T.pack "" it "renders TApp1 as (arg)" $ prettyTerm (TApp1 (+ (1 :: Int)) (TReg balanceIx) :: Term Regs Cmd '[] Int) @@ -105,9 +109,9 @@ it "renders PInCtor as the constructor name" $ prettyPred (PInCtor inCtorDeposit :: HsPred Regs Cmd) `shouldBe` T.pack "Deposit" - it "renders PEq structurally with on the literal side" $ + it "renders PEq structurally with the literal value" $ prettyPred (PEq (TReg balanceIx) (TLit (0 :: Int)) :: HsPred Regs Cmd) - `shouldBe` T.pack "balance == " + `shouldBe` T.pack "balance == 0" it "renders each PCmp direction" $ do prettyPred (PCmp CmpLt (TReg balanceIx) (TReg limitIx) :: HsPred Regs Cmd) `shouldBe` T.pack "balance < limit" @@ -127,14 +131,14 @@ ) :: HsPred Regs Cmd ) - `shouldBe` T.pack "(Deposit && (balance >= || !(limit == )))" + `shouldBe` T.pack "(Deposit && (balance >= 0 || !(limit == 0)))" describe "prettyUpdate" $ do it "renders UKeep" $ prettyUpdate (UKeep :: Update Regs '[] Cmd) `shouldBe` T.pack "(keep)" it "renders USet as slot := term" $ prettyUpdate (USet balanceN (TLit (0 :: Int)) :: Update Regs '["balance"] Cmd) - `shouldBe` T.pack "balance := " + `shouldBe` T.pack "balance := 0" it "renders UCombine comma-separated" $ prettyUpdate ( UCombine @@ -142,4 +146,4 @@ (USet balanceN (TLit (1 :: Int))) :: Update Regs '["balance", "balance"] Cmd ) - `shouldBe` T.pack "balance := limit, balance := " + `shouldBe` T.pack "balance := limit, balance := 1" diff --git a/test/Keiki/SymbolicSpec.hs b/test/Keiki/SymbolicSpec.hs --- a/test/Keiki/SymbolicSpec.hs +++ b/test/Keiki/SymbolicSpec.hs @@ -1,5 +1,6 @@ module Keiki.SymbolicSpec (spec) where +import Control.Monad (forM_) import Data.Int (Int32, Int64) import Data.Kind (Type) import Data.Maybe (isJust, isNothing) @@ -476,6 +477,48 @@ predicateTranslationExact unsatisfiable `shouldBe` True verifyPredicate satisfiable `shouldReturn` VerifiedSatisfiable verifyPredicate unsatisfiable `shouldReturn` VerifiedUnsatisfiable + + it "keeps every readable/opaque literal equality pairing exact" $ do + let readable value = lit value :: Term '[] () '[] Bool + hidden value = opaqueLit value :: Term '[] () '[] Bool + equalPairs = + [ (readable True, readable True), + (readable True, hidden True), + (hidden True, readable True), + (hidden True, hidden True) + ] + unequalPairs = + [ (readable True, readable False), + (readable True, hidden False), + (hidden True, readable False), + (hidden True, hidden False) + ] + forM_ equalPairs $ \(left, right) -> do + let predicate = PEq left right :: HsPred '[] () + predicateTranslationReport predicate `shouldBe` ExactTranslation + verifyPredicate predicate `shouldReturn` VerifiedSatisfiable + detail <- verifyPredicateDetailed predicate + detail `shouldSatisfy` \case + PredicateSatisfiable ExactTranslation [] -> True + _ -> False + forM_ unequalPairs $ \(left, right) -> do + let predicate = PEq left right :: HsPred '[] () + predicateTranslationReport predicate `shouldBe` ExactTranslation + verifyPredicate predicate `shouldReturn` VerifiedUnsatisfiable + + it "keeps every readable/opaque literal ordering pairing exact" $ do + let readable value = lit value :: Term '[] () '[] Int + hidden value = opaqueLit value :: Term '[] () '[] Int + pairings = + [ (readable 3, readable 5), + (readable 3, hidden 5), + (hidden 3, readable 5), + (hidden 3, hidden 5) + ] + forM_ pairings $ \(left, right) -> do + let predicate = PCmp CmpLt left right :: HsPred '[] () + predicateTranslationReport predicate `shouldBe` ExactTranslation + verifyPredicate predicate `shouldReturn` VerifiedSatisfiable it "verifies supported structural arithmetic" $ do let arithmetic = diff --git a/test/Keiki/ValidationSpec.hs b/test/Keiki/ValidationSpec.hs --- a/test/Keiki/ValidationSpec.hs +++ b/test/Keiki/ValidationSpec.hs @@ -1,5 +1,6 @@ module Keiki.ValidationSpec (spec) where +import Control.Monad (forM_) import Data.List (isInfixOf) import Data.Proxy (Proxy (..)) import Data.Word (Word8) @@ -675,6 +676,23 @@ it "uses a mentioned non-integral literal as a concrete witness" $ checkTransitionDeterminismPure boolLiteralWitnessT `shouldSatisfy` (not . null) + + it "treats every readable/opaque literal pairing identically" $ do + let readable value = lit value :: Term OverlapRegs Cmd '[] Int + hidden value = opaqueLit value :: Term OverlapRegs Cmd '[] Int + pairings = + [ (readable 3, readable 5), + (readable 3, hidden 5), + (hidden 3, readable 5), + (hidden 3, hidden 5) + ] + forM_ pairings $ \(left, right) -> do + checkTransitionDeterminismPure + (overlapFixture (PEq left left) (PEq right right)) + `shouldSatisfy` (not . null) + checkTransitionDeterminismPure + (overlapFixture (PCmp CmpLt left right) PTop) + `shouldSatisfy` (not . null) it "finds an interior overlap in Natural's zero-bounded domain" $ do let purePairs = map warningPair (checkTransitionDeterminismPure naturalInteriorOverlapT)