Symbolic constructs

[olynch]

We should have a macro that makes writing symbolic functions as easy as writing normal functions. Something like

@symbolic(ThRing) function foo(a, b)
  a^2 + b^2
end

should produce a symbolic function in the theory of rings out of the context [a,b]. Then symbolic functions should be able to be applied inside other symbolic functions, so we could have

@symbolic(ThRing) function bar(x,y,z)
  foo(x,y) + foo(y,z)
end

Of course, this should support types, so that we have

@symbolic(ThModule) function interpolate(r::Scalar, v::Vector, w::Vector)::Vector
  (1 - r) * v + r * w
end

This should extend to "symbolic structs".

@symbolic(ThRing) struct Pos2D
  x
  y
end

@symbolic(ThRing) function abs2(p::Pos2D)
  foo(p.x, p.y)
end

Finally, we should support some sort of "comptime" abstraction, where symbolic functions can have parameters which are Julia values. Something like:

@symbolic(ThRing) function power(n::Int)(a)
  acc = 1
  for i in (@julia 1):n
    acc = acc * a
  end
  acc
end

This would expand into a Julia function that looked something like

function power(n::Int)
   _context = ...
   _a = Trm(Lvl(1; context=true))
   function _mul(x,y)
      Trm(getlevel(ThRing.*), [x,y])
   end
   _1 = Trm(getlevel(ThRing.one), [])
   acc = _1
   for i in 1:n
     acc = _mul(acc, _a)
   end
   TrmInContext(_context, acc)
end

I think this is a good design for how to work with #73. Of course, this takes us dangerously close to implementing Agda in Julia, but I think this actually shouldn't be too hard (famous last words).

[olynch]

It's a short, dangerous step from here to want higher-level functions... and I can kind of see how they would work...