Skip to content

Commit

Permalink
now with documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
olynch committed Sep 20, 2023
1 parent 1730be1 commit 9ce9a93
Show file tree
Hide file tree
Showing 4 changed files with 24 additions and 12 deletions.
3 changes: 2 additions & 1 deletion src/models/SymbolicModels.jl
Original file line number Diff line number Diff line change
Expand Up @@ -278,7 +278,8 @@ macro symbolic_model(decl, theoryname, body)
Expr(
:toplevel,
module_decl,
esc.(generate_function.([theory_overloads; generator_overloads]))...
:(Core.@__doc__ $(esc(name))),
esc.(generate_function.([theory_overloads; generator_overloads]))...,
)
end

Expand Down
15 changes: 10 additions & 5 deletions src/syntax/TheoryInterface.jl
Original file line number Diff line number Diff line change
Expand Up @@ -97,11 +97,16 @@ macro theory(head, body)
push!(modulelines, :($(GlobalRef(TheoryInterface, :GAT_MODULE_LOOKUP))[$(gettag(newsegment))] = $name))

esc(
Expr(:toplevel, :(
module $name
$(modulelines...)
end
)))
Expr(
:toplevel,
:(
module $name
$(modulelines...)
end
),
:(Core.@__doc__ $(name))
)
)
end

end
10 changes: 10 additions & 0 deletions test/cover.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
using Pkg, Coverage

bashit(str) = run(`bash -c "$str"`)

Pkg.test("GATlab"; coverage=true)
coverage = process_folder()
open("lcov.info", "w") do io
LCOV.write(io, coverage)
end;
bashit("find . -name *.cov -delete")
8 changes: 2 additions & 6 deletions test/models/SymbolicModels.jl
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@ f = FreeCategory.Hom{:generator}([:f], [x, y])

""" Theory of monoids.
"""

@theory ThMonoid begin
Elem::TYPE
munit()::Elem
Expand All @@ -33,7 +32,6 @@ end

""" Syntax for the theory of monoids.
"""

@symbolic_model FreeMonoid{GATExpr} ThMonoid

import .ThMonoid: Elem
Expand All @@ -48,8 +46,8 @@ Elem(mod::Module, args...) = Elem(mod.Elem, args...)
x, y, z = Elem(FreeMonoid,:x), Elem(FreeMonoid,:y), Elem(FreeMonoid,:z)
@test isa(mtimes(x,y), FreeMonoid.Elem)
@test isa(munit(FreeMonoid.Elem), FreeMonoid.Elem)
# @test gat_typeof(x) == :Elem
# @test gat_typeof(mtimes(x,y)) == :Elem
@test gat_typeof(x) == :Elem
@test gat_typeof(mtimes(x,y)) == :Elem
@test mtimes(mtimes(x,y),z) != mtimes(x,mtimes(y,z))

# # Test equality
Expand Down Expand Up @@ -101,15 +99,13 @@ x = Elem(FreeMonoidTyped.Elem, :x)

""" A monoid with two distinguished elements.
"""

@theory ThMonoidTwo <: ThMonoid begin
one()::Elem
two()::Elem
end

""" The free monoid on two generators.
"""

# @symbolic_model FreeMonoidTwo{GATExpr} ThMonoidTwo begin
# Elem(::Type{Elem}, value) = error("No extra generators allowed!")
# end
Expand Down

0 comments on commit 9ce9a93

Please sign in to comment.