From 06be9f03715c15d8b9a00a6834ffaeb6400ca041 Mon Sep 17 00:00:00 2001 From: Kris Brown Date: Wed, 20 Sep 2023 17:13:48 -0700 Subject: [PATCH] generalize typemap to be valued in TypeInCtx remove reference --- src/stdlib/theorymaps/Maps.jl | 11 +++- src/syntax/GATs.jl | 61 ++++++++++++++++------- src/syntax/Scopes.jl | 21 ++++++-- src/syntax/TheoryMaps.jl | 94 +++++++++++++++++++---------------- test/syntax/GATs.jl | 6 ++- test/syntax/TheoryMaps.jl | 15 +++++- 6 files changed, 141 insertions(+), 67 deletions(-) diff --git a/src/stdlib/theorymaps/Maps.jl b/src/stdlib/theorymaps/Maps.jl index f1ef772e..d69bf108 100644 --- a/src/stdlib/theorymaps/Maps.jl +++ b/src/stdlib/theorymaps/Maps.jl @@ -1,6 +1,6 @@ module Maps -export SwapMonoid, NatPlusMonoid, PreorderCat +export SwapMonoid, NatPlusMonoid, PreorderCat, OpCat using ...StdTheories using ....Syntax @@ -19,6 +19,15 @@ NatPlusMonoid = @theorymap ThMonoid => ThNatPlus begin (x ⋅ y) ⊣ [x, y] => x+y ⊣ [(x, y)::ℕ] end + +OpCat = @theorymap ThCategory => ThCategory begin + Ob => Ob + Hom => Hom(codom,dom) ⊣ [dom::Ob, codom::Ob] + compose(f, g) ⊣ [a::Ob, b::Ob, c::Ob, f::(a → b), g::(b → c)] => + compose(g, f) ⊣ [a::Ob, b::Ob, c::Ob, f::(b → a), g::(c → b)] + id(a) ⊣ [a::Ob] => id(a) ⊣ [a::Ob] +end + """Preorders are categories""" PreorderCat = @theorymap ThCategory => ThPreorder begin Ob => default diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl index 9cb73d4e..69a3eb8e 100644 --- a/src/syntax/GATs.jl +++ b/src/syntax/GATs.jl @@ -4,7 +4,7 @@ export Constant, AlgTerm, AlgType, AlgTermConstructor, AlgTypeConstructor, AlgAxiom, sortsignature, JudgmentBinding, GATSegment, GAT, sortcheck, allnames, sorts, sortname, termcons, typecons, accessors, equations, build_infer_expr, compile, - TermInCtx, headof, argsof, argcontext + InCtx, TermInCtx, TypeInCtx, headof, argsof, argcontext using ..Scopes using ..ExprInterop @@ -173,17 +173,19 @@ permitted. const SortScope = Scope{AlgSort, Nothing} """ -A term with an accompanying type scope, e.g. +A type or term with an accompanying type scope, e.g. - (a,b)::R ------------ - a*(a+b) + (a,b)::R (a,b)::Ob +----------- or ---------- + a*(a+b) Hom(a,b) """ -@struct_hash_equal struct TermInCtx +@struct_hash_equal struct InCtx{T<:TrmTyp} ctx::TypeScope - trm::AlgTerm + trm::T end +const TermInCtx = InCtx{AlgTerm} +const TypeInCtx = InCtx{AlgType} """ `sortcheck(ctx::Context, t::AlgTerm)` @@ -499,14 +501,29 @@ function compile(expr_lookup::Dict{Ident}, term::AlgTerm; theorymodule=nothing) end end -"""Get the canonical term associated with a term constructor""" -function TermInCtx(g::GAT, k::Ident) +InCtx(g::GAT, k::Ident) = + (getvalue(g[k]) isa AlgTermConstructor ? TermInCtx : TypeInCtx)(g, k) + +""" +Get the canonical term + ctx associated with a term constructor. +""" +function InCtx{AlgTerm}(g::GAT, k::Ident) tcon = getvalue(g[k]) lc = argcontext(tcon) ids = reverse(reverse(idents(lc))[1:(length(tcon.args))]) TermInCtx(lc, AlgTerm(k, AlgTerm.(ids))) end +""" +Get the canonical type + ctx associated with a type constructor. +""" +function InCtx{AlgType}(g::GAT, k::Ident) + tcon = getvalue(g[k]) + lc = argcontext(tcon) + TypeInCtx(lc, AlgType(k, AlgTerm.(idents(lc)))) +end + + """ Infer the type of the term of a term. If it is not in context, recurse on its arguments. The term constructor's output type yields the resulting type once @@ -533,6 +550,7 @@ function infer_type(theory::GAT, t::TermInCtx) if hasident(t.ctx, head) getvalue(t.ctx[head]) # base case else + #println("Inferring type of $t w/ head $head") tc = getvalue(theory[head]) eqs = equations(theory, head) typed_terms = Dict{Ident, Pair{AlgTerm,AlgType}}() @@ -560,14 +578,16 @@ Take a term constructor and determine terms of its local context. This function is mutually recursive with `infer_type`. """ -function bind_localctx(theory::GAT, t::TermInCtx) +function bind_localctx(theory::GAT, t::InCtx{T}) where T head = headof(t.trm) tc = getvalue(theory[head]) eqs = equations(theory, head) typed_terms = Dict{Ident, Pair{AlgTerm,AlgType}}() + #println("BINDING LOCAL CONTEXT $t") for (i,a) in zip(tc.args, t.trm.args) + #println("tc.arg $i => t.trm arg $a") tt = (a => infer_type(theory, TermInCtx(t.ctx, a))) typed_terms[ident(tc.args, name=nameof(i))] = tt end @@ -585,13 +605,13 @@ function bind_localctx(theory::GAT, t::TermInCtx) end """ Replace idents with AlgTerms. """ -function substitute_term(t::TrmTyp, dic::Dict{Ident,AlgTerm}) +function substitute_term(t::T, dic::Dict{Ident,AlgTerm}) where T<:TrmTyp iden = headof(t) if haskey(dic, iden) isempty(t.args) || error("Cannot substitute a term with arguments") dic[iden] else - AlgTerm(headof(t), substitute_term.(argsof(t), Ref(dic))) + T(headof(t), substitute_term.(argsof(t), Ref(dic))) end end @@ -716,23 +736,26 @@ function parseaxiom(c::Context, localcontext, type_expr, e; name=nothing) end end -function ExprInterop.fromexpr(c::Context, e, ::Type{TermInCtx}) +function ExprInterop.fromexpr(c::Context, e, ::Type{InCtx{T}}) where T (binding, localcontext) = @match normalize_decl(e) begin Expr(:call, :(⊣), binding, Expr(:vect, args...)) => (binding, parsetypescope(c, args)) e => (e, TypeScope()) end c′ = AppendScope(c, localcontext) bound = Dict([nameof(b) => getvalue(b) for b in getbindings(localcontext)]) - t = ExprInterop.fromexpr(c′, binding, AlgTerm; bound=bound) - TermInCtx(localcontext, t) + t = ExprInterop.fromexpr(c′, binding, T; bound=bound) + InCtx{T}(localcontext, t) end -ExprInterop.toexpr(c::Context, tic::TermInCtx) = let c′=AppendScope(c,tic.ctx); - Expr(:call, :(⊣), ExprInterop.toexpr(c′, tic.trm), ExprInterop.toexpr(c′, tic.ctx)) +function ExprInterop.toexpr(c::Context, tic::InCtx; kw...) + c′=AppendScope(c,tic.ctx) + etrm = ExprInterop.toexpr(c′, tic.trm; kw...) + ectx = ExprInterop.toexpr(c′, tic.ctx; kw...) + Expr(:call, :(⊣), etrm, ectx) end -ExprInterop.toexpr(c::Context, ts::TypeScope) = - Expr(:vect,[Expr(:(::), nameof(b), toexpr(c, getvalue(b))) for b in ts]...) +ExprInterop.toexpr(c::Context, ts::TypeScope; kw...) = + Expr(:vect,[Expr(:(::), nameof(b), toexpr(c, getvalue(b); kw...)) for b in ts]...) ExprInterop.toexpr(c::Context, at::Binding{AlgType, Nothing}) = Expr(:(::), nameof(at), ExprInterop.toexpr(c, getvalue(at))) diff --git a/src/syntax/Scopes.jl b/src/syntax/Scopes.jl index a4cb9fea..da4e972e 100644 --- a/src/syntax/Scopes.jl +++ b/src/syntax/Scopes.jl @@ -214,8 +214,23 @@ disambiguated by a signature in `Sig` in the case of overloading. end end -function Base.show(io::IO, b::Binding) - print(io, isnothing(nameof(b)) ? "_" : nameof(b)) +"""Type for printing out bindings with colored keys""" +@struct_hash_equal struct ScopedBinding + scope::ScopeTag + binding::Binding +end + +Base.show(io::IO, b::ScopedBinding) = + Base.show(io, b.binding; crayon=tagcrayon(b.scope)) + +function Base.show(io::IO, b::Binding; crayon=nothing) + bname = isnothing(nameof(b)) ? "_" : nameof(b) + if isnothing(crayon) || !(get(io, :color, true)) + print(io, bname) + else + print(io, crayon, bname) + print(io, inv(crayon)) + end if length(getaliases(b)) > 1 print(io, "(aliases=") join(io, filter(x -> x != nameof(b), getaliases(b)), ", ") @@ -407,7 +422,7 @@ end function Base.show(io::IO, x::Scope) print(io, "{") for (i, b) in enumerate(x.bindings) - print(io, b) + print(io, ScopedBinding(gettag(x), b)) if i < length(x.bindings) print(io, ", ") end diff --git a/src/syntax/TheoryMaps.jl b/src/syntax/TheoryMaps.jl index 544c1b84..7c34b697 100644 --- a/src/syntax/TheoryMaps.jl +++ b/src/syntax/TheoryMaps.jl @@ -4,7 +4,7 @@ export IdTheoryMap, TheoryIncl, AbsTheoryMap, TheoryMap, @theorymap, using ..GATs, ..Scopes, ..ExprInterop using ..Scopes: unsafe_pushbinding! -using ..GATs: bindingexprs, bind_localctx, substitute_term +using ..GATs: InCtx, TrmTyp, bindingexprs, bind_localctx, substitute_term import ..ExprInterop: toexpr, fromexpr @@ -23,13 +23,19 @@ thought of in many ways. The main methods for an AbsTheoryMap to implement are: - dom, codom, - - typemap: A dictionary of Ident (of AlgTypeConstructor in domain) to AlgSort - (This must be a AlgSort of the same arity.) + - typemap: A dictionary of Ident (of AlgTypeConstructor in domain) to + TypeInCtx (The TypeScope of the TypeInCtx must be structurally + identical to the localcontext of the type constructor + associated with the key). - termmap: A dictionary of Ident (of AlgTermConstructor in domain) to TermInCtx. (The TypeScope of the TrmInCtx must be structurally identical to the localcontext + args of the term constructor associated with the key.) - + +The requirement that the values of `typemap` and `termmap` be structurally +identical to the contexts in the domain can eventually be relaxed (to allow +reordering, additional derived elements, dropping unused arguments), but for now +we require this for simplicity. """ abstract type AbsTheoryMap end @@ -40,7 +46,7 @@ dom(f::AbsTheoryMap)::GAT = f.dom # assume this exists by default codom(f::AbsTheoryMap)::GAT = f.codom # assume this exists by default function compose(f::AbsTheoryMap, g::AbsTheoryMap) - typmap = Dict(k => typemap(g)[v.ref] for (k,v) in pairs(typemap(f))) + typmap = Dict(k => g(v) for (k, v) in pairs(typemap(f))) trmmap = Dict(k => g(v) for (k, v) in pairs(termmap(f))) TheoryMap(dom(f), codom(g), typmap, trmmap) end @@ -60,26 +66,24 @@ end """Map a context in the domain theory into a context of the codomain theory""" function (f::AbsTheoryMap)(ctx::TypeScope) - scope = TypeScope() - cache = Dict{Symbol, AlgTerm}() - for b in ctx - argnames = nameof.(headof.(b.value.args)) - val = AlgType(f(b.value.head).ref, AlgTerm[cache[a] for a in argnames]) + fctx = TypeScope() + for i in 1:length(ctx) + b = ctx[LID(i)] + partial_scope = Scope(getbindings(ctx)[1:i-1]; tag=gettag(ctx)) + val = f(partial_scope, getvalue(b), fctx) new_binding = Binding{AlgType, Nothing}(b.primary, b.aliases, val, b.sig) - cache[nameof(b)] = AlgTerm(Ident(gettag(scope), LID(length(scope)+1), - nameof(new_binding))) - unsafe_pushbinding!(scope, new_binding) + unsafe_pushbinding!(fctx, new_binding) end - scope + fctx end -function (f::AbsTheoryMap)(t::TermInCtx) +function (f::AbsTheoryMap)(t::InCtx{T}) where T fctx = f(t.ctx) - TermInCtx(fctx, f(t.ctx, t.trm, fctx)) + InCtx{T}(fctx, f(t.ctx, t.trm, fctx)) end -""" Map a term `t` in context `c` along `f`. """ -function (f::AbsTheoryMap)(ctx::TypeScope, t::AlgTerm, fctx=nothing)::AlgTerm +""" Map a term (or type) `t` in context `c` along `f`. """ +function (f::AbsTheoryMap)(ctx::TypeScope, t::T, fctx=nothing) where {T<:TrmTyp} fctx = isnothing(fctx) ? f(ctx) : fctx head = headof(t) if hasident(ctx, head) @@ -93,19 +97,23 @@ function (f::AbsTheoryMap)(ctx::TypeScope, t::AlgTerm, fctx=nothing)::AlgTerm for x in [termcon.args, termcon.localcontext]) # new_term has same context as termcon, so recursively map over components - lc = bind_localctx(f.dom, TermInCtx(ctx,t)) - flc = Dict(retag(rt_dict, k) => f(ctx, v, fctx) for (k, v) in pairs(lc)) - + lc = bind_localctx(f.dom, InCtx{T}(ctx, t)) + flc = Dict{Ident, AlgTerm}(map(collect(pairs(lc))) do (k, v) + if hasident(termcon.args, k) # offset when squashing localcontext and args + k = Ident(gettag(k), LID(getlid(k).val+length(termcon.localcontext)), nameof(k)) + end + retag(rt_dict, k) => f(ctx, v, fctx) + end) substitute_term(new_term.trm, flc) end end function toexpr(m::AbsTheoryMap) typs = map(collect(typemap(m))) do (k, v) - Expr(:call, :(=>), toexpr(dom(m), k), toexpr(codom(m), v)) - end + Expr(:call, :(=>), toexpr(dom(m), k), toexpr(codom(m), v)) + end trms = map(collect(termmap(m))) do (k,v) - domterm = toexpr(dom(m), TermInCtx(dom(m), k)) + domterm = toexpr(dom(m), InCtx(dom(m), k)) Expr(:call, :(=>), domterm, toexpr(codom(m), v)) end Expr(:block, typs...,trms...) @@ -146,7 +154,7 @@ A theory inclusion has a subset of scopes end typemap(ι::Union{IdTheoryMap,TheoryIncl}) = - Dict(k => AlgSort(k) for k in typecons(dom(ι))) + Dict(k => TypeInCtx(dom(ι), k) for k in typecons(dom(ι))) termmap(ι::Union{IdTheoryMap,TheoryIncl}) = Dict(k=>TermInCtx(dom(ι), k) for k in termcons(dom(ι))) @@ -170,28 +178,27 @@ TODO: check that it is well-formed, axioms are preserved. @struct_hash_equal struct TheoryMap <: AbsTheoryMap dom::GAT codom::GAT - typemap::Dict{Ident,AlgSort} + typemap::Dict{Ident,TypeInCtx} termmap::Dict{Ident,TermInCtx} function TheoryMap(dom, codom, typmap, trmmap) missing_types = setdiff(Set(keys(typmap)), Set(typecons(dom))) missing_terms = setdiff(Set(keys(trmmap)), Set(termcons(dom))) isempty(missing_types) || error("Missing types $missing_types") isempty(missing_terms) || error("Missing types $missing_terms") - f = new(dom, codom, typmap, trmmap) - - # Check type constructors are coherent - for (k, v) in pairs(typmap) - f_args = f(argcontext(getvalue(dom[k]))) - arg_fs = argcontext(getvalue(codom[v.ref])) - err = "Bad type map $k => $v ($f_args != $arg_fs)" - Scopes.equiv(f_args, arg_fs) || error(err) + + tymap′, trmap′ = map([typmap, trmmap]) do tmap + Dict(k => v isa Ident ? InCtx(codom, v) : v for (k,v) in pairs(tmap)) end - # Check term constructors are coherent - for (k, v) in pairs(trmmap) - f_args = f(argcontext(getvalue(dom[k]))) - arg_fs = v.ctx - err = "Bad term map $k => $v ($f_args != $arg_fs)" - Scopes.equiv(f_args, arg_fs) || error(err) + + f = new(dom, codom, tymap′, trmap′) + # Check type/term constructors are coherent + for (typtrm, tmap) in ["type"=>tymap′, "term"=>trmap′] + for (k, v) in pairs(tmap) + f_args = f(argcontext(getvalue(dom[k]))) + arg_fs = v.ctx + err = "Bad $typtrm map $k => $v ($f_args != $arg_fs)" + Scopes.equiv(f_args, arg_fs) || error(err) + end end f @@ -209,15 +216,18 @@ TODO: we currently ignore LineNumberNodes. TheoryMap data structure could TODO: handle more ambiguity via type inference """ function fromexpr(dom::GAT, codom::GAT, e, ::Type{TheoryMap}) - tyms, trms = Dict{Ident, AlgSort}(), Dict{Ident, TermInCtx}() + tyms = Dict{Ident, Union{Ident, TypeInCtx}}() + trms = Dict{Ident, Union{Ident, TermInCtx}}() exprs = @match e begin Expr(:block, e1::Expr, es...) => [e1,es...] Expr(:block, ::LineNumberNode, es...) => filter(x->!(x isa LineNumberNode), es) end for expr in exprs e1, e2 = @match expr begin Expr(:call, :(=>), e1, e2) => (e1,e2) end + if e1 ∈ nameof.(typecons(dom)) - tyms[fromexpr(dom, e1, Ident)] = fromexpr(codom, e2, AlgSort) + val = e2 isa Symbol ? fromexpr(codom, e2, Ident) : fromexpr(codom, e2, TypeInCtx) + tyms[fromexpr(dom, e1, Ident)] = val else val = fromexpr(codom, e2, TermInCtx) key = fromexpr(dom, e1, TermInCtx) diff --git a/test/syntax/GATs.jl b/test/syntax/GATs.jl index e374ecc8..20becce1 100644 --- a/test/syntax/GATs.jl +++ b/test/syntax/GATs.jl @@ -93,11 +93,15 @@ TG = ThGraph.THEORY @test TG ⊆ T @test T ⊈ TG -# TermInCtx +# InCtx #---------- tic = fromexpr(T, :(compose(f,compose(id(b),id(b))) ⊣ [a::Ob, b::Ob, f::Hom(a,b)]), TermInCtx); tic2 = fromexpr(T,toexpr(T, tic),TermInCtx) # same modulo scope tags + +typic = fromexpr(T, :(Hom(a,b) ⊣ [a::Ob, b::Ob, f::Hom(a,b)]), TypeInCtx) +typic2 = fromexpr(T,toexpr(T, typic), TypeInCtx) # same modulo scope tags + # Type inference #--------------- diff --git a/test/syntax/TheoryMaps.jl b/test/syntax/TheoryMaps.jl index 045601c8..a0216f97 100644 --- a/test/syntax/TheoryMaps.jl +++ b/test/syntax/TheoryMaps.jl @@ -52,9 +52,15 @@ end # Applying theorymap as a function to Ident and TermInCtx #-------------------------------------------------------- + +# Test PreorderCat + (Ob, Hom), (Cmp, Id) = typecons(T), termcons(T) -@test PreorderCat(Ob) == AlgSort(ident(T2; name=:default)) +@test PreorderCat(Ob) == InCtx(T2, ident(T2; name=:default)) @test PreorderCat(Cmp) isa TermInCtx + +PreorderCat(argcontext(getvalue(T[Cmp]))) + @test PreorderCat(argcontext(getvalue(T[Cmp]))) isa TypeScope @test_throws KeyError PreorderCat(first(typecons(T2))) @@ -68,6 +74,13 @@ res = NatPlusMonoid(xterm) expected = fromexpr(ThNatPlus.THEORY, :(Z+(Z+x) ⊣ [x::ℕ]), TermInCtx) @test toexpr(ThNatPlus.THEORY, res) == toexpr(ThNatPlus.THEORY, expected) +# Test OpCat + +xterm = fromexpr(T, :(id(x) ⋅ p ⋅ q ⋅ id(z) ⊣ [(x,y,z)::Ob, p::Hom(x,y), q::Hom(y,z)]), TermInCtx) +expected = :(compose(id(z), compose(q, compose(p, id(x)))) ⊣ [x::Ob,y::Ob,z::Ob, p::Hom(y,x), q::Hom(z,y)]) +@test toexpr(T, OpCat(xterm)) == expected + + # Inclusions ############# TLC = ThLawlessCat.THEORY