From 844207b7cc22fe0dc3f232efa2ad8ff961446c74 Mon Sep 17 00:00:00 2001 From: Owen Lynch Date: Mon, 18 Sep 2023 18:17:39 -0700 Subject: [PATCH] @symbolic_models replicates most of the functionality of @syntax --- docs/src/concepts/scopes.md | 31 ++- src/models/GATExprUtils.jl | 101 +++++++++ src/models/SymbolicModels.jl | 400 +++++++++++++++++++++++++++------- src/models/module.jl | 2 + src/syntax/GATs.jl | 24 +- src/util/MetaUtils.jl | 12 +- test/models/SymbolicModels.jl | 199 ++++++++--------- 7 files changed, 566 insertions(+), 203 deletions(-) create mode 100644 src/models/GATExprUtils.jl diff --git a/docs/src/concepts/scopes.md b/docs/src/concepts/scopes.md index ce68e78c..610614fc 100644 --- a/docs/src/concepts/scopes.md +++ b/docs/src/concepts/scopes.md @@ -2,17 +2,26 @@ Design rationale: -Namespacing should be first class. This doesn't play nicely with deBruijn -levels; we don't want to do a bunch of math to convert between flattened and -unflattened versions of contexts. There is an accepted solution to the problem -of organizing names: use refs! Mathematically speaking, a ref is just a list +Namespacing, i.e. references which look like `britain.economy.GDP`, should be +first class. This doesn't play nicely with the internal representation of names +via [deBruijn levels](https://en.wikipedia.org/wiki/De_Bruijn_index); we don't +want to do a bunch of math to convert between flattened and nested versions +of contexts. Conceptually, we should then switch our identifiers to be *lists* of deBruijn levels. -However, deBruijn levels are unfriendly for users; we want to be able to give -names to our variables! +But there are also significant subtleties in the translation between named and +nameless representations of identifiers. Also in practice if we are referencing +something that might change over time, like a C-set, we don't want to use +deBruijn levels, because we don't want have to change all of our identifiers +when we delete something, so in the rest of this I will instead say "local +identifier" instead of deBruijn level to refer to a nameless representation of +an identifier. -In general, naming is given by a *relation* between symbols and bindings (as -referred to by deBruijn levels). Each binding may be associated with zero or +(the name "local identifier" and also some of this philosophy is taken from +[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 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. @@ -55,11 +64,11 @@ 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 deBruijn level within that scope. Thus, the name in the `Ident` is never -needed for later stages of programatic manipulation. +and an local identifier ("lid") within that scope. Thus, the name in the `Ident` +is never needed for later stages of programatic manipulation. Scopes cache the relation between names and bindings, by providing a way to go -from binding (as reified by deBruijn level) to a set of aliases with +from binding (as reified by local identifier) to a set of aliases with distinguished primary alias, and to go from name to the set of bindings that have that name that we need to disambiguate between in the case of an overload. diff --git a/src/models/GATExprUtils.jl b/src/models/GATExprUtils.jl new file mode 100644 index 00000000..ec99c045 --- /dev/null +++ b/src/models/GATExprUtils.jl @@ -0,0 +1,101 @@ +""" Rewriting for GAT expressions. + +The current content of this module exists purely for backwards compatibility +with the existing rewriting in Catlab; the more advanced implementation uses +e-graphs and works with AlgTerms instead of GATExprs. +""" +module GATExprUtils +export associate, associate_unit_inv, associate_unit, + distribute_unary, involute, normalize_zero + +using ..SymbolicModels + +#Warning: assumes expr has only two args! +""" Simplify associative binary operation. + +Maintains the normal form `op(e1,e2,...)` where `e1`,`e2`,... are expressions +that are *not* applications of `op()` +""" +function associate(expr::E)::E where E <: GATExpr + op, e1, e2 = head(expr), first(expr), last(expr) + args1 = head(e1) == op ? args(e1) : [e1] + args2 = head(e2) == op ? args(e2) : [e2] + E([args1; args2], gat_type_args(expr)) +end + +""" Simplify associative binary operation with unit. + +Reduces a freely generated (typed) monoid to normal form. +""" +function associate_unit(expr::GATExpr, unit::Function)::GATExpr + e1, e2 = first(expr), last(expr) + if (head(e1) == nameof(unit)) e2 + elseif (head(e2) == nameof(unit)) e1 + else associate(expr) end +end + +""" Simplify associative binary operation with unit and inverses. +""" +function associate_unit_inv(expr::E, unit::Function, + inverse::Function)::GATExpr where E <: GATExpr + op, e1, e2 = head(expr), first(expr), last(expr) + if (head(e1) == nameof(unit)) e2 + elseif (head(e2) == nameof(unit)) e1 + else + args1 = head(e1) == op ? args(e1) : [e1] + args2 = head(e2) == op ? args(e2) : [e2] + while !isempty(args1) && !isempty(args2) + l = args1[end]; r = args2[1] + if (head(l) == nameof(inverse) && first(l) == r || + head(r) == nameof(inverse) && l == first(r)) + pop!(args1); popfirst!(args2) + else break end + end + newargs = [args1; args2] + # XXX: Assumes that the unit/identity takes exactly one argument, hence this + # function will not work for the algebraic theory of groups. + if (isempty(newargs)) unit(only(unique(gat_type_args(expr)))) + elseif (length(newargs) == 1) only(newargs) + else E(newargs, gat_type_args(expr)) end + end +end + +""" Distribute unary operation over binary operation. +""" +function distribute_unary(expr::GATExpr, unary::Function, binary::Function; + unit::Union{Function,Nothing}=nothing, + contravariant::Bool=false)::GATExpr + if (head(expr) != nameof(unary)) return expr end + @assert length(args(expr)) == 1 + arg = first(expr) + if head(arg) == nameof(binary) + binary(map(unary, (contravariant ? reverse : identity)(args(arg)))) + elseif !isnothing(unit) && head(arg) == nameof(unit) + arg + else + expr + end +end + +""" Simplify involutive unary operation. +""" +function involute(expr::GATExpr) + @assert length(args(expr)) == 1 + arg = first(expr) + head(expr) == head(arg) ? first(arg) : expr +end +""" +If given GATExpr contains a zero morphism, +collapse the expression to a single zero morphism. +""" +function normalize_zero(expr::E;zname=:zeromap) where E <: GATExpr + ztype = E + for subexpr in args(expr) + if head(subexpr) == zname + ztype = typeof(subexpr) + s,t = gat_type_args(expr) + return ztype([s,t],[s,t]) + end end + expr +end +end diff --git a/src/models/SymbolicModels.jl b/src/models/SymbolicModels.jl index be46b16e..359e7390 100644 --- a/src/models/SymbolicModels.jl +++ b/src/models/SymbolicModels.jl @@ -1,6 +1,7 @@ module SymbolicModels -export GATExpr, @symbolic_model, SyntaxDomainError +export GATExpr, @symbolic_model, SyntaxDomainError, head, args, gat_typeof, gat_type_args +using ...Util using ...Syntax using Base.Meta: ParseError @@ -84,47 +85,202 @@ end # Syntax ######## - """ -This is backwards compatible with the @syntax macro in Catlab +@symbolic_model generates the free model of a theory, generated by +symbols. + +This is backwards compatible with the @syntax macro in Catlab. + +One way of thinking about this is that for every type constructor, we +add an additional term constructor that builds a "symbolic" element +of that type from any Julia value. This term constructor is called "generator". + +An invocation of `@symbolic_model` creates the following. + +1. A module with a struct for each type constructor, which has a single type +parameter `T` and two fields, `args` and `type_args`. Instances of this struct +are thought of as elements of the type given by the type constructor applied to +`type_args`. The type parameter refers to the term constructor that was used +to generate the element, including the special term constructor `:generator`, +which has as its single argument an `Any`. + +For instance, in the theory of categories, we might have the following elements. + +``` +using .FreeCategory +x = Ob{:generator}([:x], []) +y = Ob{:generator}([:y], []) +f = Hom{:generator}([:f], [x, y]) +g = Hom{:generator}([:g], [y, x]) +h = Hom{:compose}([f, g], [x, x]) +``` + +2. Methods inside the module (not exported) for all of the term constructors and +field accessors (i.e. stuff like `compose, id, dom, codom`), which construct terms. + +3. A default instance (i.e., without a model parameter) of the theory using the +types in this generated model. Methods in this instance can be overridden by +the body of `@symbolic_model` to perform rewriting for the sake of normalization, +for instance flattening associative and unital operations. + +4. Coercion methods of the type constructors that allow one to introduce generators. + +``` +x = ThCategory.Ob(FreeCategory.Ob, :x) +y = ThCategory.Ob(FreeCategory.Ob, :y) +f = ThCategory.Hom(:f, x, y) +``` +Note that in both the instance and in these coercion methods, we must give the +expected type as the first argument when it cannot be infered by the other arguments. +For instance, instead of + +``` +munit() = ... +``` + +we have + +``` +munit(::Type{FreeSMC.Ob}) = ... +``` + +and likewise instead of + +``` +ThCategory.Ob(x::Any) = ... +``` + +we have + +``` +ThCategory.Ob(::Type{FreeCategory.Ob}, x::Any) = ... +``` + +Example: + +```julia @symbolic_model FreeCategory{ObExr, HomExpr} ThCategory begin + compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id) end +``` + +This generates: ```julia module FreeCategory -export Ob,Hom +export Ob, Hom using ..__module__ -theory() = ThCategory +const THEORY_MODULE = ThCategory -struct Ob{T} <: ObExpr{T} # T is :generator or a Symbol +struct Ob{T} <: __module__.ObExpr{T} # T is :generator or a Symbol args::Vector type_args::Vector{GATExpr} end -struct Hom{T} <: HomExpr{T} +struct Hom{T} <: __module__.HomExpr{T} args::Vector type_args::Vector{GATExpr} end +dom(x::Hom) = x.type_args[1] + +codom(x::Hom) = x.type_args[2] + +function compose(f::Hom, g::Hom; strict=true) + if strict && !(codom(f) == dom(g)) + throw(SyntaxDomainError(:compose, [f, g])) + end + Hom{:compose}([f, g], [dom(f), codom(g)]) +end + +function id(x::Ob) + Ob{:id}([x], [x, x]) +end +end + # default implementations -function ThCategory.dom(x::Hom)::Ob - x.type_args[1] +function ThCategory.dom(x::FreeCategory.Hom)::FreeCategory.Ob + FreeCategory.dom(x) end -function Ob(::Typ{Ob}, __value__::Any)::Ob - Ob{:generator}([__value__], []) +function ThCategory.Ob(::Type{FreeCategory.Ob}, __value__::Any)::FreeCategory.Ob + FreeCategory.Ob{:generator}([__value__], []) end -function ThCategory.id(A::Ob)::Hom - Hom{:id}([A], [A, A]) +function ThCategory.id(A::FreeCategory.Ob)::FreeCategory.Hom + FreeCategory.id(A) end -end #module +function ThCategory.compose(f::FreeCategory.Hom, g::FreeCategory.Hom; strict=true) + associate_unit(FreeCategory.compose(f, g; strict), id) +end ``` """ +macro symbolic_model(decl, theoryname, body) + # Part 0: Parsing input + + theory = macroexpand(__module__, :($theoryname.@theory)) + + (name, abstract_types) = @match decl begin + Expr(:curly, name, abstract_types...) => (name, abstract_types) + _ => throw(ParseError("Ill-formed head of @symbolic_model $decl")) + end + + overrides = Dict{Ident, JuliaFunction}() + + if !isnothing(body) + body.head == :block || error("expected a block as the body of @symbolic_model") + + for line in body.args + if line isa LineNumberNode + continue + end + f = parse_function(line) + juliasig = parse_function_sig(f) + gatsig = AlgSort.(idents(theory; name=juliasig.types)) + x = ident(theory; name=f.name, sig=gatsig) + overrides[x] = f + end + end + + theorymodule = :($__module__.$theoryname) + + # Part 1: Generating structs + + module_structs = symbolic_structs(theory, abstract_types, __module__) + + # Part 2: Generating internal methods + + module_methods = [internal_accessors(theory)..., + internal_constructors(theory)...] + + module_decl = :(module $(esc(name)) + export $(nameof.(typecons(theory))...) + using ..($(nameof(__module__))) + import ..($(nameof(__module__))): $theoryname + const $(esc(:THEORY_MODULE)) = $(esc(theoryname)) + + $(module_structs...) + $(generate_function.(module_methods)...) + end) + + # Part 3: Generating instance of theory + theory_overloads = symbolic_instance_methods(theory, theoryname, name, overrides) + + # Part 4: Generating generators. + + # generator_overloads = symbolic_generators(theorymodule, theory) + generator_overloads = [] + + Expr( + :toplevel, + module_decl, + esc.(generate_function.([theory_overloads; generator_overloads]))... + ) +end function symbolic_struct(name, abstract_type, parentmod)::Expr quote @@ -136,103 +292,179 @@ function symbolic_struct(name, abstract_type, parentmod)::Expr end function symbolic_structs(theory::GAT, abstract_types, parentmod)::Vector{Expr} - Expr[ + map(zip(theory.typecons, abstract_types)) do (X, abstract_type) symbolic_struct(nameof(X), abstract_type, parentmod) - for (X, abstract_type) in zip(theory.typecons, abstract_types) - ] + end end -function symbolic_accessor(theoryname, argname, typename, rettypename, argindex, parentmod) - quote - function $parentmod.$theoryname.$argname(x::$(esc(typename)))::$(rettypename) - x.type_args[$argindex] - end +function typename(theory::GAT, type::AlgType; parentmod=nothing) + name = nameof(sortname(theory, type)) + if !isnothing(parentmod) + Expr(:(.), parentmod, QuoteNode(name)) + else + esc(name) end end -function symbolic_accessors(theoryname, theory::GAT, parentmod)::Vector{Expr} - Expr[ - symbolic_accessor(theoryname, nameof(binding), nameof(X), typename(theory, getvalue(binding)), i, parentmod) - for X in typecons(theory) for (i, binding) in enumerate(getvalue(theory[X]).args) - ] -end +function internal_accessors(theory::GAT) + map(typecons(theory)) do X + map(enumerate(getvalue(theory[X]).args)) do (i, binding) + JuliaFunction( + name=esc(nameof(binding)), + args=[:(x::$(esc(nameof(X))))], + return_type = typename(theory, getvalue(binding)), + impl=:(x.type_args[$i]) + ) + end + end |> Iterators.flatten +end + +function internal_constructors(theory::GAT)::Vector{JuliaFunction} + map(termcons(theory)) do f + name = nameof(f) + termcon = getvalue(theory, f) + args = map(termcon.args) do binding + Expr(:(::), nameof(binding), typename(theory, getvalue(binding))) + end + + eqs = equations(termcon.args, termcon.localcontext, theory) + + throw_expr = Expr( + :call, + throw, + Expr( + :call, + SyntaxDomainError, + Expr(:quote, name), + Expr(:vect, nameof.(termcon.args)...) + ) + ) -function typename(theory::GAT, type::AlgType) - esc(nameof(sortname(theory, type))) -end + check_expr = Expr( + :&&, + map(filter(exprs -> length(exprs) > 1, collect(values(eqs)))) do exprs + cmp_expr = [] + for e in exprs + append!(cmp_expr, [build_infer_expr(e), esc(:(==))]) + end + Expr(:comparison, cmp_expr[1:end-1]...) + end... + ) -function symbolic_constructor(theoryname, name::Ident, termcon::AlgTermConstructor, theory::GAT, parentmod) - eqs = equations(termcon.args, termcon.localcontext, theory) - eq_exprs = Expr[] + check_or_error = Expr(:(||), :(!strict), check_expr, throw_expr) + exprs = [idents(termcon.args)..., idents(termcon.localcontext)...] + expr_lookup = Dict{Reference, Any}(map(exprs) do x + Reference(x) => build_infer_expr(first(eqs[x])) + end) - theorymodule = :($parentmod.$theoryname) - for expr_set in values(eqs) - exprs = build_infer_expr.(Ref(theorymodule), [expr_set...]) - for (a, b) in zip(exprs, exprs[2:end]) - errexpr = Expr(:call, throw, Expr(:call, GlobalRef(SymbolicModels, :SyntaxDomainError), - Expr(:quote, nameof(name)), - Expr(:vect, nameof.(termcon.args)...))) + build = Expr( + :call, + Expr(:curly, typename(theory, termcon.type), Expr(:quote, name)), + Expr(:vect, nameof.(termcon.args)...), + Expr(:ref, GATExpr, compile.(Ref(expr_lookup), termcon.type.args)...) + ) - push!(eq_exprs, Expr(:(||), Expr(:call, :(==), a, b), errexpr)) + JuliaFunction( + ;name=esc(name), + args=args, + kwargs=[Expr(:kw, :strict, false)], + impl=Expr(:block, check_or_error, build) + ) + end +end + +macro symbolic_model(decl, theoryname) + esc(:(@symbolic_model $decl $theoryname $nothing)) +end + +"""Julia function for every type constructor, accessor, and term constructor. +Term constructors can be overwritten by `overrides`. """ +function symbolic_instance_methods( + theory::GAT, theorymodule, syntaxname::Symbol, + overrides::Dict{Ident, JuliaFunction})::Vector{JuliaFunction} + + type_con_funs = [] + accessors_funs = [] + for type_con_id in typecons(theory) + type_con = getvalue(theory[type_con_id]) + symgen = symbolic_generator(theorymodule, syntaxname, type_con_id, type_con, theory) + push!(type_con_funs, symgen) + for binding in type_con.args + push!(accessors_funs, symbolic_accessor(theorymodule, theory, syntaxname, type_con_id, binding)) end end - expr_lookup = Dict{Reference, Any}( - [Reference(x) => build_infer_expr(theorymodule, first(eqs[x])) - for x in [idents(termcon.args)..., idents(termcon.localcontext)...]] - ) + type_replacements = [nameof(X) => Expr(:(.), syntaxname, QuoteNode(nameof(X))) for X in typecons(theory)] - quote - function $theorymodule.$(nameof(name))( - $([Expr(:(::), nameof(binding), typename(theory, getvalue(binding))) - for binding in termcon.args]...) - ) - $(eq_exprs...) - $(typename(theory, termcon.type)){$(Expr(:quote, nameof(name)))}( - $(Expr(:vect, nameof.(termcon.args)...)), - $(Expr(:ref, GlobalRef(SymbolicModels, :GATExpr), - [compile(theorymodule, expr_lookup, arg) for arg in termcon.type.args]...)) + term_con_funs = map(termcons(theory)) do term_con_id + if haskey(overrides, term_con_id) + replace_symbols( + Dict([ + :new => Expr(:(.), syntaxname, QuoteNode(nameof(term_con_id))); type_replacements + ]), + setname(overrides[term_con_id], Expr(:(.), theorymodule, QuoteNode(nameof(term_con_id)))) ) + else + symbolic_termcon(theorymodule, theory, syntaxname, term_con_id) end end + [type_con_funs..., accessors_funs..., term_con_funs...] end -function symbolic_constructors(theoryname, theory::GAT, parentmod)::Vector{Expr} - Expr[ - symbolic_constructor(theoryname, x, getvalue(theory[x]), theory, parentmod) - for x in termcons(theory) + +function symbolic_generator(theorymodule, syntaxname, X::Ident, typecon::AlgTypeConstructor, theory::GAT) + value_param = gensym(:value) + name = nameof(X) + args = [ + Expr(:(::), value_param, Any); + [Expr(:(::), nameof(binding), typename(theory, getvalue(binding); parentmod=syntaxname)) + for binding in typecon.args] ] -end -macro symbolic_model(decl, theoryname, body) - theory = macroexpand(__module__, :($theoryname.@theory)) - - (name, abstract_types) = @match decl begin - Expr(:curly, name, abstract_types...) => (name, abstract_types) - _ => throw(ParseError("Ill-formed head of @symbolic_model $decl")) + if isempty(typecon.args) + args = [Expr(:(::), Expr(:curly, Type, Expr(:(.), syntaxname, QuoteNode(name)))); args] end + impl = quote + $(Expr(:(.), syntaxname, QuoteNode(name))){:generator}( + $(Expr(:vect, value_param, nameof.(typecon.args)...)), + $(Expr(:ref, GATExpr, nameof.(typecon.args)...)) + ) + end + JuliaFunction(name=Expr(:(.), theorymodule, QuoteNode(name)), args=args,impl=impl ) +end - structs = symbolic_structs(theory, abstract_types, __module__) - - accessors = symbolic_accessors(theoryname, theory, __module__) - - constructors = symbolic_constructors(theoryname, theory, __module__) - - Expr(:toplevel, - :(module $(esc(name)) - using ..($(nameof(__module__))) - import ..($(nameof(__module__))): $theoryname - const $(esc(:THEORY_MODULE)) = $(esc(theoryname)) - - $(structs...) - - $(accessors...) +function symbolic_accessor(theorymodule, theory, name, typecon::Ident, accessor::Binding, ) + typcon_name = QuoteNode(nameof(typecon)) + accessor_name = QuoteNode(nameof(accessor)) + JuliaFunction( + name=Expr(:(.), theorymodule, accessor_name), + args=[:(x::$(Expr(:(.), name, typcon_name)))], + return_type = typename(theory, getvalue(accessor); parentmod=name), + impl=Expr(:call, Expr(:(.), name, accessor_name), :x) + ) +end - $(constructors...) - end) +function symbolic_termcon(theorymodule, theory, syntaxname, termcon_id::Ident ) + termcon_name = QuoteNode(nameof(termcon_id)) + termcon = getvalue(theory[termcon_id]) + return_type = typename(theory, termcon.type; parentmod=syntaxname) + args = if !isempty(termcon.args) + map(termcon.args) do argbinding + type = typename(theory, getvalue(argbinding); parentmod=syntaxname) + Expr(:(::), nameof(argbinding), type) + end + else + [Expr(:(::), Expr(:curly, Type, return_type))] + end + JuliaFunction( + name=Expr(:(.), theorymodule, termcon_name), + args=args, + return_type=return_type, + impl=Expr(:call, Expr(:(.), syntaxname, termcon_name), nameof.(termcon.args)...) ) end + # Reflection ############ diff --git a/src/models/module.jl b/src/models/module.jl index 1a9c9b6c..d44fc8d2 100644 --- a/src/models/module.jl +++ b/src/models/module.jl @@ -4,8 +4,10 @@ using Reexport include("ModelInterface.jl") include("SymbolicModels.jl") +include("GATExprUtils.jl") @reexport using .ModelInterface @reexport using .SymbolicModels +@reexport using .GATExprUtils end diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl index 1d2e2c28..32e6347a 100644 --- a/src/syntax/GATs.jl +++ b/src/syntax/GATs.jl @@ -387,11 +387,17 @@ end const InferExpr = Union{Ident, AccessorApplication} -function build_infer_expr(theorymodule, e::InferExpr) +function build_infer_expr(e::InferExpr; theorymodule=nothing) if e isa Ident nameof(e) else - Expr(:call, :($theorymodule.$(nameof(e.accessor))), build_infer_expr(theorymodule, e.to)) + name = nameof(e.accessor) + accessor = if !isnothing(theorymodule) + :($theorymodule.$name) + else + esc(name) + end + Expr(:call, accessor, build_infer_expr(e.to; theorymodule)) end end @@ -453,18 +459,20 @@ function equations(args::TypeScope, localcontext::TypeScope, theory::GAT) ways_of_computing end -function compile(theorymodule, expr_lookup::Dict{Reference}, term::AlgTerm) +function compile(expr_lookup::Dict{Reference}, term::AlgTerm; theorymodule=nothing) if term.head isa Constant term.head.value else if haskey(expr_lookup, term.head) expr_lookup[term.head] else - Expr( - :call, - :($theorymodule.$(nameof(only(term.head)))), - [compile(theorymodule, expr_lookup, arg) for arg in term.args]... - ) + name = nameof(only(term.head)) + fun = if !isnothing(theorymodule) + :($theorymodule.$name) + else + esc(name) + end + Expr(:call, fun, [compile(expr_lookup, arg; theorymodule) for arg in term.args]...) end end end diff --git a/src/util/MetaUtils.jl b/src/util/MetaUtils.jl index 5c15ec56..e6708a0f 100644 --- a/src/util/MetaUtils.jl +++ b/src/util/MetaUtils.jl @@ -1,7 +1,7 @@ """ General-purpose tools for metaprogramming in Julia. """ module MetaUtils -export JuliaFunction, setimpl, +export JuliaFunction, setimpl, setname, JuliaFunctionSig, parse_docstring, parse_function, parse_function_sig, generate_docstring, generate_function, replace_symbols, strip_lines, @@ -29,11 +29,19 @@ const Expr0 = Union{Symbol,Expr} return_type=nothing, impl=nothing, doc=nothing) new(name, args, kwargs, whereparams, return_type, impl, doc) end + + function JuliaFunction(;name::Expr0, args=Expr0[], kwargs=Expr0[], whereparams=Expr0[], + return_type=nothing, impl=nothing, doc=nothing) + new(name, args, kwargs, whereparams, return_type, impl, doc) + end end setimpl(f::JuliaFunction, impl) = JuliaFunction(f.name, f.args, f.kwargs, f.whereparams, f.return_type, impl, f.doc) +setname(f::JuliaFunction, name) = + JuliaFunction(name, f.args, f.kwargs, f.whereparams, f.return_type, f.impl, f.doc) + @struct_hash_equal struct JuliaFunctionSig name::Expr0 types::Vector{Expr0} @@ -155,7 +163,7 @@ end """ function replace_symbols(bindings::AbstractDict, f::JuliaFunction)::JuliaFunction JuliaFunction( - replace_symbols(bindings, f.name), + f.name, replace_symbols.(Ref(bindings), f.args), replace_symbols.(Ref(bindings), f.kwargs), replace_symbols.(Ref(bindings), f.whereparams), diff --git a/test/models/SymbolicModels.jl b/test/models/SymbolicModels.jl index 52a8a95b..856f11c6 100644 --- a/test/models/SymbolicModels.jl +++ b/test/models/SymbolicModels.jl @@ -9,6 +9,7 @@ abstract type ObExpr{T} <: CategoryExpr{T} end abstract type HomExpr{T} <: CategoryExpr{T} end @symbolic_model FreeCategory{ObExpr, HomExpr} ThCategory begin + compose(f::Hom, g::Hom) = associate_unit(new(f,g), ThCategory.id) end x, y = FreeCategory.Ob{:generator}([:x], []), FreeCategory.Ob{:generator}([:y], []) @@ -16,100 +17,100 @@ f = FreeCategory.Hom{:generator}([:f], [x, y]) @test x isa ObExpr{:generator} @test ThCategory.id(x) isa HomExpr{:id} -@test ThCategory.compose(ThCategory.id(x), f) isa HomExpr{:compose} -@test_throws SyntaxDomainError ThCategory.compose(f, f) - -try - ThCategory.compose(f, f) -catch e - @test sprint(showerror, e) isa String -end +@test ThCategory.compose(ThCategory.id(x), f) == f # Monoid ######## -# """ Theory of monoids. -# """ -# @theory ThMonoid begin -# Elem::TYPE -# munit()::Elem -# mtimes(x::Elem,y::Elem)::Elem -# end +""" Theory of monoids. +""" -# """ Syntax for the theory of monoids. -# """ -# @symbolic_model FreeMonoid{GATExpr} ThMonoid begin -# end +@theory ThMonoid begin + Elem::TYPE + munit()::Elem + mtimes(x::Elem,y::Elem)::Elem +end + +""" Syntax for the theory of monoids. +""" + +@symbolic_model FreeMonoid{GATExpr} ThMonoid -# Elem(mod::Module, args...) = Elem(mod.Elem, args...) +import .ThMonoid: Elem +using .ThMonoid -# @test isa(FreeMonoid, Module) +Elem(mod::Module, args...) = Elem(mod.Elem, args...) + +@test isa(FreeMonoid, Module) # @test occursin("theory of monoids", string(Docs.doc(FreeMonoid))) # @test sort(names(FreeMonoid)) == sort([:FreeMonoid, :Elem]) -# x, y, z = Elem(FreeMonoid,:x), Elem(FreeMonoid,:y), Elem(FreeMonoid,:z) -# @test isa(mtimes(x,y), FreeMonoid.Elem) -# @test isa(munit(FreeMonoid.Elem), FreeMonoid.Elem) +x, y, z = Elem(FreeMonoid,:x), Elem(FreeMonoid,:y), Elem(FreeMonoid,:z) +@test isa(mtimes(x,y), FreeMonoid.Elem) +@test isa(munit(FreeMonoid.Elem), FreeMonoid.Elem) # @test gat_typeof(x) == :Elem # @test gat_typeof(mtimes(x,y)) == :Elem -# @test mtimes(mtimes(x,y),z) != mtimes(x,mtimes(y,z)) +@test mtimes(mtimes(x,y),z) != mtimes(x,mtimes(y,z)) # # Test equality -# @test x == Elem(FreeMonoid,:x) -# @test x != y -# @test Elem(FreeMonoid,"X") == Elem(FreeMonoid,"X") -# @test Elem(FreeMonoid,"X") != Elem(FreeMonoid,"Y") - -# # Test hash -# @test hash(x) == hash(x) -# @test hash(x) != hash(y) -# @test hash(mtimes(x,y)) == hash(mtimes(x,y)) -# @test hash(mtimes(x,y)) != hash(mtimes(x,z)) - -# @syntax FreeMonoidAssoc ThMonoid begin -# mtimes(x::Elem, y::Elem) = associate(new(x,y)) -# end +@test x == Elem(FreeMonoid,:x) +@test x != y +@test Elem(FreeMonoid,"X") == Elem(FreeMonoid,"X") +@test Elem(FreeMonoid,"X") != Elem(FreeMonoid,"Y") + +# Test hash +@test hash(x) == hash(x) +@test hash(x) != hash(y) +@test hash(mtimes(x,y)) == hash(mtimes(x,y)) +@test hash(mtimes(x,y)) != hash(mtimes(x,z)) + +@symbolic_model FreeMonoidAssoc{GATExpr} ThMonoid begin + mtimes(x::Elem, y::Elem) = associate(new(x,y)) +end -# x, y, z = [ Elem(FreeMonoidAssoc,sym) for sym in [:x,:y,:z] ] -# e = munit(FreeMonoidAssoc.Elem) -# @test mtimes(mtimes(x,y),z) == mtimes(x,mtimes(y,z)) -# @test mtimes(e,x) != x && mtimes(x,e) != x +x, y, z = [ Elem(FreeMonoidAssoc,sym) for sym in [:x,:y,:z] ] +e = munit(FreeMonoidAssoc.Elem) +@test mtimes(mtimes(x,y),z) == mtimes(x,mtimes(y,z)) +@test mtimes(e,x) != x && mtimes(x,e) != x -# @syntax FreeMonoidAssocUnit ThMonoid begin -# mtimes(x::Elem, y::Elem) = associate_unit(new(x,y), munit) -# end +@symbolic_model FreeMonoidAssocUnit{GATExpr} ThMonoid begin + mtimes(x::Elem, y::Elem) = associate_unit(new(x,y), munit) +end -# x, y, z = [ Elem(FreeMonoidAssocUnit,sym) for sym in [:x,:y,:z] ] -# e = munit(FreeMonoidAssocUnit.Elem) -# @test mtimes(mtimes(x,y),z) == mtimes(x,mtimes(y,z)) -# @test mtimes(e,x) == x && mtimes(x,e) == x +x, y, z = [ Elem(FreeMonoidAssocUnit,sym) for sym in [:x,:y,:z] ] +e = munit(FreeMonoidAssocUnit.Elem) +@test mtimes(mtimes(x,y),z) == mtimes(x,mtimes(y,z)) +@test mtimes(e,x) == x && mtimes(x,e) == x -# abstract type MonoidExpr{T} <: GATExpr{T} end -# @syntax FreeMonoidTyped{MonoidExpr} ThMonoid +abstract type MonoidExpr{T} <: GATExpr{T} end +@symbolic_model FreeMonoidTyped{MonoidExpr} ThMonoid -# x = Elem(FreeMonoidTyped.Elem, :x) -# @test FreeMonoidTyped.Elem <: MonoidExpr -# @test isa(x, FreeMonoidTyped.Elem) && isa(x, MonoidExpr) +x = Elem(FreeMonoidTyped.Elem, :x) +@test FreeMonoidTyped.Elem <: MonoidExpr +@test isa(x, FreeMonoidTyped.Elem) && isa(x, MonoidExpr) # @signature ThMonoidNumeric{Elem} <: ThMonoid{Elem} begin # elem_int(x::Int)::Elem # end + # @syntax FreeMonoidNumeric ThMonoidNumeric # x = elem_int(FreeMonoidNumeric.Elem, 1) # @test isa(x, FreeMonoidNumeric.Elem) # @test first(x) == 1 -# """ A monoid with two distinguished elements. -# """ -# @signature ThMonoidTwo{Elem} <: ThMonoid{Elem} begin -# one()::Elem -# two()::Elem -# end +""" A monoid with two distinguished elements. +""" + +@theory ThMonoidTwo <: ThMonoid begin + one()::Elem + two()::Elem +end + +""" The free monoid on two generators. +""" -# """ The free monoid on two generators. -# """ -# @syntax FreeMonoidTwo ThMonoidTwo begin +# @symbolic_model FreeMonoidTwo{GATExpr} ThMonoidTwo begin # Elem(::Type{Elem}, value) = error("No extra generators allowed!") # end @@ -117,50 +118,52 @@ end # @test all(isa(expr, FreeMonoidTwo.Elem) for expr in [x, y, mtimes(x,y)]) # @test_throws ErrorException Elem(FreeMonoidTwo, :x) -# # Category -# ########## +# Category +########## -# @signature ThCategory{Ob,Hom} begin -# Ob::TYPE -# Hom(dom::Ob, codom::Ob)::TYPE +@theory ThCategory′ begin + Ob::TYPE + Hom(dom::Ob, codom::Ob)::TYPE -# id(X::Ob)::Hom(X,X) -# compose(f::Hom(X,Y), g::Hom(Y,Z))::Hom(X,Z) ⊣ (X::Ob, Y::Ob, Z::Ob) -# end + id(X::Ob)::Hom(X,X) + compose(f::Hom(X,Y), g::Hom(Y,Z))::Hom(X,Z) ⊣ [X::Ob, Y::Ob, Z::Ob] +end -# @syntax FreeCategory ThCategory begin -# compose(f::Hom, g::Hom) = associate(new(f,g)) -# end +@symbolic_model FreeCategory′{GATExpr, GATExpr} ThCategory′ begin + compose(f::Hom, g::Hom) = associate(new(f,g)) +end -# @test isa(FreeCategory, Module) -# @test sort(names(FreeCategory)) == sort([:FreeCategory, :Ob, :Hom]) +@test isa(FreeCategory′, Module) +@test sort(names(FreeCategory′)) == sort([:FreeCategory′, :Ob, :Hom]) -# X, Y, Z, W = [ Ob(FreeCategory.Ob, sym) for sym in [:X, :Y, :Z, :W] ] -# f, g, h = Hom(:f, X, Y), Hom(:g, Y, Z), Hom(:h, Z, W) -# @test isa(X, FreeCategory.Ob) && isa(f, FreeCategory.Hom) -# @test_throws MethodError FreeCategory.Hom(:f) -# @test dom(f) == X -# @test codom(f) == Y +using .ThCategory′ -# @test isa(id(X), FreeCategory.Hom) -# @test dom(id(X)) == X -# @test codom(id(X)) == X +X, Y, Z, W = [ Ob(FreeCategory′.Ob, sym) for sym in [:X, :Y, :Z, :W] ] +f, g, h = Hom(:f, X, Y), Hom(:g, Y, Z), Hom(:h, Z, W) +@test isa(X, FreeCategory′.Ob) && isa(f, FreeCategory′.Hom) +@test_throws MethodError FreeCategory′.Hom(:f) +@test dom(f) == X +@test codom(f) == Y -# @test isa(compose(f,g), FreeCategory.Hom) -# @test dom(compose(f,g)) == X -# @test codom(compose(f,g)) == Z -# @test isa(compose(f,f), FreeCategory.Hom) # Doesn't check domains. -# @test compose(compose(f,g),h) == compose(f,compose(g,h)) +@test isa(id(X), FreeCategory′.Hom) +@test dom(id(X)) == X +@test codom(id(X)) == X -# @syntax FreeCategoryStrict ThCategory begin -# compose(f::Hom, g::Hom) = associate(new(f,g; strict=true)) -# end +@test isa(compose(f,g), FreeCategory′.Hom) +@test dom(compose(f,g)) == X +@test codom(compose(f,g)) == Z +@test isa(compose(f,f), FreeCategory′.Hom) # Doesn't check domains. +@test compose(compose(f,g),h) == compose(f,compose(g,h)) + +@symbolic_model FreeCategoryStrict{ObExpr, HomExpr} ThCategory′ begin + compose(f::Hom, g::Hom) = associate(new(f,g; strict=true)) +end -# X, Y = Ob(FreeCategoryStrict.Ob, :X), Ob(FreeCategoryStrict.Ob, :Y) -# f, g = Hom(:f, X, Y), Hom(:g, Y, X) +X, Y = Ob(FreeCategoryStrict.Ob, :X), Ob(FreeCategoryStrict.Ob, :Y) +f, g = Hom(:f, X, Y), Hom(:g, Y, X) -# @test isa(compose(f,g), FreeCategoryStrict.Hom) -# @test_throws SyntaxDomainError compose(f,f) +@test isa(compose(f,g), FreeCategoryStrict.Hom) +@test_throws SyntaxDomainError compose(f,f) # # Functor # #########