Adding new scopes for standard Ltac structures.

8 files changed, 199 insertions, 8 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 21612f9a25..4a2f615df9 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -9,12 +9,29 @@
 open Pp
 open Util
 open Names
+open Tok
 open Pcoq
 open Constrexpr
 open Misctypes
 open Tac2expr
 open Ltac_plugin
 
+let err () = raise Stream.Failure
+
+(* idem for (x:=t) and (1:=t) *)
+let test_lpar_idnum_coloneq =
+  Gram.Entry.of_parser "test_lpar_idnum_coloneq"
+    (fun strm ->
+      match stream_nth 0 strm with
+        | KEYWORD "(" ->
+            (match stream_nth 1 strm with
+              | IDENT _ | INT _ ->
+                  (match stream_nth 2 strm with
+                    | KEYWORD ":=" -> ()
+                    | _ -> err ())
+              | _ -> err ())
+        | _ -> err ())
+
 let tac2expr = Tac2entries.Pltac.tac2expr
 let tac2type = Gram.entry_create "tactic:tac2type"
 let tac2def_val = Gram.entry_create "tactic:tac2def_val"
@@ -24,11 +41,12 @@ let tac2def_syn = Gram.entry_create "tactic:tac2def_syn"
 let tac2mode = Gram.entry_create "vernac:ltac2_command"
 
 let inj_wit wit loc x = CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x)
-let inj_constr loc c = inj_wit Stdarg.wit_constr loc c
 let inj_open_constr loc c = inj_wit Stdarg.wit_open_constr loc c
-let inj_ident loc c = inj_wit Stdarg.wit_ident loc c
 let inj_pattern loc c = inj_wit Tac2env.wit_pattern loc c
 
+let mk_constr ~loc kn args =
+  CTacApp (loc, CTacCst (loc, AbsKn (Other kn)), args)
+
 let pattern_of_qualid loc id =
   if Tac2env.is_constructor (snd id) then CPatRef (loc, RelId id, [])
   else
@@ -108,11 +126,11 @@ GEXTEND Gram
       | s = Prim.string -> CTacAtm (Loc.tag ~loc:!@loc (AtmStr s))
       | id = Prim.qualid ->
         if Tac2env.is_constructor (snd id) then CTacCst (!@loc, RelId id) else CTacRef (RelId id)
-      | "@"; id = Prim.ident -> inj_ident !@loc id
+      | "@"; id = Prim.ident -> Tac2quote.of_ident ~loc:!@loc id
       | "'"; c = Constr.constr -> inj_open_constr !@loc c
-      | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_constr !@loc c
+      | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> Tac2quote.of_constr ~loc:!@loc c
       | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_open_constr !@loc c
-      | IDENT "ident"; ":"; "("; c = Prim.ident; ")" -> inj_ident !@loc c
+      | IDENT "ident"; ":"; "("; c = Prim.ident; ")" -> Tac2quote.of_ident ~loc:!@loc c
       | IDENT "pattern"; ":"; "("; c = Constr.lconstr_pattern; ")" -> inj_pattern !@loc c
     ] ]
   ;
@@ -256,6 +274,41 @@ GEXTEND Gram
   ;
 END
 
