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

Handle UnivCo #162

Closed conal closed 8 years ago

conal commented 8 years ago

Handle UnivCo: navigation, transformation, pretty-printing. I was in some unfamiliar territory, and I don't have any tests. Some questions:

conal commented 8 years ago

I see the "Merge remote-tracking branch 'upstream/master'" commit listed here (presumably for @xich's merge of my previous pull request) in addition to my new content. Am I doing something wonky with git?

conal commented 8 years ago

See conversation at #160.

xich commented 8 years ago

I think, instead of a catch-all case, we should use readerT (http://hackage.haskell.org/package/kure-2.16.12/docs/Language-KURE-Combinators-Transform.html) so we get an exhaustiveness check from GHC... but we can do that in another diff.

Yes, no need for UnivCo in the Walker c Coercion instance because a UnivCo doesn't contain other coercions.

Yes, I would use retApps so the types get parens around them if necessary.

I think the merge commit would disappear if you rebased this onto my merge commit for SubCo, but that would probably require a git push -f... we can just see what happens to it when I merge this in. Mind doing the retApps bit? Otherwise looks good!

conal commented 8 years ago

@xich Thanks. I added a commit with retApps.

Makes sense about UnivCo having no sub-conversions.

I need to learn git better.

xich commented 8 years ago

Eh, git I understand... github, on the other hand, is still a mystery much of the time.

Thanks for the patches!