search

tschrijv / AutBound

Code voor Abstract Syntax Tree Code Generator for Haskell-based Com- and Transpilers
1 stars 0 forks source link

Invariance over DeBruijn and String representation #4

Open VonTum opened 4 years ago

VonTum commented 4 years ago

Generate abstractions for dealing with inherent differences between String and DeBruijn representations, so that the same Implementation file can be applied to both. Or at least a greater effort is made unifying the two.

Two important places:

Constructor argument count is different between String and DeBruijn

namespace Var: Term
sort Term
  inh vctx Var
  | Abstraction (t: Term) [z: Var]

generates data Term = Abstraction Term for DeBruijn and data Term = Abstraction Variable Term for String

Abstract away manual shifting of DeBruijn indices.

This strongly locks a codebase into DeBruijn indices.

VonTum commented 4 years ago

Another inconsistency: xyzabcSubstitute generates with type signature abc -> Variable -> xyz -> xyz in DeBruijn and Variable -> abc -> xyz -> xyz in String representation

LorenNuyts commented 4 years ago

In the ExEff.txt file is a native code section that needs to be slightly adapted for De Bruijn indices due to functions that have a different number of arguments than in the string representation. A more uniform interface would also solve that issue.