1

I'm trying to port a Coq tactic (currently written in Ltac) to OCaml, in order to be able to extend that tactic more easily (and avoid the hacks I needed to emulate in Ltac some data structures that are otherwise quite standard in OCaml).

I am currently facing with the following problems:

  1. Can we define an OCaml tactic taking as argument a Ltac expression k (intended to be a continuation)?
  2. How can we apply one such Ltac expression k to a given constr v?
  3. How can we call a given Ltac tactic tac from a plugin?
  4. Can we pass a Ltac closure to one such tactic from the plugin code? (in order to implement the Ltac idiom tac ltac:(fun r => ...) in OCaml)

I did a grep on the Coq sources searching TACTIC EXTEND but did not found some example of that kind of approach...

As a minimal example, below is a toy Ltac tactic running_example that I'd like to port in OCaml, relying on the existing Ltac tactic tac:

Require Import Reals.
Inductive type := Cstrict (ub : R) | Clarge (ub : R).

Ltac tac g k :=
  let aux c lb := k (c lb) in
  match g with
  | Rle ?x ?y => aux Clarge y
  | Rge ?x ?y => aux Clarge x
  | Rlt ?x ?y => aux Cstrict y
  | Rgt ?x ?y => aux Cstrict x
  end.

Ltac running_example expr (*point 1*) k :=
  let conc := constr:((R0 <= expr)%R) in
  tac (*point 3*) conc (*point 4*) ltac:(fun r => let v :=
    match r with
    | Clarge ?x => constr:((true, x))
    | Cstrict ?x => constr:((false, x))
    end in (*point 2*)
    k v).

Goal True.
running_example 12%R ltac:(fun r => idtac r).
(* Should display (true, 12%R) *)

So far I've obtained the code below (which only addresses point 1):

open Ltac_plugin
open Stdarg
open Tacarg

TACTIC EXTEND running_example
| [ "running_example" constr(expr) tactic0(k) ] ->
  [ Proofview.Goal.nf_enter begin fun gl ->
    (Tacinterp.tactic_of_value ist k) end ]
END

Any pointers or suggestions are very welcome.

ErikMD
  • 13,377
  • 3
  • 35
  • 71
  • Have you considered using Ltac2? https://github.com/ppedrot/ltac2 – Jason Gross Sep 11 '18 at 05:09
  • Thanks @JasonGross, we didn't try Ltac2 yet. I've just seen that we can call Ltac1 tactics from Ltac2 ones, but that Ltac2 bound variables can't be passed to Ltac1 tactics (https://github.com/ppedrot/ltac2/blob/d4c019e9/tests/compat.v#L24-L25). So I'm not sure it is feasible to achieve what I want (port only one Ltac1 tactic to a more expressive language such as ML−or Ltac2−, while ensuring compatibility back-and-forth with the other custom tactics that would stay in Ltac1). Of course, if it were not possible to achieve this in ML, maybe we could also port everything to Ltac2… – ErikMD Sep 11 '18 at 21:53
  • 1
    You can pass values back and forth in both directions by using the context. Here's some helper tactics I wrote: https://github.com/mit-plv/reification-by-parametricity/blob/master/Ltac2Common.v#L63-L114, and here's an example of them being used: https://github.com/mit-plv/reification-by-parametricity/blob/master/Ltac2.v#L105-L116 – Jason Gross Sep 12 '18 at 22:09
  • OK, thank you @JasonGross for your pointers! So I'll have to test this approach :) – ErikMD Sep 13 '18 at 19:37

0 Answers0