From c649f924361ae33b976a864f110b7fd75b08a23c Mon Sep 17 00:00:00 2001 From: Kris Brown Date: Wed, 27 Sep 2023 15:20:57 -0700 Subject: [PATCH] infer axiom type + improved normalize_decl --- src/stdlib/theories/Algebra.jl | 4 +- src/stdlib/theories/Categories.jl | 10 ++-- src/stdlib/theories/Naturals.jl | 31 ++++++----- src/syntax/GATs.jl | 88 +++++++++++++++---------------- 4 files changed, 64 insertions(+), 69 deletions(-) diff --git a/src/stdlib/theories/Algebra.jl b/src/stdlib/theories/Algebra.jl index 330b24d0..68b8ef89 100644 --- a/src/stdlib/theories/Algebra.jl +++ b/src/stdlib/theories/Algebra.jl @@ -71,9 +71,9 @@ end @theory ThPreorder <: ThSet begin Leq(dom, codom)::TYPE @op (≤) := Leq - refl(p)::Leq(p,p) + refl(p)::Leq(p,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)] + irrev := f == g :: Leq(p,q) ⊣ [p,q, (f,g)::Leq(p,q)] end end diff --git a/src/stdlib/theories/Categories.jl b/src/stdlib/theories/Categories.jl index 352243d4..cb474116 100644 --- a/src/stdlib/theories/Categories.jl +++ b/src/stdlib/theories/Categories.jl @@ -30,11 +30,11 @@ The data of a category without any axioms of associativity or identities. """ ThLawlessCat @theory ThAscCat <: ThLawlessCat begin - assoc := ((f ⋅ g) ⋅ h) == (f ⋅ (g ⋅ h)) :: Hom(a,d) ⊣ + assoc := ((f ⋅ g) ⋅ h) == (f ⋅ (g ⋅ h)) ⊣ [a::Ob, b::Ob, c::Ob, d::Ob, f::Hom(a,b), g::Hom(b,c), h::Hom(c,d)] end -@doc """ ThAscCat +@doc """ ThAsCat The theory of a category with the associative law for composition. """ ThAscCat @@ -49,8 +49,8 @@ The theory of a category without identity axioms. """ ThIdLawlessCat @theory ThCategory <: ThIdLawlessCat begin - idl := id(a) ⋅ f == f :: Hom(a,b) ⊣ [a::Ob, b::Ob, f::Hom(a,b)] - idr := f ⋅ id(b) == f :: Hom(a,b) ⊣ [a::Ob, b::Ob, f::Hom(a,b)] + idl := id(a) ⋅ f == f ⊣ [a::Ob, b::Ob, f::Hom(a,b)] + idr := f ⋅ id(b) == f ⊣ [a::Ob, b::Ob, f::Hom(a,b)] end @doc """ ThCategory @@ -59,7 +59,7 @@ The theory of a category with composition operations and associativity and ident """ ThCategory @theory ThThinCategory <: ThCategory begin - thineq := f == g :: Hom(A,B) ⊣ [A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B)] + thineq := f == g ⊣ [A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B)] end @doc """ ThThinCategory diff --git a/src/stdlib/theories/Naturals.jl b/src/stdlib/theories/Naturals.jl index aac38948..2bd49cee 100644 --- a/src/stdlib/theories/Naturals.jl +++ b/src/stdlib/theories/Naturals.jl @@ -3,23 +3,22 @@ export ThNat, ThNatPlus, ThNatPlusTimes using ....Syntax -# Natural numbers + # Natural numbers + @theory ThNat begin + ℕ :: TYPE + Z :: ℕ + S(n::ℕ) :: ℕ + end -@theory ThNat begin - ℕ :: TYPE - Z :: ℕ - S(n::ℕ) :: ℕ -end - -@theory ThNatPlus <: ThNat begin - import Base: + - ((x::ℕ) + (y::ℕ))::ℕ - (n + S(m) == S(n+m) :: ℕ) ⊣ [n::ℕ,m::ℕ] -end + @theory ThNatPlus <: ThNat begin + import Base: + + ((x::ℕ) + (y::ℕ))::ℕ + (n + S(m) == S(n+m) :: ℕ) ⊣ [n::ℕ,m::ℕ] + end -@theory ThNatPlusTimes <: ThNatPlus begin - ((x::ℕ) * (y::ℕ))::ℕ - (n * S(m) == ((n * m) + n) :: ℕ) ⊣ [n::ℕ,m::ℕ] -end + @theory ThNatPlusTimes <: ThNatPlus begin + ((x::ℕ) * (y::ℕ))::ℕ + (n * S(m) == ((n * m) + n)) ⊣ [n::ℕ,m::ℕ] + end end diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl index d7ef3a70..c935bc3a 100644 --- a/src/syntax/GATs.jl +++ b/src/syntax/GATs.jl @@ -461,7 +461,7 @@ Start from the arguments. We know how to compute each of the arguments; they are given. Each argument tells us how to compute other arguments, and also elements of the context """ -function equations(context::TypeCtx, args::AbstractVector{Ident}, theory::GAT; init=nothing) +function equations(context::TypeCtx, args::AbstractVector{Ident}, theory::Context; init=nothing) ways_of_computing = Dict{Ident, Set{InferExpr}}() to_expand = Pair{Ident, InferExpr}[x => x for x in args] if !isnothing(init) @@ -508,7 +508,7 @@ function equations(theory::GAT, t::TypeInCtx) end """Get equations for a term or type constructor""" -equations(theory::GAT, x::Ident) = let x = getvalue(theory[x]); +equations(theory::Context, x::Ident) = let x = getvalue(theory[x]); equations(x, idents(x; lid=x.args),theory) end @@ -573,50 +573,33 @@ 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 = headof(t.trm) - if hasident(t.ctx, head) - getvalue(t.ctx[head]) # base case +function infer_type(ctx::Context, t::AlgTerm) + head = headof(t) + tc = getvalue(ctx[head]) + if tc isa AlgType + tc # 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.localcontext, lid=i)] = tt - end - for lc_arg in reverse(getidents(tc)) - if getlid(lc_arg) ∈ tc.args - continue - end - # 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) + typed_terms = bind_localctx(ctx, t) + AlgType(headof(tc.type), substitute_term.(argsof(tc.type), Ref(typed_terms))) end end +infer_type(ctx::Context, t::TermInCtx) = infer_type(AppendScope(ctx, t.ctx), t.trm) + """ 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::InCtx{T}) where T - head = headof(t.trm) +function bind_localctx(ctx::Context, t::TrmTyp) + head = headof(t) - tc = getvalue(theory[head]) - eqs = equations(theory, head) + tc = getvalue(ctx[head]) + eqs = equations(ctx, 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))) + for (i,a) in zip(tc.args, t.args) + tt = (a => infer_type(ctx, a)) typed_terms[ident(tc, lid=i)] = tt end @@ -628,13 +611,15 @@ function bind_localctx(theory::GAT, t::InCtx{T}) where T 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)) + 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 +bind_localctx(ctx::Context, t::InCtx) = bind_localctx(AppendScope(ctx, t.ctx), t.trm) + """ Replace idents with AlgTerms. """ function substitute_term(t::T, dic::Dict{Ident,AlgTerm}) where T<:TrmTyp x = headof(t) @@ -755,23 +740,32 @@ end """ `axiom=true` adds a `::default` to exprs like `f(a,b) ⊣ [a::A, b::B]` """ -function normalize_decl(e; axiom=false) +function normalize_decl(e) @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) => axiom ? :(($trmcon :: default) ⊣ $ctx) : e - e => e + :($name := $lhs == $rhs ⊣ $ctx) => :((($name := ($lhs == $rhs))) ⊣ $ctx) + :($lhs == $rhs ⊣ $ctx) => :(($lhs == $rhs) ⊣ $ctx) + :($(trmcon::Symbol) ⊣ $ctx) => :(($trmcon :: default) ⊣ $ctx) + :($f($(args...)) ⊣ $ctx) && if f ∉ [:(==), :(⊣)] end => :(($f($(args...)) :: default) ⊣ $ctx) + trmcon::Symbol => :($trmcon :: default) + :($f($(args...))) && if f ∉ [:(==), :(⊣)] end => :($e :: default) + _ => e end end function parseaxiom(c::Context, localcontext, type_expr, e; name=nothing) @match e begin Expr(:call, :(==), lhs_expr, rhs_expr) => begin - equands = fromexpr.(Ref(c), [lhs_expr, rhs_expr], Ref(AlgTerm)) - type = fromexpr(c, type_expr, AlgType) + c′ = AppendScope(c, localcontext) + equands = fromexpr.(Ref(c′), [lhs_expr, rhs_expr], Ref(AlgTerm)) + type = if isnothing(type_expr) + infer_type(c′, first(equands)) + else + fromexpr(c′, type_expr, AlgType) + end axiom = AlgAxiom(localcontext, type, equands) JudgmentBinding(name, axiom) end @@ -789,7 +783,7 @@ explicitly annotated symbols. For explicit annotations to be registered as such rather than parsed as Constants, set kwarg `constants=false`. """ function fromexpr(c::Context, e, ::Type{InCtx{T}}; kw...) where T - (binding, localcontext) = @match normalize_decl(e) begin + (binding, localcontext) = @match e begin Expr(:call, :(⊣), binding, Expr(:vect, args...)) => (binding, parsetypescope(c, args)) e => (e, TypeScope()) end @@ -809,7 +803,9 @@ toexpr(c::Context, ts::TypeScope; kw...) = Expr(:vect,[Expr(:(::), nameof(b), toexpr(c, getvalue(b); kw...)) for b in ts]...) function fromexpr(c::Context, e, ::Type{JudgmentBinding}) - (binding, localcontext) = @match normalize_decl(e; axiom=true) begin + e = normalize_decl(e) + + (binding, localcontext) = @match e begin Expr(:call, :(⊣), binding, Expr(:vect, args...)) => (binding, parsetypescope(c, args)) e => (e, TypeScope()) end @@ -818,12 +814,12 @@ function fromexpr(c::Context, e, ::Type{JudgmentBinding}) (head, type_expr) = @match binding begin Expr(:(::), head, type_expr) => (head, type_expr) - _ => (binding, :default) + _ => (binding, nothing) end @match head begin - Expr(:(:=), name, equation) => parseaxiom(c′, localcontext, type_expr, equation; name) - Expr(:call, :(==), _, _) => parseaxiom(c′, localcontext, type_expr, head) + Expr(:(:=), name, equation) => parseaxiom(c, localcontext, type_expr, equation; name) + Expr(:call, :(==), _, _) => parseaxiom(c, localcontext, type_expr, head) _ => begin (name, arglist) = @match head begin Expr(:call, name, args...) => (name, args)