Library iris.proofmode.ident_name

From stdpp Require Import base.
From iris.prelude Require Import options.

ident_name is a way to remember an identifier within the binder of a (trivial) function, which can be constructed and retrieved with Ltac but is easy to forward around opaquely in Gallina (through typeclasses, for example)

Definition ident_name := unit → unit.

to_ident_name id returns a constr of type ident_name that holds id in the binder name

Ltac to_ident_name id :=
eval cbv in (ltac:(clear; intros id; assumption) : unit → unit).

to_ident_name is a Gallina-level version of to_ident_name for constructing ident_name literals.

Notation to_ident_name id := (λ id:unit , id) (only parsing).

The idea of AsIdentName is to convert the binder in f to an ident_name representing the name of the binder. If f is not a lambda, this typeclass can produce the fallback identifier __unknown. For example, if the user writes bi_exist Φ, there is no binder anywhere to extract.

This class has only one instance, a Hint Extern which implements that conversion to resolve name in Ltac (see solve_as_ident_name).

Class AsIdentName {A B} (f : A → B) (name : ident_name) := as_ident_name {}.
Global Arguments as_ident_name {A B f} name : assert.

Ltac solve_as_ident_name :=
  lazymatch goal with

  | |- AsIdentName (λ H , _) _ ⇒
    let name := to_ident_name H in
    notypeclasses refine (as_ident_name name)
  | |- AsIdentName _ _ ⇒
     let name := to_ident_name ident:(__unknown) in
     notypeclasses refine (as_ident_name name)
  | |- _ ⇒ fail "solve_as_ident_name: goal should be `AsIdentName`"
  end.

Global Hint Extern 1 (AsIdentName _ _) ⇒ solve_as_ident_name : typeclass_instances.