From 2ee5b8da58990d0f5f3a1570452b94695d65d368 Mon Sep 17 00:00:00 2001 From: Calvin Josenhans Date: Sat, 21 Dec 2024 21:48:38 -0500 Subject: [PATCH] More verbosity options --- abstract_syntax.py | 16 ++++++++++++---- deduce.py | 12 +++++++++--- error.py | 23 +++++++++++++++++++++++ proof_checker.py | 24 +++++++++++++++--------- 4 files changed, 59 insertions(+), 16 deletions(-) diff --git a/abstract_syntax.py b/abstract_syntax.py index 8cce546..2328df8 100644 --- a/abstract_syntax.py +++ b/abstract_syntax.py @@ -1,7 +1,7 @@ from dataclasses import dataclass, field from lark.tree import Meta from typing import Any, Tuple, List -from error import error, set_verbose, get_verbose +from error import error, set_verbose, get_verbose, get_unique_names, VerboseLevel from pathlib import Path import os @@ -503,12 +503,14 @@ def __str__(self): 'resolved_names is a string but should be a list: ' \ + self.resolved_names) - if base_name(self.name) == 'zero' and not get_verbose(): + if base_name(self.name) == 'zero' and not get_unique_names() and not get_verbose(): return '0' - elif base_name(self.name) == 'empty' and not get_verbose(): + elif base_name(self.name) == 'empty' and not get_unique_names() and not get_verbose(): return '[]' elif get_verbose(): return self.name + '{' + ','.join(self.resolved_names) + '}' + elif get_unique_names(): + return self.name else: if is_operator(self): return 'operator ' + base_name(self.name) @@ -2411,6 +2413,10 @@ def __str__(self): def uniquify(self, env): if get_verbose(): print('uniquify import ' + self.name) + old_verbose = get_verbose() + if get_verbose() == VerboseLevel.CURR_ONLY: + set_verbose(VerboseLevel.NONE) + global uniquified_modules if self.name in uniquified_modules.keys(): self.ast = uniquified_modules[self.name] @@ -2434,6 +2440,7 @@ def uniquify(self, env): stmt.collect_exports(env) if get_verbose(): print('\tuniquify finished import ' + self.name) + set_verbose(old_verbose) def collect_exports(self, export_env): pass @@ -2611,6 +2618,7 @@ def __str__(self): class TermBinding(Binding): typ : Type defn : Term = None + local : bool = False def __str__(self): return str(self.typ) + (' = ' + str(self.defn) if self.defn else '') @@ -2640,7 +2648,7 @@ def __contains__(self, item): def proofs_str(self): return ',\n'.join(['\t' + base_name(k) + ': ' + str(v) \ for (k,v) in reversed(self.dict.items()) \ - if isinstance(v,ProofBinding) and (v.local or get_verbose())]) + if isinstance(v,ProofBinding) and (v.local or get_verbose() == VerboseLevel.FULL)]) def declare_type(self, loc, name): new_env = Env(self.dict) diff --git a/deduce.py b/deduce.py index 90f6719..f148f3f 100644 --- a/deduce.py +++ b/deduce.py @@ -1,6 +1,6 @@ -from error import set_verbose, get_verbose +from error import set_verbose, get_verbose, set_unique_names, get_unique_names from proof_checker import check_deduce, uniquify_deduce -from abstract_syntax import add_import_directory, print_theorems, get_recursive_descent, set_recursive_descent, get_uniquified_modules, add_uniquified_module +from abstract_syntax import add_import_directory, print_theorems, get_recursive_descent, set_recursive_descent, get_uniquified_modules, add_uniquified_module, VerboseLevel import sys import os import parser @@ -93,8 +93,14 @@ def deduce_directory(directory, recursive_directories): if argument == '--error': error_expected = True + elif argument == '--unique-names': + set_unique_names(True) elif argument == '--verbose': - set_verbose(True) + if i + 1 < len(sys.argv) and sys.argv[i+1] == 'full': + set_verbose(VerboseLevel.FULL) + set_unique_names(True) + else: + set_verbose(VerboseLevel.CURR_ONLY) elif argument == '--dir': add_import_directory(sys.argv[i+1]) already_processed_next = True diff --git a/error.py b/error.py index 329b5d0..19bc0aa 100644 --- a/error.py +++ b/error.py @@ -1,3 +1,24 @@ +from enum import Enum + +class VerboseLevel(Enum): + NONE = 0 + CURR_ONLY = 1 + FULL = 2 + +# flag for displaying uniquified names + +unique_names = False + +def set_unique_names(b): + global unique_names + unique_names = b + +def get_unique_names(): + global unique_names + return unique_names + +# flag for verbose trace + verbose = False def set_verbose(b): @@ -6,6 +27,8 @@ def set_verbose(b): def get_verbose(): global verbose + if verbose == VerboseLevel.NONE: + return False return verbose # flag for expect fail diff --git a/proof_checker.py b/proof_checker.py index c038285..3054b59 100644 --- a/proof_checker.py +++ b/proof_checker.py @@ -20,7 +20,7 @@ # and run the print and assert statements. from abstract_syntax import * -from error import error, incomplete_error, warning, error_header, get_verbose, set_verbose, IncompleteProof +from error import error, incomplete_error, warning, error_header, get_verbose, set_verbose, IncompleteProof, VerboseLevel imported_modules = set() checked_modules = set() @@ -2300,7 +2300,12 @@ def process_declaration(stmt, env): return Union(loc, name, typarams, new_alts), env case Import(loc, name, ast): + old_verbose = get_verbose() + if get_verbose() == VerboseLevel.CURR_ONLY: + set_verbose(VerboseLevel.NONE) + if name in imported_modules: + set_verbose(old_verbose) return stmt, env else: imported_modules.add(name) @@ -2322,6 +2327,7 @@ def process_declaration(stmt, env): check_proofs(s, env) checked_modules.add(name) + set_verbose(old_verbose) return Import(loc, name, ast3), env case Assert(loc, frm): @@ -2499,23 +2505,23 @@ def check_deduce(ast, module_name): new_s, env = process_declaration(s, env) ast2.append(new_s) if get_verbose(): - for s in ast2: - print(s) + for s in ast2: + print(s) if get_verbose(): - print('env:\n' + str(env)) - print('--------- Type Checking ------------------------') + print('env:\n' + str(env)) + print('--------- Type Checking ------------------------') ast3 = [] for s in ast2: new_s = type_check_stmt(s, env) ast3.append(new_s) if get_verbose(): - for s in ast3: - print(s) + for s in ast3: + print(s) if get_verbose(): - print('env:\n' + str(env)) - print('--------- Proof Checking ------------------------') + print('env:\n' + str(env)) + print('--------- Proof Checking ------------------------') for s in ast3: env = collect_env(s, env)