Verified Commit 16282df9 authored by Tej Chajed's avatar Tej Chajed

Re-implement passing identifier back to Ltac1

This implementation avoids use of Unsafe, so it is compatible with v8.11
and forward, and also has the benefit of being simpler.
parent af5d0d55
......@@ -66,43 +66,34 @@ Module StringToIdent.
(* [coq_string_to_ident] is the Ltac2 function we want *)
Ltac2 coq_string_to_ident (s: constr) := ident_from_string (coq_string_to_string s).
(* We want to wrap this in Ltac1, which requires extracting the identifier and
passing the input string to Ltac2.
(* We want to wrap this in an Ltac1 API, which requires passing a string to
Ltac2 and then returning the resulting identifier.
The only FFI from Ltac1 to Ltac2 is to call an Ltac2 expression that solves
a goal. We'll solve that goal with `fun (x:unit) => x` where the name x is
a goal. We'll solve that goal with `fun (x:unit) => tt` where the name x is
the desired identifier - Coq remembers the identifier and we can extract it
with Ltac1 pattern matching. However, [constr:(fun (x:unit => x))] doesn't work
because there's no way to inject the Ltac2 identifier --- instead, we
construct the term manually using Ltac2's Constr.Unsafe. *)
with Ltac1 pattern matching. *)
Module U := Ltac2.Constr.Unsafe.
Ltac2 get_opt o := match o with None => Control.throw Not_found | Some x => x end.
(* The identity function with a specific name for the bound variable. Strictly
speaking we could generate (fun (x:unit) => tt), but we really generate the
identity function so when it's printed the name is shown. (Even though the
name is printed as _ for unused binders, it's still stored and pattern
matching can retrieve it). The only downside is that we have to refer to the
bound variable with an explicit de Bruijn index [Rel 1]. *)
Ltac2 ident_to_lambda id := U.make (U.Lambda (Constr.Binder.make (Some id) 'unit) (U.make (U.Rel 1))).
(** this Ltac solves a goal of the form [unit -> unit] with a function that
has the appropriate name *)
Ltac2 get_opt o := match o with None => Control.throw Not_found | Some x => x end.
(* Passing the string into Ltac2 is comparatively easier: we use the ltac2:(x
|- ...) syntax, which creates an Ltac1 function which takes an argument x and
passes it to the inner Ltac2 code, which casts it from a dynamically-typed
Ltac.t to a constr. *)
Ltac coq_string_to_ident_lambda :=
ltac2:(s1 |- let s := get_opt (Ltac1.to_constr s1) in
let ident_lambda := ident_to_lambda (coq_string_to_ident s) in
exact $ident_lambda).
let ident := coq_string_to_ident s in
clear; (* needed since ident might already be in scope where
this is called *)
intros $ident;
exact tt).
End StringToIdent.
(* Finally we wrap everything up by running coq_string_to_ident_lambda in a
new context using tactics-in-terms, extracting just the identifier from the
(* Finally we wrap everything up by running coq_string_to_ident_lambda in a new
context using a tactic-in-terms, extracting just the identifier from the
produced lambda, and returning it as an Ltac1 value. *)
Ltac string_to_ident s :=
let s := (eval cbv in s) in
let x := constr:(ltac:(StringToIdent.coq_string_to_ident_lambda s)) in
let x := constr:(ltac:(StringToIdent.coq_string_to_ident_lambda s) : unit -> unit) in
match x with
| (fun (name:_) => _) => name
end.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment