cleanup. fixed failing test

philzook58 · Jan 26, 2025 · 28cf767 · 28cf767
1 parent 1cf7045
commit 28cf767
Show file tree

Hide file tree

Showing 10 changed files with 29 additions and 4 deletions.
diff --git a/kdrag/datatype.py b/kdrag/datatype.py
@@ -1,5 +1,6 @@
 """
-Goodies related to datatypes.
+Convenience features for datatypes.
+
 You should use these instead of raw `smt.Datatype`. This also maintains a record of exisitng datatypes
 so that you don't clobber old ones, a possible source of unsoundness.
 

diff --git a/kdrag/hypothesis.py b/kdrag/hypothesis.py
@@ -1,3 +1,14 @@
+"""
+Helper functions for the hypothesis property based testing library.
+
+This can be useful for:
+- Giving counterexamples to poorly stated theorems before you spend much effort on them
+- Sanity checking axioms
+- Connecting formal models to other code
+- Testing Knuckledragger facilities
+- Testing Z3 intended meaning
+"""
+
 import kdrag as kd
 import kdrag.smt as smt
 import hypothesis

diff --git a/kdrag/reflect.py b/kdrag/reflect.py
@@ -1,3 +1,7 @@
+"""
+Reflecting and reifying SMT expressions from/into Python values.
+"""
+
 import kdrag.smt as smt
 import kdrag as kd
 import typing

diff --git a/kdrag/theories/logic/hol_light.py b/kdrag/theories/logic/hol_light.py
diff --git a/kdrag/theories/logic/ideas.md b/kdrag/theories/logic/ideas.md
@@ -0,0 +1,8 @@
+- Kuratowski topology <https://en.wikipedia.org/wiki/Kuratowski_closure_axioms>
+- Peano arithmetic in the axiomatic style
+- sequent calculus
+- robinson arithmetic
+- hol light
+- modal logic
+- Intuitionistic logic - Deep or shallow
+- GAT
diff --git a/kdrag/theories/logic/kuratowski.py b/kdrag/theories/logic/kuratowski.py
diff --git a/kdrag/theories/logic/modal.py b/kdrag/theories/logic/modal.py
diff --git a/kdrag/theories/logic/sequent.py b/kdrag/theories/logic/sequent.py
diff --git a/kdrag/utils.py b/kdrag/utils.py
@@ -335,6 +335,9 @@ def subterms(t: smt.ExprRef, into_binder=False):
 
 
 def is_subterm(t: smt.ExprRef, t2: smt.ExprRef) -> bool:
+    """
+    TODO: Not alpha invariant or going into binders
+    """
     if t.eq(t2):
         return True
     elif smt.is_app(t2):
@@ -345,7 +348,7 @@ def is_subterm(t: smt.ExprRef, t2: smt.ExprRef) -> bool:
 
 def sorts(t: smt.ExprRef):
     """Generate all sorts in a term"""
-    for t in subterms(t):
+    for t in subterms(t, into_binder=True):
         yield t.sort()
 
 

diff --git a/tests/test_logic.py b/tests/test_logic.py
@@ -4,7 +4,6 @@
 import kdrag.theories.logic.zf as zf
 import kdrag.theories.logic.robinson as robinson
 import kdrag.theories.logic.peano as peano
-import kdrag.theories.logic.hol_light as hol_light
 
 
 def test_logic():