From 8e105908ff1eb15b7aa10e7e6d6557eee38d8686 Mon Sep 17 00:00:00 2001
From: Matt <cuffaro.matt@gmail.com>
Date: Mon, 10 Jun 2024 12:18:06 -0400
Subject: [PATCH] identified an issue with multiple-inheritance

---
 src/stdlib/models/twosorted.jl |  2 --
 src/stdlib/theories/algebra.jl | 49 ++++------------------------------
 src/stdlib/theories/dec.jl     |  7 +++++
 src/syntax/TheoryInterface.jl  | 11 ++------
 4 files changed, 14 insertions(+), 55 deletions(-)

diff --git a/src/stdlib/models/twosorted.jl b/src/stdlib/models/twosorted.jl
index d0683eb2..28452c5d 100644
--- a/src/stdlib/models/twosorted.jl
+++ b/src/stdlib/models/twosorted.jl
@@ -72,5 +72,3 @@ end
 @withmodel RMatricesTwo() (e, i, ⊕, zero, unit, *, +, -, ⋅) begin
     i(2⋅rand(2,2) ⊕ rand(2,2))
 end
-# @time -1*(2*rand(2,2) + rand(2,2))
-
diff --git a/src/stdlib/theories/algebra.jl b/src/stdlib/theories/algebra.jl
index e2644ef2..6084517e 100644
--- a/src/stdlib/theories/algebra.jl
+++ b/src/stdlib/theories/algebra.jl
@@ -1,4 +1,4 @@
-export ThEmpty, ThSet, ThMagma, ThSemiGroup, ThMonoid, ThGroup, ThCMonoid, ThAb, ThSemiRing, ThRing, ThCRing, ThDiffRing, ThBooleanRing, ThDivisionRing, ThField, ThCRig, ThElementary, ThPreorder, ThLeftModule, ThRightModule, ThBiModule, ThModule, ThCommRModule
+export ThEmpty, ThSet, ThMagma, ThSemiGroup, ThMonoid, ThGroup, ThCMonoid, ThAb, ThSemiRing, ThRing, ThCommRing, ThDiffRing, ThBooleanRing, ThDivisionRing, ThCRig, ThElementary, ThPreorder, ThLeftModule, ThRightModule, ThModule, ThCommRModule
 
 import Base: +, *, zero, one
 
@@ -122,7 +122,7 @@ Examples:
   - 
 
 """
-@theory ThCRing begin
+@theory ThCommRing begin
   using ThRing
   x * y == y * x ⊣ [x,y]
 end
@@ -131,7 +131,7 @@ end
 A commutative ring equipped with a *derivation* operator `d` which fulfills linearity and the Leibniz product rule.
 """
 @theory ThDiffRing begin
-  using ThCRing
+  using ThCommRing
   d(x) :: default ⊣ [x::default]
   d(x + y) == d(x) + d(y) ⊣ [x::default, y::default]
   d(x*y) == d(x)*y + x*d(y) ⊣ [x::default, y::default]
@@ -144,7 +144,7 @@ Examples:
 
 """
 @theory ThBooleanRing begin
-  using ThCRing
+  using ThCommRing
   x * x == x ⊣ [x]
 end
 
@@ -160,41 +160,13 @@ end
   x * i(x) == one() ⊣ [x]
 end
 
-# TODO: how to handle cases where RHS of axiom must be a different sort (e.g., nonzero) than those on the LHS (e.g., default)? Can we define a sort which inherits axioms defined on another sort (default)?
-""" The theory of a commutative ring where multiplication by nonzero elements is nonzero 
-
- - 
-
-"""
-# @theory ThIntegralDomain begin
-#   using ThCRing
-#   nonzero::TYPE
-#   # using ThCRing: default as nonzero
-#   x * y == z ⊣ [x::nonzero, y::nonzero, z::nonzero]
-# end
-
-# using two theories which overlap considerably, we can still add unique elem
-# best to export default as K or something
-""" The theory of a commutative division ring
-
- - The rational numbers ℚ and algebraic extensions, i.e. ℚ[√2]
- - The real numbers ℝ and its algebraic completion, the complex numbers ℂ
- - 
-
-"""
-@theory ThField begin
-  using ThDivisionRing
-  using ThCRing
-end
-# TODO user needs to define inv as 0 when 0
-
 @theory ThCRig begin
   using ThRig
   a * b == b * a ⊣ [a,b]
 end
 
 @theory ThElementary begin
-  using ThCRing
+  using ThCommRing
   sin(x) ⊣ [x]
   cos(x) ⊣ [x]
   tan(x) ⊣ [x]
@@ -285,17 +257,6 @@ end
 #     1.b: it does not exist in the old theory
 #   2. ThBiModule contributes both Left and Right Modules. Since the scalars are being renamed (to the same name), they are checked if they have new 
 
-# TODO we do not change the idents, so M and Scalar show
-# @theory __ThModule begin
-#   using ThLeftModule
-#   using ThRightModule
-# end
-
-@theory ThVectorSpace begin
-  using ThModule
-  using ThField: default as Scalar, i as inv
-end
-
 # TODO Fix axioms
 @theory ThCommRModule begin
   using ThModule
diff --git a/src/stdlib/theories/dec.jl b/src/stdlib/theories/dec.jl
index 56a19330..a1abbb6c 100644
--- a/src/stdlib/theories/dec.jl
+++ b/src/stdlib/theories/dec.jl
@@ -14,6 +14,13 @@ end
   ap(α ⋅ x) == α ⋅ ap(x) ⊣ [x::DomVector]
 end
 
+# TODO current implementation of multiple-inheritance does not overload the axioms in Form1 and Form2 Modules, so they are treated as the same and therefore eliminated.
+#
+# @theory _CoChains begin
+#   using Module: M as Form0
+#   using Module: M as Form1
+#   using Module: M as Form2
+# end
 @theory CoChains begin
   using Module: Vector as Form0
   using Module: Vector as Form1
diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl
index eea0aee5..d3669d1e 100644
--- a/src/syntax/TheoryInterface.jl
+++ b/src/syntax/TheoryInterface.jl
@@ -82,12 +82,7 @@ function rename_impl(newname, body, __module__)
   #
   lines = Any[]
   newnames = Symbol[]
-
-  ## XXX "for binding in segment" was "... in newsegment", and I wrapped this
-  ## in a for-loop for segments. This was done to debug an issue with ModelInterface
-  ## where the `default` function was not being declared.
-  ##
-  ## owen: this should be in newsegment as before
+ 
   for segment in newtheory.segments.scopes
     for binding in segment
       judgment = getvalue(binding)
@@ -258,9 +253,7 @@ function theory_impl(head, body, __module__)
 
   theory = fromexpr(parent, body, GAT; name, current_module=fqmn(__module__))
 
-
-  newsegment = theory.segments.scopes[end]
-  # @info "NEWSEGMENT" newsegment
+  # newsegment = theory.segments.scopes[end]
   docstr = repr(theory)
 
   lines = Any[]