The Principia Machina/TPC-PY/tpc module.py: Difference between revisions
m 1 revision imported |
TPC-PY source tpc_module.py (0.1.1), SHA-256 d68e993487ff39b7; conformed TPS 0.4.0; PROPOSED, not declared (TPC-PY 0.2.0) |
||
| Line 51: | Line 51: | ||
import tpc_identity as ID | import tpc_identity as ID | ||
VERSION = "0.1. | VERSION = "0.1.1" # proposed PATCH with TPC-PY 0.2.0 (C-MS-5: the TPK handed to the zone functions keeps {} apart from []); 0.1.0: P2-04, S48-S54 | ||
TPC_MODULE_VERSION = VERSION | TPC_MODULE_VERSION = VERSION | ||
MAX_BYTES = 262144 # RD-MS-16 (ESTIMATE) | MAX_BYTES = 262144 # RD-MS-16 (ESTIMATE) | ||
Revision as of 02:10, 30 September 2026
# -*- coding: utf-8 -*-
"""
TPC-PY --- environment modules: the module text and its digest, the binding,
the expansion into a draft's TPK, the interview check, the catalogue state,
the declaration checks and the views (tpc_module 0.1.0, PROPOSED; D178.1
(a)-(g); rulings S48-S54 of RULINGS_P8)
=========================================================================
Standard library only; Python 3.8+; Windows/Linux. Spec: tpm_module_spec
0.2.0, which states every rule, every check order and every message this
module implements; section references below are that spec's. Vectors:
vectors/module_corpus.json (gen_module_corpus.py 0.2.0, written before this
module: VECTORS FIRST). TPC-PHP mirrors it operation for operation
(tpc_php/tpc_module.php).
THE ELEVEN FUNCTIONS (section 6): module_parse, module_digest, module_bind,
module_expand, module_verify, interview_check, not_included_lines,
catalogue_state, module_check, draft_module_status, module_use_view; and
run_case(fn, args), the corpus entry (6.12), which renders a result as JSON
text (2.3) and module_expand by its RENDER rule (6.4).
WHAT IT REUSES, NEVER RE-IMPLEMENTS. The strict JSON reader's lexer is
tpc_identity's (_Parser: strings, numbers, white space; CJ1-CJ4), driven here
to produce values (2.7). Text safety, blankness, NFC and echo safety are
tpc_zone's (_first_bad, _blank, _text, _show); DIMENSION and decimals are
tpc_zone's (normalize_dimension, dimension_out_of_range, canon_decimal,
_dec_sign, _is_ident); UNIT is tpc_units.unit_parse; forms are tpc_form's
(form_tree, parse_form, form_names and its printer _pr); T1 is
tpc_zone.t1_well_formed; the equation-of-motion map is tpc_eom.eom_map; the
kernel tests and T3 at depth 1 are tpc_tests.kernel_tests and
tpc_tests.t3_consistency (module_check's rows: the checks check_draft runs);
D(TPK) is tpc_zone.d_tpk; a merge compares tpc_zone._entry_list; every
digest is tpc_digest.digest_fields. The module digest (section 4, S49) is
digest_fields(["TPC-MODULE", "1", canonical text]) and reads none of
tpc_zone's, tpc_form's or tpc_units' spellings.
NEVER RAISES on bad input: a refusal is ["REFUSED", reason], the first
problem in the spec's check order, every reason passed through
tpc_zone._show (TPS 2.5.14). Every walk of a form tree runs on an explicit
stack, so no template depth reaches Python's recursion limit.
"""
import json
import re
import tpc_zone as Z
import tpc_form as F
import tpc_units as U
import tpc_digest as G
import tpc_tests as K
import tpc_eom as EO
import tpc_identity as ID
VERSION = "0.1.1" # proposed PATCH with TPC-PY 0.2.0 (C-MS-5: the TPK handed to the zone functions keeps {} apart from []); 0.1.0: P2-04, S48-S54
TPC_MODULE_VERSION = VERSION
MAX_BYTES = 262144 # RD-MS-16 (ESTIMATE)
NOT_INTEGER = 0.5 # the reader's NOT-AN-INTEGER value (2.7): every field refuses it
NOTJSON = "MODULE: the text is not JSON (RFC 8259, strict)"
FNS = ["module_parse", "module_digest", "module_bind", "module_expand", "module_verify",
"interview_check", "not_included_lines", "catalogue_state", "module_check",
"draft_module_status", "module_use_view"]
TOP = ["ID", "VERSION", "TITLE", "SOURCE", "PREREQUISITES", "PARAMETERS", "SUMS", "TERMS",
"ASSUMPTIONS", "BOUNDARIES", "NOT_CHOSEN", "NOT_INCLUDED", "EXCLUDES", "INTERACTS_WITH",
"TEST_BINDINGS"]
FIELD_ORDER = {
"PREREQUISITES": ["SLOT", "KIND", "DIMENSION", "MIN", "MAX", "LABEL"],
"PARAMETERS": ["NAME", "DIMENSION", "SUPPLY", "LABEL", "VALUE", "UNIT", "UNCERTAINTY",
"OVERRIDABLE"],
"SUMS": ["NAME", "OVER", "EACH"],
"TERMS": ["TARGET", "SIGN", "EXPR", "LABEL"],
"ASSUMPTIONS": ["NAME", "PROPOSITION", "REFS"],
"BOUNDARIES": ["NAME", "PREDICATE", "CONDITION"],
"INTERACTS_WITH": ["WITH", "QUESTION_ID", "QUESTION", "YES_LINE", "NO_LINE"],
"TEST_BINDINGS": ["NAME", "TPK", "BIND", "VALUES", "ANSWERS"],
}
ACTS = {
"MODULE ADD": ["ID", "VERSION", "DIGEST", "DATE"],
"MODULE VERSION": ["ID", "VERSION", "DIGEST", "DATE"],
"MODULE RETIRE": ["ID", "VERSION", "DATE"],
"MODULE REINSTATE": ["ID", "VERSION", "DATE"],
"MODULE WITHDRAW": ["ID", "VERSION", "REASON", "DATE"],
}
CLAIM_FIELDS = ["ID", "VERSION", "DIGEST", "BIND", "VALUES", "ANSWERS"]
CATCH_LINE = "Any interaction not listed under INCLUDED is absent from this kernel."
_RX_MODULE_ID = re.compile(r"[A-Z][A-Z0-9]*(-[A-Z0-9]+)*\Z")
_RX_VERSION = re.compile(r"(0|[1-9][0-9]{0,3})\.(0|[1-9][0-9]{0,3})\.(0|[1-9][0-9]{0,3})\Z")
_RX_SLOT = re.compile(r"[A-Z][A-Z0-9_]*\Z")
_RX_DIGEST = re.compile(r"[0-9a-f]{64}\Z")
_RX_DATE = re.compile(r"([0-9]{4})-([0-9]{2})-([0-9]{2})\Z")
_RX_INT = re.compile(r"-?(0|[1-9][0-9]{0,3})\Z")
class _Refused(Exception):
pass
def _R(msg):
raise _Refused(msg)
def _refuse(msg):
return ["REFUSED", Z._show(msg)]
# ---- value types (2.1) -------------------------------------------------------------------
def _is_str(x):
return type(x) is str
def _is_int(x):
return type(x) is int
def _is_obj(x):
return type(x) is dict
def _is_list(x):
return type(x) is list
def _str_list(x):
return _is_list(x) and all(_is_str(e) for e in x)
def _keys(o):
return sorted(o.keys())
# ---- patterns (2.6) ------------------------------------------------------------------------
def _is_module_id(s):
return _is_str(s) and len(s) <= 32 and _RX_MODULE_ID.match(s) is not None
def _is_pattern(s):
if _is_module_id(s):
return True
return _is_str(s) and s.endswith("-*") and _is_module_id(s[:-2])
def _matches(p, mid):
if p.endswith("-*"):
return mid.startswith(p[:-1])
return mid == p
def _is_version(s):
return _is_str(s) and _RX_VERSION.match(s) is not None
def _vkey(v):
return tuple(int(x) for x in v.split("."))
def _is_slot(s):
return _is_str(s) and len(s) <= 32 and _RX_SLOT.match(s) is not None
def _is_entry_name(s):
return (Z._is_ident(s) and len(s) <= 64
and any("a" <= c <= "z" for c in s))
def _is_answer_key(k):
if _is_slot(k):
return True
return _is_str(k) and k.startswith("FIXED:") and Z._is_ident(k[6:])
def _is_digest(s):
return _is_str(s) and _RX_DIGEST.match(s) is not None
def _is_date(s):
if not _is_str(s):
return False
m = _RX_DATE.match(s)
if m is None:
return False
y, mo, d = int(m.group(1)), int(m.group(2)), int(m.group(3))
if y < 1 or mo < 1 or mo > 12 or d < 1:
return False
days = [31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31][mo - 1]
if mo == 2 and (y % 4 == 0 and (y % 100 != 0 or y % 400 == 0)):
days = 29
return d <= days
def _least_dup(names):
seen, dup = set(), []
for n in names:
if n in seen:
dup.append(n)
seen.add(n)
return min(dup) if dup else None
# ---- the strict reader (2.7): tpc_identity's lexer, driven to values -----------------------
def _rd_value(p, depth):
if depth > ID.MAX_DEPTH:
p.fail()
p.ws()
if p.i >= p.n:
p.fail()
c = p.t[p.i]
if c == "{":
return _rd_obj(p, depth)
if c == "[":
return _rd_arr(p, depth)
if c == '"':
return p.string()
if c == "-" or "0" <= c <= "9":
start = p.i
p.number()
lit = p.t[start:p.i]
return int(lit) if _RX_INT.match(lit) else NOT_INTEGER
for lit, v in (("true", True), ("false", False), ("null", None)):
if p.t.startswith(lit, p.i):
p.i += len(lit)
return v
p.fail()
def _rd_obj(p, depth):
p.i += 1
out = {}
p.ws()
if p.i < p.n and p.t[p.i] == "}":
p.i += 1
return out
while True:
p.ws()
if p.i >= p.n or p.t[p.i] != '"':
p.fail()
k = p.string()
if "\x00" in k: # C-MS-6: no residence object holds it
p.fail()
p.ws()
if p.i >= p.n or p.t[p.i] != ":":
p.fail()
p.i += 1
v = _rd_value(p, depth + 1)
if k in out:
p.fail()
out[k] = v
p.ws()
if p.i >= p.n:
p.fail()
if p.t[p.i] == ",":
p.i += 1
continue
if p.t[p.i] == "}":
p.i += 1
return out
p.fail()
def _rd_arr(p, depth):
p.i += 1
out = []
p.ws()
if p.i < p.n and p.t[p.i] == "]":
p.i += 1
return out
while True:
out.append(_rd_value(p, depth + 1))
p.ws()
if p.i >= p.n:
p.fail()
if p.t[p.i] == ",":
p.i += 1
continue
if p.t[p.i] == "]":
p.i += 1
return out
p.fail()
def _read(text):
p = ID._Parser(text)
try:
v = _rd_value(p, 0)
p.ws()
if p.i != p.n:
p.fail()
except ValueError:
_R(NOTJSON)
return v
# ---- field checks (2.8, 2.9) ---------------------------------------------------------------
def _fields(tag, o, req, opt=()):
allowed = list(req) + list(opt)
for k in _keys(o):
if k not in allowed:
_R(tag + ": unknown field " + k)
for f in req:
if f not in o:
_R(tag + ": missing field " + f)
def _str(tag, f, v, blank_ok=True):
if not _is_str(v):
_R(tag + ": field " + f + " has the wrong type")
bad = Z._first_bad(v)
if bad is not None:
_R(tag + ": field " + f + " contains disallowed character " + bad)
if not blank_ok and Z._blank(v):
_R(tag + ": field " + f + " is blank")
return v
def _strs(tag, f, v, cap=None):
if not _str_list(v):
_R(tag + ": field " + f + " has the wrong type")
if cap is not None and len(v) > cap:
_R(tag + ": field " + f + " has more than %d entries" % cap)
for x in v:
bad = Z._first_bad(x)
if bad is not None:
_R(tag + ": field " + f + " contains disallowed character " + bad)
return v
def _objs(tag, f, v, cap):
if not (_is_list(v) and all(_is_obj(e) for e in v)):
_R(tag + ": field " + f + " has the wrong type")
if len(v) > cap:
_R(tag + ": field " + f + " has more than %d entries" % cap)
return v
def _dimension(tag, v):
d = Z.normalize_dimension(v)
if d is None:
if Z.dimension_out_of_range(v):
_R(tag + ": DIMENSION " + v + ": an exponent is out of range")
_R(tag + ": DIMENSION " + v + " is not a dimension")
return d
def _tag(prefix, e, field):
v = e.get(field)
return prefix + (v if _is_str(v) else "?")
# ---- form trees: explicit stacks --------------------------------------------------------------
def _nodes(tree):
out, stack = [], [tree]
while stack:
n = stack.pop()
out.append(n)
for c in reversed(n[1:]):
if _is_list(c) and c and _is_str(c[0]) and c[0] in F._NODE_KINDS:
stack.append(c)
return out
def _idents(tree):
acc = set()
for n in _nodes(tree):
if n[0] == "id":
acc.add(n[1])
elif n[0] == "D":
acc.add(n[1])
acc.add(n[2])
return sorted(acc)
def _has_d(tree):
return any(n[0] == "D" for n in _nodes(tree))
def _subst(tree, m):
"""The tree with every ["id", x] for x in m replaced by m[x] (a node); a
post-order rebuild on an explicit stack."""
stack = [(tree, False)]
done = []
while stack:
n, visited = stack.pop()
if n[0] == "id":
done.append(m[n[1]] if n[1] in m else n)
continue
kids = [i for i, c in enumerate(n) if i > 0 and _is_list(c) and c and _is_str(c[0])
and c[0] in F._NODE_KINDS]
if not kids:
done.append(n)
continue
if not visited:
stack.append((n, True))
for i in reversed(kids):
stack.append((n[i], False))
continue
vals = done[len(done) - len(kids):]
del done[len(done) - len(kids):]
out = list(n)
for i, v in zip(kids, vals):
out[i] = v
done.append(out)
return done[0]
def _strip(n):
while n[0] in ("paren", "pparen"):
n = n[1]
return n
def _factors(side):
num, den, stack = [], [], [side]
while stack:
n = stack.pop()
k = n[0]
if k in ("paren", "neg"):
stack.append(n[1])
elif k == "bin" and n[1] == "*":
stack.append(n[3])
stack.append(n[2])
elif k == "bin" and n[1] == "/":
den.append(n[3])
stack.append(n[2])
else:
num.append(n)
return num, den
def _shaped(side, q, consts):
"""tpc_eom's equation-of-motion shape of a side for q (6.4 S7 b)."""
num, den = _factors(side)
ds = [f for f in num if f[0] == "D"]
if len(ds) != 1 or ds[0][1] != q:
return False
rest = [f for f in num if f[0] != "D"] + den
return all(all(x in consts for x in _idents(f)) for f in rest)
# ---- the module text (section 3) ----------------------------------------------------------------
def _placeholders(tag, s, slots):
i, n = 0, len(s)
while i < n:
c = s[i]
if c == "}":
_R(tag + ": a brace outside a {SLOT} placeholder")
if c == "{":
j = s.find("}", i + 1)
if j < 0:
_R(tag + ": a brace outside a {SLOT} placeholder")
x = s[i + 1:j]
if x not in slots:
_R(tag + ": {" + x + "} is not a slot of this module")
i = j + 1
else:
i += 1
def _value_object(tag, v, dim):
"""6.3 B4's VALUE OBJECT checks; tag "VALUES: <p>" (with any prefix)."""
if not _is_obj(v):
_R(tag + " has the wrong type")
for k in _keys(v):
if k not in ("VALUE", "UNIT", "UNCERTAINTY"):
_R(tag + ": unknown field " + k)
if "VALUE" in v and "UNIT" not in v:
_R(tag + ": VALUE requires UNIT")
if "UNIT" in v and "VALUE" not in v:
_R(tag + ": UNIT requires VALUE")
if "UNCERTAINTY" in v and "VALUE" not in v:
_R(tag + ": UNCERTAINTY requires VALUE")
for f in ("VALUE", "UNIT", "UNCERTAINTY"):
if f not in v:
continue
x = _str(tag, f, v[f])
if f == "VALUE" and Z.canon_decimal(x) is None:
_R(tag + ": VALUE " + x + " is not a decimal")
if f == "UNIT":
r = U.unit_parse(x)
if r[0] != "OK":
_R(tag + ": " + r[1])
if f == "UNCERTAINTY":
if Z.canon_decimal(x) is None:
_R(tag + ": UNCERTAINTY " + x + " is not a decimal")
if Z._dec_sign(x) < 0:
_R(tag + ": UNCERTAINTY " + x + " is negative")
if "UNIT" in v:
ud = U.unit_parse(v["UNIT"])[2]
if ud != dim:
_R(tag + ": UNIT " + v["UNIT"] + " has dimension " + ud + ", not " + dim)
def _form_tree(tag, field, text, mode):
r = F.form_tree(text, mode)
if r[0] != "OK":
_R(tag + ": " + field + " does not parse: " + r[1])
return r[1]
def _parse(text):
"""module_parse's checks (section 3); the parsed module as a dict."""
if not _is_str(text):
_R("MODULE: the text is not a string")
if len(text.encode("utf-8", "surrogatepass")) > MAX_BYTES:
_R("MODULE: the text is longer than %d bytes" % MAX_BYTES)
v = _read(text)
if not _is_obj(v):
_R("MODULE: the text is not a JSON object")
_fields("MODULE", v, TOP)
mid = _str("MODULE", "ID", v["ID"])
if not _is_module_id(mid):
_R("MODULE: ID " + mid + " is not a module ID")
ver = _str("MODULE", "VERSION", v["VERSION"])
if not _is_version(ver):
_R("MODULE: VERSION " + ver + " is not a version")
_str("MODULE", "TITLE", v["TITLE"], False)
_str("MODULE", "SOURCE", v["SOURCE"], False)
M = {"ID": mid, "VERSION": ver, "VALUE": v, "TEXT": text}
# 3.2 PREREQUISITES
slots = []
for e in _objs("MODULE", "PREREQUISITES", v["PREREQUISITES"], 16):
tag = _tag("PREREQUISITE:", e, "SLOT")
_fields(tag, e, FIELD_ORDER["PREREQUISITES"])
s = _str(tag, "SLOT", e["SLOT"])
if not _is_slot(s):
_R(tag + ": SLOT " + s + " is not a slot name")
k = _str(tag, "KIND", e["KIND"])
if k not in ("DOF", "CONSTANT"):
_R(tag + ": KIND " + k + " is not DOF or CONSTANT")
d = _dimension(tag, _str(tag, "DIMENSION", e["DIMENSION"]))
for f in ("MIN", "MAX"):
x = e[f]
if not (_is_int(x) and 1 <= x <= 16):
_R(tag + ": " + f + " is not an integer from 1 to 16")
_str(tag, "LABEL", e["LABEL"], False)
if e["MIN"] > e["MAX"]:
_R(tag + ": MIN is greater than MAX")
if k == "CONSTANT" and not (e["MIN"] == 1 and e["MAX"] == 1):
_R(tag + ": a CONSTANT slot takes exactly one name")
slots.append({"SLOT": s, "KIND": k, "DIM": d, "MIN": e["MIN"], "MAX": e["MAX"]})
dup = _least_dup([s["SLOT"] for s in slots])
if dup is not None:
_R("MODULE: duplicate slot " + dup)
slot_of = dict((s["SLOT"], s) for s in slots)
M["SLOTS"], M["SLOT_OF"] = slots, slot_of
# 3.3 PARAMETERS
params = []
for e in _objs("MODULE", "PARAMETERS", v["PARAMETERS"], 32):
tag = _tag("PARAMETER:", e, "NAME")
_fields(tag, e, FIELD_ORDER["PARAMETERS"][:4], FIELD_ORDER["PARAMETERS"][4:])
n = _str(tag, "NAME", e["NAME"])
if not _is_entry_name(n):
_R(tag + ": NAME " + n + " is not an entry name (an identifier with a lower-case "
"letter)")
d = _dimension(tag, _str(tag, "DIMENSION", e["DIMENSION"]))
sup = _str(tag, "SUPPLY", e["SUPPLY"])
if sup not in ("DECLARED", "AUTHOR"):
_R(tag + ": SUPPLY " + sup + " is not DECLARED or AUTHOR")
_str(tag, "LABEL", e["LABEL"], False)
if "VALUE" in e:
x = _str(tag, "VALUE", e["VALUE"])
if Z.canon_decimal(x) is None:
_R(tag + ": VALUE " + x + " is not a decimal")
if "UNIT" in e:
r = U.unit_parse(_str(tag, "UNIT", e["UNIT"]))
if r[0] != "OK":
_R(tag + ": " + r[1])
if "UNCERTAINTY" in e:
x = _str(tag, "UNCERTAINTY", e["UNCERTAINTY"])
if Z.canon_decimal(x) is None:
_R(tag + ": UNCERTAINTY " + x + " is not a decimal")
if Z._dec_sign(x) < 0:
_R(tag + ": UNCERTAINTY " + x + " is negative")
if "OVERRIDABLE" in e:
o = _str(tag, "OVERRIDABLE", e["OVERRIDABLE"])
if o not in ("YES", "NO"):
_R(tag + ": OVERRIDABLE " + o + " is not YES or NO")
if sup == "DECLARED":
for f in ("VALUE", "UNIT", "OVERRIDABLE"):
if f not in e:
_R(tag + ": DECLARED requires " + f)
else:
for f in ("VALUE", "UNIT", "UNCERTAINTY", "OVERRIDABLE"):
if f in e:
_R(tag + ": AUTHOR forbids " + f)
if "UNIT" in e:
ud = U.unit_parse(e["UNIT"])[2]
if ud != d:
_R(tag + ": UNIT " + e["UNIT"] + " has dimension " + ud + ", not " + d)
params.append({"NAME": n, "DIM": d, "SUPPLY": sup, "VALUE": e.get("VALUE"),
"UNIT": e.get("UNIT"), "UNCERTAINTY": e.get("UNCERTAINTY"),
"OVERRIDABLE": e.get("OVERRIDABLE")})
dup = _least_dup([p["NAME"] for p in params])
if dup is not None:
_R("MODULE: duplicate parameter " + dup)
pnames = set(p["NAME"] for p in params)
M["PARAMS"], M["PARAM_OF"] = params, dict((p["NAME"], p) for p in params)
# 3.4 SUMS
sums = []
for e in _objs("MODULE", "SUMS", v["SUMS"], 16):
tag = _tag("SUM:", e, "NAME")
_fields(tag, e, FIELD_ORDER["SUMS"])
n = _str(tag, "NAME", e["NAME"])
if not _is_slot(n):
_R(tag + ": NAME " + n + " is not a slot name")
if n in slot_of:
_R(tag + ": NAME " + n + " is the name of a slot")
o = _str(tag, "OVER", e["OVER"])
if o not in slot_of or slot_of[o]["KIND"] != "DOF":
_R(tag + ": OVER " + o + " is not a DOF slot")
tree = _form_tree(tag, "EACH", _str(tag, "EACH", e["EACH"]), "expression")
if _has_d(tree):
_R(tag + ": EACH uses D")
for x in _idents(tree):
if x != o and x not in pnames:
_R(tag + ": EACH names " + x + ", which is not " + o + " or a parameter")
sums.append({"NAME": n, "OVER": o, "TREE": tree, "CANON": F._pr(tree)})
dup = _least_dup([s["NAME"] for s in sums])
if dup is not None:
_R("MODULE: duplicate sum " + dup)
sum_of = dict((s["NAME"], s) for s in sums)
M["SUMS"], M["SUM_OF"] = sums, sum_of
# 3.5 TERMS
terms = []
for i, e in enumerate(_objs("MODULE", "TERMS", v["TERMS"], 16), 1):
tag = "TERM:%d" % i
_fields(tag, e, FIELD_ORDER["TERMS"])
t = _str(tag, "TARGET", e["TARGET"])
if t not in slot_of or slot_of[t]["KIND"] != "DOF":
_R(tag + ": TARGET " + t + " is not a DOF slot")
sg = _str(tag, "SIGN", e["SIGN"])
if sg not in ("+", "-"):
_R(tag + ": SIGN " + sg + " is not + or -")
tree = _form_tree(tag, "EXPR", _str(tag, "EXPR", e["EXPR"]), "expression")
canon = F._pr(tree)
if canon.startswith("-"):
_R(tag + ": EXPR begins with a minus sign; the sign is SIGN's")
if _has_d(tree):
_R(tag + ": EXPR uses D")
for x in _idents(tree):
s = slot_of.get(x)
if s is not None and s["MAX"] > 1 and x != t:
_R(tag + ": EXPR names the list slot " + x + " outside its own TERM")
if not (s is not None or x in pnames or x in sum_of):
_R(tag + ": EXPR names " + x + ", which is not a slot, parameter or sum of this "
"module")
lab = _str(tag, "LABEL", e["LABEL"], False)
terms.append({"TARGET": t, "SIGN": sg, "TREE": tree, "CANON": canon, "LABEL": lab})
M["TERMS"] = terms
# 3.6 ASSUMPTIONS
asms = []
for e in _objs("MODULE", "ASSUMPTIONS", v["ASSUMPTIONS"], 32):
tag = _tag("ASSUMPTION:", e, "NAME")
_fields(tag, e, FIELD_ORDER["ASSUMPTIONS"])
n = _str(tag, "NAME", e["NAME"])
if not _is_entry_name(n):
_R(tag + ": NAME " + n + " is not an entry name (an identifier with a lower-case "
"letter)")
prop = _str(tag, "PROPOSITION", e["PROPOSITION"], False)
_placeholders(tag + ": PROPOSITION", prop, slot_of)
refs = _strs(tag, "REFS", e["REFS"])
if len(set(refs)) != len(refs):
_R(tag + ": field REFS has duplicate entries")
for r in refs:
if r not in slot_of and r not in pnames:
_R(tag + ": REFS " + r + " is not a slot or parameter of this module")
asms.append({"NAME": n, "PROPOSITION": prop, "REFS": refs})
dup = _least_dup([p["NAME"] for p in params] + [a["NAME"] for a in asms])
if dup is not None:
_R("MODULE: duplicate entry name " + dup)
M["ASSUMPTIONS"] = asms
# 3.7 BOUNDARIES
bnds = []
for e in _objs("MODULE", "BOUNDARIES", v["BOUNDARIES"], 16):
tag = _tag("BOUNDARY:", e, "NAME")
_fields(tag, e, FIELD_ORDER["BOUNDARIES"])
n = _str(tag, "NAME", e["NAME"])
if not _is_entry_name(n):
_R(tag + ": NAME " + n + " is not an entry name (an identifier with a lower-case "
"letter)")
pred = _str(tag, "PREDICATE", e["PREDICATE"], False)
_placeholders(tag + ": PREDICATE", pred, slot_of)
tree = _form_tree(tag, "CONDITION", _str(tag, "CONDITION", e["CONDITION"]), "predicate")
for x in _idents(tree):
s = slot_of.get(x)
if s is not None and s["MAX"] > 1:
_R(tag + ": CONDITION names the list slot " + x + " outside a sum")
if not (s is not None or x in pnames or x in sum_of):
_R(tag + ": CONDITION names " + x + ", which is not a slot, parameter or sum "
"of this module")
bnds.append({"NAME": n, "PREDICATE": pred, "TREE": tree, "CANON": F._pr(tree)})
dup = _least_dup([p["NAME"] for p in params] + [a["NAME"] for a in asms]
+ [b["NAME"] for b in bnds])
if dup is not None:
_R("MODULE: duplicate entry name " + dup)
M["BOUNDARIES"] = bnds
# 3.1 the lines and the references
M["NOT_CHOSEN"] = _str("MODULE", "NOT_CHOSEN", v["NOT_CHOSEN"], False)
ni = _strs("MODULE", "NOT_INCLUDED", v["NOT_INCLUDED"], 32)
for i, x in enumerate(ni, 1):
if Z._blank(x):
_R("MODULE: NOT_INCLUDED %d is blank" % i)
if len(set(ni)) != len(ni):
_R("MODULE: field NOT_INCLUDED has duplicate entries")
M["NOT_INCLUDED"] = ni
ex = _strs("MODULE", "EXCLUDES", v["EXCLUDES"], 32)
for p in ex:
if not _is_pattern(p):
_R("MODULE: EXCLUDES " + p + " is not a module ID or pattern")
if _matches(p, mid):
_R("MODULE: EXCLUDES " + p + " matches the module's own ID")
if len(set(ex)) != len(ex):
_R("MODULE: field EXCLUDES has duplicate entries")
M["EXCLUDES"] = ex
# 3.8 INTERACTS_WITH
qs = []
for i, e in enumerate(_objs("MODULE", "INTERACTS_WITH", v["INTERACTS_WITH"], 16), 1):
tag = "INTERACTS_WITH:%d" % i
_fields(tag, e, FIELD_ORDER["INTERACTS_WITH"])
w = _str(tag, "WITH", e["WITH"])
if not _is_pattern(w):
_R(tag + ": WITH " + w + " is not a module ID or pattern")
if _matches(w, mid):
_R(tag + ": WITH " + w + " matches the module's own ID")
q = _str(tag, "QUESTION_ID", e["QUESTION_ID"])
if not _is_slot(q):
_R(tag + ": QUESTION_ID " + q + " is not a question ID")
for f in ("QUESTION", "YES_LINE", "NO_LINE"):
_str(tag, f, e[f], False)
qs.append({"WITH": w, "QID": q, "YES": e["YES_LINE"], "NO": e["NO_LINE"]})
dup = _least_dup([q["QID"] for q in qs])
if dup is not None:
_R("MODULE: duplicate question " + dup)
M["QUESTIONS"] = qs
# 3.9 TEST_BINDINGS
tb = v["TEST_BINDINGS"]
if not (_is_list(tb) and all(_is_obj(e) for e in tb)):
_R("MODULE: field TEST_BINDINGS has the wrong type")
if not tb:
_R("MODULE: field TEST_BINDINGS is empty (a module declares at least one test binding)")
if len(tb) > 8:
_R("MODULE: field TEST_BINDINGS has more than 8 entries")
bindings = []
for e in tb:
tag = _tag("TEST_BINDING:", e, "NAME")
_fields(tag, e, FIELD_ORDER["TEST_BINDINGS"])
n = _str(tag, "NAME", e["NAME"])
if not _is_slot(n):
_R(tag + ": NAME " + n + " is not a binding name")
tpk = e["TPK"]
if not _is_obj(tpk):
_R(tag + ": field TPK has the wrong type")
t1 = Z.t1_well_formed(tpk)
if not t1[0]:
_R(tag + ": TPK fails T1: " + t1[1][0])
b = e["BIND"]
if not _is_obj(b):
_R(tag + ": field BIND has the wrong type")
for k in _keys(b):
if k not in slot_of:
_R(tag + ": BIND: unknown slot " + k)
for s in slots:
if s["SLOT"] not in b:
_R(tag + ": BIND: slot " + s["SLOT"] + " is not bound")
for s in slots:
if not _str_list(b[s["SLOT"]]):
_R(tag + ": BIND: slot " + s["SLOT"] + " has the wrong type")
vals = e["VALUES"]
if not _is_obj(vals):
_R(tag + ": field VALUES has the wrong type")
for k in _keys(vals):
if k not in M["PARAM_OF"]:
_R(tag + ": VALUES: unknown parameter " + k)
for k in _keys(vals):
x = vals[k]
if _is_obj(x) and not x:
continue
_value_object(tag + ": VALUES: " + k, x, M["PARAM_OF"][k]["DIM"])
ans = e["ANSWERS"]
if not _is_obj(ans):
_R(tag + ": field ANSWERS has the wrong type")
for k in _keys(ans):
if not _is_answer_key(k):
_R(tag + ": ANSWERS: " + k + " is not a question")
if not (_is_str(ans[k]) and ans[k] in ("YES", "NO")):
_R(tag + ": ANSWERS: " + k + " is not YES or NO")
bindings.append({"NAME": n, "TPK": tpk, "BIND": b, "VALUES": vals, "ANSWERS": ans})
dup = _least_dup([b["NAME"] for b in bindings])
if dup is not None:
_R("MODULE: duplicate test binding " + dup)
M["BINDINGS"] = bindings
return M
# ---- the canonical text and the digest (section 4, S49) ---------------------------------------
def _ct_str(s):
out = ['"']
for ch in Z._text(s):
if ch == '"' or ch == "\\":
out.append("\\" + ch)
elif ord(ch) < 0x20:
out.append("\\u%04x" % ord(ch))
else:
out.append(ch)
out.append('"')
return "".join(out)
def _ct_value(v):
if v is True:
return "true"
if v is False:
return "false"
if v is None or type(v) is float: # unreachable: module_parse refuses them
return "null"
if _is_str(v):
return _ct_str(v)
if _is_int(v):
return str(v)
if _is_list(v):
return "[" + ",".join(_ct_value(x) for x in v) + "]"
return "{" + ",".join(_ct_str(k) + ":" + _ct_value(v[k]) for k in _keys(v)) + "}"
def _canonical_text(v):
parts = []
for k in TOP:
x = v[k]
if k in FIELD_ORDER:
order = FIELD_ORDER[k]
parts.append(_ct_str(k) + ":[" + ",".join(
"{" + ",".join(_ct_str(f) + ":" + _ct_value(e[f]) for f in order if f in e) + "}"
for e in x) + "]")
else:
parts.append(_ct_str(k) + ":" + _ct_value(x))
return "{" + ",".join(parts) + "}"
def _digest(M):
if "DIGEST" not in M:
M["DIGEST"] = G.digest_fields(["TPC-MODULE", "1", _canonical_text(M["VALUE"])])
return M["DIGEST"]
# ---- 5.1 claims, 5.2 modules -----------------------------------------------------------------
def _claims(claims):
if not _is_list(claims):
_R("CLAIMS: not a list")
out = []
for i, c in enumerate(claims, 1):
tag = "CLAIM %d" % i
if not _is_obj(c):
_R(tag + ": not an object")
_fields(tag, c, CLAIM_FIELDS)
if not _is_module_id(c["ID"]):
_R(tag + ": ID is not a module ID")
if not _is_version(c["VERSION"]):
_R(tag + ": VERSION is not a version")
if not _is_digest(c["DIGEST"]):
_R(tag + ": DIGEST is not a digest")
if not (_is_obj(c["BIND"]) and all(_str_list(c["BIND"][k]) for k in c["BIND"])):
_R(tag + ": field BIND has the wrong type")
if not (_is_obj(c["VALUES"]) and all(_is_obj(c["VALUES"][k]) for k in c["VALUES"])):
_R(tag + ": field VALUES has the wrong type")
if not (_is_obj(c["ANSWERS"]) and all(_is_str(c["ANSWERS"][k]) for k in c["ANSWERS"])):
_R(tag + ": field ANSWERS has the wrong type")
out.append(c)
dup = _least_dup([c["ID"] for c in out])
if dup is not None:
_R("CLAIMS: duplicate module " + dup)
return sorted(out, key=lambda c: c["ID"])
def _modules(modules):
if not _str_list(modules):
_R("MODULES: not a list of texts")
out = []
for i, t in enumerate(modules, 1):
try:
out.append(_parse(t))
except _Refused as e:
_R("MODULES %d: %s" % (i, e))
pairs = sorted((m["ID"], m["VERSION"]) for m in out)
for a, b in zip(pairs, pairs[1:]):
if a == b:
_R("MODULES: duplicate text of " + a[0] + " " + a[1])
return dict(((m["ID"], m["VERSION"]), m) for m in out)
def _declared_texts(texts, state):
for key in sorted(texts):
if key not in state["V"]:
_R("MODULES: " + key[0] + " " + key[1] + " is not declared")
if _digest(texts[key]) != state["V"][key]["DIGEST"]:
_R("MODULES: " + key[0] + " " + key[1] + ": the text's digest does not match the "
"declaration")
def _claim_texts(claims, texts):
for c in claims:
key = (c["ID"], c["VERSION"])
cv = c["ID"] + " " + c["VERSION"]
if key not in texts:
_R("CLAIM " + cv + ": no module text")
if c["DIGEST"] != _digest(texts[key]):
_R("CLAIM " + cv + ": DIGEST does not match the module text")
def _claims_declared(claims, texts, state):
for c in claims:
key = (c["ID"], c["VERSION"])
cv = c["ID"] + " " + c["VERSION"]
if key not in state["V"]:
_R("CLAIM " + cv + ": not declared")
if c["DIGEST"] != state["V"][key]["DIGEST"]:
_R("CLAIM " + cv + ": DIGEST does not match the declaration")
if key not in texts:
_R("CLAIM " + cv + ": no module text")
def _excludes(claims, texts):
for i in range(len(claims)):
for j in range(i + 1, len(claims)):
a, b = claims[i], claims[j]
ma, mb = texts[(a["ID"], a["VERSION"])], texts[(b["ID"], b["VERSION"])]
if (any(_matches(p, b["ID"]) for p in ma["EXCLUDES"])
or any(_matches(p, a["ID"]) for p in mb["EXCLUDES"])):
_R("CLAIMS: " + a["ID"] + " " + a["VERSION"] + " and " + b["ID"] + " "
+ b["VERSION"] + " exclude each other (EXCLUDES)")
# ---- 6.3 module_bind ----------------------------------------------------------------------------
def _t1(tpk):
"""T1 over a draft's TPK: tpc_zone.t1_well_formed, a non-object refused with T1's own
first problem before it is read (TPC-PHP's arrays cannot tell a JSON [] from {})."""
if not _is_obj(tpk):
return [False, ["TPK: zone is not an object"]]
return Z.t1_well_formed(tpk)
def _tpk_entries(tpk, kind):
lst = tpk.get(kind, [])
return lst if _is_list(lst) else []
def _bind(M, tpk, bind, values):
if not _is_obj(bind):
_R("BIND: not an object")
for k in _keys(bind):
if k not in M["SLOT_OF"]:
_R("BIND: unknown slot " + k)
for s in M["SLOTS"]:
if s["SLOT"] not in bind:
_R("BIND: slot " + s["SLOT"] + " is not bound")
bound = []
for s in M["SLOTS"]:
sl = s["SLOT"]
names = bind[sl]
if not _str_list(names):
_R("BIND: slot " + sl + " has the wrong type")
if not (s["MIN"] <= len(names) <= s["MAX"]):
_R("BIND: slot %s takes from %d to %d names, not %d" % (sl, s["MIN"], s["MAX"],
len(names)))
if any(names[i] >= names[i + 1] for i in range(len(names) - 1)):
_R("BIND: slot " + sl + ": the names are not in code point order without repeats")
entries = dict((e.get("NAME"), e) for e in _tpk_entries(tpk, s["KIND"]))
for n in names:
if n not in entries:
_R("BIND: slot " + sl + ": " + n + " is not a " + s["KIND"] + " of the TPK")
d = Z.normalize_dimension(entries[n].get("DIMENSION"))
if d != s["DIM"]:
_R("BIND: slot " + sl + ": " + n + " has dimension " + str(d) + ", not "
+ s["DIM"])
bound.append([sl, list(names)])
where = {}
for sl, names in bound:
for n in names:
where.setdefault(n, []).append(sl)
two = sorted(n for n in where if len(where[n]) > 1)
if two:
n = two[0]
_R("BIND: " + n + " is bound to two slots, " + where[n][0] + " and " + where[n][1])
if not _is_obj(values):
_R("VALUES: not an object")
for k in _keys(values):
if k not in M["PARAM_OF"]:
_R("VALUES: unknown parameter " + k)
rows = []
for p in M["PARAMS"]:
n, tag = p["NAME"], "VALUES: " + p["NAME"]
if p["SUPPLY"] == "DECLARED":
if n not in values:
rows.append([n, "DECLARED", p["VALUE"], p["UNIT"], p["UNCERTAINTY"]])
continue
if p["OVERRIDABLE"] == "NO":
_R(tag + " is not OVERRIDABLE")
x = values[n]
_value_object(tag, x, p["DIM"])
if not x:
_R(tag + ": an override needs VALUE and UNIT")
rows.append([n, "OVERRIDDEN", x.get("VALUE"), x.get("UNIT"), x.get("UNCERTAINTY")])
else:
if n not in values:
_R(tag + " is author supplied: give a value, or {} for a symbolic constant")
x = values[n]
if _is_obj(x) and not x:
rows.append([n, "SYMBOLIC", None, None, None])
continue
_value_object(tag, x, p["DIM"])
rows.append([n, "AUTHOR", x.get("VALUE"), x.get("UNIT"), x.get("UNCERTAINTY")])
return bound, rows
def module_parse(text):
try:
M = _parse(text)
except _Refused as e:
return _refuse(str(e))
return ["OK", M["ID"], M["VERSION"],
[[s["SLOT"], s["KIND"], s["DIM"], s["MIN"], s["MAX"]] for s in M["SLOTS"]],
[[p["NAME"], p["SUPPLY"], p["DIM"]] for p in M["PARAMS"]],
[[s["NAME"], s["OVER"], s["CANON"]] for s in M["SUMS"]],
[[t["TARGET"], t["SIGN"], t["CANON"]] for t in M["TERMS"]],
[a["NAME"] for a in M["ASSUMPTIONS"]],
[[b["NAME"], b["CANON"]] for b in M["BOUNDARIES"]],
sorted(M["EXCLUDES"]),
[[q["WITH"], q["QID"]] for q in M["QUESTIONS"]],
[b["NAME"] for b in M["BINDINGS"]]]
def module_digest(text):
try:
return ["OK", _digest(_parse(text))]
except _Refused as e:
return _refuse(str(e))
def module_bind(tpk, text, bind, values):
try:
M = _parse(text)
t1 = _t1(tpk)
if not t1[0]:
_R("BASE: the TPK fails T1: " + t1[1][0])
bound, rows = _bind(M, tpk, bind, values)
except _Refused as e:
return _refuse(str(e))
return ["OK", [["SLOT", s, n] for s, n in bound],
[["PARAMETER", r[0], r[1]] + [x if x is not None else "" for x in r[2:]]
for r in rows]]
# ---- 6.4 module_expand -------------------------------------------------------------------------
def _expand_template(tree, rename, M, members_of):
"""S9: the template's tree with slots renamed and sums replaced (3.4)."""
m = {}
for x, name in rename.items():
m[x] = ["id", name]
for s in M["SUMS"]:
each = _strip(s["TREE"][1])
terms = [_subst(each, {s["OVER"]: ["id", q]}) for q in members_of[s["OVER"]]]
acc = terms[0]
for t in terms[1:]:
acc = ["bin", "+", acc, t]
m[s["NAME"]] = ["paren", acc]
return _subst(tree, m)
def _expand(draft, claims, modules):
"""(expanded draft, composed, emitted rows, dropped) or raises _Refused."""
if not _is_obj(draft):
_R("DRAFT: not an object")
for k in _keys(draft):
if k not in ("TPK", "TrM", "TMS"):
_R("DRAFT: unknown zone " + k)
if "TPK" not in draft:
_R("DRAFT: missing zone TPK")
tpk = draft["TPK"]
t1 = _t1(tpk)
if not t1[0]:
_R("BASE: the TPK fails T1: " + t1[1][0])
texts = _modules(modules)
cls = _claims(claims)
_claim_texts(cls, texts)
_excludes(cls, texts)
binds = []
for c in cls:
M = texts[(c["ID"], c["VERSION"])]
try:
binds.append(_bind(M, tpk, c["BIND"], c["VALUES"]))
except _Refused as e:
_R("CLAIM " + c["ID"] + " " + c["VERSION"] + ": " + str(e))
MAP = {}
if any(texts[(c["ID"], c["VERSION"])]["TERMS"] for c in cls):
E = EO.eom_map({"TPK": tpk})
if E[0] != "OK":
_R("EXPAND: the structure check refuses the TPK: " + E[1])
for row in E[1]:
if row[0] == "MAP":
for q, label, law in row[1]:
MAP[q] = (label, law)
laws = dict((e.get("NAME"), e) for e in _tpk_entries(tpk, "LAW"))
consts = set(e.get("NAME") for e in _tpk_entries(tpk, "CONSTANT"))
ids = [c["ID"] for c in cls]
receiving = {} # law -> [term records]
dside = {}
dropped_all = []
per_claim_dropped = []
for c, (bound, rows) in zip(cls, binds):
M = texts[(c["ID"], c["VERSION"])]
cv = c["ID"] + " " + c["VERSION"]
ans = c["ANSWERS"]
for k in _keys(ans): # S7 a
if not _is_answer_key(k):
_R("CLAIM " + cv + ": answer " + k + " is not a question")
if ans[k] not in ("YES", "NO"):
_R("CLAIM " + cv + ": answer " + k + " is not YES or NO")
members = dict((s, n) for s, n in bound)
raised = set()
dropped = []
for i, t in enumerate(M["TERMS"], 1): # S7 b
for q in members[t["TARGET"]]:
label, lname = MAP.get(q, ("NO LAW", ""))
pre = "CLAIM " + cv + ": TERM %d: " % i
if label == "DETERMINED":
L = laws[lname]
role = L.get("ROLE")
if role != "EOM(" + q + ")":
_R(pre + q + "'s equation of motion LAW " + lname + " has ROLE "
+ str(role) + ", not EOM(" + q + ")")
r = F.form_tree(L.get("EQUATION"), "equation")
sides = [_shaped(r[1][1], q, consts), _shaped(r[1][2], q, consts)] \
if r[0] == "OK" else [False, False]
if sides.count(True) != 1:
_R(pre + "LAW " + lname + " has no single side of the equation-of-motion "
"shape for " + q)
dside[lname] = 0 if sides[0] else 1
rename = {}
for s in M["SLOTS"]:
if s["MAX"] == 1:
rename[s["SLOT"]] = members[s["SLOT"]][0]
rename[t["TARGET"]] = q
tree = _expand_template(t["TREE"], rename, M, members)
e_j = F._pr(tree)
top = _strip(tree[1])
w_j = "(" + e_j + ")" if top[0] == "bin" and top[1] in ("+", "-") else e_j
receiving.setdefault(lname, []).append((t["SIGN"], e_j, w_j, t["LABEL"]))
elif label == "FIXED":
key = "FIXED:" + q
raised.add(key)
if key not in ans:
_R("CLAIM " + cv + ": question FIXED:" + q + " is not answered (" + q
+ " is FIXED: does a constraint force balance the forces this module "
"adds along it?)")
if ans[key] == "NO":
_R(pre + q + " is FIXED and the answer to FIXED:" + q + " is NO: a force "
"along a fixed DOF with no constraint force balancing it contradicts "
"the constraint")
if q not in dropped:
dropped.append(q)
elif label == "REMOVED":
_R(pre + q + " is REMOVED; no module is bound to a removed DOF")
elif label == "INPUT":
_R(pre + q + " is an INPUT DOF and has no equation of motion")
elif label == "INDEPENDENT":
_R(pre + q + " is the independent variable")
elif label in ("UNDER", "OVER"):
_R(pre + q + "'s equation of motion is not determined (" + label
+ "); resolve it, then bind the module")
else:
_R(pre + q + " has no equation of motion (" + label + "); write it, then "
"bind the module")
for qd in M["QUESTIONS"]: # S7 c
if any(o != c["ID"] and _matches(qd["WITH"], o) for o in ids):
raised.add(qd["QID"])
if qd["QID"] not in ans:
_R("CLAIM " + cv + ": question " + qd["QID"] + " is not answered")
for k in _keys(ans): # S7 d
if k not in raised:
_R("CLAIM " + cv + ": answer " + k + " answers no question raised")
per_claim_dropped.append(dropped)
for q in dropped:
dropped_all.append([cv, q])
# S8 emission
base_names = set()
for kind in Z.TPK_KINDS:
for e in _tpk_entries(tpk, kind):
base_names.add(e.get("NAME"))
emitted = [] # [kind, entry, [sources]]
by_name = {}
for c, (bound, rows), dropped in zip(cls, binds, per_claim_dropped):
M = texts[(c["ID"], c["VERSION"])]
cv = c["ID"] + " " + c["VERSION"]
members = dict((s, n) for s, n in bound)
out = []
for r in rows:
e = {"NAME": r[0], "DIMENSION": M["PARAM_OF"][r[0]]["DIM"]}
for f, x in zip(("VALUE", "UNIT", "UNCERTAINTY"), r[2:]):
if x is not None:
e[f] = x
out.append(("CONSTANT", e))
for a in M["ASSUMPTIONS"]:
refs = set()
for x in a["REFS"]:
if x in members:
refs.update(members[x])
else:
refs.add(x)
out.append(("ASSUMPTION", {"NAME": a["NAME"],
"PROPOSITION": _fill(a["PROPOSITION"], members),
"REFS": sorted(refs)}))
for b in M["BOUNDARIES"]:
rename = {}
for s in M["SLOTS"]:
if s["MAX"] == 1:
rename[s["SLOT"]] = members[s["SLOT"]][0]
tree = _expand_template(b["TREE"], rename, M, members)
cond = F._pr(tree)
out.append(("BOUNDARY", {"NAME": b["NAME"], "PREDICATE": _fill(b["PREDICATE"], members),
"REFS": _idents(tree), "CONDITION": cond}))
for q in dropped:
out.append(("ASSUMPTION", {"NAME": "fixed_" + q + "_balanced",
"PROPOSITION": "a constraint force along " + q
+ " balances every other force along " + q,
"REFS": [q]}))
for kind, e in out:
n = e["NAME"]
if n in base_names:
_R("EXPAND: " + cv + " emits " + kind + " " + n + ", but the TPK already has an "
"entry named " + n)
if n in by_name:
k0, e0, src = by_name[n]
fields = Z.TPK_FIELDS[kind][0] + Z.TPK_FIELDS[kind][1]
if k0 != kind or Z._entry_list(e0, fields) != Z._entry_list(e, fields):
_R("EXPAND: " + src[0] + " and " + cv + " both emit " + n + ", differently")
src.append(cv)
continue
rec = [kind, e, [cv]]
by_name[n] = rec
emitted.append(rec)
# S10 composition
composed, new_laws = [], {}
for L in _tpk_entries(tpk, "LAW"):
ln = L.get("NAME")
if ln not in receiving:
continue
terms = receiving[ln]
canon = F.parse_form(L["EQUATION"], "equation")[1]
sides = canon.split("=")
f = sides[1 - dside[ln]]
if f == "0":
s1, e1, w1, _ = terms[0]
force = (e1 if s1 == "+" else "-" + w1) + "".join(s + w for s, _, w, _ in terms[1:])
else:
force = f + "".join(s + w for s, _, w, _ in terms)
new = sides[0] + "=" + force if dside[ln] == 0 else force + "=" + sides[1]
r = F.parse_form(new, "equation")
if r[0] != "OK":
_R("EXPAND: LAW " + ln + ": the composed EQUATION is refused: " + r[1])
L2 = dict(L)
L2["EQUATION"] = r[1]
L2["REFS"] = F.form_names(r[1], "equation")[1]
L2["STATEMENT"] = L["STATEMENT"] + "".join("; with " + lab + ": " + s + w
for s, _, w, lab in terms)
new_laws[ln] = L2
composed.append([ln, r[1]])
# S11 the result
out_tpk = {}
for k in tpk:
v = tpk[k]
if k == "LAW" and _is_list(v):
v = [new_laws.get(e.get("NAME"), e) if _is_obj(e) else e for e in v]
elif _is_list(v):
v = list(v)
out_tpk[k] = v
for kind in Z.TPK_KINDS:
add = [e for k, e, _ in emitted if k == kind]
if add:
out_tpk[kind] = list(out_tpk.get(kind, [])) + add
xdraft = dict(draft)
xdraft["TPK"] = out_tpk
rows = [[k, e["NAME"], list(src)] for k, e, src in emitted]
return xdraft, composed, rows, dropped_all
def _fill(s, members):
"""PROPOSITION or PREDICATE with each {SLOT} replaced by its names joined with ", "."""
out, i, n = [], 0, len(s)
while i < n:
if s[i] == "{":
j = s.find("}", i + 1)
out.append(", ".join(members[s[i + 1:j]]))
i = j + 1
else:
out.append(s[i])
i += 1
return "".join(out)
def module_expand(draft, claims, modules):
try:
return ["OK", _expand(draft, claims, modules)[0]]
except _Refused as e:
return _refuse(str(e))
def _render_expand(draft, claims, modules):
try:
x, composed, rows, dropped = _expand(draft, claims, modules)
except _Refused as e:
return _refuse(str(e))
return ["OK", ["D(TPK)", Z.d_tpk(x["TPK"])], ["COMPOSED", composed], ["EMITTED", rows],
["DROPPED", dropped]]
# ---- 5.3, 6.8 catalogue_state ---------------------------------------------------------------------
def _state(lines):
if not _is_list(lines):
_R("LINES: not a list")
V = {} # (ID, VERSION) -> {DIGEST, STATUS, DATE, NOTE}
states = []
prev = None
for n, ln in enumerate(lines, 1):
tag = "LINE %d" % n
if not _is_obj(ln):
_R(tag + ": not an object")
if "ACT" not in ln:
_R(tag + ": missing field ACT")
act = ln["ACT"]
if not _is_str(act):
_R(tag + ": field ACT has the wrong type")
if act not in ACTS:
_R(tag + ": ACT " + act + " is not a module act")
fields = ACTS[act]
opt = ["REPLACED_BY"] if act == "MODULE WITHDRAW" else []
for k in _keys(ln):
if k != "ACT" and k not in fields and k not in opt:
_R(tag + ": unknown field " + k)
for f in fields:
if f not in ln:
if f == "REASON":
_R(tag + ": MODULE WITHDRAW without a reason")
_R(tag + ": missing field " + f)
for f in fields + opt:
if f in ln and not _is_str(ln[f]):
_R(tag + ": field " + f + " has the wrong type")
if act == "MODULE WITHDRAW":
bad = Z._first_bad(ln["REASON"])
if bad is not None:
_R(tag + ": field REASON contains disallowed character " + bad)
mid, ver, date = ln["ID"], ln["VERSION"], ln["DATE"]
if not _is_module_id(mid):
_R(tag + ": ID " + mid + " is not a module ID")
if not _is_version(ver):
_R(tag + ": VERSION " + ver + " is not a version")
rep = ln.get("REPLACED_BY")
if rep is not None and not _is_version(rep):
_R(tag + ": REPLACED_BY " + rep + " is not a version")
if "DIGEST" in fields and not _is_digest(ln["DIGEST"]):
_R(tag + ": DIGEST is not a digest")
if not _is_date(date):
_R(tag + ": DATE " + date + " is not a date")
if act == "MODULE WITHDRAW" and Z._blank(ln["REASON"]):
_R(tag + ": MODULE WITHDRAW without a reason")
if prev is not None and date < prev:
_R(tag + ": DATE " + date + " is before the previous line's")
prev = date
key = (mid, ver)
mine = [k for k in V if k[0] == mid]
offered = [k for k in mine if V[k]["STATUS"] == "OFFERED"]
if act in ("MODULE ADD", "MODULE VERSION"):
if act == "MODULE ADD" and mine:
_R(tag + ": MODULE ADD of " + mid + ", an ID already declared (no ID is reissued)")
if act == "MODULE VERSION":
if not mine:
_R(tag + ": MODULE VERSION of " + mid + ", an ID never added")
if key in V:
_R(tag + ": " + mid + " " + ver + " is already declared (no version is "
"reissued)")
vmax = max(mine, key=lambda k: _vkey(k[1]))
if _vkey(ver) <= _vkey(vmax[1]):
_R(tag + ": " + mid + " " + ver + " is not greater than " + mid + " "
+ vmax[1])
for k in sorted(V):
if V[k]["DIGEST"] == ln["DIGEST"]:
_R(tag + ": DIGEST already declared for " + k[0] + " " + k[1])
for k in offered:
V[k].update(STATUS="SUPERSEDED", DATE=date)
V[key] = {"DIGEST": ln["DIGEST"], "STATUS": "OFFERED", "DATE": date, "NOTE": ""}
else:
if key not in V:
_R(tag + ": " + mid + " " + ver + " is not declared")
st = V[key]["STATUS"]
if act == "MODULE RETIRE":
if st != "OFFERED":
_R(tag + ": MODULE RETIRE of " + mid + " " + ver + ", which is " + st
+ ", not OFFERED")
V[key].update(STATUS="RETIRED", DATE=date)
elif act == "MODULE WITHDRAW":
if st == "WITHDRAWN":
_R(tag + ": " + mid + " " + ver + " is already WITHDRAWN (WITHDRAWN is final)")
if rep is not None:
if st != "OFFERED":
_R(tag + ": REPLACED_BY needs " + mid + " " + ver + " OFFERED; it is "
+ st)
if (mid, rep) not in V:
_R(tag + ": REPLACED_BY " + mid + " " + rep + " is not declared")
rst = V[(mid, rep)]["STATUS"]
if rst not in ("SUPERSEDED", "RETIRED"):
_R(tag + ": REPLACED_BY " + mid + " " + rep + " is " + rst
+ ", not SUPERSEDED or RETIRED")
V[key].update(STATUS="WITHDRAWN", DATE=date, NOTE=ln["REASON"])
if rep is not None:
V[(mid, rep)].update(STATUS="OFFERED", DATE=date)
else:
if st == "WITHDRAWN":
_R(tag + ": MODULE REINSTATE of " + mid + " " + ver + ", which is WITHDRAWN "
"(WITHDRAWN is final)")
if st == "OFFERED":
_R(tag + ": MODULE REINSTATE of " + mid + " " + ver + ", which is already "
"OFFERED")
for k in offered:
V[k].update(STATUS="SUPERSEDED", DATE=date)
V[key].update(STATUS="OFFERED", DATE=date)
states.append([n, _state_digest(_offer(V))])
return {"V": V, "STATES": states, "N": len(lines)}
def _offer(V):
return [[k[0], k[1], V[k]["DIGEST"]] for k in sorted(V) if V[k]["STATUS"] == "OFFERED"]
def _state_digest(offer):
f = ["TPC-MODULE-OFFER", "1"]
for i, v, d in offer:
f += [i, v, d]
return G.digest_fields(f)
def _catalogue(lines):
try:
return _state(lines)
except _Refused as e:
_R("CATALOGUE: " + str(e))
def catalogue_state(lines):
try:
S = _state(lines)
except _Refused as e:
return _refuse(str(e))
V = S["V"]
return ["OK", ["VERSIONS", [[k[0], k[1], V[k]["DIGEST"], V[k]["STATUS"], V[k]["DATE"],
V[k]["NOTE"]] for k in sorted(V)]],
["OFFERED", _offer(V)], ["STATES", S["STATES"]]]
def _offer_at(lines, at):
"""OFFER(at): the OFFERED list after line at (lines already accepted)."""
if at == 0:
return []
return _offer(_state(lines[:at])["V"])
# ---- 6.5 module_verify -----------------------------------------------------------------------------
def module_verify(base, claims, modules, lines, draft):
try:
S = _catalogue(lines)
texts = _modules(modules)
_declared_texts(texts, S)
cls = _claims(claims)
_claims_declared(cls, texts, S)
x = _expand(base, claims, modules)[0]
if not _is_obj(draft):
_R("DRAFT: not an object")
if "TPK" not in draft:
_R("DRAFT: missing zone TPK")
except _Refused as e:
return _refuse(str(e))
want = Z.d_tpk(x["TPK"])
got = Z.d_tpk(draft["TPK"]) if _t1(draft["TPK"])[0] else "NOT WELL-FORMED"
return ["OK", "MATCH" if want == got else "MISMATCH", want, got,
[[c["ID"], c["VERSION"], S["V"][(c["ID"], c["VERSION"])]["STATUS"]] for c in cls]]
# ---- 5.4-5.5a, 6.6 interview_check -------------------------------------------------------------------
def _triples(x):
return _is_list(x) and all(_is_list(t) and len(t) == 3 and all(_is_str(s) for s in t)
for t in x)
def _carried(carried, S):
if not _triples(carried):
_R("CARRIED: not a list of [ID, VERSION, DIGEST]")
for i, v, d in carried:
if (i, v) not in S["V"]:
_R("CARRIED " + i + " " + v + ": not declared")
if S["V"][(i, v)]["DIGEST"] != d:
_R("CARRIED " + i + " " + v + ": DIGEST does not match the declaration")
return [list(t) for t in carried]
def _modified(modified, S, cls):
if not (_is_list(modified) and all(_is_list(t) and len(t) == 2 and all(_is_str(s) for s in t)
for t in modified)):
_R("MODIFIED: not a list of [ID, VERSION]")
dup = _least_dup([t[0] for t in modified])
if dup is not None:
_R("MODIFIED: duplicate module " + dup)
claimed = set(c["ID"] for c in cls)
out = sorted([list(t) for t in modified])
for i, v in out:
if (i, v) not in S["V"]:
_R("MODIFIED " + i + " " + v + ": not declared")
if i in claimed:
_R("MODIFIED " + i + " " + v + ": the ID is also claimed")
return out
def _answer(answer, lines, N):
"""5.4: the rounds, each with its COVERED and CHOSEN (a list of IDs or [])."""
if not _is_list(answer):
_R("ANSWER: not a list")
if not answer:
_R("INTERACTIONS: not answered")
rounds, covered_ids, prev_at = [], set(), None
for k, r in enumerate(answer, 1):
tag = "ANSWER ROUND %d" % k
if not _is_obj(r):
_R(tag + ": not an object")
_fields(tag, r, ["AT", "COVERED", "CHOSEN"], ["RESELECT"])
at = r["AT"]
if not (_is_int(at) and 0 <= at <= N):
_R(tag + ": AT is not a line count from 0 to %d" % N)
if prev_at is not None and at <= prev_at:
_R(tag + ": AT is not after the previous round's")
offer = _offer_at(lines, at)
resel = r.get("RESELECT", [])
if "RESELECT" in r:
if not _str_list(resel):
_R(tag + ": field RESELECT has the wrong type")
if any(resel[i] >= resel[i + 1] for i in range(len(resel) - 1)):
_R(tag + ": RESELECT is not in code point order without repeats")
offered_ids = set(e[0] for e in offer)
for x in resel:
if x not in covered_ids:
_R(tag + ": RESELECT " + x + " was not covered before")
if x not in offered_ids:
_R(tag + ": RESELECT " + x + " is not offered at AT")
cov = r["COVERED"]
if not _triples(cov):
_R(tag + ": field COVERED has the wrong type")
if k == 1:
want = offer
else:
want = [e for e in offer if e[0] not in covered_ids or e[0] in resel]
if not want:
_R(tag + ": no module was added since the previous round")
if [list(t) for t in cov] != want:
_R(tag + ": COVERED is not the offer the round was given over")
ch = r["CHOSEN"]
if ch == "NONE":
chosen = []
else:
if not _str_list(ch):
_R(tag + ": field CHOSEN has the wrong type")
if not ch:
_R(tag + ": CHOSEN is empty; the exclusive answer is NONE")
if any(ch[i] >= ch[i + 1] for i in range(len(ch) - 1)):
_R(tag + ": CHOSEN is not in code point order without repeats")
cids = [e[0] for e in want]
for x in ch:
if x not in cids:
_R(tag + ": CHOSEN " + x + " is not in COVERED")
chosen = list(ch)
rounds.append({"COVERED": want, "CHOSEN": chosen})
covered_ids.update(e[0] for e in want)
prev_at = at
latest = {} # ID -> (round's entry, chosen?)
for r in rounds:
for e in r["COVERED"]:
latest[e[0]] = (e, e[0] in r["CHOSEN"])
return latest
def _questions(cls, texts, skip_fixed):
"""6.4 S7 a, c and d over the claims (interview_check I7)."""
ids = [c["ID"] for c in cls]
for c in cls:
M = texts[(c["ID"], c["VERSION"])]
cv = c["ID"] + " " + c["VERSION"]
ans = c["ANSWERS"]
for k in _keys(ans):
if not _is_answer_key(k):
_R("CLAIM " + cv + ": answer " + k + " is not a question")
if ans[k] not in ("YES", "NO"):
_R("CLAIM " + cv + ": answer " + k + " is not YES or NO")
raised = set()
for qd in M["QUESTIONS"]:
if any(o != c["ID"] and _matches(qd["WITH"], o) for o in ids):
raised.add(qd["QID"])
if qd["QID"] not in ans:
_R("CLAIM " + cv + ": question " + qd["QID"] + " is not answered")
for k in _keys(ans):
if k in raised or (skip_fixed and k.startswith("FIXED:")):
continue
_R("CLAIM " + cv + ": answer " + k + " answers no question raised")
def _interview(answer, claims, lines, modules, carried, modified):
S = _catalogue(lines)
texts = _modules(modules)
_declared_texts(texts, S)
cls = _claims(claims)
car = _carried(carried, S)
mod = _modified(modified, S, cls)
latest = _answer(answer, lines, S["N"])
rows = []
for c in cls:
key = (c["ID"], c["VERSION"])
cv = c["ID"] + " " + c["VERSION"]
if key not in S["V"]:
_R("CLAIM " + cv + ": not declared")
if c["DIGEST"] != S["V"][key]["DIGEST"]:
_R("CLAIM " + cv + ": DIGEST does not match the declaration")
if key not in texts:
_R("CLAIM " + cv + ": no module text")
trip = [c["ID"], c["VERSION"], c["DIGEST"]]
if c["ID"] in latest:
entry, chosen = latest[c["ID"]]
if not chosen:
_R("CLAIM " + cv + ": the answer did not choose " + c["ID"])
if entry == trip:
rows.append([c["ID"], c["VERSION"], "PINNED"])
elif trip in car:
rows.append([c["ID"], c["VERSION"], "CARRIED"])
else:
_R("CLAIM " + cv + ": not OFFERED when chosen (a new claim names the OFFERED "
"version)")
elif trip in car:
rows.append([c["ID"], c["VERSION"], "CARRIED"])
else:
_R("CLAIM " + cv + ": " + c["ID"] + " is not in the answer")
claimed = set(c["ID"] for c in cls) | set(i for i, _ in mod)
for i in sorted(latest):
if latest[i][1] and i not in claimed:
_R("ANSWER: " + i + " is chosen but not claimed")
_excludes(cls, texts)
_questions(cls, texts, True)
ask = [e for e in _offer(S["V"]) if e[0] not in latest]
return {"ASK": ask, "ROWS": rows, "LATEST": latest, "TEXTS": texts, "CLAIMS": cls, "MOD": mod}
def interview_check(answer, claims, lines, modules, carried, modified):
try:
R = _interview(answer, claims, lines, modules, carried, modified)
except _Refused as e:
return _refuse(str(e))
return ["OK", ["ASK", R["ASK"]], ["CLAIMS", R["ROWS"]]]
# ---- 6.7 not_included_lines -------------------------------------------------------------------------
def not_included_lines(answer, claims, lines, modules, carried, modified):
try:
R = _interview(answer, claims, lines, modules, carried, modified)
texts, latest = R["TEXTS"], R["LATEST"]
a_lines = []
for i in sorted(latest):
entry, chosen = latest[i]
if chosen:
continue
key = (entry[0], entry[1])
if key not in texts:
_R("MODULES: no text of " + entry[0] + " " + entry[1] + ", covered by the answer")
a_lines.append([entry[0] + " " + entry[1], texts[key]["NOT_CHOSEN"]])
except _Refused as e:
return _refuse(str(e))
out = list(a_lines)
cls = R["CLAIMS"]
for c in cls:
M = texts[(c["ID"], c["VERSION"])]
for x in M["NOT_INCLUDED"]:
out.append([c["ID"] + " " + c["VERSION"], x])
for i, v in R["MOD"]:
out.append([i + " " + v, "Modified from " + i + " " + v + ": its entries are the "
"author's own."])
ids = [c["ID"] for c in cls]
for c in cls:
M = texts[(c["ID"], c["VERSION"])]
for qd in M["QUESTIONS"]:
if any(o != c["ID"] and _matches(qd["WITH"], o) for o in ids):
out.append([c["ID"] + " " + c["VERSION"],
qd["YES"] if c["ANSWERS"][qd["QID"]] == "YES" else qd["NO"]])
out.append(["-", CATCH_LINE])
return ["OK", out]
# ---- 6.9 module_check -------------------------------------------------------------------------------
def _kernel_verdict(tpk):
kt = K.kernel_tests(tpk)
if kt[0] is not True:
for name, passed, probs in kt[1]:
if passed is False:
return name + ": " + (probs[0] if probs else "failed")
return "kernel tests: not passed"
t3 = K.t3_consistency(tpk, {"PARAMETERS": {"S_MAX": 1}})
if not t3[0]:
return "T3: " + (t3[1][0] if t3[1] else "failed")
return "PASS"
def _binding_claim(M, b, other_ids):
ans = dict(b["ANSWERS"])
for qd in M["QUESTIONS"]:
if any(_matches(qd["WITH"], o) for o in other_ids) and qd["QID"] not in ans:
ans[qd["QID"]] = "NO"
return {"ID": M["ID"], "VERSION": M["VERSION"], "DIGEST": _digest(M), "BIND": b["BIND"],
"VALUES": b["VALUES"], "ANSWERS": ans}
def module_check(text, act, date, lines, modules):
try:
if act not in ("MODULE ADD", "MODULE VERSION"):
_R("ACT: " + (act if _is_str(act) else "?") + " is not MODULE ADD or MODULE VERSION")
M = _parse(text)
S = _catalogue(lines)
texts = _modules(modules)
_declared_texts(texts, S)
for i, v, _ in _offer(S["V"]):
if (i, v) not in texts:
_R("MODULES: no text of " + i + " " + v + " (OFFERED)")
line = {"ACT": act, "ID": M["ID"], "VERSION": M["VERSION"], "DIGEST": _digest(M),
"DATE": date}
S2 = _catalogue(list(lines) + [line])
except _Refused as e:
return _refuse(str(e))
rows = [["DIGEST", _digest(M)]]
declared = sorted(set(k[0] for k in S2["V"] if k[0] != M["ID"]))
ref = "PASS"
for p in sorted(M["EXCLUDES"]):
if not any(_matches(p, i) for i in declared):
ref = "EXCLUDES " + p + " matches no declared module"
break
if ref == "PASS":
for qd in M["QUESTIONS"]:
if not any(_matches(qd["WITH"], i) for i in declared):
ref = "WITH " + qd["WITH"] + " matches no declared module"
break
rows.append(["REFERENCES", ref])
for b in M["BINDINGS"]:
claim = _binding_claim(M, b, [])
try:
x = _expand({"TPK": b["TPK"]}, [claim], [text])[0]
verdict = _kernel_verdict(x["TPK"])
except _Refused as e:
verdict = str(e)
rows.append(["BINDING", b["NAME"], Z._show(verdict)])
authors = dict((p["NAME"], p["DIM"]) for p in M["PARAMS"] if p["SUPPLY"] == "AUTHOR")
for i, v, _ in _offer(S2["V"]):
if i == M["ID"]:
continue
B = texts[(i, v)]
if (any(_matches(p, i) for p in M["EXCLUDES"])
or any(_matches(p, M["ID"]) for p in B["EXCLUDES"])):
rows.append(["PAIR", i, v, "EXCLUDED"])
continue
shared = sorted(p["NAME"] for p in B["PARAMS"]
if p["SUPPLY"] == "AUTHOR" and p["NAME"] in authors)
differ = [n for n in shared if authors[n] != B["PARAM_OF"][n]["DIM"]]
if differ:
n = differ[0]
rows.append(["PAIR", i, v, "-", "SHARED PARAMETER " + n + ": DIMENSION " + authors[n]
+ " in " + M["ID"] + " " + M["VERSION"] + ", "
+ B["PARAM_OF"][n]["DIM"] + " in " + i + " " + v])
continue
bnames = dict((bb["NAME"], bb) for bb in B["BINDINGS"])
any_shared = False
for b in M["BINDINGS"]:
bb = bnames.get(b["NAME"])
if bb is None or Z.d_tpk(bb["TPK"]) != Z.d_tpk(b["TPK"]):
continue
any_shared = True
ca = _binding_claim(M, b, [i])
cb = _binding_claim(B, bb, [M["ID"]])
try:
x1 = _expand({"TPK": b["TPK"]}, [ca, cb], [text, B["TEXT"]])[0]
x2 = _expand({"TPK": b["TPK"]}, [cb, ca], [B["TEXT"], text])[0]
if Z.d_tpk(x1["TPK"]) != Z.d_tpk(x2["TPK"]):
verdict = "TWO SELECTION ORDERS GIVE TWO D(TPK)"
else:
verdict = _kernel_verdict(x1["TPK"])
except _Refused as e:
verdict = str(e)
rows.append(["PAIR", i, v, b["NAME"], Z._show(verdict)])
if not any_shared:
rows.append(["PAIR", i, v, "-", "NO SHARED BINDING"])
for n in shared:
rows.append(["SHARED PARAMETER", M["ID"], M["VERSION"], i, v, n])
rows.append(["ATOMICITY", [a["NAME"] for a in M["ASSUMPTIONS"]]])
bad = any(r[-1] not in ("PASS", "EXCLUDED") for r in rows
if r[0] in ("REFERENCES", "BINDING", "PAIR"))
return ["OK", "FAIL" if bad else "PASS", rows]
# ---- 6.10 draft_module_status ----------------------------------------------------------------------
def draft_module_status(base, claims, modules, lines):
try:
S = _catalogue(lines)
texts = _modules(modules)
_declared_texts(texts, S)
cls = _claims(claims)
_claims_declared(cls, texts, S)
x = _expand(base, claims, modules)[0]
mine = Z.d_tpk(x["TPK"])
rows, gate = [], []
for c in cls:
key = (c["ID"], c["VERSION"])
st = S["V"][key]
if st["STATUS"] == "OFFERED":
rows.append([c["ID"], c["VERSION"], "OFFERED"])
elif st["STATUS"] == "SUPERSEDED":
cur = [k for k in S["V"] if k[0] == c["ID"] and S["V"][k]["STATUS"] == "OFFERED"]
if not cur:
rows.append([c["ID"], c["VERSION"], "SUPERSEDED", "NONE OFFERED"])
continue
ck = cur[0]
if ck not in texts:
_R("MODULES: no text of " + ck[0] + " " + ck[1] + " (OFFERED)")
alt = [dict(o, VERSION=ck[1], DIGEST=S["V"][ck]["DIGEST"]) if o is c else o
for o in cls]
try:
y = _expand(base, alt, modules)[0]
rows.append([c["ID"], c["VERSION"], "SUPERSEDED", ck[1],
"SAME" if Z.d_tpk(y["TPK"]) == mine else "DIFFERS"])
except _Refused as e:
rows.append([c["ID"], c["VERSION"], "SUPERSEDED", ck[1],
Z._show("NOT EXPANDED: " + str(e))])
elif st["STATUS"] == "RETIRED":
rows.append([c["ID"], c["VERSION"], "RETIRED", st["DATE"]])
else:
rows.append([c["ID"], c["VERSION"], "WITHDRAWN", st["DATE"], st["NOTE"]])
gate.append("This draft uses " + c["ID"] + " " + c["VERSION"] + ", withdrawn on "
+ st["DATE"] + " for: " + st["NOTE"] + ". Declare with it?")
except _Refused as e:
return _refuse(str(e))
return ["OK", ["CLAIMS", rows], ["GATE", gate]]
# ---- 5.6, 6.11 module_use_view -----------------------------------------------------------------------
def module_use_view(certificates, lines):
try:
S = _catalogue(lines)
if not _is_list(certificates):
_R("CERTIFICATES: not a list")
for i, c in enumerate(certificates, 1):
tag = "CERTIFICATE %d" % i
if not _is_obj(c):
_R(tag + ": not an object")
_fields(tag, c, ["PREFIX", "MODULES_USED"])
if not _is_str(c["PREFIX"]):
_R(tag + ": field PREFIX has the wrong type")
if not _triples(c["MODULES_USED"]):
_R(tag + ": field MODULES_USED has the wrong type")
if not Z._is_ident(c["PREFIX"]):
_R(tag + ": PREFIX " + c["PREFIX"] + " is not a prefix")
dup = _least_dup([c["PREFIX"] for c in certificates])
if dup is not None:
_R("CERTIFICATES: duplicate prefix " + dup)
rows, n_wd = [], 0
for c in certificates:
tag = "CERTIFICATE " + c["PREFIX"]
used = c["MODULES_USED"]
dup = _least_dup([t[0] for t in used])
if dup is not None:
_R(tag + ": duplicate module " + dup)
wd = False
for i, v, d in used:
if (i, v) not in S["V"]:
_R(tag + ": " + i + " " + v + " is not declared")
if S["V"][(i, v)]["DIGEST"] != d:
_R(tag + ": " + i + " " + v + ": DIGEST does not match the declaration")
st = S["V"][(i, v)]["STATUS"]
wd = wd or st == "WITHDRAWN"
rows.append([i, v, c["PREFIX"], st])
n_wd += 1 if wd else 0
except _Refused as e:
return _refuse(str(e))
return ["OK", ["ROWS", sorted(rows)], ["UWCS ON WITHDRAWN", n_wd]]
# ---- run_case (6.12) -------------------------------------------------------------------------------
def _J(v):
return json.dumps(v, ensure_ascii=True, separators=(",", ":"))
def _text_arg(args):
if "text_parts" in args:
return "".join(p[0] * p[1] for p in args["text_parts"])
return args.get("text")
def run_case(fn, args):
"""One corpus case: the rendered result (2.3; 6.4 RENDER). An unknown fn
raises: a corpus error, not a vector."""
if fn not in FNS:
raise ValueError("fn")
a = args
if fn == "module_parse":
return _J(module_parse(_text_arg(a)))
if fn == "module_digest":
return _J(module_digest(_text_arg(a)))
if fn == "module_bind":
return _J(module_bind(a.get("tpk"), a.get("text"), a.get("bind"), a.get("values")))
if fn == "module_expand":
return _J(_render_expand(a.get("draft"), a.get("claims"), a.get("modules")))
if fn == "module_verify":
return _J(module_verify(a.get("base"), a.get("claims"), a.get("modules"), a.get("lines"),
a.get("draft")))
if fn == "interview_check":
return _J(interview_check(a.get("answer"), a.get("claims"), a.get("lines"),
a.get("modules"), a.get("carried"), a.get("modified")))
if fn == "not_included_lines":
return _J(not_included_lines(a.get("answer"), a.get("claims"), a.get("lines"),
a.get("modules"), a.get("carried"), a.get("modified")))
if fn == "catalogue_state":
return _J(catalogue_state(a.get("lines")))
if fn == "module_check":
return _J(module_check(a.get("text"), a.get("act"), a.get("date"), a.get("lines"),
a.get("modules")))
if fn == "draft_module_status":
return _J(draft_module_status(a.get("base"), a.get("claims"), a.get("modules"),
a.get("lines")))
return _J(module_use_view(a.get("certificates"), a.get("lines")))