Skip to content

Commit

Permalink
initial morphism work
Browse files Browse the repository at this point in the history
  • Loading branch information
Kris Brown authored and olynch committed Sep 13, 2023
1 parent 1e4dfeb commit 61c182e
Show file tree
Hide file tree
Showing 17 changed files with 738 additions and 88 deletions.
20 changes: 20 additions & 0 deletions src/stdlib/models/GATs.jl
Original file line number Diff line number Diff line change
@@ -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
2 changes: 2 additions & 0 deletions src/stdlib/models/module.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 2 additions & 0 deletions src/stdlib/module.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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
10 changes: 9 additions & 1 deletion src/stdlib/theories/Algebra.jl
Original file line number Diff line number Diff line change
@@ -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

Expand Down Expand Up @@ -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
23 changes: 1 addition & 22 deletions src/stdlib/theories/Naturals.jl
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ using ....Syntax
@theory ThNat begin
:: TYPE
Z ::
S(n::ℕ) ::
S(n::ℕ) ::
end

@theory ThNatPlus <: ThNat begin
Expand All @@ -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
36 changes: 36 additions & 0 deletions src/stdlib/theorymaps/Maps.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
module Maps

export SwapMonoid, NatPlusMonoid, PreorderCat

using ...StdTheories
using ....Syntax


SwapMonoid = @theorymap ThMonoid => ThMonoid begin
default => default
xy [x, y] => yx [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
9 changes: 9 additions & 0 deletions src/stdlib/theorymaps/module.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
module StdTheoryMaps

using Reexport

include("Maps.jl") # split into files when big enough

@reexport using .Maps

end
11 changes: 6 additions & 5 deletions src/syntax/ExprInterop.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down Expand Up @@ -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)
Expand All @@ -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
Expand Down
Loading

0 comments on commit 61c182e

Please sign in to comment.