Introducing the all-mighty intro-patterns.

11 files changed, 250 insertions, 24 deletions

diff --git a/_CoqProject b/_CoqProject
index ab73af1295..b8064c46a4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -17,6 +17,7 @@ src/tac2ffi.ml
 src/tac2ffi.mli
 src/tac2core.ml
 src/tac2core.mli
+src/tac2qexpr.mli
 src/tac2quote.ml
 src/tac2quote.mli
 src/tac2stdlib.ml
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 4a2f615df9..b058680645 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -14,6 +14,7 @@ open Pcoq
 open Constrexpr
 open Misctypes
 open Tac2expr
+open Tac2qexpr
 open Ltac_plugin
 
 let err () = raise Stream.Failure
@@ -44,9 +45,6 @@ let inj_wit wit loc x = CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x)
 let inj_open_constr loc c = inj_wit Stdarg.wit_open_constr 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
@@ -278,14 +276,19 @@ END
 
 open Tac2entries.Pltac
 
+let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
+
 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
+  GLOBAL: q_ident q_bindings q_intropatterns;
+  ident_or_anti:
+    [ [ id = Prim.ident -> QExpr id
+      | "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
     ] ]
   ;
- simple_binding:
+  q_ident:
+    [ [ id = ident_or_anti -> Tac2quote.of_anti ~loc:!@loc Tac2quote.of_ident 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; ")" ->
@@ -302,9 +305,61 @@ GEXTEND Gram
   ;
   q_bindings:
     [ [ "with"; bl = bindings -> bl
-      | -> mk_constr ~loc:!@loc Tac2core.Core.c_no_bindings []
+      | -> Tac2quote.of_bindings ~loc:!@loc Misctypes.NoBindings
     ] ]
   ;
+  intropatterns:
+    [ [ l = LIST0 nonsimple_intropattern -> l ]]
+  ;
+(*   ne_intropatterns: *)
+(*     [ [ l = LIST1 nonsimple_intropattern -> l ]] *)
+(*   ; *)
+  or_and_intropattern:
+    [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> QIntroOrPattern tc
+      | "()" -> QIntroAndPattern []
+      | "("; si = simple_intropattern; ")" -> QIntroAndPattern [si]
+      | "("; si = simple_intropattern; ",";
+             tc = LIST1 simple_intropattern SEP "," ; ")" ->
+             QIntroAndPattern (si::tc)
+      | "("; si = simple_intropattern; "&";
+	     tc = LIST1 simple_intropattern SEP "&" ; ")" ->
+	  (* (A & B & C) is translated into (A,(B,C)) *)
+	  let rec pairify = function
+	    | ([]|[_]|[_;_]) as l -> l
+	    | t::q -> [t; (QIntroAction (QIntroOrAndPattern (QIntroAndPattern (pairify q))))]
+	  in QIntroAndPattern (pairify (si::tc)) ] ]
+  ;
+  equality_intropattern:
+    [ [ "->" -> QIntroRewrite true
+      | "<-" -> QIntroRewrite false
+      | "[="; tc = intropatterns; "]" -> QIntroInjection tc ] ]
+  ;
+  naming_intropattern:
+    [ [ LEFTQMARK; prefix = ident_or_anti -> QIntroFresh prefix
+      | LEFTQMARK -> QIntroAnonymous
+      | id = ident_or_anti -> QIntroIdentifier id ] ]
+  ;
+  nonsimple_intropattern:
+    [ [ l = simple_intropattern -> l
+      | "*"  -> QIntroForthcoming true
+      | "**" -> QIntroForthcoming false ]]
+  ;
+  simple_intropattern:
+    [ [ pat = simple_intropattern_closed ->
+(*         l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] -> *)
+        (** TODO: handle %pat *)
+        pat
+    ] ]
+  ;
+  simple_intropattern_closed:
+    [ [ pat = or_and_intropattern   -> QIntroAction (QIntroOrAndPattern pat)
+      | pat = equality_intropattern -> QIntroAction pat
+      | "_" -> QIntroAction QIntroWildcard 
+      | pat = naming_intropattern -> QIntroNaming pat ] ]
+  ;
+  q_intropatterns:
+    [ [ ipat = intropatterns -> Tac2quote.of_intro_patterns ~loc:!@loc ipat ] ]
+  ;
 END
 
 (** Extension of constr syntax *)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index fef16dcc06..266e3b5f11 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -42,10 +42,8 @@ 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 c_true = coq_core "true"
