Coq: Port a Ltac tactic using CPS style to an ML tactic (OCaml plugin)

184 views Asked by At

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.

0

There are 0 answers