Lightmarey/FormulaTransformEngine

Lightmarey`FormulaTransformEngine`

PlanFormulaTransformParts

PlanFormulaTransformParts[rule,opts][expr]
	查找与目标匹配的部分，并可对每个候选预览规则。

PlanFormulaTransformParts["",opts][expr]
	仅列出匹配部分，不生成规则预览。

更多信息和选项

▪

Parameters 必须包含 targetRelation 或 targetPattern。前者选择关系的左端，后者按 Wolfram Language 模式解析。

▪

成功结果包含 CandidateCount 和 Candidates。每个候选包含 Part、PartPath、Expression 和 ExpressionInputForm；规则预览还包含 Applicable 和 PlanPreview。

▪

参数:

rule	String	已编译规则或结构变换的名称。
opts	Options	下表列出的任意通用变换选项。
expr	Expression 或 HoldComplete	从中选择目标部分并执行变换的完整表达式。

▪

可以使用下列选项：

"Direction"	"Auto"	请求的方向：Auto、Upper、Lower、TwoSided 或 Equal。
"Part"	"Whole"	表达式选择器：Whole、Auto、整数路径、列表路径或 Named:name。
"Parameters"	<\|\|>	规则参数、targetRelation/targetPattern，以及可选的 namedParts。
"Assumptions"	True	检查变换条件时使用的符号假设。
"AssumptionsText"	""	证明义务消解器使用的自然语言假设证据。
"Context"	<\|\|>	传给引擎的结构化分析上下文。
"ContextText"	""	证明义务消解器使用的自然语言上下文证据。
"State"	FormulaTransformState	包含轨迹和延迟证明义务的初始状态关联。

范例

(1)

基本范例

(1)

In[1]:=

Needs["Lightmarey`FormulaTransformEngine`"]

查找与目标模式匹配的所有部分：

In[2]:=

parts=

PlanFormulaTransformParts

["","Parameters"Association["targetPattern""Inactive[Times][__]"]][a×b+c×d];parts["Candidates"]

Out[2]=

{Part{1},PartPath{1},Expressiona×b,ExpressionInputFormInactive[Times][a, b],Part{2},PartPath{2},Expressionc×d,ExpressionInputFormInactive[Times][c, d]}

缺少目标说明时会明确报告：

In[1]:=

PlanFormulaTransformParts

[""][a+b]

Out[1]=

StatusFailure,KindFormulaTransform,FailureTypeInvalidRequest,Messageplan_parts requires parameters.targetRelation or parameters.targetPattern.,Trace{StepPlanPartsParseHeld,Time2026-07-26T21:30:36,Rule},StateHeadFormulaTransformState,Obligations{},Trace{}

targetRelation 选择与其左端等价的表达式：

In[2]:=

parts=

PlanFormulaTransformParts

["","Parameters"Association["targetRelation""a<=c"]][a+b];parts["CandidateCount"]

Out[2]=

参见

PlanFormulaTransform

▪

ApplyFormulaTransform