+let c_false = coq_core "false"
 
 let t_qhyp = std_core "hypothesis"
 let c_named_hyp = std_core "NamedHyp"
@@ -853,6 +851,14 @@ let () = add_scope "ident" begin function
 | _ -> scope_fail ()
 end
 
+let () = add_scope "thunk" begin function
+| [tok] ->
+  let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+  let act e = rthunk (act e) in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
 let () = add_scope "bindings" begin function
 | [] ->
   let scope = Extend.Aentry Tac2entries.Pltac.q_bindings in
@@ -861,10 +867,10 @@ let () = add_scope "bindings" begin function
 | _ -> scope_fail ()
 end
 
-let () = add_scope "thunk" begin function
-| [tok] ->
-  let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
-  let act e = rthunk (act e) in
+let () = add_scope "intropatterns" begin function
+| [] ->
+  let scope = Extend.Aentry Tac2entries.Pltac.q_intropatterns in
+  let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | _ -> scope_fail ()
 end
diff --git a/src/tac2core.mli b/src/tac2core.mli
index 118b7aaa42..6fd48e85f7 100644
--- a/src/tac2core.mli
+++ b/src/tac2core.mli
@@ -24,10 +24,8 @@ 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 c_true : ltac_constructor
+val c_false : ltac_constructor
 
 val t_qhyp : type_constant
 val c_anon_hyp : ltac_constructor
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index d293a87975..d7ee07e9e2 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -26,6 +26,7 @@ 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"
+let q_intropatterns = Pcoq.Gram.entry_create "tactic:q_intropatterns"
 end
 
 (** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 4d5a234daf..e5031fdba2 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -59,4 +59,5 @@ val tac2expr : raw_tacexpr Pcoq.Gram.entry
 
 val q_ident : raw_tacexpr Pcoq.Gram.entry
 val q_bindings : raw_tacexpr Pcoq.Gram.entry
+val q_intropatterns : raw_tacexpr Pcoq.Gram.entry
 end
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
new file mode 100644
index 0000000000..794281cc75
--- /dev/null
+++ b/src/tac2qexpr.mli
@@ -0,0 +1,36 @@
+(************************************************************************)
+(*  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 Util
+open Loc
+open Names
+
+(** Quoted variants of Ltac syntactic categories. Contrarily to the former, they
+    sometimes allow anti-quotations. Used for notation scopes. *)
+
+type 'a or_anti =
+| QExpr of 'a
+| QAnti of Id.t located
+
+type intro_pattern =
+| QIntroForthcoming of bool
+| QIntroNaming of intro_pattern_naming
+| QIntroAction of intro_pattern_action
+and intro_pattern_naming =
+| QIntroIdentifier of Id.t or_anti
+| QIntroFresh of Id.t or_anti
+| QIntroAnonymous
+and intro_pattern_action =
+| QIntroWildcard
+| QIntroOrAndPattern of or_and_intro_pattern
+| QIntroInjection of intro_pattern list
+(* | QIntroApplyOn of Empty.t (** Not implemented yet *) *)
+| QIntroRewrite of bool
+and or_and_intro_pattern =
+| QIntroOrPattern of intro_pattern list list
+| QIntroAndPattern of intro_pattern list
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 2d9521d30c..96a3a5d9b8 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -7,14 +7,18 @@
 (************************************************************************)
 
 open Pp
+open Names
 open Util
 open Misctypes
 open Tac2intern
 open Tac2expr
+open Tac2qexpr
 open Tac2core
 
 (** Syntactic quoting of expressions. *)
 
+let std_core n = KerName.make2 Tac2env.std_prefix (Label.of_id (Id.of_string n))
+
 let dummy_loc = Loc.make_loc (-1, -1)
 
 let constructor ?loc kn args =
@@ -23,6 +27,9 @@ let constructor ?loc kn args =
   if List.is_empty args then cst
   else CTacApp (loc, cst, args)
 
+let std_constructor ?loc name args =
+  constructor ?loc (std_core name) args
+
 let of_pair ?loc (e1, e2) =
   let loc = Option.default dummy_loc loc in
   CTacApp (loc, CTacCst (loc, AbsKn (Tuple 2)), [e1; e2])
@@ -40,10 +47,18 @@ let of_variable ?loc id =
     CErrors.user_err ?loc (str "Invalid identifier")
   else CTacRef (RelId (Loc.tag ?loc qid))
 
+let of_anti ?loc f = function
+| QExpr x -> f ?loc x
+| QAnti (loc, id) -> of_variable ?loc id
+
 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 of_bool ?loc b =
+  let c = if b then Core.c_true else Core.c_false in
+  constructor ?loc c []
+
 let rec of_list ?loc = function
 | [] -> constructor Core.c_nil []
 | e :: l ->
@@ -55,9 +70,45 @@ let of_qhyp ?loc = function
 
 let of_bindings ?loc = function
 | NoBindings ->
-  constructor ?loc Core.c_no_bindings []
+  std_constructor ?loc "NoBindings" []
 | ImplicitBindings tl ->
-  constructor ?loc Core.c_implicit_bindings [of_list ?loc tl]
+  std_constructor ?loc "ImplicitBindings" [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]
+  std_constructor ?loc "ExplicitBindings" [of_list ?loc tl]
+
+let rec of_intro_pattern ?loc = function
+| QIntroForthcoming b ->
+  std_constructor ?loc "IntroForthcoming" [of_bool b]
+| QIntroNaming iname ->
+  std_constructor ?loc "IntroNaming" [of_intro_pattern_naming iname]
+| QIntroAction iact ->
+  std_constructor ?loc "IntroAction" [of_intro_pattern_action iact]
+
+and of_intro_pattern_naming ?loc = function
+| QIntroIdentifier id ->
+  std_constructor ?loc "IntroIdentifier" [of_anti ?loc of_ident id]
+| QIntroFresh id ->
+  std_constructor ?loc "IntroFresh" [of_anti ?loc of_ident id]
+| QIntroAnonymous ->
+  std_constructor ?loc "IntroAnonymous" []
+
+and of_intro_pattern_action ?loc = function
+| QIntroWildcard ->
+  std_constructor ?loc "IntroWildcard" []
+| QIntroOrAndPattern pat ->
+  std_constructor ?loc "IntroOrAndPattern" [of_or_and_intro_pattern ?loc pat]
+| QIntroInjection il ->
+  std_constructor ?loc "IntroInjection" [of_intro_patterns ?loc il]
+| QIntroRewrite b ->
+  std_constructor ?loc "IntroRewrite" [of_bool ?loc b]
+
+and of_or_and_intro_pattern ?loc = function
+| QIntroOrPattern ill ->
+  let ill = List.map (of_intro_patterns ?loc) ill in
+  std_constructor ?loc "IntroOrPattern" [of_list ?loc ill]
+| QIntroAndPattern il ->
+  std_constructor ?loc "IntroAndPattern" [of_intro_patterns ?loc il]
+
+and of_intro_patterns ?loc l =
+  of_list ?loc (List.map (of_intro_pattern ?loc) l)
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index ba6a878d50..32973ff5ba 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Misctypes
+open Tac2qexpr
 open Tac2expr
 
 (** Syntactic quoting of expressions. *)
@@ -17,6 +18,8 @@ open Tac2expr
 
 val constructor : ?loc:Loc.t -> ltac_constructor -> raw_tacexpr list -> raw_tacexpr
 
+val of_anti : ?loc:Loc.t -> (?loc:Loc.t -> 'a -> raw_tacexpr) -> 'a or_anti -> raw_tacexpr
+
 val of_int : ?loc:Loc.t -> int -> raw_tacexpr
 
 val of_pair : ?loc:Loc.t -> raw_tacexpr * raw_tacexpr -> raw_tacexpr
@@ -30,3 +33,7 @@ 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
+
+val of_intro_pattern : ?loc:Loc.t -> intro_pattern -> raw_tacexpr
+
+val of_intro_patterns : ?loc:Loc.t -> intro_pattern list -> raw_tacexpr
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index e093b5c97f..44fad48955 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -85,6 +85,39 @@ let to_red_flag = function
   }
 | _ -> assert false
 
+let rec to_intro_pattern = function
+| ValBlk (0, [| b |]) -> IntroForthcoming (Value.to_bool b)
+| ValBlk (1, [| pat |]) -> IntroNaming (to_intro_pattern_naming pat)
+| ValBlk (2, [| act |]) -> IntroAction (to_intro_pattern_action act)
+| _ -> assert false
+
+and to_intro_pattern_naming = function
+| ValBlk (0, [| id |]) -> IntroIdentifier (Value.to_ident id)
+| ValBlk (1, [| id |]) -> IntroFresh (Value.to_ident id)
+| ValInt 0 -> IntroAnonymous
+| _ -> assert false
+
+and to_intro_pattern_action = function
+| ValInt 0 -> IntroWildcard
+| ValBlk (0, [| op |]) -> IntroOrAndPattern (to_or_and_intro_pattern op)
+| ValBlk (1, [| inj |]) ->
+  let map ipat = Loc.tag (to_intro_pattern ipat) in
+  IntroInjection (Value.to_list map inj)
+| ValBlk (2, [| _ |]) -> IntroApplyOn (assert false, assert false) (** TODO *)
+| ValBlk (3, [| b |]) -> IntroRewrite (Value.to_bool b)
+| _ -> assert false
+
+and to_or_and_intro_pattern = function
+| ValBlk (0, [| ill |]) ->
+  IntroOrPattern (Value.to_list to_intro_patterns ill)
+| ValBlk (1, [| il |]) ->
+  IntroAndPattern (to_intro_patterns il)
+| _ -> assert false
+
+and to_intro_patterns il =
+  let map ipat = Loc.tag (to_intro_pattern ipat) in
+  Value.to_list map il
+
 (** Standard tactics sharing their implementation with Ltac1 *)
 
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
@@ -132,6 +165,16 @@ let define_prim3 name tac =
 
 (** Tactics from Tacexpr *)
 
+let () = define_prim1 "tac_intros" begin fun ipat ->
+  let ipat = to_intro_patterns ipat in
+  Tactics.intros_patterns false ipat
+end
+
+let () = define_prim1 "tac_eintros" begin fun ipat ->
+  let ipat = to_intro_patterns ipat in
+  Tactics.intros_patterns true ipat
+end
+
 let () = define_prim2 "tac_eelim" begin fun c copt ->
   let c = to_constr_with_bindings c in
   let copt = Value.to_option to_constr_with_bindings copt in
diff --git a/theories/Std.v b/theories/Std.v
index 3070c2e005..a27790c35d 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -49,8 +49,35 @@ Ltac2 Type red_flags := {
   rConst : evaluable_reference list
 }.
 
+Ltac2 Type 'a not_implemented.
+
+Ltac2 Type rec intro_pattern := [
+| IntroForthcoming (bool)
+| IntroNaming (intro_pattern_naming)
+| IntroAction (intro_pattern_action)
+]
+with intro_pattern_naming := [
+| IntroIdentifier (ident)
+| IntroFresh (ident)
+| IntroAnonymous
+]
+with intro_pattern_action := [
+| IntroWildcard
+| IntroOrAndPattern (or_and_intro_pattern)
+| IntroInjection (intro_pattern list)
+| IntroApplyOn ((constr * intro_pattern) not_implemented) (* Not Implemented yet *)
+| IntroRewrite (bool)
+]
+with or_and_intro_pattern := [
+| IntroOrPattern (intro_pattern list list)
+| IntroAndPattern (intro_pattern list)
+].
+
 (** Standard, built-in tactics. See Ltac1 for documentation. *)
 
+Ltac2 @ external intros : intro_pattern list -> unit := "ltac2" "tac_intros".
+Ltac2 @ external eintros : intro_pattern list -> unit := "ltac2" "tac_eintros".
+
 Ltac2 @ external eelim : constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_eelim".
 Ltac2 @ external ecase : constr_with_bindings -> unit := "ltac2" "tac_ecase".