Coq: перенести тактику Ltac с использованием стиля CPS на тактику ML (плагин OCaml) - PullRequest
Новая
       63

Coq: перенести тактику Ltac с использованием стиля CPS на тактику ML (плагин OCaml)

0 голосов
/ 04 сентября 2018

Я пытаюсь перенести тактику Coq (в настоящее время написанную на Ltac) на OCaml, чтобы иметь возможность более легко расширять эту тактику (и избежать хаков, которые мне понадобились, чтобы эмулировать в Ltac некоторые структуры данных, которые в противном случае достаточно стандарт в OCaml).

В настоящее время я сталкиваюсь со следующими проблемами:

  1. Можем ли мы определить тактику OCaml, принимая в качестве аргумента выражение Ltac k (предназначенное для продолжения)?
  2. Как мы можем применить одно из таких выражений Ltac k к данной константе v?
  3. Как мы можем назвать данную тактику Ltac tac из плагина?
  4. Можем ли мы передать закрытие Ltac одной такой тактике из кода плагина? (для реализации идиомы Ltac tac ltac:(fun r => ...) в OCaml)

Я сделал grep по поиску источников Coq TACTIC EXTEND, но не нашел ни одного примера такого подхода ...

В качестве минимального примера ниже представлена ​​игрушечная тактика Ltac running_example, которую я хотел бы перенести в OCaml, опираясь на существующую тактику Ltac 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) *)

Пока что я получил код ниже (который адресует только пункт 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

Любые указатели или предложения приветствуются.

...