Gatlab -> GATlab

Project.toml

@@ -1,4 +1,4 @@
-name = "Gatlab"
+name = "GATlab"
 uuid = "f0ffcf3b-d13a-433e-917c-cc44ccf5ead2"
 authors = ["AlgebraicJulia Developers"]
 version = "0.0.1"

README.md

@@ -1,4 +1,4 @@
-# Gatlab
+# GATlab
 
 A collection of tools that one can use to reason with GATs and organize models of GATs.
 

docs/Project.toml

@@ -1,5 +1,5 @@
 [deps]
 Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
-Gatlab = "f0ffcf3b-d13a-433e-917c-cc44ccf5ead2"
+GATlab = "f0ffcf3b-d13a-433e-917c-cc44ccf5ead2"
 Literate = "98b081ad-f1c9-55d3-8b20-4c87d4299306"
 LiveServer = "16fef848-5104-11e9-1b77-fb7a48bbb589"

docs/make.jl

@@ -1,14 +1,14 @@
 using Documenter
 using Literate
 
-@info "Loading Gatlab"
-using Gatlab
+@info "Loading GATlab"
+using GATlab
 
 # Set Literate.jl config if not being compiled on recognized service.
 config = Dict{String,String}()
 if !(haskey(ENV, "GITHUB_ACTIONS") || haskey(ENV, "GITLAB_CI"))
-  config["nbviewer_root_url"] = "https://nbviewer.jupyter.org/github/AlgebraicJulia/Gatlab.jl/blob/gh-pages/dev"
-  config["repo_root_url"] = "https://github.com/AlgebraicJulia/Gatlab.jl/blob/main/docs"
+  config["nbviewer_root_url"] = "https://nbviewer.jupyter.org/github/AlgebraicJulia/GATlab.jl/blob/gh-pages/dev"
+  config["repo_root_url"] = "https://github.com/AlgebraicJulia/GATlab.jl/blob/main/docs"
 end
 
 const literate_dir = joinpath(@__DIR__, "..", "examples")
