Skip to content

Commit

Permalink
fixed up reident stuff
Browse files Browse the repository at this point in the history
  • Loading branch information
olynch committed Jul 3, 2024
1 parent bb83512 commit 41a9fc3
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 24 deletions.
50 changes: 28 additions & 22 deletions src/syntax/gats/ast.jl
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,11 @@
fields::OrderedDict{Symbol, T}
end

function Base.map(f, t::AlgNamedTuple)
newfields = OrderedDict((x, f(v)) for (x,v) in t.fields)
AlgNamedTuple(newfields)

Check warning on line 10 in src/syntax/gats/ast.jl

View check run for this annotation

Codecov / codecov/patch

src/syntax/gats/ast.jl#L8-L10

Added lines #L8 - L10 were not covered by tests
end

# AlgSorts
#---------
abstract type AbstractAlgSort end
Expand All @@ -18,48 +23,49 @@ A *sort*, which is essentially a type constructor without arguments
body::Union{Tuple{Ident, Ident}, AlgNamedTuple{AlgSort}}
end

function reident(reps::Dict{Ident}, a::AlgSort)
newhead = reident(reps, headof(a))
newmethod = retag(Dict(a.head.tag => newhead.tag), methodof(a))
AlgSort(newhead, newmethod)
AlgSort(head::Ident, method::Ident) = AlgSort((head, method))

iseq(::AlgSort) = false
istuple(s::AlgSort) = s.body isa AlgNamedTuple

function reident(reps::Dict{Ident}, s::AlgSort)
if istuple(s)
AlgSort(map(s -> reident(reps, s), s.body))

Check warning on line 33 in src/syntax/gats/ast.jl

View check run for this annotation

Codecov / codecov/patch

src/syntax/gats/ast.jl#L33

Added line #L33 was not covered by tests
else
newhead = reident(reps, headof(s))
newmethod = retag(Dict(headof(s).tag => newhead.tag), methodof(s))
AlgSort(newhead, newmethod)
end
end

AlgSort(head::Ident, method::Ident) = AlgSort((head, method))

headof(a::AlgSort) = a.body[1]
methodof(a::AlgSort) = a.body[2]


"""
`AlgSort`
A sort for equality judgments of terms for a particular sort
"""
@struct_hash_equal struct AlgEqSort <: AbstractAlgSort
head::Ident
method::Ident
sort::AlgSort
end

AlgEqSort(head::Ident, method::Ident) = AlgEqSort(AlgSort(head, method))
headof(s::AlgEqSort) = headof(s.sort)
methodof(s::AlgEqSort) = methodof(s.sort)

Check warning on line 57 in src/syntax/gats/ast.jl

View check run for this annotation

Codecov / codecov/patch

src/syntax/gats/ast.jl#L56-L57

Added lines #L56 - L57 were not covered by tests

iseq(::AlgEqSort) = true
iseq(::AlgSort) = false
istuple(s::AlgSort) = s.body isa AlgNamedTuple
headof(a::AbstractAlgSort) = a.body[1]
methodof(a::AbstractAlgSort) = a.body[2]

Base.nameof(sort::AbstractAlgSort) = nameof(headof(sort))

getdecl(s::AbstractAlgSort) = headof(s)

function reident(reps::Dict{Ident}, a::AlgEqSort)
newhead = reident(reps, headof(a))
newmethod = retag(Dict(a.head.tag => newhead.tag), methodof(a))
AlgEqSort(newhead, newmethod)
AlgEqSort(reident(reps, a.sort))
end


function reident(reps::Dict{Ident}, a::AlgEqSort)
newhead = reident(reps, headof(a))
newmethod = retag(Dict(a.head.tag => newhead.tag), methodof(a))
AlgEqSort(newhead, newmethod)
end


"""
We need this to resolve a mutual reference loop; the only subtype is Constant
"""
Expand Down
4 changes: 2 additions & 2 deletions test/syntax/GATs.jl
Original file line number Diff line number Diff line change
Expand Up @@ -91,8 +91,8 @@ HomS = AlgSort(HomT)
@test rename(gettag(scope), Dict(:A=>:Z), HomT) isa AlgType
@test retag(Dict(gettag(scope)=>newscopetag()), HomT) isa AlgType
@test reident(Dict(A=>ident(scope; name=:B)), HomS) isa AlgSort
@test reident(Dict(A=>ident(scope; name=:B)), AlgEqSort(HomS.head, HomS.method)) ==
AlgEqSort(HomS.head, HomS.method)
@test reident(Dict(A=>ident(scope; name=:B)), AlgEqSort(HomS)) ==
AlgEqSort(HomS)

@test sortcheck(c, AlgTerm(A)) == ObS

Expand Down

0 comments on commit 41a9fc3

Please sign in to comment.