More verbosity options

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)

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

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

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)