From c53fb4be8c65a89dd03d4aedc2fc65d9807da915 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 14 Sep 2017 00:15:09 +0200
Subject: Binding the pose/set family of tactics.

---
 src/g_ltac2.ml4     | 37 ++++++++++++++++++++++++++++++++++++-
 src/tac2core.ml     |  1 +
 src/tac2entries.ml  |  1 +
 src/tac2entries.mli |  1 +
 src/tac2qexpr.mli   |  2 ++
 src/tac2quote.ml    |  3 +++
 src/tac2quote.mli   |  2 ++
 src/tac2stdlib.ml   |  7 +++----
 8 files changed, 49 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 7295f31181..dfd586d5ef 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -40,6 +40,27 @@ let test_lpar_idnum_coloneq =
               | _ -> err ())
         | _ -> err ())
 
+(* Hack to recognize "(x := t)" and "($x := t)" *)
+let test_lpar_coloneq =
+  Gram.Entry.of_parser "test_coloneq"
+    (fun strm ->
+      match stream_nth 0 strm with
+        | KEYWORD "(" ->
+            (match stream_nth 1 strm with
+              | IDENT _ ->
+                  (match stream_nth 2 strm with
+                    | KEYWORD ":=" -> ()
+                    | _ -> err ())
+              | KEYWORD "$" ->
+                (match stream_nth 2 strm with
+                  | IDENT _ ->
+                      (match stream_nth 3 strm with
+                        | KEYWORD ":=" -> ()
+                        | _ -> err ())
+                  | _ -> err ())
+              | _ -> err ())
+        | _ -> err ())
+
 (* Hack to recognize "(x)" *)
 let test_lpar_id_rpar =
   Gram.Entry.of_parser "lpar_id_coloneq"
@@ -369,7 +390,7 @@ GEXTEND Gram
   GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause
           q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag
           q_destruction_arg q_reference q_with_bindings q_constr_matching
-          q_hintdb q_move_location;
+          q_hintdb q_move_location q_pose;
   anti:
     [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
   ;
@@ -702,6 +723,20 @@ GEXTEND Gram
   q_move_location:
     [ [ mv = move_location -> mv ] ]
   ;
+  as_name:
+    [ [ -> None
+      | "as"; id = ident_or_anti -> Some id
+    ] ]
+  ;
+  pose:
+    [ [ test_lpar_coloneq; "("; id = ident_or_anti; ":="; c = Constr.lconstr; ")" ->
+        Loc.tag ~loc:!@loc (Some id, c)
+      | c = Constr.constr; na = as_name -> Loc.tag ~loc:!@loc (na, c)
+    ] ]
+  ;
+  q_pose:
+    [ [ p = pose -> p ] ]
+  ;
 END
 
 (** Extension of constr syntax *)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 7bd0164b4d..bb6578090d 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -1118,6 +1118,7 @@ let () = add_expr_scope "dispatch" q_dispatch Tac2quote.of_dispatch
 let () = add_expr_scope "strategy" q_strategy_flag Tac2quote.of_strategy_flag
 let () = add_expr_scope "reference" q_reference Tac2quote.of_reference
 let () = add_expr_scope "move_location" q_move_location Tac2quote.of_move_location
+let () = add_expr_scope "pose" q_pose Tac2quote.of_pose
 let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_matching
 
 let () = add_generic_scope "constr" Pcoq.Constr.constr Tac2quote.wit_constr
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 26f96f7d72..d622aaba69 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -40,6 +40,7 @@ let q_strategy_flag = Pcoq.Gram.entry_create "tactic:q_strategy_flag"
 let q_constr_matching = Pcoq.Gram.entry_create "tactic:q_constr_matching"
 let q_hintdb = Pcoq.Gram.entry_create "tactic:q_hintdb"
 let q_move_location = Pcoq.Gram.entry_create "tactic:q_move_location"
+let q_pose = Pcoq.Gram.entry_create "tactic:q_pose"
 end
 
 (** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 7c71130402..55e658884b 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -79,6 +79,7 @@ val q_strategy_flag : strategy_flag Pcoq.Gram.entry
 val q_constr_matching : constr_matching Pcoq.Gram.entry
 val q_hintdb : hintdb Pcoq.Gram.entry
 val q_move_location : move_location Pcoq.Gram.entry
+val q_pose : pose Pcoq.Gram.entry
 end
 
 (** {5 Hooks} *)
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 7d02022e07..580039afe5 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -139,3 +139,5 @@ type move_location_r =
 | QMoveLast
 
 type move_location = move_location_r located
+
+type pose = (Id.t located or_anti option * Constrexpr.constr_expr) located
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index f14612d58f..466c1f5094 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -370,3 +370,6 @@ let of_move_location (loc, mv) = match mv with
 | QMoveBefore id -> std_constructor ?loc "MoveBefore" [of_anti of_ident id]
 | QMoveFirst -> std_constructor ?loc "MoveFirst" []
 | QMoveLast -> std_constructor ?loc "MoveLast" []
+
+let of_pose p =
+  of_pair (fun id -> of_option (fun id -> of_anti of_ident id) id) of_open_constr p
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 9f42c60042..ccb832535a 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -75,6 +75,8 @@ val of_dispatch : dispatch -> raw_tacexpr
 
 val of_strategy_flag : strategy_flag -> raw_tacexpr
 
+val of_pose : pose -> raw_tacexpr
+
 val of_constr_matching : constr_matching -> raw_tacexpr
 
 (** {5 Generic arguments} *)
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 28bcd6a1cf..0db71fb293 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -294,13 +294,12 @@ let () = define_prim2 "tac_pose" begin fun idopt c ->
   Tactics.letin_tac None na c None Locusops.nowhere
 end
 
-let () = define_prim4 "tac_set" begin fun ev idopt c cl ->
+let () = define_prim3 "tac_set" begin fun ev p cl ->
   let ev = Value.to_bool ev in
-  let na = to_name idopt in
   let cl = to_clause cl in
   Proofview.tclEVARMAP >>= fun sigma ->
-  thaw c >>= fun c ->
-  let c = Value.to_constr c in
+  thaw p >>= fun p ->
+  let (na, c) = to_pair to_name Value.to_constr p in
   Tactics.letin_pat_tac ev None na (sigma, c) cl
 end
 
-- 
cgit v1.2.3