From 0f734fc4a53671b43638fb2d4e1c8e286988d2ef Mon Sep 17 00:00:00 2001 From: Kris Brown Date: Sat, 23 Dec 2023 09:11:35 -0500 Subject: [PATCH 1/4] initial combinatorial work add and remove part NestedType/Term, better add/rem part Iterate through NM more hom progress. checkpoint before refactor NestedType/Term, better add/rem part implement ThCategory, functioning HomSearch epic / monic constraint (begun) hom search working iso initial constraint --- .gitignore | 2 + GATlab/Project.toml | 2 + Project.toml | 1 + src/GATlab.jl | 2 + src/combinatorial/CModels.jl | 316 ++++++++++++++++ src/combinatorial/DataStructs.jl | 536 +++++++++++++++++++++++++++ src/combinatorial/HomSearch.jl | 347 +++++++++++++++++ src/combinatorial/Limits.jl | 42 +++ src/combinatorial/TypeScopes.jl | 76 ++++ src/combinatorial/Visualization.jl | 172 +++++++++ src/combinatorial/module.jl | 20 + src/models/ModelInterface.jl | 1 + src/nonstdlib/theories/Categories.jl | 9 + src/nonstdlib/theories/Petri.jl | 19 + src/nonstdlib/theories/Wiring.jl | 39 ++ src/nonstdlib/theories/module.jl | 2 + src/syntax/GATs.jl | 2 +- src/syntax/Scopes.jl | 8 +- src/syntax/TheoryMaps.jl | 58 ++- src/syntax/gats/algorithms.jl | 2 +- src/syntax/gats/gat.jl | 15 +- src/syntax/gats/judgments.jl | 2 +- src/util/Eithers.jl | 5 +- test/combinatorial/Combinatorial.jl | 72 ++++ test/combinatorial/Constructor.jl | 158 ++++++++ test/combinatorial/HomSearch.jl | 104 ++++++ test/combinatorial/tests.jl | 7 + test/models/ModelInterface.jl | 2 +- test/runtests.jl | 4 + 29 files changed, 1999 insertions(+), 26 deletions(-) create mode 100644 GATlab/Project.toml create mode 100644 src/combinatorial/CModels.jl create mode 100644 src/combinatorial/DataStructs.jl create mode 100644 src/combinatorial/HomSearch.jl create mode 100644 src/combinatorial/Limits.jl create mode 100644 src/combinatorial/TypeScopes.jl create mode 100644 src/combinatorial/Visualization.jl create mode 100644 src/combinatorial/module.jl create mode 100644 src/nonstdlib/theories/Categories.jl create mode 100644 src/nonstdlib/theories/Petri.jl create mode 100644 src/nonstdlib/theories/Wiring.jl create mode 100644 test/combinatorial/Combinatorial.jl create mode 100644 test/combinatorial/Constructor.jl create mode 100644 test/combinatorial/HomSearch.jl create mode 100644 test/combinatorial/tests.jl diff --git a/.gitignore b/.gitignore index 5d6c467f..f11e04be 100644 --- a/.gitignore +++ b/.gitignore @@ -26,3 +26,5 @@ docs/site/ # committed for packages, but should be committed for applications that require a static # environment. Manifest.toml + +src/.DS_Store diff --git a/GATlab/Project.toml b/GATlab/Project.toml new file mode 100644 index 00000000..5a88dc4d --- /dev/null +++ b/GATlab/Project.toml @@ -0,0 +1,2 @@ +[deps] +PrettyTables = "08abe8d2-0d0c-5749-adfa-8a2ac140af0d" diff --git a/Project.toml b/Project.toml index 1e59b305..17c8c208 100644 --- a/Project.toml +++ b/Project.toml @@ -10,6 +10,7 @@ Crayons = "a8cc5b0e-0ffa-5ad4-8c14-923d3ee1735f" DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8" JSON = "682c06a0-de6a-54ab-a142-c8b1cf79cde6" MLStyle = "d8e11817-5142-5d16-987a-aa16d5891078" +PrettyTables = "08abe8d2-0d0c-5749-adfa-8a2ac140af0d" Random = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c" Reexport = "189a3867-3050-52da-a836-e630ba90ab69" StructEquality = "6ec83bb0-ed9f-11e9-3b4c-2b04cb4e219c" diff --git a/src/GATlab.jl b/src/GATlab.jl index bc3b0dc5..67294083 100644 --- a/src/GATlab.jl +++ b/src/GATlab.jl @@ -7,11 +7,13 @@ include("util/module.jl") include("syntax/module.jl") include("models/module.jl") include("stdlib/module.jl") +include("combinatorial/module.jl") include("nonstdlib/module.jl") # don't reexport this @reexport using .Util @reexport using .Syntax @reexport using .Models @reexport using .Stdlib +@reexport using .Combinatorial end # module GATlab diff --git a/src/combinatorial/CModels.jl b/src/combinatorial/CModels.jl new file mode 100644 index 00000000..196ba369 --- /dev/null +++ b/src/combinatorial/CModels.jl @@ -0,0 +1,316 @@ +"""Helpful functions for interacting with combinatorial models of GATs""" +module CModels + +export interpret, add_part!, rem_part! + +using ...Models +using ...Util.MetaUtils +using ...Syntax +import ...Syntax: GATContext, AlgSort, headof, argsof +using ...Syntax.TheoryMaps: infer_type, bind_localctx + +using ..DataStructs +using ..DataStructs: NMIs, NMI, getsort, subterms, ScopedNMs, ScopedNM, Nest +using ..TypeScopes: partition, subscope, vars, repartition, repartition_idx +import ..DataStructs: CombinatorialModel, random_cardinalities + +# Generating random model +######################### + +""" +Create a random combinatorial model, possibly with initialized data. For +unspecified cardinality data, a range of possible set sizes is specifiable. +""" +function CombinatorialModel(t::GAT; init=nothing, card_range=nothing) + isets, ifuns = [Dict{AlgSort, NMI}() for _ in 1:2] + for (k, v) in (isnothing(init) ? [] : init) + (k ∈ sorts(t) ? isets : ifuns)[k] = (v isa ScopedNM ? getvalue(v) : v) + end + sets = random_cardinalities(t, card_range; init=isets) + funs = random_functions(sets, t; init=ifuns) + CombinatorialModel(t, sets, funs) +end + +""" +Randomly generate a choice of cardinality for every possible set associated +with the sorts of a theory. This is a dependent process: the possible elements +of |Ob| determine the possible elements of |Hom| (which happens to be |Ob|²). +But there can be trickiness depending on the signature, e.g.: + +Hom2(f,g) ⊣ [(a,b)::Ob, (f,g)::Hom(a,b)] --- partition = [[1,2],[3,4]] + +|Hom2| is NOT equal to |Hom|², since `f` and `g` are not completely independent: +they must have the same dom and codom. If we have: + + |Ob| = 2 |Hom(1,1)| = 2 |Hom(2,1)| = 0 |Hom(1,2)| = 1 |Hom(2,2)| = 1 + +e.g. Ob=[ω,β] Hom(ω,ω) = [η,μ] Hom(β,ω) = [] Hom(ω,β) = [δ] Hom(β,β) = [ξ] + +Then we could potentially get a Hom2 matrix like: + + a=ω a=β + ⌜-------------⌝ +b=ω | [3 2 | | i.e. Hom2(η,η) = |3|, Hom2(η,μ) = |2|, Hom2(μ,η) = |1| + | 1 0] |[]₀ₓ₀| Hom2(μ,μ) = |0|, Hom2(δ,δ) = |2|, Hom2(ξ,ξ) = |1| + |-------------| +b=β | [2] | [1] | + ⌞-------------⌟ +""" +function random_cardinalities(theory::GAT, card_range=nothing; + init=nothing)::NMIs + res = isnothing(init) ? NMIs() : (init isa Dict ? ScopedNMs(theory, init) : init) + card_range = isnothing(card_range) ? (0:3) : card_range + for sort in setdiff(sorts(theory), keys(res)) + ctx = getcontext(theory, sort) + res[sort] = ScopedNM(rand_nm(res, theory, ctx, Int[], card_range), ctx) + end + res +end + +""" Generate random functions for a combinatorial model """ +function random_functions(cards::NMIs, theory::GAT; init=nothing)::NMIs + res = isnothing(init) ? NMIs() : (init isa Dict ? ScopedNMs(theory, init) : init) + for s in funsorts(theory) + haskey(res, s) && continue + res[s] = ScopedNM(random_function(cards, theory, s), getcontext(theory, s)) + end + res +end + +""" +Given a term constructor context, e.g. [(a,b,c)::Ob, f::a→b, g::b→c], and given +some choices of sets (e.g. [[a=1,b=3,c=2],[f=2,g=4]]) determine the dependent set +which is the codomain of the function and randomly pick an element of it. + +"0" represents an unspecified output, which should be used if the codom is +empty. +""" +function random_function(cards::NMIs, theory::GAT, s::AlgSort) + tc = getvalue(theory[methodof(s)]) + lc = tc.localcontext + retlc = getcontext(theory, AlgSort(tc.type)) + p = partition(retlc) + function r(choices) + sum(length.(choices)) == length(lc) || error(err) + r = Dict(k.lid => v.body.lid for (k,v) in + pairs(bind_localctx(GATContext(theory, lc), tc.type))) + idxs = map(getidents(retlc)) do x + r[x.lid].val # RELATE CHOICES OF TERMCON LC TO THAT OF TYPECON LC + end + card = index_nmi(getvalue(cards[AlgSort(tc.type)]), p, choices[idxs]) + card == 0 ? 0 : rand(1:card) # if codom is empty set, pick 0 + end + rand_nm(cards, theory, lc, Int[], r, Int) +end + + +""" Random matrix for some typescope with uniform sampling of `vals`. """ +function rand_nm(d::NMIs,t::GAT,lc::TypeScope, choices::Vector{Int}, + vals::AbstractVector{T}) where T + rand_nm(d, t, lc, choices, (_)->rand(vals), T) +end + +""" +Make a random NestedMatrix given the type scope for an AlgTypeConstructor. +`f` is a unary function of `choices` that returns a T +""" +function rand_nm(d::NMIs, theory::GAT, lc::TypeScope, + choices::Vector{Int}, f::Function, T::Type) + p = partition(lc) + plens = [0, cumsum(length.(p))...] + # Ranges of idxs in partition: e.g. p=[[1,2,4],[3,5],[7,6]] => [1:3,4:5,6:7] + ranges = [UnitRange(a+1,b) for (a,b) in zip(plens, plens[2:end])] + # Choices has decided values for some number of the partitions + i = findfirst(==(length(choices)), plens) + if i == length(p) + 1 # we have fully determined the whole context + NMI(f(choices)) # pick an element to go in the leaf cell + else + lens = map(LID.(ranges[i])) do idx + vs = sort(getvalue.(collect(vars(lc, idx)))) + idx_choices = choices[vs] + Base.OneTo(length(enum(d, theory, subscope(lc,idx), idx_choices))) + end + NMI(Nest(Array{NestedMatrix{T}}(map(Iterators.product(lens...)) do idx + rand_nm(d, theory, lc, [choices...,idx...], f, T) + end)); depth = length(p) - i + 1) + end +end + +""" +Given a mapping of AlgSorts to cardinalities, e.g. (where we give arbitrary names) +Ob = [a,b] Hom(1,1) = [c] Hom(2,1) = [] Hom(1,2) = [d,e] Hom(2,2) = [f,g] + +Determine a cardinality in a context, e.g. |f| ⊣ [a::Ob, f::Hom(a,a)] + +This example would result in: `[1, 1], [2, 1], [2, 2]` + (i.e. `[a, c], [b, f], [b, g]`) +""" +function enum(cardinalities::NMIs, theory::GAT, ctx::TypeScope, init=Int[]) + queue = Vector{Int}[init] + res = Vector{Int}[] + while !isempty(queue) + curr = popfirst!(queue) + if length(curr) == length(ctx) + push!(res, curr) + else + typ = getvalue(ctx[LID(length(curr)+1)]) + s = AlgSort(typ) + bound = bind_localctx(GATContext(theory, ctx), typ) + rep = Dict(k.lid => v.body.lid for (k,v) in pairs(bound)) + p = Vector{Vector{LID}}(map(partition(getcontext(theory, s))) do seg + LID[rep[x] for x in seg] # need to reindex into ctx + end) + idx = index_nmi(getvalue(cardinalities[s]), p, curr) + news = [[curr..., i] for i in 1:idx] + append!(queue, news) + end + end + res +end + +""" +A NestedMatrix has been constructed with a particular type scope (and partition +of the type scope) in mind. Given that partition (and choices of indices for each +dimension), access an element of the NestedMatrix. +""" +function index_nmi(nmi::NestedMatrix{T}, p::Vector{Vector{LID}}, + idx::Vector{Int}; depth::Int=0)::T where T + depth+length(p) == nmi.depth || error("Bad indexing length $p vs $(nmi.depth)") + for seg in p + nmi = getvalue(getvalue(nmi))[idx[getvalue.(seg)]...] + end + nmi.depth == depth || error("Bad nmi $nmi") # sanity check + getvalue(nmi) +end + + +# Modify cardinalities +###################### + +""" +If we naively add a part to some set, there may be sets which +depend on the set which has been extended, so empty sets need to be created for +all of these. E.g. if Ob=[1,2] and H11=[1], H12=[], H21=[1,2], H22[1]. +If we add 3 to Ob, then we need to create H13=[], H31=[], H12=[], H32=[], H33=[]. + +Furthermore, new function arguments become possible, and the default value of +the function is 0. + +This implementation creates modified NestedMatrices and then replaces the ones +in the CombinatorialModel. A more sophisticated algorithm would do this in place. +""" +function add_part!(m::CombinatorialModel, + type::NestedType=NestedType())::NestedTerm + T = gettheory(m) + enums = Dict(s => collect(m[s]) for s in sorts(T)) # store for later + new_cardinality = getvalue(m[type]) + 1 + m[type] = NMI(new_cardinality) + for s in sorts(T) + getsort(type) ∈ sortsignature(getvalue(T, methodof(s))) || continue + tc = getcontext(T, s) + new_nm = rand_nm(m.sets, T, tc, Int[], [0]) # all empty sets + for (e, val) in enums[s] # copy over old data + new_nm[e] = NMI(val) + end + m[s] = new_nm + end + for s in funsorts(T) + new_fun = random_function(m.sets, T, s) + for (e, v) in m[s] # copy over old data + new_fun[e] = NMI(v) + end + m[s] = new_fun + end + NestedTerm(new_cardinality, type) +end + +""" +Remove an element of a dependent set, specified by a NestedTerm. This has an +effect on any sets dependent on that element. Removal involves pop-and-swap. + +This implementation creates modified NestedMatrices and then replaces the ones +in the CombinatorialModel. A more sophisticated algorithm would do this inplace. +""" +function rem_part!(m::CombinatorialModel, term::NestedTerm) + T = gettheory(m) + type = argsof(term) + swapped_index = getvalue(m[type]) + m[type] = NMI(swapped_index - 1) + for s in sorts(T) + getsort(type) ∈ sortsignature(getvalue(T, methodof(s))) || continue + new_nm = rand_nm(m.sets, T, getcontext(T, s), Int[], [0]) # all empty sets + for (e, _) in new_nm + e = NestedType(s, e) + new_e = deepcopy(e) + for (i, subterm) in enumerate(subterms(T, e)) + if subterm == term + new_e[i] = swapped_index + end + end + new_nm[e] = m[s][new_e] + end + m[s] = new_nm + end + for s in funsorts(T) + new_fun = random_function(m.sets, T, s) + for (e, _) in new_fun # copy over old data + e = NestedType(s, e) + new_e = deepcopy(e) + for (i, subterm) in enumerate(subterms(T, e)) + if subterm == term + new_e[i] = swapped_index + end + end + val = m(new_e) + new_fun[e] = (val == term ? swapped_index : getvalue(val)) |> NMI + end + m[s] = new_fun + end +end + +""" +Convert a "NestedType" with a term constructor sort to an actual NestedTerm +by evaluating. E.g. compose[[1,4,5],[3,2]] => Hom[[1,5]]#4 via looking up in the +compose table the value (4) and inferring the result type parameters. +""" +function (m::CombinatorialModel)(term::NestedType)::NestedTerm + T = gettheory(m) + srt = getsort(term) + rtype = getvalue(T[methodof(srt)]).type + rsort = AlgSort(rtype) + lc = bind_localctx(GATContext(T, getcontext(T, srt)), rtype) + flat_idxs = map(sort(collect(pairs(lc)); by=x->getvalue(x[1].lid))) do (_,b) + GATs.isvariable(b) ? term[getvalue(b.body.lid)] : error("Bad ret type $b") + end + idxs = repartition_idx(T, rsort, flat_idxs) + NestedTerm(getvalue(m[term]), NestedType(rsort, idxs)) +end + +# Enforce equations +################### + +"""Merely enforce equalities implied by equations of GAT via chase""" +function eq_saturate!(m::CombinatorialModel) + error("NOT IMPLEMENTED YET") +end + +""" +Enforce equalities implied by equations of GAT via chase as well as create new +elements of dependent sets for every undefined function output. This process +can potentially not terminate. + +Returns a boolean indicating whether or not the process terminated and an +integer describing how many steps it took. +""" +function saturate!(m::CombinatorialModel; steps::Int=100) + for step in 1:steps + eq_saturate!(m) + error("NOT IMPLEMENTED YET") + # ... && return (true, step) + end + false, steps +end + +is_saturated(m::CombinatorialModel) = last(saturate!(m)) == 0 + +end # module diff --git a/src/combinatorial/DataStructs.jl b/src/combinatorial/DataStructs.jl new file mode 100644 index 00000000..0dc58404 --- /dev/null +++ b/src/combinatorial/DataStructs.jl @@ -0,0 +1,536 @@ +module DataStructs +export NestedMatrix, CombinatorialModel, CombinatorialModelMorphism, + NestedType, NestedTerm, CombinatorialModelC, is_natural, getsort + +using StructEquality + +using ...Syntax +import ...Syntax: getvalue, AlgSort, argsof, headof, gettheory, getcontext +using ...Syntax.TheoryMaps: bind_localctx +using ...Models +using ...Stdlib +using ..TypeScopes: partition, repartition, repartition_idx + +# Nested Matrices +################# +abstract type AbsNest{T} end # to resolve mutually-recursive structs. + +""" +The shape of the nested matrices depends on the indices of the outer matrix, +though the depth of the nested matrices are always the same. Furthermore the +dimensionality is consistent for every level of depth. + +- `T` is the type at the very end of the nesting, which we call a "leaf". +- `depth` parameter is used for runtime sanity check. + +In principle, this data structure is independent of GATs, but in practice each +NestedMatrix has an associated TypeScope which gives meaning to the indices. +See `ScopedNM`. +""" +@struct_hash_equal mutable struct NestedMatrix{T} + data::Union{T, AbsNest{T}} + const depth::Int + + """Create a leaf matrix""" + NestedMatrix{T}(data::T) where T = new{T}(data, 0) + + """Non-leaf matrix. Caller must manually provide depth if `data` is empty""" + function NestedMatrix{T}(data::AbsNest{T}; depth = nothing) where T + depth = isnothing(depth) ? (first(data).depth + 1) : depth + depths = (m -> m.depth).(getvalue(data)) # depths of all matrices one level below + if all(==(depth - 1), depths) + sizes = depth == 1 ? Int[] : size.(getvalue.(data)) + err = "Not all submatrices have the same dimensionality: $sizes" + length(unique(length.(sizes))) <= 1 || error(err) + new{T}(data, depth) + else + error("Bad depths $depths != $(depth - 1)") + end + end +end + +const NM = NestedMatrix + +@struct_hash_equal struct Nest{T} <: AbsNest{T} + val::Array{NM{T}} # array of nested matrices +end + +Base.size(n::Nest{T}) where T = size(getvalue(n)) + +Base.length(n::Nest{T}) where T = length(getvalue(n)) + +Base.iterate(n::Nest{T}) where T = iterate(getvalue(n)) + +Base.iterate(n::Nest{T}, i) where T = iterate(getvalue(n), i) + +Base.first(n::Nest{T}) where T = first(getvalue(n)) + +Base.getindex(n::Nest{T}, i) where T = getindex(getvalue(n), i) + +Base.setindex!(n::Nest{T}, i, k) where T = setindex!(getvalue(n), i, k) + +Base.CartesianIndices(n::Nest{T}) where T = CartesianIndices(getvalue(n)) + +function getvalue(n::Nest{T})::Array{NM{T}} where T + n.val +end + +Base.length(nm::NM)::Int = + (nm.depth == 0) ? 1 : sum(length.(getvalue(getvalue(nm))); init=0) + +getvalue(nm::NM) = nm.data + +const Idx = CartesianIndex + +"""Access a submatrix (not necessarily a leaf) of a NestedMatrix""" +function Base.getindex(nm::NM{T}, idx::Vector{<:Idx})::NM{T} where T + res = nm + for i in idx + res = res.data[i] + end + res +end + +function Base.setindex!(nm::NM{T}, data::NM{T}, idx::Vector{<:Idx}) where T + if isempty(idx) + # TODO if this is not depth=0, need to delete all elems of array, then add + nm.depth == data.depth == 0 || error("Bad depth") + nm.data = data.data + else + init_indices..., last_index = idx + nm[init_indices].data[last_index] = data + end +end + +""" +Get a canonical NestedMatrix which just has the branching structure, ignoring +the data on the leaves. +""" +shape(nm::NM)::NM{Nothing} = const_nm(nm, nothing) + +""" Replace all leaves with a constant value. Optionally deepcopy that value """ +function const_nm(nm::NM, v::T; copy=false)::NM{T} where T + map_nm(_ -> (copy ? deepcopy : identity)(v), T, nm) +end + +""" +Map a function over the leaf values of a NestedMatrix, returning one of +identical shape. This must be a unary function (operating on the leaf value) +unless `index=true`, in which case it must accept an argument for the nesting +index as well as the leaf value. +""" +function map_nm(fun, ret_type::Type, nm::NM; index=false, curr=Idx[]) + if nm.depth == 0 + elem::ret_type = index ? fun(curr, nm.data) : fun(nm.data) + NM{ret_type}(elem) + else + res = Array{NM{ret_type}}(undef, size(nm.data)...) + for I in CartesianIndices(res) + res[I] = map_nm(fun, ret_type, getvalue(nm.data)[I]; index, curr=[curr..., I]) + end + NestedMatrix{ret_type}(Nest(res); depth=nm.depth) + end +end + +Base.eltype(::Type{NestedMatrix{T}}) where T = Pair{Vector{<:Idx}, T} + +Base.IteratorSize(::Type{<:NestedMatrix}) = Base.SizeUnknown() + +""" +Get all the leaves of a NestedMatrix along with their coordinate indices. + +The iterator navigates the nested matrix with a state consisting of the current +position in the indexing and a boolean representing whether we should move down +(descend in depth, if true) or across (to the next index at the same depth, if +false). The algorithm is a depth-first search. +""" +function Base.iterate(nm::NestedMatrix{T}, state=(true => Idx[])) where T + down, idxs = state + curr = nm[idxs] + if down + if curr.depth == 0 + return (idxs => curr.data, false => idxs) + else + next_inds = CartesianIndices(curr.data) + if isempty(next_inds) + iterate(nm, false => idxs) + else + iterate(nm, true => [idxs..., first(next_inds)]) + end + end + else + if isempty(idxs) + return nothing + else + prev_idxs = idxs[1 : end-1] + prev = nm[prev_idxs] + nxt = iterate(CartesianIndices(prev.data), last(idxs)) + if isnothing(nxt) + iterate(nm, false => prev_idxs) + else + return iterate(nm, true => [prev_idxs..., first(nxt)]) + end + end + end +end + +Base.sum(nm::NestedMatrix) = sum(getvalue.(nm.data)) # total sum of leaves + + +"""A NestedMatrix with a TypeScope to make sense of the indexing""" +@struct_hash_equal struct ScopedNM{T} + val::NM{T} + ts::TypeScope + partition::Vector{Vector{LID}} + function ScopedNM(val::NM{T}, ts::TypeScope) where T + new{T}(val, ts, partition(ts)) + end +end + +getvalue(s::ScopedNM) = s.val + +getcontext(s::ScopedNM) = s.ts + +shape(s::ScopedNM) = shape(getvalue(s)) + +Base.sum(s::ScopedNM) = sum(getvalue(s)) + +Base.length(s::ScopedNM{T}) where T = length(getvalue(s)) + +Base.iterate(s::ScopedNM{T}) where T = iterate(getvalue(s)) + +Base.iterate(s::ScopedNM{T}, i) where T = iterate(getvalue(s), i) + +Base.getindex(n::ScopedNM{T}, i) where T = getindex(getvalue(n), i) + +Base.setindex!(n::ScopedNM{T}, i, k) where T = setindex!(getvalue(n), i, k) + +map_nm(fun, ret_type, nm::ScopedNM; kw...) = + ScopedNM(map_nm(fun, ret_type, getvalue(nm); kw...), getcontext(nm)) + +const_nm(n::ScopedNM, v; copy=false) = + ScopedNM(const_nm(getvalue(n), v; copy), getcontext(n)) + +const AlgDict{T} = Dict{AlgSort, NM{T}} + +@struct_hash_equal struct ScopedNMs{T} + val::Dict{AlgSort, ScopedNM{T}} +end + +function ScopedNMs(theory::GAT, xs::AlgDict{T}) where T + ScopedNMs{T}(Dict(k=>ScopedNM(v, getcontext(theory, k)) for (k,v) in pairs(xs))) +end + +function ScopedNMs{T}() where T + ScopedNMs{T}(Dict{AlgSort, ScopedNM{T}}()) +end + +getvalue(s::ScopedNMs{T}) where T = s.val + +Base.getindex(s::ScopedNMs{T}, i) where T = getvalue(s)[i] + +Base.keys(s::ScopedNMs{T}) where T = keys(getvalue(s)) + +Base.length(s::ScopedNMs{T}) where T = length(getvalue(s)) + +Base.setindex!(s::ScopedNMs{T}, i, k) where T = setindex!(getvalue(s), i, k) + +Base.iterate(s::ScopedNMs{T}) where T = iterate(getvalue(s)) + +Base.iterate(s::ScopedNMs{T}, i) where T = iterate(getvalue(s), i) + +Base.haskey(s::ScopedNMs{T}, k::AlgSort) where T = haskey(getvalue(s), k) + +Base.get(s::ScopedNMs{T}, k, v) where T = get(getvalue(s), k, v) + +const NMI = NM{Int} + +const NMVI = NM{Vector{Int}} + +const NMIs = ScopedNMs{Int} + +const NMVIs = ScopedNMs{Vector{Int}} + +# Nested Types and Terms +######################## + +abstract type Nested end + +""" +Effectively picks out a dependent set from a typescope which has been +partitioned into levels (by `partition`). E.g. Hom2[[2,3],[5,1]] means +Hom2(Hom#5(Ob#2 => Ob#3), Hom#1(Ob#2 => Ob#3)). +""" +@struct_hash_equal struct NestedType <: Nested + s::AlgSort + val::Vector{Idx} + lookup::Vector{Pair{Int,Int}} # cached mapping for linear indexing + NestedType(s,v=Idx[]) = new(s,v,make_lookup(v)) +end + +NestedType(s, vs::Vector{Vector{Int}}) = NestedType(s, [Idx(v...) for v in vs]) + +"""How to interpret a list of lists as a flat list""" +function make_lookup(xs)::Vector{Pair{Int,Int}} + res = Pair{Int,Int}[] + for (i, x) in enumerate(xs) + for j in 1:length(x.I) + push!(res, i => j) + end + end + res +end + +getvalue(nestedtype::NestedType) = nestedtype.val + +getsort(n::NestedType)::AlgSort = n.s # type inference fails if we extend AlgSort?! + +Base.getindex(nm::NestedMatrix, idx::NestedType) = nm[getvalue(idx)] + +Base.setindex!(nm::NestedMatrix, data::NestedMatrix, idx::NestedType) = + setindex!(nm, data, getvalue(idx)) + +Base.length(n::NestedType) = length(n.lookup) + +function Base.getindex(typ::NestedType, i::Int) + (x, y) = typ.lookup[i] + getvalue(typ)[x][y] +end + +function Base.setindex!(typ::NestedType, idx::Int, i::Int) + (x, y) = typ.lookup[i] + new_idx = [y == j ? idx : val for (j, val) in enumerate(getvalue(typ)[x].I)] + getvalue(typ)[x] = CartesianIndex(new_idx...) +end + +"""Picks out an *element* of a dependent set (which is now assumed to be 1:n).""" +@struct_hash_equal struct NestedTerm <: Nested + val::Int + args::NestedType +end + +getvalue(nestedterm::NestedTerm) = nestedterm.val + +argsof(nestedterm::NestedTerm)::NestedType = nestedterm.args + +getsort(n::NestedTerm)::AlgSort = getsort(argsof(n)) + +Base.getindex(nm::NestedMatrix{Vector{T}}, idx::NestedTerm) where T = + getvalue(nm[argsof(idx)])[getvalue(idx)] + +function Base.setindex!(nm::NMVI, data::Int, idx::NestedTerm) + getvalue(nm[argsof(idx)])[getvalue(idx)] = data +end + +""" +Helper function for `subterms`. + +Suppose we have indices corresponding to elements of a typescope, e.g. +Hom#2[1,2,3,4] (representing the third Hom2 between Hom#3(Ob#1=>Ob#2) and +Hom#4(Ob#1=>Ob#2)). We return [[], [], [1,2], [1,2] ] +""" +function sub_indices(theory::GAT, lc::TypeScope)::Vector{Vector{Int}} + map(1:length(lc)) do i + type = getvalue(lc[LID(i)]) + bound = bind_localctx(GATContext(theory, lc), type) + map(getidents(getcontext(theory, AlgSort(type)))) do j + if GATs.isvariable(bound[j]) + return bound[j].body.lid.val + else + error("$j: non var $(bound[j]) ") + end + end + end +end + +sub_indices(theory::GAT, s::AlgSort) = sub_indices(theory, getcontext(theory, s)) + +""" +A nested term like Hom2[1,3,2,1]#3 (i.e. the third Hom2 between +Hom#2(Ob#1=>Ob#3) and Hom#1(Ob#1=>Ob#3)) produces a vector [Ob[]#1, Ob[]#3, +Hom[2,1]#2, Hom[2,1]#1] +""" +function subterms(theory::GAT, trm::Nested)::Vector{NestedTerm} + typ = trm isa NestedTerm ? argsof(trm) : trm + ctx = getcontext(theory, getsort(trm)) + sub_inds = sub_indices(theory, ctx) + map(1:length(ctx)) do i + arg_srt = AlgSort(getvalue(ctx[LID(i)])) + arg_localctx = getcontext(theory, arg_srt) + part_subs = repartition(arg_localctx, sub_inds[i]) + arg_typ = NestedType(arg_srt, map(part_subs) do subs + CartesianIndex([typ[x] for x in subs]...) + end) + NestedTerm(typ[i], arg_typ) + end +end + +# Models +######## + +""" +A cardinality for each (dependent) set and a family of functions for each term +constructor. + +One might be tempted to call this a GATset. +""" +@struct_hash_equal struct CombinatorialModel + theory::GAT + sets::NMIs + funs::NMIs + function CombinatorialModel(t, s=NMIs(), f=NMIs()) + s, f = [sf isa NMIs ? sf : ScopedNMs(t, sf) for sf in [s,f]] + Set(keys(s)) == Set(sorts(t)) || error("Bad sort keys $s") + Set(keys(f)) == Set(funsorts(t)) || error("Bad fun keys $s") + new(t, s, f) + end +end +const Comb = CombinatorialModel +gettheory(c::Comb) = c.theory + +Base.getindex(m::Comb, s::AlgSort) = if haskey(m.sets,s) + m.sets[s] +elseif haskey(m.funs, s) + m.funs[s] +else + throw(KeyError(s)) +end + +function Base.setindex!(m::Comb, n::NMI, s::AlgSort) + val = ScopedNM(n, getcontext(m.theory, s)) + if haskey(m.sets,s) + m.sets[s] = val + elseif haskey(m.funs, s) + m.funs[s] = val + else + throw(KeyError(s)) + end +end + +Base.getindex(m::Comb, t::NestedType) = m[getsort(t)][t] + +Base.getindex(m::ScopedNMs, t::Nested) = m[getsort(t)][t] + +function Base.setindex!(m::ScopedNMs, val, t::Nested) + m[getsort(t)][t] = val +end + +Base.setindex!(m::Comb, data::NMI, t::NestedType) = + m.sets[getsort(t)][getvalue(t)] = data + +function random_cardinalities end # defined in CModels + +""" +Make sure cardinalities are consistent with each other and that function values +are defined (nonzero) and within bounds. +""" +function validate(c::Comb) + T = gettheory(c) + init = Dict{AlgSort, NMI}() #NMIs() + for s in sorts(T) + initdict = Dict{AlgSort, NMI}(k=>get(init, k, NMI(0)) for k in sorts(T) if k != s) + r = random_cardinalities(T; init=initdict)[s] # generate a random one + shape(c.sets[s]) == shape(r) || return false + init[s] = getvalue(c.sets[s]) + end + for (funsort, vs) in c.funs + for (e, v) in collect(vs) + retterm = c(NestedType(funsort, e)) + max = getvalue(c.sets[getsort(retterm)][argsof(retterm)]) + 0 < v ≤ max || return false + end + end + true +end + +"""Mapping for each TypeConstructor""" +@struct_hash_equal struct CombinatorialModelMorphism + components::NMVIs + dom::Comb + codom::Comb + function CombinatorialModelMorphism(c, d, cd) + c = c isa NMVIs ? c : ScopedNMs(gettheory(d), c) + gettheory(d) == gettheory(cd) || error("Theory mismatch") + new(c, d, cd) + end +end + +const Morphism = CombinatorialModelMorphism + +Base.getindex(c::Morphism, k) = components(c)[k] + +gettheory(c::Morphism) = gettheory(c.dom) + +components(c::Morphism) = c.components + +function (f::Morphism)(t::NestedType)::NestedType + T, srt = gettheory(f), getsort(t) + NestedType(srt, repartition_idx(T, srt, Int[getvalue.(f.(subterms(T, t)))...])) +end + +function (f::Morphism)(t::NestedTerm)::NestedTerm + NestedTerm(components(f)[getsort(t)][t], f(argsof(t))) +end + +function is_natural(m::Morphism) + T = gettheory(m) + for (funsort, nestedmatrix) in m.dom.funs + for (idx, _) in collect(nestedmatrix) + # apply operation, then map over morphism + dom_funapp = NestedType(funsort, idx) + dom_funres = m.dom(dom_funapp) + op_f = m(dom_funres) + # map arguments to operation over morphism, then apply operation + cod_idxs = getvalue.(m.(subterms(T, dom_funapp))) + cod_funapp = NestedType(funsort, repartition_idx(T, funsort, cod_idxs)) + f_op = m.codom(cod_funapp) + op_f == f_op || return false + end + end + true +end + +# Category instance +################### + +# For now, at least, the theory is run-time data. +@struct_hash_equal struct CombinatorialModelC <: Model{Tuple{Comb, Morphism}} + theory::GAT +end + +@instance ThCategory{Comb, Morphism} [model::CombinatorialModelC] begin + function Ob(n::Comb) + model.theory == n.theory || @fail "Model theory mismatch" + validate(n) || @fail "Failed validation" + n + end + function Hom(f::Morphism, A::Comb, B::Comb) + ThCategory.dom[model](f) == A || @fail "bad domain $A" + ThCategory.codom[model](f) == B || @fail "bad codomain $B" + is_natural(f) || @fail "unnatural" + f + end + + id(n::Comb) = Morphism(Dict(map(collect(n.sets)) do (k,v) + k => map_nm(i->collect(1:i), Vector{Int}, getvalue(v)) + end), n, n) + + function compose(f::Morphism, g::Morphism) + Morphism(Dict(map(collect(components(f))) do (k, fk) + b = f.codom + g.dom == b || error("Cannot compose $f and $g") + function fun(idx::Vector{<:Idx}, vs::Vector{Int})::Vector{Int} + map(1:length(vs)) do i + b_term = NestedTerm(i, NestedType(k, idx)) + components(g)[f(b_term)] + end + end + k => map_nm(fun, Vector{Int}, getvalue(fk); index=true) + end), f.dom, g.codom) + end + + dom(A::Morphism) = A.dom + codom(A::Morphism) = A.codom +end + +end # module diff --git a/src/combinatorial/HomSearch.jl b/src/combinatorial/HomSearch.jl new file mode 100644 index 00000000..f16720d2 --- /dev/null +++ b/src/combinatorial/HomSearch.jl @@ -0,0 +1,347 @@ +module HomSearch +export homomorphism, homomorphisms + +using StructEquality + +using ..TypeScopes: partition, repartition +using ..DataStructs +using ..DataStructs: map_nm, sub_indices, subterms, getsort, Comb, + NM, NMI, NMIs, NMVI, NMVIs, const_nm, ScopedNMs +using ...Syntax +using ..Visualization +import ...Syntax: gettheory, argsof + +""" Find a homomorphism between two attributed Combinatorial Models. + +Returns `nothing` if no homomorphism exists. The +homomorphism problem is NP-complete and thus this procedure generally +runs in exponential time. It works best when the domain object is small. +""" +function homomorphism(X::Comb, Y::Comb; kw...) + result = nothing + backtracking_search(X, Y; kw...) do α + result = α; return true + end + result +end + +""" Find all homomorphisms between two attributed ``C``-sets. + +This function is at least as expensive as [`homomorphism`](@ref) and when no +homomorphisms exist, it is exactly as expensive. +""" +function homomorphisms(X::Comb, Y::Comb; kw...) + results = CombinatorialModelMorphism[] + backtracking_search(X, Y; kw...) do α + push!(results, deepcopy(α)); return false + end + results +end + +# Backtracking search +#-------------------- +const Maybe{T} = Union{Nothing, T} + +""" Internal state for backtracking search for CombinatorialModel homomorphisms. + +Assignment of attribute variables maintains both the assignment as well as the +number of times that variable has been bound. We can only *freely* assign the +variable to match any AttrVar or concrete attribute value if it has not yet +been bound. +""" +@struct_hash_equal struct BacktrackingState + assignment::NMVIs + assignment_depth::NMVIs + inv_assignment::ScopedNMs{NMVI} + refcounts::ScopedNMs{NMVI} + unassigned::NMIs + dom::Comb + codom::Comb +end + +gettheory(b::BacktrackingState) = b.dom.theory + +function Base.show(io::IO, m::MIME"text/plain", s::BacktrackingState) + for (k, v) in s.assignment + println(io, k) + show(io, m, v) + end +end +Base.string(n::BacktrackingState) = sprint(show, MIME"text/plain"(), n) + +""" +Allow opt-in constraints via `monic`/`epic`/`iso` kwargs. By default these are +on the basis of each dependent set, so an iso constraint on Hom would mean that +each Hom set is isomorphic to the hom set it is mapped to. Future work could +include a constraint which could require domain ⨿Hom to be in bijection with +codomain ⨿Hom. + +Future work is to allow finer granularity specification than the AlgSort level, +e.g. Hom-Sets 1=>1 and 1=>2 are epic and Hom-Sets 2=>1 and 2=>2 are monic, etc. + +Then `inv_assignment`s would have type NestedMatrix{Union{Nothing, Vector{Int}}} +""" +function normalize_monic_epic_iso(monic::Union{Bool, AbstractVector}, + epic::Union{Bool, AbstractVector}, + iso::Union{Bool, AbstractVector}, + theory::GAT + )::Tuple{Vector{AlgSort},Vector{AlgSort}} + Tsorts = sorts(theory) + to_sort(s::Union{AlgSort, Symbol}) = s isa AlgSort ? s : AlgSort(theory, s) + if iso == true + return (Tsorts, Tsorts) + else + m, e = map([monic, epic]) do mono_epi + if mono_epi isa Bool + (mono_epi ? copy(Tsorts) : AlgSort[]) + else + to_sort.(mono_epi) + end + end + if iso != false + append!.([m,e], Ref(to_sort.(iso))) + end + (m, e) + end +end + +getinitial(::Comb, ::Comb, ::Nothing) = Pair{NestedTerm, NestedTerm}[] + +"""An assignment (for each nonzero vector element) for all elements""" +function getinitial(X::Comb, Y::Comb, xys::NMVIs) + m = CombinatorialModelMorphism(xys, X, Y) + res = Pair{NestedTerm, NestedTerm}[] + for s in sorts(gettheory(X)) + for (idx, vals) in get(xys, s, []) + xtype = NestedType(s, idx) + for xᵢ in 1:length(vals) + x = NestedTerm(xᵢ, xtype) + push!(res, x => m(x)) + end + end + end + res +end + +getinitial(::Comb, ::Comb, x::AbstractVector{Pair{NestedTerm, NestedTerm}}) = x + +function backtracking_search(f, X::Comb, Y::Comb; monic=false, epic=false, + iso=false, initial=nothing) + X.theory == Y.theory || error("Theories must match for morphism search") + T = X.theory + + monic, epic = normalize_monic_epic_iso(monic, epic, iso, T) + # TODO: constraint asserting a constraint across all elements of a sort + # sort_monic, sort_epic = normalize_monic_epic_iso(monic′, epic′, iso′, T) + + # Initialize state variables for search. + assignment = NMVIs(Dict(c=>map_nm(i->zeros(Int,i), Vector{Int}, X.sets[c]) + for c in sorts(T))) + assignment_depth = deepcopy(assignment) + + nmvis(c) = const_nm(getvalue(X.sets[c]), map_nm(i->zeros(Int, i), Vector{Int}, + getvalue(Y.sets[c])); copy=true) + inv_assgn = ScopedNMs(T, Dict{AlgSort,NM{NMVI}}(c => nmvis(c) for c in monic)) + refcounts = ScopedNMs(T, Dict{AlgSort,NM{NMVI}}(c => nmvis(c) for c in epic)) + + unassigned = NMIs(Dict(c => deepcopy(X.sets[c]) for c in epic)) + + state = BacktrackingState(assignment, assignment_depth, inv_assgn, + refcounts, unassigned, X, Y) + + # Make any initial assignments, failing immediately if inconsistent. + for (x, y) in getinitial(X, Y, initial) + assign_elem!(state, 0, x, y) || return false + end + # Start the main recursion for backtracking search. + backtracking_search(f, state, 1) +end + +function backtracking_search(f, state::BacktrackingState, depth::Int) + # Choose the next unassigned element. + mrv, x = find_mrv_elem(state, depth) + if isnothing(x) + # No unassigned elements remain, so we have a complete assignment. + return f(CombinatorialModelMorphism(state.assignment, state.dom, state.codom)) + elseif isempty(mrv) + # An element has no allowable assignment, so we must backtrack. + return false + end + + # Iterate through all valid assignments of the chosen element. + for y in mrv + @assert assign_elem!(state, depth, x, y) # find_mrv_elem checks assignment + backtracking_search(f, state, depth + 1) && return true + unassign_elem!(state, depth, x) + end + return false +end + +""" Find an unassigned element having the minimum remaining values (MRV). +""" +function find_mrv_elem(state::BacktrackingState, depth::Int) + T = gettheory(state) + mrv, remaining_values, mrv_elem = Inf, NestedTerm[], nothing + Y = state.codom + for c in sorts(T), (depsₓ, depset) in state.assignment[c] + for (xval, y) in enumerate(depset) + y == 0 || continue + x = NestedTerm(xval, NestedType(c, depsₓ)) + success = [] + for (depsᵧ, yvals) in Y.sets[c] + for yval in 1:yvals + y = NestedTerm(yval, NestedType(c, depsᵧ)) + if can_assign_elem(state, depth, x, y) + push!(success, y) + end + end + end + if length(success) < mrv + mrv, remaining_values, mrv_elem = length(success), success, x + end + end + end + (remaining_values, mrv_elem) +end + +""" Check whether element (c,x) can be assigned to (c,y) in current assignment. +""" +function can_assign_elem(state::BacktrackingState, depth::Int, x::NestedTerm, y::NestedTerm) + # Although this method is nonmutating overall, we must temporarily mutate the + # backtracking state, for several reasons. First, an assignment can be a + # consistent at each individual subpart but not consistent for all subparts + # simultaneously (consider trying to assign a self-loop to an edge with + # distinct vertices). Moreover, in schemas with non-trivial endomorphisms, we + # must keep track of which elements we have visited to avoid looping forever. + save_state′ = deepcopy(state) + ok = assign_elem!(state, depth, x, y) + unassign_elem!(state, depth, x) + for f in fieldnames(Comb) + fa, fb = getfield.([save_state′.dom,state.dom], Ref(f)) + fa == fb || error("$f: \n$fa \n!= \n$fb") + end + save_state′ == state || error("Unassign x$(string(x))↦y$(string(y)) doesn't undo assign \n$(string(save_state′))\n\n$(string(state))") + + return ok +end + +""" Attempt to assign element (c,x) to (c,y) in the current assignment. + +Returns whether the assignment succeeded. Note that the backtracking state can +be mutated even when the assignment fails. +""" + +function assign_elem!(state::BacktrackingState, depth::Int, x::NestedTerm, y::NestedTerm) + c = getsort(x) + c == getsort(y) || error("Mismatched sorts $c $(getsort(y))") + y′ = state.assignment[x] + sts = subterms(gettheory(state), x) + ysts = [state.assignment[getsort(st)][st] for st in sts] + ctx = getcontext(gettheory(state), c) + yidxs = [CartesianIndex(i...) for i in repartition(ctx, ysts)] + y′term = NestedTerm(y′, NestedType(c, yidxs)) + y′term == y && return true # If x is already assigned to y, return immediately. + y′ == 0 || return false # Otherwise, x must be unassigned. + if haskey(state.inv_assignment, c) + if getvalue(state.inv_assignment[argsof(x)])[y] != 0 + return false # Also, y must unassigned in the inverse assignment. + end + end + # With an epic constraint, fail based on the # of unassigned in dom vs codom + if haskey(state.refcounts, c) + # Number of free values in x's set (X) we have remaining to fill y's set (Y) + unassigned = getvalue(state.unassigned[argsof(x)]) + # How many elements of X are pointing at each element in Y + refcounts = getvalue(state.refcounts[argsof(x)])[argsof(y)] |> getvalue + # How many elements of Y have nothing pointing at them from X. + # (ignore y, as this value is about to be assigned to by x) + to_assign = count(((i, rc),)-> i!=y′ && rc==0, enumerate(refcounts)) + if unassigned < to_assign + return false + end + end + # Set dependent set values based on type constructor arguments + for (subX, subY) in zip(subterms.(Ref(gettheory(state)), [x,y])...) + assign_elem!(state, depth, subX, subY) || return false + end + + # Make the assignment and recursively assign subparts. + state.assignment[x] = getvalue(y) + state.assignment_depth[x] = depth + if haskey(state.inv_assignment, c) + inv = getvalue(state.inv_assignment[argsof(x)]) + inv[y] = getvalue(x) + end + if haskey(state.refcounts, c) + xcounts = getvalue(state.refcounts[argsof(x)]) + xunassgn = state.unassigned[argsof(x)] + xcounts[y] += 1 + xunassgn.data = xunassgn.data - 1 + end + + # Set other values based on term constructor naturality constraints + for (funsort, fun_data) in state.dom.funs + for (dom_deps, _) in fun_data # check, for each combination of args: + valX_expr = NestedType(funsort, dom_deps) + valX = state.dom(valX_expr) + sts = subterms(gettheory(state), valX_expr) + any(==(x), sts) || continue # only if the term we just set is an arg + ysts = [state.assignment[getsort(st)][st] for st in sts] + any(==(0), ysts) && continue # only if all args of this f(...) are defined + yidxs = [CartesianIndex(i...) for i in repartition(length.(dom_deps), ysts)] + valY = state.codom(NestedType(funsort, yidxs)) + assign_elem!(state, depth, valX, valY) || return false + end + end + return true +end + +function (state::BacktrackingState)(x::NestedTerm) + sts = subterms(gettheory(state), x) + (y, ysts...) = ys = [state.assignment[getsort(st)][st] for st in [x, sts...]] + any(==(0), ys) && return nothing # only if all args are defined + lens = length.(partition(getcontext(gettheory(state), getsort(x)))) + yidxs = [CartesianIndex(i...) for i in repartition(lens, ysts)] + NestedTerm(y, NestedType(getsort(x), yidxs)) +end + +""" Unassign the element (c,deps,x) in the current assignment. +""" +function unassign_elem!(state::BacktrackingState, depth::Int, x::NestedTerm) + c = getsort(x) + y = state(x) + + for sub in subterms(gettheory(state), x) + unassign_elem!(state, depth, sub) + end + state.assignment[x] == 0 && return + + assign_depth = state.assignment_depth[x] + @assert assign_depth <= depth + assign_depth == depth || return + if haskey(state.inv_assignment, c) + getvalue(state.inv_assignment[argsof(x)])[y] = 0 + end + + if haskey(state.unassigned, c) + xcounts = getvalue(state.refcounts[argsof(x)]) + xunassgn = state.unassigned[argsof(x)] + xcounts[y] -= 1 + xunassgn.data = xunassgn.data + 1 + end + + state.assignment[x] = 0 + state.assignment_depth[x] = 0 + + for (funsort, fun_data) in state.dom.funs + for (deps, _) in fun_data + fx = NestedType(funsort, deps) + if x ∈ subterms(gettheory(state), fx) + fx_val = state.dom(fx) + unassign_elem!(state, depth, fx_val) + end + end + end +end + +end # module diff --git a/src/combinatorial/Limits.jl b/src/combinatorial/Limits.jl new file mode 100644 index 00000000..e67c9c37 --- /dev/null +++ b/src/combinatorial/Limits.jl @@ -0,0 +1,42 @@ +module Limits + +using ..DataStructs +using ..CModels +using ...Syntax + +initial(T::GAT) = CombinatorialModel(T; card_range=0:0) +terminal(T::GAT) = CombinatorialModel(T; card_range=1:1) + +""" +Pushout a span B <-f- A -g-> C. This is a stub for a function that will be written. + +This must be done iteratively for each sort, depending on the earlier sorts. + +A colimit of finite GAT models can itself be infinite. So we cannot expect +`saturate!` to terminate with the result. +""" +function pushout(f::CombinatorialModelMorphism, g::CombinatorialModelMorphism) + T = gettheory(f) + C = CombinatorialModelC(T) + A, B, C = dom[C](f), codom[C](f), codom[C](g) + A == dom[C](g) || error("Cannot pushout without common apex") + ι1, ι2 = NMVIs(), NMVIs() + init = NMIs() + for s in sorts(T) + init[s] = random_nm(init, T, getcontext(T, s),Int[],[0]) # initialize w/ zeros + for (idx, _) in init[s] + error("NotImplementedYet $s: $idx") + end + end + + for s in funsorts(s) + error("NotImplementedYet $s") + init[s] = NestedMatrix() + end + apex = CombinatorialModel(T; init) + (apex, Morphism(ι1, B, apex), Morphism(ι2, C, apex)) +end + +# TODO Implement ThPushout + +end # module \ No newline at end of file diff --git a/src/combinatorial/TypeScopes.jl b/src/combinatorial/TypeScopes.jl new file mode 100644 index 00000000..3f718ee4 --- /dev/null +++ b/src/combinatorial/TypeScopes.jl @@ -0,0 +1,76 @@ +module TypeScopes + +using ...Syntax + +# Managing TypeScopes +##################### +""" +Factor a dependent typescope into pieces which are independent. These chunks +become the different layers of the NestedMatrix. The groupings (though not ordering +within the groupings) should be independent +of the permutation of terms in the typescope. + +In other parts of the code (such as `repartition`) it's convenient to +assume that the values of the partition are strictly increasing, rather than +some permutation. This is not true in general and will have to be revised, but +for now a runtime check at the end makes sure this assumption holds. +""" +function partition(t::TypeScope)::Vector{Vector{LID}} + if length(t) == 0 return Vector{LID}[] end + res = [[LID(1)]] + for i in LID.(2:length(t)) + vs = vars(t, i) + intersects = findlast([!isempty(s ∩ vs) for s in res]) + if isnothing(intersects) + push!(res[1], i) + elseif intersects == length(res) + push!(res, [i]) + else + push!(res[intersects + 1], i) + end + end + flat = getvalue.(Iterators.flatten(res)) + sort(flat) == flat || error("Assumption of monotonic increase violated") + res +end + +"""Get all idents""" +vars(ts::TypeScope, t::AlgAST)::Set{LID} = vars(ts, t.body) +vars(ts::TypeScope, t::GATs.MethodApp)::Set{LID} = + union(Set{LID}(),vars.(Ref(ts), t.args)...) +vars(ts::TypeScope, t::Ident)::Set{LID} = + union(Set([t.lid]), vars(ts, getvalue(ts[t.lid]))) +vars(ts::TypeScope, i::LID)::Set{LID} = vars(ts, getvalue(ts[i])) + +function subscope(t::TypeScope, js::Vector{LID})::TypeScope + d = Dict{LID,LID}([j=>LID(i) for (i, j) in enumerate(js)]) + TypeScope(Binding{AlgType}[relid(d, t[j]) for j in js]; tag=gettag(t)) +end + +subscope(t::TypeScope, i::LID)::TypeScope = + subscope(t, LID[sort(collect(vars(t, i)); by=getvalue); i]) + +relid(t::Dict{LID, LID}, x) = error("HERE $t $x $(typeof(x))") +relid(t::Dict{LID, LID}, x::Binding) = setvalue(x, relid(t, getvalue(x))) +relid(t::Dict{LID, LID}, x::T) where T<:AlgAST = T(relid(t, bodyof(x))) +relid(t::Dict{LID, LID}, x::GATs.MethodApp{AlgTerm}) = + GATs.MethodApp{AlgTerm}(headof(x),methodof(x),relid.(Ref(t),argsof(x))) +relid(t::Dict{LID, LID}, x::Ident) = Ident(gettag(x), t[getlid(x)], nameof(x)) + + +""" +Take a vector corresponding to idents of a typescope and group them together +according to the partition +""" +repartition(ts::TypeScope, v) = repartition(length.(partition(ts)), v) + +repartition_idx(t::GAT, s::AlgSort, v::Vector{Int}) = + [CartesianIndex(x...) for x in repartition(getcontext(t, s), v)] + +""" lens = [3,3,2], v = [a,b,c,d,e,f,g,h] => [[a,b,c],[d,e,f],[g,h]] """ +function repartition(lens::Vector{Int}, v::Vector{T})::Vector{Vector{T}} where T + cs = zip([0, lens...] .+ 1, cumsum(lens)) + [v[i:j] for (i,j) in cs] +end + +end # module \ No newline at end of file diff --git a/src/combinatorial/Visualization.jl b/src/combinatorial/Visualization.jl new file mode 100644 index 00000000..8f0dc161 --- /dev/null +++ b/src/combinatorial/Visualization.jl @@ -0,0 +1,172 @@ +module Visualization + +export render, ScopedNM + +using ...Syntax +using ..DataStructs +using ..DataStructs: ScopedNM, Nest, Nested +using ..TypeScopes: partition +using PrettyTables, StructEquality +import ..DataStructs: getvalue +import ...Syntax: headof + +# Nested +######## + +function Base.show(io::IO, ::MIME"text/plain", nestedtype::NestedType) + print(io, "$(nameof(getsort(nestedtype)))[") + join(io, Tuple.(getvalue(nestedtype)), ",") + print(io, "]") +end + +function Base.show(io::IO, m::MIME"text/plain", nestedterm::NestedTerm) + show(io, m, argsof(nestedterm)) + print(io, "#$(getvalue(nestedterm))") +end + +Base.string(n::Nested) = sprint(show, MIME"text/plain"(), n) + +# NestedMatrix +############## +"""Visualize NestedMatrix using HTML""" +function render(nm::ScopedNM) + str = renderstr(nm) + f = tempname()*".html" + write(f, str) + cmd = "open -a \"Google Chrome\" $f" + run(`bash -c $cmd`) +end + +render(nm::NestedMatrix, ts::HasContext{AlgType}) = render(nm, getscope(ts)) + +function renderstr(nm::ScopedNM) + """ + + + + + + + $(str_table(getvalue(nm), getcontext(nm), nm.partition)) + + """ +end + +"""Helper function for `render`""" +function str_table(nm::NestedMatrix, + ts::Union{Nothing,TypeScope}=nothing, + p::Union{Nothing,Vector{Vector{LID}}}=nothing, + caption::String="") + if nm.depth == 0 + "
$caption
$(string(getvalue(nm)))
" + else + nextp, currmsg = if isnothing(p) + nothing => "" + else + p[2:end] => join(map(p[1]) do x + n = " $(nameof(ident(ts; lid=x)))::" + n * str_algast(getvalue(ts[x])) + end," × ") + end + l = length(size(getvalue(nm))) + z, n, m = if l == 3 + size(getvalue(nm)) + elseif l == 2 + [1, size(getvalue(nm))...] + elseif l == 1 + 1, 1, only(size(getvalue(nm))) + else + error("Unexpected shape $(size(getvalue(nm)))") + end + body = join(map(1:z) do k + row = join(map(1:n) do i + rowelem = join(map(1:m) do j + idxs = [[j], [i,j], [k,i,j]][l] + cap = if isnothing(p) + string(idxs) + else + "("*join(map(zip(p[1], idxs)) do (x, idx) + "$(nameof(ts[ident(ts; lid=x)]))=$idx" + end,", ")*")" + end + str_table(getvalue(getvalue(nm))[idxs...], ts, nextp, cap) + end,"\n") + "$rowelem" + end,"\n") + "$row" + end, "\n") + " $body
$caption $currmsg
" + end +end + +"""Like `show` but ignores colors. For HTML rendering.""" +function str_algast(t::AlgAST)::String + if GATs.isapp(t) + if isempty(t.body.args) + nameof(t.body.head) |> string + else + args = join(str_algast.(t.body.args), ",") + "$(nameof(t.body.head))($args)" + end + elseif GATs.isvariable(t) + nameof(t.body) |> string + end +end + +""" +Enumerate all the leaf elements of the nested matrix along with their indices. +Print as a table. +""" +function Base.show(io::IO, ::MIME"text/plain", nm::ScopedNM) + table = permutedims(hcat(mk_table(getvalue(nm))...)) + pretty_table(io, table; header=[nameof.(getidents(nm.ts)); :val]) +end + +function mk_table(nm::NestedMatrix{T}, curr = nothing) where T + curr = isnothing(curr) ? Int[] : curr + res = Vector{String}[] + val = getvalue(nm) + if val isa Nest + for i in CartesianIndices(getvalue(val)) + append!(res, mk_table(getvalue(val)[i], [curr; i.I...])) + end + else + push!(res, string.(Union{Int,T}[curr..., val])) + end + res +end + +function Base.show(io::IO, m::MIME"text/plain", nm::CombinatorialModel) + for s in [sorts(nm.theory); funsorts(nm.theory)] + print(io, nameof(headof(s))) + tc = getvalue(nm.theory[methodof(s)]) + ctx = getcontext(tc) + if !isempty(ctx) + print(io, " ") + show(io, m, ctx) + end + if hasfield(typeof(tc), :type) + print(io, " :: ", tc.type) + end + print(io, "\n") + show(io, m, nm[s]) + end +end + +end # module diff --git a/src/combinatorial/module.jl b/src/combinatorial/module.jl new file mode 100644 index 00000000..c78d5088 --- /dev/null +++ b/src/combinatorial/module.jl @@ -0,0 +1,20 @@ +module Combinatorial + +using Reexport + +include("TypeScopes.jl") +include("DataStructs.jl") +include("Visualization.jl") +include("CModels.jl") +include("HomSearch.jl") +include("Limits.jl") + + +@reexport using .TypeScopes +@reexport using .DataStructs +@reexport using .Visualization +@reexport using .CModels +@reexport using .HomSearch +@reexport using .Limits + +end # module \ No newline at end of file diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl index deb0d9ad..ba46d438 100644 --- a/src/models/ModelInterface.jl +++ b/src/models/ModelInterface.jl @@ -782,4 +782,5 @@ end migrate_model(theorymap::Module, m::Model) = theorymap.Migrator(m) + end # module diff --git a/src/nonstdlib/theories/Categories.jl b/src/nonstdlib/theories/Categories.jl new file mode 100644 index 00000000..0e5f0461 --- /dev/null +++ b/src/nonstdlib/theories/Categories.jl @@ -0,0 +1,9 @@ +@theory Th2Cat <: ThCategory begin + Hom2(dom::(a→b), codom::(a→b))::TYPE ⊣ [a::Ob, b::Ob] + dummy(x::(a→b),y::(a→b),F::Hom2(x,y))::Hom2(y, x) ⊣ [(a,b)::Ob] +end + +@theory ThTwoCat <: ThCategory begin + Hom2(fwd::(a→b), rev::(b→a))::TYPE ⊣ [a::Ob, b::Ob] + dummy(x::(a→b),y::(b→a),F::Hom2(x,y))::Hom2(y, x) ⊣ [(a,b)::Ob] +end \ No newline at end of file diff --git a/src/nonstdlib/theories/Petri.jl b/src/nonstdlib/theories/Petri.jl new file mode 100644 index 00000000..0f631602 --- /dev/null +++ b/src/nonstdlib/theories/Petri.jl @@ -0,0 +1,19 @@ +export ThPetri, ThPetriFibered + +@theory ThPetri begin + S::TYPE + T::TYPE + I(s::S,t::T)::TYPE + O(s::S,t::T)::TYPE +end + +@theory ThPetriFibered begin + S::TYPE + T::TYPE + I::TYPE + O::TYPE + is(i::I)::S + os(o::O)::S + it(i::I)::T + ot(o::O)::T +end \ No newline at end of file diff --git a/src/nonstdlib/theories/Wiring.jl b/src/nonstdlib/theories/Wiring.jl new file mode 100644 index 00000000..0291f897 --- /dev/null +++ b/src/nonstdlib/theories/Wiring.jl @@ -0,0 +1,39 @@ +"""Wires can split and merge""" +@theory NestedWD begin + Diagram::TYPE + Box(d::Diagram)::TYPE + IP(b)::TYPE ⊣ [d::Diagram, b::Box(d)] # InPort + OP(b)::TYPE ⊣ [d::Diagram, b::Box(d)] # OutPort + Wire(op, ip)::TYPE ⊣ [d::Diagram, (b,b′)::Box(d), op::OP(b),ip::IP(b′)] + OIP(d::Diagram)::TYPE # OuterInPort + OOP(d::Diagram)::TYPE # OuterOutPort + IWire(oip,ip)::TYPE ⊣ [d::Diagram, b::Box(d), oip::OIP(d), ip::IP(b)] + OWire(op,oop)::TYPE ⊣ [d::Diagram, b::Box(d), oop::OOP(d), op::OP(b)] + + # Diagrams form a poset with a distinguished top element + ⊤::Diagram + Leq(x::Diagram, y::Diagram)::TYPE # immediate or distant descendent + @op (≤) := Leq + refl(p)::(p ≤ p) ⊣ [p::Diagram] + trans(f::(p ≤ q),g::(q ≤ r))::(p ≤ r) ⊣ [(p,q,r)::Diagram] + top(d::Diagram)::(d ≤ ⊤()) + irrev := f == g ⊣ [(p,q)::Diagram, (f, g)::(p ≤ q)] + poset := x == y ⊣ [(x,y)::Diagram, f::(x ≤ y), g::(y ≤ x)] + + # Nesting associates a box to another diagram + nest(b)::Diagram ⊣ [d::Diagram, b::Box(d)] + + # Nesting respects the ≤ relation + nest_leq(b)::(nest(b) ≤ d) ⊣ [d::Diagram, b::Box(d)] + + # There (only) one box which refers to its own diagram + # TODO + + # Iso between inports and outer inports for any nesting + ip_oip(i)::OIP(nest(b)) ⊣ [d::Diagram, b::Box(d), i::IP(b)] + oip_ip(i)::IP(b) ⊣ [d::Diagram, b::Box(d), i::OIP(nest(b))] + + oip_ip(ip_oip(i)) == i ⊣ [d::Diagram, b::Box(d), i::IP(b)] + ip_oip(oip_ip(i)) == i ⊣ [d::Diagram, b::Box(d), i::OIP(nest(b))] + # Likewise for outports and outer outports for any nesting +end \ No newline at end of file diff --git a/src/nonstdlib/theories/module.jl b/src/nonstdlib/theories/module.jl index ac482603..81804f05 100644 --- a/src/nonstdlib/theories/module.jl +++ b/src/nonstdlib/theories/module.jl @@ -6,5 +6,7 @@ using ...Stdlib using Reexport include("Pushouts.jl") +include("Categories.jl") +include("Petri.jl") end diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl index 3d451eb2..0c8a8f20 100644 --- a/src/syntax/GATs.jl +++ b/src/syntax/GATs.jl @@ -5,7 +5,7 @@ export Constant, AlgTerm, AlgType, AlgAST, AlgTypeConstructor, AlgAccessor, AlgAxiom, AlgStruct, AlgDot, AlgFunction, typesortsignature, sortsignature, getdecl, GATSegment, GAT, GATContext, gettheory, gettypecontext, allmethods, - resolvemethod, + resolvemethod, funsorts, termcons,typecons, accessors, structs, primitive_sorts, struct_sorts, equations, build_infer_expr, compile, sortcheck, allnames, sorts, sortname, InCtx, TermInCtx, TypeInCtx, headof, argsof, methodof, bodyof, argcontext, diff --git a/src/syntax/Scopes.jl b/src/syntax/Scopes.jl index e9cb32f3..57f92a02 100644 --- a/src/syntax/Scopes.jl +++ b/src/syntax/Scopes.jl @@ -79,7 +79,7 @@ rename(tag::ScopeTag, replacements::Dict{Symbol, Symbol}, x) = x An error to throw when an identifier has an unexpected scope tag """ -struct ScopeTagError <: Exception +@struct_hash_equal struct ScopeTagError <: Exception expectedcontext::Any thing::Any end @@ -679,7 +679,7 @@ Must implement: """ abstract type HasScopeList{T} <: Context{T} end -struct ScopeList{T} <: HasScopeList{T} +@struct_hash_equal struct ScopeList{T} <: HasScopeList{T} scopes::Vector{HasScope{T}} taglookup::Dict{ScopeTag, Int} namelookup::Dict{Symbol, Int} @@ -771,7 +771,7 @@ alltags(hsl::HasScopeList) = Set(gettag.(getscopelist(hsl).scopes)) # AppendContext ############### -struct AppendContext{T₁, T₂} <: Context{Union{T₁,T₂}} +@struct_hash_equal struct AppendContext{T₁, T₂} <: Context{Union{T₁,T₂}} ctx1::Context{T₁} ctx2::Context{T₂} function AppendContext(ctx1::Context{T₁}, ctx2::Context{T₂}) where {T₁, T₂} @@ -818,7 +818,7 @@ alltags(c::AppendContext) = union(alltags(c.ctx1), alltags(c.ctx2)) # EmptyContext ############## -struct EmptyContext{T} <: Context{T} +@struct_hash_equal struct EmptyContext{T} <: Context{T} end getscope(c::EmptyContext, level::Int) = throw(BoundsError(c, level)) diff --git a/src/syntax/TheoryMaps.jl b/src/syntax/TheoryMaps.jl index fae0f915..b6906a3f 100644 --- a/src/syntax/TheoryMaps.jl +++ b/src/syntax/TheoryMaps.jl @@ -174,32 +174,66 @@ This function is mutually recursive with `infer_type`. bind_localctx(ctx::GATContext, t::InCtx) = bind_localctx(GATContext(ctx.theory, AppendContext(ctx.context, t.ctx)), t.val) +# function bind_localctx(ctx::GATContext, t::AlgAST) +# m = methodof(t.body) +# tc = getvalue(ctx[m]) +# eqs = equations(ctx.theory, m) +# typed_terms = Dict{Ident, Pair{AlgTerm,AlgType}}() +# for (i,a) in zip(tc.args, t.body.args) +# tt = (a => infer_type(ctx, a)) +# typed_terms[ident(tc, lid=i, level=1)] = tt +# end + +# for lc_arg in reverse(getidents(getcontext(tc))) +# if getlid(lc_arg) ∈ tc.args +# continue +# end +# # one way of determining lc_arg's value +# app = bodyof(first(filter(GATs.isapp, eqs[lc_arg]))) +# to = bodyof(only(argsof(app))) +# m = methodof(app) +# inferred_term = typed_terms[to][2].body.args[getvalue(ctx.theory[m]).arg] +# inferred_type = infer_type(ctx, inferred_term) +# typed_terms[lc_arg] = inferred_term => inferred_type +# end + +# Dict([k=>v[1] for (k,v) in pairs(typed_terms)]) +# end + function bind_localctx(ctx::GATContext, t::AlgAST) m = methodof(t.body) tc = getvalue(ctx[m]) eqs = equations(ctx.theory, m) - typed_terms = Dict{Ident, Pair{AlgTerm,AlgType}}() - for (i,a) in zip(tc.args, t.body.args) + typed_terms = Dict{AlgTerm, Pair{AlgTerm,AlgType}}() + res = Dict{Ident, AlgTerm}() + for (i, a) in zip(tc.args, t.body.args) + x = ident(tc, lid=i, level=1) tt = (a => infer_type(ctx, a)) - typed_terms[ident(tc, lid=i, level=1)] = tt + res[x] = a + for eq in eqs[x] + typed_terms[eq] = tt + end end - for lc_arg in reverse(getidents(getcontext(tc))) - if getlid(lc_arg) ∈ tc.args - continue - end + if getlid(lc_arg) ∈ tc.args + continue + end # one way of determining lc_arg's value app = bodyof(first(filter(GATs.isapp, eqs[lc_arg]))) - to = bodyof(only(argsof(app))) - m = methodof(app) - inferred_term = typed_terms[to][2].body.args[getvalue(ctx.theory[m]).arg] + to = only(argsof(app)) + arg = getvalue(ctx.theory[methodof(app)]).arg + inferred_term = typed_terms[to][2].body.args[arg] inferred_type = infer_type(ctx, inferred_term) - typed_terms[lc_arg] = inferred_term => inferred_type + res[lc_arg] = inferred_term + for x in eqs[lc_arg] + typed_terms[x] = (inferred_term => inferred_type) + end end - Dict([k=>v[1] for (k,v) in pairs(typed_terms)]) + res end + # ID #--- @struct_hash_equal struct IdTheoryMap <: AbsTheoryMap diff --git a/src/syntax/gats/algorithms.jl b/src/syntax/gats/algorithms.jl index b19ee1ac..b5aa889a 100644 --- a/src/syntax/gats/algorithms.jl +++ b/src/syntax/gats/algorithms.jl @@ -204,4 +204,4 @@ function substitute_funs(ctx::Context, t::AlgTerm) elseif isdot(t) AlgTerm(AlgDot(headof(b), substitute_funs(ctx, bodyof(b)))) end -end \ No newline at end of file +end diff --git a/src/syntax/gats/gat.jl b/src/syntax/gats/gat.jl index 53ca6b8b..15609b2f 100644 --- a/src/syntax/gats/gat.jl +++ b/src/syntax/gats/gat.jl @@ -6,7 +6,7 @@ disambiguated by argument sorts. This is a struct rather than just a type alias so that we can customize the show method. """ -struct GATSegment <: HasScope{Judgment} +@struct_hash_equal struct GATSegment <: HasScope{Judgment} scope::Scope{Judgment} end @@ -54,7 +54,7 @@ type constructors, and axioms so that they can be iterated through faster. GATs allow overloading but not shadowing. """ -struct GAT <: HasScopeList{Judgment} +@struct_hash_equal struct GAT <: HasScopeList{Judgment} name::Symbol segments::ScopeList{Judgment} resolvers::OrderedDict{Ident, MethodResolver} @@ -163,6 +163,12 @@ function allnames(theory::GAT; aliases=false) end sorts(theory::GAT) = theory.sorts +funsorts(theory::GAT) = [AlgSort(x...) for x in termcons(theory)] +allsorts(theory::GAT) = sorts(theory) ∪ funsorts(theory) + +AlgSort(theory::GAT, s::Symbol) = only([x for x in allsorts(theory) + if nameof(headof(x)) == s]) + primitive_sorts(theory::GAT) = filter(s->getvalue(theory[methodof(s)]) isa AlgTypeConstructor, sorts(theory)) @@ -194,10 +200,11 @@ function typecons(theory::GAT) xs end - Base.issubset(t1::GAT, t2::GAT) = all(s->hastag(t2, s), gettag.(Scopes.getscopelist(t1).scopes)) +Scopes.getcontext(theory::GAT, s::AlgSort) = getcontext(getvalue(theory[methodof(s)])) + """ `GATContext` @@ -238,4 +245,4 @@ else end """Get all structs in a theory""" -structs(t::GAT) = AlgStruct[getvalue(t[methodof(s)]) for s in struct_sorts(t)] \ No newline at end of file +structs(t::GAT) = AlgStruct[getvalue(t[methodof(s)]) for s in struct_sorts(t)] diff --git a/src/syntax/gats/judgments.jl b/src/syntax/gats/judgments.jl index 096de5eb..71045826 100644 --- a/src/syntax/gats/judgments.jl +++ b/src/syntax/gats/judgments.jl @@ -7,7 +7,7 @@ A scope where variables are assigned to `AlgType`s. We use a wrapper here so that it pretty prints as `[a::B]` instead of `{a => AlgType(B)}` """ -struct TypeScope <: HasScope{AlgType} +@struct_hash_equal struct TypeScope <: HasScope{AlgType} scope::Scope{AlgType} end diff --git a/src/util/Eithers.jl b/src/util/Eithers.jl index ea6bf3e6..f7e6f205 100644 --- a/src/util/Eithers.jl +++ b/src/util/Eithers.jl @@ -1,11 +1,12 @@ module Eithers export Either, Left, Right, isleft, isright +using StructEquality -struct Left{T} +@struct_hash_equal struct Left{T} val::T end -struct Right{S} +@struct_hash_equal struct Right{S} val::S end diff --git a/test/combinatorial/Combinatorial.jl b/test/combinatorial/Combinatorial.jl new file mode 100644 index 00000000..c5bf8f83 --- /dev/null +++ b/test/combinatorial/Combinatorial.jl @@ -0,0 +1,72 @@ +module TestCombinatorial + +using GATlab +using Test +using GATlab.Combinatorial.DataStructs: shape, subterms, validate, NMI, Nest, ScopedNMs +using GATlab.Combinatorial.CModels: enum,random_cardinalities +using GATlab.Combinatorial.Visualization: renderstr +using GATlab.NonStdlib.NonStdTheories: Th2Cat, ThTwoCat +using GATlab.Syntax.TheoryMaps: bind_localctx + +# Unpack theory +T = Th2Cat.Meta.theory; +os, hs, h2s = sorts(T) + +# Manually create a consistent cardinality assignment +m0, m1, m2, m3, m4 = NMI.(0:4) +sing(x::NMI)::NMI = NMI(Nest(reshape([x], 1, 1))) +h2mat = NMI[NMI(Nest([m3 m2; m1 m0])) NMI(reshape(NMI[], 0, 0)|>Nest, depth=1); + sing(m2) sing(m1)] +d = ScopedNMs(T, Dict(os => NMI(2), + hs => NMI(Nest([m2 m0; m1 m1])), + h2s => NMI(Nest(h2mat)))) + +@test sprint(show, MIME"text/plain"(), d[hs]) isa String # render as a table +@test renderstr(d[h2s]) isa String +# render(d[h2s]) # to visualize a nested matrix in html on a Mac + +# Generate one automatically, fixing the Ob and Hom sets +gen_ds = random_cardinalities(T; init=Dict(os => NMI(2), hs => NMI(Nest([m2 m0; m1 m1])))) +# Shape of Hom2 is fixed by sizes of Ob and Hom sets +@test shape(d[h2s]) == shape(gen_ds[h2s]) + +m = CombinatorialModel(T; card_range=1:1) # terminal +@test validate(m) +m.sets[os] = ScopedNM(NMI(2), getcontext(T,os)) +@test !validate(m) + +# Modifying models +#----------------- +ntos = NestedType(os) +m = CombinatorialModel(T; init=deepcopy(d)); +@test NestedTerm(3, ntos) == add_part!(m, ntos) +h11 = NestedType(hs, [CartesianIndex(1,1)]) +m = CombinatorialModel(T; init=deepcopy(d)); +add_part!(m, h11) + +h2_h12 = NestedType(h2s, [CartesianIndex(1,2), CartesianIndex(3,2)]) +@test getvalue.(subterms(T, h2_h12))==[1,2,3,2] + +######### +# TWOCAT # +########## +# Unpack theory +T = ThTwoCat.Meta.theory; +os, hs, h2s = sorts(T) +idsort = AlgSort(termcons(T)[2]...) + +m0, m1, m2, m3, m4 = NMI.(0:4) +rs(x, i, j, d=nothing) = NM(reshape(x, i, j); depth=d) +sing(x) = rs([x], 1, 1) + +d = Dict(os => NMI(2), hs => NMI(Nest([m3 m0; m2 m1]))) + +d = random_cardinalities(T, 1:1; init=deepcopy(d)); +ntos = NestedType(os) + +m = CombinatorialModel(T; init=deepcopy(d)); +add_part!(m, ntos) +rem_part!(m, NestedTerm(1,ntos)) +@test last.(collect(m[idsort])) == [0, 1] + +end # module diff --git a/test/combinatorial/Constructor.jl b/test/combinatorial/Constructor.jl new file mode 100644 index 00000000..ac5ada9f --- /dev/null +++ b/test/combinatorial/Constructor.jl @@ -0,0 +1,158 @@ +"""Helper functions to construct Combinatorial Models""" +module Constructor +export create_graph, create_petri, create_category + +using Test +using GATlab +using GATlab.Combinatorial.DataStructs: NM, NMI, Nest +using GATlab.NonStdlib.NonStdTheories: ThPetri + +# ThGraph +######### + +T = ThGraph.Meta.theory; +os, hs = sorts(T) + +function create_graph(v::Int, es::Vector{Tuple{Int,Int}}=Tuple{Int,Int}[]) + sets = Dict(os => NMI(v), hs => NMI(Nest(map(Iterators.product(1:v,1:v)) do ij + NMI(count(==(ij), es)) + end))) + CombinatorialModel(ThGraph.Meta.theory, sets) +end + +# ThPetri +######### + +Ss, Ts, Is, Os = sorts(ThPetri.Meta.theory) + +function create_petri(I::AbstractMatrix{Int}, O::AbstractMatrix{Int}) + S, T = size(I) + size(I) == size(O) || error("Dimension mismatch: $I vs $O") + sets = Dict(Ss => NMI(S), Ts => NMI(T), + Is => NMI(Nest(NMI.(I))), Os=>NMI(Nest(NMI.(O)))) + CombinatorialModel(ThPetri.Meta.theory, sets) +end + +# ThCategory +############ + +T = ThCategory.Meta.theory; +os, hs = sorts(T) +otc, htc = getvalue.(T[x] for x in methodof.(sorts(T))); +c, i = getvalue.(T[x] for x in last.(termcons(T))); +cs, is = [AlgSort(s...) for s in termcons(T)] + +const Path = Vector{Symbol} +const Edges = Dict{Symbol,Pair{Symbol,Symbol}} + +""" +Category via generators and relations. E.g. commutative square cat would be + +vs = [:A,:B,:C,;D], es=(ab=(:a=>:b),bd=(:b=>:d),ac=(:a=>:c), cd=(:c=>:d)) +eqs = [ [[:ab,:bd], [:ac,:cd]] ] + +No fancy equational reasoning takes place: equality of terms is determined by +converting all subpaths found in the equations to their normal form (the first +element of the list of equands). +""" +function create_category(vs::Set{Symbol}, es::Edges=Edges(), + eqs::Vector{Vector{Path}}=Vector{Path}[]) + N = length(vs) + vord = sort(collect(vs)) + vind = Dict(v => findfirst(==(v), vord) for v in vs) + rep = Dict{Path,Path}() # map subpaths to simpler ones + for eq in eqs + for pth in eq[2:end] + rep[pth] = first(eq) # assume first one in list is the normal form + end + end + + # All the paths initially known (id and generators) + path_map = map(Iterators.product(1:N,1:N)) do ij + [(ij[1]==ij[2] ? [Symbol[]] : [])..., + [[k] for (k, (s, t)) in collect(es) if (vind[s], vind[t]) == ij]...] + end + + # Iteratively compose morphisms + queue = Tuple{Vector{Symbol},Vector{Symbol}}[([i],[j]) + for ((i,(_,tᵢ)), (j, (sⱼ,_))) in + Iterators.product(collect(es), collect(es)) if tᵢ == sⱼ] + + step = 0 + while !isempty(queue) + (step += 1) < 1000 || error("Overflow") + f, g = pop!(queue) + d, cd = vind[es[first(f)][1]], vind[es[last(g)][2]] + concat = normalize!(rep, [f; g]) + idx = findfirst(==(concat), path_map[d, cd]) + if isnothing(idx) + push!(path_map[d, cd], concat) + for i in 1:N + for morph in filter(!isempty, path_map[i, d]) + push!(queue,(morph, concat)) + end + for morph in filter(!isempty, path_map[cd, i]) + push!(queue,(concat, morph)) + end + end + end + end + + # Data for compose + cdata = NMI(Nest(map(Iterators.product(1:N,1:N,1:N)) do (i,j,k) + NMI(Nest(Array{NMI}( + map(Iterators.product(path_map[i,j],path_map[j,k])) do (f,g) + idx = findfirst(==(normalize!(rep, [f;g])), path_map[i, k]) + NMI(something(idx)) + end)); depth=1) + end)) + + sets = Dict(os => NMI(N), hs => NMI(Nest(map(Iterators.product(1:N,1:N)) do ij + NMI(length(path_map[ij...])) + end))) + funs = Dict(is => NMI(Nest(map(i -> NMI(1), 1:N))), + cs => cdata) + CombinatorialModel(T, sets, funs) +end + +create_category(vs::Vector{Symbol}, es, eqs=Vector{Path}[]) = + create_category(Set(vs), es, eqs) + +create_category(vs::Set{Symbol}, es::NamedTuple, eqs=Vector{Path}[]) = + create_category(vs, Edges(pairs(es)), eqs) + + +# Helper functions +"""Find a subarray within an array (from StackOverflow)""" +function issubarray(needle::Vector{T}, haystack::Vector{T})::Union{Nothing,Int} where T + getView(vec, i, len) = view(vec, i:i+len-1) + ithview(i) = getView(haystack, i, length(needle)) + return findfirst(i -> ithview(i) == needle, 1:length(haystack)-length(needle)+1) +end + +"""Replace a subarray with another subarray""" +function repl!(pat::Vector{T}, rep::Vector{T}, data::Vector{T})::Bool where T + i = issubarray(pat, data) + isnothing(i) && return false + for _ in 1:length(pat) + popat!(data, i) + end + for r in reverse(rep) + insert!(data, i, r) + end + true +end + +"""Apply replacements greedily until no more can be applied""" +function normalize!(d::Dict{Vector{T},Vector{T}}, data::Vector{T}) where T + while !isempty(d) + if !all([repl!(k,v,data) for (k,v) in d]) + break + end + end + data +end +z = [1,1,2,5,6,1,2,3] +@test normalize!(Dict([1,2]=>[500]), z) == [1,500,5,6,500,3] + +end # module \ No newline at end of file diff --git a/test/combinatorial/HomSearch.jl b/test/combinatorial/HomSearch.jl new file mode 100644 index 00000000..ce4f4add --- /dev/null +++ b/test/combinatorial/HomSearch.jl @@ -0,0 +1,104 @@ +module TestHomSearch + +using Test +using GATlab +using GATlab.Combinatorial.DataStructs: map_nm, validate, NM, NMI, NMVI, ScopedNMs, Nest +using ..Constructor + +function test_homs(ms, n::Int) + @test all(is_natural, ms) + @test length(ms) == n +end + +# Theory Graph (indexed, not fibered) +##################################### +T = ThGraph.Meta.theory +os, hs = sorts(T) + +# Discrete hom search +for (a,b) in Iterators.product(1:3,1:3) + Ga, Gb = create_graph.([a,b]) + test_homs(homomorphisms(Ga,Gb), b ^ a) +end + +G_12 = create_graph(2, [(1,2)]) +G_12_12 = create_graph(2, [(1,2),(1,2)]) + +@test isempty(homomorphisms(G_12, G_12_12; epic=[:Hom])) +test_homs(homomorphisms(create_graph(2), create_graph(2); iso=[:Ob]), 2) + +G_12_21 = create_graph(2, [(1,2),(2,1)]) +G_11 = create_graph(1, [(1,1)]) +test_homs(homomorphisms(G_12_21, G_11; monic=[:Hom]), 1) + +x = NestedTerm(1, NestedType(hs, [[1,2]])) +y = NestedTerm(1, NestedType(hs, [[2,1]])) +test_homs(homomorphisms(G_12, G_12_12; initial=[x=>y]), 1) +e = NMVI(Int[]) +nmi = ScopedNMs(T, Dict(os => NMVI([2,1]), hs=>NMVI(Nest([e NMVI([1]) ;e e ])))) +test_homs(homomorphisms(G_12, G_12_12; initial=nmi), 1) + +G_21 = create_graph(2, [(2,1)]) +for (a,b) in Iterators.product([G_21,G_12],[G_21,G_12]) + test_homs(homomorphisms(a,b), 1) + test_homs(homomorphisms(a, G_11), 1) +end + +test_homs(homomorphisms(G_12_21,G_12_21), 2) + +G_cyc3 = create_graph(3, [(1,2),(2,3),(3,1)]) +G_cyc6 = create_graph(6, [(1,2),(2,3),(3,4),(4,5),(5,6),(6,1)]) +test_homs(homomorphisms(G_cyc6,G_cyc3), 3) + +# ThCategory +############ + +walking_arrow = create_category([:a,:b], (f=(:a=>:b),)) + +test_homs(homomorphisms(walking_arrow, walking_arrow), 3) + +# 1->2->3 with an additional generator 1->3 +m_123 = create_category([:a,:b,:c], (f=(:a=>:b),g=(:b=>:c), i=(:a=>:c))) +parallel_paths = create_category([:a,:b], (f=(:a=>:b),g=(:a=>:b))) + +# Maps out of parallel_paths are pairs of parallel arrows + +for x in [m_123, walking_arrow, parallel_paths] + test_homs(homomorphisms(parallel_paths, x), sum(map_nm(x->x^2, Int, x[hs]))) +end + +h1 = homomorphism(walking_arrow, parallel_paths) +h2 = homomorphism(parallel_paths, m_123) +h12′ = homomorphism(walking_arrow, m_123) + +using .ThCategory + +C = CombinatorialModelC(ThCategory.Meta.theory) + +@withmodel C (id, compose, Ob, Hom) begin + @test Ob(walking_arrow) isa CombinatorialModel + @test Hom(h1, walking_arrow, parallel_paths) isa CombinatorialModelMorphism + @test h12′ == compose(h1,h2) + @test compose(id(walking_arrow), h1) == h1 +end + +# Theory Petri +############### + +P11_21 = create_petri([1 0; 0 2], [1 0; 0 1 ]) +P11 = create_petri([1 0]', [0 1 ]') +P21 = create_petri([2 0]', [0 1 ]') + +test_homs(homomorphisms(P11, P11_21; monic=[:I,:O]), 3) +test_homs(homomorphisms(P21, P11_21; monic=[:I,:O]), 2) + +test_homs(homomorphisms(P11, P11_21; iso=[:I,:O]), 1) + +# One input species and output species, a 1-1 and a 2-1 transition +PA = create_petri([1 2; 0 0], [0 0; 1 1]) +# Two disjoint 1-in 1-out transitions +PB = create_petri([1 0 ; 0 0;0 1;0 0], [0 0; 1 0; 0 0; 0 1]) + +test_homs(homomorphisms(PB, PA; iso=[:I,:O]), 1) + +end # module diff --git a/test/combinatorial/tests.jl b/test/combinatorial/tests.jl new file mode 100644 index 00000000..85bdc7cc --- /dev/null +++ b/test/combinatorial/tests.jl @@ -0,0 +1,7 @@ +module CombinatorialTests + +include("Constructor.jl") +include("HomSearch.jl") +include("Combinatorial.jl") + +end diff --git a/test/models/ModelInterface.jl b/test/models/ModelInterface.jl index 55181643..8e98e328 100644 --- a/test/models/ModelInterface.jl +++ b/test/models/ModelInterface.jl @@ -58,7 +58,7 @@ end @test implements(FinSetC(), ThCategory) # Todo: get things working where Ob and Hom are the same type (i.e. binding dict not monic) -struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}} +@struct_hash_equal struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}} ntypes::Int end diff --git a/test/runtests.jl b/test/runtests.jl index da2cd870..af1fdaae 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -16,6 +16,10 @@ end include("stdlib/tests.jl") end +@testset "Combinatorial" begin + include("combinatorial/tests.jl") +end + @testset "nonstdlib" begin include("nonstdlib/tests.jl") end From bd76a06c4fe661f7367bfeb0283b370f3d5e9677 Mon Sep 17 00:00:00 2001 From: Kris Brown Date: Sat, 23 Dec 2023 12:02:35 -0500 Subject: [PATCH 2/4] better coverage --- src/combinatorial/DataStructs.jl | 10 ---------- src/combinatorial/HomSearch.jl | 8 -------- src/combinatorial/Limits.jl | 13 ++++--------- src/combinatorial/TypeScopes.jl | 1 - src/combinatorial/Visualization.jl | 9 ++------- test/combinatorial/Combinatorial.jl | 16 +++++++++++++--- test/combinatorial/HomSearch.jl | 5 ++++- 7 files changed, 23 insertions(+), 39 deletions(-) diff --git a/src/combinatorial/DataStructs.jl b/src/combinatorial/DataStructs.jl index 0dc58404..8ebfea88 100644 --- a/src/combinatorial/DataStructs.jl +++ b/src/combinatorial/DataStructs.jl @@ -132,10 +132,6 @@ function map_nm(fun, ret_type::Type, nm::NM; index=false, curr=Idx[]) end end -Base.eltype(::Type{NestedMatrix{T}}) where T = Pair{Vector{<:Idx}, T} - -Base.IteratorSize(::Type{<:NestedMatrix}) = Base.SizeUnknown() - """ Get all the leaves of a NestedMatrix along with their coordinate indices. @@ -290,8 +286,6 @@ Base.getindex(nm::NestedMatrix, idx::NestedType) = nm[getvalue(idx)] Base.setindex!(nm::NestedMatrix, data::NestedMatrix, idx::NestedType) = setindex!(nm, data, getvalue(idx)) -Base.length(n::NestedType) = length(n.lookup) - function Base.getindex(typ::NestedType, i::Int) (x, y) = typ.lookup[i] getvalue(typ)[x][y] @@ -343,8 +337,6 @@ function sub_indices(theory::GAT, lc::TypeScope)::Vector{Vector{Int}} end end -sub_indices(theory::GAT, s::AlgSort) = sub_indices(theory, getcontext(theory, s)) - """ A nested term like Hom2[1,3,2,1]#3 (i.e. the third Hom2 between Hom#2(Ob#1=>Ob#3) and Hom#1(Ob#1=>Ob#3)) produces a vector [Ob[]#1, Ob[]#3, @@ -402,8 +394,6 @@ function Base.setindex!(m::Comb, n::NMI, s::AlgSort) m.sets[s] = val elseif haskey(m.funs, s) m.funs[s] = val - else - throw(KeyError(s)) end end diff --git a/src/combinatorial/HomSearch.jl b/src/combinatorial/HomSearch.jl index f16720d2..10acd8e8 100644 --- a/src/combinatorial/HomSearch.jl +++ b/src/combinatorial/HomSearch.jl @@ -61,14 +61,6 @@ end gettheory(b::BacktrackingState) = b.dom.theory -function Base.show(io::IO, m::MIME"text/plain", s::BacktrackingState) - for (k, v) in s.assignment - println(io, k) - show(io, m, v) - end -end -Base.string(n::BacktrackingState) = sprint(show, MIME"text/plain"(), n) - """ Allow opt-in constraints via `monic`/`epic`/`iso` kwargs. By default these are on the basis of each dependent set, so an iso constraint on Hom would mean that diff --git a/src/combinatorial/Limits.jl b/src/combinatorial/Limits.jl index e67c9c37..7de496a2 100644 --- a/src/combinatorial/Limits.jl +++ b/src/combinatorial/Limits.jl @@ -4,8 +4,8 @@ using ..DataStructs using ..CModels using ...Syntax -initial(T::GAT) = CombinatorialModel(T; card_range=0:0) -terminal(T::GAT) = CombinatorialModel(T; card_range=1:1) +# initial(T::GAT) = CombinatorialModel(T; card_range=0:0) +# terminal(T::GAT) = CombinatorialModel(T; card_range=1:1) """ Pushout a span B <-f- A -g-> C. This is a stub for a function that will be written. @@ -28,13 +28,8 @@ function pushout(f::CombinatorialModelMorphism, g::CombinatorialModelMorphism) error("NotImplementedYet $s: $idx") end end - - for s in funsorts(s) - error("NotImplementedYet $s") - init[s] = NestedMatrix() - end - apex = CombinatorialModel(T; init) - (apex, Morphism(ι1, B, apex), Morphism(ι2, C, apex)) + # apex = CombinatorialModel(T; init) + # (apex, Morphism(ι1, B, apex), Morphism(ι2, C, apex)) end # TODO Implement ThPushout diff --git a/src/combinatorial/TypeScopes.jl b/src/combinatorial/TypeScopes.jl index 3f718ee4..e7007a27 100644 --- a/src/combinatorial/TypeScopes.jl +++ b/src/combinatorial/TypeScopes.jl @@ -50,7 +50,6 @@ end subscope(t::TypeScope, i::LID)::TypeScope = subscope(t, LID[sort(collect(vars(t, i)); by=getvalue); i]) -relid(t::Dict{LID, LID}, x) = error("HERE $t $x $(typeof(x))") relid(t::Dict{LID, LID}, x::Binding) = setvalue(x, relid(t, getvalue(x))) relid(t::Dict{LID, LID}, x::T) where T<:AlgAST = T(relid(t, bodyof(x))) relid(t::Dict{LID, LID}, x::GATs.MethodApp{AlgTerm}) = diff --git a/src/combinatorial/Visualization.jl b/src/combinatorial/Visualization.jl index 8f0dc161..48dadf39 100644 --- a/src/combinatorial/Visualization.jl +++ b/src/combinatorial/Visualization.jl @@ -28,17 +28,12 @@ Base.string(n::Nested) = sprint(show, MIME"text/plain"(), n) # NestedMatrix ############## -"""Visualize NestedMatrix using HTML""" +""" Visualize NestedMatrix using HTML """ # (only tested on Macbook) function render(nm::ScopedNM) - str = renderstr(nm) f = tempname()*".html" - write(f, str) - cmd = "open -a \"Google Chrome\" $f" - run(`bash -c $cmd`) + write(f, renderstr(nm)); run(`bash -c $("open -a \"Google Chrome\" $f")`) end -render(nm::NestedMatrix, ts::HasContext{AlgType}) = render(nm, getscope(ts)) - function renderstr(nm::ScopedNM) """ diff --git a/test/combinatorial/Combinatorial.jl b/test/combinatorial/Combinatorial.jl index c5bf8f83..38474f89 100644 --- a/test/combinatorial/Combinatorial.jl +++ b/test/combinatorial/Combinatorial.jl @@ -2,7 +2,8 @@ module TestCombinatorial using GATlab using Test -using GATlab.Combinatorial.DataStructs: shape, subterms, validate, NMI, Nest, ScopedNMs +using GATlab.Combinatorial.DataStructs: shape, subterms, validate, NMI, Nest, + ScopedNMs, const_nm using GATlab.Combinatorial.CModels: enum,random_cardinalities using GATlab.Combinatorial.Visualization: renderstr using GATlab.NonStdlib.NonStdTheories: Th2Cat, ThTwoCat @@ -23,7 +24,11 @@ d = ScopedNMs(T, Dict(os => NMI(2), @test sprint(show, MIME"text/plain"(), d[hs]) isa String # render as a table @test renderstr(d[h2s]) isa String -# render(d[h2s]) # to visualize a nested matrix in html on a Mac +# render(d[h2s]) # to visualize a nested matrix in HTML on a Mac + + +@test_throws ErrorException NMI(Nest([m3 m2; m1 getvalue(d[hs])])) # not all same depth +@test const_nm(d[hs], :a) isa ScopedNM{Symbol} # Generate one automatically, fixing the Ob and Hom sets gen_ds = random_cardinalities(T; init=Dict(os => NMI(2), hs => NMI(Nest([m2 m0; m1 m1])))) @@ -34,7 +39,10 @@ m = CombinatorialModel(T; card_range=1:1) # terminal @test validate(m) m.sets[os] = ScopedNM(NMI(2), getcontext(T,os)) @test !validate(m) - +@test all(x -> x isa String, [renderstr(m[s]) for s in funsorts(T)]) +@test sprint(show, MIME"text/plain"(), m) isa String +@test_throws KeyError m[only(sorts(ThGroup.Meta.theory))] +@test_throws KeyError m[only(sorts(ThGroup.Meta.theory))] = NMI(3) # Modifying models #----------------- ntos = NestedType(os) @@ -47,6 +55,8 @@ add_part!(m, h11) h2_h12 = NestedType(h2s, [CartesianIndex(1,2), CartesianIndex(3,2)]) @test getvalue.(subterms(T, h2_h12))==[1,2,3,2] +@test string(NestedTerm(3, h11)) == "Hom[(1, 1)]#3" + ######### # TWOCAT # ########## diff --git a/test/combinatorial/HomSearch.jl b/test/combinatorial/HomSearch.jl index ce4f4add..9ee0e79b 100644 --- a/test/combinatorial/HomSearch.jl +++ b/test/combinatorial/HomSearch.jl @@ -41,6 +41,7 @@ test_homs(homomorphisms(G_12, G_12_12; initial=nmi), 1) G_21 = create_graph(2, [(2,1)]) for (a,b) in Iterators.product([G_21,G_12],[G_21,G_12]) test_homs(homomorphisms(a,b), 1) + test_homs(homomorphisms(a,b; iso=true), 1) test_homs(homomorphisms(a, G_11), 1) end @@ -49,7 +50,7 @@ test_homs(homomorphisms(G_12_21,G_12_21), 2) G_cyc3 = create_graph(3, [(1,2),(2,3),(3,1)]) G_cyc6 = create_graph(6, [(1,2),(2,3),(3,4),(4,5),(5,6),(6,1)]) test_homs(homomorphisms(G_cyc6,G_cyc3), 3) - +isempty(homomorphisms(G_cyc3, G_cyc6; iso=true)) # ThCategory ############ @@ -71,6 +72,8 @@ h1 = homomorphism(walking_arrow, parallel_paths) h2 = homomorphism(parallel_paths, m_123) h12′ = homomorphism(walking_arrow, m_123) +@test h1[hs] isa ScopedNM{Vector{Int}} + using .ThCategory C = CombinatorialModelC(ThCategory.Meta.theory) From 1c29beccac9d4bbc9fc4ae3fa82cfbf2e5f76c91 Mon Sep 17 00:00:00 2001 From: Kris Brown Date: Sun, 24 Dec 2023 01:03:29 -0500 Subject: [PATCH 3/4] type/term iterator, homsearch assign whole terms, pushouts, --- src/combinatorial/CModels.jl | 13 ++-- src/combinatorial/DataStructs.jl | 99 +++++++++++++++++++++++------ src/combinatorial/HomSearch.jl | 94 ++++++++++++--------------- src/combinatorial/Limits.jl | 85 ++++++++++++++++++++----- src/combinatorial/Visualization.jl | 4 +- test/combinatorial/Combinatorial.jl | 3 +- test/combinatorial/HomSearch.jl | 9 +-- test/combinatorial/Limits.jl | 48 ++++++++++++++ test/combinatorial/tests.jl | 1 + 9 files changed, 254 insertions(+), 102 deletions(-) create mode 100644 test/combinatorial/Limits.jl diff --git a/src/combinatorial/CModels.jl b/src/combinatorial/CModels.jl index 196ba369..256960d2 100644 --- a/src/combinatorial/CModels.jl +++ b/src/combinatorial/CModels.jl @@ -62,7 +62,7 @@ function random_cardinalities(theory::GAT, card_range=nothing; card_range = isnothing(card_range) ? (0:3) : card_range for sort in setdiff(sorts(theory), keys(res)) ctx = getcontext(theory, sort) - res[sort] = ScopedNM(rand_nm(res, theory, ctx, Int[], card_range), ctx) + res[sort] = ScopedNM(rand_nm(res, theory, ctx, Int[], card_range), ctx, sort) end res end @@ -72,7 +72,7 @@ function random_functions(cards::NMIs, theory::GAT; init=nothing)::NMIs res = isnothing(init) ? NMIs() : (init isa Dict ? ScopedNMs(theory, init) : init) for s in funsorts(theory) haskey(res, s) && continue - res[s] = ScopedNM(random_function(cards, theory, s), getcontext(theory, s)) + res[s] = ScopedNM(random_function(cards, theory, s), theory, s) end res end @@ -199,8 +199,7 @@ the function is 0. This implementation creates modified NestedMatrices and then replaces the ones in the CombinatorialModel. A more sophisticated algorithm would do this in place. """ -function add_part!(m::CombinatorialModel, - type::NestedType=NestedType())::NestedTerm +function add_part!(m::CombinatorialModel, type::NestedType)::NestedTerm T = gettheory(m) enums = Dict(s => collect(m[s]) for s in sorts(T)) # store for later new_cardinality = getvalue(m[type]) + 1 @@ -239,8 +238,7 @@ function rem_part!(m::CombinatorialModel, term::NestedTerm) for s in sorts(T) getsort(type) ∈ sortsignature(getvalue(T, methodof(s))) || continue new_nm = rand_nm(m.sets, T, getcontext(T, s), Int[], [0]) # all empty sets - for (e, _) in new_nm - e = NestedType(s, e) + for e in TypeIterator(ScopedNM(new_nm, T, s)) new_e = deepcopy(e) for (i, subterm) in enumerate(subterms(T, e)) if subterm == term @@ -253,8 +251,7 @@ function rem_part!(m::CombinatorialModel, term::NestedTerm) end for s in funsorts(T) new_fun = random_function(m.sets, T, s) - for (e, _) in new_fun # copy over old data - e = NestedType(s, e) + for e in TypeIterator(ScopedNM(new_fun, T, s)) # copy over old data new_e = deepcopy(e) for (i, subterm) in enumerate(subterms(T, e)) if subterm == term diff --git a/src/combinatorial/DataStructs.jl b/src/combinatorial/DataStructs.jl index 8ebfea88..11efd3dc 100644 --- a/src/combinatorial/DataStructs.jl +++ b/src/combinatorial/DataStructs.jl @@ -1,6 +1,7 @@ module DataStructs export NestedMatrix, CombinatorialModel, CombinatorialModelMorphism, - NestedType, NestedTerm, CombinatorialModelC, is_natural, getsort + NestedType, NestedTerm, CombinatorialModelC, is_natural, getsort, + TermIterator, TypeIterator using StructEquality @@ -109,8 +110,8 @@ the data on the leaves. shape(nm::NM)::NM{Nothing} = const_nm(nm, nothing) """ Replace all leaves with a constant value. Optionally deepcopy that value """ -function const_nm(nm::NM, v::T; copy=false)::NM{T} where T - map_nm(_ -> (copy ? deepcopy : identity)(v), T, nm) +function const_nm(nm::NM, v::T; copy=false, type=nothing) where T + map_nm(_ -> (copy ? deepcopy : identity)(v), isnothing(type) ? T : type, nm) end """ @@ -170,21 +171,29 @@ function Base.iterate(nm::NestedMatrix{T}, state=(true => Idx[])) where T end end -Base.sum(nm::NestedMatrix) = sum(getvalue.(nm.data)) # total sum of leaves - +Base.sum(nm::NestedMatrix{<:Number}) = if nm.depth == 0 + nm.data +else + sum(getvalue.(nm.data)) # total sum of leaves +end """A NestedMatrix with a TypeScope to make sense of the indexing""" @struct_hash_equal struct ScopedNM{T} val::NM{T} + sort::AlgSort ts::TypeScope partition::Vector{Vector{LID}} - function ScopedNM(val::NM{T}, ts::TypeScope) where T - new{T}(val, ts, partition(ts)) + function ScopedNM(val::NM{T}, theory::GAT, s::AlgSort) where T + ts = getcontext(theory, s) + new{T}(val, s, ts, partition(ts)) + end + function ScopedNM(val::NM{T}, scope::TypeScope, s::AlgSort) where T + new{T}(val, s, scope, partition(scope)) end end getvalue(s::ScopedNM) = s.val - +getsort(s::ScopedNM) = s.sort getcontext(s::ScopedNM) = s.ts shape(s::ScopedNM) = shape(getvalue(s)) @@ -201,11 +210,11 @@ Base.getindex(n::ScopedNM{T}, i) where T = getindex(getvalue(n), i) Base.setindex!(n::ScopedNM{T}, i, k) where T = setindex!(getvalue(n), i, k) -map_nm(fun, ret_type, nm::ScopedNM; kw...) = - ScopedNM(map_nm(fun, ret_type, getvalue(nm); kw...), getcontext(nm)) +map_nm(fun, ret_type, n::ScopedNM; kw...) = + ScopedNM(map_nm(fun, ret_type, getvalue(n); kw...), getcontext(n), getsort(n)) const_nm(n::ScopedNM, v; copy=false) = - ScopedNM(const_nm(getvalue(n), v; copy), getcontext(n)) + ScopedNM(const_nm(getvalue(n), v; copy), getcontext(n), getsort(n)) const AlgDict{T} = Dict{AlgSort, NM{T}} @@ -214,7 +223,7 @@ const AlgDict{T} = Dict{AlgSort, NM{T}} end function ScopedNMs(theory::GAT, xs::AlgDict{T}) where T - ScopedNMs{T}(Dict(k=>ScopedNM(v, getcontext(theory, k)) for (k,v) in pairs(xs))) + ScopedNMs{T}(Dict(k=>ScopedNM(v, theory, k) for (k,v) in pairs(xs))) end function ScopedNMs{T}() where T @@ -239,6 +248,8 @@ Base.haskey(s::ScopedNMs{T}, k::AlgSort) where T = haskey(getvalue(s), k) Base.get(s::ScopedNMs{T}, k, v) where T = get(getvalue(s), k, v) +Base.values(s::ScopedNMs{T}) where T = values(getvalue(s)) + const NMI = NM{Int} const NMVI = NM{Vector{Int}} @@ -312,7 +323,7 @@ getsort(n::NestedTerm)::AlgSort = getsort(argsof(n)) Base.getindex(nm::NestedMatrix{Vector{T}}, idx::NestedTerm) where T = getvalue(nm[argsof(idx)])[getvalue(idx)] -function Base.setindex!(nm::NMVI, data::Int, idx::NestedTerm) +function Base.setindex!(nm::NM{Vector{T}}, data::T, idx::NestedTerm) where T getvalue(nm[argsof(idx)])[getvalue(idx)] = data end @@ -357,6 +368,53 @@ function subterms(theory::GAT, trm::Nested)::Vector{NestedTerm} end end +""" +Enumerate a NestedMatrix, yielding expressions like `compose[1,2,3,1,4]` + +This ignores the leaf values of the NestedMatrix. +""" +struct TypeIterator + s::ScopedNM{Int} +end +Base.length(s::TypeIterator) = length(s.s) +Base.eltype(::Type{TypeIterator}) = NestedType +Base.iterate(s::TypeIterator) = iterate(s, Iterators.Stateful(s.s)) +Base.iterate(s::TypeIterator, it) = + isempty(it) ? nothing : (NestedType(getsort(s.s), popfirst!(it)[1]), it) + +""" +Enumerate a typecon matrix, yielding expressions like `Hom[1,2]#1`, `Hom[1,2]#2` +""" +struct TermIterator + s::ScopedNM{Int} +end + +Base.length(s::TermIterator) = sum(s.s) + +Base.eltype(::Type{TermIterator}) = NestedTerm + +Base.iterate(s::TermIterator) = + iterate(s, (Iterators.Stateful(s.s), nothing, Int[])) + +function Base.iterate(s::TermIterator, state) + (it, idx, queue) = state + if isempty(queue) + if isempty(it) + nothing + else + idx, val = popfirst!(it) + iterate(s, (it, idx, collect(1:val))) + end + else + nxt = popfirst!(queue) + NestedTerm(nxt, NestedType(getsort(s.s), idx)), (it, idx, queue) + end +end + + +# Base.iterate(s::ScopedNM{T}, i) where T = iterate(getvalue(s), i) + + # Models ######## @@ -370,16 +428,20 @@ One might be tempted to call this a GATset. theory::GAT sets::NMIs funs::NMIs - function CombinatorialModel(t, s=NMIs(), f=NMIs()) + function CombinatorialModel(t, s=NMIs(), f=NMIs(); check=true) s, f = [sf isa NMIs ? sf : ScopedNMs(t, sf) for sf in [s,f]] - Set(keys(s)) == Set(sorts(t)) || error("Bad sort keys $s") - Set(keys(f)) == Set(funsorts(t)) || error("Bad fun keys $s") + if check + Set(keys(s)) == Set(sorts(t)) || error("Bad sort keys $s") + Set(keys(f)) == Set(funsorts(t)) || error("Bad fun keys $s") + end new(t, s, f) end end const Comb = CombinatorialModel gettheory(c::Comb) = c.theory +Base.getindex(m::Comb, s::Symbol) = m[AlgSort(gettheory(m), s)] + Base.getindex(m::Comb, s::AlgSort) = if haskey(m.sets,s) m.sets[s] elseif haskey(m.funs, s) @@ -389,7 +451,7 @@ else end function Base.setindex!(m::Comb, n::NMI, s::AlgSort) - val = ScopedNM(n, getcontext(m.theory, s)) + val = ScopedNM(n, m.theory, s) if haskey(m.sets,s) m.sets[s] = val elseif haskey(m.funs, s) @@ -447,7 +509,8 @@ end const Morphism = CombinatorialModelMorphism -Base.getindex(c::Morphism, k) = components(c)[k] +Base.getindex(c::Morphism, k::AlgSort) = components(c)[k] +Base.getindex(c::Morphism, k::Symbol) = components(c)[AlgSort(gettheory(c), k)] gettheory(c::Morphism) = gettheory(c.dom) diff --git a/src/combinatorial/HomSearch.jl b/src/combinatorial/HomSearch.jl index 10acd8e8..6ec25d70 100644 --- a/src/combinatorial/HomSearch.jl +++ b/src/combinatorial/HomSearch.jl @@ -5,8 +5,8 @@ using StructEquality using ..TypeScopes: partition, repartition using ..DataStructs -using ..DataStructs: map_nm, sub_indices, subterms, getsort, Comb, - NM, NMI, NMIs, NMVI, NMVIs, const_nm, ScopedNMs +using ..DataStructs: map_nm, sub_indices, subterms, getsort, Comb, AlgDict, + NM, NMI, NMIs, NMVI, NMVIs, Idx, const_nm, ScopedNMs using ...Syntax using ..Visualization import ...Syntax: gettheory, argsof @@ -48,9 +48,14 @@ Assignment of attribute variables maintains both the assignment as well as the number of times that variable has been bound. We can only *freely* assign the variable to match any AttrVar or concrete attribute value if it has not yet been bound. + +Assignment must store an entire NestedTerm per domain set element because one +might unassign the dom of a Hom before unassigning the Hom. So if we used a +NestedMatrix{Int}, it would no longer be clear what element taht Hom is mapping +to. """ @struct_hash_equal struct BacktrackingState - assignment::NMVIs + assignment::ScopedNMs{Vector{Maybe{NestedTerm}}} assignment_depth::NMVIs inv_assignment::ScopedNMs{NMVI} refcounts::ScopedNMs{NMVI} @@ -103,12 +108,11 @@ getinitial(::Comb, ::Comb, ::Nothing) = Pair{NestedTerm, NestedTerm}[] function getinitial(X::Comb, Y::Comb, xys::NMVIs) m = CombinatorialModelMorphism(xys, X, Y) res = Pair{NestedTerm, NestedTerm}[] - for s in sorts(gettheory(X)) - for (idx, vals) in get(xys, s, []) - xtype = NestedType(s, idx) - for xᵢ in 1:length(vals) - x = NestedTerm(xᵢ, xtype) - push!(res, x => m(x)) + for s in filter(s->haskey(xys,s), sorts(gettheory(X))) + for x in TermIterator(X[s]) + y = m(x) + if getvalue(y) > 0 + push!(res, x => y) end end end @@ -127,14 +131,16 @@ function backtracking_search(f, X::Comb, Y::Comb; monic=false, epic=false, # sort_monic, sort_epic = normalize_monic_epic_iso(monic′, epic′, iso′, T) # Initialize state variables for search. - assignment = NMVIs(Dict(c=>map_nm(i->zeros(Int,i), Vector{Int}, X.sets[c]) - for c in sorts(T))) - assignment_depth = deepcopy(assignment) + assignment = ScopedNMs{Vector{Maybe{NestedTerm}}}(Dict(map(sorts(T)) do c + c => map_nm(i->fill(nothing,i), Vector{Maybe{NestedTerm}}, X.sets[c]) + end)) + assignment_depth = NMVIs(Dict(c=>map_nm(i->zeros(Int,i), Vector{Int}, X.sets[c]) + for c in sorts(T))) nmvis(c) = const_nm(getvalue(X.sets[c]), map_nm(i->zeros(Int, i), Vector{Int}, getvalue(Y.sets[c])); copy=true) - inv_assgn = ScopedNMs(T, Dict{AlgSort,NM{NMVI}}(c => nmvis(c) for c in monic)) - refcounts = ScopedNMs(T, Dict{AlgSort,NM{NMVI}}(c => nmvis(c) for c in epic)) + inv_assgn = ScopedNMs(T, AlgDict{NMVI}(c => nmvis(c) for c in monic)) + refcounts = ScopedNMs(T, AlgDict{NMVI}(c => nmvis(c) for c in epic)) unassigned = NMIs(Dict(c => deepcopy(X.sets[c]) for c in epic)) @@ -154,7 +160,10 @@ function backtracking_search(f, state::BacktrackingState, depth::Int) mrv, x = find_mrv_elem(state, depth) if isnothing(x) # No unassigned elements remain, so we have a complete assignment. - return f(CombinatorialModelMorphism(state.assignment, state.dom, state.codom)) + asgn = Dict(map(collect(state.assignment)) do (k, v) + k => map_nm(xs->getvalue.(xs), Vector{Int}, getvalue(v)) + end) + return f(CombinatorialModelMorphism(asgn, state.dom, state.codom)) elseif isempty(mrv) # An element has no allowable assignment, so we must backtrack. return false @@ -176,16 +185,13 @@ function find_mrv_elem(state::BacktrackingState, depth::Int) mrv, remaining_values, mrv_elem = Inf, NestedTerm[], nothing Y = state.codom for c in sorts(T), (depsₓ, depset) in state.assignment[c] - for (xval, y) in enumerate(depset) - y == 0 || continue + for (xval, yval) in enumerate(depset) + isnothing(yval) || continue x = NestedTerm(xval, NestedType(c, depsₓ)) success = [] - for (depsᵧ, yvals) in Y.sets[c] - for yval in 1:yvals - y = NestedTerm(yval, NestedType(c, depsᵧ)) - if can_assign_elem(state, depth, x, y) - push!(success, y) - end + for y in TermIterator(Y.sets[c]) + if can_assign_elem(state, depth, x, y) + push!(success, y) end end if length(success) < mrv @@ -208,12 +214,7 @@ function can_assign_elem(state::BacktrackingState, depth::Int, x::NestedTerm, y: save_state′ = deepcopy(state) ok = assign_elem!(state, depth, x, y) unassign_elem!(state, depth, x) - for f in fieldnames(Comb) - fa, fb = getfield.([save_state′.dom,state.dom], Ref(f)) - fa == fb || error("$f: \n$fa \n!= \n$fb") - end save_state′ == state || error("Unassign x$(string(x))↦y$(string(y)) doesn't undo assign \n$(string(save_state′))\n\n$(string(state))") - return ok end @@ -227,13 +228,7 @@ function assign_elem!(state::BacktrackingState, depth::Int, x::NestedTerm, y::Ne c = getsort(x) c == getsort(y) || error("Mismatched sorts $c $(getsort(y))") y′ = state.assignment[x] - sts = subterms(gettheory(state), x) - ysts = [state.assignment[getsort(st)][st] for st in sts] - ctx = getcontext(gettheory(state), c) - yidxs = [CartesianIndex(i...) for i in repartition(ctx, ysts)] - y′term = NestedTerm(y′, NestedType(c, yidxs)) - y′term == y && return true # If x is already assigned to y, return immediately. - y′ == 0 || return false # Otherwise, x must be unassigned. + isnothing(y′) || return y′ == y # If x is already assigned to y, return immediately. if haskey(state.inv_assignment, c) if getvalue(state.inv_assignment[argsof(x)])[y] != 0 return false # Also, y must unassigned in the inverse assignment. @@ -258,7 +253,7 @@ function assign_elem!(state::BacktrackingState, depth::Int, x::NestedTerm, y::Ne end # Make the assignment and recursively assign subparts. - state.assignment[x] = getvalue(y) + state.assignment[x] = y state.assignment_depth[x] = depth if haskey(state.inv_assignment, c) inv = getvalue(state.inv_assignment[argsof(x)]) @@ -273,14 +268,13 @@ function assign_elem!(state::BacktrackingState, depth::Int, x::NestedTerm, y::Ne # Set other values based on term constructor naturality constraints for (funsort, fun_data) in state.dom.funs - for (dom_deps, _) in fun_data # check, for each combination of args: - valX_expr = NestedType(funsort, dom_deps) + for valX_expr in TypeIterator(fun_data) # check, for each combination of args: valX = state.dom(valX_expr) sts = subterms(gettheory(state), valX_expr) any(==(x), sts) || continue # only if the term we just set is an arg ysts = [state.assignment[getsort(st)][st] for st in sts] - any(==(0), ysts) && continue # only if all args of this f(...) are defined - yidxs = [CartesianIndex(i...) for i in repartition(length.(dom_deps), ysts)] + any(isnothing, ysts) && continue # only if all args of this f(...) are defined + yidxs = [Idx(i...) for i in repartition(length.(getvalue(valX_expr)), getvalue.(ysts))] valY = state.codom(NestedType(funsort, yidxs)) assign_elem!(state, depth, valX, valY) || return false end @@ -288,25 +282,16 @@ function assign_elem!(state::BacktrackingState, depth::Int, x::NestedTerm, y::Ne return true end -function (state::BacktrackingState)(x::NestedTerm) - sts = subterms(gettheory(state), x) - (y, ysts...) = ys = [state.assignment[getsort(st)][st] for st in [x, sts...]] - any(==(0), ys) && return nothing # only if all args are defined - lens = length.(partition(getcontext(gettheory(state), getsort(x)))) - yidxs = [CartesianIndex(i...) for i in repartition(lens, ysts)] - NestedTerm(y, NestedType(getsort(x), yidxs)) -end - """ Unassign the element (c,deps,x) in the current assignment. """ function unassign_elem!(state::BacktrackingState, depth::Int, x::NestedTerm) c = getsort(x) - y = state(x) + y = state.assignment[x] for sub in subterms(gettheory(state), x) unassign_elem!(state, depth, sub) end - state.assignment[x] == 0 && return + isnothing(y) && return assign_depth = state.assignment_depth[x] @assert assign_depth <= depth @@ -322,12 +307,11 @@ function unassign_elem!(state::BacktrackingState, depth::Int, x::NestedTerm) xunassgn.data = xunassgn.data + 1 end - state.assignment[x] = 0 + state.assignment[x] = nothing state.assignment_depth[x] = 0 - for (funsort, fun_data) in state.dom.funs - for (deps, _) in fun_data - fx = NestedType(funsort, deps) + for fun_data in values(state.dom.funs) + for fx in TypeIterator(fun_data) if x ∈ subterms(gettheory(state), fx) fx_val = state.dom(fx) unassign_elem!(state, depth, fx_val) diff --git a/src/combinatorial/Limits.jl b/src/combinatorial/Limits.jl index 7de496a2..ecba3000 100644 --- a/src/combinatorial/Limits.jl +++ b/src/combinatorial/Limits.jl @@ -1,35 +1,90 @@ module Limits +export pushout, initial, terminal using ..DataStructs +using ..DataStructs: Idx, NMI, NMIs, NMVIs, ScopedNM, Morphism, Comb, map_nm using ..CModels +using ..CModels: rand_nm, random_function using ...Syntax +using ...Stdlib +using ...Models +using .ThCategory -# initial(T::GAT) = CombinatorialModel(T; card_range=0:0) -# terminal(T::GAT) = CombinatorialModel(T; card_range=1:1) +using DataStructures: IntDisjointSets, find_root! + +initial(T::GAT) = CombinatorialModel(T; card_range=0:0) + +terminal(T::GAT) = CombinatorialModel(T; card_range=1:1) """ -Pushout a span B <-f- A -g-> C. This is a stub for a function that will be written. +Pushout a span B <-f- A -g-> C. This must be done iteratively for each sort, depending on the earlier sorts. A colimit of finite GAT models can itself be infinite. So we cannot expect `saturate!` to terminate with the result. + +With a bit of work this code could be generalized to work on bipartite colimit +diagrams. """ -function pushout(f::CombinatorialModelMorphism, g::CombinatorialModelMorphism) +function pushout(f::Morphism, g::Morphism) T = gettheory(f) - C = CombinatorialModelC(T) - A, B, C = dom[C](f), codom[C](f), codom[C](g) - A == dom[C](g) || error("Cannot pushout without common apex") - ι1, ι2 = NMVIs(), NMVIs() - init = NMIs() - for s in sorts(T) - init[s] = random_nm(init, T, getcontext(T, s),Int[],[0]) # initialize w/ zeros - for (idx, _) in init[s] - error("NotImplementedYet $s: $idx") + @withmodel CombinatorialModelC(T) (dom, codom) begin + A, B, C = dom(f), codom(f), codom(g) + A == dom(g) || error("Cannot pushout without common apex") + apex = initial(T) + ι₁, ι₂ = Morphism(NMVIs(), B, apex), Morphism(NMVIs(), C, apex) + + # Populate cardinality data of apex and populate maps ι₁, ι₂ + for s in sorts(T) + apex.sets[s] = ScopedNM(rand_nm(apex.sets, T, getcontext(T, s), Int[],[0]), T, s) # apex w/ zeros + (Bs, Bs⁻¹), (Cs, Cs⁻¹) = map([B=>false,C=>true]) do (X, offset) + Xs = collect(TermIterator(X[s])) + Xs => Dict([v => (i + (offset ? sum(B[s]) : 0)) for (i, v) in enumerate(Xs)]) + end + i1, i2 = 1:length(Bs), 1:length(Cs) .+ length(Bs) + eq = IntDisjointSets(i2.stop) + for aterm in TermIterator(A[s]) + union!(eq, Bs⁻¹[f(aterm)], Cs⁻¹[g(aterm)]) + end + roots = find_root!.(Ref(eq), 1:length(eq)) + uroots = unique(roots) + rootdict = [findfirst(==(i), uroots) for i in 1:length(eq)] + apex_terms = map(uroots) do eq_idx + f_id = findfirst(==(eq_idx), i1) + ι, trm = if !isnothing(f_id) + (ι₁, Bs[f_id]) + else + (ι₂, Cs[findfirst(==(eq_idx), i2) - i1.stop]) + end + typ = ι(argsof(trm)) + add_part!(apex, typ) |> getvalue + end + function fun1(idx::Vector{<:Idx}, val::Int)::Vector{Int} + terms = getindex.(Ref(Bs⁻¹), NestedTerm.(1:val,Ref(NestedType(s, idx)))) + apex_terms[rootdict[roots[i1[terms]]]] + end + ι₁.components[s] = map_nm(fun1, Vector{Int}, B[s]; index=true) + function fun2(idx::Vector{<:Idx}, val::Int)::Vector{Int} + terms = getindex.(Ref(Cs⁻¹), NestedTerm.(1:val,Ref(NestedType(s, idx)))) + apex_terms[rootdict[roots[i2[terms]]]] + end + ι₂.components[s] = map_nm(fun2, Vector{Int}, C[s]; index=true) + end + # Populate function data + for s in funsorts(T) + apex.funs[s] = ScopedNM(rand_nm(apex.sets, T, getcontext(T, s), Int[], [0]), T, s) + for bargs in TypeIterator(B[s]) + fbargs = ι₁(bargs) + apex.funs[s][fbargs] = NMI(getvalue(ι₁(B(bargs)))) + end + for cargs in TypeIterator(C[s]) + gcargs = ι₂(cargs) + apex.funs[s][gcargs] = NMI(getvalue(ι₂(C(cargs)))) + end end + return (apex, ι₁, ι₂) end - # apex = CombinatorialModel(T; init) - # (apex, Morphism(ι1, B, apex), Morphism(ι2, C, apex)) end # TODO Implement ThPushout diff --git a/src/combinatorial/Visualization.jl b/src/combinatorial/Visualization.jl index 48dadf39..123e1093 100644 --- a/src/combinatorial/Visualization.jl +++ b/src/combinatorial/Visualization.jl @@ -130,7 +130,9 @@ Print as a table. """ function Base.show(io::IO, ::MIME"text/plain", nm::ScopedNM) table = permutedims(hcat(mk_table(getvalue(nm))...)) - pretty_table(io, table; header=[nameof.(getidents(nm.ts)); :val]) + if !isempty(table) + pretty_table(io, table; header=[nameof.(getidents(nm.ts)); :val]) + end end function mk_table(nm::NestedMatrix{T}, curr = nothing) where T diff --git a/test/combinatorial/Combinatorial.jl b/test/combinatorial/Combinatorial.jl index 38474f89..03050c3c 100644 --- a/test/combinatorial/Combinatorial.jl +++ b/test/combinatorial/Combinatorial.jl @@ -37,12 +37,13 @@ gen_ds = random_cardinalities(T; init=Dict(os => NMI(2), hs => NMI(Nest([m2 m0; m = CombinatorialModel(T; card_range=1:1) # terminal @test validate(m) -m.sets[os] = ScopedNM(NMI(2), getcontext(T,os)) +m.sets[os] = ScopedNM(NMI(2), T, os) @test !validate(m) @test all(x -> x isa String, [renderstr(m[s]) for s in funsorts(T)]) @test sprint(show, MIME"text/plain"(), m) isa String @test_throws KeyError m[only(sorts(ThGroup.Meta.theory))] @test_throws KeyError m[only(sorts(ThGroup.Meta.theory))] = NMI(3) + # Modifying models #----------------- ntos = NestedType(os) diff --git a/test/combinatorial/HomSearch.jl b/test/combinatorial/HomSearch.jl index 9ee0e79b..e1cf7a04 100644 --- a/test/combinatorial/HomSearch.jl +++ b/test/combinatorial/HomSearch.jl @@ -34,8 +34,9 @@ test_homs(homomorphisms(G_12_21, G_11; monic=[:Hom]), 1) x = NestedTerm(1, NestedType(hs, [[1,2]])) y = NestedTerm(1, NestedType(hs, [[2,1]])) test_homs(homomorphisms(G_12, G_12_12; initial=[x=>y]), 1) + e = NMVI(Int[]) -nmi = ScopedNMs(T, Dict(os => NMVI([2,1]), hs=>NMVI(Nest([e NMVI([1]) ;e e ])))) +nmi = ScopedNMs(T, Dict(os => NMVI([2,1]), hs=>NMVI(Nest([e NMVI([1]); e e ])))) test_homs(homomorphisms(G_12, G_12_12; initial=nmi), 1) G_21 = create_graph(2, [(2,1)]) @@ -51,6 +52,7 @@ G_cyc3 = create_graph(3, [(1,2),(2,3),(3,1)]) G_cyc6 = create_graph(6, [(1,2),(2,3),(3,4),(4,5),(5,6),(6,1)]) test_homs(homomorphisms(G_cyc6,G_cyc3), 3) isempty(homomorphisms(G_cyc3, G_cyc6; iso=true)) + # ThCategory ############ @@ -63,16 +65,15 @@ m_123 = create_category([:a,:b,:c], (f=(:a=>:b),g=(:b=>:c), i=(:a=>:c))) parallel_paths = create_category([:a,:b], (f=(:a=>:b),g=(:a=>:b))) # Maps out of parallel_paths are pairs of parallel arrows - for x in [m_123, walking_arrow, parallel_paths] - test_homs(homomorphisms(parallel_paths, x), sum(map_nm(x->x^2, Int, x[hs]))) + test_homs(homomorphisms(parallel_paths, x), sum(map_nm(x->x^2, Int, x[:Hom]))) end h1 = homomorphism(walking_arrow, parallel_paths) h2 = homomorphism(parallel_paths, m_123) h12′ = homomorphism(walking_arrow, m_123) -@test h1[hs] isa ScopedNM{Vector{Int}} +@test h1[:Hom] isa ScopedNM{Vector{Int}} using .ThCategory diff --git a/test/combinatorial/Limits.jl b/test/combinatorial/Limits.jl new file mode 100644 index 00000000..125681e6 --- /dev/null +++ b/test/combinatorial/Limits.jl @@ -0,0 +1,48 @@ +module TestLimits + +using Test +using GATlab +using GATlab.Combinatorial.DataStructs: TermIterator, TypeIterator +using ..Constructor + +# ThGraph +######### + +G_1212 = create_graph(2, [(1,2),(1,2)]) +G_12_2323 = create_graph(3, [(1,2),(2,3),(2,3)]) +G_1212_2323 = create_graph(3, [(1,2),(1,2),(2,3),(2,3)]) + +T = ThGraph.Meta.theory +os, hs = sorts(T) +e1, e2 = NestedTerm.(1:2, Ref(NestedType(hs, [[1,2]]))) +e3, e4 = NestedTerm.(1:2, Ref(NestedType(hs, [[2,3]]))) + +f = homomorphism(G_1212, G_12_2323; initial=[e1=>e3,e2=>e4]) +g = homomorphism(G_1212, G_1212_2323; initial=[e1=>e2,e2=>e2]) + +@test getvalue(getvalue(f[:Ob])) == [2,3] +@test getvalue(getvalue(g[:Ob])) == [1,2] +@test getindex.(Ref(f[:Hom]),[e1,e2]) == [1,2] +@test getindex.(Ref(g[:Hom]),[e1,e2]) == [2,2] + +apex, ι₁, ι₂ = pushout(f, g); + +@test argsof(ι₁(e1)) == NestedType(hs, [[1,2]]) +@test argsof(ι₁(e3)) == NestedType(hs, [[2,3]]) +@test ι₁(e3) == ι₁(e4) # these got merged together +@test argsof(ι₂(e1)) == NestedType(hs, [[2,3]]) +@test ι₂(e3) != ι₂(e4) # These are not merged together +@test argsof(ι₂(e3)) == NestedType(hs, [[3,4]]) + + +# ThCategory +walking_arrow = create_category([:a,:b], (f=(:a=>:b),)) +c2 = create_category([:a,:b], (;)) + +f, g = homomorphisms(c2, walking_arrow; monic=true) +apex, ι₁, ι₂ = pushout(f,g); + +# The two non-identity compositions are left undefined: +@test count(==(0),last.(collect(apex[:compose]))) == 2 + +end # module diff --git a/test/combinatorial/tests.jl b/test/combinatorial/tests.jl index 85bdc7cc..7a783401 100644 --- a/test/combinatorial/tests.jl +++ b/test/combinatorial/tests.jl @@ -3,5 +3,6 @@ module CombinatorialTests include("Constructor.jl") include("HomSearch.jl") include("Combinatorial.jl") +include("Limits.jl") end From 29720407b44bb3b594b49862d61cc8c40b20b24b Mon Sep 17 00:00:00 2001 From: Kris Brown Date: Fri, 29 Dec 2023 00:48:58 -0500 Subject: [PATCH 4/4] more colimits Doesn't terminate when it should: likely because all TGDs and all EGDs must be applied at once, rather than one at a time. more colimits remove test file rem --- src/combinatorial/CModels.jl | 61 ++++++---------- src/combinatorial/DataStructs.jl | 54 +++++++++----- src/combinatorial/HomSearch.jl | 3 + src/combinatorial/Limits.jl | 106 +++++++++++++++++++++++++--- src/combinatorial/TypeScopes.jl | 2 +- src/combinatorial/module.jl | 1 - src/syntax/GATs.jl | 2 +- src/syntax/gats/ast.jl | 5 ++ test/combinatorial/Combinatorial.jl | 9 +++ test/combinatorial/Limits.jl | 5 ++ test/combinatorial/tests.jl | 2 +- 11 files changed, 181 insertions(+), 69 deletions(-) diff --git a/src/combinatorial/CModels.jl b/src/combinatorial/CModels.jl index 256960d2..50c09d4c 100644 --- a/src/combinatorial/CModels.jl +++ b/src/combinatorial/CModels.jl @@ -10,7 +10,7 @@ import ...Syntax: GATContext, AlgSort, headof, argsof using ...Syntax.TheoryMaps: infer_type, bind_localctx using ..DataStructs -using ..DataStructs: NMIs, NMI, getsort, subterms, ScopedNMs, ScopedNM, Nest +using ..DataStructs: NM, NMIs, NMI, getsort, subterms, ScopedNMs, ScopedNM, Nest using ..TypeScopes: partition, subscope, vars, repartition, repartition_idx import ..DataStructs: CombinatorialModel, random_cardinalities @@ -103,6 +103,8 @@ function random_function(cards::NMIs, theory::GAT, s::AlgSort) rand_nm(cards, theory, lc, Int[], r, Int) end +empty_function(cards::NMIs, theory::GAT, s::AlgSort) = + rand_nm(cards, theory, getcontext(theory, s), Int[], [0]) """ Random matrix for some typescope with uniform sampling of `vals`. """ function rand_nm(d::NMIs,t::GAT,lc::TypeScope, choices::Vector{Int}, @@ -123,14 +125,14 @@ function rand_nm(d::NMIs, theory::GAT, lc::TypeScope, # Choices has decided values for some number of the partitions i = findfirst(==(length(choices)), plens) if i == length(p) + 1 # we have fully determined the whole context - NMI(f(choices)) # pick an element to go in the leaf cell + NM{T}(f(choices)) # pick an element to go in the leaf cell else - lens = map(LID.(ranges[i])) do idx + lens = map(LID.(ranges[i])) do idx vs = sort(getvalue.(collect(vars(lc, idx)))) idx_choices = choices[vs] Base.OneTo(length(enum(d, theory, subscope(lc,idx), idx_choices))) end - NMI(Nest(Array{NestedMatrix{T}}(map(Iterators.product(lens...)) do idx + NM{T}(Nest(Array{NestedMatrix{T}}(map(Iterators.product(lens...)) do idx rand_nm(d, theory, lc, [choices...,idx...], f, T) end)); depth = length(p) - i + 1) end @@ -206,15 +208,14 @@ function add_part!(m::CombinatorialModel, type::NestedType)::NestedTerm m[type] = NMI(new_cardinality) for s in sorts(T) getsort(type) ∈ sortsignature(getvalue(T, methodof(s))) || continue - tc = getcontext(T, s) - new_nm = rand_nm(m.sets, T, tc, Int[], [0]) # all empty sets + new_nm = empty_function(m.sets, T, s) for (e, val) in enums[s] # copy over old data new_nm[e] = NMI(val) end m[s] = new_nm end for s in funsorts(T) - new_fun = random_function(m.sets, T, s) + new_fun = empty_function(m.sets, T, s) for (e, v) in m[s] # copy over old data new_fun[e] = NMI(v) end @@ -227,6 +228,10 @@ end Remove an element of a dependent set, specified by a NestedTerm. This has an effect on any sets dependent on that element. Removal involves pop-and-swap. +Rather than recursively delete parts, when a function output refers to the +deleted term, the value is replaced with "-1" (as "0" has a semantics of being a +free value). + This implementation creates modified NestedMatrices and then replaces the ones in the CombinatorialModel. A more sophisticated algorithm would do this inplace. """ @@ -234,10 +239,11 @@ function rem_part!(m::CombinatorialModel, term::NestedTerm) T = gettheory(m) type = argsof(term) swapped_index = getvalue(m[type]) + swapterm = NestedTerm(swapped_index, type) m[type] = NMI(swapped_index - 1) for s in sorts(T) getsort(type) ∈ sortsignature(getvalue(T, methodof(s))) || continue - new_nm = rand_nm(m.sets, T, getcontext(T, s), Int[], [0]) # all empty sets + new_nm = empty_function(m.sets, T, s) for e in TypeIterator(ScopedNM(new_nm, T, s)) new_e = deepcopy(e) for (i, subterm) in enumerate(subterms(T, e)) @@ -250,7 +256,7 @@ function rem_part!(m::CombinatorialModel, term::NestedTerm) m[s] = new_nm end for s in funsorts(T) - new_fun = random_function(m.sets, T, s) + new_fun = empty_function(m.sets, T, s) for e in TypeIterator(ScopedNM(new_fun, T, s)) # copy over old data new_e = deepcopy(e) for (i, subterm) in enumerate(subterms(T, e)) @@ -259,7 +265,13 @@ function rem_part!(m::CombinatorialModel, term::NestedTerm) end end val = m(new_e) - new_fun[e] = (val == term ? swapped_index : getvalue(val)) |> NMI + new_fun[e] = (if val == term + -1 # sentinel value representing an undefined element + elseif val == swapterm + getvalue(term) + else + getvalue(val) + end) |> NMI end m[s] = new_fun end @@ -276,38 +288,11 @@ function (m::CombinatorialModel)(term::NestedType)::NestedTerm rtype = getvalue(T[methodof(srt)]).type rsort = AlgSort(rtype) lc = bind_localctx(GATContext(T, getcontext(T, srt)), rtype) - flat_idxs = map(sort(collect(pairs(lc)); by=x->getvalue(x[1].lid))) do (_,b) + flat_idxs = map(sort(collect(pairs(lc)); by=x->getvalue(x[1].lid))) do (_, b) GATs.isvariable(b) ? term[getvalue(b.body.lid)] : error("Bad ret type $b") end idxs = repartition_idx(T, rsort, flat_idxs) NestedTerm(getvalue(m[term]), NestedType(rsort, idxs)) end -# Enforce equations -################### - -"""Merely enforce equalities implied by equations of GAT via chase""" -function eq_saturate!(m::CombinatorialModel) - error("NOT IMPLEMENTED YET") -end - -""" -Enforce equalities implied by equations of GAT via chase as well as create new -elements of dependent sets for every undefined function output. This process -can potentially not terminate. - -Returns a boolean indicating whether or not the process terminated and an -integer describing how many steps it took. -""" -function saturate!(m::CombinatorialModel; steps::Int=100) - for step in 1:steps - eq_saturate!(m) - error("NOT IMPLEMENTED YET") - # ... && return (true, step) - end - false, steps -end - -is_saturated(m::CombinatorialModel) = last(saturate!(m)) == 0 - end # module diff --git a/src/combinatorial/DataStructs.jl b/src/combinatorial/DataStructs.jl index 11efd3dc..31d5ead1 100644 --- a/src/combinatorial/DataStructs.jl +++ b/src/combinatorial/DataStructs.jl @@ -76,6 +76,8 @@ function getvalue(n::Nest{T})::Array{NM{T}} where T n.val end +Base.zero(::Type{NM{T}}) where T = NM{T}(zero(T)) + Base.length(nm::NM)::Int = (nm.depth == 0) ? 1 : sum(length.(getvalue(getvalue(nm))); init=0) @@ -213,8 +215,8 @@ Base.setindex!(n::ScopedNM{T}, i, k) where T = setindex!(getvalue(n), i, k) map_nm(fun, ret_type, n::ScopedNM; kw...) = ScopedNM(map_nm(fun, ret_type, getvalue(n); kw...), getcontext(n), getsort(n)) -const_nm(n::ScopedNM, v; copy=false) = - ScopedNM(const_nm(getvalue(n), v; copy), getcontext(n), getsort(n)) +const_nm(n::ScopedNM, v; copy=false, type=nothing) = + ScopedNM(const_nm(getvalue(n), v; copy, type), getcontext(n), getsort(n)) const AlgDict{T} = Dict{AlgSort, NM{T}} @@ -376,9 +378,13 @@ This ignores the leaf values of the NestedMatrix. struct TypeIterator s::ScopedNM{Int} end + Base.length(s::TypeIterator) = length(s.s) + Base.eltype(::Type{TypeIterator}) = NestedType + Base.iterate(s::TypeIterator) = iterate(s, Iterators.Stateful(s.s)) + Base.iterate(s::TypeIterator, it) = isempty(it) ? nothing : (NestedType(getsort(s.s), popfirst!(it)[1]), it) @@ -411,10 +417,6 @@ function Base.iterate(s::TermIterator, state) end end - -# Base.iterate(s::ScopedNM{T}, i) where T = iterate(getvalue(s), i) - - # Models ######## @@ -467,8 +469,10 @@ function Base.setindex!(m::ScopedNMs, val, t::Nested) m[getsort(t)][t] = val end -Base.setindex!(m::Comb, data::NMI, t::NestedType) = - m.sets[getsort(t)][getvalue(t)] = data +function Base.setindex!(m::Comb, data::NMI, t::NestedType) + sort = getsort(t) + (haskey(m.sets, sort) ? m.sets : m.funs)[sort][getvalue(t)] = data +end function random_cardinalities end # defined in CModels @@ -510,39 +514,51 @@ end const Morphism = CombinatorialModelMorphism Base.getindex(c::Morphism, k::AlgSort) = components(c)[k] + Base.getindex(c::Morphism, k::Symbol) = components(c)[AlgSort(gettheory(c), k)] +Base.getindex(c::Morphism, n::Nested) = components(c)[getsort(n)][n] + gettheory(c::Morphism) = gettheory(c.dom) components(c::Morphism) = c.components -function (f::Morphism)(t::NestedType)::NestedType - T, srt = gettheory(f), getsort(t) - NestedType(srt, repartition_idx(T, srt, Int[getvalue.(f.(subterms(T, t)))...])) +(f::Morphism)(t::NestedTerm)::NestedTerm = + apply_morphism(gettheory(f), components(f), t) + +(f::Morphism)(t::NestedType)::NestedType = + apply_morphism(gettheory(f), components(f), t) + +function apply_morphism(T::GAT, comps::NMVIs, t::NestedTerm)::NestedTerm + val = getvalue(t) == 0 ? 0 : comps[t] + NestedTerm(val, apply_morphism(T, comps, argsof(t))) end -function (f::Morphism)(t::NestedTerm)::NestedTerm - NestedTerm(components(f)[getsort(t)][t], f(argsof(t))) +function apply_morphism(T::GAT, comps::NMVIs, t::NestedType)::NestedType + srt = getsort(t) + NestedType(srt, repartition_idx(T, srt, Int[getvalue.(apply_morphism.(Ref(T), Ref(comps), subterms(T, t)))...])) end -function is_natural(m::Morphism) - T = gettheory(m) +"""E-graphs are needed to handle cases where dom/codom have free elements""" +function naturality_failures(m::Morphism) + T, res = gettheory(m), [] for (funsort, nestedmatrix) in m.dom.funs - for (idx, _) in collect(nestedmatrix) + for dom_funapp in TypeIterator(nestedmatrix) # apply operation, then map over morphism - dom_funapp = NestedType(funsort, idx) dom_funres = m.dom(dom_funapp) op_f = m(dom_funres) # map arguments to operation over morphism, then apply operation cod_idxs = getvalue.(m.(subterms(T, dom_funapp))) cod_funapp = NestedType(funsort, repartition_idx(T, funsort, cod_idxs)) f_op = m.codom(cod_funapp) - op_f == f_op || return false + op_f == f_op || push!(res, (funsort, dom_funapp, cod_funapp, op_f, f_op)) end end - true + res end +is_natural(m::Morphism) = isempty(naturality_failures(m)) + # Category instance ################### diff --git a/src/combinatorial/HomSearch.jl b/src/combinatorial/HomSearch.jl index 6ec25d70..ef20c599 100644 --- a/src/combinatorial/HomSearch.jl +++ b/src/combinatorial/HomSearch.jl @@ -16,6 +16,9 @@ import ...Syntax: gettheory, argsof Returns `nothing` if no homomorphism exists. The homomorphism problem is NP-complete and thus this procedure generally runs in exponential time. It works best when the domain object is small. + +NOTE: E-graphs are needed to handle cases where dom/codom have free elements. + """ function homomorphism(X::Comb, Y::Comb; kw...) result = nothing diff --git a/src/combinatorial/Limits.jl b/src/combinatorial/Limits.jl index ecba3000..2aaf8b2e 100644 --- a/src/combinatorial/Limits.jl +++ b/src/combinatorial/Limits.jl @@ -1,13 +1,22 @@ +""" +Currently just colimits. + +Rather than a whole reimplementation of the generic (co)limit and diagram +infrastructure of Catlab, we opt for specific implementations of initial, +coproduct, and pushout. This could form the starting point for a generic +implementation down the line. +""" module Limits -export pushout, initial, terminal +export pushout, initial, terminal, coproduct, oplus, copair using ..DataStructs -using ..DataStructs: Idx, NMI, NMIs, NMVIs, ScopedNM, Morphism, Comb, map_nm +using ..DataStructs: Idx, NMI, NMIs, NMVI, NMVIs, ScopedNM, ScopedNMs,Morphism, + Comb, map_nm, apply_morphism, const_nm using ..CModels -using ..CModels: rand_nm, random_function +using ..CModels: empty_function # rand_nm, using ...Syntax using ...Stdlib -using ...Models +using ...Models: @withmodel using .ThCategory using DataStructures: IntDisjointSets, find_root! @@ -37,7 +46,7 @@ function pushout(f::Morphism, g::Morphism) # Populate cardinality data of apex and populate maps ι₁, ι₂ for s in sorts(T) - apex.sets[s] = ScopedNM(rand_nm(apex.sets, T, getcontext(T, s), Int[],[0]), T, s) # apex w/ zeros + apex.sets[s] = ScopedNM(empty_function(apex.sets, T, s), T,s) # apex w/ zeros (Bs, Bs⁻¹), (Cs, Cs⁻¹) = map([B=>false,C=>true]) do (X, offset) Xs = collect(TermIterator(X[s])) Xs => Dict([v => (i + (offset ? sum(B[s]) : 0)) for (i, v) in enumerate(Xs)]) @@ -73,20 +82,101 @@ function pushout(f::Morphism, g::Morphism) end # Populate function data for s in funsorts(T) - apex.funs[s] = ScopedNM(rand_nm(apex.sets, T, getcontext(T, s), Int[], [0]), T, s) + apex.funs[s] = ScopedNM(empty_function(apex.sets, T, s), T, s) for bargs in TypeIterator(B[s]) fbargs = ι₁(bargs) - apex.funs[s][fbargs] = NMI(getvalue(ι₁(B(bargs)))) + bval = B(bargs) + getvalue(bval) > 0 || continue + apex.funs[s][fbargs] = NMI(getvalue(ι₁(bval))) end for cargs in TypeIterator(C[s]) gcargs = ι₂(cargs) apex.funs[s][gcargs] = NMI(getvalue(ι₂(C(cargs)))) end end + ι₁.dom == B || error("Bad i1") + ι₂.dom == C || error("Bad i2") return (apex, ι₁, ι₂) end end -# TODO Implement ThPushout +""" +Coproduct of (non-empty) list of models. +""" +function coproduct(Xs::Vector{Comb}) + M = first(Xs) + T = gettheory(M) + res = initial(T) + comps = [ScopedNMs(T, Dict{AlgSort, NMVI}()) => X for X in Xs] + for s in sorts(T) + res[s] = empty_function(res.sets, T, s) + for (comp, X) in comps + function fun(idx::Vector{<:Idx}, v::Int)::Vector{Int} + nm = res[s][apply_morphism(T, comp, NestedType(s,idx))] + vec = (1:v) .+ getvalue(nm) + nm.data = getvalue(nm) + v + collect(vec) + end + comp[s] = map_nm(fun, Vector{Int}, X[s]; index=true) + end + end + for s in funsorts(T) + res[s] = empty_function(res.sets, T, s) + for (comp, X) in comps + for args in TypeIterator(X[s]) + res[apply_morphism(T, comp, args)] = NMI(getvalue(apply_morphism(T, comp, X(args)))) + end + end + end + [Morphism(comp, X, res) for (comp, X) in comps] +end + + +""" +Take a nonempty collection of maps Aᵢ → B and make a single map ΣA → B +""" +function copair(vs::Vector{Morphism}) + ι = coproduct([v.dom for v in vs]) + all([v.codom == first(vs).codom for v in vs]) || error("Cannot copair") + dom, codom = [first(x).codom for x in [ι, vs]] + comps = Dict(map(sorts(gettheory(dom))) do s + res = const_nm(getvalue(dom[s]), Int[]; copy=true, type=Vector{Int}) + for (i,v) in zip(ι, vs) + for (idx, mapping) in v[s] + append!(getvalue(res[i(NestedType(s, idx))]), mapping) + end + end + s => res + end) + res = Morphism(comps, dom, codom) + is_natural(res) || error("unnatural") + res +end + +""" +Take a nonempty collection of maps Aᵢ → Bᵢ and make a single map ΣA → ΣB +""" +function oplus(vs::Vector{Morphism}) + Aι = coproduct([v.dom for v in vs]) + Bι = coproduct([v.codom for v in vs]) + dom, codom = [first(x).codom for x in [Aι, Bι]] + comps = Dict(map(sorts(gettheory(dom))) do s + res = const_nm(getvalue(dom[s]), Int[]; copy=true, type=Vector{Int}) + for (Ai, v, Bi) in zip(Aι, vs, Bι) + for (idx, mapping) in v[s] + A_args = NestedType(s, idx) + mapping′ = Bi.(v.(NestedTerm.(1:length(mapping), Ref(A_args)))) + append!(getvalue(res[Ai(A_args)]), getvalue.(mapping′)) + end + end + s => res + end) + res = Morphism(comps, dom, codom) + is_natural(res) || error("unnatural") + res +end + + +# TODO Implement ThPushout for CombinatorialModelC end # module \ No newline at end of file diff --git a/src/combinatorial/TypeScopes.jl b/src/combinatorial/TypeScopes.jl index e7007a27..ec7a2d15 100644 --- a/src/combinatorial/TypeScopes.jl +++ b/src/combinatorial/TypeScopes.jl @@ -34,7 +34,7 @@ function partition(t::TypeScope)::Vector{Vector{LID}} res end -"""Get all idents""" +"""Get all idents which appear, explicitly or implcitly (in types)""" vars(ts::TypeScope, t::AlgAST)::Set{LID} = vars(ts, t.body) vars(ts::TypeScope, t::GATs.MethodApp)::Set{LID} = union(Set{LID}(),vars.(Ref(ts), t.args)...) diff --git a/src/combinatorial/module.jl b/src/combinatorial/module.jl index c78d5088..ca9a46a6 100644 --- a/src/combinatorial/module.jl +++ b/src/combinatorial/module.jl @@ -9,7 +9,6 @@ include("CModels.jl") include("HomSearch.jl") include("Limits.jl") - @reexport using .TypeScopes @reexport using .DataStructs @reexport using .Visualization diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl index 0c8a8f20..bb23b21f 100644 --- a/src/syntax/GATs.jl +++ b/src/syntax/GATs.jl @@ -5,7 +5,7 @@ export Constant, AlgTerm, AlgType, AlgAST, AlgTypeConstructor, AlgAccessor, AlgAxiom, AlgStruct, AlgDot, AlgFunction, typesortsignature, sortsignature, getdecl, GATSegment, GAT, GATContext, gettheory, gettypecontext, allmethods, - resolvemethod, funsorts, + resolvemethod, funsorts, getvariables, termcons,typecons, accessors, structs, primitive_sorts, struct_sorts, equations, build_infer_expr, compile, sortcheck, allnames, sorts, sortname, InCtx, TermInCtx, TypeInCtx, headof, argsof, methodof, bodyof, argcontext, diff --git a/src/syntax/gats/ast.jl b/src/syntax/gats/ast.jl index 6cfc7120..5be14d27 100644 --- a/src/syntax/gats/ast.jl +++ b/src/syntax/gats/ast.jl @@ -137,6 +137,11 @@ function AlgSort(c::Context, t::AlgTerm) end end +getvariables(t::AlgTerm)::Set{Ident} = getvariables(bodyof(t)) +getvariables(t::MethodApp)::Set{Ident} = + union(Set{Ident}(), getvariables.(argsof(t))...) +getvariables(i::Ident)::Set{Ident} = Set([i]) + """ `Eq` diff --git a/test/combinatorial/Combinatorial.jl b/test/combinatorial/Combinatorial.jl index 03050c3c..56dcf31d 100644 --- a/test/combinatorial/Combinatorial.jl +++ b/test/combinatorial/Combinatorial.jl @@ -8,6 +8,7 @@ using GATlab.Combinatorial.CModels: enum,random_cardinalities using GATlab.Combinatorial.Visualization: renderstr using GATlab.NonStdlib.NonStdTheories: Th2Cat, ThTwoCat using GATlab.Syntax.TheoryMaps: bind_localctx +using ..Constructor # Unpack theory T = Th2Cat.Meta.theory; @@ -80,4 +81,12 @@ add_part!(m, ntos) rem_part!(m, NestedTerm(1,ntos)) @test last.(collect(m[idsort])) == [0, 1] + +# ThCategory +############ +is = AlgSort(T, :id) +X = create_category([:A,:B],(f=(:A=>:B),g=(:A=>:A)), [[Symbol[],[:g,:g]]]) +rem_part!(X, NestedTerm(1, NestedType(hs, [[1,1]]))) +@test getvalue(X[NestedType(is,[[1]])]) == -1 + end # module diff --git a/test/combinatorial/Limits.jl b/test/combinatorial/Limits.jl index 125681e6..fcefd3b4 100644 --- a/test/combinatorial/Limits.jl +++ b/test/combinatorial/Limits.jl @@ -36,12 +36,17 @@ apex, ι₁, ι₂ = pushout(f, g); # ThCategory +############ + walking_arrow = create_category([:a,:b], (f=(:a=>:b),)) c2 = create_category([:a,:b], (;)) f, g = homomorphisms(c2, walking_arrow; monic=true) apex, ι₁, ι₂ = pushout(f,g); +@test is_natural(copair([f,g])) +@test is_natural(oplus([f,g])) + # The two non-identity compositions are left undefined: @test count(==(0),last.(collect(apex[:compose]))) == 2 diff --git a/test/combinatorial/tests.jl b/test/combinatorial/tests.jl index 7a783401..dc7d1567 100644 --- a/test/combinatorial/tests.jl +++ b/test/combinatorial/tests.jl @@ -1,8 +1,8 @@ module CombinatorialTests include("Constructor.jl") -include("HomSearch.jl") include("Combinatorial.jl") +include("HomSearch.jl") include("Limits.jl") end