In your talk at the Simons Institute, you say you want to use if ... then ... else like in normal Haskell programs. You actually can, you just need to enable RebindableSyntax and locally redefine ifThenElse. I have a simple solution here [https://github.com/SamuelSchlesinger/nlambda/blob/master/src/Nominal/If.hs].
I don't think you really have a need to get up inside the compiler itself, as there are plugins and other easier ways to change these things. Also, have you considered implementing the difference between ordered atoms and equality atoms as a type family or something of that sort? Is that a problem on the end of getting Z3 to behave with the two separate universes? As well, is the API referentially transparent? If so, how do you handle Z3 in the background to make it so?
Awesome work by the way, really excited to use/read it
In your talk at the Simons Institute, you say you want to use if ... then ... else like in normal Haskell programs. You actually can, you just need to enable RebindableSyntax and locally redefine ifThenElse. I have a simple solution here [https://github.com/SamuelSchlesinger/nlambda/blob/master/src/Nominal/If.hs].
I don't think you really have a need to get up inside the compiler itself, as there are plugins and other easier ways to change these things. Also, have you considered implementing the difference between ordered atoms and equality atoms as a type family or something of that sort? Is that a problem on the end of getting Z3 to behave with the two separate universes? As well, is the API referentially transparent? If so, how do you handle Z3 in the background to make it so?
Awesome work by the way, really excited to use/read it