Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Lightmarey`FormulaTransformEngine`
CompileFormulaObligationDischarger  |
|
| | ||||
▪
证明义务消解器匹配义务类型，并在假设或上下文文本中查找声明的证据；它不会证明任意命题。
▪
编译过程只接受声明式数据。可执行构造、未知编译原语、未绑定模板槽和不一致的方向都会被拒绝。
▪
成功时返回包含 Status -> "Compiled"、Kind -> "FormulaObligationDischarger"、Name、规范化字段和 Raw 的关联。无效输入返回 Status -> "Failure"、FailureType -> "InvalidRuleJSON" 以及 Issues 列表。
▪
参数:
json | Association | 描述符字段如下表所示。 |
▪
描述符字段:
name | String，必需 | 注册表名称。 | |
matchesObligation | 字符串或列表，必需 | 本消解器识别的证明义务类型。 | |
evidence | 对象或列表 | 结构化证据规则。 | |
source | any | assumptions | context | 证据规则检查的文本来源。 | |
containsAny / containsAll | 字符串或列表 | 不区分大小写的证据片段。 | |
obligationKinds | 字符串或列表 | 可选的逐规则义务过滤器。 | |
evidenceText | 字符串或列表 | 旧式证据片段。 |
范例
(1)
基本范例
(1)
In[1]:=
Needs["Lightmarey`FormulaTransformEngine`"]
编译并注册一个最小有效描述符：
In[2]:=
 | CompileFormulaObligationDischarger |
Out[2]=
StatusCompiled,KindFormulaObligationDischarger,HeadCompiledFormulaObligationDischarger,RegistryKindObligationDischarger,NameExampleDischarger,MatchesObligation{RealValued},EvidenceText{},EvidenceRules{LabelEvidenceRule1,Sourcecontext,ObligationKinds{},ContainsAny{real-valued},ContainsAll{}},RawkindObligationDischarger,nameExampleDischarger,matchesObligation{RealValued},evidence{sourcecontext,containsAny{real-valued}}
无效描述符返回结构化诊断，而不会执行任意代码：
In[1]:=
| CompileFormulaObligationDischarger |
Out[1]=
StatusFailure,KindFormulaTransform,FailureTypeInvalidRuleJSON,MessageObligation discharger JSON was rejected.,Issues{name must be a non-empty string.},Discharger
""