make structural validation optional, mark lemmas as imported

Author: konstantinosKokos

scripts/preprocess.py

@@ -4,7 +4,7 @@
 
 
 if __name__ == '__main__':
-    files = [tokenize_file(file) for file in parse_dir('../data/stdlib', False)]
+    files = [tokenize_file(file) for file in parse_dir('../data/stdlib', strict=False, validate=True)]
 
     print(f'Tokenized {len(files)} files with {sum(len(file.hole_asts) for file in files)} holes.')
     with open('../data/tokenized.p', 'wb') as f:

src/Name/data/agda/operations.py

@@ -14,7 +14,8 @@ def enum_references(file: File[Name]) -> tuple[File[int], dict[int, Name]]:
                 name=name_to_index[entry.name],
                 type=entry.type.substitute(name_to_index),
                 definition=entry.definition.substitute(name_to_index),
-                holes=[hole.substitute(name_to_index) for hole in entry.holes])
+                holes=[hole.substitute(name_to_index) for hole in entry.holes],
+                is_import=entry.is_import)
             for entry in file.scope])
     return file, index_to_name
 
@@ -59,7 +60,7 @@ def top_sort_entries(file: File[Name]) -> dict[Name, int]:
         pre_resolved=dict())
 
 
-def merge_contexts(file: File[Name], merge_holes: bool, unique_only: bool) -> File[Name]:
+def merge_contexts(file: File[Name], merge_holes: bool, unique_only: bool, validate: bool = True) -> File[Name]:
     def ctx_to_pi(hole: Hole[Name]) -> Hole[Name]:
         return Hole(
             context=(),
@@ -84,8 +85,10 @@ def f(holes: list[Hole[Name]]) -> list[Hole[Name]]:
                 name=entry.name,
                 type=entry.type,
                 definition=entry.definition,
-                holes=f([ctx_to_pi(h) for h in entry.holes]))
-            for entry in file.scope])
+                holes=f([ctx_to_pi(h) for h in entry.holes]),
+                is_import=entry.is_import)
+            for entry in file.scope],
+        validate=validate)
 
 
 def _merge_holes(holes: list[Hole[Name]]) -> list[Hole[Name]]:

src/Name/data/agda/reader.py

@@ -19,36 +19,38 @@ def wrapper(json: dict) -> T:
     return wrapper if DEBUG else wrapped
 
 
-def parse_dir(directory: str, strict: bool) -> Iterator[File[str]]:
+def parse_dir(directory: str, strict: bool, validate: bool = True) -> Iterator[File[str]]:
     for file in listdir(directory):
         print(f'Parsing {file}')
         try:
-            yield parse_file(path.join(directory, file))
+            yield parse_file(path.join(directory, file), validate)
         except AssertionError as e:
             if strict:
                 raise e
             print(f'\tFailed: {e}.')
             continue
 
 
-def parse_file(filepath: str) -> File[str]:
+def parse_file(filepath: str, validate: bool) -> File[str]:
     with open(filepath, 'r') as f:
-        return parse_data(load(f))
+        return parse_data(load(f), validate=validate)
 
 
-def parse_data(json: dict) -> File[str]:
+def parse_data(json: dict, validate: bool) -> File[str]:
     return File(
         name=json['name'],
         scope=[parse_scope_entry(d, True) for d in json['scope-global']] +
-              [parse_scope_entry(d, False) for d in json['scope-local']])
+              [parse_scope_entry(d, False) for d in json['scope-local']],
+        validate=validate)
 
 
 def parse_scope_entry(json: dict, is_import: bool) -> ScopeEntry[str]:
     return ScopeEntry(
         name=json['name'],
         type=parse_term(json['type']),
         definition=parse_definition(json['definition']),
-        holes=[] if is_import else [parse_hole(hole) for hole in json['holes']])
+        holes=[] if is_import else [parse_hole(hole) for hole in json['holes']],
+        is_import=is_import)
 
 
 @debug

src/Name/data/agda/syntax.py

@@ -20,10 +20,12 @@ def substitute(self, names: dict[Name, Other]) -> Self: ...
 class File(_AgdaExpr[Name]):
     name: str
     scope: list[ScopeEntry[Name]]
+    validate: bool = True
 
     def __post_init__(self):
-        assert self.valid_reference_structure(), 'Invalid reference structure.'
-        assert self.unique_entry_names(), 'Duplicate entry names.'
+        if self.validate:
+            assert self.valid_reference_structure(), 'Invalid reference structure.'
+            assert self.unique_entry_names(), 'Duplicate entry names.'
 
     def valid_reference_structure(self) -> bool:
         names = [entry.name for entry in self.scope]
@@ -66,6 +68,7 @@ def substitute(self, names: dict[Name, Other]) -> NamedType[Other]:
 class ScopeEntry(NamedType[Name]):
     definition: AgdaDefinition[Name]
     holes: list[Hole[Name]]
+    is_import: bool
 
     def __repr__(self) -> str:
         return f'{super(ScopeEntry, self).__repr__()} ({len(self.holes)} holes)'
@@ -75,7 +78,8 @@ def substitute(self, names: dict[Name, Other]) -> ScopeEntry[Other]:
             name=names[self.name],
             type=self.type.substitute(names),
             definition=self.definition.substitute(names),
-            holes=[hole.substitute(names) for hole in self.holes])
+            holes=[hole.substitute(names) for hole in self.holes],
+            is_import=self.is_import)
 
 
 @dataclass(frozen=True)