AlgDot and AlgStruct fields use symbols

src/models/ModelInterface.jl

@@ -492,10 +492,10 @@ end
 function mk_fun(f::AlgFunction, theory, mod, jltype_by_sort)
   name = nameof(f.declaration)
   args = map(zip(f.args, sortsignature(f))) do (i,s)
-    Expr(:(::),nameof(f[i]),jltype_by_sort[s])
+    Expr(:(::), nameof(f[i]), jltype_by_sort[s])
   end
-  impl = to_call_impl(f.value,theory, mod, false)
-  JuliaFunction(;name=name, args, impl)
+  impl = to_call_impl(f.value, theory, mod, false)
+  JuliaFunction(; name=name, args, impl)
 end
 
 function make_alias_definitions(theory, theory_module, jltype_by_sort, model_type, whereparams, ext_functions)
@@ -756,11 +756,7 @@ function to_call_impl(t::AlgTerm, theory::GAT, mod::Union{Symbol,Module}, migrat
     nameof(b)
   elseif  GATs.isdot(t)
     impl = to_call_impl(b.body, theory, mod, migrate)
-    if isnamed(b.head)
-      Expr(:., impl, QuoteNode(nameof(b.head)))
-    else 
-      Expr(:ref, impl, getlid(b.head).val)
-    end
+    Expr(:., impl, QuoteNode(b.head))
   else
     args = to_call_impl.(argsof(b), Ref(theory), Ref(mod), migrate)
     name = nameof(headof(b))

src/nonstdlib/models/Pushouts.jl

@@ -2,8 +2,6 @@ using DataStructures, StructEquality
 
 export PushoutInt
 
-using GATlab
-
 """Data required to specify a pushout. No fancy caching."""
 @struct_hash_equal struct PushoutInt
   ob::Int

src/syntax/gats/ast.jl

@@ -130,7 +130,7 @@ function AlgSort(c::Context, t::AlgTerm)
     AlgSort(value.type)
   elseif isdot(t)
     algstruct = c[AlgSort(c, bodyof(bodyof(t))).method] |> getvalue
-    AlgSort(getvalue(algstruct.fields[headof(bodyof(t))]))
+    AlgSort(algstruct.fields[headof(bodyof(t))])
   else # variable
     binding = c[t.body]
     AlgSort(getvalue(binding))
@@ -218,7 +218,7 @@ end
 Accessing a name from a term of tuple type
 """
 @struct_hash_equal struct AlgDot <: AbstractDot
-  head::Ident
+  head::Symbol
   body::AlgTerm
 end
 headof(a::AlgDot) = a.head 

src/syntax/gats/exprinterop.jl

@@ -37,7 +37,7 @@ function fromexpr(c::GATContext, e, ::Type{AlgTerm})
     Expr(:., body, QuoteNode(head)) => begin 
       t = fromexpr(c, body, AlgTerm)
       algstruct = c[AlgSort(c, t).method] |> getvalue
-      AlgTerm(AlgDot(ident(algstruct.fields; name=head), t))# , str))
+      AlgTerm(AlgDot(head, t))
   end
     Expr(:call, head::Symbol, argexprs...) => AlgTerm(parse_methodapp(c, head, argexprs))
     Expr(:(::), val, type) => AlgTerm(Constant(val, fromexpr(c, type, AlgType)))
@@ -378,7 +378,8 @@ function parse_struct!(theory::GAT, e, linenumber, ctx=nothing)
   (name, args...) = @match e begin 
     Expr(:struct, false, Expr(:call, name, lc...), Expr(:block, body...)) => begin
       typeargs = parseargs!(theory, lc, localcontext)
-      args = fromexpr(GATContext(theory, localcontext),Expr(:vect,body...),TypeScope)  
+      ts_args = fromexpr(GATContext(theory, localcontext),Expr(:vect,body...),TypeScope)  
+      args = OrderedDict(nameof(x)=>getvalue(ts_args[x]) for x in getidents(ts_args))
       (name, localcontext, typeargs, args)
     end
   end

src/syntax/gats/judgments.jl

@@ -167,14 +167,16 @@ Is tantamount to (in a vanilla GAT):
   declaration::Ident
   localcontext::TypeScope
   typeargs::Vector{LID}
-  fields::TypeScope
+  fields::OrderedDict{Symbol, AlgType}
 end
 
 Base.nameof(t::AlgStruct) = nameof(t.declaration)
 typeargsof(t::AlgStruct) = t[t.typeargs]
 typesortsignature(tc::AlgStruct) =
   AlgSort.(getvalue.(typeargsof(tc)))
-argsof(t::AlgStruct) = getbindings(t.fields)
+argsof(t::AlgStruct) = map(collect(pairs(t.fields))) do (k,v) 
+  Binding{AlgType}(k, v)
+end
 
 """
 A shorthand for a function, such as "square(x) := x * x".  It is relevant for 

test/util/MetaUtils.jl

@@ -7,6 +7,8 @@ using Base.Meta: ParseError
 using GATlab
 
 strip_all(expr) = strip_lines(expr, recurse=true)
+strip_all(f::JuliaFunction) = setimpl(f, strip_all(f.impl))
+
 parse_fun(expr) = parse_function(strip_all(expr))
 
 # Function generation
@@ -29,20 +31,21 @@ end
 
 # Function parsing
 @test_throws ParseError parse_fun(:(f(x,y)))
-@test (parse_fun(:(function f(x,y) x end)) ==
-       JuliaFunction(:f, [:(x::Any), :(y::Any)], [], [], nothing, quote x end))
-
+@test (strip_all(parse_fun(:(function f(x,y) x end))) ==
+       strip_all(JuliaFunction(:f, [:(x::Any), :(y::Any)], [], [], nothing, quote x end)))
+f = parse_fun(:(function f(x,y) x end))
+x = JuliaFunction(:f, [:(x::Any), :(y::Any)], [], [], nothing, quote x end)
 @test parse_fun((quote
   """ My docstring
   """
   function f(x,y) x end
-end).args[1]) == JuliaFunction(:f, [:(x::Any), :(y::Any)], [], [], nothing, quote x end, " My docstring\n")
+end).args[2]) == strip_all(JuliaFunction(:f, [:(x::Any), :(y::Any)], [], [], nothing, quote x end, " My docstring\n"))
 
 @test (parse_fun(:(function f(x::Int,y::Int)::Int x end)) ==
-       JuliaFunction(:f, [:(x::Int),:(y::Int)], [], [], :Int, quote x end))
+       strip_all(JuliaFunction(:f, [:(x::Int),:(y::Int)], [], [], :Int, quote x end)))
 
 @test (parse_fun(:(f(x,y) = x)) ==
-       JuliaFunction(:f, [:(x::Any), :(y::Any)], [], [], nothing, quote x end))
+       strip_all(JuliaFunction(:f, [:(x::Any), :(y::Any)], [], [], nothing, quote x end)))
 
 sig = JuliaFunctionSig(:f, [:Int,:Int])
 @test parse_function_sig(parse_fun(:(function f(x::Int,y::Int)::Int end))) == sig