Introducing notations for destruct and induction arguments.

9 files changed, 223 insertions, 11 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index ca3631799b..8c7db71a47 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -30,7 +30,7 @@ let test_lpar_idnum_coloneq =
                   (match stream_nth 2 strm with
                     | KEYWORD ":=" -> ()
                     | _ -> err ())
-              | LEFTQMARK ->
+              | KEYWORD "$" ->
                 (match stream_nth 2 strm with
                   | IDENT _ ->
                       (match stream_nth 3 strm with
@@ -40,6 +40,20 @@ let test_lpar_idnum_coloneq =
               | _ -> err ())
         | _ -> err ())
 
+(* Hack to recognize "(x)" *)
+let test_lpar_id_rpar =
+  Gram.Entry.of_parser "lpar_id_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 ())
+	      | _ -> err ())
+	| _ -> err ())
+
 let tac2expr = Tac2entries.Pltac.tac2expr
 let tac2type = Gram.entry_create "tactic:tac2type"
 let tac2def_val = Gram.entry_create "tactic:tac2def_val"
@@ -291,17 +305,17 @@ 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_intropattern q_intropatterns;
+  GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause;
   ident_or_anti:
     [ [ id = Prim.ident -> QExpr id
-      | LEFTQMARK; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
+      | "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
     ] ]
   ;
   q_ident:
     [ [ id = ident_or_anti -> Tac2quote.of_anti ~loc:!@loc Tac2quote.of_ident id ] ]
   ;
   simple_binding:
