| """lean/syntax_check.py offline: the node-kind whitelist, the generated parser program and |
| how answers are read (fake Lean). The real parser runs in tests/test_syntax_check_lean.py.""" |
|
|
| from __future__ import annotations |
|
|
| import pytest |
|
|
| from formal_mas.lean.runner import LeanMessage, LeanResult |
| from formal_mas.lean.statement import DEFAULT_HEADER |
| from formal_mas.lean.syntax_check import SyntaxChecker, _last, check_kinds, kind_allowed, program |
|
|
|
|
| @pytest.mark.parametrize("kind", [ |
| "null", "num", "token.«⊢»", "Lean.Parser.Tactic.omega", "Mathlib.Tactic.nlinarith", "Lean.Parser.Term.app", |
| "Lean.Parser.Term.dotIdent", "Lean.Parser.Term.anonymousCtor", "«term_+_»", "Real.«term√_»", "Nat.term_!", |
| "Lean.«binderPred∈_»", "Lean.«term∀__,_»", "BigOperators.bigsum", "termℝ", "Mathlib.Notation.«term∃!_,_»", |
| |
| "Lean.Parser.Tactic.classical", "Mathlib.Linter.HaveILetI.tacticLetI__", "Mathlib.Linter.HaveILetI.tacticHaveI__", |
| "Mathlib.Meta.SetNotationForOrder.subsetStx'", "Mathlib.Meta.SetNotationForOrder.ssubsetStx'", |
| "Mathlib.Meta.SetNotationForOrder.supsetStx'", "Mathlib.Meta.SetNotationForOrder.ssupsetStx'", |
| ]) |
| def test_allowed_kinds(kind): |
| assert kind_allowed(kind) == (True, ""), kind |
|
|
|
|
| @pytest.mark.parametrize("kind, reason", [ |
| ("Lean.Parser.Tactic.tacticSorry", "sorry"), ("Lean.Parser.Tactic.tacticStop_", "sorry"), |
| ("Lean.Parser.Term.sorry", "sorry"), ("Lean.Parser.Tactic.exact?", "search"), |
| ("Lean.Parser.Tactic.simpTrace", "search"), ("Mathlib.Tactic.Polyrith.«tacticPolyrithOnly[_]»", "search"), |
| ("Lean.Parser.Tactic.nativeDecide", "native"), ("Lean.Parser.Tactic.runTac", "metaprogramming"), |
| ("Lean.byElab", "metaprogramming"), ("Lean.Parser.Term.quot", "syntax"), |
| ("Lean.Parser.Term.doubleQuotedName", "syntax"), ("Lean.Parser.Term.do", "syntax"), |
| ("Lean.Parser.Term.doSeqIndent", "syntax"), ("Lean.Parser.Term.unsafe", "metaprogramming"), |
| ("Lean.Parser.Tactic.traceState", "syntax"), ("Mathlib.Tactic.ExtractGoal.extractGoal", "syntax"), |
| ("Some.Unknown.tactic", "syntax"), ("Qq.«term_q(_)»", "syntax"), ("Lean.Parser.Command.declaration", "syntax"), |
| ]) |
| def test_rejected_kinds(kind, reason): |
| assert kind_allowed(kind) == (False, reason), kind |
|
|
|
|
| def test_last_component_ignores_dots_in_guillemets(): |
| assert _last("Mathlib.Tactic.GCongr.«tacticRel[_]»") == "tacticRel[_]" |
| assert _last("Lean.«term∀__,_»") == "term∀__,_" |
| assert _last("«term_._»") == "term_._" |
| assert check_kinds(["null", "Lean.Parser.Tactic.exact?"]).reason == "search" |
|
|
|
|
| def test_program_embeds_text_in_raw_strings(): |
| code, lines = program(DEFAULT_HEADER, [__import__("formal_mas.lean.syntax_check", fromlist=["Item"]).Item( |
| "tactics", " constructor\n · simp")]) |
| assert 'r#"by\n constructor\n · simp"#' in code and "runParserCategory" in code |
| assert code.splitlines()[lines[0] - 1] == "open Lean in" |
|
|
|
|
| class FakeParser: |
| """Answers every `SYNTAX i` command; `kinds[i]` (list) or a parse error string.""" |
|
|
| def __init__(self, answers, status="finished", shift=1, duplicate=False): |
| self.answers, self.status, self.shift, self.duplicate = answers, status, shift, duplicate |
| self.codes = [] |
|
|
| def verify(self, code, theorem=None, timeout=None): |
| self.codes.append(code) |
| lines = [no for no, ln in enumerate(code.split("\n"), start=1) if ln == "open Lean in"] |
| msgs = [] |
| for i, (line, ans) in enumerate(zip(lines, self.answers)): |
| text = f"SYNTAX {i} ERROR\n{ans}" if isinstance(ans, str) else f"SYNTAX {i} OK\n" + "\n".join(ans) |
| msgs.append(LeanMessage("info", line + self.shift, 0, text)) |
| if self.duplicate: |
| msgs.append(LeanMessage("info", line + self.shift, 0, text)) |
| return LeanResult(self.status, "repl", msgs) |
|
|
|
|
| OK_KINDS = ["Lean.Parser.Term.byTactic", "Lean.Parser.Tactic.tacticSeq", "null", "Lean.Parser.Tactic.omega"] |
|
|
|
|
| def test_checker_offline_layer_first_then_parser(): |
| fake = FakeParser([OK_KINDS, OK_KINDS + ["Lean.Parser.Tactic.exact?"], "<input>:2:3: unknown tactic", |
| ["Lean.Parser.Term.app", "«term_=_»"]]) |
| res = SyntaxChecker(fake).check(DEFAULT_HEADER, tactics=["omega", "sorry", "omega\nfoo", "begin_x"], |
| terms=["x = 1"]) |
| assert [r.reason for r in res] == ["", "sorry", "search", "parse", ""] |
| assert res[0].ok and res[4].ok and len(fake.codes) == 1 |
| assert "sorry" not in fake.codes[0] |
|
|
|
|
| def test_comments_never_reach_the_raw_string(): |
| from formal_mas.lean.syntax_check import Item |
|
|
| code, _ = program(DEFAULT_HEADER, [Item("tactics", "skip -- a comment #\nomega /- b -/")]) |
| assert "comment" not in code and "/-" not in code and 'r#"by\n skip' in code |
| code, _ = program(DEFAULT_HEADER, [Item("tactics", 'skip -- "# x')]) |
| assert '"# x' not in code |
| with pytest.raises(ValueError): |
| program(DEFAULT_HEADER, [Item("tactics", 'skip "# x')]) |
| fake = FakeParser([OK_KINDS]) |
| (res,) = SyntaxChecker(fake).check(DEFAULT_HEADER, tactics=['skip -- "# #eval IO.Process.exit 0']) |
| assert res.reason == "string" and fake.codes == [] |
|
|
|
|
| def test_checker_fails_closed(): |
| for fake in (FakeParser([OK_KINDS], status="timeout"), FakeParser([OK_KINDS], shift=5), |
| FakeParser([OK_KINDS], duplicate=True), FakeParser([])): |
| (res,) = SyntaxChecker(fake).check(DEFAULT_HEADER, tactics=["omega"]) |
| assert not res.ok and res.reason == "syntax_unavailable" |
| assert SyntaxChecker(FakeParser([OK_KINDS], shift=0)).check(DEFAULT_HEADER, tactics=["omega"])[0].ok |
| assert SyntaxChecker(FakeParser([])).check(DEFAULT_HEADER) == [] |
|
|
