Browse Source

EHN: Enforce unitality of composition in FreeSchema

pull/430/head
Sophie Libkind - Programming 4 weeks ago
parent
commit
815b6d2927
  1. 2
      src/theories/Schema.jl
  2. 4
      test/theories/Schema.jl

2
src/theories/Schema.jl

@ -31,6 +31,8 @@ abstract type AttrExpr{T} <: SchemaExpr{T} end
@syntax FreeSchema{ObExpr,HomExpr,DataExpr,AttrExpr} Schema begin
# should have a normal representation for precompose of a morphism + a generator attribute
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
compose(f::Hom, x::Attr) = associate_unit(new(f,x; strict=true), id)
end
# Type-level representation of Schema

4
test/theories/Schema.jl

@ -16,6 +16,10 @@ x, y = Attr(:x, A, C), Attr(:y, B, C)
@test codom(x) == C
@test dom(compose(f,y)) == A
@test dom(compose(g,x)) == B
@test compose(f, compose(g,f)) == compose(compose(f,g), f)
@test compose(f, compose(g, x)) == compose(compose(f, g), x)
@test compose(id(A), f) == f
@test compose(id(A), x) == x
# CatDesc and AttrDesc
######################

Loading…
Cancel
Save