Tracking issue for Gibbon-GHC gaps relevant to Sorting Paper

[rrnewton]

General issues

• Let expressions are not recursive #223 Recursion Let Expressions
• Support where expressions in Gibbon #209 Where expressions
• Ignoring Bang (!) patterns
• Pattern binding in let is not supported (e.g. let Just v = k `lookup` assocs in ...)

Issues pertaining to Liquid-Haskell verification

• make sure Liquid checks for us ASAP

• delete everything after ?

• delete every top level binding starting with lemma_ (or convince ourselves that DCE can handle it)

• handle proof threading in _____

• make sure the functional+inplace linearish array library works in both Gibbon/GHC

  • Probably need to add a Gibbon-specific array wrapper in lieu of the reference List.hs or GHC specific
    Mutable.hs

  • Probably should update the common Array.hs lib to say IFDEF __GIBBON__ or some such.

  • Adding CPP support to Gibbon could be a good beginner task in Gibbon. Call GHC's CPP or make a CLI call out to do it.

Separate issues for Linear-Haskell compatibility

(LOW PRIORITY)

• undo CPS-ish code that is there for linear haskell's limitations