joelburget / lvca

language verification, construction, and analysis
https://lvca.dev
MIT License
20 stars 0 forks source link

Allow specifying whether a language sort should generate variable definitions or not. #20

Closed joelburget closed 3 years ago

joelburget commented 3 years ago

This applies only to the lvca.abstract_syntax_module ppx. There, term := Operator(list term) generates:

type 'info term =
  | Operator of 'info * 'info List.t 
  | Term_var of 'info * string 

Do we want the Term_var constructor? Probably, usually. If the language ever binds a term, then yes:

term := Operator(list term)
scope := Scope(term. term)

But not if there's no scope. This can be easily statically determined when all definitions live in the same language, but not if term is imported as an external into another language, however I guess at that point it would be represented as Nominal (currently).

joelburget commented 3 years ago

Though I closed this by doing the binding check described above, it occurs to me now, we could also modify abstract syntax definitions with explicit variable declarations, eg

term :=
  | x
  | Operator(list term)