Penrose 语言新特性全解析：对称谓词、谓词别名、匹配元数据与内联比较运算符

开发工具数据可视化【免费下载链接】penroseCreate beautiful diagrams just by typing notation in plain text.项目地址https://gitcode.com/gh_mirrors/pe/penrose点击查看免费下载导读本文基于 Penrose 核心仓库中 packages/docs-site/blog/new-language-features.md 这篇官方博客系统讲解 Penrose 在 2022 年引入的四项语言级改进二元对称谓词Binary Symmetric Predicates、谓词别名Predicate Aliasing、匹配元数据Match Metadata即match_id/match_total以及内联比较运算符、、。这四项特性共同作用在 Domain、Substance、Style 三种语言之上让 Style 程序对 Substance 的匹配更加自然、灵活且富有表达力。读完本文你将理解每个特性解决的真实痛点、语法用法、约束条件以及它们在packages/core编译器与解析器中的底层实现原理可直接用于编写更简洁、可复用的 Penrose 程序。背景三个语言文件如何协同工作在进入具体特性之前先明确 Penrose 的编程模型一份 Penrose 图由三个纯文本文件组成——Domain.domain声明类型如Atom、谓词如Bond(Atom, Atom)与函数相当于词汇表Substance.substance用 Domain 中声明的类型与谓词描述有什么相当于事实清单Style.style通过forall ... where ... { ... }选择器块匹配 Substance 中的对象与关系并决定画成什么样。Style 块与 Substance 之间的**匹配matching**过程是整个渲染管线的核心where子句中的每个谓词都会被拿去与 Substance 中的谓词实例比对并生成一个把 Style 变量映射到 Substance 变量的映射mapping。本文介绍的四项特性本质上都是在优化这个匹配过程及其产物相关的语法解析与匹配实现可在 packages/core/src/parser/Style.ne 与 packages/core/src/compiler/Style.ts 中查看。一、二元对称谓词symmetric为什么需要它Bond 的水分子困境数学关系往往是对称的若集合A等于集合B则B也等于A。但早期的 Penrose 并没有对称的概念Style 作者必须靠复制代码来模拟对称性。这个问题最初由 Keenan Crane 在 GitHub issue 中提出用的是一个非常直观的例子。考虑如下 Domaintype Atom type Hydrogen : Atom type Oxygen : Atom predicate Bond(Atom, Atom)在该 Domain 下一个水分子可以有多种合法的 Substance 写法例如-- version 1 Hydrogen H1, H2 Oxygen O Bond(O, H1) Bond(O, H2)-- version 2 Hydrogen H1, H2 Oxygen O Bond(H1, O) Bond(O, H2)现在Style 作者想强制水分子中两条键的夹角为 104.5 度于是写出forall Oxygen o; Hydrogen h1; Hydrogen h2 where Bond(o, h1); Bond(o, h2) { -- enforce that the angle between the two bonds are 104.5 degrees }问题来了这个 Style 块只匹配version 1。因为按照当时的匹配逻辑Bond(o, h1)无法匹配Bond(H1, O)——o的声明类型是Oxygen而H1的声明类型是Hydrogenh1的声明类型是Hydrogen而O的类型是Oxygen类型对不上匹配失败。可人类直觉上Bond(H1, O)与Bond(O, H1)是同一个化学事实。Penrose 并不理解这一点于是为了匹配version 2作者只能复制整段 Style 代码。解决方案symmetric关键字解决方案是在 Domain 语言中为二元谓词增加symmetric关键字实现于对应的 PR 中symmetric predicate Bond(Atom, Atom)声明之后当 Style 的谓词Bond(o, h1)去匹配 Substance 的Bond(H1, O)时匹配器会利用对称性同时考虑Bond(O, H1)从而匹配成功。被标注symmetric的谓词必须满足两条硬性要求否则 Penrose 会直接报错必须是二元谓词即恰好两个参数目前不支持更多参数。两个声明参数类型必须完全相同。因为对称谓词的两个参数被视为可互换所以可以写symmetric predicate Bond(Atom, Atom)但不能写symmetric predicate Bond(Atom, Oxygen)。当然在 Substance 或 Style 中实际应用该谓词时仍然可以使用子类型如Hydrogen : Atom。这两条校验在编译期完成packages/core/src/compiler/Domain.ts中的checkSymmetricArgs会检查参数个数是否为 2否则报symmetricArgLengthMismatch并逐一比对参数类型否则报symmetricTypeMismatch。对应的测试用例可以在 packages/core/src/compiler/Domain.test.ts 中找到其中覆盖了正常声明参数类型不匹配含子类型场景和参数个数不为 2三种情况。实现原理先直配再翻转第一版实现的核心算法如下将 Style 谓词StyName(...StyArgs)与 Substance 谓词SubName(...SubArgs)匹配if (StyName ! SubName) return fail // match_raw(StyArgs, SubArgs) 要求精确匹配且考虑参数顺序 mapping_raw match_raw(StyArgs, SubArgs) // 若匹配成功直接返回该映射 if success: return mapping_raw // 翻转 Substance 侧的参数顺序 SubArgsSym [SubArgs[1], SubArgs[0]] // 用翻转后的参数再尝试一次 mapping_sym match_raw(StyArgs, SubArgsSym) if success: return mapping_sym return fail即先尝试匹配原始 Substance 谓词Bond(H1, O)仅在失败时才尝试翻转参数后的Bond(O, H1)。在 packages/core/src/compiler/Style.ts 的matchStyApplyToSubApply中可以看到这一逻辑的落地它先按原顺序调用matchStyArgsToSubArgs得到rSubstOriginal随后检查varEnv.predicateDecls.get(subRel.name.value)?.symmetric若为真则构造flippedStyArgs [styRel.args[1], styRel.args[0]]再匹配一次得到rSubstSymmetric最后把两批替换结果合并返回。一次教训为什么必须同时尝试两种版本先直配、失败再翻转的算法有一个隐蔽缺陷。假设Equal是Set之间的对称谓词Substance 程序为Set A, B, C Equal(B, A) Equal(B, C)Style 程序为forall Set x, y, z where Equal(x, y); Equal(y, z) { -- some code }按上述失败才翻转的算法这个 Style 块匹配失败。原因在于Equal(x, y)已经能直接匹配Equal(B, A)匹配器便认定变量映射为{x - B, y - A}根本不会去考虑Equal(B, A)的对称版本而在这个映射下y - A导致Equal(y, z)无论是否利用对称性都无法匹配Equal(B, C)A与B不是同一个Set变量。但如果匹配器主动考虑Equal(B, A)的对称版本就能得到另一种兼容的映射{x - A, y - B}它与Equal(y, z)匹配Equal(B, C)产生的{y - B, z - C}完全相容从而匹配成功。这个 bug 于 2022 年 10 月被发现并记录修复方案是要求匹配器始终同时尝试对称谓词的两种参数版本而不是仅在直配失败时才翻转if (StyName ! SubName) return fail toReturn [] mapping_raw match_raw(StyArgs, SubArgs) if success: toReturn.push(mapping_raw) // 翻转 Substance 侧的参数 SubArgsSym [SubArgs[1], SubArgs[0]] mapping_sym match_raw(StyArgs, SubArgsSym) if success: toReturn.push(mapping_sym) if toReturn.length 0: return fail return toReturn注意虽然博客中的伪代码翻转的是 Substance 参数当前仓库实现packages/core/src/compiler/Style.ts在rSubstOriginal之外翻转的是Style 侧参数效果等价——关键在于两种顺序都要尝试。这一行为有专门测试验证symmetric predicate should match 1Bond(H, O)配合where Bond(o, h)应能匹配见 packages/core/src/compiler/Style.test.tssymmetric predicate should match 2Equal(A, B); Equal(A, C)配合where Equal(x, y); Equal(y, z)应能匹配见 packages/core/src/compiler/Style.test.ts这正是修复前会失败的场景此外还有no double matching, symmetric等测试确保对称匹配不会产生重复的冗余匹配。二、谓词别名Predicate Aliasing为什么需要它一条键的线属于谁假设我们想在两个Atom之间存在Bond谓词时为它们画一条连线。直觉上可以写forall Atom a; Atom b where Bond(a, b) { ???.bondLine Line { -- ... } }问题在于???该填什么bondLine这条线应该属于谁填a或b都不合理——Bond的连线不属于它的任一参数而是被a和b共享的不填即bondLine Line { ... }也不行——匿名赋值无法在块外被引用后续就无法再覆盖它的其他属性。自然而言bondLine应该属于谓词Bond(a, b)本身最好能写出类似Bond(a, b).bondLine的语法。解决方案where Bond(a, b) as bond谓词别名的想法最早于 2021 年 7 月由 Helena Yang 提出但未合并2022 年 7 月由本文作者Yiliang Liang重新实现并合入。它允许 Style 作者写成forall Atom a; Atom b where Bond(a, b) as bond { -- ^^^^ -- 现在 bond 在该 Style 块内指代 Bond(a, b) bond.bondLine Line { -- ... } }这样一来当该 Style 块匹配到 Substance 谓词Bond(X, Y)时bondLine就归属于bond Bond(X, Y)。如果另一个 Style 块也匹配到了同一个Bond(X, Y)它同样可以通过自己块内定义的别名访问这个bondLine——不同块对同一个谓词实例的别名是互通的因为它们指向同一个谓词实例名。实现原理把别名加进映射回顾匹配过程Style 块匹配 Substance 程序会得到一组映射例如Bond(a, b)匹配Bond(X, Y)得到{a - X, b - Y}。当存在谓词别名时匹配器会在生成映射时追加一个额外条目把别名映射到被匹配谓词的特殊谓词实例名{ a - X, b - Y, bond - Bond_X_Y }其中Bond_X_Y就是被匹配的Bond(X, Y)的谓词实例名。因为映射中存在bond - Bond_X_Y后续就可以合法地引用它的子属性例如把bond.bondLine赋值为一个形状。这段逻辑同样实现在 packages/core/src/compiler/Style.ts 的matchStyApplyToSubApply中当styRel.alias存在时对每一份替换结果追加aliasName - { tag: SubstanceVar, name: getSubPredAliasInstanceName(subRel) }。可见别名本质上被处理成一个特殊的 Substance 变量从而自然地融入了既有的变量映射体系。三、匹配元数据match_id与match_total为什么需要它刻度线的数量问题一个 Style 块可能被匹配多次例如forall MyType t对每个MyType实例各匹配一次。2022 年 1 月Keenan Crane 提出每个 Style 块需要访问两类信息匹配的总次数即 Style 块的基数例如画一组刻度线时需要根据总刻度数确定间距当前这一次匹配的序号即序数例如决定在一个被标记的角度上画几条刻度线。解决方案两个保留变量Penrose 为每个 Style 块引入了两个保留变量match_total记录该 Style 块总共被匹配的次数match_id记录当前这次匹配的1 起始序号。来看一个最小示例type MyType的 Domain、四个实例的 Substance以及forall MyType t { ... }的 Style画布配置省略type MyTypeMyType T1, T2, T3, T4-- canvas specifications omitted forall MyType t { // 可以在此使用 match_id 和 match_total }由于该 Style 块匹配了四次块内match_total等于 4而match_id依当前匹配的不同取 1、2、3 或 4 之一。实现原理向块体注入两条伪造赋值实现方式非常巧妙对每个 Style 块编译器在块体最前面注入两个人工 AST 节点仿佛它们原本就是 Style 程序的一部分一个节点相当于match_total 该块匹配的总次数另一个节点相当于match_id 当前匹配的序数。随后按常规流程处理整个 Style 块。于是match_total和match_id被当作块内局部变量正确赋值后即可在后续语句中使用。对应实现位于 packages/core/src/compiler/Style.ts 的processBlock先用makeFakeIntPathAssign(match_id, substIndex 1)与makeFakeIntPathAssign(match_total, substs.length)构造两条伪路径赋值substs就是该块的全部匹配替换列表再用augmentedStatements把这两条语句拼接在原始块语句之前统一交给processStmt处理。测试用例可参考 packages/core/src/compiler/Style.test.ts其中验证了match_id的取值恰好为[1, 2, 3]等行为。四、内联比较运算符、、语法糖从函数调用到运算符前三个特性解决的是匹配问题内联比较运算符解决的则是书写体验问题。Penrose 为、、提供了语法糖分别对应函数调用lessThan、equal、greaterThan。例如ensure circle1.r circle2.r会被等价地视为ensure lessThan(circle1.r, circle2.r)语法与实现比较运算被翻译成函数调用实现分为两步。第一步修改约束constraint与目标objective声明的文法ensure/encourageconstr :: ensure body staged layout obj :: encourage body staged layout body :: identifier ( expr_list ) // 函数调用 | expr op expr // 内联比较 op :: // Equal | // Less Than | // Greater Than即body现在可以是函数调用或内联比较两种形式之一。第二步在 Style 编译器中处理约束与目标时遇到函数调用按原有流程处理遇到内联比较则把它当作函数调用来处理——根据运算符选择对应的函数名lessThan、greaterThan或equal并把左右两个操作数作为该函数的参数。文法层面的证据在 packages/core/src/parser/Style.necomparison_op规则依次匹配、、并生成ComparisonOp节点obj_constr_body除了原有的identifier ( expr_list )函数调用分支还新增了expr _ comparison_op _ expr分支产出InlineComparison节点。编译层面的翻译则在 packages/core/src/compiler/Style.ts 的extractObjConstrBody中完成mapInlineOpToFunctionName把、、分别映射为lessThan、equal、greaterThan并将arg1、arg2作为参数列表返回。注意事项为什么没有和原本还计划支持和但最终没有实现原因有二Penrose 系统中不存在与这两个运算符对应的函数从优化器的角度看与被同等对待与被同等对待——引入它们并不会带来新的语义价值。因此当前可用的内联比较运算符只有、、三个。结语packages/docs-site/blog/new-language-features.md这篇博客记录的这四项特性看似基础却实实在在提升了 Penrose 三种语言的自然度、灵活度与表达力symmetric谓词让 Style 匹配理解数学关系的对称性消除了大量重复代码谓词别名让形状可以归属于关系本身而不再被迫挂在某个参数名下match_id/match_total把匹配过程的基数与序数暴露给 Style 作者支撑了更精细的排布逻辑内联比较运算符让约束与目标语句更接近数学直觉写起来更顺手。如果需要动手验证可以直接在 packages/examples 的示例集中寻找使用这些特性的.domain/.substance/.style组合并参考 packages/core/src/compiler/Style.test.ts 与 packages/core/src/compiler/Domain.test.ts 中的测试用例理解每种语法的精确行为与边界约束。赞分享开发工具数据可视化【免费下载链接】penroseCreate beautiful diagrams just by typing notation in plain text.项目地址https://gitcode.com/gh_mirrors/pe/penrose点击查看免费下载相关推荐Penrose 谓词声明Predicate Declarations完全指南语法、对称谓词与引擎实现Penrose 谓词声明Predicate Declarations完全指南语法、对称谓词与引擎实现 本指南以 Penrose 仓库中 Predicate开发工具数据可视化Cassandra 条件与谓词缺陷类别深度解析38 个比较、守卫与谓词 Bug 模式及源码对照Cassandra 条件与谓词缺陷类别深度解析38 个比较、守卫与谓词 Bug 模式及源码对照 本文以 Apache Cassandra 仓库内 condit数据库分布式数据库大数据后端Penrose Substance 语句语法全解对象声明、谓词应用、函数/构造器调用与标签语句Penrose Substance 语句语法全解对象声明、谓词应用、函数/构造器调用与标签语句 Penrose本仓库 gh_mirrors/pe/penro开发工具数据可视化创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考