From 860f8843b39c181a3968287b1ad0cee72261e16d Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Fri, 29 Mar 2024 21:22:41 -0700
Subject: [PATCH 1/5] Forester autogeneration

pth="/Users/kristopherbrown/code/kbforest/trees/gat"; to_forest(pth; clear=true)
---
 src/GATlab.jl                 |   2 +
 src/forest/module.jl          | 197 ++++++++++++++++++++++++++++++++++
 src/models/ModelInterface.jl  |   9 ++
 src/syntax/TheoryInterface.jl |   9 +-
 src/syntax/TheoryMaps.jl      |  11 +-
 src/syntax/gats/judgments.jl  |   1 +
 6 files changed, 226 insertions(+), 3 deletions(-)
 create mode 100644 src/forest/module.jl

diff --git a/src/GATlab.jl b/src/GATlab.jl
index bc3b0dc5..bbb412ed 100644
--- a/src/GATlab.jl
+++ b/src/GATlab.jl
@@ -8,10 +8,12 @@ include("syntax/module.jl")
 include("models/module.jl")
 include("stdlib/module.jl")
 include("nonstdlib/module.jl") # don't reexport this
+include("forest/module.jl") # don't reexport this
 
 @reexport using .Util
 @reexport using .Syntax
 @reexport using .Models
 @reexport using .Stdlib
+@reexport using .Forest
 
 end # module GATlab