-    [ [ "("; LEFTQMARK; id = Prim.ident; ":="; c = Constr.lconstr; ")" ->
+    [ [ "("; "$"; id = Prim.ident; ":="; c = Constr.lconstr; ")" ->
         Loc.tag ~loc:!@loc (QAnti (Loc.tag ~loc:!@loc id), Tac2quote.of_open_constr ~loc:!@loc c)
       | "("; n = Prim.natural; ":="; c = Constr.lconstr; ")" ->
         Loc.tag ~loc:!@loc (QExpr (AnonHyp n), Tac2quote.of_open_constr ~loc:!@loc c)
@@ -378,6 +392,89 @@ GEXTEND Gram
   q_intropattern:
     [ [ ipat = simple_intropattern -> Tac2quote.of_intro_pattern ~loc:!@loc ipat ] ]
   ;
+  nat_or_anti:
+    [ [ n = Prim.natural -> QExpr n
+      | "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
+    ] ]
+  ;
+  eqn_ipat:
+    [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some pat
+      | -> None
+    ] ]
+  ;
+  with_bindings:
+    [ [ "with"; bl = bindings -> bl | -> QNoBindings ] ]
+  ;
+  constr_with_bindings:
+    [ [ c = Constr.constr; l = with_bindings -> (c, l) ] ]
+  ;
+  destruction_arg:
+    [ [ n = Prim.natural -> QElimOnAnonHyp n
+      | (c, bnd) = constr_with_bindings -> QElimOnConstr (c, bnd)
+    ] ]
+  ;
+  as_or_and_ipat:
+    [ [ "as"; ipat = or_and_intropattern -> Some ipat
+      | -> None
+    ] ]
+  ;
+  occs_nums:
+    [ [ nl = LIST1 nat_or_anti -> QOnlyOccurrences nl
+      | "-"; n = nat_or_anti; nl = LIST0 nat_or_anti ->
+        QAllOccurrencesBut (n::nl)
+    ] ]
+  ;
+  occs:
+    [ [ "at"; occs = occs_nums -> occs | -> QAllOccurrences ] ]
+  ;
+  hypident:
+    [ [ id = ident_or_anti ->
+          id,Locus.InHyp
+      | "("; IDENT "type"; IDENT "of"; id = ident_or_anti; ")" ->
+	  id,Locus.InHypTypeOnly
+      | "("; IDENT "value"; IDENT "of"; id = ident_or_anti; ")" ->
+	  id,Locus.InHypValueOnly
+    ] ]
+  ;
+  hypident_occ:
+    [ [ (id,l)=hypident; occs=occs -> ((occs,id),l) ] ]
+  ;
+  in_clause:
+    [ [ "*"; occs=occs ->
+        { q_onhyps = None; q_concl_occs = occs }
+      | "*"; "|-"; occs = concl_occ ->
+        { q_onhyps = None; q_concl_occs = occs }
+      | hl = LIST0 hypident_occ SEP ","; "|-"; occs = concl_occ ->
+        { q_onhyps = Some hl; q_concl_occs = occs }
+      | hl = LIST0 hypident_occ SEP "," ->
+        { q_onhyps = Some hl; q_concl_occs = QNoOccurrences }
+    ] ]
+  ;
+  opt_clause:
+    [ [ "in"; cl = in_clause -> Some cl
+      | "at"; occs = occs_nums -> Some { q_onhyps = Some []; q_concl_occs = occs }
+      | -> None
+    ] ]
+  ;
+  concl_occ:
+    [ [ "*"; occs = occs -> occs
+      | -> QNoOccurrences
+    ] ]
+  ;
+  induction_clause:
+    [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
+        cl = opt_clause ->
+        {
+          indcl_arg = c;
+          indcl_eqn = eq;
+          indcl_as = pat;
+          indcl_in = cl;
+        }
+    ] ]
+  ;
+  q_induction_clause:
+    [ [ cl = induction_clause -> Tac2quote.of_induction_clause ~loc:!@loc cl ] ]
+  ;
 END
 
 (** Extension of constr syntax *)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 329c115be3..45fa52ff9b 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -899,6 +899,14 @@ let () = add_scope "intropatterns" begin function
 | _ -> scope_fail ()
 end
 
+let () = add_scope "induction_clause" begin function
+| [] ->
+  let scope = Extend.Aentry Tac2entries.Pltac.q_induction_clause in
+  let act tac = tac in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
 let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr
 let () = add_generic_scope "open_constr" Pcoq.Constr.constr Stdarg.wit_open_constr
 
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 52a5899d25..ce86e8aa33 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -28,6 +28,7 @@ let q_ident = Pcoq.Gram.entry_create "tactic:q_ident"
 let q_bindings = Pcoq.Gram.entry_create "tactic:q_bindings"
 let q_intropattern = Pcoq.Gram.entry_create "tactic:q_intropattern"
 let q_intropatterns = Pcoq.Gram.entry_create "tactic:q_intropatterns"
+let q_induction_clause = Pcoq.Gram.entry_create "tactic:q_induction_clause"
 end
 
 (** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 2e51a4fb2e..1567551246 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -61,4 +61,5 @@ val q_ident : raw_tacexpr Pcoq.Gram.entry
 val q_bindings : raw_tacexpr Pcoq.Gram.entry
 val q_intropattern : raw_tacexpr Pcoq.Gram.entry
 val q_intropatterns : raw_tacexpr Pcoq.Gram.entry
+val q_induction_clause : raw_tacexpr Pcoq.Gram.entry
 end
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index b68efe73ac..5075f2d7d4 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -40,3 +40,26 @@ and intro_pattern_action =
 and or_and_intro_pattern =
 | QIntroOrPattern of intro_pattern list list
 | QIntroAndPattern of intro_pattern list
+
+type occurrences =
+| QAllOccurrences
+| QAllOccurrencesBut of int or_anti list
+| QNoOccurrences
+| QOnlyOccurrences of int or_anti list
+
+type hyp_location = (occurrences * Id.t or_anti) * Locus.hyp_location_flag
+
+type clause =
+  { q_onhyps : hyp_location list option; q_concl_occs : occurrences; }
+
+type destruction_arg =
+| QElimOnConstr of Constrexpr.constr_expr * bindings
+| QElimOnIdent of Id.t
+| QElimOnAnonHyp of int
+
+type induction_clause = {
+  indcl_arg : destruction_arg;
+  indcl_eqn : intro_pattern_naming option;
+  indcl_as : or_and_intro_pattern option;
+  indcl_in : clause option;
+}
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index e30acc48ab..9858f611fe 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -36,13 +36,31 @@ let constructor ?loc kn args =
 let std_constructor ?loc name args =
   constructor ?loc (std_core name) args
 
+let std_proj ?loc name =
+  AbsKn (std_core name)
+
+let thunk e =
+  let t_unit = coq_core "unit" in
+  let loc = Tac2intern.loc_of_tacexpr e in
+  let var = [CPatVar (Some loc, Anonymous), Some (CTypRef (loc, AbsKn (Other t_unit), []))] in
+  CTacFun (loc, var, e)
+
 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_tuple ?loc el =
+  let loc = Option.default dummy_loc loc in
+  let len = List.length el in
+  CTacApp (loc, CTacCst (loc, AbsKn (Tuple len)), el)
+
 let of_int ?loc n =
   CTacAtm (Loc.tag ?loc (AtmInt n))
 
+let of_option ?loc opt = match opt with
+| None -> constructor ?loc (coq_core "None") []
+| Some e -> constructor ?loc (coq_core "Some") [e]
+
 let inj_wit ?loc wit x =
   let loc = Option.default dummy_loc loc in
   CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x)
@@ -121,17 +139,66 @@ and of_or_and_intro_pattern ?loc = function
 and of_intro_patterns ?loc l =
   of_list ?loc (List.map (of_intro_pattern ?loc) l)
 
+let of_hyp_location_flag ?loc = function
+| Locus.InHyp -> std_constructor ?loc "InHyp" []
+| Locus.InHypTypeOnly -> std_constructor ?loc "InHypTypeOnly" []
+| Locus.InHypValueOnly -> std_constructor ?loc "InHypValueOnly" []
+
+let of_occurrences ?loc occ = match occ with
+| QAllOccurrences -> std_constructor ?loc "AllOccurrences" []
+| QAllOccurrencesBut occs ->
+  let map occ = of_anti ?loc of_int occ in
+  let occs = of_list ?loc (List.map map occs) in
+  std_constructor ?loc "AllOccurrencesBut" [occs]
+| QNoOccurrences -> std_constructor ?loc "NoOccurrences" []
+| QOnlyOccurrences occs ->
+  let map occ = of_anti ?loc of_int occ in
+  let occs = of_list ?loc (List.map map occs) in
+  std_constructor ?loc "OnlyOccurrences" [occs]
+
+let of_hyp_location ?loc ((occs, id), flag) =
+  of_tuple ?loc [
+    of_anti ?loc of_ident id;
+    of_occurrences ?loc occs;
+    of_hyp_location_flag ?loc flag;
+  ]
+
+let of_clause ?loc cl =
+  let loc = Option.default dummy_loc loc in
+  let hyps = of_option ~loc (Option.map (fun l -> of_list ~loc (List.map of_hyp_location l)) cl.q_onhyps) in
+  let concl = of_occurrences ~loc cl.q_concl_occs in
+  CTacRec (loc, [
+    std_proj "on_hyps", hyps;
+    std_proj "on_concl", concl;
+  ])
+
+let of_destruction_arg ?loc = function
+| QElimOnConstr (c, bnd) ->
+  let c = of_constr ?loc c in
+  let bnd = of_bindings ?loc bnd in
+  let arg = thunk (of_pair ?loc (c, bnd)) in
+  std_constructor ?loc "ElimOnConstr" [arg]
+| QElimOnIdent id -> std_constructor ?loc "ElimOnIdent" [of_ident ?loc id]
+| QElimOnAnonHyp n -> std_constructor ?loc "ElimOnAnonHyp" [of_int ?loc n]
+
+let of_induction_clause ?loc cl =
+  let arg = of_destruction_arg ?loc cl.indcl_arg in
+  let eqn = of_option ?loc (Option.map of_intro_pattern_naming cl.indcl_eqn) in
+  let as_ = of_option ?loc (Option.map of_or_and_intro_pattern cl.indcl_as) in
+  let in_ = of_option ?loc (Option.map of_clause cl.indcl_in) in
+  let loc = Option.default dummy_loc loc in
+  CTacRec (loc, [
+    std_proj "indcl_arg", arg;
+    std_proj "indcl_eqn", eqn;
+    std_proj "indcl_as", as_;
+    std_proj "indcl_in", in_;
+  ])
+
 let of_hyp ?loc id =
   let loc = Option.default dummy_loc loc in
   let hyp = CTacRef (AbsKn (control_core "hyp")) in
   CTacApp (loc, hyp, [of_ident ~loc id])
 
-let thunk e =
-  let t_unit = coq_core "unit" in
-  let loc = Tac2intern.loc_of_tacexpr e in
-  let var = [CPatVar (Some loc, Anonymous), Some (CTypRef (loc, AbsKn (Other t_unit), []))] in
-  CTacFun (loc, var, e)
-
 let of_exact_hyp ?loc id =
   let loc = Option.default dummy_loc loc in
   let refine = CTacRef (AbsKn (control_core "refine")) in
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 4cbe854f75..40ea58e334 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -40,6 +40,8 @@ val of_intro_pattern : ?loc:Loc.t -> intro_pattern -> raw_tacexpr
 
 val of_intro_patterns : ?loc:Loc.t -> intro_pattern list -> raw_tacexpr
 
+val of_induction_clause : ?loc:Loc.t -> induction_clause -> raw_tacexpr
+
 val of_hyp : ?loc:Loc.t -> Id.t -> raw_tacexpr
 (** id ↦ 'Control.hyp @id' *)
 
diff --git a/tests/example2.v b/tests/example2.v
index 79f230ab57..d89dcfd450 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -16,7 +16,7 @@ Qed.
 
 Goal exists n, n = 0.
 Proof.
-let myvar := Std.NamedHyp @x in split with (?myvar := 0).
+let myvar := Std.NamedHyp @x in split with ($myvar := 0).
 split.
 Qed.
 
diff --git a/theories/Std.v b/theories/Std.v
index 3d1e8f462d..c2027e41c7 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -73,6 +73,19 @@ with or_and_intro_pattern := [
 | IntroAndPattern (intro_pattern list)
 ].
 
+Ltac2 Type destruction_arg := [
+| ElimOnConstr (unit -> constr_with_bindings)
+| ElimOnIdent (ident)
+| ElimOnAnonHyp (int)
+].
+
+Ltac2 Type induction_clause := {
+  indcl_arg : destruction_arg;
+  indcl_eqn : intro_pattern_naming option;
+  indcl_as : or_and_intro_pattern option;
+  indcl_in : clause option;
+}.
+
 Ltac2 Type evar_flag := bool.
 Ltac2 Type advanced_flag := bool.