Multiple inheritance of GATs (#147)

* unions working, still need renaming

* trying to get renaming via using-as statments right

* work so far. issue encountered with default not defined in modelinterface.

* Multiple inheritance seems to work but not tested on withmodel.

* functions are now being generated from type constructors during theory definition, but a test in models is now broken

* ThModule now defined. Category.Ob problem in test persists. Code somewhat cleaned up after my debugging.

* just about there. tests were passing and some examples/new tests are being created but it needs clean up and review.

* working through module code and tests

* these changes repair reidentification on empty alg sort arrays

* fixed bug where second using-rename statements collide with names in the theory

* identified an issue with multiple-inheritance

* readded newsegment in theory_impl

* removed renaming, added manual renames to algebra.jl

* fixed imports

* import - from base

* addressed review comments

* workk done so far on resolving code coverage

* improve coverage

---------

Co-authored-by: Matt <[email protected]>

docs/src/concepts/scopes.md

@@ -21,7 +21,7 @@ an identifier.
 [chit](https://github.com/davidad/chit))
 
 In general, naming is given by a *relation* between symbols and *bindings* (as
-refered to by local identifiers).  Each binding may be associated with zero or
+referred to by local identifiers).  Each binding may be associated with zero or
 more symbols, and each symbol might be associated with zero or more bindings.
 
 We name the failure of this relation to be a bijection in several ways.
@@ -65,7 +65,7 @@ scopes, and the most recent scope "wins".
 Parsing turns a `Symbol` into an `Ident`. The `Ident` contains the original
 `Symbol` for printing, but it also contains a reference to a scope via ScopeTag,
 and an local identifier ("lid") within that scope. Thus, the name in the `Ident`
-is never needed for later stages of programatic manipulation.
+is never needed for later stages of programmatic manipulation.
 
 Scopes cache the relation between names and bindings, by providing a way to go
 from binding (as reified by local identifier) to a set of aliases with

src/models/ModelInterface.jl

@@ -597,23 +597,27 @@ end
 macro withmodel(model, subsexpr, body)
   modelvar = gensym("model")
 
+  # e.g., (ℕ, Z, S) => [ℕ, Z, S]
   subs = @match subsexpr begin
     Expr(:tuple, subs...) => [subs...]
     sub::Symbol => [sub]
   end
 
+  # gensym these subs
   subvars = gensym.(subs) # e.g. #25compose to avoid global method overloading
 
+  # set gensym(ℕ) = ℕ, etc.
   subvardefs = [
     Expr(:(=), var, sub)
     for (sub, var) in zip(subs, subvars)
   ]
 
+  # set ℕ = (args...; kwargs...) -> gensym(ℕ)(MyModel, args...; kwargs...) 
   subdefs = [
     Expr(:(=), sub, :((args...;kwargs...) -> $var($modelvar, args...;kwargs...)))
     for (sub, var) in zip(subs, subvars)
-  ]
- 
+  ] 
+
   esc(
     Expr(:let,
       Expr(:block, :($modelvar = $(Expr(:call, TheoryInterface.WithModel, model))), subvardefs...),

src/stdlib/models/arithmetic.jl

@@ -1,8 +1,15 @@
-export IntNatPlus, IntPreorder
+export IntNat, IntNatPlus, IntPreorder, ZRing, BoolRing
 
 using ...Models
 using ..StdTheories
 
+struct IntNat <: Model{Tuple{Int}} end
+
+@instance ThNat{Int} [model::IntNat] begin
+  Z() = 0
+  S(n::Int) = n + 1
+end
+
 struct IntNatPlus <: Model{Tuple{Int}} end
 
 @instance ThNatPlus{Int} [model::IntNatPlus] begin
@@ -22,3 +29,13 @@ struct IntPreorder <: Model{Tuple{Int, Tuple{Int,Int}}} end
     error("Cannot compose $ab and $bc")
   end
 end
+
+struct ZRing <: Model{Tuple{Int}} end
+
+@instance ThRing{Int} [model::ZRing] begin
+  zero() = 0
+  one() = 1
+  -(x::Int) = -1 * x
+  +(x::Int, y::Int) = x + y
+  *(x::Int, y::Int) = x * y
+end