Open roboguy13 opened 7 years ago
Yes, this is GHC enforcing the let/app invariant:
It is because the let is built with mkCoreLets:
https://downloads.haskell.org/~ghc/latest/docs/html/libraries/ghc-8.0.1/MkCore.html#v:mkCoreLets
Your best bet is probably to build the lemma directly, instead of via a rule. You could define your own library, e.g.
The appendix of the reasoning paper sort of explains what is going on there:
http://ku-fpg.github.io/files/Farmer-15-HERMIT-reasoning.pdf
FWIW, mkLets
will build let expressions without enforcing the invariant:
https://downloads.haskell.org/~ghc/latest/docs/html/libraries/ghc-8.0.1/CoreSyn.html#v:mkLets
I have a RULE:
When I try to bring it into a lemma with
rule-to-lemma
(or look at it withshow-rule
), it "becomes":I imagine this is something GHC is doing, not HERMIT. As a result of this (I think), I cannot apply it where I would like to (where there is a
let
, not acase
). I know thatcase
andlet
have different semantics in Core with regard to strictness, so I imagine this is why I can't apply it in those places.Is there a way around this or a way to tell it to keep it as
let
?