Trivial docs edits and rename @Migrate

Project.toml

@@ -5,6 +5,7 @@ version = "0.0.7"
 
 [deps]
 AlgebraicInterfaces = "23cfdc9f-0504-424a-be1f-4892b28e2f0c"
+Catlab = "134e5e36-593f-5add-ad60-77f754baafbe"
 Colors = "5ae59095-9a9b-59fe-a467-6f913c188581"
 Crayons = "a8cc5b0e-0ffa-5ad4-8c14-923d3ee1735f"
 DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8"

docs/src/concepts/catlab_differences.md

@@ -1,6 +1,6 @@
 # Changes from Catlab GATs
 
-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 from Catlab versions older than 0.16. 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.
 
 However, GATlab has a full backward compatibility layer with the GAT system as used to be used in Catlab; the new features are mostly only opt-in.
 
@@ -29,7 +29,7 @@ An e-graph is a data structure used to store congruence relations on a collectio
 
 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.
+Additionally, it allows us to perform a weak form of typechecking. Fully general typechecking in a GAT  is undecidable, as types may depend on terms and *term* equality is certainly 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.
 
 ## 3. Indexed dependent types in models
 
@@ -39,7 +39,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. E.g., 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/theories.md

@@ -109,20 +109,12 @@ inherit a theory that already has the alias defined.
 
 The result of the `@theory` macro is a module with the following members:
 
-1. For each *declaration* in the theory (which includes term constructors,
-type constructors, arguments to type constructors (i.e. accessors like `dom`
-and `codom`), and aliases of the above), a function named with the name of the
-declaration. These functions are not necessarily original to this module; they
-may be imported. This allows us to, for instance, use `Base.+` as a method for a
-theory. For instance, `ThCategory` has functions `Ob, Hom, dom, codom, compose,
-id, ⋅, →`.
+1. For each *declaration* in the theory (which includes term constructors, type constructors, arguments to type constructors (i.e. accessors like `dom` and `codom`), and aliases of the above), a function named with the name of the declaration. These functions are not necessarily original to this module; they may be imported. This allows us to, for instance, use `Base.+` as a method for a theory. For instance, `ThCategory` has functions `Ob, Hom, dom, codom, compose, id, ⋅, →`.
 
 2. A submodule called `Meta` with members:
-  - `T`: a zero-field struct that serves as a type-level signifier for the
-theory
+  - `T`: a zero-field struct that serves as a type-level signifier for the theory.
   - `theory`: a constant of type `GAT` which stores the data of the theory.
-  - `@theory`: a macro which expands directly to `theory`, which is used to pass
-around the data of the theory at macro-expand time.
+  - `@theory`: a macro which expands directly to `theory`, which is used to pass around the data of the theory at macro-expand time.
 
 !!! note
 

docs/src/index.md

@@ -8,18 +8,18 @@ CurrentModule = GATlab
 
 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. E.g., 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:
 
 - 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 the theory of a rings, one can construct a model of the theory of modules over that ring where the scalars are ring elements and the vectors are `Vector`s of ring elements. This corresponds mathematically to the infinite direct sum of copies of the ring with itself.
 
-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 (as of Catlab 0.16) 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)

src/models/ModelInterface.jl

@@ -1,7 +1,7 @@
 module ModelInterface
 
 export Model, implements, TypeCheckFail, SignatureMismatchError, 
-       @model, @instance, @withmodel, @fail, @migrate
+       @model, @instance, @withmodel, @fail, @migrate_theory
 
 using ...Syntax
 using ...Util.MetaUtils
@@ -585,7 +585,7 @@ E.g. given NatIsMonoid: ThMonoid->ThNatPlus and IntPlus <: Model{Tuple{Int}}
 and IntPlus implements ThNatPlus:
 
 ```
-@migrate IntPlusMonoid = NatIsMonoid(IntPlus){Int}
+@migrate_theory IntPlusMonoid = NatIsMonoid(IntPlus){Int}
 ```
 
 Yields:
@@ -601,7 +601,7 @@ end
 Future work: There is some subtlety in how accessor functions should be handled.
 TODO: The new instance methods do not yet handle the `context` keyword argument.
 """
-macro migrate(head)
+macro migrate_theory(head)
   # Parse
   (name, mapname, modelname) = @match head begin
     Expr(:(=), name, Expr(:call, mapname, modelname)) =>

src/stdlib/derivedmodels/DerivedModels.jl

@@ -6,12 +6,12 @@ using ...StdTheoryMaps
 using ...StdModels
 
 # Given a model of a category C, we can derive a model of Cᵒᵖ.
-@migrate OpFinSetC = OpCat(FinSetC)
+@migrate_theory OpFinSetC = OpCat(FinSetC)
 
 # Interpret `e` as `0` and `⋅` as `+`.
-@migrate IntMonoid = NatPlusMonoid(IntNatPlus)
+@migrate_theory IntMonoid = NatPlusMonoid(IntNatPlus)
 
 # Interpret `id` as reflexivity and `compose` as transitivity.
-@migrate IntPreorderCat = PreorderCat(IntPreorder)
+@migrate_theory IntPreorderCat = PreorderCat(IntPreorder)
 
 end