The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

Here's a solution (perhaps more complicated than you were expecting):

Note a significant part of the nastiness comes from not having Ltac1.of_ident, please complain to Pierre-Marie Pedrot that this is a useful feature and workarounds for it are horrendous. Otherwise the complications are somewhat necessary due to a bunch of higher-order stuff that has to back and forth between the two languages.

From Ltac2 Require Import Ltac2.

Ltac2 hyploop (tac : ident -> unit) :=
  let rec loop hs :=
      match hs with
      | h3 :: hs => match h3 with
                    | (h, _, _) => tac h; loop hs
                    end
      | _ => ()
      end in loop (Control.hyps ()).

(* ident_to_constr is a helper to serialize an identifier as a constr of type
[unit -> unit], which uses the ident as the binder *)
Ltac2 ident_to_constr (i:ident) :=
  constr:(ltac2:(clear; intros $i; exact tt) : unit -> unit).

Ltac allhyps_fast tac :=
  (* tac can't be called from Ltac2 because we can't convert an ident to an
  Ltac1 dynamically typed value (the type Ltac1.t in Ltac2); instead, we will
  call a variant that expects its argument as the binder of a constr *)
  let tac_constr i_constr :=
      lazymatch i_constr with
      | fun i => _ => tac i
      end in
  (* at the outermost level, we're constructing hyploop using the ltac1-to-ltac2
  FFI which allows passing an argument so we can pass tac (as [tac_constr]) to
  it *)
  let hyploop :=
      ltac2:(t |- (* t is passed as an Ltac1 opaque object of type [Ltac1.t].
      Remember that it's an Ltac1 tactic that takes a constr and returns
      nothing. *)
         (* we now convert the ident hyploop will pass us to an Ltac1
         dynamically-typed bundle... *)
         let ident_to_arg (i: ident) := Ltac1.of_constr (ident_to_constr i) in
         (* And finally construct the higher-order argument to hyploop using
         [Ltac1.apply], the most general way to call an Ltac1 function. The
         third argument is a CPS tactic to use the result, but these tactics
         passed to hyploop (thankfully) don't return anything. *)
         let tac (i: ident) := Ltac1.apply t [ident_to_arg i] (fun _ => ()) in
         hyploop tac) in
  hyploop tac_constr.

Set Default Proof Mode "Classic".

Goal nat -> bool -> nat.
Proof.
  intros x y.
  allhyps_fast ltac:(fun i => let P := type of i in idtac i ":" P).
  (* prints x : nat and y : bool, as expected *)
Abort.

On Sat, Aug 15, 2020 at 8:12 PM jonikelee AT gmail.com jonikelee AT gmail.com wrote:

I have the following Ltac2 function to iterate over hypotheses:

Ltac2 hyploop (tac : ident -> unit) :=
  let rec loop hs :=
      match hs with
      | h3 :: hs => match h3 with
                    | (h, _, _) => tac h; loop hs
                    end
      | _ => ()
      end in loop (Control.hyps ()).

How do I call hyploop from Ltac1, passing in an Ltac1 function
for the tac argument?

Ltac allhyps_fast tac :=
  ltac2:(hyploop ltac1:(????)).