diff --git a/src/forest/module.jl b/src/forest/module.jl
new file mode 100644
index 00000000..d0611043
--- /dev/null
+++ b/src/forest/module.jl
@@ -0,0 +1,197 @@
+module Forest
+export to_forest
+using ...Syntax
+using ...Syntax.GATs: TrmTypConstructor, AlgAST, MethodApp
+using ...Stdlib: ThSet
+import ...Models: show_latex, ModelInterface
+using ...Util.MetaUtils: generate_function
+
+const nn = "\n\n"
+latex(x::String) = "#{$x}"
+p(x::String) = "\\p{$x}"
+code(x::Union{SubString,String}) = "\\code{$x}"
+function writefile(pth, str)
+  io = open(pth, "w"); write(io, str); close(io)
+end
+alphanum(i) = reverse(string(i, base=35))[1:5]
+
+function show_latex(T::GAT, expr::TypeScope)
+  body = join(map(getbindings(expr)) do b 
+    v = getvalue(b)
+    noshow = methodof(bodyof(v)) == methodof(only(ThSet.Meta.theory.sorts))
+    string(nameof(b)) * (noshow ? "" : "::$(show_latex(T, v))")
+  end,",\\ ")
+  "\\dashv [$body]"
+end
+
+show_latex(T::GAT, expr::InCtx) = 
+  latex(show_latex(T, getvalue(expr)) * show_latex(T, getcontext(expr)))
+
+
+function show_latex(T::GAT, expr::A) where {A<:AlgAST} 
+  show_latex(T, bodyof(expr))
+end
+show_latex(T::GAT, x::Ident) = nameof(x)
+
+
+function show_latex(T::GAT, expr::MethodApp)
+  binary, head = false, headof(expr)
+  if length(argsof(expr)) <= 2
+    for x in getidents(T; aliases=true)
+      v = getvalue(T[x])
+      if v isa Alias && Base.isoperator(nameof(x)) && v.ref == head 
+        binary, head = true, x
+      end
+    end
+  end
+  if !binary 
+    join(["\\mathop{\\mathrm{$(nameof(head))}}",
+  (isempty(argsof(expr)) ? [] : ["\\left(",
+  join([show_latex(T,arg) for arg in argsof(expr)], ","),
+  "\\right)"])...])
+  else 
+    join(["\\left(", show_latex(T,first(argsof(expr))), 
+    "\\mathop{\\mathrm{$(nameof(head))}}",
+    show_latex(T,last(argsof(expr))), "\\right)"])
+  end
+end
+
+function to_forest_model(mod::Module, model::Any)
+  stmts = map(mod.Meta.models[model]) do jf 
+    str = string(Base.remove_linenums!(generate_function(jf)))
+    code(replace(str, r"#=.+=#" => ""))
+  end
+  "\\title{$(nameof(model))}\\taxon{definition} $(join(p.(stmts),nn))"
+end
+
+
+function to_forest(T::GAT, method::Ident, x::TrmTypConstructor)
+  is_trm = hasfield(typeof(x), :type)
+  ty = is_trm ? ("::"*show_latex(T, x.type)) : ""
+  ctx = getcontext(x)
+  canonterm = (is_trm ? AlgTerm : AlgType)(x.declaration, method, AlgTerm.(idents(ctx; lid=x.args)))
+  "\\title{$(nameof(x.declaration))}\n" *latex(show_latex(T, canonterm) * ty * show_latex(T, ctx))
+end
+
+to_forest(T::GAT, n::Ident, ::AlgDeclaration) = "\\title{$(nameof(n))}"
+
+function to_forest(T::GAT, n::Ident, x::Alias)
+  "\\title{$(nameof(n))}\n \\p{Alias for \\ref{$(finame(x.ref))}}"
+end
+
+function to_forest(T::GAT, ::Ident, x::AlgAccessor)
+  "\\title{$(nameof(x.declaration))}"
+end 
+
+function to_forest(T::GAT, n::Ident, x::AlgAxiom)
+  name = isnothing(nameof(n)) ? "" : "$(nameof(n)): "
+  "\\title{$name}\n" * latex(join(show_latex.(Ref(T), x.equands), " = ")*show_latex(T, getcontext(x)))
+end
+
+
+"""Create a UUID for each judgment's Ident"""
+finame(x::Ident) =  "$(alphanum(gettag(x).val.value+getlid(x).val))"
+
+"""
+Convert a Module (for a theory) into a tree, a definition tree, and a tree 
+for each judgment.
+"""
+function to_forest(mod::Module, path::String)
+  T = mod.Meta.theory
+
+  hsh = alphanum(Syntax.TheoryInterface.REVERSE_GAT_MODULE_LOOKUP[mod].val.value)
+  println("$mod $hsh")
+  for xs in T.segments.scopes
+    for (x, v) in identvalues(xs)
+      fi = joinpath(path, "$(finame(x)).tree")
+      writefile(fi, to_forest(T, x, v))
+    end
+  end
+
+  typs = join(map(last.(typecons(T))) do tc
+    "\\transclude{$(finame(tc))}"
+  end, nn)
+  trms = join(map(last.(termcons(T))) do tc
+    "\\transclude{$(finame(tc))}"
+  end, nn)
+
+  axs = join(map(T.axioms) do x
+    "\\transclude{$(finame(x))}"
+  end, nn)
+
+  doms = join(map(Syntax.TheoryMaps.THEORY_DOM_LOOKUP[mod]) do m 
+    "\\transclude{$(alphanum(hash(m)))}"
+  end)
+  codoms = join(map(Syntax.TheoryMaps.THEORY_CODOM_LOOKUP[mod]) do m 
+    "\\transclude{$(alphanum(hash(m)))}"
+  end)
+
+  mods = join(map(enumerate(ModelInterface.GAT_MODEL_LOOKUP[mod])) do (i,m)
+    mhsh = alphanum(hash(mod) + i)
+    fi = joinpath(path, "$(mhsh).tree")
+    writefile(fi, to_forest_model(mod, m))
+    "\\transclude{$(mhsh)}"
+  end, nn)
+  def = """  
+\\title{$(nameof(T))}
+\\taxon{definition}\n\n
+\\subtree{\\title{Type Constructors} \n$typs}\n
+\\subtree{\\title{Term Constructors} \n$trms}\n
+\\subtree{\\title{Axioms} \n$axs}\n
+"""
+  writefile(joinpath(path, "$(hsh)_def.tree"), def)
+  page = """  
+\\title{$(nameof(T))}\n\n
+\\transclude{$(hsh)_def}\n
+\\subtree{\\title{Models}\n \\put\\transclude/expanded{false} $mods}\n
+\\subtree{\\title{TheoryMaps} \n
+\\subtree{\\title{As domain} \\put\\transclude/expanded{false} $doms}\n
+\\subtree{\\title{As codomain} \\put\\transclude/expanded{false} $codoms}}\n
+"""
+  writefile(joinpath(path, "$hsh.tree"), page)
+
+end
+
+"""
+Convert a theory map into a tree for the definition nested inside 
+a general tree for the theory map.
+"""
+function to_forest_map(mod::Module, path::String)
+  M = mod.MAP
+  hsh = alphanum(hash(mod))
+  typs, trms = map([typemap,termmap]) do fmap 
+    join(map(collect(pairs(fmap(M)))) do (k, tic)
+      tc = getvalue(M.dom[k])
+      decl = tc.declaration
+      blck = join(p.(["[$(nameof(decl))]($(finame(decl))):", 
+                   latex(show_latex(M.dom, TermInCtx(M.dom, k))), 
+                   latex(show_latex(M.codom, tic))]))
+      "\\scope{$blck}"
+    end, nn)
+  end
+
+  # transcluding leads to infinite forester compilation loop
+  scope = p("[$(nameof(M.dom))]($(Syntax.TheoryInterface.REVERSE_GAT_MODULE_LOOKUP[mod.dom].val.value|> alphanum)) #{\\rightarrow} [$(nameof(M.codom))]($(Syntax.TheoryInterface.REVERSE_GAT_MODULE_LOOKUP[mod.codom].val.value |> alphanum))")
+
+  def = """  
+\\title{$(nameof(mod))}
+\\taxon{definition}\n\n$scope
+\\subtree{\\title{Type Mapping} \n$typs}\n
+\\subtree{\\title{Term Mapping} \n$trms}\n
+"""
+  writefile(joinpath(path, "$(hsh).tree"), def)
+end 
+
+"""
+Create a forest in a directory based on all user-declared theories, theorymaps, 
+and models
+"""
+function to_forest(path::String; clear=false)
+  clear && rm.(joinpath.(path, readdir(path)))
+  for T in values(Syntax.TheoryInterface.GAT_MODULE_LOOKUP)
+    occursin("NonStdlib", string(T)) || to_forest(T, path)
+  end
+  to_forest_map.(values(Syntax.TheoryMaps.THEORY_MAPS)  , path);
+end
+
+end # module
diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index deb0d9ad..f8e8b7ab 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -159,6 +159,8 @@ macro instance(head, model, body)
   generate_instance(theory, theory_module, jltype_by_sort, model_type, whereparams, body)
 end
 
