Pattern matching variables get renamed in RULES on 'case'

[roboguy13]

I notice that if I have

{-# RULES "abs/case-float-pair" [~]
    forall d x.
    abs (case d of (,) a b -> x)
      =
    case d of
      (,) a b -> abs x
  #-}

and I fire the rule, it will rename the variables in the match to a and b, but it doesn't perform the corresponding substitution in the body (abs x), leading to references to nonexistent names. Is it possible to avoid this problem? I have tried using _s instead of a and b, but it seems to run into the same problem (except that the specific names used are generated by GHC).

If not, is there another way to implement this sort of floating transformation that specifically targets a certain function (in this case abs)? I notice that there is case-float-arg and case-float-arg-unsafe. I have tried case-float-arg-unsafe [| abs |] on the node abs <type and dictionary arguments> (case ds pf wild (,) x y -> ..., but it says

Error in expression: case-float-arg-unsafe [| abs |]
Rewrite failed:Case floating from App argument failed: given function does not match current application.

I imagine this is because I am giving it [| abs |] instead of [| (abs <type and dictionary arguments>) |]. If that's the case, is there a good way to provide it with the appropriate arguments (or avoid the issue altogether)? Ideally, I would like it to apply regardless of the specific type and dictionary arguments.

[roboguy13]

I was able to do this manually with case-float-arg-unsafe by running:

hermit> occurrence-of 'abs
hermit> up
hermit> up
hermit> up
hermit> let-intro 'abs-mono
hermit> let-body
hermit> case-float-arg-unsafe [| abs-mono |]

The abs can then be put back into its original form with up; let-subst.

I'm not sure how I would generalize this so that I could put it into something like a repeat though (since repeat only works on core rewrites)...

This also does sort of seem to suggest that there could be a combinator added that temporarily gives a name to a monomorphized function (without needing to worry about the specifics of what it is monomorphized to) in order to perform a transformation like this.

[xich]

Have you tried using case-float-arg-unsafe "throwawaylemmaname"? It should generate a lemma for the strictness condition and let you keep going.

I think we should kill the variants that take a name. This was mean to make them targetable, but we have better ways to do that. Something like:

{ application-of 'abs ; case-float-arg-unsafe "absCaseFloatLemma" }

[roboguy13]

@xich Thanks, that works with case-float-arg-lemma. Is there a way to automate that composition of things so that it repeats until it no longer applies? I tried using focus, but I can't seem to get that to typecheck.

[xich]

Yeah, focus is a bit of a mess. There isn't a variant with the right type (:: TransformH LCoreTC LocalPathH -> RewriteH LCore -> RewriteH LCore) in src/HERMIT/Dictionary/Kure.hs.

You might be able to get away with focus (application-of 'abs) (promote (case-float-arg-unsafe "lemmaname")).

[xich]

(or add another variant of focus with the right type)

This is where a monomorphic scripting language bites us hard.

[roboguy13]

@xich It works with promote. Thanks!

[roboguy13]

Actually, I may have spoken too soon... That doesn't seem to work with repeat. Might need to add a new variant of focus as you suggested.

[roboguy13]

Hmm, would it make sense to have variants of KURE commands that use LCoreTC? Like repeat :: RewriteLCoreTC -> RewriteLCoreTC? Right now it looks like they only exist for RewriteLCores. I don't really know what LCoreTC is though.

[roboguy13]

Ahhh, it looks like extract :: RewriteLCoreTC -> RewriteLCore is what I want. It looks like case-float-arg-lemma puts me in the prover though and I'm not sure if I can add proof commands to the expression I give to repeat (particularly assume, for the time being at least).

[roboguy13]

You suggested getting rid of the variants that take names which makes sense, but is there currently a way to say something like "apply case-float-lemma ... to all applications of 'abs'"? Sometimes it picks the "wrong" application of abs. Ultimately what I'd like to do with this transformation is try to apply it to all applications of abs (unless this other transformation can apply to the particular application of abs under consideration).