Initial commit

README.md

@@ -0,0 +1,79 @@
+## Introduction: Athena's source files and their dependencies
+
+This repo contains the source code for Athena, a system for proof engineering based on polymorphic multi-sorted first-order logic. <br>
+Athena is implemented in SML. At its present state, that implementation comprises 80 files, listed in sources.cm.
+
+There are some resources in the repo that specify the dependencies between the various source files:
+
+* `file_dependencies.yaml` lists all the files that each source file depends on.
+
+* `structure_dependencies.yaml` lists all the (SML) structures defined in the code base, and for each structure S, <br> it lists all structures on which S depends.
+
+* `dependency_graph.pdf` is a graph (that can be viewed with any pdf reader, e.g., using a browser), which depicts these dependencies graphically.
+
+Note that `athena.sml` is at the top of the graph (it's essentially the 'main' file of the project), while
+`base.sml` is at the bottom.
+
+## Hacking Athena 
+
+Developing Athena is best done with smlnj. Bring up smlnj (after installing it), and then do: 
+
+`- CM.make("sources.cm");`
+
+This will compile the entire project. After compilation is done, type:
+
+`- Athena.run();`
+
+to enter Athena's main REPL (read-eval-print loop). You can then go back and make more code changes, remake the project <br>
+(by executing `- CM.make("sources.cm");` again), enter the REPL, and so on. 
+
+## Producing a stand-alone program with smlnj
+
+* Make an Athena heap image by starting smlnj, compiling (with `- CM.make("sources.cm");`), and then doing one of the following, <br> depending on how you prefer to use the stand-alone: <br>
+  * `- SMLofNJ.exportFn("athena_image",fn (_,arg1::_) => (Athena.runWithStarterFileAndQuit(SOME(arg1)); OS.Process.success));` <br> if you want the executable to take as input an Athena file, execute that file, and then quit. This will save a file athena_image.x86-linux (the extension is OS-specic).
+  * `- SMLofNJ.exportFn("athena_image",fn (_,arg1::_) => (Athena.runWithStarterFile(SOME(arg1)); OS.Process.success));` <br> if you want the executable to take as input an initial Athena file, execute it, and then go into the usual Athena REPL.<br>This will also save a file athena_image.x86-linux locally.
+
+* To start the program with an input file, do the following: `sml @SMLload=athenaImage.x86-linux input_file.ath`
+
+## Producing a stand-alone binary with MLton
+
+Simply run `./make_mlton_binary`. By default, the output will be a natively compiled executable named `athena`.<br><br>
+You can run that executable by itself (without any arguments), or you can pass it as an argument the name of an initial<br>
+Athena file to load upon starting. After loading, Athena will enter its REPL. If you want Athena to quit after loading <br>
+the initial file, pass 'quit' as the second argument to the executable (e.g., `athena some_file.ath quit`). <br><br>
+**Note**: The file `athena.mlb` contains the list of source files used by MLton. If you add/delete source files to/from<br>
+Athena, you must update both `sources.cm` and `athena.mlb` as needed.
+
+## Regression testing
+
+Run `python3 regressionTest.py`. The function `runAthenaTests` will return 0 if all the tests pass and some positive integer <br>
+less than 125 otherwise. Thus, this function can be used with `git bisect`, which is useful in debugging a range of commits. By default, <br>
+the script runs with a heap image produced by smlnj as described above, but you can also pass it (as the first argument) the name of an <br>
+executable produced by MLton (these executables tend to be faster than the heap images produced by smlnj), <br>e.g., `python3 regressionTest.py './athena'`.
+
+## Making Athena with C and XSB
+
+To make Athena with C (using MLton's [FFI](mlton.org/ForeignFunctionInterface))  and assuming you have XSB on ~/.xsb, do: <br>
+
+`mlton -default-ann 'allowFFI true' -export-header athena.h -stop tc athena.mlb`
+
+`XSB_arch='ls ~/.xsb/config'`
+
+`gcc -c -I/$XSB_HOME/emu -I/$XSB_HOME/config/$XSB_arch -O3 -fno-strict-aliasing  -Wall -pipe -D_GNU_SOURCE athena_with_xsb.c`
+
+Finally:
+
+`if [ 'uname -s' == 'Darwin' ]`<br>
+  `then mlton -drop-pass deepFlatten -default-ann 'allowFFI true' -output athena-mac -link-opt '-lm -ldl -Wl -lpthread' athena.mlb $XSB_HOME/config/$XSB_arch/saved.o/xsb.o athena_with_xsb.o`<br>
+  `else mlton -drop-pass deepFlatten -default-ann 'allowFFI true' -output athena-linux -link-opt '-lm -ldl -Wl -export-dynamic -lpthread' athena.mlb $XSB_HOME/config/$XSB_arch/saved.o/xsb.o athena_with_xsb.o`<br>
+`fi`
+
+
+## A bit of history
+
+Athena was developed by Konstantine Arkoudas, roughly between 2000 and 2015. The core of the language had more or less settled <br>
+by 2004, but there were a number of subsequent changes and extensions, some of them conceived and implemented after 2010, <br>
+such as modules, a good deal of infix syntax, proof chaining (implemented via the primitive 'chain' procedure, both for equations <br>
+and for logical implications/equivalences), integration with SMT solvers and tabled Prolog systems such as XSB, and others. 
+
+

ab.sig

@@ -0,0 +1,58 @@
+(*======================================================================
+
+The signature of assumption bases.
+
+=======================================================================*)
+
+signature ABASE = 
+sig 
+
+    type assum_base
+
+    val empty_ab: assum_base
+
+    val isMember: Prop.prop * assum_base -> bool 
+
+    val areMembers: Prop.prop list * assum_base -> bool
+
+    val insert: Prop.prop * assum_base -> assum_base
+
+    val remove: assum_base * Prop.prop  -> assum_base
+
+    val augment: assum_base * Prop.prop list -> assum_base
+
+    val fetch: assum_base * (Prop.prop -> bool) -> Prop.prop option
+
+    val fetchAll: assum_base * (Prop.prop -> bool) -> Prop.prop list
+
+    val getAll: assum_base -> Prop.prop list 
+
+    val getTag: assum_base -> int 
+
+    val getPropCode: Prop.prop -> int 
+
+    val occursFree: AthTermVar.ath_term_var * assum_base -> bool 
+
+    val occursFreeUpToSubsorting: AthTermVar.ath_term_var * assum_base -> bool 
+
+    (* occursFreeUpToSubsorting uses Prop.occursFreeUpToSubsorting *)
+
+    val propCount: unit -> int
+
+    val insertions: int ref
+
+    val look_ups: int ref
+
+    val bucketSizes: unit -> int list 
+    val getBucketSizeStatistics: unit -> string
+
+    val getAssertions: assum_base -> Prop.prop list
+    val addAssertion: Prop.prop * assum_base -> assum_base
+    val addAssertions: Prop.prop list * assum_base -> assum_base
+    val isAssertion: Prop.prop * assum_base -> bool 
+
+    val adjustHashTable: assum_base -> unit 
+
+    val top_assum_base: assum_base ref
+
+end

ab.sml

@@ -0,0 +1,242 @@
+(*======================================================================
+
+An implementation of the assumption base signature.
+
+=======================================================================*)
+
+structure ABase: ABASE = 
+struct
+
+structure HTable = HashTable
+
+exception AssumptionBase
+
+val insertions = ref(0)
+
+val look_ups = ref(0)
+
+val sizeHint = 32257
+
+open Prop
+
+val max_prop_hash_length = getMaxHashLength()
+
+val next_code = ref 2
+
+type code_type = int
+
+val hash = Prop.hash
+
+val hashtable : (prop,(code_type * bool)) HashTable.hash_table = 
+     		 HashTable.mkTable(hash, (fn (p1,p2) => (Prop.alEq(p1,p2)))) (sizeHint,AssumptionBase)
+
+fun bucketSizes() = HashTable.bucketSizes(hashtable)
+
+fun getBucketSizeStatistics() = 
+      let val bucket_sizes = bucketSizes()
+          val max_bucket_size = Basic.maxLst(bucket_sizes)
+          val _ = print("\nMax bucket size: "^(Int.toString(max_bucket_size)))
+          val A = Array.array(max_bucket_size + 1,0)
+          fun loop([]) = ()
+            | loop(sz::more) = (Array.update(A,sz,Array.sub(A,sz) + 1);loop(more))
+          val _ = loop(bucket_sizes)
+          val str = "\nThere were "^(Int.toString(length(bucket_sizes)))^" buckets in total."
+          val str1 = "\nThe sizes were distributed as follows:\n\n"
+          val AL:int list = Basic.arrayToList(A)
+          val lines = Basic.mapWithIndex((fn (x,i) => "There were "^(Int.toString(x))^" buckets of size "^(Int.toString(i))),AL)
+          val str2 = Basic.printListStr(lines,fn x => x,"\n")
+      in
+         str^str1^str2
+      end
+
+fun propCount() = HashTable.numItems(hashtable)
+
+fun printHashTable() = 
+   let val pair_list: (prop * (code_type * bool)) list = HashTable.listItemsi(hashtable)
+      val res =       Basic.printListStr(pair_list,fn (p,(i,b)) => let val s1 = "\nHT prop: "
+                                                                       val s2 = (Prop.toPrettyStringDefault(0,p))
+								       val s3 = ", HT code: " ^ (Int.toString(i))
+								       val s4 = " and HT assertion type: " ^ (Basic.boolToString(b))
+                                                                   in
+								      s1 ^ s2 ^ s3 ^ s4
+                                                                   end,
+                                         "\n")
+
+   in
+      res 
+   end
+
+fun getPropCodeAux P = 
+   let val res = (case (HashTable.find hashtable P) of 
+                          SOME (i,_) => i
+                       | _ => let val i = !next_code
+                                  val _ = next_code := !next_code + 1
+                                  in
+                                    (HashTable.insert hashtable (P,(i,false));i)
+                                  end)
+   in
+     res
+    end
+
+val no_adjustments_yet = ref(true)
+
+fun getPropCode(P) = 
+    if !no_adjustments_yet then
+       case getCode(P) of
+          ref(SOME(i)) => i
+        | _ => let val i = getPropCodeAux(P)
+               in
+                 (setCode(P,i);i)
+               end
+    else getPropCodeAux(P)			    
+
+val next_ab_tag = ref 0
+
+fun hashFun(code:int,tag:int) = Basic.hashPair(code,tag)
+
+fun equalityFun((code1,tag1),(code2,tag2)) = code1 = code2 andalso tag1 = tag2
+
+val memoization_table: ((int * int),bool) HashTable.hash_table = HashTable.mkTable(hashFun, equalityFun) (3467,AssumptionBase)
+
+val count = ref 0
+
+val inc = Basic.incAndReturn
+
+structure Table = IntMapTable(type key = int 
+                              fun getInt(n) = n)
+
+datatype assum_base = abase of {prop_table: prop IntBinaryMap.map,tag:int}
+
+fun getTag(abase({tag,...})) = tag
+
+val empty_prop_table: prop IntBinaryMap.map = IntBinaryMap.empty
+
+val empty_ab = abase {prop_table=empty_prop_table,tag=0}
+
+val assertions = ref(empty_prop_table)
+
+fun remove(ab as (abase {prop_table,tag,...}),P) = 
+  let val code = getPropCode(P)
+      val (m,_) = (IntBinaryMap.remove(prop_table,code)) handle _ => (prop_table,P)
+  in
+    abase({prop_table=m,tag=inc(next_ab_tag)})
+  end 
+
+fun addAssertion(p,abase({prop_table,tag,...}):assum_base) = 
+ let val _ = (case (HashTable.find hashtable p) of 
+                 SOME (i,_) => (HashTable.insert hashtable (p,(i,true)))
+               | _ => let val i = !next_code
+                          val _ = next_code := !next_code + 1
+                      in
+                        ((HashTable.insert hashtable (p,(i,true)));
+                         setCode(p,i))
+                      end)
+ in
+   abase({prop_table=prop_table,tag=inc(next_ab_tag)})
+ end
+
+fun addAssertions(props,beta:assum_base) = 
+  let fun loop([],res) = res
+        | loop(a::more,res) = loop(more,addAssertion(a,res))
+  in loop(props,beta) end
+
+fun isAssertion(p,abase({prop_table,...}):assum_base) = 
+      (case IntBinaryMap.find(prop_table,getPropCode(p)) of
+           NONE => false
+         | _ => (case (HashTable.find hashtable p) of 
+                    SOME (_,b) => b
+                  | _ => false))
+
+fun isAssertionAlt(p) = 
+                (case (HashTable.find hashtable p) of 
+                    SOME (_,b) => b
+                  | _ => false)
+
+fun getAssertions(abase({prop_table,...}):assum_base) =  
+      List.filter isAssertionAlt (IntBinaryMap.listItems prop_table)
+
+fun isMember(P,ab as abase({prop_table,...}): assum_base) = 
+       (Basic.inc(look_ups);
+        let val code = getPropCode(P)
+        in
+         (case IntBinaryMap.find(prop_table,code) of
+             NONE => false
+           | _ => true)
+        end)
+
+fun adjustHT(ab) = 
+ let val _ = HashTable.filteri (fn (p,_) => isMember(p,ab)) hashtable 
+ in
+    no_adjustments_yet := false
+ end
+
+val adjustment_size_trigger_1 = 1000000
+val adjustment_size_trigger_2 = 2000000
+
+fun adjustHashTable(ab:assum_base as abase({prop_table,...})) =
+       let val hash_table_count = HashTable.numItems(hashtable)
+           val ab_count = Table.domainSize(prop_table)
+           val deciding_condition_1 = (hash_table_count > adjustment_size_trigger_1 andalso hash_table_count < adjustment_size_trigger_2 
+                                       andalso hash_table_count > 7 * ab_count)
+           val deciding_condition_2 = (hash_table_count > adjustment_size_trigger_2
+                                       andalso hash_table_count >= 2 * ab_count)
+       in
+         if deciding_condition_1 orelse deciding_condition_2 then adjustHT(ab) else ()
+       end
+
+fun isMemberMem(P,ab as abase({prop_table,tag,...}): assum_base) = 
+       (Basic.inc(look_ups);
+        let val code = getPropCode(P)
+        in
+           (case (HashTable.find memoization_table (code,tag)) of
+               SOME(res) => res 
+              | _ => (case IntBinaryMap.find(prop_table,code) of
+                         NONE => let val res = false
+                                     val _ = HashTable.insert memoization_table ((code,tag),res)
+                                 in
+                                    res
+                                 end
+                       | _ => let val res = true 
+                                     val _ = HashTable.insert memoization_table ((code,tag),res)
+                                 in
+                                    res
+                                 end))
+        end)
+
+fun areMembers(props,ab) = List.all (fn p => isMember(p,ab)) props
+
+fun insertAux(P,ab as abase({prop_table,tag,...}): assum_base) =  
+     let val _ = Basic.inc(insertions)
+	 val code = getPropCode(P)
+     in 
+       abase({prop_table=IntBinaryMap.insert(prop_table,code,P),tag=inc(next_ab_tag)})
+     end
+
+fun insert(P,ab) =  insertAux(P,ab)
+
+fun augment(ab,props) = List.foldl insert ab props
+
+fun getAll(ab as abase({prop_table,...}):assum_base) = IntBinaryMap.listItems(prop_table)
+
+fun occursFree(v,ab) = List.exists (fn (P) => Prop.occursFree(v,P)) (getAll ab) 
+
+fun occursFreeUpToSubsorting(v,ab) = List.exists (fn (P) => Prop.occursFreeUpToSubsorting(v,P)) (getAll ab) 
+
+fun fetchAll(ab as abase({prop_table,...}):assum_base,test) = 
+    IntBinaryMap.foldl (fn (P,accum) => if test(P) then P::accum else accum) [] prop_table
+
+exception FetchResult of Prop.prop
+
+fun fetch(ab as abase({prop_table,...}):assum_base,test) = 
+      let fun f() = IntBinaryMap.foldl 
+                    (fn (P,accum) => if test(P) then raise FetchResult(P) else accum) [] prop_table;
+      in
+         (f();NONE) handle FetchResult(P) => SOME(P)
+      end
+
+val top_assum_base = ref(empty_ab)
+
+end
+
+
+