The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

> But, why doesn't this work?:

The problem is that you are throwing away the applied tactic without running it.  You have two options:

1. Make your thunk immediate, e.g., by replacing `ltac:(fun i => idtac i)` with `ltac:(fun i => match goal with _ => idtac i end)`

2. Run the tactic in the continuation of Ltac1.apply by replacing `(fun _ => ())` with `Ltac1.run`

On Sun, Aug 16, 2020 at 2:01 PM jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

On Sat, 15 Aug 2020 21:39:11 -0500
Tej Chajed <tchajed AT mit.edu> wrote:

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

I guess I shouldn't be embarassed that I didn't figure this one out on
my own. ;)

But, why doesn't this work?:

From Ltac2 Require Import Ltac2.

Ltac2 hyploop (tac : constr -> unit) :=
  let hypconstrs := List.map (fun (id, _, _) => Control.hyp id) (Control.hyps ()) in
  let rec loop hs :=
      match hs with
      | h :: hs => tac h; loop hs
      | _ => ()
  end in loop hypconstrs.

Ltac allhyps_fast tac :=
  let hyploop' :=
      ltac2:(t |-
         let tac2 (i: constr) := Ltac1.apply t [Ltac1.of_constr i] (fun _ => ()) in
         hyploop tac2) in
  hyploop' tac.

Set Default Proof Mode "Classic".

Goal nat -> bool -> nat.
Proof.
  intros x y.
  allhyps_fast ltac:(fun i => idtac i).
Abort.

Even staying entirely within Ltac2, if there no way more
straightforward than this ident_to_constr kludge cast to get hypotheses
as constrs instead of idents, that seems like a significant shortcoming
of Ltac2 having nothing to do with the Ltac1/Ltac2 interface.


>
> 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 <http://mailto: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:(????)).
> >
> >