@@ -29,13 +29,13 @@ end
 
 @info "Building Documenter.jl docs"
 makedocs(
-  modules=[Gatlab],
+  modules=[GATlab],
   format=Documenter.HTML(),
-  sitename="Gatlab.jl",
+  sitename="GATlab.jl",
   doctest=false,
   checkdocs=:none,
   pages=Any[
-    "Gatlab.jl" => "index.md",
+    "GATlab.jl" => "index.md",
     "Concepts" => Any[
       "concepts/overview.md",
       "concepts/theories.md",
@@ -49,6 +49,6 @@ makedocs(
 @info "Deploying docs"
 deploydocs(
   target="build",
-  repo="github.com/AlgebraicJulia/Gatlab.jl.git",
+  repo="github.com/AlgebraicJulia/GATlab.jl.git",
   branch="gh-pages"
 )

docs/src/api.md

@@ -1,37 +1,37 @@
 # Library Reference
 
 ```@autodocs
-Modules = [Gatlab]
+Modules = [GATlab]
 ```
 
 ## Syntax
 
 ```@autodocs
 Modules = [
-  Gatlab.Syntax,
-  Gatlab.Syntax.Scopes,
-  Gatlab.Syntax.GATs,
-  Gatlab.Syntax.Presentations,
-  Gatlab.Syntax.ExprInterop,
-  Gatlab.Syntax.TheoryInterface,
+  GATlab.Syntax,
+  GATlab.Syntax.Scopes,
+  GATlab.Syntax.GATs,
+  GATlab.Syntax.Presentations,
+  GATlab.Syntax.ExprInterop,
+  GATlab.Syntax.TheoryInterface,
 ]
 ```
 
 ## Models
 
 ```@autodocs
 Modules = [
-  Gatlab.Models,
-  Gatlab.Models.ModelInterface,
-  Gatlab.Models.SymbolicModels,
+  GATlab.Models,
+  GATlab.Models.ModelInterface,
+  GATlab.Models.SymbolicModels,
   ]
 ```
 
 ## Utilities
 
 ```@autodocs
 Modules = [
-  Gatlab.Util,
-  Gatlab.Util.MetaUtils,
+  GATlab.Util,
+  GATlab.Util.MetaUtils,
   ]
 ```

docs/src/concepts/models.md

@@ -1,6 +1,6 @@
 # Model families
 
-The semantics part of Gatlab is the *model family* infrastructure.
+The semantics part of GATlab is the *model family* infrastructure.
 
 Given a theory, one can declare a model family for that theory. This consists of the following.
 

docs/src/concepts/overview.md

@@ -1,6 +1,6 @@
 # For Catlab users
 
-Gatlab is a refactoring of the core GAT system in Catlab. There are three main differences between the Gatlab GAT system and the Catlab GAT system, in addition to a variety of new features enabled by these differences.
+GATlab is a refactoring of the core GAT system in Catlab. There are three main differences between the GATlab GAT system and the Catlab GAT system, in addition to a variety of new features enabled by these differences.
 
 ## 1. Models as values
 
@@ -14,7 +14,7 @@ end
 
 This is not ideal, but the larger problem is that this made it difficult to have models of a GAT that were parameterized by other models, because there was no way of referring to a particular model. So constructions like slice categories, dual categories, or cospan categories were not easy to do.
 
-In Gatlab, we instead do models of GATs in a more "Standard ML" style. That is, each model is a *value* that can be passed around dynamically. Then the implementations of the GAT term constructors are attached via multiple dispatch to that value. In simple cases, that value might be the unique instance of a zero-field struct, but more generally there could be more data inside the value, as is the case for slice categories. If the struct has fields, then we can think of it like a "functor" in ML parlance (which has little to do with the standard categorical use of the word functor); i.e. it is a parameterized model of the theory.
+In GATlab, we instead do models of GATs in a more "Standard ML" style. That is, each model is a *value* that can be passed around dynamically. Then the implementations of the GAT term constructors are attached via multiple dispatch to that value. In simple cases, that value might be the unique instance of a zero-field struct, but more generally there could be more data inside the value, as is the case for slice categories. If the struct has fields, then we can think of it like a "functor" in ML parlance (which has little to do with the standard categorical use of the word functor); i.e. it is a parameterized model of the theory.
 
 Sometimes we refer to this by "categories as contexts", because the category (i.e., the model of the theory of categories) serves as a context for disambiguating which method to use, and this is a pun off of the famous category theory book "Categories in Context" by Emily Riehl.
 
@@ -25,7 +25,7 @@ An e-graph is a data structure used to store congruence relations on a collectio
 - finding simple representations of terms
 - deciding whether two terms are equal
 
-The syntax systems we use for GATs in Gatlab are built from the ground-up to be compatible with a purpose-built e-graph implementation. This allows us to make use of the axioms in a GAT to rewrite terms and perform equational reasoning.
+The syntax systems we use for GATs in GATlab are built from the ground-up to be compatible with a purpose-built e-graph implementation. This allows us to make use of the axioms in a GAT to rewrite terms and perform equational reasoning.
 
 Additionally, it allows us to perform a weak form of typechecking. Typechecking in general for a GAT requires deciding the equality of arbitrary terms, which is undecidable. However, we can typecheck "up to" the collection of equivalences that we have recorded in an e-graph. Any well-typed term can be typechecked using this procedure by first placing the necessary equalities in the e-graph and then running the type-checking algorithm. Moreover, whenever this algorithm finds a positive result, one can be sure that the term does in fact typecheck. This is analogous to the termination-checking in proof assistants; we circumvent undecidability by putting the burden on the user to give us some additional data to show that their program is valid. And in many circumstances, very little additional data is required. For instance, in the bare theory of categories, there are no term constructors that produce objects. So checking whether two objects are equal in a presentation of a category is a simple problem of computing an equivalence relation (instead of a congruence relation). Thus, typechecking is very easy in this circumstance.
 
@@ -37,7 +37,7 @@ Mathematically, this can be interpreted as a requirement that models of GATs int
 
 The practical downside to this is that if you want to store several morphisms that have the same domain/codomain, you have to redundantly store the domain and codomain. So although a C-set consists of a collection of objects and morphisms in `FinSet`, we do not actually define it in this way in Catlab, because we don't want to redundantly store the objects in each morphism.
 
-In Gatlab, we fix this in the following way. When you declares a model in Gatlab, you associate types to it that correspond to the "bare" data. I.e., we would just associate `Vector{Int}` to `Hom` in an implementation of `FinSet`. Then various methods expect you to pass in the domain and codomain of a morphism in addition to the data of the morphism, rather than assuming that you can infer the domain and codomain from the data.
+In GATlab, we fix this in the following way. When you declares a model in GATlab, you associate types to it that correspond to the "bare" data. I.e., we would just associate `Vector{Int}` to `Hom` in an implementation of `FinSet`. Then various methods expect you to pass in the domain and codomain of a morphism in addition to the data of the morphism, rather than assuming that you can infer the domain and codomain from the data.
 
 Mathematically, we interpret this by saying that we interpret the dependent types as *indexed*. That is, we assign a set to each pair of objects, *and those sets can intersect*. I.e., `Hom(a,b)` could intersect non-trivially `Hom(c,d)`. So whenever we handle a morphism, we need external data that tells us what the domain and codomain is.
 

docs/src/concepts/scopes.md

@@ -37,7 +37,7 @@ context, for instance what type it is expected to be, or what arguments is it
 receiving. The second way is via *shadowing*. In shadowing, a name is resolved
 by making it point to the "most recently defined" thing with that name.
 
-In Gatlab, we handle overloading and shadowing with a notion of *scope*.
+In GATlab, we handle overloading and shadowing with a notion of *scope*.
 Anything which binds variables introduces a scope, for instance a `@theory`
 declaration or a context. Each scope is identified with a ScopeTag, which is an
 opaque identifier (i.e. a UUID). We take this idea from Racket, but we don't

docs/src/concepts/theories.md

@@ -1,6 +1,6 @@
 # Theories
 
-A theory in Gatlab consists of two parts.
+A theory in GATlab consists of two parts.
 
 1. A Julia value of type `Theory` that describes the theory.
 2. A module named by the theory with various Julia types that give us handles
@@ -19,7 +19,7 @@ Example:
 
 ```julia
 module Category
-using Gatlab.Theories
+using GATlab.Theories
 
 struct Th <: AbstractTheory end
 

docs/src/index.md

@@ -1,25 +1,25 @@
-# Gatlab.jl
+# GATlab.jl
 
 ```@meta
-CurrentModule = Gatlab
+CurrentModule = GATlab
 ```
 
-`Gatlab.jl` is a computer algebra system based on Generalized Algebraic Theories.
+`GATlab.jl` is a computer algebra system based on Generalized Algebraic Theories.
 
-Roughly speaking, Gatlab consists of two parts. The first part is concerned with *symbolic constructs*. The prototypical symbolic construct is simply a *term*, i.e. a syntax tree. In Gatlab, every term is always relative to a *context*, in which the free variables in that term are typed. And the context and term themselves are relative to an underlying theory, which defines the allowable type and term constructors that can be used in contexts and terms, along with laws that allow one to rewrite terms into equivalent other terms.
+Roughly speaking, GATlab consists of two parts. The first part is concerned with *symbolic constructs*. The prototypical symbolic construct is simply a *term*, i.e. a syntax tree. In GATlab, every term is always relative to a *context*, in which the free variables in that term are typed. And the context and term themselves are relative to an underlying theory, which defines the allowable type and term constructors that can be used in contexts and terms, along with laws that allow one to rewrite terms into equivalent other terms.
 
-We think about a term as a symbolic representation of a function from an assignment of values to the free variables to a value for the term. I.e., the term $x^{2} + y^{2}$ represents the function $\mathbb{R}^2 \to \mathbb{R}$ given by $(x,y) \mapsto x^{2} + y^{2}$. However, Gatlab also supports higher-level symbolic constructs. For instance, we can consider "substitutions" between contexts, which map free variables in one context to terms in another, as [symbolic functions](https://blog.algebraicjulia.org/post/2023/03/algebraic-geometry-1/), and we can consider a collection of equations between terms in a context as a symbolic relation. We can use these building blocks to build [symbolic dynamical systems](https://blog.algebraicjulia.org/post/2023/05/algebraic-geometry-2/) and other things along these lines. Gatlab ensures that all of the manipulation of symbolic constructs is *well-typed*, so that you don't do something like accidently add a vector and a scalar.
+We think about a term as a symbolic representation of a function from an assignment of values to the free variables to a value for the term. I.e., the term $x^{2} + y^{2}$ represents the function $\mathbb{R}^2 \to \mathbb{R}$ given by $(x,y) \mapsto x^{2} + y^{2}$. However, GATlab also supports higher-level symbolic constructs. For instance, we can consider "substitutions" between contexts, which map free variables in one context to terms in another, as [symbolic functions](https://blog.algebraicjulia.org/post/2023/03/algebraic-geometry-1/), and we can consider a collection of equations between terms in a context as a symbolic relation. We can use these building blocks to build [symbolic dynamical systems](https://blog.algebraicjulia.org/post/2023/05/algebraic-geometry-2/) and other things along these lines. GATlab ensures that all of the manipulation of symbolic constructs is *well-typed*, so that you don't do something like accidently add a vector and a scalar.
 
-The second part of Gatlab is concerned with *computational semantics*. The core of computational semantics is *models* of theories. A model tells you:
+The second part of GATlab is concerned with *computational semantics*. The core of computational semantics is *models* of theories. A model tells you:
 
 - When a Julia value is a valid instance of a type in a theory
 - How to apply term constructors to Julia values
 
-Given a model for a theory, a term in a context, and values for each of the free variables in that context, one can produce a new value by recursively applying the term constructors; this is known as *interpreting* the term. One can also *compile* the term by producing a Julia function that takes as its arguments values for the free variables in the context and then computes the value of the term. This can be faster than interpreting, because one only has to walk the syntax tree at runtime, not compile time. Analogous operations of interpretation and compilation can also be defined for higher level symbolic constructs. Moreover, Gatlab provides facilities for manipulation of *models themselves*. For instance, from a model of a ring, one can construct the model of a module over that ring, where the scalars are ring elements and the vectors are `Vector`s of ring elements.
+Given a model for a theory, a term in a context, and values for each of the free variables in that context, one can produce a new value by recursively applying the term constructors; this is known as *interpreting* the term. One can also *compile* the term by producing a Julia function that takes as its arguments values for the free variables in the context and then computes the value of the term. This can be faster than interpreting, because one only has to walk the syntax tree at runtime, not compile time. Analogous operations of interpretation and compilation can also be defined for higher level symbolic constructs. Moreover, GATlab provides facilities for manipulation of *models themselves*. For instance, from a model of a ring, one can construct the model of a module over that ring, where the scalars are ring elements and the vectors are `Vector`s of ring elements.
 
-Gatlab is the new backend for [Catlab](https://github.com/AlgebraicJulia/Catlab.jl), and we are currently working to replace the old implementation of GATs with this new one.
+GATlab is the new backend for [Catlab](https://github.com/AlgebraicJulia/Catlab.jl), and we are currently working to replace the old implementation of GATs with this new one.
 
-There are many programs which have influenced the development of Gatlab, here we just list a few
+There are many programs which have influenced the development of GATlab, here we just list a few
 
 - [MMT](https://uniformal.github.io/doc/)
 - [Maude](http://maude.cs.illinois.edu/w/index.php/The_Maude_System:About)

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.Categories.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,34 +15,34 @@ 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.Categories.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.Categories.ThClass
 ```
 
 ```@docs
-Gatlab.Stdlib.StdTheories.Categories.ThLawlessCat
+GATlab.Stdlib.StdTheories.Categories.ThLawlessCat
 ```
 
 ```@docs
-Gatlab.Stdlib.StdTheories.Categories.ThAscCat
+GATlab.Stdlib.StdTheories.Categories.ThAscCat
 ```
 
 ```@docs
-Gatlab.Stdlib.StdTheories.Categories.ThIdLawlessCat
+GATlab.Stdlib.StdTheories.Categories.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,
+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/Gatlab.jl

@@ -1,4 +1,4 @@
-module Gatlab
+module GATlab
 using Reexport
 
 # Util contains code that could be a separate package, but we include in gatlab
@@ -13,4 +13,4 @@ include("stdlib/module.jl")
 @reexport using .Models
 @reexport using .Stdlib
 
-end # module Gatlab
+end # module GATlab

src/syntax/ExprInterop.jl

@@ -8,7 +8,7 @@ using MLStyle
 """
 `toexpr(c::Context, t) -> Any`
 
-Converts Gatlab syntax into an Expr that can be read in via `fromexpr` to get
+Converts GATlab syntax into an Expr that can be read in via `fromexpr` to get
 the same thing. Crucially, the output of this will depend on the order of the
 scopes in `c`, and if read back in with a different `c` may end up with
 different results.

src/syntax/Scopes.jl

@@ -389,7 +389,7 @@ nscopes(hs::HasScope) = 1
 """
 `Scope{T, Sig}`
 
-In Gatlab, we handle overloading and shadowing with a notion of *scope*.
+In GATlab, we handle overloading and shadowing with a notion of *scope*.
 Anything which binds variables introduces a scope, for instance a `@theory`
 declaration or a context. For example, a scope with 3 elements:
 

test/Project.toml

@@ -1,4 +1,4 @@
 [deps]
-Gatlab = "f0ffcf3b-d13a-433e-917c-cc44ccf5ead2"
+GATlab = "f0ffcf3b-d13a-433e-917c-cc44ccf5ead2"
 StructEquality = "6ec83bb0-ed9f-11e9-3b4c-2b04cb4e219c"
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"

test/models/ModelInterface.jl

@@ -1,6 +1,6 @@
 module TestModelInterface 
 
-using Gatlab
+using GATlab
 using Test
 using StructEquality
 

test/models/SymbolicModels.jl

@@ -1,6 +1,6 @@
 module TestSymbolicModels
 
-using Gatlab, Test
+using GATlab, Test
 
 abstract type CategoryExpr{T} <: GATExpr{T} end
 

test/stdlib/models/FinMatrices.jl

@@ -1,6 +1,6 @@
 module TestFinMatrices
 
-using Gatlab, Test
+using GATlab, Test
 
 using .ThCategory
 

test/stdlib/models/FinSets.jl

@@ -1,6 +1,6 @@
 module TestFinSets
 
-using Gatlab, Test
+using GATlab, Test
 
 using .ThCategory
 

test/stdlib/models/Nothings.jl

@@ -1,6 +1,6 @@
 module TestNothings
 
-using Test, Gatlab
+using Test, GATlab
 
 using .ThCategory
 

test/stdlib/models/ScopeTrees.jl

@@ -1,6 +1,6 @@
 module TestScopeTrees
 
-using Test, Gatlab
+using Test, GATlab
 
 t = wrap(
   :a => pure(1),

test/stdlib/models/SliceCategories.jl

@@ -1,6 +1,6 @@
 module TestSliceCategories
 
-using Gatlab, Test
+using GATlab, Test
 
 const C = SliceC{Int, Vector{Int}, FinSetC}(FinSetC(), 4)
 const MkOb = SliceOb{Int, Vector{Int}}

test/syntax/ExprInterop.jl

@@ -1,6 +1,6 @@
 module TestExprInterop
 
-using Gatlab, Test
+using GATlab, Test
 
 bind_x = Binding{String}(:x, Set([:x, :X]), "ex")
 bind_y = Binding{String}(:y, Set([:y, :Y]), "why")

test/syntax/GATs.jl

@@ -1,6 +1,6 @@
 module TestGATs 
 
-using Gatlab, Test
+using GATlab, Test
 
 # GAT ASTs
 ##########