I took a stab at this but couldn't get a decent solution quickly, hence making a note.
When we have a function with a default argument such as
val pts_to (#a:Type) (r : ref a) (#[exact (`1.0R)] p:perm) (v:a) : vprop
we mostly use it without instantiating the argument, using the default, and mostly pay no attention to it. But the argument is there since it can of course be something other than 1.0R, in which case it becomes important. Without looking at the implicit, we may get errors like expected pts_to r v, got pts_to r v, which is of course bad, and in a trace message (or Pulse state dumps) we may miss the fact that the implicit is 0.5R or whatever. Turning on implicits (--print_implicits) will display it, but it will also show #a and many many other implicits that we do not care about.
So, I wonder if we can show the implicits that have been manually instantiated by the user instead of being solved by the tactic.
Another alternative is add a notion of default argument to the checker, and then we can compare to see if it matches, and display it if not. This would help in not showing the permission is the user writes pts_to r #1.0R v, or if that term is generated via a metaprogram.
I took a stab at this but couldn't get a decent solution quickly, hence making a note.
When we have a function with a default argument such as
we mostly use it without instantiating the argument, using the default, and mostly pay no attention to it. But the argument is there since it can of course be something other than
1.0R, in which case it becomes important. Without looking at the implicit, we may get errors likeexpected pts_to r v, got pts_to r v, which is of course bad, and in a trace message (or Pulse state dumps) we may miss the fact that the implicit is0.5Ror whatever. Turning on implicits (--print_implicits) will display it, but it will also show#aand many many other implicits that we do not care about.So, I wonder if we can show the implicits that have been manually instantiated by the user instead of being solved by the tactic.
Another alternative is add a notion of default argument to the checker, and then we can compare to see if it matches, and display it if not. This would help in not showing the permission is the user writes
pts_to r #1.0R v, or if that term is generated via a metaprogram.