The Principia Machina/TPC-PY/tpc form.py: Difference between revisions
TPC-PY source tpc_form.py (0.2.1), SHA-256 21ed78428c06b4a4; conformed TPS 0.4.0; PROPOSED, not declared (TPC-PY 0.2.0) |
m 1 revision imported |
||
(No difference)
| |||
Latest revision as of 02:11, 30 September 2026
# -*- coding: utf-8 -*-
"""
TPC-PY --- the declared form of a LAW, a BOUNDARY and a SIGNATURE
(TPC step 2, increment 8; D108.1, phase E at Option 1 of every slot
S1-S11 of tpm_increment_8_phase_F 0.1.0, selected 2026-09-24)
=================================================================
Standard library only; Python 3.8+; Windows/Linux. Spec: tpm_kernel_tests
0.2.0 section 12, tpm_increment_8_0_1_0 (the phase E report).
THE FORM IS OPTIONAL (S1). A LAW may carry EQUATION and a BOUNDARY may
carry CONDITION beside its prose; a SIGNATURE may carry FORM and
IMAGE_FORM beside IMAGE (S8). Absent means no form: the entry passes every
check it passed at increment 7, and the check the form would have made
MECHANICAL stays INSPECTION by H-DECL, reported as such, never silently
passed (kernel tests 12.3).
THE GRAMMAR (S2, S3, S4, S6), closed, ASCII, one canonical spelling (S10):
equation := expr "=" expr (EQUATION)
form := expr ( "=" expr )? (FORM, IMAGE_FORM)
predicate := disj (CONDITION)
disj := conj ( "or" conj )* left-associative
conj := neg ( "and" neg )* left-associative
neg := "not" neg | "(" predicate ")" | expr cmp expr
cmp := "<" | "<=" | ">" | ">=" | "=" | "!="
expr := term ( ("+" | "-") term )* left-associative
term := unary ( ("*" | "/") unary )* left-associative
unary := "-" power | power -a^2 is -(a^2)
power := atom ( "^" exponent )? a^2^3 is refused: parenthesize
exponent := integer | "(" "-"? integer ")" | "(" "-"? integer "/" integer ")"
atom := identifier | literal | "(" expr ")" | function "(" expr ")"
| "D" "(" identifier "," identifier ( "," integer )? ")"
function := exp | ln | sin | cos | tan | abs | sqrt
identifier := [A-Za-z_][A-Za-z0-9_]* (a REFS, OVER or inventory name)
literal := digits ("." digits)? ([eE] [-+]? digits{1,4})? no sign
integer := digits a positive one after "," in D
Whitespace (space, TAB, LF) between tokens is ignored. No implicit
multiplication, no unit inside an expression, no chained comparison, no
"--". The parser is LL(1) with one token of lookahead; a parenthesis in a
CONDITION opens a predicate when a comparison operator or a keyword sits
at depth one inside it, else an expression. Both residences assert the
GRAMMAR WITNESSES below when loaded, and their count.
BOUNDS (D186.1; tpc_form 0.2.0): an integer (an exponent, a rational
exponent's p and q, D's order) is at most 4 digits as written, a leading
zero counted, as a DIMENSION exponent is (9999); a form is at most 4096
code points of its canonical text (LF line endings, then NFC; whitespace
counted) and at most 64 parentheses deep, every "(" opening a level (a
function's, D's and a parenthesized exponent's included) and a ")" with none
open closing none. Order: the canonical text; its length; its depth, in one
linear scan; then the tokens and the grammar, an integer's digits checked
where the grammar reads that integer, before it is converted. A form beyond
a bound is refused for the first bound it exceeds and is read no further:
"the form is longer than 4096 code points"; "more than 64 nested parentheses
at N"; "an integer of more than 4 digits at N", N a 1-based code point
position. A written integer therefore fits a native integer in both
residences.
COMPUTED EXPONENTS (S14; tpc_form 0.2.0): T1, dimension-free: for every
identifier and every D under nested powers and square roots, the exponent the
form composes - the product of the enclosing exponents from the innermost, a
sqrt counting 1/2 and abs 1, while exp, ln, sin, cos and tan yield a pure
number and end the product - has, in lowest terms, a numerator and a
denominator of at most 9999 at every power and root, checked as the parser
completes each: "a computed exponent beyond 9999 at N", N the position of that
^ or of the function name. The dimension walk (T4, T6, form_dimension) and the
KIND walk (T3, eval_form): every exponent read from a DIMENSION or a KIND and
every exponent a step computes (*, /, ^, D) lies within -9999..9999, as
tpc_units requires of a UNIT's DIMENSION; else "an exponent is out of range"
or "a kind exponent is out of range". Each operand is then within 9999, every
intermediate below 10^8, so no residence overflows. A zero base under a
negative rational exponent is refused as under a negative integer one.
CANONICAL SPELLING: no whitespace except one space around "and"/"or" and
after "not"; literals in canon_decimal form ("0.50" -> "5e-1", "100" ->
"1e2"); integer exponents without leading zeros; D(x,t,1) written D(x,t);
the author's operand order and parenthesization kept; redundant enclosing
parentheses dropped at every delimiter-bounded slot (the whole, each side
of "=" or a comparison, a function argument). Only spelling is canonical:
"x*2" and "2*x" are different statements (S10). The canonical form parses
back to the same tree.
DIMENSIONS (S4): + and - need equal DIMENSIONs and yield it; * adds
exponents, / subtracts; ^ multiplies by an integer, or by p/q when every
resulting exponent is an integer (sqrt(L2) is L1; sqrt(L1) is refused);
exp, ln, sin, cos, tan need a dimensionless argument and yield 1; abs
keeps its argument's; sqrt halves; a literal is dimensionless, except
that THE LITERAL ZERO HAS EVERY DIMENSION (so "D(z,t,2)=0" and "x!=0"
are homogeneous; a delegated reading, see the note); = and every
comparison need equal DIMENSIONs; D(x,s,n) yields dim(x) less n times
dim(s), in integer exponents, the result within -9999..9999 (D177.1; the
former requirement that s be of DIMENSION T1 is removed); dividing by an
expression of the literal zero's dimension is refused ("divides by zero").
THE D VARIABLE (D177.1; tpc_form 0.2.0): the second argument s of D(x,s,n)
in any LAW's EQUATION is the D variable. T1 (d_variable_check, run by
tpc_zone.t1_well_formed): s is a DOF of the TPK ("LAW:<n>: EQUATION's D
variable s is not a DOF") and the TARGET of no CONSTRAINT, FIX or REMOVE
("... is the TARGET of CONSTRAINT:<c>"); under the TPK PARAMETERS'
D_VARIABLES ONE (ONE when absent) every D of the TPK's forms uses one s,
under SEVERAL any number. d_variables lists the distinct s in code point
order. A form that does not parse uses no D variable (T1 reports it). The
TrM's SIGNATURE FORM is not read by the rule: it is the TrM's, entered
after T1. The evaluator is unchanged: D of a bound identifier is 0 with the
bound identifier's KIND; under T1 the variable s is a DOF under no FIX, so
T3 never binds it.
THE PARSE TREE (S32; tpc_form 0.2.0): form_tree(text, mode) returns ["OK",
tree] with the tree every check here walks, or the refusal parse_form gives;
public so that another module (tpc_eom) reads a form without this module's
private parser. Its node shapes are listed in its docstring.
NAMES (S5): every identifier in a form is a REFS (OVER) member and every
REFS (OVER) member is named in the form; both directions, in T1.
TOTALITY (S6, T6): + - * abs exp sin cos and ^ with an integer >= 0 are
total; / needs the guard E != 0 (or 0 != E) on its divisor E; ln(E) needs
E > 0 (0 < E); sqrt(E) and E^(p/q) need E >= 0 (0 <= E); E^(negative)
needs E != 0; tan is refused in a predicate; D is not permitted in a
predicate. A guard is a conjunct beside the comparison: the other operands
of every "and" on the path from the root, through "not" and parentheses;
an "or" on the path hides the conjuncts below it from those above. Guards
match by canonical spelling.
T3 OVER LAWS, THE GROUND FRAGMENT AT DEPTH 1 (S7, S11): a law whose every
identifier is bound (a CONSTANT with VALUE and UNIT, or a DOF under a FIX
constraint; a derivative variable need not be) evaluates in coherent SI as
IEEE doubles in one written order, both sides compared through canon()
at twelve significant digits; false is P and not-P; a KIND difference
between the sides is returned as T3 over constraints returns it; a
non-finite value or a partial operation outside its domain returns the
law unevaluated; D of a bound identifier is 0; two laws with one canonical
left side and different canonical right sides are P and not-P. Nothing
beyond depth 1 is claimed.
IC4 (a), SYNTACTIC (S8): IMAGE_FORM equals FORM with every DOF replaced by
its entry's ENVIRONMENT_QUANTITY, as canonical spellings; a DOF in OVER
with no entry leaves the signature undecided (IC2's gap, not IC4's
failure). Whether the image holds in the environment stays INSPECTION.
Every function returns canonical lists, never raises on malformed input,
and escapes what it quotes (tpm_zone_schemas 6.3). The parser and every walk
of a tree run on an explicit stack (_run, 0.1.1): a recursive step is written
"yield <sub-call>", so no nesting depth reaches Python's recursion limit and
every depth TPC-PHP answers is answered alike.
"""
import math
import tpc_zone as Z
import tpc_strike as S
TPC_FORM_VERSION = "0.2.1" # proposed PATCH with TPC-PY 0.2.0: C-MS-5 (TPC-PHP reads the
# JSON as written); 0.2.0 carried D186.1, S14, D177.1 (the D
# variable) and S32 (form_tree); D181.2 left it unchanged (S27).
MAX_CODE_POINTS = 4096 # D186.1 (ESTIMATE): code points of the canonical text
MAX_NESTING = 64 # D186.1 (ESTIMATE): parentheses open at once
MAX_INTEGER_DIGITS = 4 # D186.1: the DIMENSION bound, 9999 (TPS 2.5.12)
EXP_MAX = 9999 # S14: every computed exponent, as tpc_units' EXP_MAX
_PURE = ("exp", "ln", "sin", "cos", "tan") # S14: yield a pure number; end the product
FUNCTIONS =["exp", "ln", "sin", "cos", "tan", "abs", "sqrt"]
KEYWORDS = ["and", "or", "not"]
CMP_OPS = ["<", "<=", ">", ">=", "=", "!="]
MODES = ["expression", "equation", "predicate", "form"]
MODE_OF_FIELD = {"EQUATION": "equation", "CONDITION": "predicate",
"FORM": "form", "IMAGE_FORM": "form"}
_KIND_BASES = ["rad", "Hz", "Bq", "Gy", "Sv"]
_EVAL_REASONS = {
"div0": "division by zero", "fin": "not a finite double", "ln": "ln of a non-positive value",
"sqrt": "sqrt of a negative value", "rat": "a negative base under a rational exponent",
"neg0": "0 under a negative exponent",
}
class _Refused(Exception):
pass
def _run(gen):
"""Drive a recursion written as generators on an explicit stack: each
generator yields the generator of a sub-call and is sent its result, or
thrown its exception, at that point, exactly where a call would have
returned or raised. The Python stack stays flat at any depth."""
stack, value, exc = [gen], None, None
while True:
g = stack[-1]
try:
if exc is None:
sub = g.send(value)
else:
sub, exc = g.throw(exc), None
except StopIteration as done:
stack.pop()
if not stack:
return done.value
value, exc = done.value, None
continue
except BaseException as e: # the sub-call raised: to its caller
stack.pop()
if not stack:
raise
value, exc = None, e.with_traceback(None)
continue
stack.append(sub)
value = None
# ---- tokens --------------------------------------------------------------------
def _is_alpha(c):
return ("a" <= c <= "z") or ("A" <= c <= "Z") or c == "_"
def _is_digit(c):
return "0" <= c <= "9"
def _tokens(text):
"""[(kind, value, position)]; kind in id num op; position 1-based."""
out, i, n = [], 0, len(text)
while i < n:
c = text[i]
if c in (" ", "\t", "\n"):
i += 1
continue
if _is_alpha(c):
j = i + 1
while j < n and (_is_alpha(text[j]) or _is_digit(text[j])):
j += 1
out.append(("id", text[i:j], i + 1))
i = j
continue
if _is_digit(c):
j = i
while j < n and _is_digit(text[j]):
j += 1
if j + 1 < n and text[j] == "." and _is_digit(text[j + 1]):
j += 1
while j < n and _is_digit(text[j]):
j += 1
if j < n and text[j] in ("e", "E"):
k = j + 1
if k < n and text[k] in ("+", "-"):
k += 1
m = k
while m < n and _is_digit(text[m]) and m - k < 4:
m += 1
if m > k and not (m < n and _is_digit(text[m])):
j = m
out.append(("num", text[i:j], i + 1))
i = j
continue
two = text[i:i + 2]
if two in ("<=", ">=", "!="):
out.append(("op", two, i + 1))
i += 2
continue
if c in "<>=+-*/^(),":
out.append(("op", c, i + 1))
i += 1
continue
raise _Refused("unexpected character %s at %d" % (Z._show(c), i + 1))
return out
# ---- the parser ----------------------------------------------------------------
class _P(object):
def __init__(self, toks, mode):
self.t, self.i, self.mode = toks, 0, mode
def peek(self, k=0):
j = self.i + k
return self.t[j] if j < len(self.t) else None
def is_op(self, v, k=0):
p = self.peek(k)
return p is not None and p[0] == "op" and p[1] == v
def fail_here(self):
p = self.peek()
if p is None:
raise _Refused("unexpected end")
raise _Refused("unexpected token %s at %d" % (p[1], p[2]))
def take_op(self, v):
if not self.is_op(v):
self.fail_here()
self.i += 1
def integer(self):
p = self.peek()
if p is None or p[0] != "num" or not all(_is_digit(c) for c in p[1]):
return None
if len(p[1]) > MAX_INTEGER_DIGITS: # D186.1: refused before conversion
raise _Refused("an integer of more than %d digits at %d" % (MAX_INTEGER_DIGITS, p[2]))
self.i += 1
return int(p[1])
# -- predicates (generators: a sub-rule is "yield self.rule()", run by _run) --
def predicate(self):
left = yield self.conj()
while self.peek() is not None and self.peek()[0] == "id" and self.peek()[1] == "or":
self.i += 1
left = ["or", left, (yield self.conj())]
return left
def conj(self):
left = yield self.neg()
while self.peek() is not None and self.peek()[0] == "id" and self.peek()[1] == "and":
self.i += 1
left = ["and", left, (yield self.neg())]
return left
def neg(self):
p = self.peek()
if p is not None and p[0] == "id" and p[1] == "not":
self.i += 1
return ["not", (yield self.neg())]
if self.is_op("(") and self.paren_is_predicate():
self.i += 1
inner = yield self.predicate()
self.take_op(")")
return ["pparen", inner]
a = yield self.expr()
q = self.peek()
if q is None or q[0] != "op" or q[1] not in CMP_OPS:
self.fail_here()
self.i += 1
b = yield self.expr()
return ["cmp", q[1], a, b]
def paren_is_predicate(self):
depth, j = 0, self.i
while j < len(self.t):
k, v, _ = self.t[j]
if k == "op" and v == "(":
depth += 1
elif k == "op" and v == ")":
depth -= 1
if depth == 0:
return False
elif depth >= 1 and ((k == "op" and v in CMP_OPS) or (k == "id" and v in KEYWORDS)):
return True
j += 1
return False
# -- expressions --
def expr(self):
left = yield self.term()
while self.is_op("+") or self.is_op("-"):
op = self.peek()[1]
self.i += 1
left = ["bin", op, left, (yield self.term())]
return left
def term(self):
left = yield self.unary()
while self.is_op("*") or self.is_op("/"):
op = self.peek()[1]
self.i += 1
left = ["bin", op, left, (yield self.unary())]
return left
def unary(self):
if self.is_op("-"):
prev = self.t[self.i - 1] if self.i > 0 else None
if prev is not None and prev[0] == "op" and prev[1] in ("+", "-", "*", "/", "^"):
self.fail_here() # two operators in a row
self.i += 1
return ["neg", (yield self.power())]
return (yield self.power())
def power(self):
base = yield self.atom()
if not self.is_op("^"):
return base
pos = self.peek()[2]
self.i += 1
p = self.integer()
if p is not None:
pq = [p, 1]
elif self.is_op("("):
self.i += 1
sign = 1
if self.is_op("-"):
sign = -1
self.i += 1
p = self.integer()
if p is None:
raise _Refused("^ takes an integer or a parenthesized rational exponent at %d" % pos)
q = 1
if self.is_op("/"):
self.i += 1
q = self.integer()
if q is None:
raise _Refused("^ takes an integer or a parenthesized rational exponent at %d" % pos)
if q == 0:
raise _Refused("a rational exponent needs a positive denominator at %d" % pos)
if not self.is_op(")"):
raise _Refused("^ takes an integer or a parenthesized rational exponent at %d" % pos)
self.i += 1
pq = [sign * p, q]
else:
raise _Refused("^ takes an integer or a parenthesized rational exponent at %d" % pos)
if self.is_op("^"):
raise _Refused("chained ^ needs parentheses at %d" % self.peek()[2])
_composed(base, pq[0], pq[1], pos) # S14, T1
return ["pow", base, pq]
def atom(self):
p = self.peek()
if p is None:
raise _Refused("unexpected end")
k, v, pos = p
if k == "num":
self.i += 1
return ["num", Z.canon_decimal(v)]
if k == "op" and v == "(":
self.i += 1
inner = yield self.expr()
self.take_op(")")
return ["paren", inner]
if k == "id":
if v in KEYWORDS:
self.fail_here()
if self.is_op("(", 1):
if v == "D":
if self.mode == "predicate":
raise _Refused("D is not permitted in a CONDITION at %d" % pos)
return self.derivative(pos)
if v not in FUNCTIONS:
raise _Refused("unknown function %s at %d" % (v, pos))
self.i += 2
arg = yield self.expr()
self.take_op(")")
if v == "sqrt":
_composed(arg, 1, 2, pos) # S14, T1: sqrt counts 1/2
return ["fn", v, arg]
self.i += 1
return ["id", v]
self.fail_here()
def derivative(self, pos):
msg = "D is written D(x,t) or D(x,t,n) at %d" % pos
self.i += 2
x = self.peek()
if x is None or x[0] != "id" or x[1] in KEYWORDS:
raise _Refused(msg)
self.i += 1
if not self.is_op(","):
raise _Refused(msg)
self.i += 1
t = self.peek()
if t is None or t[0] != "id" or t[1] in KEYWORDS:
raise _Refused(msg)
self.i += 1
n = 1
if self.is_op(","):
self.i += 1
n = self.integer()
if n is None or n < 1:
raise _Refused(msg)
if not self.is_op(")"):
raise _Refused(msg)
self.i += 1
return ["D", x[1], t[1], n]
def top(self):
if not self.t:
raise _Refused("empty form")
if self.mode == "predicate":
tree = ["pred", (yield self.predicate())]
else:
a = yield self.expr()
if self.is_op("="):
if self.mode == "expression":
self.fail_here()
self.i += 1
tree = ["eq", a, (yield self.expr())]
elif self.mode == "equation":
if self.peek() is not None:
self.fail_here()
raise _Refused("the equation has no =")
else:
tree = ["expr", a]
if self.peek() is not None:
self.fail_here()
return tree
def _gcd(a, b):
"""Euclid on magnitudes; _gcd(0, d) = d. Written out so both residences
run the same steps."""
a, b = abs(a), abs(b)
while b:
a, b = b, a % b
return a
def _composed(base, p, q, pos):
"""S14, T1: every exponent the form composes for an identifier or a D under
base, times p/q, in lowest terms, has numerator and denominator within
EXP_MAX; raises _Refused at pos otherwise. Each composition under base was
checked when its own power or root completed, so every value here is a
product of bounded parts."""
acc = {}
_run(_composed_g(base, 1, 1, acc))
for n, d in acc.values():
a, b = n * p, d * q
g = _gcd(a, b)
if abs(a // g) > EXP_MAX or b // g > EXP_MAX:
raise _Refused("a computed exponent beyond %d at %d" % (EXP_MAX, pos))
def _composed_g(node, n, d, acc):
k = node[0]
if k in ("id", "D"):
acc[str(n) + "/" + str(d)] = (n, d)
elif k in ("neg", "paren"):
yield _composed_g(node[1], n, d, acc)
elif k == "bin":
yield _composed_g(node[2], n, d, acc)
yield _composed_g(node[3], n, d, acc)
elif k == "pow":
a, b = n * node[2][0], d * node[2][1]
g = _gcd(a, b)
yield _composed_g(node[1], a // g, b // g, acc)
elif k == "fn" and node[1] not in _PURE:
if node[1] == "sqrt":
a, b = n, d * 2
g = _gcd(a, b)
yield _composed_g(node[2], a // g, b // g, acc)
else:
yield _composed_g(node[2], n, d, acc)
def _in_range(e, kind=False):
"""S14: every exponent within -EXP_MAX..EXP_MAX, as tpc_units requires of a
UNIT's DIMENSION; None (the literal zero's ANY) passes."""
if e is not None and any(x > EXP_MAX or x < -EXP_MAX for x in e):
raise _Refused("a kind exponent is out of range" if kind else "an exponent is out of range")
return e
def _bounds(t):
"""D186.1, on the canonical text before any token is read: the length in
code points, then the depth of parentheses in one linear scan; raises
_Refused at the first bound exceeded."""
if len(t) > MAX_CODE_POINTS:
raise _Refused("the form is longer than %d code points" % MAX_CODE_POINTS)
depth = 0
for i, ch in enumerate(t):
if ch == "(":
depth += 1
if depth > MAX_NESTING:
raise _Refused("more than %d nested parentheses at %d" % (MAX_NESTING, i + 1))
elif ch == ")" and depth > 0:
depth -= 1
def _parse(text, mode):
"""The parse tree, or raises _Refused."""
if mode not in MODES:
raise _Refused("unknown mode " + Z._show(str(mode)))
if not isinstance(text, str):
raise _Refused("the form is not a string")
t = Z._text(text)
_bounds(t)
return _run(_P(_tokens(t), mode).top())
# ---- canonical spelling ----------------------------------------------------------
def _strip(node):
while node[0] in ("paren", "pparen"):
node = node[1]
return node
def _pr(node):
return _run(_pr_g(node))
def _pr_g(node):
k = node[0]
if k == "num":
return node[1]
if k == "id":
return node[1]
if k == "neg":
return "-" + (yield _pr_g(node[1]))
if k == "paren":
return "(" + (yield _pr_g(node[1])) + ")"
if k == "bin":
return (yield _pr_g(node[2])) + node[1] + (yield _pr_g(node[3]))
if k == "pow":
p, q = node[2]
if q == 1 and p >= 0:
e = str(p)
elif q == 1:
e = "(" + str(p) + ")"
else:
e = "(" + str(p) + "/" + str(q) + ")"
return (yield _pr_g(node[1])) + "^" + e
if k == "fn":
return node[1] + "(" + (yield _pr_g(_strip(node[2]))) + ")"
if k == "D":
return "D(" + node[1] + "," + node[2] + (("," + str(node[3])) if node[3] != 1 else "") + ")"
if k == "cmp":
return (yield _pr_g(_strip(node[2]))) + node[1] + (yield _pr_g(_strip(node[3])))
if k == "and":
return (yield _pr_g(node[1])) + " and " + (yield _pr_g(node[2]))
if k == "or":
return (yield _pr_g(node[1])) + " or " + (yield _pr_g(node[2]))
if k == "not":
return "not " + (yield _pr_g(node[1]))
if k == "pparen":
return "(" + (yield _pr_g(node[1])) + ")"
if k == "eq":
return (yield _pr_g(_strip(node[1]))) + "=" + (yield _pr_g(_strip(node[2])))
if k == "expr":
return (yield _pr_g(_strip(node[1])))
if k == "pred":
return (yield _pr_g(_strip(node[1])))
raise TypeError("print: unknown node")
def _refuse(reason):
return ["REFUSED", Z._show(reason)]
def parse_form(text, mode):
"""["OK", canonical spelling] or ["REFUSED", reason]. mode: expression,
equation (EQUATION), predicate (CONDITION) or form (FORM, IMAGE_FORM)."""
try:
return ["OK", _pr(_parse(text, mode))]
except _Refused as e:
return _refuse(str(e))
def form_tree(text, mode):
"""["OK", parse tree] or ["REFUSED", reason], the reason exactly as
parse_form gives it (S32; tpc_form 0.2.0, unreleased). The tree is the
one every check of this module walks, as parsed (a parenthesis the
canonical spelling drops is kept as a "paren" node):
top ["eq", l, r] (equation, form with "="), ["expr", e] (expression,
form without "="), ["pred", p] (predicate)
expr ["num", canonical decimal], ["id", name], ["neg", e],
["paren", e], ["bin", op, l, r] (op + - * /),
["pow", e, [p, q]] (integers, q >= 1, as written), ["fn", f, e],
["D", x, s, n] (n an integer >= 1; 1 when not written)
pred ["cmp", op, l, r], ["and", a, b], ["or", a, b], ["not", a],
["pparen", a]
Pure; the caller's copy is its own."""
try:
return ["OK", _parse(text, mode)]
except _Refused as e:
return _refuse(str(e))
def _idents(node, acc):
_run(_idents_g(node, acc))
def _idents_g(node, acc):
k = node[0]
if k == "id":
acc.add(node[1])
elif k == "D":
acc.add(node[1])
acc.add(node[2])
elif k in ("num",):
pass
else:
for c in node[1:]:
if isinstance(c, list) and c and isinstance(c[0], str) and c[0] in _NODE_KINDS:
yield _idents_g(c, acc)
_NODE_KINDS = {"num", "id", "neg", "paren", "bin", "pow", "fn", "D", "cmp", "and", "or",
"not", "pparen", "eq", "expr", "pred"}
def _children(node):
return [c for c in node[1:] if isinstance(c, list) and c and isinstance(c[0], str)
and c[0] in _NODE_KINDS]
def form_names(text, mode):
"""["OK", sorted identifiers the form names] or ["REFUSED", reason]. A
function name and D are not identifiers; D's operand and variable are."""
try:
acc = set()
_idents(_parse(text, mode), acc)
return ["OK", sorted(acc)]
except _Refused as e:
return _refuse(str(e))
# ---- dimensions (S4) ---------------------------------------------------------------
def _exps(dim):
"""Canonical DIMENSION string -> exponent list, or None."""
d = Z.normalize_dimension(dim)
if d is None:
return None
out = [0] * len(Z.DIM_BASES)
if d == "1":
return out
for tok in d.split(" "):
for i, b in enumerate(Z.DIM_BASES):
if tok.startswith(b) and tok[len(b):].lstrip("-").isdigit():
out[i] = int(tok[len(b):])
break
return out
def _dstr(e):
if e is None:
return "ANY"
return Z.canon_dimension(dict(zip(Z.DIM_BASES, e)))
def _dim(node, dims, opname):
"""Exponent list, None for the literal zero's ANY; raises _Refused."""
return _run(_dim_g(node, dims, opname))
def _dim_g(node, dims, opname):
k = node[0]
if k == "num":
return None if node[1] == "0" else [0] * 7
if k == "id":
if node[1] not in dims or dims[node[1]] is None:
raise _Refused("%s has no DIMENSION" % node[1])
return _in_range(list(dims[node[1]]))
if k in ("neg", "paren"):
return (yield _dim_g(node[1], dims, opname))
if k == "bin":
a = yield _dim_g(node[2], dims, opname)
b = yield _dim_g(node[3], dims, opname)
op = node[1]
if op in ("+", "-"):
if a is None:
return b
if b is None:
return a
if a != b:
raise _Refused("%s joins %s and %s" % (op, _dstr(a), _dstr(b)))
return a
if op == "*":
if a is None or b is None:
return None
return _in_range([x + y for x, y in zip(a, b)])
if b is None:
raise _Refused("divides by zero")
if a is None:
return None
return _in_range([x - y for x, y in zip(a, b)])
if k == "pow":
a = yield _dim_g(node[1], dims, opname)
p, q = node[2]
if a is None:
return None
out = []
for x in a:
if (x * p) % q != 0:
raise _Refused("^ (%d/%d) of %s is not a dimension" % (p, q, _dstr(a)))
out.append((x * p) // q)
return _in_range(out)
if k == "fn":
a = yield _dim_g(node[2], dims, opname)
f = node[1]
if f == "abs":
return a
if f == "sqrt":
if a is None:
return None
if any(x % 2 != 0 for x in a):
raise _Refused("sqrt of %s is not a dimension" % _dstr(a))
return [x // 2 for x in a]
if a is not None and any(x != 0 for x in a):
raise _Refused("%s needs a dimensionless argument, not %s" % (f, _dstr(a)))
return [0] * 7
if k == "D":
x, t, n = node[1], node[2], node[3]
if x not in dims or dims[x] is None:
raise _Refused("%s has no DIMENSION" % x)
if t not in dims or dims[t] is None:
raise _Refused("%s has no DIMENSION" % t)
a = _in_range(list(dims[x])) # D177.1: dim(x) less n times dim(s)
b = _in_range(list(dims[t]))
return _in_range([p - n * q for p, q in zip(a, b)])
if k == "cmp":
a = yield _dim_g(node[2], dims, opname)
b = yield _dim_g(node[3], dims, opname)
if a is not None and b is not None and a != b:
raise _Refused("%s compares %s and %s" % (node[1], _dstr(a), _dstr(b)))
return [0] * 7
if k in ("and", "or"):
yield _dim_g(node[1], dims, opname)
yield _dim_g(node[2], dims, opname)
return [0] * 7
if k in ("not", "pparen", "pred"):
yield _dim_g(node[1], dims, opname)
return [0] * 7
if k == "expr":
return (yield _dim_g(node[1], dims, opname))
if k == "eq":
a = yield _dim_g(node[1], dims, opname)
b = yield _dim_g(node[2], dims, opname)
if a is None:
return b
if b is None:
return a
if a != b:
raise _Refused("sides have dimensions %s and %s" % (_dstr(a), _dstr(b)))
return a
raise TypeError("dim: unknown node")
def _dims_of(dimensions):
"""{name: DIMENSION string} -> {name: exponent list or None}."""
out = {}
if isinstance(dimensions, dict):
for k, v in dimensions.items():
out[k] = _exps(v) if isinstance(v, str) else None
return out
def form_dimension(text, mode, dimensions):
"""["OK", DIMENSION] or ["REFUSED", reason]: the DIMENSION of an
expression, equation or form under {name: DIMENSION}; "ANY" for the
literal zero alone; "1" for a predicate whose comparisons are homogeneous."""
try:
tree = _parse(text, mode)
return ["OK", _dstr(_dim(tree, _dims_of(dimensions), mode))]
except _Refused as e:
return _refuse(str(e))
# ---- totality (S6) ------------------------------------------------------------------
def _guards_needed(node, acc):
"""(what, operand canonical, guard canonical forms accepted) per partial
operation in an expression subtree; tan is listed with no guard."""
_run(_guards_needed_g(node, acc))
def _guards_needed_g(node, acc):
k = node[0]
if k == "bin":
yield _guards_needed_g(node[2], acc)
yield _guards_needed_g(node[3], acc)
if node[1] == "/":
e = _pr(_strip(node[3]))
acc.append(("/ on " + e, "guard " + e + " != 0", [e + "!=0", "0!=" + e]))
elif k == "pow":
yield _guards_needed_g(node[1], acc)
p, q = node[2]
e = _pr(_strip(node[1]))
if q != 1:
acc.append(("^ with a rational exponent on " + e, "guard " + e + " >= 0", [e + ">=0", "0<=" + e]))
elif p < 0:
acc.append(("^ with a negative exponent on " + e, "guard " + e + " != 0", [e + "!=0", "0!=" + e]))
elif k == "fn":
yield _guards_needed_g(node[2], acc)
e = _pr(_strip(node[2]))
if node[1] == "ln":
acc.append(("ln on " + e, "guard " + e + " > 0", [e + ">0", "0<" + e]))
elif node[1] == "sqrt":
acc.append(("sqrt on " + e, "guard " + e + " >= 0", [e + ">=0", "0<=" + e]))
elif node[1] == "tan":
acc.append(("tan on " + e, None, []))
elif k in ("neg", "paren"):
yield _guards_needed_g(node[1], acc)
def _totality(node, guards, probs):
"""Walk a predicate; guards is the list of canonical conjuncts in force."""
_run(_totality_g(node, guards, probs))
def _totality_g(node, guards, probs):
k = node[0]
if k == "and":
c2 = yield _conjuncts_g(node[2])
yield _totality_g(node[1], guards + c2, probs)
c1 = yield _conjuncts_g(node[1])
yield _totality_g(node[2], guards + c1, probs)
elif k == "or":
yield _totality_g(node[1], guards, probs)
yield _totality_g(node[2], guards, probs)
elif k in ("not", "pparen", "pred"):
yield _totality_g(node[1], guards, probs)
elif k == "cmp":
need = []
_guards_needed(node[2], need)
_guards_needed(node[3], need)
for what, guard, forms in need:
if guard is None:
probs.append("uses " + what + ", which is not total")
elif not any(f in guards for f in forms):
probs.append("uses " + what + " with no " + guard)
def _conjuncts(node):
"""The canonical comparisons a conjunct supplies as guards: the
comparison itself, or the conjuncts of a nested "and"."""
return _run(_conjuncts_g(node))
def _conjuncts_g(node):
n = node
while n[0] == "pparen":
n = n[1]
if n[0] == "cmp":
return [_pr(n)]
if n[0] == "and":
return (yield _conjuncts_g(n[1])) + (yield _conjuncts_g(n[2]))
return []
def form_totality(text, dimensions):
"""["OK", []] when a CONDITION is total under the guard table, else
["OK", sorted problems]; ["REFUSED", reason] when it does not parse or
is not dimensionally homogeneous."""
try:
tree = _parse(text, "predicate")
_dim(tree, _dims_of(dimensions), "predicate")
probs = []
_totality(tree, [], probs)
return ["OK", sorted(set(probs))]
except _Refused as e:
return _refuse(str(e))
# ---- evaluation, the ground fragment (S7, S11) --------------------------------------
def _kexps(kind):
out = [0] * len(_KIND_BASES)
if not isinstance(kind, str) or kind == "none":
return out
for tok in kind.split(" "):
for i, b in enumerate(_KIND_BASES):
if tok.startswith(b) and tok[len(b):].lstrip("-").isdigit():
out[i] = int(tok[len(b):])
break
return out
def _kstr(k):
toks = [_KIND_BASES[j] + str(k[j]) for j in range(len(_KIND_BASES)) if k[j] != 0]
return " ".join(toks) if toks else "none"
class _Unbound(Exception):
pass
class _Convention(Exception):
pass
def _ev(node, b):
"""(value, kind exponents); raises _Unbound, _Convention or _Refused."""
return _run(_ev_g(node, b))
def _ev_g(node, b):
k = node[0]
if k == "num":
return float(node[1]), [0] * 5
if k == "id":
if node[1] not in b:
raise _Unbound(node[1])
return b[node[1]][0], _in_range(list(b[node[1]][1]), True)
if k == "paren":
return (yield _ev_g(node[1], b))
if k == "neg":
v, kk = yield _ev_g(node[1], b)
return -v, kk
if k == "bin":
va, ka = yield _ev_g(node[2], b)
vb, kb = yield _ev_g(node[3], b)
op = node[1]
if op in ("+", "-"):
if ka != kb:
raise _Convention("units of different kind: %s and %s" % (_kstr(ka), _kstr(kb)))
return (va + vb) if op == "+" else (va - vb), ka
if op == "*":
return va * vb, _in_range([x + y for x, y in zip(ka, kb)], True)
if vb == 0.0:
raise _Refused(_EVAL_REASONS["div0"])
return va / vb, _in_range([x - y for x, y in zip(ka, kb)], True)
if k == "pow":
va, ka = yield _ev_g(node[1], b)
p, q = node[2]
kk = []
for x in ka:
if (x * p) % q != 0:
raise _Refused("^ (%d/%d) of kind %s is not a kind" % (p, q, _kstr(ka)))
kk.append((x * p) // q)
_in_range(kk, True)
if q == 1:
r = 1.0
for _ in range(abs(p)):
r = r * va
if p < 0:
if r == 0.0:
raise _Refused(_EVAL_REASONS["neg0"])
r = 1.0 / r
return r, kk
if va < 0.0:
raise _Refused(_EVAL_REASONS["rat"])
if va == 0.0 and p < 0: # S14: as 0 under a negative integer
raise _Refused(_EVAL_REASONS["neg0"])
try:
return math.pow(va, float(p) / float(q)), kk
except OverflowError:
return math.inf, kk # as C pow: overflow is +inf
if k == "fn":
va, ka = yield _ev_g(node[2], b)
f = node[1]
if f == "abs":
return abs(va), ka
if f == "sqrt":
if va < 0.0:
raise _Refused(_EVAL_REASONS["sqrt"])
if any(x % 2 != 0 for x in ka):
raise _Refused("sqrt of kind %s is not a kind" % _kstr(ka))
return math.sqrt(va), [x // 2 for x in ka]
if f == "ln":
if va <= 0.0:
raise _Refused(_EVAL_REASONS["ln"])
return math.log(va), [0] * 5
if f == "exp":
try:
return math.exp(va), [0] * 5
except OverflowError:
return math.inf, [0] * 5
if not _finite(va):
raise _Refused(_EVAL_REASONS["fin"]) # sin, cos, tan of a non-finite argument
if f == "sin":
return math.sin(va), [0] * 5
if f == "cos":
return math.cos(va), [0] * 5
return math.tan(va), [0] * 5
if k == "D":
if node[1] not in b:
raise _Unbound(node[1])
return 0.0, _in_range(list(b[node[1]][1]), True)
raise TypeError("eval: unknown node")
def _bindings(bindings):
"""{name: {VALUE, UNIT}} -> {name: (x_SI, kind exponents)}; a value that
cannot be normalized raises _Refused with the reason."""
U = _units()
out = {}
if not isinstance(bindings, dict):
return out
for name in sorted(bindings):
e = bindings[name]
if not isinstance(e, dict):
continue
r = U.normalize_measurement(e.get("VALUE"), "0", e.get("UNIT"))
if r[0] != "OK":
raise _Refused(r[1])
out[name] = (r[1], _kexps(r[4]))
return out
def _units():
import tpc_units
return tpc_units
def _finite(v):
return not (v != v or v in (math.inf, -math.inf))
def eval_form(text, mode, bindings):
"""The ground fragment's evaluator. bindings: {name: {"VALUE": decimal,
"UNIT": unit}}, each normalized to coherent SI. Returns
["OK", value, KIND] for an expression or form without "=", ["OK", left,
right, KIND] for an equation, ["UNBOUND", name] when an identifier is not
bound (a derivative variable need not be), ["CONVENTION", reason] on a
KIND difference, ["REFUSED", reason] otherwise. Values are IEEE doubles
in one written order; compare through canon()."""
try:
tree = _parse(text, mode)
if mode == "predicate":
raise _Refused("a predicate is not evaluated")
b = _bindings(bindings)
if tree[0] == "eq":
va, ka = _ev(tree[1], b)
vb, kb = _ev(tree[2], b)
if not (_finite(va) and _finite(vb)):
raise _Refused(_EVAL_REASONS["fin"])
if ka != kb:
raise _Convention("units of different kind: %s and %s" % (_kstr(ka), _kstr(kb)))
return ["OK", va + 0.0, vb + 0.0, _kstr(ka)]
v, kk = _ev(tree[1], b)
if not _finite(v):
raise _Refused(_EVAL_REASONS["fin"])
return ["OK", v + 0.0, _kstr(kk)]
except _Unbound as e:
return ["UNBOUND", str(e)]
except _Convention as e:
return ["CONVENTION", Z._show(str(e))]
except _Refused as e:
return _refuse(str(e))
# ---- the checks over a TPK ---------------------------------------------------------
def _entries_of(zone, key):
if not Z._obj(zone):
return []
v = zone.get(key, [])
return [e for e in v if Z._obj(e)] if Z._list(v) else []
def _s(e, f):
v = e.get(f)
return v if isinstance(v, str) else None
def _set(e, f):
v = e.get(f)
if Z._list(v) and all(isinstance(x, str) for x in v):
return v
return []
def _tpk_dims(tpk):
out = {}
for kind in ("DOF", "CONSTANT"):
for e in _entries_of(tpk, kind):
n, d = _s(e, "NAME"), _s(e, "DIMENSION")
if n is not None and n not in out:
out[n] = _exps(d) if d is not None else None
return out
def names_check(tpk):
"""S5, both directions, for every LAW with EQUATION and BOUNDARY with
CONDITION: the form names only REFS members and every REFS member. A
form that does not parse is reported here. [pass, problems]. Part of T1,
beside d_variable_check (D177.1)."""
probs = []
for kind, field in (("LAW", "EQUATION"), ("BOUNDARY", "CONDITION")):
for e in _entries_of(tpk, kind):
f = e.get(field)
if field not in e or not isinstance(f, str) or Z._first_bad(f) is not None:
continue
tag = kind + ":" + Z._name(e)
try:
tree = _parse(f, MODE_OF_FIELD[field])
except _Refused as x:
probs.append(tag + ": " + field + " does not parse: " + str(x))
continue
named = set()
_idents(tree, named)
refs = set(_set(e, "REFS"))
for n in sorted(named - refs):
probs.append(tag + ": " + field + " names " + n + ", which is not in REFS")
for n in sorted(refs - named):
probs.append(tag + ": REFS " + n + " is not named in " + field)
return Z._done(probs)
def form_coverage(tpk):
"""[laws without EQUATION, boundaries without CONDITION], sorted names:
what stays INSPECTION under T4, T3 over laws and T6 for this TPK."""
laws = sorted(Z._name(e) for e in _entries_of(tpk, "LAW") if "EQUATION" not in e)
bnds = sorted(Z._name(e) for e in _entries_of(tpk, "BOUNDARY") if "CONDITION" not in e)
return [laws, bnds]
def _dvars_g(node, acc, law):
k = node[0]
if k == "D":
acc.setdefault(node[2], set()).add(law)
elif k not in ("num", "id"):
for c in _children(node):
yield _dvars_g(c, acc, law)
def _law_dvars(tpk):
"""{D variable: set of LAW tags} over every LAW whose EQUATION is a string
free of disallowed code points that parses; a form that does not is T1's to
report and uses no D variable."""
acc = {}
for e in _entries_of(tpk, "LAW"):
f = e.get("EQUATION")
if not isinstance(f, str) or Z._first_bad(f) is not None:
continue
try:
tree = _parse(f, "equation")
except _Refused:
continue
_run(_dvars_g(tree, acc, "LAW:" + Z._name(e)))
return acc
def d_variables(tpk):
"""D177.1: the distinct D variables of the TPK's forms (the second argument
of every D in a LAW's EQUATION that parses), in code point order."""
return sorted(_law_dvars(tpk))
def d_variable_check(tpk):
"""D177.1, part of T1: every D variable is a DOF of the TPK and the TARGET of
no CONSTRAINT (FIX or REMOVE, whatever the ACTION reads); under the TPK
PARAMETERS' D_VARIABLES ONE (ONE when PARAMETERS or D_VARIABLES is absent)
the forms use one D variable, under SEVERAL any number; a PARAMETERS part or a
D_VARIABLES that T1 refuses applies no count. [pass, problems]."""
if not Z._obj(tpk):
return Z._done([])
uses = _law_dvars(tpk)
dofs = set(n for n in (_s(e, "NAME") for e in _entries_of(tpk, "DOF")) if n is not None)
targets = {}
for c in _entries_of(tpk, "CONSTRAINT"):
t = _s(c, "TARGET")
if t is not None:
targets.setdefault(t, set()).add("CONSTRAINT:" + Z._name(c))
probs = []
for s in sorted(uses):
for law in sorted(uses[s]):
if s not in dofs:
probs.append(law + ": EQUATION's D variable " + s + " is not a DOF")
for c in sorted(targets.get(s, ())):
probs.append(law + ": EQUATION's D variable " + s + " is the TARGET of " + c)
pm = tpk.get("PARAMETERS", {})
mode = pm.get("D_VARIABLES", Z.D_VARIABLES_DEFAULT) if Z._obj(pm) else None
if mode == "ONE" and len(uses) > 1:
probs.append("TPK: D_VARIABLES is ONE (ONE when absent), but the forms use D variables "
+ ", ".join(s + " (" + ", ".join(sorted(uses[s])) + ")" for s in sorted(uses)))
return Z._done(probs)
def t4_homogeneity(tpk):
"""Kernel test T4, the law half (guide 3.6), over every LAW with EQUATION:
the equation is dimensionally homogeneous under the DIMENSIONs of the DOF
and CONSTANTs it names. [pass, problems]. Runs on a TPK that passes T1."""
probs = []
dims = _tpk_dims(tpk)
for e in _entries_of(tpk, "LAW"):
f = e.get("EQUATION")
if not isinstance(f, str):
continue
tag = "LAW:" + Z._name(e)
try:
tree = _parse(f, "equation")
except _Refused:
continue # T1's to report
try:
_dim(tree, dims, "equation")
except _Refused as x:
probs.append(tag + ": EQUATION " + str(x) + " (T4)")
return Z._done(probs)
def t6_totality(tpk):
"""Kernel test T6, totality (guide 3.6), over every BOUNDARY with
CONDITION: every comparison is homogeneous and every partial operation is
guarded by a conjunct beside it. [pass, problems]. Runs after T1."""
probs = []
dims = _tpk_dims(tpk)
for e in _entries_of(tpk, "BOUNDARY"):
f = e.get("CONDITION")
if not isinstance(f, str):
continue
tag = "BOUNDARY:" + Z._name(e)
try:
tree = _parse(f, "predicate")
except _Refused:
continue # T1's to report
try:
_dim(tree, dims, "predicate")
found = []
_totality(tree, [], found)
for p in found:
probs.append(tag + ": CONDITION " + p + " (T6)")
except _Refused as x:
probs.append(tag + ": CONDITION " + str(x) + " (T6)")
return Z._done(probs)
def _fix_bindings(tpk):
"""{DOF: (constraint name, entry)} for the first FIX by NAME order."""
out = {}
cs = sorted(_entries_of(tpk, "CONSTRAINT"), key=lambda c: Z._name(c))
for c in cs:
t = _s(c, "TARGET")
if t is not None and _s(c, "ACTION") == "FIX" and t not in out \
and isinstance(c.get("VALUE"), str) and isinstance(c.get("UNIT"), str):
out[t] = (Z._name(c), c)
return out
def t3_laws(tpk):
"""Kernel test T3 over the laws, the ground fragment at depth 1 (S7):
(i) a LAW with EQUATION whose every identifier is bound - a CONSTANT with
VALUE and UNIT, or a DOF under a FIX constraint - evaluates in coherent SI;
a closed equation false through canon() is P and not-P; (ii) two laws with
one canonical left side and different canonical right sides are P and
not-P. [pass, problems]. Nothing beyond depth 1 is claimed."""
probs = []
consts = {}
for e in _entries_of(tpk, "CONSTANT"):
n = _s(e, "NAME")
if n is not None and isinstance(e.get("VALUE"), str) and isinstance(e.get("UNIT"), str):
consts.setdefault(n, e)
fixes = _fix_bindings(tpk)
lefts = {}
for e in sorted(_entries_of(tpk, "LAW"), key=lambda l: Z._name(l)):
f = e.get("EQUATION")
if not isinstance(f, str):
continue
tag = "LAW:" + Z._name(e)
try:
tree = _parse(f, "equation")
except _Refused:
continue # T1's to report
lefts.setdefault(_pr(_strip(tree[1])), []).append((Z._name(e), _pr(_strip(tree[2]))))
named = set()
_idents(tree, named)
b, used = {}, []
for n in sorted(named):
if n in consts:
b[n] = {"VALUE": consts[n]["VALUE"], "UNIT": consts[n]["UNIT"]}
elif n in fixes:
b[n] = {"VALUE": fixes[n][1]["VALUE"], "UNIT": fixes[n][1]["UNIT"]}
used.append(fixes[n][0])
who = tag + ("".join(" and CONSTRAINT:" + c for c in sorted(set(used))))
basis = "under the fixed values" if used else "under the declared values"
try:
bb = _bindings(b)
except _Refused as x:
probs.append(tag + ": EQUATION cannot be evaluated: " + str(x) + " (T3)")
continue
try:
va, ka = _ev(tree[1], bb)
vb, kb = _ev(tree[2], bb)
if not (_finite(va) and _finite(vb)):
raise _Refused(_EVAL_REASONS["fin"])
if ka != kb:
probs.append(tag + ": the two sides of EQUATION cannot be compared: units of different kind: "
+ _kstr(ka) + " and " + _kstr(kb) + " (T3)")
elif S.canon(va + 0.0) != S.canon(vb + 0.0):
probs.append(who + ": " + Z._name(e) + " evaluates " + S.canon(va + 0.0) + " = "
+ S.canon(vb + 0.0) + " " + basis + " (T3)")
except _Unbound:
pass # nothing claimed
except _Convention as x:
probs.append(tag + ": the two sides of EQUATION cannot be compared: " + str(x) + " (T3)")
except _Refused as x:
probs.append(tag + ": EQUATION cannot be evaluated " + basis + ": " + str(x) + " (T3)")
for left in sorted(lefts):
rs = lefts[left]
for i in range(len(rs)):
for j in range(i + 1, len(rs)):
if rs[i][1] != rs[j][1]:
probs.append("LAW:" + rs[i][0] + " and LAW:" + rs[j][0] + ": the left side " + left
+ " is equated to " + rs[i][1] + " and to " + rs[j][1] + " (T3)")
return Z._done(probs)
# ---- IC4 (a), syntactic (S8) --------------------------------------------------------
def _rename(node, m):
return _run(_rename_g(node, m))
def _rename_g(node, m):
k = node[0]
if k == "id":
return ["id", m.get(node[1], node[1])]
if k == "D":
return ["D", m.get(node[1], node[1]), m.get(node[2], node[2]), node[3]]
if k == "num":
return node
out = [node[0]]
for c in node[1:]:
if isinstance(c, list) and c and isinstance(c[0], str) and c[0] in _NODE_KINDS:
out.append((yield _rename_g(c, m)))
else:
out.append(c)
return out
def ic4a_signature(trm, tpk):
"""IC4 (a), the syntactic reading: for every SIGNATURE with FORM and
IMAGE_FORM, IMAGE_FORM equals FORM with every DOF replaced by its entry's
ENVIRONMENT_QUANTITY, as canonical spellings. [pass, problems, undecided]:
a signature naming a DOF no entry identifies is undecided (IC2's gap).
Runs on a TrM that is well-formed against a TPK passing T1."""
probs, und = [], []
if not Z._obj(trm):
return [True, [], []]
ents = sorted(_entries_of(trm, "ENTRIES"), key=lambda e: Z._name(e))
q_of = {}
for e in ents:
d, q = _s(e, "DOF"), _s(e, "ENVIRONMENT_QUANTITY")
if d is not None and q is not None and d not in q_of:
q_of[d] = q
for sg in _entries_of(trm.get("HEADER"), "SIGNATURE"):
f, im = sg.get("FORM"), sg.get("IMAGE_FORM")
if not (isinstance(f, str) and isinstance(im, str)):
continue
tag = "SIGNATURE:" + Z._name(sg)
try:
tf, ti = _parse(f, "form"), _parse(im, "form")
except _Refused:
continue # the structural check's to report
named = set()
_idents(tf, named)
missing = sorted(n for n in named if n not in q_of)
if missing:
und.append("IC4(a): " + tag + ": DOF " + ", ".join(missing) + " untied, not decided")
continue
got, want = _pr(_rename(tf, q_of)), _pr(ti)
if got != want:
probs.append("IC4(a): " + tag + ": FORM under the entries reads " + got
+ ", not IMAGE_FORM " + want)
p = sorted(set(Z._show(x) for x in probs))
return [not p, p, sorted(set(und))]
# ---- the grammar witnesses, asserted when loaded (S2: unambiguity as a vector) ------
GRAMMAR_WITNESSES = [
("a-b-c", "expression", "a-b-c"),
("a-(b-c)", "expression", "a-(b-c)"),
("a/b*c", "expression", "a/b*c"),
("a/(b*c)", "expression", "a/(b*c)"),
("-a^2", "expression", "-a^2"),
("(-a)^2", "expression", "(-a)^2"),
("a^2^3", "expression", "REFUSED"),
("(a^2)^3", "expression", "(a^2)^3"),
("a+b*c", "expression", "a+b*c"),
("(a+b)*c", "expression", "(a+b)*c"),
("((a))", "expression", "a"),
("a*((b))", "expression", "a*((b))"),
("sqrt((x))", "expression", "sqrt(x)"),
("x^(-1)", "expression", "x^(-1)"),
("x^(1/2)", "expression", "x^(1/2)"),
("x^02", "expression", "x^2"),
("0.50*x", "expression", "5e-1*x"),
("100*x", "expression", "1e2*x"),
("D(x, t, 1)", "expression", "D(x,t)"),
("m * D(v, t) = -k_s * x", "equation", "m*D(v,t)=-k_s*x"),
("(a)=(b)", "equation", "a=b"),
("a or b and c", "predicate", "REFUSED"),
("x<1 or y>2 and z=3", "predicate", "x<1 or y>2 and z=3"),
("(x<1 or y>2) and z=3", "predicate", "(x<1 or y>2) and z=3"),
("not x<1 and y>2", "predicate", "not x<1 and y>2"),
("not (x<1 and y>2)", "predicate", "not (x<1 and y>2)"),
("(x+1)<2", "predicate", "x+1<2"),
("(x<1)", "predicate", "x<1"),
("abs( x ) < x_max", "predicate", "abs(x)<x_max"),
("a--b", "expression", "REFUSED"),
("a*-b", "expression", "REFUSED"),
("2x", "expression", "REFUSED"),
("0.05 m", "expression", "REFUSED"),
]
GRAMMAR_WITNESS_COUNT = 33
def _assert_grammar():
assert len(GRAMMAR_WITNESSES) == GRAMMAR_WITNESS_COUNT
for text, mode, want in GRAMMAR_WITNESSES:
r = parse_form(text, mode)
got = r[1] if r[0] == "OK" else "REFUSED"
assert got == want, (text, want, got)
if r[0] == "OK":
assert parse_form(r[1], mode)[1] == r[1], ("canonical form does not round-trip", text)
_assert_grammar()