diff --git a/create_content.py b/create_content.py new file mode 100644 index 0000000..320468e --- /dev/null +++ b/create_content.py @@ -0,0 +1,72 @@ +import json +from collections import namedtuple + +# Define a named tuple class +Declaration = namedtuple('Declaration', ['name', 'type', 'label', 'statement', 'proof', 'dependencies']) + +def get_label_from_docstring(docstring): + lines = docstring.split('\n') + lines = [line.strip() for line in lines] + lines = [line for line in lines if line.startswith(r'\label{')] + assert len(lines) == 1, f'Expected exactly one line starting with \label{{, got {len(lines)}' + line = lines[0] + label = line.split('{')[1] + return label + +def get_type_from_docstring(docstring): + lines = docstring.split('\n') + lines = [line.strip() for line in lines] + lines = [line for line in lines if line.startswith(r'\begin{')] + assert lines.length in {1, 2}, f'Expected exactly one or two lines starting with \begin{{, got {len(lines)}' + line = lines[0] + type = line.split('{')[1] + return type + +def short_type(type): + if type == "theorem": + return "thm" + + if type == "lemma": + return "lem" + + if type == "definition": + return "def" + + assert False, f'Unknown type {type}' + +def auto_label(name, type): + return f'{short_type(type)}:{name}' + + +# Default docstring +with open('template.tex') as f: + default_docstring = f.read() + +# Declarations and their docstrings and dependencies +with open('blueprintDecls.json') as f: + data = json.load(f) + +# Holds the declarations +decls = [] + +for item in data: + decl = Declaration(name=item[0], docstring=item[1], type=None, label=None, dependencies=item[2]) + + if decl.docstring is None: + decl.type = 'theorem' + decl.label = auto_label(decl.name, decl.type) + decl.docstring = + pass + print(item) + break + +""" +\begin{theorem} + \label{thm:pythagoras} + The square of the hypotenuse of a right triangle is equal to the sum of the squares of the other two sides. +\end{theorem} +\begin{proof} + This is a proof. +\end{proof} + +""" \ No newline at end of file diff --git a/extract.py b/extract.py deleted file mode 100644 index a71c4c7..0000000 --- a/extract.py +++ /dev/null @@ -1,93 +0,0 @@ -import os -import re - -ALLOWED_TYPES = [ - "lemma", - "theorem", - "def", - "class", - "structure", - "inductive", - "namespace", - "section", -] - - -def merge_consecutive_spaces(text): - return re.sub(r"\s+", " ", text) - - -def get_type_and_name(line): - tmp = line.split(" ") - - if len(tmp) == 1: - return tmp[0], None - - return tmp[0], tmp[1] - - -def relevant(line): - type, _ = get_type_and_name(line) - return type in ALLOWED_TYPES - - -def trim(line): - return merge_consecutive_spaces(line.strip()) - - -def readlines_raw(path): - try: - with open(path, "r") as file: - return file.readlines() - except FileNotFoundError: - raise FileNotFoundError(f"File '{path}' not found.") - - -def readlines_trimmed(path): - try: - with open(path, "r") as file: - return [trim(line) for line in file.readlines()] - except FileNotFoundError: - raise FileNotFoundError(f"File '{path}' not found.") - - -def remove_irrelevant(lines): - return [line for line in lines if relevant(line)] - - -def process(lines): - data = [None for _ in lines] - for i, line in enumerate(lines): - data[i] = get_type_and_name(line) - return data - - -def readlines_processed(path): - lines = readlines_trimmed(path) - lines = remove_irrelevant(lines) - lines = process(lines) - return lines - - -# def remove_namespace(lines): -# mask = [True for _ in lines] -# for i, line in enumerate(lines): -# if re.match(start_with_namespace, line): -# pass - - -# def remove_section(lines): -# raise NotImplementedError - - -def main(): - # Read and print the content of the file - path = os.path.join("ForMathlib", "Language.lean") - - lines = readlines_processed(path) - for line in lines: - print(line) - - -if __name__ == "__main__": - main()