+(** Quotation scopes used by notations *)
+
+open Tac2entries.Pltac
+
+GEXTEND Gram
+  GLOBAL: q_ident q_bindings;
+  q_ident:
+    [ [ id = Prim.ident -> Tac2quote.of_ident ~loc:!@loc id
+      | "$"; id = Prim.ident -> Tac2quote.of_variable ~loc:!@loc id
+    ] ]
+  ;
+ simple_binding:
+    [ [ "("; id = Prim.ident; ":="; c = Constr.lconstr; ")" ->
+        Loc.tag ~loc:!@loc (NamedHyp id, Tac2quote.of_constr ~loc:!@loc c)
+      | "("; n = Prim.natural; ":="; c = Constr.lconstr; ")" ->
+        Loc.tag ~loc:!@loc (AnonHyp n, Tac2quote.of_constr ~loc:!@loc c)
+    ] ]
+  ;
+  bindings:
+    [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
+        Tac2quote.of_bindings ~loc:!@loc (ExplicitBindings bl)
+      | bl = LIST1 Constr.constr ->
+        let bl = List.map (fun c -> Tac2quote.of_constr ~loc:!@loc c) bl in
+        Tac2quote.of_bindings ~loc:!@loc (Misctypes.ImplicitBindings bl)
+    ] ]
+  ;
+  q_bindings:
+    [ [ "with"; bl = bindings -> bl
+      | -> mk_constr ~loc:!@loc Tac2core.Core.c_no_bindings []
+    ] ]
+  ;
+END
+
+(** Extension of constr syntax *)
+
 GEXTEND Gram
   Pcoq.Constr.operconstr: LEVEL "0"
     [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack
index 1d7b655dce..8d2d7dc0f4 100644
--- a/src/ltac2_plugin.mlpack
+++ b/src/ltac2_plugin.mlpack
@@ -5,5 +5,6 @@ Tac2interp
 Tac2entries
 Tac2ffi
 Tac2core
+Tac2quote
 Tac2stdlib
 G_ltac2
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 515cadc525..111ef1c8eb 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -21,6 +21,7 @@ open Proofview.Notations
 module Value = Tac2ffi
 
 let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
+let std_core n = KerName.make2 Tac2env.std_prefix (Label.of_id (Id.of_string_soft n))
 
 module Core =
 struct
@@ -41,6 +42,15 @@ let c_cons = coq_core "::"
 let c_none = coq_core "None"
 let c_some = coq_core "Some"
 
+let t_bindings = std_core "bindings"
+let c_no_bindings = std_core "NoBindings"
+let c_implicit_bindings = std_core "ImplicitBindings"
+let c_explicit_bindings = std_core "ExplicitBindings"
+
+let t_qhyp = std_core "hypothesis"
+let c_named_hyp = std_core "NamedHyp"
+let c_anon_hyp = std_core "AnonHyp"
+
 end
 
 open Core
@@ -835,5 +845,20 @@ let () = add_scope "tactic" begin function
 | _ -> scope_fail ()
 end
 
-let () = add_generic_scope "ident" Pcoq.Prim.ident Stdarg.wit_ident
+let () = add_scope "ident" begin function
+| [] ->
+  let scope = Extend.Aentry Tac2entries.Pltac.q_ident in
+  let act tac = rthunk tac in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "bindings" begin function
+| [] ->
+  let scope = Extend.Aentry Tac2entries.Pltac.q_bindings in
+  let act tac = rthunk tac in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
 let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr
diff --git a/src/tac2core.mli b/src/tac2core.mli
index 07ff6cd539..118b7aaa42 100644
--- a/src/tac2core.mli
+++ b/src/tac2core.mli
@@ -16,12 +16,21 @@ module Core :
 sig
 
 val t_list : type_constant
-val c_nil : ltac_constant
-val c_cons : ltac_constant
+val c_nil : ltac_constructor
+val c_cons : ltac_constructor
 
 val t_int : type_constant
 val t_option : type_constant
 val t_string : type_constant
 val t_array : type_constant
 
+val t_bindings : type_constant
+val c_no_bindings : ltac_constructor
+val c_implicit_bindings : ltac_constant
+val c_explicit_bindings : ltac_constant
+
+val t_qhyp : type_constant
+val c_anon_hyp : ltac_constructor
+val c_named_hyp : ltac_constructor
+
 end
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 7bc4c75510..d293a87975 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -23,6 +23,9 @@ open Vernacexpr
 module Pltac =
 struct
 let tac2expr = Pcoq.Gram.entry_create "tactic:tac2expr"
+
+let q_ident = Pcoq.Gram.entry_create "tactic:q_ident"
+let q_bindings = Pcoq.Gram.entry_create "tactic:q_bindings"
 end
 
 (** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 71e8150057..4d5a234daf 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -54,4 +54,9 @@ val call : default:bool -> raw_tacexpr -> unit
 module Pltac :
 sig
 val tac2expr : raw_tacexpr Pcoq.Gram.entry
+
+(** Quoted entries. They directly return an Ltac2 expression *)
+
+val q_ident : raw_tacexpr Pcoq.Gram.entry
+val q_bindings : raw_tacexpr Pcoq.Gram.entry
 end
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
new file mode 100644
index 0000000000..2d9521d30c
--- /dev/null
+++ b/src/tac2quote.ml
@@ -0,0 +1,63 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Util
+open Misctypes
+open Tac2intern
+open Tac2expr
+open Tac2core
+
+(** Syntactic quoting of expressions. *)
+
+let dummy_loc = Loc.make_loc (-1, -1)
+
+let constructor ?loc kn args =
+  let loc = Option.default dummy_loc loc in
+  let cst = CTacCst (loc, AbsKn (Other kn)) in
+  if List.is_empty args then cst
+  else CTacApp (loc, cst, args)
+
+let of_pair ?loc (e1, e2) =
+  let loc = Option.default dummy_loc loc in
+  CTacApp (loc, CTacCst (loc, AbsKn (Tuple 2)), [e1; e2])
+
+let of_int ?loc n =
+  CTacAtm (Loc.tag ?loc (AtmInt n))
+
+let inj_wit ?loc wit x =
+  let loc = Option.default dummy_loc loc in
+  CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x)
+
+let of_variable ?loc id =
+  let qid = Libnames.qualid_of_ident id in
+  if Tac2env.is_constructor qid then
+    CErrors.user_err ?loc (str "Invalid identifier")
+  else CTacRef (RelId (Loc.tag ?loc qid))
+
+let of_ident ?loc id = inj_wit ?loc Stdarg.wit_ident id
+
+let of_constr ?loc c = inj_wit ?loc Stdarg.wit_constr c
+
+let rec of_list ?loc = function
+| [] -> constructor Core.c_nil []
+| e :: l ->
+  constructor ?loc Core.c_cons [e; of_list ?loc l]
+
+let of_qhyp ?loc = function
+| AnonHyp n -> constructor Core.c_anon_hyp [of_int ?loc n]
+| NamedHyp id -> constructor Core.c_named_hyp [of_ident ?loc id]
+
+let of_bindings ?loc = function
+| NoBindings ->
+  constructor ?loc Core.c_no_bindings []
+| ImplicitBindings tl ->
+  constructor ?loc Core.c_implicit_bindings [of_list ?loc tl]
+| ExplicitBindings tl ->
+  let tl = List.map (fun (loc, (qhyp, e)) -> of_pair ?loc (of_qhyp ?loc qhyp, e)) tl in
+  constructor ?loc Core.c_explicit_bindings [of_list ?loc tl]
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
new file mode 100644
index 0000000000..ba6a878d50
--- /dev/null
+++ b/src/tac2quote.mli
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Misctypes
+open Tac2expr
+
+(** Syntactic quoting of expressions. *)
+
+(** Contrarily to Tac2ffi, which lives on the semantic level, this module
+    manipulates pure syntax of Ltac2. Its main purpose is to write notations. *)
+
+val constructor : ?loc:Loc.t -> ltac_constructor -> raw_tacexpr list -> raw_tacexpr
+
+val of_int : ?loc:Loc.t -> int -> raw_tacexpr
+
+val of_pair : ?loc:Loc.t -> raw_tacexpr * raw_tacexpr -> raw_tacexpr
+
+val of_variable : ?loc:Loc.t -> Id.t -> raw_tacexpr
+
+val of_ident : ?loc:Loc.t -> Id.t -> raw_tacexpr
+
+val of_constr : ?loc:Loc.t -> Constrexpr.constr_expr -> raw_tacexpr
+
+val of_list : ?loc:Loc.t -> raw_tacexpr list -> raw_tacexpr
+
+val of_bindings : ?loc:Loc.t -> raw_tacexpr bindings -> raw_tacexpr