fix docs, more tests

docs/src/concepts/theories.md

@@ -2,33 +2,8 @@
 
 A theory in GATlab consists of two parts.
 
-1. A Julia value of type `Theory` that describes the theory.
+1. A Julia value of type `GAT` that describes the theory.
 2. A module named by the theory with various Julia types that give us handles
 for metaprogramming.
 
-These metaprogramming types include:
 
-- A singleton struct named `Th` and subtyping `AbstractTheory` that has an
-   overload of `gettheory` on it returning the Julia value from 1. This is used
-   to pass around the entire theory at the type level.
-- A singleton struct for each type constructor and term constructor in the
-   theory. These are used in place of `Lvl` in types, so that backtraces are
-   more readable.
-
-Example:
-
-```julia
-module Category
-using GATlab.Theories
-
-struct Th <: AbstractTheory end
-
-Theories.gettheory(::Th) = ...
-
-struct Ob <: TypCon{1} end
-struct Hom <: TypCon{2} end
-
-struct compose <: TrmCon{3} end
-...
-end
-```

docs/src/stdlib.md

@@ -5,7 +5,7 @@
 Our friend `ThCategory` is the main theory in this module.
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThCategory
+GATlab.Stdlib.StdTheories.ThCategory
 ```
 
 You can specialize a theory by adding more axioms. In this case we can specialize the theory of categories to that of thin category by adding the axiom that two morphisms are equal if they have the same domain and codomain.
@@ -15,33 +15,30 @@ thineq := f == g :: Hom(A,B) ⊣ [A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B)]
 ```
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThThinCategory
+GATlab.Stdlib.StdTheories.ThThinCategory
 ```
 ### Category Building Blocks
 The remaining theories in this module are not necessarily useful, but go to show demonstrate the theory hierarchy can be built up in small increments.
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThClass
+GATlab.Stdlib.StdTheories.ThClass
 ```
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThLawlessCat
+GATlab.Stdlib.StdTheories.ThLawlessCat
 ```
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThAscCat
+GATlab.Stdlib.StdTheories.ThAscCat
 ```
 
 ```@docs
-GATlab.Stdlib.StdTheories.Categories.ThIdLawlessCat
+GATlab.Stdlib.StdTheories.ThIdLawlessCat
 ```
 
 ```@autodocs
 Modules = [GATlab.Stdlib,
   GATlab.Stdlib.StdTheories,
-  GATlab.Stdlib.StdTheories.Algebra,
-  GATlab.Stdlib.StdTheories.Monoidal,
-  GATlab.Stdlib.StdTheories.Naturals,
   GATlab.Stdlib.StdModels,
   GATlab.Stdlib.StdModels.FinSets,
   ]

src/models/Presentations.jl

@@ -10,7 +10,7 @@ in applications like knowledge representation.
 module Presentations
 export @present, Presentation, generator, generators, generator_index,
   has_generator, equations, add_generator!, add_generators!, add_definition!,
-  add_equation!, add_equations!, change_theory
+  add_equation!, add_equations!
 
 using Base.Meta: ParseError
 using MLStyle: @match
@@ -49,21 +49,7 @@ function Base.:(==)(pres1::Presentation, pres2::Presentation)
   pres1.syntax == pres2.syntax && pres1.generators == pres2.generators &&
     pres1.equations == pres2.equations
 end
-"""
-Move a presentation to a new syntax,
-duplicating all the data on shared names. In particular,
-this is lossless if all the generators of the original
-presentation are at names in the new syntax.
-"""
-function change_theory(syntax::Module,pres::Presentation{S,Name}) where {S,Name}
-  T = syntax.theory()
-  pres_new = Presentation(syntax)
-  types = intersect(keys(pres_new.generators),keys(pres.generators))
-  for t in types map(pres.generators[t]) do x
-    add_generator!(pres_new,generator_switch_syntax(syntax,x)) end end
-  #XX: test on equations
-  pres_new
-end
+
 function Base.copy(pres::Presentation{T,Name}) where {T,Name}
   Presentation{T,Name}(pres.syntax, map(copy, pres.generators),
                        copy(pres.generator_name_index), copy(pres.equations))

src/syntax/Scopes.jl

@@ -352,8 +352,6 @@ struct Scope{T} <: HasScope{T}
   end
 end
 
-Scope(s::Scope) = s
-
 Base.:(==)(s1::Scope, s2::Scope) = s1.tag == s2.tag
 
 Base.hash(s::Scope, h::UInt64) = hash(s.tag, h)
@@ -701,24 +699,6 @@ function ScopeList{T}(scopes::Vector{<:HasScope{T}}) where {T}
   c
 end
 
-function Scope(hsl::ScopeList{T}) where T
-  if nscopes(hsl) == 0
-    Scope{T}() 
-  else 
-    res = Scope{T}()
-    newtag = gettag(res)
-    retagdict = Dict{ScopeTag, ScopeTag}()
-    for nextscope in getscope.(hsl.scopes)
-      retagdict[gettag(nextscope)] = newtag
-      nextscope = retag(retagdict, nextscope)
-      for b in getbindings(nextscope)
-        unsafe_pushbinding!(res, b)
-      end
-    end
-    res
-  end
-end
-
 function Base.copy(c::ScopeList{T}) where {T}
   ScopeList{T}(copy(c.scopes), copy(c.taglookup), copy(c.namelookup))
 end

test/syntax/GATs.jl

@@ -65,6 +65,9 @@ c = GATContext(thcat, sortscope)
 HomT = fromexpr(c, :(Hom(A, A)), AlgType)
 HomS = AlgSort(HomT)
 
+@test rename(gettag(sortscope), Dict(:A=>:Z), HomT) isa AlgType
+@test retag(Dict(gettag(sortscope)=>newscopetag()), HomT) isa AlgType
+
 @test sortcheck(c, AlgTerm(A)) == ObS
 
 # # Good term and bad term
@@ -98,6 +101,10 @@ TG = ThGraph.Meta.theory
 @test TG ⊆ T
 @test T ⊈ TG
 
+# ToExpr
+#-------
+toexpr.(Ref(T), T.segments)
+
 # InCtx
 #----------
 # tic = fromexpr(T, :(compose(f,compose(id(b),id(b))) ⊣ [a::Ob, b::Ob, f::Hom(a,b)]), TermInCtx);

test/syntax/Scopes.jl

@@ -90,6 +90,9 @@ bind_X, bind_Y = Binding{String}(:X, Alias(x)), Binding{String}(:Y, Alias(y))
 xy_scope = Scope([bind_x, bind_y, bind_X, bind_Y]; tag=tag1)
 xy_scope′ = Scope([bind_x]; tag=tag1)
 
+@test alltags(retag(Dict(tag1=>tag2),xy_scope)) == Set([tag2])
+@test identvalues(xy_scope′) == [x => "ex"]
+
 @test xy_scope == xy_scope′
 @test hash(xy_scope) == hash(xy_scope′)
 @test basicprinted(xy_scope) == "{$(basicprinted(bind_x)), $(basicprinted(bind_y)), X = x, Y = y}"