Open ninegua opened 8 years ago
Thanks. We'll look into this.
It turns out if
D# ((/##) 1.0 (doubleFromInteger (__integer 2)))
is rewritten as:
case case doubleFromInteger (__integer 2) of w' ▲
_ → (/##) 1.0 w'
of z' ▲
_ → D# z'
Then lint will succeed. But doing so manually is rather tiresome. I tried the following with the above program, and it works (not sure about the smash
part in the proof, but whatever works!)
rhs-of 'y
repeat ((any-bu specialize) >>> smash)
application-of 'doubleFromInteger
{ let-intro 'z; let-body; case-intro-seq 'z; case-expr; inline 'z; up; up; let-elim }
up
case-float-arg-lemma A
-- recording obligations as lemmas : A
smash
end-proof -- proven A
{ let-intro 'z; let-body; case-intro-seq 'z; case-expr; inline 'z; up; up; let-elim }
up
case-float-arg-lemma B
-- recording obligations as lemmas : B
smash
end-proof -- proven B
up
Turning the "troubled" arg into case was relatively straightforward, but since there are two levels of nested application (/##)
and D#
, case-float-arg
has to be done twice.
Would appreciate if there is a more automatic way to fix this kind of error, or better yet if we can avoid violating the let/app rule in case elimination in the first place.
Given: https://github.com/ghc/ghc/blob/master/compiler/coreSyn/CoreSyn.hs#L375
My guess is that some rewrite is building the application with an explicit App
constructor rather than using the mkCoreApp
smart constructor.
Can you narrow down when exactly that expression gets built?
Here is a log after I set-auto-corelint True
and use bash-debug
:
...
[case-reduce (before)]
case D# (doubleFromInteger (__integer 2)) of wild1 ▲
D# y →
case (/##) 1.0 y of wild2 ▲
_ → D# wild2
[case-reduce (after)]
case (/##) 1.0 (doubleFromInteger (__integer 2)) of wild2 ▲
_ → D# wild2
<1> <no location info>: Warning:
In the expression: /## 1.0 (doubleFromInteger (__integer 2))
This argument does not satisfy the let/app invariant:
doubleFromInteger (__integer 2)
Error in expression: repeat ((any-bu specialize) >>> bash-debug)
Core Lint Failed:
<no location info>: Warning:
In the expression: /## 1.0 (doubleFromInteger (__integer 2))
This argument does not satisfy the let/app invariant:
doubleFromInteger (__integer 2)
The issue seems to be a result of using substExpr
in the implementation of caseReduceDataconR
. So a valid App f x
becomes invalid because x
is substituted. Not sure what is the best way to guard this. Maybe rule out the situation when the "substitutee" is of an unboxed type?
This is with hermit version 1.0.1 and GHC 7.10.3 on Linux. Program is simple:
I ran the follow hermit session:
Is it related to issue #139? Does changing GHC version help?