diff --git a/src/stdlib/models/GATs.jl b/src/stdlib/models/GATs.jl new file mode 100644 index 00000000..7fa6e8d0 --- /dev/null +++ b/src/stdlib/models/GATs.jl @@ -0,0 +1,20 @@ +module GATs +export GATC + +using ....Models +using ....Syntax +using ...StdTheories + +using GATlab, GATlab.Models + +struct GATC <: Model{Tuple{GAT, AbsTheoryMap}} +end + +@instance ThCategory{GAT, AbsTheoryMap} (;model::GATC) begin + id(x::GAT) = IdTheoryMap(x) + compose(f::AbsTheoryMap, g::AbsTheoryMap) = TheoryMaps.compose(f,g) + dom(f::AbsTheoryMap) = TheoryMaps.dom(f) + codom(f::AbsTheoryMap) = TheoryMaps.codom(f) +end + +end # module diff --git a/src/stdlib/models/module.jl b/src/stdlib/models/module.jl index 6aa71e36..1a5f992f 100644 --- a/src/stdlib/models/module.jl +++ b/src/stdlib/models/module.jl @@ -7,11 +7,13 @@ include("FinMatrices.jl") include("SliceCategories.jl") include("Nothings.jl") include("ScopeTrees.jl") +include("GATs.jl") @reexport using .FinSets @reexport using .FinMatrices @reexport using .SliceCategories @reexport using .Nothings @reexport using .ScopeTrees +@reexport using .GATs end diff --git a/src/stdlib/module.jl b/src/stdlib/module.jl index 26792d43..079e4936 100644 --- a/src/stdlib/module.jl +++ b/src/stdlib/module.jl @@ -4,8 +4,10 @@ using Reexport include("theories/module.jl") include("models/module.jl") +include("theorymaps/module.jl") @reexport using .StdTheories @reexport using .StdModels +@reexport using .StdTheoryMaps end diff --git a/src/stdlib/theories/Algebra.jl b/src/stdlib/theories/Algebra.jl index 47cc9140..0a72764d 100644 --- a/src/stdlib/theories/Algebra.jl +++ b/src/stdlib/theories/Algebra.jl @@ -1,6 +1,6 @@ module Algebra export ThSet, ThMagma, ThSemiGroup, ThMonoid, ThGroup, ThCMonoid, ThAb, ThRing, - ThCRing, ThRig, ThCRig, ThElementary + ThCRing, ThRig, ThCRig, ThElementary, ThPreorder using ....Syntax @@ -65,4 +65,12 @@ end # sigmoid(x) ⊣ [x] # end +@theory ThPreorder <: ThSet begin + Leq(dom, codom)::TYPE + @op (≤) := Leq + refl(p)::Leq(p,p) + trans(f::Leq(p,q),g::Leq(q,r))::Leq(p,r) ⊣ [p,q,r] + irrev := f == g ::Leq(p,q) ⊣ [p,q, (f,g)::Leq(p,q)] +end + end diff --git a/src/stdlib/theories/Naturals.jl b/src/stdlib/theories/Naturals.jl index 9e808f34..b226c129 100644 --- a/src/stdlib/theories/Naturals.jl +++ b/src/stdlib/theories/Naturals.jl @@ -8,7 +8,7 @@ using ....Syntax @theory ThNat begin ℕ :: TYPE Z :: ℕ - S(n::ℕ) :: ℕ + S(n::ℕ) :: ℕ end @theory ThNatPlus <: ThNat begin @@ -21,25 +21,4 @@ end (n * S(m) == ((n * m) + n) :: ℕ) ⊣ [n::ℕ,m::ℕ] end -""" -@instance NatPlusIsMonoid{ThMonoid, ThNatPlus} - Ob = ℕ - x ∘ y = x + y - e() = Z() -end - -@instance Swap{ThMonoid,ThMonoid} - Ob = Ob - ∘(x, y) = y ∘ x - e() = e() -end - -@instance CatIsPreorder{ThCategory,ThPreorder} - Ob = Ob - Hom = Leq - ⋅(a,b) = trans(a,b) - id(a) = refl(a) -end -""" - end diff --git a/src/stdlib/theorymaps/Maps.jl b/src/stdlib/theorymaps/Maps.jl new file mode 100644 index 00000000..f1ef772e --- /dev/null +++ b/src/stdlib/theorymaps/Maps.jl @@ -0,0 +1,36 @@ +module Maps + +export SwapMonoid, NatPlusMonoid, PreorderCat + +using ...StdTheories +using ....Syntax + + +SwapMonoid = @theorymap ThMonoid => ThMonoid begin + default => default + x⋅y ⊣ [x, y] => y⋅x ⊣ [x,y] + e => e +end + + +NatPlusMonoid = @theorymap ThMonoid => ThNatPlus begin + default => ℕ + e => Z + (x ⋅ y) ⊣ [x, y] => x+y ⊣ [(x, y)::ℕ] +end + +"""Preorders are categories""" +PreorderCat = @theorymap ThCategory => ThPreorder begin + Ob => default + Hom => Leq + compose(f, g) ⊣ [a::Ob, b::Ob, c::Ob, f::(a → b), g::(b → c)] => + trans(f, g) ⊣ [a, b, c, f::Leq(a, b), g::Leq(b, c)] + id(a) ⊣ [a::Ob] => refl(a) ⊣ [a] +end + +"""Thin categories are isomorphic to preorders""" +# PreorderThinCat = compose(PreorderCat, Incl(ThCategory, ThThinCategory)) +# ThinCatPreorder = inv(PreorderThinCat) + + +end # module diff --git a/src/stdlib/theorymaps/module.jl b/src/stdlib/theorymaps/module.jl new file mode 100644 index 00000000..37d3bafe --- /dev/null +++ b/src/stdlib/theorymaps/module.jl @@ -0,0 +1,9 @@ +module StdTheoryMaps + +using Reexport + +include("Maps.jl") # split into files when big enough + +@reexport using .Maps + +end diff --git a/src/syntax/ExprInterop.jl b/src/syntax/ExprInterop.jl index 5cd75571..15a4db6c 100644 --- a/src/syntax/ExprInterop.jl +++ b/src/syntax/ExprInterop.jl @@ -22,8 +22,9 @@ Converts a Julia Expr into type T, in a certain scope. """ function fromexpr end -function toexpr(c::Context, x::Ident) +function toexpr(c::Context, x::Ident; showing=false) if !hasident(c, x) + showing || error("Unknown ident $x in context $c") return x end tag_level = getlevel(c, gettag(x)) @@ -68,11 +69,11 @@ function fromexpr(c::Context, e, ::Type{Ident}; sig=nothing) end end -function reftolist(c::Context, ref::Reference) +function reftolist(c::Context, ref::Reference; kw...) symbols = [] while !isempty(ref) x = first(ref) - push!(symbols, toexpr(c, x)) + push!(symbols, toexpr(c, x; kw...)) ref = rest(ref) if !isempty(ref) c = getvalue(c, x) @@ -81,8 +82,8 @@ function reftolist(c::Context, ref::Reference) symbols end -function toexpr(c::Context, ref::Reference) - symbols = reftolist(c, ref) +function toexpr(c::Context, ref::Reference; kw...) + symbols = reftolist(c, ref; kw...) if isempty(symbols) :(_) else diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl index 1d2e2c28..8784cd89 100644 --- a/src/syntax/GATs.jl +++ b/src/syntax/GATs.jl @@ -3,11 +3,14 @@ export Constant, AlgTerm, AlgType, TypeScope, AlgSort, AlgSorts, AlgTermConstructor, AlgTypeConstructor, AlgAxiom, sortsignature, JudgmentBinding, GATSegment, GAT, sortcheck, allnames, sorts, sortname, - termcons, typecons, accessors, equations, build_infer_expr, compile + termcons, typecons, accessors, equations, build_infer_expr, compile, + TermInCtx, headof, argsof, argcontext using ..Scopes using ..ExprInterop +import ..Scopes: retag, rename + using StructEquality using MLStyle @@ -21,6 +24,7 @@ using MLStyle We need this to resolve a mutual reference loop; the only subtype is Constant """ abstract type AbstractConstant end +abstract type TrmTyp end # AlgTerm or AlgType """ `AlgTerm` @@ -28,7 +32,7 @@ abstract type AbstractConstant end One syntax tree to rule all the terms. Head can be a reference to an AlgTermConstructor, to a Binding{AlgType, Nothing}, or simply an AbstractConstant """ -@struct_hash_equal struct AlgTerm +@struct_hash_equal struct AlgTerm <: TrmTyp head::Union{Reference, AbstractConstant} args::Vector{AlgTerm} function AlgTerm(head::Union{Reference, AbstractConstant}, args::Vector{AlgTerm}=EMPTY_ARGS) @@ -40,19 +44,12 @@ const EMPTY_ARGS = AlgTerm[] AlgTerm(head::Ident, args::Vector{AlgTerm}=EMPTY_ARGS) = AlgTerm(Reference(head), args) -function ExprInterop.toexpr(c::Context, term::AlgTerm) - if term.head isa Constant - toexpr(c, term.head) - else - if isempty(term.args) - toexpr(c, term.head) - else - Expr(:call, toexpr(c, term.head), toexpr.(Ref(c), term.args)...) - end - end -end - -function ExprInterop.fromexpr(c::Context, e, ::Type{AlgTerm}) +""" +Some expr may have already been bound (e.g. by an explicit context) and thus +oughtn't be interpreted as `default` type. +""" +function ExprInterop.fromexpr(c::Context, e, ::Type{AlgTerm}; bound=nothing) + bound = isnothing(bound) ? Dict{Symbol,AlgType}() : bound @match e begin s::Symbol => begin scope = getscope(c, getlevel(c, s)) @@ -68,19 +65,14 @@ function ExprInterop.fromexpr(c::Context, e, ::Type{AlgTerm}) argsorts = AlgSorts(AlgSort.(Ref(c), args)) AlgTerm(fromexpr(c, head, Reference; sig=argsorts), args) end - Expr(:(::), val, type) => - AlgTerm(Constant(val, fromexpr(c, type, AlgType))) + Expr(:(::), val, type) => + AlgTerm(Constant(val, get(bound, val, fromexpr(c, type, AlgType; bound=bound)))) e::Expr => error("could not parse AlgTerm from $e") constant::Constant => AlgTerm(constant) i::Ident => AlgTerm(Reference(i)) end end -function Base.show(io::IO, t::AlgTerm) - print(io, "AlgTerm(") - show(io, toexpr(EmptyContext(), t)) - print(io, ")") -end """ `AlgType` @@ -88,7 +80,7 @@ end One syntax tree to rule all the types. `head` must be reference to a `AlgTypeConstructor` """ -@struct_hash_equal struct AlgType +@struct_hash_equal struct AlgType <: TrmTyp head::Reference args::Vector{AlgTerm} function AlgType(head::Reference, args::Vector{AlgTerm}=EMPTY_ARGS) @@ -98,29 +90,37 @@ end AlgType(head::Ident, args::Vector{AlgTerm}=EMPTY_ARGS) = AlgType(Reference(head), args) -function ExprInterop.toexpr(c::Context, type::AlgType) - if isempty(type.args) - toexpr(c, type.head) - else - Expr(:call, toexpr(c, type.head), toexpr.(Ref(c), type.args)...) - end -end - -function ExprInterop.fromexpr(c::Context, e, ::Type{AlgType}) +""" +Some expr may have already been bound (e.g. by an explicit context) and thus +oughtn't be interpreted as `default` type. +""" +function ExprInterop.fromexpr(c::Context, e, ::Type{AlgType}; bound=nothing)::AlgType + bound = isnothing(bound) ? Dict{Symbol, AlgType}() : bound @match e begin s::Symbol => AlgType(fromexpr(c, s, Reference)) Expr(:call, head, args...) => - AlgType(fromexpr(c, head, Reference), fromexpr.(Ref(c), args, Ref(AlgTerm))) + AlgType(fromexpr(c, head, Reference), fromexpr.(Ref(c), args, Ref(AlgTerm); bound=bound)) _ => error("could not parse AlgType from $e") end end -function Base.show(io::IO, type::AlgType) - print(io, "AlgType(") - print(io, toexpr(EmptyContext(), type)) +# Common code to Terms and Types +#------------------------------- +headof(t::TrmTyp) = t.head +argsof(t::TrmTyp) = t.args + +rename(tag::ScopeTag, reps::Dict{Symbol,Symbol}, t::T) where T<:TrmTyp = + T(rename(tag, reps, headof(t)), rename.(Ref(tag), Ref(reps), argsof(t))) + +function Base.show(io::IO, type::T) where T<:TrmTyp + print(io, "$(nameof(T))(") + print(io, toexpr(EmptyContext(), type; showing=true)) print(io, ")") end +retag(replacements::Dict{ScopeTag,ScopeTag}, t::T) where {T<:TrmTyp} = + T(retag(replacements, t.head), AlgTerm[retag.(Ref(replacements), t.args)...]) + """ `Constant` @@ -131,9 +131,6 @@ A Julia value in an algebraic context. Checked elsewhere. type::AlgType end -function ExprInterop.toexpr(c::Context, constant::Constant) - Expr(:(::), constant.value, toexpr(c, constant.type)) -end """ `AlgSort` @@ -146,6 +143,7 @@ A *sort*, which is essentially a type constructor without arguments end AlgSort(i::Ident) = AlgSort(Reference(i)) +AlgSort(t::AlgType) = AlgSort(t.head) function AlgSort(c::Context, t::AlgTerm) if t.head isa AbstractConstant @@ -179,6 +177,19 @@ permitted. """ const SortScope = Scope{AlgSort, Nothing} +""" +A term with an accompanying type scope, e.g. + + (a,b)::R +----------- + a*(a+b) +""" +@struct_hash_equal struct TermInCtx + ctx::TypeScope + trm::AlgTerm +end + + """ `sortcheck(ctx::Context, t::AlgTerm)` @@ -200,6 +211,10 @@ function sortcheck(ctx::Context, t::AlgTerm)::AlgSort return AlgSort(ctx, t) end + +sortcheck(ctx::Context, t::TermInCtx)::AlgSort = + sortcheck(AppendScope(ctx, t.ctx), t.trm) + """ `sortcheck(ctx::Context, t::AlgType)` @@ -238,6 +253,15 @@ end sortsignature(tc::Union{AlgTypeConstructor, AlgTermConstructor}) = AlgSort.([a.head for a in getvalue.(tc.args)]) +"""Local context of an AlgTermConstructor, including the arguments themselves""" +argcontext(t::Union{AlgTypeConstructor,AlgTermConstructor}) = + t.localcontext + t.args + +function retag_args(t::AlgTermConstructor) + ac = gettag(argcontext(t)) + Dict(gettag(t.localcontext)=>ac, gettag(t.args)=>ac) +end + """ `AlgAxiom` @@ -378,6 +402,9 @@ function sortname(theory::GAT, type::AlgType) canonicalize(theory, only(type.head)) end +Base.issubset(t1::GAT, t2::GAT) = + all(s->hastag(t2, s), gettag.(Scopes.getscopelist(t1).scopes)) + ## Equations struct AccessorApplication @@ -453,6 +480,11 @@ function equations(args::TypeScope, localcontext::TypeScope, theory::GAT) ways_of_computing end +"""Get equations for a term or type constructor""" +equations(theory::GAT, x::Ident) = let x = getvalue(theory[x]); + equations(x.args, x.localcontext, theory) +end + function compile(theorymodule, expr_lookup::Dict{Reference}, term::AlgTerm) if term.head isa Constant term.head.value @@ -469,9 +501,128 @@ function compile(theorymodule, expr_lookup::Dict{Reference}, term::AlgTerm) end end +"""Get the canonical term associated with a term constructor""" +function TermInCtx(g::GAT, k::Ident) + tcon = getvalue(g[k]) + lc = argcontext(tcon) + ids = reverse(reverse(idents(lc))[1:(length(tcon.args))]) + TermInCtx(lc, AlgTerm(Reference(k), AlgTerm.(ids))) +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 +its localcontext variables are substituted with the relevant AlgTerms. + + (x,y,z)::Ob, p::Hom(x,y), q::Hom(y,z) +E.g. given -------------------------------------- + id(x)⋅(p⋅q) + + (a,b,c)::Ob, f::Hom(a,b), g::Hom(b,c) +and output type: ------------------------------------ + Hom(a,c) + +We first recursively find `{id(x) => Hom(x,x), p⋅q => Hom(x,z)}`. We ultimately +want an AlgTerm for everything in the output type's context such that we can +substitute into `Hom(a,c)` to get the final answer. It will help to also compute +the AlgType for everything in the context. We work backwards, since we start by +knowing `{f => id(x)::Hom(x,x), g=> p⋅q :: Hom(x,z)}`. For `a` `b` and `c`, +we use `equations` which tell us, e.g., that `a = dom(f)`. So we can grab the +first argument of the *type* of `f` (i.e. grab `x` from `Hom(x,x)`). +""" +function infer_type(theory::GAT, t::TermInCtx) + head = only(headof(t.trm)) + if hasident(t.ctx, head) + getvalue(t.ctx[head]) # base case + else + tc = getvalue(theory[head]) + eqs = equations(theory, head) + typed_terms = Dict{Ident, Pair{AlgTerm,AlgType}}() + for (i,a) in zip(tc.args, t.trm.args) + tt = (a => infer_type(theory, TermInCtx(t.ctx, a))) + typed_terms[ident(tc.args, name=nameof(i))] = tt + end + for lc_arg in reverse(idents(tc.localcontext)) + # one way of determining lc_arg's value + filt(e) = e isa AccessorApplication && e.to isa Ident + app = first(filter(filt, eqs[lc_arg])) + + inferred_term = typed_terms[app.to][2].args[app.accessor.lid.val] + inferred_type = infer_type(theory, TermInCtx(t.ctx,inferred_term)) + typed_terms[lc_arg] = inferred_term => inferred_type + end + AlgType(headof(tc.type), map(argsof(tc.type)) do arg + substitute_term(arg, Dict([k=>v[1] for (k,v) in pairs(typed_terms)])) + end) + end +end + +""" +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) + head = only(headof(t.trm)) + + tc = getvalue(theory[head]) + eqs = equations(theory, head) + + typed_terms = Dict{Ident, Pair{AlgTerm,AlgType}}() + for (i,a) in zip(tc.args, t.trm.args) + tt = (a => infer_type(theory, TermInCtx(t.ctx, a))) + typed_terms[ident(tc.args, name=nameof(i))] = tt + end + + for lc_arg in reverse(idents(tc.localcontext)) + # one way of determining lc_arg's value + filt(e) = e isa AccessorApplication && e.to isa Ident + app = first(filter(filt, eqs[lc_arg])) + inferred_term = typed_terms[app.to][2].args[app.accessor.lid.val] + inferred_type = infer_type(theory, TermInCtx(t.ctx,inferred_term)) + typed_terms[lc_arg] = inferred_term => inferred_type + end + + Dict([k=>v[1] for (k,v) in pairs(typed_terms)]) +end + +""" Replace idents with AlgTerms. """ +function substitute_term(t::TrmTyp, dic::Dict{Ident,AlgTerm}) + iden = only(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))) + end +end + # ExprInterop ############# +function ExprInterop.toexpr(c::Context, term::T; kw...) where {T<:TrmTyp} + if term.head isa Constant + toexpr(c, term.head; kw...) + else + if isempty(term.args) + toexpr(c, term.head; kw...) + else + Expr(:call, toexpr(c, term.head; kw...), toexpr.(Ref(c), term.args; kw...)...) + end + end +end + +ExprInterop.toexpr(c::Context, constant::Constant; kw...) = + Expr(:(::), constant.value, toexpr(c, constant.type; kw...)) + + +ExprInterop.toexpr(c::Context, term::AlgSort; kw...) = + ExprInterop.toexpr(c, term.ref; kw...) + +ExprInterop.fromexpr(c::Context, e, ::Type{AlgSort}) = + AlgSort(ExprInterop.fromexpr(c, e, Reference)) + + function bindingexprs(c::Context, s::Scope) c′ = AppendScope(c, s) [Expr(:(::), nameof(b), toexpr(c′, getvalue(b))) for b in s] @@ -500,32 +651,30 @@ function ExprInterop.toexpr(c::Context, binding::JudgmentBinding) end """ -@theory ThLawlessCat <: ThGraph begin - compose(f::Hom(a,b), g::Hom(b,c))::Hom(a,c) ⊣ [a::Ob, b::Ob, c::Ob] - @op begin - (⋅) := compose - end -end -assoc := ((f ⋅ g) ⋅ h) == (f ⋅ (g ⋅ h)) :: Hom(a,d) ⊣ [a::Ob, b::Ob, c::Ob, d::Ob] -otimes(a::Hom(X,Y),b::Hom(P,Q)) ⊣ [(X,Y,P,Q)::Ob] +Return `nothing` if the binding we parse has already been bound. """ - function ExprInterop.fromexpr(c::Context, e, ::Type{Binding{AlgType, Nothing}}) @match e begin - Expr(:(::), name::Symbol, type_expr) => - Binding{AlgType, Nothing}(name, Set([name]), fromexpr(c, type_expr, AlgType)) + Expr(:(::), name::Symbol, type_expr) => + Binding{AlgType, Nothing}(name, Set([name]), fromexpr(c, type_expr, AlgType)) _ => error("could not parse binding of name to type from $e") end end -function parsetypescope(c::Context, exprs::AbstractVector) +""" +Keep track of variables already bound (e.g. in local context) so that they need +not be redefined, e.g. `compose(f,g::Hom(b,c)) ⊣ [(a,b,c)::Ob, f::Hom(a,b)]` +(If `f` were not defined in the local context, it would be parsed as `default`.) +""" +function parsetypescope(c::Context, exprs::AbstractVector; bound=nothing) + bound = isnothing(bound) ? Set{Symbol}() : bound scope = TypeScope() c′ = AppendScope(c, scope) line = nothing for expr in exprs binding_exprs = @match expr begin - a::Symbol => [:($a :: default)] - Expr(:tuple, names...) => [:($name :: default) for name in names] + a::Symbol => a ∈ bound ? [] : [:($a :: default)] + Expr(:tuple, names...) => [:($name :: default) for name in names if name ∉ bound] Expr(:(::), Expr(:tuple, names...), T) => [:($name :: $T) for name in names] :($a :: $T) => [expr] l::LineNumberNode => begin @@ -542,14 +691,17 @@ function parsetypescope(c::Context, exprs::AbstractVector) scope end -function normalize_decl(e) +""" +`axiom=true` adds a `::default` to exprs like `f(a,b) ⊣ [a::A, b::B]` +""" +function normalize_decl(e; axiom=false) @match e begin :($name := $lhs == $rhs :: $typ ⊣ $ctx) => :((($name := ($lhs == $rhs)) :: $typ) ⊣ $ctx) :($lhs == $rhs :: $typ ⊣ $ctx) => :((($lhs == $rhs) :: $typ) ⊣ $ctx) :(($lhs == $rhs :: $typ) ⊣ $ctx) => :((($lhs == $rhs) :: $typ) ⊣ $ctx) :($lhs == $rhs ⊣ $ctx) => :((($lhs == $rhs) :: default) ⊣ $ctx) :($trmcon :: $typ ⊣ $ctx) => :(($trmcon :: $typ) ⊣ $ctx) - :($trmcon ⊣ $ctx) => :(($trmcon :: default) ⊣ $ctx) + :($trmcon ⊣ $ctx) => axiom ? :(($trmcon :: default) ⊣ $ctx) : e e => e end end @@ -566,11 +718,37 @@ function parseaxiom(c::Context, localcontext, type_expr, e; name=nothing) end end -function ExprInterop.fromexpr(c::Context, e, ::Type{JudgmentBinding}) +function ExprInterop.fromexpr(c::Context, e, ::Type{TermInCtx}) (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) +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)) +end + +ExprInterop.toexpr(c::Context, ts::TypeScope) = + Expr(:vect,[Expr(:(::), nameof(b), toexpr(c, getvalue(b))) for b in ts]...) + +ExprInterop.fromexpr(c::Context, e, ::Type{TypeScope}) = @match e begin + Expr(:vect, ps...) => parsetypescope(c, ps) + _ => error("Here $e $(dump(e))") +end + +ExprInterop.toexpr(c::Context, at::Binding{AlgType, Nothing}) = + Expr(:(::), nameof(at), ExprInterop.toexpr(c, getvalue(at))) + +function ExprInterop.fromexpr(c::Context, e, ::Type{JudgmentBinding}) + (binding, localcontext) = @match normalize_decl(e; axiom=true) begin + Expr(:call, :(⊣), binding, Expr(:vect, args...)) => (binding, parsetypescope(c, args)) + e => (e, TypeScope()) + end c′ = AppendScope(c, localcontext) @@ -588,7 +766,7 @@ function ExprInterop.fromexpr(c::Context, e, ::Type{JudgmentBinding}) name::Symbol => (name, []) _ => error("failed to parse head of term constructor $call") end - args = parsetypescope(c′, arglist) + args = parsetypescope(c′, arglist; bound=Set(nameof.(localcontext))) @match type_expr begin :TYPE => begin typecon = AlgTypeConstructor(localcontext, args) @@ -598,7 +776,7 @@ function ExprInterop.fromexpr(c::Context, e, ::Type{JudgmentBinding}) c″ = AppendScope(c′, args) type = fromexpr(c″, type_expr, AlgType) termcon = AlgTermConstructor(localcontext, args, type) - argsorts = map(type -> AlgSort(type.head), getvalue.(args)) + argsorts = AlgSort.(getvalue.(args)) JudgmentBinding(name, Set([name]), termcon, argsorts) end end diff --git a/src/syntax/Scopes.jl b/src/syntax/Scopes.jl index 556ac69d..af52e75a 100644 --- a/src/syntax/Scopes.jl +++ b/src/syntax/Scopes.jl @@ -32,6 +32,10 @@ The tag that makes reference to a specific scope possible. val::UUID end +"""Deterministically combine two scope tags into a third""" +Base.:(+)(x::ScopeTag, y::ScopeTag) = + ScopeTag(Base.UUID(hash(x.val.value, hash(y.val.value)))) + newscopetag() = ScopeTag(uuid4()) const DARK_MODE = Ref(true) @@ -419,7 +423,11 @@ Base.:(==)(s1::Scope, s2::Scope) = s1.tag == s2.tag Base.hash(s::Scope, h::UInt64) = hash(s.tag, h) -Scope{T, Sig}() where {T, Sig} = Scope{T, Sig}(newscopetag(), Binding{T, Sig}[], Dict{Symbol, Dict{Sig, LID}}()) +"""Compare two scopes, ignoring the difference in the top-level scope tag.""" +equiv(s1::Scope, s2::Scope) = s1.bindings == retag(Dict(s2.tag => s1.tag), s2).bindings + +Scope{T, Sig}() where {T, Sig} = + Scope{T, Sig}(newscopetag(), Binding{T, Sig}[], Dict{Symbol, Dict{Sig, LID}}()) function make_name_dict(bindings::AbstractVector{Binding{T, Sig}}) where {T, Sig} d = Dict{Symbol, Dict{Sig, LID}}() @@ -454,6 +462,32 @@ function Scope(symbols::Symbol...; tag=newscopetag()) Scope(Pair{Symbol, Nothing}[x => nothing for x in symbols]...; tag) end +retag(replacements::Dict{ScopeTag,ScopeTag}, s::Scope{T,Sig}) where {T,Sig} = + Scope{T,Sig}(get(replacements, gettag(s), gettag(s)), + retag.(Ref(replacements), s.bindings), + s.names) + +function rename(tag::ScopeTag, + replacements::Dict{Symbol, Symbol}, + scope::Scope{T, Sig}) where {T, Sig} + if tag == gettag(scope) + Scope{T,Sig}(tag, map(scope.bindings) do b + Binding{T,Sig}(get(replacements,b.primary,b.primary), + Set([get(replacements, a, a) for a in b.aliases]), + rename(tag, replacements, b.value), b.sig, b.line) + end, Dict(get(replacements, k, k)=>v for (k,v) in collect(scope.names))) + else + Scope{T,Sig}(tag, retag(Ref(replacements), )) + end +end + +function Base.:(+)(x::Scope{T,Sig}, y::Scope{T,Sig}) where {T,Sig} + newtag = x.tag+y.tag + rep = Dict(gettag(x) => newtag, gettag(y)=>newtag) + Scope(Binding{T,Sig}[retag(rep,x).bindings..., retag(rep,y).bindings...]; + tag=newtag) +end + function Base.show(io::IO, x::Scope) print(io, "{") for (i, b) in enumerate(x.bindings) diff --git a/src/syntax/TheoryMaps.jl b/src/syntax/TheoryMaps.jl new file mode 100644 index 00000000..0aeccc72 --- /dev/null +++ b/src/syntax/TheoryMaps.jl @@ -0,0 +1,256 @@ +module TheoryMaps +export IdTheoryMap, TheoryIncl, AbsTheoryMap, TheoryMap, @theorymap, + TypeMap, TermMap, typemap, termmap + +using ..GATs, ..Scopes, ..ExprInterop +using ..Scopes: unsafe_pushbinding! +using ..GATs: bindingexprs, bind_localctx, substitute_term + +import ..ExprInterop: toexpr, fromexpr + +using StructEquality, MLStyle + +# Theory Maps +############# + +""" +TheoryMaps are morphisms in a category of GATs. A TheoryMap X -> Y can be +thought of in many ways. + +1. An "Every model of Y is also a model of X in some way" +2. Providing "X-shaped hooks" into Y. +3. X is a syntax for Y's semantics. + +The main methods for an AbsTheoryMap to implement are: + dom, codom, typemap, termmap +""" +abstract type AbsTheoryMap end + +""" +A dictionary of Ident (of AlgTypeConstructor in domain) to AlgSort + +This must be a AlgSort of the same arity. +""" +typemap(::AbsTheoryMap)::Dict{Ident, AlgSort} = error("Not implemented") + +""" +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. +""" +termmap(::AbsTheoryMap)::Dict{Ident, TermInCtx} = error("Not implemented") + +# Category of GATs +#----------------- +dom(f::AbsTheoryMap)::GAT = f.dom + +codom(f::AbsTheoryMap)::GAT = f.codom + +function compose(f::AbsTheoryMap, g::AbsTheoryMap) + typmap = Dict(k => typemap(g)[only(v.ref)] 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 + +function (t::AbsTheoryMap)(s::Ident) + if haskey(typemap(t), s) + typemap(t)[s] + elseif haskey(termmap(t), s) + termmap(t)[s] + else + throw(KeyError("Cannot find key $s")) + end +end + + +(f::AbsTheoryMap)(c::AlgTerm) = f(TermInCtx(c)) + +"""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.(only.(headof.(b.value.args))) + val = AlgType(f(only(b.value.head)).ref, AlgTerm[cache[a] for a in argnames]) + 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) + end + scope +end + +function (f::AbsTheoryMap)(t::TermInCtx) + fctx = f(t.ctx) + TermInCtx(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 + fctx = isnothing(fctx) ? f(ctx) : fctx + head = only(headof(t)) + if hasident(ctx, head) + retag(Dict(gettag(ctx)=>gettag(fctx)), t) # term is already in the context + else + termcon = getvalue(f.dom[head]) # Toplevel TermConstructor of t in domain + new_term = f(head) # Codom TermInCtx associated with the toplevel termcon + + # idents in bind_localctx refer to term constructors args and l.c. + rt_dict = Dict(gettag(x)=>gettag(new_term.ctx) + 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)) + + 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 + trms = map(collect(termmap(m))) do (k,v) + domterm = toexpr(dom(m), TermInCtx(dom(m), k)) + Expr(:call, :(=>), domterm, toexpr(codom(m), v)) + end + Expr(:block, typs...,trms...) +end + +# ID +#--- +@struct_hash_equal struct IdTheoryMap <: AbsTheoryMap + gat::GAT +end + +dom(f::IdTheoryMap)::GAT = f.gat + +codom(f::IdTheoryMap)::GAT = f.gat + +compose(::IdTheoryMap, g::AbsTheoryMap) = g + +compose(f::AbsTheoryMap, ::IdTheoryMap) = f + +"""Invert a theory iso""" +Base.inv(f::IdTheoryMap) = f + + +# Inclusion +#---------- +""" +A theory inclusion has a subset of scopes +""" +@struct_hash_equal struct TheoryIncl <: AbsTheoryMap + dom::GAT + codom::GAT + function TheoryIncl(dom,codom) + err = "Cannot construct TheoryInclusion" + dom ⊆ codom ? new(dom,codom) : error(err) + end +end + +typemap(ι::Union{IdTheoryMap,TheoryIncl}) = + Dict(k => AlgSort(k) for k in typecons(dom(ι))) + +termmap(ι::Union{IdTheoryMap,TheoryIncl}) = + Dict(k=>TermInCtx(dom(ι), k) for k in termcons(dom(ι))) + +compose(f::TheoryIncl, g::TheoryIncl) = TheoryIncl(dom(f), codom(g)) + +compose(f::AbsTheoryMap, g::TheoryIncl) = + TheoryIncl(dom(f), codom(g), typemap(f), termmap(f)) + +Base.inv(f::TheoryIncl) = + dom(f) == codom(f) ? f : error("Cannot invert a nontrivial theory inclusion") + +# Non-inclusion +#-------------- + +""" +Presently, axioms are not mapped to proofs. + +TODO: check that it is well-formed, axioms are preserved. +""" +@struct_hash_equal struct TheoryMap <: AbsTheoryMap + dom::GAT + codom::GAT + typemap::Dict{Ident,AlgSort} + 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[only(v.ref)])) + err = "Bad type map $k => $v ($f_args != $arg_fs)" + Scopes.equiv(f_args, arg_fs) || error(err) + 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) + end + + f + end +end + +typemap(t::TheoryMap) = t.typemap + +termmap(t::TheoryMap) = t.termmap + +""" +TODO: we currently ignore LineNumberNodes. TheoryMap data structure could + instead use scopes (rather than Dicts) which store this info in Bindings. + +TODO: handle more ambiguity via type inference +""" +function fromexpr(dom::GAT, codom::GAT, e, ::Type{TheoryMap}) + tyms, trms = Dict{Ident, AlgSort}(), Dict{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) + else + val = fromexpr(codom, e2, TermInCtx) + key = fromexpr(dom, e1, TermInCtx) + + # Check that dom ctx is the same (modulo retagging) with term argcontext + khead = only(key.trm.head) + a_c = argcontext(getvalue(dom[khead])) + Scopes.equiv(key.ctx, a_c) || error("CONTEXT ERROR\n$(key.ctx)\n$a_c") + + trms[khead] = val + end + end + TheoryMap(dom, codom, tyms, trms) +end + +macro theorymap(head, body) + (domname, codomname) = @match head begin + (name::Symbol) => (name, nothing) + Expr(:call,:(=>), name, parent) => (name, parent) + _ => error("could not parse head of @theory: $head") + end + + dom = macroexpand(__module__, :($domname.@theory)) + codom = macroexpand(__module__, :($codomname.@theory)) + fromexpr(dom, codom, body, TheoryMap) +end + +"""Invert a theory iso""" +Base.inv(::TheoryMap) = error("Not implemented") + +end # module diff --git a/src/syntax/module.jl b/src/syntax/module.jl index cea24b0b..b5ee07a3 100644 --- a/src/syntax/module.jl +++ b/src/syntax/module.jl @@ -7,11 +7,13 @@ include("ExprInterop.jl") include("GATs.jl") include("Presentations.jl") include("TheoryInterface.jl") +include("TheoryMaps.jl") @reexport using .Scopes @reexport using .ExprInterop @reexport using .GATs @reexport using .Presentations @reexport using .TheoryInterface +@reexport using .TheoryMaps end diff --git a/test/stdlib/models/GATs.jl b/test/stdlib/models/GATs.jl new file mode 100644 index 00000000..27f90ecb --- /dev/null +++ b/test/stdlib/models/GATs.jl @@ -0,0 +1,22 @@ +module TestGATs + +using GATlab, Test +using .ThCategory + +@withmodel GATC() (Ob, Hom, id, compose, dom, codom) begin + + codom(SwapMonoid) == dom(NatPlusMonoid) + + x = toexpr(compose(id(ThMonoid.THEORY), compose(SwapMonoid, NatPlusMonoid))) + + expected = @theorymap ThMonoid => ThNatPlus begin + default => ℕ + x ⋅ y ⊣ [x, y] => y + x ⊣ [x::ℕ, y::ℕ] + e => Z + end + + @test x == toexpr(expected) + +end + +end # module diff --git a/test/stdlib/models/tests.jl b/test/stdlib/models/tests.jl index 38fade3f..eff8aa21 100644 --- a/test/stdlib/models/tests.jl +++ b/test/stdlib/models/tests.jl @@ -5,5 +5,6 @@ include("FinMatrices.jl") include("SliceCategories.jl") include("Nothings.jl") include("ScopeTrees.jl") +include("GATs.jl") end diff --git a/test/syntax/GATs.jl b/test/syntax/GATs.jl index 0dc0bdb8..ef89f3e5 100644 --- a/test/syntax/GATs.jl +++ b/test/syntax/GATs.jl @@ -24,7 +24,7 @@ three = AlgTerm(plus, [one, two]) @test fromexpr(EmptyContext(), two.head, AlgTerm) == two @test_throws Exception fromexpr(EmptyContext(), :(x = 3), AlgTerm) -@test basicprinted(two) == "AlgTerm(:(2::number))" +@test basicprinted(two) == "AlgTerm(2::number)" @test_throws Exception AlgSort(scope, three) @@ -78,4 +78,23 @@ haia = AlgType(H,[AlgTerm(A),ida]) @test sortcheck(ss, haa) @test_throws Exception sortcheck(ss, haia) +# Subset +#------- +T = ThCategory.THEORY +TG = ThGraph.THEORY +@test TG ⊆ T +@test T ⊈ TG + +# TermInCtx +#---------- +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 + +# Type inference +#--------------- + +t = fromexpr(T,:(id(x)⋅(p⋅q) ⊣ [(x,y,z)::Ob, p::Hom(x,y), q::Hom(y,z)]), TermInCtx) +expected = fromexpr(AppendScope(T, t.ctx), :(Hom(x,z)), AlgType) +@test Syntax.GATs.infer_type(T, t) == expected + end # module diff --git a/test/syntax/TheoryMaps.jl b/test/syntax/TheoryMaps.jl new file mode 100644 index 00000000..e832bb03 --- /dev/null +++ b/test/syntax/TheoryMaps.jl @@ -0,0 +1,76 @@ +module TestTheoryMaps + +using GATlab +using Test + +# Set up +######## + +T = ThCategory.THEORY +T2 = ThPreorder.THEORY + +# TheoryMaps +############ +x = toexpr(PreorderCat); +tm2 = fromexpr(T, T2, x, TheoryMap) +x2 = toexpr(tm2) +@test x == x2 + +# Validation of putative theory maps +#----------------------------------- +@test_throws LoadError @eval @theorymap ThCategory => ThPreorder begin + Ob => default + Hom => Leq + compose(f, g) ⊣ [(a,b,c,d)::Ob, f::(a → b), g::(c → d)] => + trans(f, g) ⊣ [a,b,c,d, f::Leq(a, b), g::Leq(c, d)] # wrong ctx for compose + id(a) ⊣ [a::Ob] => refl(a) ⊣ [a] +end + +@test_throws LoadError @eval @theorymap ThCategory => ThPreorder begin + Ob => default + Hom => Leq + compose(f, g) ⊣ [(a,b,c)::Ob, f::(a → b), g::(b → c)] => + trans(f, g) ⊣ [a, b, c, f::Leq(a, b), g::Leq(b, c)] + id(a) ⊣ [a::Ob] => refl(a) ⊣ [a, b] # codom has different context +end + +@test_throws LoadError @eval @theorymap ThCategory => ThPreorder begin + Ob => default + Hom => default # bad type map + compose(f, g) ⊣ [(a,b,c)::Ob, f::(a → b), g::(b → c)] => + trans(f, g) ⊣ [a, b, c, f::Leq(a, b), g::Leq(b, c)] + id(a) ⊣ [a::Ob] => refl(a) ⊣ [a] +end + +@test_throws LoadError @eval @theorymap ThCategory => ThPreorder begin + Ob => default + Hom => Leq + compose(f, g) ⊣ [a::Ob, b::Ob, c::Ob, f::(a → b), g::(b → c)] => + trans(f, g) ⊣ [a, b, c, f::Leq(a, b), g::Leq(b, c)] + id(b) ⊣ [b::Ob] => refl(a) ⊣ [a] # the LHS doesn't match id's originally defined context +end + +# Applying theorymap as a function to Ident and TermInCtx +#-------------------------------------------------------- +(Ob, Hom), (Cmp, Id) = typecons(T), termcons(T) +@test PreorderCat(Ob) == AlgSort(ident(T2; name=:default)) +@test PreorderCat(Cmp) isa TermInCtx +@test PreorderCat(argcontext(getvalue(T[Cmp]))) isa TypeScope + +xterm = fromexpr(ThMonoid.THEORY, :(x ⊣ [x]), TermInCtx) +res = NatPlusMonoid(xterm) +toexpr(ThNat.THEORY, res) + +xterm = fromexpr(ThMonoid.THEORY, :(e⋅(e⋅x) ⊣ [x]), TermInCtx) +res = NatPlusMonoid(xterm) +expected = fromexpr(ThNatPlus.THEORY, :(Z+(Z+x) ⊣ [x::ℕ]), TermInCtx) +@test toexpr(ThNatPlus.THEORY, res) == toexpr(ThNatPlus.THEORY, expected) + +# Inclusions +############# +TLC = ThLawlessCat.THEORY +incl = TheoryIncl(TLC, T) +toexpr(incl) +@test_throws ErrorException TheoryIncl(T, TLC) + +end # module diff --git a/test/syntax/tests.jl b/test/syntax/tests.jl index ca19355d..47033529 100644 --- a/test/syntax/tests.jl +++ b/test/syntax/tests.jl @@ -23,4 +23,9 @@ end include("TheoryInterface.jl") end +@testset "TheoryMaps" begin + include("TheoryMaps.jl") +end + + end