lawref.evaluator.queries

Ветви запроса: результат и корневой proof-узел на каждый вид query.

Конвейер вычисления (engine) заканчивается общим состоянием — store, proof- реестр, манифест, позиции; здесь оно превращается в документ §208. Каждая ветвь самостоятельна и возвращает готовый документ.

Functions

Name	Description
judgment_declarations	§47.3: judgment-relations программы — id → декларация с judgment
query_argumentation	Профиль §274.1–§274.7 (law.argumentation/0.2, DECISION-0039).
query_calendar_op	Календарная операция над pinned снапшотом — §85–§86.
query_collect	Finite relation comprehension §52.1: distinct ground values,
query_formula	Four-valued status of an arbitrary closed Formula (§62).
query_interpretation_analysis	Analysis mode §156: каждая alternative указанной exactly_one-группы
query_positions	NORM_POSITION-результат §134: summary-статусы позиций
query_precedent	Профиль §276.1–§276.9 (law.precedent/0.2, DECISION-0090).
query_term	Data-term вычисление §57–§58 (несовместимости §48/§49/§50 — T022–T024).
query_truth	Truth status ground-литерала — §62/§65; конфликты §115 попадают в
query_weak_permission	Weak permission §126 — query result, НЕ норма: `weakly_permitted(actor,
query_why_not	§185 why_not(P) — blocker graph по кандидатам-правилам.

judgment_declarationsfunction#

View source

def judgment_declarations(ir_nodes: list[dict]) -> dict[str, dict]

§47.3: judgment-relations программы — id → декларация с judgment {authority, requestSchema?} (DECISION-0024/0036). external_decl канала — носитель органа; сюда он сводится к историческому виду symbol_decl. Одна таблица на все носители канала (E-0100): тело правила, valid_when §127, condition цели §123, условие дефитера §149 — и на материализацию эффектов, где решается, выпускать ли POWER_INVALID_EXERCISE.

query_argumentationfunction#

View source

def query_argumentation(query: dict, query_id: str, store: SupportStore, registry: ProofRegistry, manifest: dict, issues: list[dict], nodes: list[dict], legal_time: str, limits: dict | None = None) -> dict

Профиль §274.1–§274.7 (law.argumentation/0.2, DECISION-0039).

Вид результата — GRAPH: AF целиком в value (аргументы, атаки, разметки, класс ответа §274.6); proof graph — пустой корень query_evaluation (профиль объясняет граф value, прецедент §185). Превышение капов §274.2/§274.5 — fatal RESOURCE_LIMIT без частичного вывода (дисциплина §238).

query_calendar_opfunction#

View source

def query_calendar_op(query: dict, query_id: str, snapshot: dict | None, effective: dict, manifest: dict, issues: list[dict], calendar_resource: bytes | None) -> dict

Календарная операция над pinned снапшотом — §85–§86.

query_collectfunction#

View source

def query_collect(query: dict, query_id: str, store: SupportStore, registry: ProofRegistry, manifest: dict, issues: list[dict], interpretation_dependent: bool | None = None) -> dict

Finite relation comprehension §52.1: distinct ground values, COLLECTION без truth-измерения (§174.1, T036-контракт).

query_formulafunction#

View source

def query_formula(query: dict, query_id: str, store: SupportStore, registry: ProofRegistry, manifest: dict, issues: list[dict], term_env: Any = None) -> dict

Four-valued status of an arbitrary closed Formula (§62).

This internal query is shared by finite counterfactual search. It reads the already-computed support store and never rewrites the program, which keeps external-snapshot program bindings stable.

query_interpretation_analysisfunction#

View source

def query_interpretation_analysis(query: dict, query_id: str, ir: dict, case: dict, options: dict, registry: ProofRegistry, manifest: dict, issues: list[dict], nodes: list[dict], evaluate_fn) -> dict

Analysis mode §156: каждая alternative указанной exactly_one-группы вычисляется ОТДЕЛЬНЫМ изолированным прогоном (рекурсивный evaluate с selectedInterpretations=[alt]) — results_by_interpretation; результаты не смешиваются по построению. В value — ядро результата каждой альтернативы; в attributes — resultHash каждого изолированного документа (детерминированная сцепка §209/§211).

query_positionsfunction#

View source

def query_positions(query_id: str, registry: ProofRegistry, manifest: dict, issues: list[dict], norm_positions: list[dict], position_supports: dict[str, list[dict]], store: SupportStore | None = None, judgment_decls: dict[str, dict] | None = None, interpretation_dependent: bool | None = None) -> dict

NORM_POSITION-результат §134: summary-статусы позиций с normativeStatusSupports; сами позиции — top-level документа.

E-0100 (§47.3/§123/§124): condition цели, читающее отношение суждения при паре NEITHER, не решается вычислением — статус позиции остаётся как есть (ACTIVE), но evaluation status REQUIRES_JUDGMENT и JudgmentRequest называют, кто решает (whynot.position_judgment_blockers).

query_precedentfunction#

View source

def query_precedent(query: dict, query_id: str, store: SupportStore, registry: ProofRegistry, manifest: dict, issues: list[dict], nodes: list[dict], legal_time: str, limits: dict | None = None) -> dict

Профиль §276.1–§276.9 (law.precedent/0.2, DECISION-0090).

Вид результата — GRAPH: статусы прецедентов, связанность и непротиворечивость базы целиком в value; proof graph — пустой корень query_evaluation (профиль объясняет декларации, а holding исполнил baseline — прецедент §274). Кап §276.9 — fatal RESOURCE_LIMIT.

query_termfunction#

View source

def query_term(query: dict, query_id: str, store: SupportStore, registry: ProofRegistry, manifest: dict, issues: list[dict], env: Any = None) -> dict

Data-term вычисление §57–§58 (несовместимости §48/§49/§50 — T022–T024).

env — окружение §85/§86: term-запрос считает срок тем же add_business_days, что и правило (§86), одним кодом.

query_truthfunction#

View source

def query_truth(query: dict, query_id: str, store: SupportStore, registry: ProofRegistry, manifest: dict, issues: list[dict], conflict_reports: list[dict], norm_positions: list[dict], blocked_effects: dict[str, dict] | None = None, interpretation_required: bool = False, judgment_decls: dict[str, dict] | None = None, judgment_nodes: list[dict] | None = None, legal_time: str = '', term_env: Any = None) -> dict

Truth status ground-литерала — §62/§65; конфликты §115 попадают в результат. Transformation-запрос по эффекту, заблокированному непобеждённой парой Power/Immunity, — UNRESOLVED_NORMATIVE_CONFLICT §127.

query_weak_permissionfunction#

View source

def query_weak_permission(query: dict, query_id: str, registry: ProofRegistry, manifest: dict, issues: list[dict], norm_positions: list[dict], applicable_prohibitions: set[str]) -> dict

Weak permission §126 — query result, НЕ норма: weakly_permitted(actor, action) истинен только относительно явно выбранной политики (rule universe; source/time snapshot и interpretation уже пиннуты манифестом). Без политики отсутствие запрета — MISSING_POLICY («UNDETERMINED, а не permission»); v1-политика: query.policy == {“ruleUniverse”: true} — правила пакета объявлены полным универсумом применимых запретов. Запрет: активная позиция с forbearance-goal (§130 prohibition sugar: канонический CLIR — duty-to-forbear) с bearer=actor и goal.action=action.

query_why_notfunction#

View source

def query_why_not(query: dict, query_id: str, store: SupportStore, registry: ProofRegistry, manifest: dict, issues: list[dict], nodes: list[dict], legal_time: str, env=None, excluded: tuple[list[dict], dict[str, str]] | None = None) -> dict

§185 why_not(P) — blocker graph по кандидатам-правилам.

Вид результата — GRAPH (§174.1: «graph reference/value; semantic statuses относятся к его root nodes»), поэтому truthStatus корня — статус самой цели: спрашивающий видит и то, ЧТО получилось, и то, что этому помешало.

Blocker graph лежит в value, а не в proof graph: proof доказывает ОТВЕТ, а здесь доказывать нечего — вывод не получен. Попытка выдать кандидатов узлами rule_application была отвергнута Lean-ядром, и по делу: §180 требует от такого узла rule и substitution, которых у несработавшего правила нет. Словарь ApplicabilityStatus/TriggerStatus §174.1 при этом сохранён — он лежит у каждого кандидата внутри value.