Revision bf7edfee7fb688cd2fd62ab1dd6ff0683c1cabe5 authored by mkolosick on 06 July 2019, 00:40:25 UTC, committed by mkolosick on 06 July 2019, 07:05:04 UTC
RRTypes get flattened down as much as they can. RApp is parsed in similarly to parsing an unrefined base type, that is as an RRTy with refinement True of an RApp.
1 parent d88274d
README.md
# Mist
A tiny language for teaching and experimenting with refinement types, in the style of
[LiquidHaskell](https://github.com/ucsd-progsys/liquidhaskell).
## TODO
- [x] BUILD initial code
- [ ] STEAL make grammar more Haskelly
- [ ] PARSE in all Nano tests (but using Garter representation)
- [ ] PORT all the garter tests (using Haskelly syntax)
- [ ] PRINT all inferred (top-level) types
- [ ] ADD elaboration @a @b etc.
- [ ] PRINT "elaborated" expressions
- [ ] TYPE refinement type constraints
- [ ] GEN refinement type constraints
- [ ] SOLVE refinement type constraints (with fixpoint)
## Modules
- `Language.Mist.Utils.Misc`
- `Language.Mist.Utils.UX`
- `Language.Mist.Utils.Test`
- `Language.Mist.Basic.Types`
- `Language.Mist.Basic.ANF`
- `Language.Mist.Basic.WellFormed`
- `Language.Mist.Basic.Check`
- `Language.Mist.Liquid.Types`
- `Language.Mist.Liquid.Check`
Computing file changes ...
