Meven Lennon-Bertrand (Jan 12 2023 at 20:00): Meven Lennon-Bertrand (Jan 12 2023 at 20:00):I tried the following code:
Set Primitive Projections.
Record foo := { foo_field : nat }.
Definition map_foo (f : nat -> nat) (u : foo) : foo := {| foo_field := f u.(foo_field) |}.
Arguments map_foo f !u.
Eval cbn in (map_foo S {| foo_field := 1 |}).
From what I gather, the Arguments command should let map_foo unfold in the last line reducing to {| foo_field := 2 |}, as its second argument is a constructor. This is also what About map_foo tells me when I call it after the Arguments line. Yet, the unfolding/reduction is not triggered. Have I misunderstood the purpose of ! in Arguments? Or am I doing something else wrong?
Meven Lennon-Bertrand (Jan 12 2023 at 20:01):I seem to be observing the same issue if I replace foo by an inductive with a single field – in other words, this does not seem to be specific to records.
Gaëtan Gilbert (Jan 12 2023 at 20:29):! adds an additional condition on unfolding, so it reduces if it would reduce without the ! AND the argument reduces to a constructor
it seems like you want it to reduce IFF the argument reduces to a constructor which would be Arguments map_foo f !u /.
Paolo Giarrusso (Jan 12 2023 at 20:50):Arguments's output is indeed misleading, which comes up on the bug tracker when people try to reverse engineer simpl and cbn
Paolo Giarrusso (Jan 12 2023 at 20:51):I recall that ! without / has different meanings between simpl and cbn, but I stopped trying it so I forgot the details
Meven Lennon-Bertrand (Jan 12 2023 at 21:10):Ah, I see… The documentation and the error message are indeed not very clear
Notification Bot (Jan 12 2023 at 21:10):Meven Lennon-Bertrand has marked this topic as resolved.
Last updated: Oct 04 2023 at 23:01 UTC