Readd the prelude

deduce.py

@@ -1,3 +1,5 @@
+from abstract_syntax import Import
+from lark.tree import Meta
 from flags import *
 from proof_checker import check_deduce, uniquify_deduce, is_modified
 from abstract_syntax import init_import_directories, add_import_directory, print_theorems, get_recursive_descent, set_recursive_descent, get_uniquified_modules, add_uniquified_module, VerboseLevel
@@ -18,12 +20,11 @@ def handle_sigint(signal, stack_frame):
     print('SIGINT caught, exiting...')
     exit(137)
 
-def deduce_file(filename, error_expected):
+def deduce_file(filename, error_expected, prelude : list[str]) -> None:
     if get_verbose():
         print("Deducing file:", filename)
     module_name = Path(filename).stem
     try:
-
         if module_name in get_uniquified_modules().keys():
             ast = get_uniquified_modules()[module_name]
         else:
@@ -48,6 +49,17 @@ def deduce_file(filename, error_expected):
                 print("abstract syntax tree:\n" \
                       +'\n'.join([str(s) for s in ast])+"\n\n")
                 print("starting uniquify:\n" + '\n'.join([str(d) for d in ast]))
+
+            if len(prelude) > 0: 
+                # Create a new AST for the import statements
+                ast2 = []
+                for name in prelude:
+                    import_stmt = Import(Meta(), name, visibility='private')
+                    ast2.append(import_stmt)
+                # Add import statements at front of original AST
+                ast2 += ast
+                ast = ast2
+
             uniquify_deduce(ast)
             if get_verbose():
                 print("finished uniquify:\n" + '\n'.join([str(d) for d in ast]))
@@ -76,14 +88,27 @@ def deduce_file(filename, error_expected):
             # during development, reraise
             # raise e
 
-def deduce_directory(directory, recursive_directories):
+def deduce_directory(directory, recursive_directories, prelude) -> None:
     for file in sorted(os.listdir(directory)):
         fpath = os.path.join(directory, file)
         if os.path.isfile(fpath):
             if file[-3:] == '.pf':
-                deduce_file(fpath, error_expected)
+                deduce_file(fpath, error_expected, prelude)
         elif recursive_directories and os.path.isdir(fpath):
-            deduce_directory(fpath, recursive_directories)
+            deduce_directory(fpath, recursive_directories, prelude)
+
+def check_in_prelude(deducable : str, stdlib_dir : str) -> bool:
+    deducable_path = Path(deducable)
+    stdlib_path = Path(stdlib_dir)
+    if deducable_path.is_file():
+        return deducable_path.parent.absolute() == stdlib_path
+    elif deducable_path.is_dir():
+        return deducable_path.absolute() == stdlib_path.absolute()
+    else:
+        # If the funciton reaches this point then the path does not exist
+        # However, there is handling for that in another place
+        # So return false
+        return False
 
 if __name__ == "__main__":
     signal(SIGINT, handle_sigint)
@@ -92,7 +117,7 @@ def deduce_directory(directory, recursive_directories):
     if (sys.argv[0] == 'deduce.py'):
         sys.argv[0] = os.path.join(os.getcwd(), sys.argv[0])
 
-    stdlib_dir = os.path.join(os.path.dirname(sys.argv[0]), 'lib/')
+    stdlib_dir = os.path.join(os.path.dirname(sys.argv[0]), 'lib')
     add_stdlib = True
     deducables = []
     error_expected = False
@@ -145,9 +170,15 @@ def deduce_directory(directory, recursive_directories):
         else:
             deducables.append(argument)
 
+    prelude = []
     if add_stdlib:
         add_import_directory(stdlib_dir)
-
+        # Find files in the prelude
+        # For now we consider the entire stdlib the prelude
+        for file in sorted(os.listdir(stdlib_dir)):
+            if file.endswith('.pf'):
+                prelude.append(file.removesuffix('.pf'))
+
     if len(deducables) == 0:
         print("Couldn't find a file to deduce!")
         exit(1)
@@ -163,10 +194,19 @@ def deduce_directory(directory, recursive_directories):
     # Start deducing
 
     for deducable in deducables:
+        # If a file is in the prelude and we include the prelude
+        # Then we'll process the file twice, hence using an empty "prelude"
+        # For said file
+
+        if check_in_prelude(deducable, stdlib_dir):
+            deducable_prelude = []
+        else:
+            deducable_prelude = prelude
+
         if os.path.isfile(deducable):
