The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

On Sun, 16 Aug 2020 14:09:38 -0400
Jason Gross <jasongross9 AT gmail.com> wrote:

> > 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`  

Thanks, Jason.  I didn't notice that the lazymatch in Tej's tac_constr
function was serving that purpose as well.

Control.hyp is indeed the ident->constr mechanism needed for this to
work - so no need to gang up on PMP just yet.

The resulting hypotheses iterator also needs a Control.enter to be
fully compatible with the Ltac1 version it replaces.  As hoped, it is
significantly faster than any Ltac1-only mechanisms I've tried.

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