saw-core-rocq: support partially-applied Prelude.ite.

[chathhorn-galois]

Fixes #2981.

[brianhuffman]

Looks good. I can see that the code for handling ite applied to extra arguments was already there, but if we don't already have a test case that exercises that logic then this PR might be a good opportunity to add one.

[sauclovian-g]

I do not immediately see why it's failing; ping me if you'd like me to look into it further

[chathhorn-galois]

Looks good. I can see that the code for handling ite applied to extra arguments was already there, but if we don't already have a test case that exercises that logic then this PR might be a good opportunity to add one.

I added a case in the rocq golden-style tests, but let me know if there's somewhere else I should stick it:

let t10 = parse_core "ite (Bool -> Bool) True not (id Bool) False";
write_rocq_term "TestPartialIte_5args" [] [] "" t10;

I do not immediately see why it's failing; ping me if you'd like me to look into it further

It looks like it's yices. I was waiting for their website to come back before re-running.

[chathhorn-galois]

It looks like it's yices. I was waiting for their website to come back before re-running.

Oh wait, clearly another problem...

[sauclovian-g]

Yeah, the blst failure is yices upstream (still), the others are something real :-(

[brianhuffman]

Here's the error message from saw-core-rocq-tests:

Error:
In environment
n : nat
a : Type
conds : bitvector n
xs : Vec n a
default : a
The term "id (a -> a)" has type "Type" while it is expected to have type
 "(a -> a) -> a -> a".

It looks like this error happens while translating the (previously skipped) definition of pmux:

pmux : (n : Nat) -> (a : sort 0) -> Vec n Bool -> Vec n a -> a -> a;
pmux n a conds xs default =
  foldr (a -> a) a n (id (a -> a)) default
  (zipWith Bool a (a -> a) (ite a) n conds xs);

This is probably the only definition in the SAWCore prelude that contains an explicit call to id. Are we translating id wrong? It looks like maybe the Rocq id function has an implicit type argument, while we're passing it explicitly.

[sauclovian-g]

Ah, that's probably it.