-            deduce_file(deducable, error_expected)
+            deduce_file(deducable, error_expected, deducable_prelude)
         elif os.path.isdir(deducable):
-            deduce_directory(deducable, recursive_directories)
+            deduce_directory(deducable, recursive_directories, deducable_prelude)
         else:
             print(deducable, "was not found!")
             exit(1)

proof_checker.py

@@ -2377,10 +2377,11 @@ def process_declaration_visibility(decl : Declaration, env: Env, module_chain, d
             ast2.append(new_s)
 
           ast3 = []
-          already_done_imports = set()
+          already_done_imports : dict[str, bool] = {}
           for s in ast2:
             new_s = type_check_stmt(s, env, already_done_imports)
-            ast3.append(new_s)
+            if new_s != None:
+              ast3.append(new_s)
 
           if needs_checking[0]:
               dirty_files.add(name)
@@ -2466,7 +2467,7 @@ def type_check_fun_case(fun_case, name, params, returns, body_env, cases_present
     return FunCase(fun_case.location, fun_case.rator,
                    fun_case.pattern, fun_case.parameters, new_body)
 
-def type_check_stmt(stmt, env, already_done_imports : set):
+def type_check_stmt(stmt, env, error_on_next_import : dict[str, bool]):
   if get_verbose():
     print('type_check_stmt(' + str(stmt) + ')')
   match stmt:
@@ -2552,9 +2553,19 @@ def type_check_stmt(stmt, env, already_done_imports : set):
         return stmt
 
     case Import(loc, name, ast):
-      if name in already_done_imports:
-        error(loc, "error, module:\n\t" + name + "\nwas imported twice")
-      already_done_imports.add(name)
+      if name in error_on_next_import:
+        if error_on_next_import[name]:
+          # The first import was from the prelude
+          # So instead of erroring we'll error next time
+          # and return None to signal that this stmt should be removed
+          error_on_next_import[name] = True
+          return None # Return none to signify that this stmt should be removed
+        else:
+          # The user manually imported the module twice, so throw an error
+          error(loc, "error, module:\n\t" + name + "\nwas imported twice")
+
+      # If loc is empty then this import comes from the prelude
+      error_on_next_import[name] = loc.empty
       return stmt
 
     case Assert(loc, frm):
@@ -2903,11 +2914,13 @@ def check_deduce(ast, module_name, modified):
     print('--------- Type Checking ------------------------')
   ast3 = []
 
-  already_done_imports = set()
+  error_on_next_import : dict[str, bool] = {}
   for s in ast2:
-    new_s = type_check_stmt(s, env, already_done_imports)
-    ast3.append(new_s)
-
+    new_s = type_check_stmt(s, env, error_on_next_import)
+    # If None gets returned we want to remove the current statement
+    # Which is represented by not appending it to the new ast
+    if new_s != None:
+      ast3.append(new_s)
   if get_verbose():
     for s in ast3:
       print(s)
@@ -2922,6 +2935,3 @@ def check_deduce(ast, module_name, modified):
       if needs_checking[0]:
         check_proofs(s, env)
     checked_modules.add(module_name)  
-
-
-

test-deduce.py

@@ -9,6 +9,7 @@
 
 lib_dir = './lib'
 pass_dir = './test/should-validate'
+prelude_dir = './test/prelude'
 error_dir = './test/should-error'
 test_imports_dir = './test/test-imports'
 site_dir = './gh_pages/deduce-code'
@@ -235,20 +236,22 @@ def test_deduce_errors(deduce_call, path):
         # test generated files
         for f in sorted(os.listdir(pass_dir)):
             if f.startswith('doc_') and f.endswith('.pf'):
-                test_deduce(parsers, deduce_call, pass_dir + '/' + f)
+                test_deduce(parsers, deduce_call + f' --no-stdlib --dir {test_imports_dir} --dir {lib_dir} ', pass_dir + '/' + f)
     elif test_lib:
         test_deduce(parsers, deduce_call, lib_dir)
     elif test_passable:
-        test_deduce(parsers, deduce_call +  f' --dir {test_imports_dir} --dir {lib_dir} ', [pass_dir, './example.pf'])
+        test_deduce(parsers, deduce_call +  f' --no-stdlib --dir {test_imports_dir} --dir {lib_dir} ', [pass_dir, './example.pf'])
+        test_deduce(parsers, deduce_call, prelude_dir)
     elif test_errors:
-        test_deduce_errors(deduce_call +  f' --dir {test_imports_dir} --dir {lib_dir} ', error_dir)
+        test_deduce_errors(deduce_call +  f' --no-stdlib --dir {test_imports_dir} --dir {lib_dir} ', error_dir)
     elif test_parse:
-        test_deduce_errors(deduce_call + f' --dir {lib_dir} ', parse_dir)
+        test_deduce_errors(deduce_call + f' --no-stdlib --dir {lib_dir} ', parse_dir)
     else:
         # By default, test everything except for the doc code that gets
         # generated by doc.convert, because that requires markdown and
         # Jeremy doesn't have that installed.
         # Also not the parse errors
-        test_deduce(parsers, deduce_call +  f' --dir {test_imports_dir} --dir {lib_dir} ', [lib_dir, pass_dir, './example.pf'])
-        test_deduce_errors(deduce_call +  f' --dir {test_imports_dir} --dir {lib_dir} ', error_dir)    
-        test_deduce_errors(deduce_call + f' --dir {lib_dir} ', parse_dir)
+        test_deduce(parsers, deduce_call, lib_dir) 
+        test_deduce(parsers, deduce_call +  f' --no-stdlib --dir {test_imports_dir} --dir {lib_dir} ', [pass_dir, './example.pf'])
+        test_deduce(parsers, deduce_call, prelude_dir)
+        test_deduce_errors(deduce_call +  f' --no-stdlib --dir {test_imports_dir} --dir {lib_dir} ', error_dir)    

test/prelude/base_prelude.pf

@@ -0,0 +1,6 @@
+theorem or_not_again: all P:bool, Q:bool.
+  if (P or Q) and not P
+  then Q
+proof
+  or_not
+end

test/prelude/bigo_prelude.pf

@@ -0,0 +1,4 @@
+theorem bigo_refl_again: all f : fn UInt -> UInt. f ≲ f
+proof
+  bigo_refl
+end

test/prelude/import_the_entire_prelude.pf

@@ -0,0 +1,15 @@
+import Base
+import BigO
+import Int
+import List
+import Maps
+import MultiSet
+import Nat
+import Option
+import Pair
+import Set
+import UInt
+
+// This test ensures that the prelude imports don't trigger an error
+// So any code that validates will suffice
+assert true = true

test/prelude/int_prelude.pf

@@ -0,0 +1,4 @@
+theorem int_less_equal_refl_again: all n:Int. n ≤ n
+proof
+    int_less_equal_refl
+end

test/prelude/list_prelude.pf

@@ -0,0 +1,5 @@
+theorem length_append_again: all U :type, xs :List<U>, ys :List<U>.
+  length(xs ++ ys) = length(xs) + length(ys)
+proof
+  length_append
+end

test/prelude/maps_prelude.pf

@@ -0,0 +1,6 @@
+theorem combine_left_again: all T:type, U:type, f:fn(T)->Option<U>, g:fn(T)->Option<U>, x:T.
+  if g(x) = none
+  then combine(f, g)(x) = f(x)
+proof
+  combine_left
+end

test/prelude/multiset_prelude.pf

@@ -0,0 +1,4 @@
+theorem cnt_empty_again: all T:type. all x:T. cnt(@m_empty<T>())(x) = 0
+proof
+    cnt_empty
+end

test/prelude/nat_prelude.pf

@@ -0,0 +1,4 @@
+theorem int_less_equal_refl_again: all n:Int. n ≤ n
+proof
+    int_less_equal_refl
+end

test/prelude/option_prelude.pf

@@ -0,0 +1 @@
+assert just(5) = just(5)

test/prelude/pair_prelude.pf

@@ -0,0 +1,4 @@
+theorem first_pair_again: all T:type,U:type, x:T, y:U. first(pair(x,y)) = x
+proof
+    first_pair
+end

test/prelude/set_prelude.pf

@@ -0,0 +1,4 @@
+theorem single_member_again: <T> all x:T.  x ∈ single(x)
+proof
+    single_member
+end

test/prelude/uint_prelude.pf

@@ -0,0 +1,5 @@
+theorem toNat_add_again: all x:UInt, y:UInt.
+  toNat(x + y) = toNat(x) + toNat(y)
+proof
+    toNat_add
+end