proof-truth/Dataset/get_proof.py at main · jableable/proof-truth · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
import re
from collections import defaultdict
import pandas as pd
from metamath import Metamath
import ast


df = pd.read_csv('tag.csv',na_values=['']).iloc[:]
tag_dict = df.to_dict(orient='index')
thrd = 0
metamath = Metamath('metamath/metamath.exe')    #path from this file to metamath.exe
print(metamath.initialize(thrd))
print(metamath.send(thrd,'read "metamath/set_normal.mm"'))
print(metamath.send(thrd,'set height 1000000'))
print(metamath.send(thrd,'set width 1000000'))

tags = {}
error_tag = []
count = 0


for tag in tag_dict:
    tag_name = tag_dict[tag]['tag']

    if tag_name in tags:
        print(f"SameName error {tag_name}")
    if tag_dict[tag]['statement'].startswith('$p'):
        print(count,tag_name,tag_dict[tag]['statement'])
        count += 1
    else:
        continue
    try:
        output = metamath.send(thrd,'show proof '+str(tag_name) +'/lemmon')
    except:
        error_tag.append(tag_name)
        print(f"unknown error:  {tag_name}")
        thrd += 1
        print(metamath.initialize(thrd))
        print(metamath.send(thrd,'read "metamath/set.mm"'))
        print(metamath.send(thrd,'set height 1000000'))
        print(metamath.send(thrd,'set width 100000'))
        continue
    lines = output.split('\n')[:-1]

    if pd.isna(tag_dict[tag]['hypothesis_s']):
        tag_dict[tag]['hypothesis_s'] = "{}"
    tag_dict[tag]['hypothesis_s'] = ast.literal_eval(tag_dict[tag]['hypothesis_s'])

    tags[tag_name] = {}
    tags[tag_name]['tag'] = tag_name
    tags[tag_name]['proof'] = {}
    tags[tag_name]['node'] = {}
    tags[tag_name]['hpt'] = {}
    proof_raw = []
    for line in lines:
        line = line.strip()
        match = re.match(r'(\d+)(\s+)(\S+)(\s+)(\S+)(\s+)(\S+)(\s+)(\$.*)', line)
        if match:
            step = match.group(1)
            hpt = match.group(3)
            label = match.group(5)
            statement = match.group(9)
            tags[tag_name]['proof'][int(step)] = statement
            if label not in tags[tag_name]['node']:
                tags[tag_name]['node'][label] ={}
            tags[tag_name]['node'][label][int(step)] = [int(h) for h in hpt.split(',')]
        else:
            match = re.match(r'(\d+)(\s+)(\S+)(\s+)(\S+)(\s+)(\$.*)', line)
            if match:
                if match.group(5).startswith("@"):
                    step = match.group(1)
                    label = match.group(3)
                    if label in tag_dict[tag]['hypothesis_s']:
                        print(1/0)
                        if match.group(3) in tags[tag_name]['hpt']:
                            tags[tag_name]['hpt'][label].append(int(step))
                        else:
                            tags[tag_name]['hpt'][label] = [int(step)]
                    if label not in tags[tag_name]['node']:
                        tags[tag_name]['node'][label] ={}
                    tags[tag_name]['node'][label][int(step)] = []

                    statement = match.group(7)
                    tags[tag_name]['proof'][int(step)] = statement
                else:
                    step = match.group(1)
                    hpt = match.group(3)
                    label = match.group(5)
                    statement = match.group(7)
                    tags[tag_name]['proof'][int(step)] = statement
                    if label not in tags[tag_name]['node']:
                        tags[tag_name]['node'][label] ={}
                    tags[tag_name]['node'][label][int(step)] = [int(h) for h in hpt.split(',')]
            else:
                match = re.match(r'(\d+)(\s+)(\S+)(\s+)(\$.*)', line)
                if not match:
                    print(f"Matching Error {line}")
                    error_tag.append(tag_name)
                    continue
                step = match.group(1)
                if match.group(3).startswith("@"):
                    statement = match.group(3)
                else:
                    label = match.group(3)
                    if label in tag_dict[tag]['hypothesis_s']:
                        if match.group(3) in tags[tag_name]['hpt']:
                            tags[tag_name]['hpt'][match.group(3)].append(int(step))
                        else:
                            tags[tag_name]['hpt'][match.group(3)] = [int(step)]
                    statement = match.group(5)
                tags[tag_name]['proof'][int(step)] = statement
                if label not in tags[tag_name]['node']:
                    tags[tag_name]['node'][label] ={}
                tags[tag_name]['node'][label][int(step)] = []


    if error_tag and tag_name == error_tag[-1]:
        continue


print(f"Error Tag: {error_tag}")
df_out = pd.DataFrame(tags.values())
df_out.to_csv('tag_proof4.csv', index=False)