Theory Morphisms

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

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

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

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

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

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

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

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