1#!/usr/bin/env python3
2# --------------------------------------------------------------
3#  miz_parser.py ――  Mizar 依存グラフ可視化
4# --------------------------------------------------------------
5#  theorem             : yellow   (Th…)
6#  auto-theorem        : lavender (Th_auto…)
7#  definition / auto   : teal     (Def… / Def_auto…)
8#  lemma               : coral    (Lm…)
9#  external article    : grey     (environ 節に列挙された語)
10# --------------------------------------------------------------
11from __future__ import annotations
12import re
13import sys
14from pathlib import Path
15from typing import Iterable
16
17import networkx as nx
18# from pyvis.network import Network
19
20
21# ─── 色定義 ──────────────────────────────────────────
22COL_TH   = "#ffc107"
23COL_AUTO = "#b39ddb"
24COL_DEF  = "#17a2b8"
25COL_LM   = "#ff7f50"
26COL_EXT  = "#9e9e9e"
27
28# ─── 基本正規表現 ──────────────────────────────────
29COMMENT_RE   = re.compile(r"::.*?$", re.M)
30THEOREM_RE   = re.compile(r"\btheorem\b(?:\s+([A-Za-z0-9_]+)\s*:)?", re.I)
31DEF_HDR_RE   = re.compile(r"\bdefinition\b(?:\s+([A-Za-z0-9_]+)\s*:)?", re.I)
32
33# 行頭にある Def/Lm ラベル (  :Def1:  や  Def1:  )
34INLINE_HEAD_RE = re.compile(r"^[ \t]*:?\s*((?:Def|Lm)\d+)\s*:", re.I | re.M)
35
36# 行中に埋め込まれた :Def1: / :Lm3: など
37INLINE_INLINE_RE = re.compile(r":\s*((?:Def|Lm)\d+)\s*:", re.I)
38
39BY_RE   = re.compile(r"\bby\s+([^;]+);",   re.I | re.S)
40FROM_RE = re.compile(r"\bfrom\s+([^;]+);", re.I | re.S)
41
42# 〈記事:キーワード+番号〉も 1 トークン扱い
43LABEL_RE = re.compile(
44    r"[A-Z][A-Za-z0-9_]*:[A-Za-z0-9_]+\s*\d+"   #  TARSKI:def 1 など
45    r"|[A-Z][A-Za-z0-9_]*"                      #  単体記事名・内部ラベル
46)
47
48FOLD_RE     = re.compile(r"^[A-Z](\d+)?$")          # A, A1 …（吸収対象）
49INTERNAL_RE = re.compile(r"^(?:Th\d+|Th_auto\d+|Def\d+|Def_auto\d+|Lm\d+)$")
50EXT_ART_RE  = re.compile(r"^[A-Z][A-Z0-9_]*$")
51
52
53# ─── environ から外部アーティクル抽出 ────────────────
54def externals(txt: str) -> set[str]:
55    m = re.search(r"\benviron\b(.*?)(?:\bbegin\b)", txt, re.I | re.S)
56    return set() if not m else set(re.findall(r"[A-Z][A-Z0-9_]*", m[1]))
57
58
59# ─── 1 つの .miz を依存グラフに変換 ───────────────────
60def parse_mizar(path: Path) -> nx.DiGraph:
61    src = COMMENT_RE.sub("", path.read_text(encoding="utf-8", errors="ignore"))
62    ext_art = externals(src)
63
64    #―― theorem：明示番号を把握して auto 番衝突を防ぐ ―――――――――――
65    explicit_nums, th_matches = set(), []
66    for m in THEOREM_RE.finditer(src):
67        th_matches.append(m)
68        if m.group(1) and m.group(1).startswith("Th") and m.group(1)[2:].isdigit():
69            explicit_nums.add(int(m.group(1)[2:]))
70
71    entries, inline_taken = [], set()
72    th_auto_i = def_auto_i = 1
73
74    #── theorem ブロック登録 ──────────────────────────
75    for m in th_matches:
76        if m.group(1):                              # 明示ラベル
77            lbl, kind = m.group(1), "th"
78        else:                                       # auto 採番
79            while th_auto_i in explicit_nums:
80                th_auto_i += 1
81            lbl, kind = f"Th_auto{th_auto_i}", "th_auto"
82            th_auto_i += 1
83        entries.append(dict(start=m.start(), end=m.end(), label=lbl, kind=kind))
84
85    #── definition ヘッダ処理 ─────────────────────────
86    for m in DEF_HDR_RE.finditer(src):
87        hdr_s, hdr_e = m.span()
88        # ブロック終端＝次 the/def 手前
89        nxt_th  = THEOREM_RE.search(src, hdr_e)
90        nxt_def = DEF_HDR_RE.search(src, hdr_e + 1)
91        blk_end = min(nxt_th.start()  if nxt_th  else len(src),
92                      nxt_def.start() if nxt_def else len(src))
93
94        # --- 行頭ラベル ---
95        for im in INLINE_HEAD_RE.finditer(src[hdr_e:blk_end]):
96            abs_pos = hdr_e + im.start()
97            lbl     = im.group(1)
98            inline_taken.add(abs_pos)
99            kind = "lemma" if lbl.lower().startswith("lm") else "def"
100            entries.append(dict(start=abs_pos, end=abs_pos, label=lbl, kind=kind))
101
102        # --- 行中ラベル ---
103        for jm in INLINE_INLINE_RE.finditer(src[hdr_e:blk_end]):
104            abs_pos = hdr_e + jm.start()
105            if abs_pos in inline_taken:             # 行頭と重複しないように
106                continue
107            lbl  = jm.group(1)
108            inline_taken.add(abs_pos)
109            kind = "lemma" if lbl.lower().startswith("lm") else "def"
110            entries.append(dict(start=abs_pos, end=abs_pos, label=lbl, kind=kind))
111
112        # ヘッダに固有ラベルが無ければ auto 付与
113        if not any(hdr_s <= e["start"] < hdr_e for e in entries):
114            lbl = f"Def_auto{def_auto_i}"
115            def_auto_i += 1
116            entries.append(dict(start=hdr_s, end=hdr_e, label=lbl, kind="def"))
117
118    #── ファイル行頭の Def/Lm (未登録) ─────────────────
119    for m in INLINE_HEAD_RE.finditer(src):
120        if m.start() in inline_taken:
121            continue
122        lbl  = m.group(1)
123        kind = "lemma" if lbl.lower().startswith("lm") else "def"
124        entries.append(dict(start=m.start(), end=m.end(), label=lbl, kind=kind))
125        inline_taken.add(m.start())
126
127    # 行中 :DefN: / :LmN: (未登録)
128    for m in INLINE_INLINE_RE.finditer(src):
129        if m.start() in inline_taken:
130            continue
131        lbl  = m.group(1)
132        kind = "lemma" if lbl.lower().startswith("lm") else "def"
133        entries.append(dict(start=m.start(), end=m.end(), label=lbl, kind=kind))
134
135    #―― 時系列順 & ラベル集合 ―――――――――――――――――――――――
136    entries.sort(key=lambda d: d["start"])
137    internal_labels = {e["label"] for e in entries}
138
139    #―― グラフ (ノード) ―――――――――――――――――――――――――――
140    G = nx.DiGraph()
141    color_of = {"th": COL_TH, "th_auto": COL_AUTO, "def": COL_DEF, "lemma": COL_LM}
142    for e in entries:
143        G.add_node(e["label"], color=color_of[e["kind"]], label=e["label"])
144
145    #―― 参照エッジ解析 ―――――――――――――――――――――――――
146    for idx, blk in enumerate(entries):
147        parent = blk["label"]
148        body = src[
149            blk["end"]:
150            entries[idx + 1]["start"] if idx + 1 < len(entries) else len(src)
151        ]
152
153        refs: set[str] = set()
154        for seg in BY_RE.findall(body) + FROM_RE.findall(body):
155            for tok in LABEL_RE.findall(seg):
156                tok = tok.rstrip()
157                if FOLD_RE.fullmatch(tok):
158                    continue
159
160                # ------------ 内部ラベル ------------
161                if tok in internal_labels and INTERNAL_RE.fullmatch(tok):
162                    refs.add(tok)
163                    continue
164
165                # ------------ 外部参照 ------------
166                art = tok.split(":")[0]              # “XBOOLE_0:7” → “XBOOLE_0”
167                if art in ext_art:
168                    refs.add(art)                    # 番号無視で記事名だけ追加
169                    continue
170
171        refs.discard(parent)
172        for r in refs:
173            if r not in G:
174                col = COL_EXT if r in ext_art else COL_TH
175                G.add_node(r, color=col, label=r)
176            G.add_edge(r, parent)
177
178    return G
179
180
181# ─── 可視化 (HTML) ─────────────────────────────────
182def visualize(G: nx.DiGraph, outfile: Path) -> None:
183    net = Network(height="800px", width="100%", directed=True, notebook=False)
184    net.from_nx(G)
185    net.barnes_hut(gravity=-8000, central_gravity=0.5)
186
187    for n in net.nodes:
188        n.update({
189            "value": max(nx.degree(G, n["id"]), 1),
190            "shape": "circle",
191            "font": {"vadjust": 0},
192        })
193
194    net.show(str(outfile))
195    print(f"★ 生成完了: {outfile}")
196
197
198# ─── CLI ────────────────────────────────────────────
199def main(files: Iterable[str]) -> None:
200    paths = [Path(p) for p in files]
201    if not paths:
202        print("usage: python miz_parser.py <file1.miz> [file2.miz ...]")
203        sys.exit(1)
204
205    for p in paths:
206        if not p.exists():
207            print(f"※ file not found: {p}")
208            continue
209        graph = parse_mizar(p)
210        # visualize(graph, p.with_stem(p.stem + "_graph").with_suffix(".html"))
211
212
213if __name__ == "__main__":
214    main(sys.argv[1:])
215