search

ku-fpg / hermit

Haskell Equational Reasoning Model-to-Implementation Tunnel
http://www.ittc.ku.edu/csdl/fpg/Tools/HERMIT
BSD 2-Clause "Simplified" License
49 stars 8 forks source link

Why do we use RhsOfName, rather than just Name/HermitName? #127

Open andygill opened 9 years ago

andygill commented 9 years ago

@xich Is this for better tab completeness? Or can we unify around Name in the shell?

xich commented 9 years ago

I'm not sure I know specifically where you mean.

There are still places where we use String instead of HermitName that should be fixed. We also have several newtype wrappers for HermitName... those are purely for tab completion. They allow us to distinguish between names in the context vs names that occur in the term, and only tab complete with one or the other, for instance.

I'm guessing you mean one of those? I tried to keep their use isolated to the externals (as completion is a shell concern), so the actual transformations work on HermitName directly.

andygill commented 9 years ago

Yes, this is useful. Given they are semantically the same, we should merge them in the Shell, because there is no tab-complete that can use this. We should also add a note beside the data definition.