search

RedPRL / sml-typed-abts

second-order abstract syntax
31 stars 9 forks source link

add support for symbols & parameters #1

Closed jonsterling closed 9 years ago

jonsterling commented 9 years ago

Now that I know how the hell these work, we should add these. Will essentially mean switching to an INDEXED_OPERATOR signature, as follows:

signature INDEXED_OPERATOR =
sig
  include OPERATOR
  type symbol
  type renaming (* injective maps of finite sets of symbols *)
  val rename : renaming -> operator -> operator
  val freeSymbols : operator -> symbol list
end

Then, valences will be changed to have two zones, and the abstractor will likewise be changed to have two zones.

It won't be possible to have a "locally nameless" style representation for parameters.

jonsterling commented 9 years ago

Resolved in #3