diff --git a/docs/Project.toml b/docs/Project.toml index ce0cd327..10801c96 100644 --- a/docs/Project.toml +++ b/docs/Project.toml @@ -1,4 +1,5 @@ [deps] +DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8" Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4" GATlab = "f0ffcf3b-d13a-433e-917c-cc44ccf5ead2" Literate = "98b081ad-f1c9-55d3-8b20-4c87d4299306" diff --git a/src/GATlab.jl b/src/GATlab.jl index bc3b0dc5..bbb412ed 100644 --- a/src/GATlab.jl +++ b/src/GATlab.jl @@ -8,10 +8,12 @@ include("syntax/module.jl") include("models/module.jl") include("stdlib/module.jl") include("nonstdlib/module.jl") # don't reexport this +include("forest/module.jl") # don't reexport this @reexport using .Util @reexport using .Syntax @reexport using .Models @reexport using .Stdlib +@reexport using .Forest end # module GATlab diff --git a/src/forest/gatlab.tree b/src/forest/gatlab.tree new file mode 100644 index 00000000..f38dee03 --- /dev/null +++ b/src/forest/gatlab.tree @@ -0,0 +1,20 @@ +\title{GATlab catalog of GATs} + +\p{This is an autogenerated browser for theories defined using [GATlab](https://algebraicjulia.github.io/GATlab.jl/stable/).} + +\p{This site was generated using [Forester](https://www.jonmsterling.com/jms-005P.xml).} + +\scope{ +\put\transclude/title{Theories} +\query{\query/tag{theory}} +} + +\scope{ +\put\transclude/title{Models} +\query{\query/tag{model}} +} + +\scope{ +\put\transclude/title{Theory morphisms} +\query{\query/tag{theorymap}} +} diff --git a/src/forest/module.jl b/src/forest/module.jl new file mode 100644 index 00000000..92bddd44 --- /dev/null +++ b/src/forest/module.jl @@ -0,0 +1,233 @@ +module Forest +export to_forest +using ...Syntax +using ...Syntax.GATs: TrmTypConstructor, AlgAST, MethodApp +using ...Stdlib: ThSet, StdTheories +import ...Models: show_latex, ModelInterface +using ...Util.MetaUtils: generate_function +import Markdown + +const nn = "\n\n" +latex(x::String) = "#{$x}" +p(x::String) = "\\p{$x}" +code(x::Union{SubString,String}) = "\\code{$x}" +function writefile(pth, str) + io = open(pth, "w"); write(io, str); close(io) +end +alphanum(i) = reverse(string(i, base=35))[1:5] + +function show_latex(T::GAT, expr::TypeScope) + body = join(map(getbindings(expr)) do b + v = getvalue(b) + noshow = methodof(bodyof(v)) == methodof(only(ThSet.Meta.theory.sorts)) + string(nameof(b)) * (noshow ? "" : "::$(show_latex(T, v))") + end,",\\ ") + "\\dashv [$body]" +end + +show_latex(T::GAT, expr::InCtx) = + latex(show_latex(T, getvalue(expr)) * show_latex(T, getcontext(expr))) + + +function show_latex(T::GAT, expr::A) where {A<:AlgAST} + show_latex(T, bodyof(expr)) +end +show_latex(T::GAT, x::Ident) = nameof(x) + + +function show_latex(T::GAT, expr::MethodApp) + binary, head = false, headof(expr) + if length(argsof(expr)) <= 2 + for x in getidents(T; aliases=true) + v = getvalue(T[x]) + if v isa Alias && Base.isoperator(nameof(x)) && v.ref == head + binary, head = true, x + end + end + end + if !binary + join(["\\mathop{\\mathrm{ $(nameof(head)) }}", + (isempty(argsof(expr)) ? [] : ["\\left(", + join([show_latex(T,arg) for arg in argsof(expr)], ","), + "\\right)"])...]) + else + join(["\\left(", show_latex(T,first(argsof(expr))), + "\\mathop{\\mathrm{ $(nameof(head)) }}", + show_latex(T,last(argsof(expr))), "\\right)"]) + end +end + +function to_forest_model(mod::Module, model::Any) + stmts = map(mod.Meta.models[model]) do jf + str = string(Base.remove_linenums!(generate_function(jf))) + code(replace(str, r"#=.+=#" => "")) + end + "\\title{$(nameof(model))}\n\\taxon{definition}\n\\tag{model}$(join(p.(stmts),nn))" +end + + +function to_forest(T::GAT, method::Ident, x::TrmTypConstructor) + is_trm = hasfield(typeof(x), :type) + ty = is_trm ? ("::"*show_latex(T, x.type)) : "" + ctx = getcontext(x) + canonterm = (is_trm ? AlgTerm : AlgType)(x.declaration, method, AlgTerm.(idents(ctx; lid=x.args))) + "\\title{$(nameof(x.declaration))}\n" *latex(show_latex(T, canonterm) * ty * show_latex(T, ctx)) +end + +to_forest(T::GAT, n::Ident, ::AlgDeclaration) = "\\title{$(nameof(n))}" + +function to_forest(T::GAT, n::Ident, x::Alias) + n = nameof(n) == :\ ? "(Backslash)" : nameof(n) + "\\title{$n}\n \\p{Alias for \\ref{$(finame(x.ref))}}" +end + +function to_forest(T::GAT, ::Ident, x::AlgAccessor) + "\\title{$(nameof(x.declaration))}" +end + +function to_forest(T::GAT, n::Ident, x::AlgAxiom) + name = isnothing(nameof(n)) ? "" : "$(nameof(n)): " + "\\title{$name}\n" * latex(join(show_latex.(Ref(T), x.equands), " = ")*show_latex(T, getcontext(x))) +end + + +"""Create a UUID for each judgment's Ident""" +finame(x::Ident) = "$(alphanum(gettag(x).val.value+getlid(x).val))" + +""" +Convert a Module (for a theory) into a tree, a definition tree, and a tree +for each judgment. +""" +function to_forest(mod::Module, path::String; verbose=true) + T = mod.Meta.theory + + hsh = alphanum(Syntax.TheoryInterface.REVERSE_GAT_MODULE_LOOKUP[mod].val.value) + verbose && println("$mod $hsh") + for xs in T.segments.scopes + for (x, v) in identvalues(xs) + fi = joinpath(path, "$(finame(x)).tree") + writefile(fi, to_forest(T, x, v)) + end + end + + typs = join(map(last.(typecons(T))) do tc + "\\transclude{$(finame(tc))}" + end, nn) + trms = join(map(last.(termcons(T))) do tc + "\\transclude{$(finame(tc))}" + end, nn) + + axs = join(map(T.axioms) do x + "\\transclude{$(finame(x))}" + end, nn) + + doms = join(map(Syntax.TheoryMaps.THEORY_DOM_LOOKUP[mod]) do m + "\\transclude{$(alphanum(hash(m)))}" + end) + codoms = join(map(Syntax.TheoryMaps.THEORY_CODOM_LOOKUP[mod]) do m + "\\transclude{$(alphanum(hash(m)))}" + end) + + mods′ = filter(m->!isnothing(m) && nameof(m)!=:Migrator, + ModelInterface.GAT_MODEL_LOOKUP[mod]) + mods = join(map(enumerate(mods′)) do (i,m) + mhsh = alphanum(hash(mod) + i) + fi = joinpath(path, "$(mhsh).tree") + writefile(fi, to_forest_model(mod, m)) + "\\transclude{$(mhsh)}" + end, nn) + def = """ +\\title{$(nameof(T))} +\\taxon{definition}\n\n +\\subtree{\\title{Type Constructors} \n$typs}\n +\\subtree{\\title{Term Constructors} \n$trms}\n +\\subtree{\\title{Axioms} \n$axs}\n +""" + writefile(joinpath(path, "$(hsh)_def.tree"), def) + + doc = to_forest(Base.Docs.doc(mod)) + + page = """ +\\title{$(nameof(T))}\n\\tag{theory}\n\n $doc +\\scope{ \\put\\transclude/heading{false} +\\transclude{$(hsh)_def}\n } +\\subtree{\\title{Models}\n \\put\\transclude/expanded{false} $mods}\n +\\subtree{\\title{TheoryMaps} \n +\\subtree{\\title{As domain} \\put\\transclude/expanded{false} $doms}\n +\\subtree{\\title{As codomain} \\put\\transclude/expanded{false} $codoms}}\n +""" + writefile(joinpath(path, "$hsh.tree"), page) + +end + +""" +Convert a theory map into a tree for the definition nested inside +a general tree for the theory map. +""" +function to_forest_map(mod::Module, path::String) + M = mod.MAP + hsh = alphanum(hash(mod)) + typs, trms = map([typemap,termmap]) do fmap + join(map(collect(pairs(fmap(M)))) do (k, tic) + tc = getvalue(M.dom[k]) + decl = tc.declaration + blck = join(p.(["[$(nameof(decl))]($(finame(decl))):", + latex(show_latex(M.dom, TermInCtx(M.dom, k))), + latex(show_latex(M.codom, tic))])) + "\\scope{$blck}" + end, nn) + end + + # transcluding leads to infinite forester compilation loop + scope = p("[$(nameof(M.dom))]($(Syntax.TheoryInterface.REVERSE_GAT_MODULE_LOOKUP[mod.dom].val.value|> alphanum)) #{\\rightarrow} [$(nameof(M.codom))]($(Syntax.TheoryInterface.REVERSE_GAT_MODULE_LOOKUP[mod.codom].val.value |> alphanum))") + + def = """ +\\title{$(nameof(mod))}\n\\tag{theorymap} +\\taxon{definition}\n\n$scope +\\subtree{\\title{Type Mapping} \n$typs}\n +\\subtree{\\title{Term Mapping} \n$trms}\n +""" + writefile(joinpath(path, "$(hsh).tree"), def) +end + +""" +Create a forest in a directory based on all user-declared theories, theorymaps, +and models. These models are defined in modules +""" +function to_forest(path::String; whitelist=nothing, blacklist=nothing, + clear=false, verbose=true) + ispath(path) && clear && rm.(joinpath.(path, readdir(path))) + isnothing(whitelist) || isnothing(blacklist) || error("Cannot set both white/blacklist") + for T in values(Syntax.TheoryInterface.GAT_MODULE_LOOKUP) + if isnothing(whitelist) || !isempty(parentmodules(T) ∩ whitelist) + if isnothing(blacklist) || isempty(parentmodules(T) ∩ blacklist) + println("T $T") + to_forest(T, path; verbose) + end + end + end + to_forest_map.(values(Syntax.TheoryMaps.THEORY_MAPS) , path); + cp(joinpath(@__DIR__,"gatlab.tree"), joinpath(path,"gatlab.tree")) + return nothing +end + +"""Ad hoc translation for GATlab docstrings to look passable in Forester""" +function to_forest(doc::Markdown.MD)::String + str = split(string(doc), "\n\n##")[1] # auto docs produces stuff after this point + res = replace(str, + r"```\n((.|\n)*?)\n```"=> s"\\code{\1}", # convert ``` ``` codeblocks + r"`(.+?)`"=> s"\\code{\1}", # convert ` ` inline code + r"\$(.+?)\$"=> s"#{\1}" # convert ` ` inline code + ) + join(p.(string.((split(res, r"\n+"))))) # handle newlines +end + +"""Get all modules in the hierarchy, for use in white/blacklist constraints""" +function parentmodules(m::Module, res=nothing) + res = isnothing(res) ? Module[] : res + push!(res, m) + p = parentmodule(m) + p == m ? res : parentmodules(p, res) +end + +end # module diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl index deb0d9ad..f8e8b7ab 100644 --- a/src/models/ModelInterface.jl +++ b/src/models/ModelInterface.jl @@ -159,6 +159,8 @@ macro instance(head, model, body) generate_instance(theory, theory_module, jltype_by_sort, model_type, whereparams, body) end +const GAT_MODEL_LOOKUP = DefaultDict{Module,Vector{Any}}(()->[]) + function generate_instance( theory::GAT, theory_module::Union{Expr0, Module}, @@ -213,8 +215,11 @@ function generate_instance( docsink = gensym(:docsink) code = Expr(:block, + [add_source_code(theory_module, model_type, whereparams, f) for f in functions]..., [generate_function(f) for f in qualified_functions]..., implements_declarations..., + :(push!($(GlobalRef(ModelInterface, :GAT_MODEL_LOOKUP))[$theory_module], + $model_type where {$(whereparams...)})), :(function $docsink end), :(Core.@__doc__ $docsink) ) @@ -222,6 +227,10 @@ function generate_instance( escape ? esc(code) : code end +function add_source_code(theory_module, mod, whereparams, f) + :(push!($(theory_module).Meta.models[$mod where {$(whereparams...)}], $f)) +end + macro instance(head, body) esc(:(@instance $head $(nothing) $body)) end diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl index 22e5d472..b095b296 100644 --- a/src/syntax/TheoryInterface.jl +++ b/src/syntax/TheoryInterface.jl @@ -38,8 +38,13 @@ A constant called `Meta.theory` which is the `GAT` data structure. When we declare a new theory, we add the scope tag of its new segment to this dictionary pointing to the module corresponding to the new theory. """ + const GAT_MODULE_LOOKUP = Dict{ScopeTag, Module}() +const REVERSE_GAT_MODULE_LOOKUP = Dict{Module,ScopeTag}() + + + macro signature(head, body) theory_impl(head, body, __module__) end @@ -115,18 +120,16 @@ function theory_impl(head, body, __module__) doctarget = gensym() push!(modulelines, Expr(:toplevel, :(module Meta + using DataStructures: DefaultDict struct T end @doc ($(Markdown.MD)((@doc $(__module__).$doctarget), $docstr)) const theory = $theory - + const models = DefaultDict(()->[]) macro theory() $theory end macro theory_module() parentmodule(@__MODULE__) end end))) - push!(modulelines, :($(GlobalRef(TheoryInterface, :GAT_MODULE_LOOKUP))[$(gettag(newsegment))] = $name)) - - esc( Expr( :toplevel, @@ -136,10 +139,16 @@ function theory_impl(head, body, __module__) :( module $name $(modulelines...) + + function __init__() + $(GlobalRef(TheoryInterface, :GAT_MODULE_LOOKUP))[$(gettag(newsegment))] = $name + $(GlobalRef(TheoryInterface, :REVERSE_GAT_MODULE_LOOKUP))[$name] = $(gettag(newsegment)) + end + $(structlines...) end ), - :(@doc ($(Markdown.MD)((@doc $doctarget), $docstr)) $name) + :(@doc ($(Markdown.MD)((@doc $doctarget), $docstr)) $name), ) ) end diff --git a/src/syntax/TheoryMaps.jl b/src/syntax/TheoryMaps.jl index fae0f915..934f023e 100644 --- a/src/syntax/TheoryMaps.jl +++ b/src/syntax/TheoryMaps.jl @@ -9,7 +9,7 @@ using ..TheoryInterface import ..ExprInterop: toexpr, fromexpr using StructEquality, MLStyle -using DataStructures: OrderedDict +using DataStructures: OrderedDict, DefaultDict # Theory Maps ############# @@ -389,6 +389,9 @@ end reorder(b::Binding{T}, tag::ScopeTag, perm::Dict{Int,Int}) where {T} = setvalue(b, reorder(getvalue(b), tag, perm)) +const THEORY_DOM_LOOKUP = DefaultDict{Module, Vector{Module}}(()->Module[]) +const THEORY_CODOM_LOOKUP = DefaultDict{Module, Vector{Module}}(()->Module[]) +const THEORY_MAPS = Module[] macro theorymap(head, body) (name, domname, codomname) = @match head begin @@ -413,11 +416,16 @@ macro theorymap(head, body) macro map() $tmap end macro dom() $dommod end macro codom() $codommod end - + const dom = $dommod + const codom = $dommod $mig end ), :(Core.@__doc__ $(name)), + :(push!($(GlobalRef(TheoryMaps, :THEORY_MAPS)), $name)), + :(push!($(GlobalRef(TheoryMaps, :THEORY_DOM_LOOKUP))[$dommod], $name)), + :(push!($(GlobalRef(TheoryMaps, :THEORY_CODOM_LOOKUP))[$codommod], $name)), + name ) ) end diff --git a/src/syntax/gats/judgments.jl b/src/syntax/gats/judgments.jl index 096de5eb..610fa2b3 100644 --- a/src/syntax/gats/judgments.jl +++ b/src/syntax/gats/judgments.jl @@ -120,6 +120,7 @@ A declaration of an axiom equands::Vector{AlgTerm} end +Scopes.getcontext(ax::AlgAxiom) = ax.localcontext """ `AlgSorts` diff --git a/test/forest/tests.jl b/test/forest/tests.jl new file mode 100644 index 00000000..d786fb2d --- /dev/null +++ b/test/forest/tests.jl @@ -0,0 +1,9 @@ +module TestForest +using Test +using GATlab + +tmp = joinpath(tempdir(), "forest") +ispath(tmp) || mkdir(tmp) +to_forest(tmp; whitelist=[Stdlib], clear=true, verbose=false) + +end \ No newline at end of file diff --git a/test/runtests.jl b/test/runtests.jl index da2cd870..5291a64a 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -20,3 +20,7 @@ end include("nonstdlib/tests.jl") end +@testset "forest" begin + include("forest/tests.jl") +end +