Merge branch 'tchajed/simplify-passing-identifier' into 'master'

Re-implement passing identifier back to Ltac1

See merge request !5

theories/ltac2_string_ident.v

@@ -67,43 +67,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.