+const GAT_MODEL_LOOKUP = DefaultDict{Module,Vector{Any}}(()->[])
+
 function generate_instance(
   theory::GAT,
   theory_module::Union{Expr0, Module},
@@ -213,8 +215,11 @@ function generate_instance(
   docsink = gensym(:docsink)
 
   code = Expr(:block,
+    [add_source_code(theory_module, model_type, whereparams, f) for f in functions]...,
     [generate_function(f) for f in qualified_functions]...,
     implements_declarations...,
+    :(push!($(GlobalRef(ModelInterface, :GAT_MODEL_LOOKUP))[$theory_module], 
+            $model_type where {$(whereparams...)})),
     :(function $docsink end),
     :(Core.@__doc__ $docsink)
   )
@@ -222,6 +227,10 @@ function generate_instance(
   escape ? esc(code) : code
 end
 
+function add_source_code(theory_module, mod, whereparams, f)
+  :(push!($(theory_module).Meta.models[$mod where {$(whereparams...)}], $f))
+end
+
 macro instance(head, body)
   esc(:(@instance $head $(nothing) $body))
 end
diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl
index 22e5d472..8e020716 100644
--- a/src/syntax/TheoryInterface.jl
+++ b/src/syntax/TheoryInterface.jl
@@ -5,6 +5,7 @@ using ..Scopes, ..GATs, ..ExprInterop, GATlab.Util
 # using GATlab.Util
 
 using MLStyle, StructEquality, Markdown
+using DataStructures: DefaultDict
 
 abstract type Model{Tup <: Tuple} end
 
@@ -40,6 +41,10 @@ dictionary pointing to the module corresponding to the new theory.
 """
 const GAT_MODULE_LOOKUP = Dict{ScopeTag, Module}()
 
+const REVERSE_GAT_MODULE_LOOKUP = Dict{Module,ScopeTag}()
+
+
+
 macro signature(head, body)
   theory_impl(head, body, __module__)
 end
@@ -115,16 +120,18 @@ function theory_impl(head, body, __module__)
   doctarget = gensym()
 
   push!(modulelines, Expr(:toplevel, :(module Meta
+    using DataStructures: DefaultDict
     struct T end
    
     @doc ($(Markdown.MD)((@doc $(__module__).$doctarget), $docstr))
     const theory = $theory
-
+    const models = DefaultDict(()->[])
     macro theory() $theory end
     macro theory_module() parentmodule(@__MODULE__) end
   end)))
 
   push!(modulelines, :($(GlobalRef(TheoryInterface, :GAT_MODULE_LOOKUP))[$(gettag(newsegment))] = $name))
+  push!(modulelines, :($(GlobalRef(TheoryInterface, :REVERSE_GAT_MODULE_LOOKUP))[$name] = $(gettag(newsegment))))
 
 
   esc(
diff --git a/src/syntax/TheoryMaps.jl b/src/syntax/TheoryMaps.jl
index fae0f915..547bba83 100644
--- a/src/syntax/TheoryMaps.jl
+++ b/src/syntax/TheoryMaps.jl
@@ -9,7 +9,7 @@ using ..TheoryInterface
 import ..ExprInterop: toexpr, fromexpr
 
 using StructEquality, MLStyle
-using DataStructures: OrderedDict
+using DataStructures: OrderedDict, DefaultDict
 
 # Theory Maps
 #############
@@ -389,6 +389,9 @@ end
 reorder(b::Binding{T}, tag::ScopeTag, perm::Dict{Int,Int}) where {T} = 
   setvalue(b, reorder(getvalue(b), tag, perm))
 
+const THEORY_DOM_LOOKUP = DefaultDict{Module, Vector{Module}}(()->Module[])
+const THEORY_CODOM_LOOKUP = DefaultDict{Module, Vector{Module}}(()->Module[])
+const THEORY_MAPS = Module[]
 
 macro theorymap(head, body)
   (name, domname, codomname) = @match head begin
@@ -413,11 +416,15 @@ macro theorymap(head, body)
           macro map() $tmap end
           macro dom() $dommod end
           macro codom() $codommod end
-
+          const dom = $dommod
+          const codom = $dommod
           $mig
         end
       ),
       :(Core.@__doc__ $(name)),
+      :(push!($(GlobalRef(TheoryMaps, :THEORY_MAPS)), $name)),
+      :(push!($(GlobalRef(TheoryMaps, :THEORY_DOM_LOOKUP))[$dommod], $name)),
+      :(push!($(GlobalRef(TheoryMaps, :THEORY_CODOM_LOOKUP))[$codommod], $name))
     )
   )
 end
diff --git a/src/syntax/gats/judgments.jl b/src/syntax/gats/judgments.jl
index 096de5eb..610fa2b3 100644
--- a/src/syntax/gats/judgments.jl
+++ b/src/syntax/gats/judgments.jl
@@ -120,6 +120,7 @@ A declaration of an axiom
   equands::Vector{AlgTerm}
 end
 
+Scopes.getcontext(ax::AlgAxiom) = ax.localcontext
 
 """
 `AlgSorts`

From 9b7a680f75d8aa409c2de5cf118ff66f298b2151 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Tue, 2 Apr 2024 19:41:25 -0700
Subject: [PATCH 2/5] fix return value of @theorymap

---
 src/syntax/TheoryInterface.jl | 1 -
 src/syntax/TheoryMaps.jl      | 3 ++-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl
index 8e020716..f12d7ea4 100644
--- a/src/syntax/TheoryInterface.jl
+++ b/src/syntax/TheoryInterface.jl
@@ -5,7 +5,6 @@ using ..Scopes, ..GATs, ..ExprInterop, GATlab.Util
 # using GATlab.Util
 
 using MLStyle, StructEquality, Markdown
-using DataStructures: DefaultDict
 
 abstract type Model{Tup <: Tuple} end
 
diff --git a/src/syntax/TheoryMaps.jl b/src/syntax/TheoryMaps.jl
index 547bba83..934f023e 100644
--- a/src/syntax/TheoryMaps.jl
+++ b/src/syntax/TheoryMaps.jl
@@ -424,7 +424,8 @@ macro theorymap(head, body)
       :(Core.@__doc__ $(name)),
       :(push!($(GlobalRef(TheoryMaps, :THEORY_MAPS)), $name)),
       :(push!($(GlobalRef(TheoryMaps, :THEORY_DOM_LOOKUP))[$dommod], $name)),
-      :(push!($(GlobalRef(TheoryMaps, :THEORY_CODOM_LOOKUP))[$codommod], $name))
+      :(push!($(GlobalRef(TheoryMaps, :THEORY_CODOM_LOOKUP))[$codommod], $name)),
+      name
     )
   )
 end

From de27e3067a1b7691a10c41937458e28803e9d2be Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Wed, 3 Apr 2024 19:52:30 -0700
Subject: [PATCH 3/5] Add docstrings and a landing page

---
 docs/Project.toml      |  1 +
 src/forest/gatlab.tree | 20 ++++++++++++++++++++
 src/forest/module.jl   | 38 ++++++++++++++++++++++++++++----------
 test/forest/tests.jl   |  9 +++++++++
 test/runtests.jl       |  4 ++++
 5 files changed, 62 insertions(+), 10 deletions(-)
 create mode 100644 src/forest/gatlab.tree
 create mode 100644 test/forest/tests.jl

diff --git a/docs/Project.toml b/docs/Project.toml
index ce0cd327..10801c96 100644
--- a/docs/Project.toml
+++ b/docs/Project.toml
@@ -1,4 +1,5 @@
 [deps]
+DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8"
 Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
 GATlab = "f0ffcf3b-d13a-433e-917c-cc44ccf5ead2"
 Literate = "98b081ad-f1c9-55d3-8b20-4c87d4299306"
diff --git a/src/forest/gatlab.tree b/src/forest/gatlab.tree
new file mode 100644
index 00000000..03301faf
--- /dev/null
+++ b/src/forest/gatlab.tree
@@ -0,0 +1,20 @@
+\title{GATlab catalog of GATs}
+
+\p{This is an autogenerated browser for theories defined using [GATlab](https://github.com/AlgebraicJulia/GATlab.jl).}
+
+\p{This site was generated using [Forester](https://www.jonmsterling.com/jms-005P.xml).}
+
+\scope{
+\put\transclude/title{Theories}
+\query{\query/tag{theory}}
+}
+
+\scope{
+\put\transclude/title{Models}
+\query{\query/tag{model}}
+}
+
+\scope{
+\put\transclude/title{Theory morphisms}
+\query{\query/tag{theorymap}}
+}
diff --git a/src/forest/module.jl b/src/forest/module.jl
index d0611043..5f204fec 100644
--- a/src/forest/module.jl
+++ b/src/forest/module.jl
@@ -5,6 +5,7 @@ using ...Syntax.GATs: TrmTypConstructor, AlgAST, MethodApp
 using ...Stdlib: ThSet
 import ...Models: show_latex, ModelInterface
 using ...Util.MetaUtils: generate_function
+import Markdown
 
 const nn = "\n\n"
 latex(x::String) = "#{$x}"
@@ -61,7 +62,7 @@ function to_forest_model(mod::Module, model::Any)
     str = string(Base.remove_linenums!(generate_function(jf)))
     code(replace(str, r"#=.+=#" => ""))
   end
-  "\\title{$(nameof(model))}\\taxon{definition} $(join(p.(stmts),nn))"
+  "\\title{$(nameof(model))}\n\\taxon{definition}\n\\tag{model}$(join(p.(stmts),nn))"
 end
 
 
@@ -96,11 +97,11 @@ finame(x::Ident) =  "$(alphanum(gettag(x).val.value+getlid(x).val))"
 Convert a Module (for a theory) into a tree, a definition tree, and a tree 
 for each judgment.
 """
-function to_forest(mod::Module, path::String)
+function to_forest(mod::Module, path::String; verbose=true)
   T = mod.Meta.theory
 
   hsh = alphanum(Syntax.TheoryInterface.REVERSE_GAT_MODULE_LOOKUP[mod].val.value)
-  println("$mod $hsh")
+  verbose && println("$mod $hsh")
   for xs in T.segments.scopes
     for (x, v) in identvalues(xs)
       fi = joinpath(path, "$(finame(x)).tree")
@@ -126,7 +127,8 @@ function to_forest(mod::Module, path::String)
     "\\transclude{$(alphanum(hash(m)))}"
   end)
 
-  mods = join(map(enumerate(ModelInterface.GAT_MODEL_LOOKUP[mod])) do (i,m)
+  mods′ = filter(m->nameof(m)!=:Migrator, ModelInterface.GAT_MODEL_LOOKUP[mod])
+  mods = join(map(enumerate(mods′)) do (i,m)
     mhsh = alphanum(hash(mod) + i)
     fi = joinpath(path, "$(mhsh).tree")
     writefile(fi, to_forest_model(mod, m))
@@ -140,9 +142,13 @@ function to_forest(mod::Module, path::String)
 \\subtree{\\title{Axioms} \n$axs}\n
 """
   writefile(joinpath(path, "$(hsh)_def.tree"), def)
+
+  doc = to_forest(Base.Docs.doc(mod))
+
   page = """  
-\\title{$(nameof(T))}\n\n
-\\transclude{$(hsh)_def}\n
+\\title{$(nameof(T))}\n\\tag{theory}\n\n $doc
+\\scope{  \\put\\transclude/heading{false} 
+\\transclude{$(hsh)_def}\n }
 \\subtree{\\title{Models}\n \\put\\transclude/expanded{false} $mods}\n
 \\subtree{\\title{TheoryMaps} \n
 \\subtree{\\title{As domain} \\put\\transclude/expanded{false} $doms}\n
@@ -174,7 +180,7 @@ function to_forest_map(mod::Module, path::String)
   scope = p("[$(nameof(M.dom))]($(Syntax.TheoryInterface.REVERSE_GAT_MODULE_LOOKUP[mod.dom].val.value|> alphanum)) #{\\rightarrow} [$(nameof(M.codom))]($(Syntax.TheoryInterface.REVERSE_GAT_MODULE_LOOKUP[mod.codom].val.value |> alphanum))")
 
   def = """  
-\\title{$(nameof(mod))}
+\\title{$(nameof(mod))}\n\\tag{theorymap}
 \\taxon{definition}\n\n$scope
 \\subtree{\\title{Type Mapping} \n$typs}\n
 \\subtree{\\title{Term Mapping} \n$trms}\n
@@ -186,12 +192,24 @@ end
 Create a forest in a directory based on all user-declared theories, theorymaps, 
 and models
 """
-function to_forest(path::String; clear=false)
-  clear && rm.(joinpath.(path, readdir(path)))
+function to_forest(path::String; clear=false, verbose=true)
+  ispath(path) && clear && rm.(joinpath.(path, readdir(path)))
   for T in values(Syntax.TheoryInterface.GAT_MODULE_LOOKUP)
-    occursin("NonStdlib", string(T)) || to_forest(T, path)
+    occursin("NonStdlib", string(T)) || to_forest(T, path; verbose)
   end
   to_forest_map.(values(Syntax.TheoryMaps.THEORY_MAPS)  , path);
+  cp(joinpath(@__DIR__,"gatlab.tree"), joinpath(path,"gatlab.tree"))
+  return nothing
+end
+
+"""Ad hoc translation for GATlab docstrings to look passable in Forester"""
+function to_forest(doc::Markdown.MD)::String
+  str = split(string(doc), "\n\n##")[1] # auto docs produces stuff after this point
+  res = replace(str, 
+    r"```\n((.|\n)*)\n```"=> s"\\code{\1}", # convert ``` ``` codeblocks
+    r"`(.+)`"=> s"\\code{\1}" # convert ` ` inline code
+    )
+  join(p.(string.((split(res, r"\n+"))))) # handle newlines
 end
 
 end # module
diff --git a/test/forest/tests.jl b/test/forest/tests.jl
new file mode 100644
index 00000000..aed8acae
--- /dev/null
+++ b/test/forest/tests.jl
@@ -0,0 +1,9 @@
+module TestForest 
+using Test
+using GATlab
+
+tmp = joinpath(tempdir(), "forest")
+ispath(tmp) || mkdir(tmp)
+to_forest(tmp; clear=true, verbose=false)
+
+end
\ No newline at end of file
diff --git a/test/runtests.jl b/test/runtests.jl
index da2cd870..5291a64a 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -20,3 +20,7 @@ end
   include("nonstdlib/tests.jl")
 end
 
+@testset "forest" begin
+  include("forest/tests.jl")
+end
+

From b5d7298814a11fc6a754d2d02241eeb7b670ac1b Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Wed, 3 Apr 2024 20:12:07 -0700
Subject: [PATCH 4/5] check for nothing

how did a nothing get in there?!
---
 src/forest/gatlab.tree | 2 +-
 src/forest/module.jl   | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/forest/gatlab.tree b/src/forest/gatlab.tree
index 03301faf..f38dee03 100644
--- a/src/forest/gatlab.tree
+++ b/src/forest/gatlab.tree
@@ -1,6 +1,6 @@
 \title{GATlab catalog of GATs}
 
-\p{This is an autogenerated browser for theories defined using [GATlab](https://github.com/AlgebraicJulia/GATlab.jl).}
+\p{This is an autogenerated browser for theories defined using [GATlab](https://algebraicjulia.github.io/GATlab.jl/stable/).}
 
 \p{This site was generated using [Forester](https://www.jonmsterling.com/jms-005P.xml).}
 
diff --git a/src/forest/module.jl b/src/forest/module.jl
index 5f204fec..2fee8447 100644
--- a/src/forest/module.jl
+++ b/src/forest/module.jl
@@ -127,7 +127,8 @@ function to_forest(mod::Module, path::String; verbose=true)
     "\\transclude{$(alphanum(hash(m)))}"
   end)
 
-  mods′ = filter(m->nameof(m)!=:Migrator, ModelInterface.GAT_MODEL_LOOKUP[mod])
+  mods′ = filter(m->!isnothing(m) && nameof(m)!=:Migrator, 
+                 ModelInterface.GAT_MODEL_LOOKUP[mod])
   mods = join(map(enumerate(mods′)) do (i,m)
     mhsh = alphanum(hash(mod) + i)
     fi = joinpath(path, "$(mhsh).tree")

From b3eca72d08a1dbd98df131388a43f6342a474e21 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Fri, 5 Apr 2024 13:57:16 -0700
Subject: [PATCH 5/5] use of __init__ for adding to global dict, module-level
 constraints

---
 src/forest/module.jl          | 35 ++++++++++++++++++++++++++---------
 src/syntax/TheoryInterface.jl | 13 ++++++++-----
 test/forest/tests.jl          |  2 +-
 3 files changed, 35 insertions(+), 15 deletions(-)

diff --git a/src/forest/module.jl b/src/forest/module.jl
index 2fee8447..92bddd44 100644
--- a/src/forest/module.jl
+++ b/src/forest/module.jl
@@ -2,7 +2,7 @@ module Forest
 export to_forest
 using ...Syntax
 using ...Syntax.GATs: TrmTypConstructor, AlgAST, MethodApp
-using ...Stdlib: ThSet
+using ...Stdlib: ThSet, StdTheories
 import ...Models: show_latex, ModelInterface
 using ...Util.MetaUtils: generate_function
 import Markdown
@@ -46,13 +46,13 @@ function show_latex(T::GAT, expr::MethodApp)
     end
   end
   if !binary 
-    join(["\\mathop{\\mathrm{$(nameof(head))}}",
+    join(["\\mathop{\\mathrm{ $(nameof(head)) }}",
   (isempty(argsof(expr)) ? [] : ["\\left(",
   join([show_latex(T,arg) for arg in argsof(expr)], ","),
   "\\right)"])...])
   else 
     join(["\\left(", show_latex(T,first(argsof(expr))), 
-    "\\mathop{\\mathrm{$(nameof(head))}}",
+    "\\mathop{\\mathrm{ $(nameof(head)) }}",
     show_latex(T,last(argsof(expr))), "\\right)"])
   end
 end
@@ -77,7 +77,8 @@ end
 to_forest(T::GAT, n::Ident, ::AlgDeclaration) = "\\title{$(nameof(n))}"
 
 function to_forest(T::GAT, n::Ident, x::Alias)
-  "\\title{$(nameof(n))}\n \\p{Alias for \\ref{$(finame(x.ref))}}"
+  n = nameof(n) == :\ ? "(Backslash)" : nameof(n)
+  "\\title{$n}\n \\p{Alias for \\ref{$(finame(x.ref))}}"
 end
 
 function to_forest(T::GAT, ::Ident, x::AlgAccessor)
@@ -191,12 +192,19 @@ end
 
 """
 Create a forest in a directory based on all user-declared theories, theorymaps, 
-and models
+and models. These models are defined in modules
 """
-function to_forest(path::String; clear=false, verbose=true)
+function to_forest(path::String; whitelist=nothing, blacklist=nothing, 
+                                 clear=false, verbose=true)
   ispath(path) && clear && rm.(joinpath.(path, readdir(path)))
+  isnothing(whitelist) || isnothing(blacklist) || error("Cannot set both white/blacklist")
   for T in values(Syntax.TheoryInterface.GAT_MODULE_LOOKUP)
-    occursin("NonStdlib", string(T)) || to_forest(T, path; verbose)
+    if isnothing(whitelist) || !isempty(parentmodules(T) ∩ whitelist)
+      if isnothing(blacklist) || isempty(parentmodules(T) ∩ blacklist)
+        println("T $T")
+        to_forest(T, path; verbose)
+      end
+    end
   end
   to_forest_map.(values(Syntax.TheoryMaps.THEORY_MAPS)  , path);
   cp(joinpath(@__DIR__,"gatlab.tree"), joinpath(path,"gatlab.tree"))
@@ -207,10 +215,19 @@ end
 function to_forest(doc::Markdown.MD)::String
   str = split(string(doc), "\n\n##")[1] # auto docs produces stuff after this point
   res = replace(str, 
-    r"```\n((.|\n)*)\n```"=> s"\\code{\1}", # convert ``` ``` codeblocks
-    r"`(.+)`"=> s"\\code{\1}" # convert ` ` inline code
+    r"```\n((.|\n)*?)\n```"=> s"\\code{\1}", # convert ``` ``` codeblocks
+    r"`(.+?)`"=> s"\\code{\1}", # convert ` ` inline code
+    r"\$(.+?)\$"=> s"#{\1}" # convert ` ` inline code
     )
   join(p.(string.((split(res, r"\n+"))))) # handle newlines
 end
 
+"""Get all modules in the hierarchy, for use in white/blacklist constraints"""
+function parentmodules(m::Module, res=nothing)
+  res = isnothing(res) ? Module[] : res  
+  push!(res, m)
+  p = parentmodule(m)
+  p == m ? res : parentmodules(p, res)
+end 
+
 end # module
diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl
index f12d7ea4..b095b296 100644
--- a/src/syntax/TheoryInterface.jl
+++ b/src/syntax/TheoryInterface.jl
@@ -38,6 +38,7 @@ A constant called `Meta.theory` which is the `GAT` data structure.
 When we declare a new theory, we add the scope tag of its new segment to this
 dictionary pointing to the module corresponding to the new theory.
 """
+
 const GAT_MODULE_LOOKUP = Dict{ScopeTag, Module}()
 
 const REVERSE_GAT_MODULE_LOOKUP = Dict{Module,ScopeTag}()
@@ -129,10 +130,6 @@ function theory_impl(head, body, __module__)
     macro theory_module() parentmodule(@__MODULE__) end
   end)))
 
-  push!(modulelines, :($(GlobalRef(TheoryInterface, :GAT_MODULE_LOOKUP))[$(gettag(newsegment))] = $name))
-  push!(modulelines, :($(GlobalRef(TheoryInterface, :REVERSE_GAT_MODULE_LOOKUP))[$name] = $(gettag(newsegment))))
-
-
   esc(
     Expr(
       :toplevel,
@@ -142,10 +139,16 @@ function theory_impl(head, body, __module__)
       :(
         module $name
         $(modulelines...)
+
+        function __init__()
+          $(GlobalRef(TheoryInterface, :GAT_MODULE_LOOKUP))[$(gettag(newsegment))] = $name
+          $(GlobalRef(TheoryInterface, :REVERSE_GAT_MODULE_LOOKUP))[$name] = $(gettag(newsegment))
+        end
+      
         $(structlines...)
         end
       ),
-      :(@doc ($(Markdown.MD)((@doc $doctarget), $docstr)) $name)
+      :(@doc ($(Markdown.MD)((@doc $doctarget), $docstr)) $name),
     )
   )
 end
diff --git a/test/forest/tests.jl b/test/forest/tests.jl
index aed8acae..d786fb2d 100644
--- a/test/forest/tests.jl
+++ b/test/forest/tests.jl
@@ -4,6 +4,6 @@ using GATlab
 
 tmp = joinpath(tempdir(), "forest")
 ispath(tmp) || mkdir(tmp)
-to_forest(tmp; clear=true, verbose=false)
+to_forest(tmp; whitelist=[Stdlib], clear=true, verbose=false)
 
 end
\ No newline at end of file