Introducing a macro for constr matching.

7 files changed, 104 insertions, 6 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index fce4c9e159..5d5bc6b941 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -368,7 +368,7 @@ 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 q_induction_clause
           q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag
-          q_reference q_with_bindings;
+          q_reference q_with_bindings q_constr_matching;
   anti:
     [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
   ;
@@ -661,6 +661,25 @@ GEXTEND Gram
   q_strategy_flag:
     [ [ flag = strategy_flag -> flag ] ]
   ;
+  match_pattern:
+    [ [ IDENT "context";  id = OPT Prim.ident;
+          "["; pat = Constr.lconstr_pattern; "]" -> (Some id, pat)
+      | pat = Constr.lconstr_pattern -> (None, pat) ] ]
+  ;
+  match_rule:
+    [ [ mp = match_pattern; "=>"; tac = tac2expr ->
+        match mp with
+        | None, pat -> Loc.tag ~loc:!@loc @@ QConstrMatchPattern (pat, tac)
+        | Some oid, pat -> Loc.tag ~loc:!@loc @@ QConstrMatchContext (oid, pat, tac)
+    ] ]
+  ;
+  match_list:
+    [ [ mrl = LIST1 match_rule SEP "|" -> Loc.tag ~loc:!@loc @@ mrl
+      | "|"; mrl = LIST1 match_rule SEP "|" -> Loc.tag ~loc:!@loc @@ mrl ] ]
+  ;
+  q_constr_matching:
+    [ [ m = match_list -> m ] ]
+  ;
 END
 
 (** Extension of constr syntax *)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index f5dd74d642..39fcff0c73 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open CSig
+open Util
 open Pp
 open Names
 open Genarg
@@ -1069,6 +1070,7 @@ let () = add_expr_scope "occurrences" q_occurrences Tac2quote.of_occurrences
 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 "constr_matching" q_constr_matching Tac2quote.of_constr_matching
 
 let () = add_generic_scope "constr" Pcoq.Constr.constr Tac2quote.wit_constr
 let () = add_generic_scope "open_constr" Pcoq.Constr.constr Tac2quote.wit_open_constr
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 9c5d9a659b..34022b86c9 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -36,6 +36,7 @@ let q_dispatch = Pcoq.Gram.entry_create "tactic:q_dispatch"
 let q_occurrences = Pcoq.Gram.entry_create "tactic:q_occurrences"
 let q_reference = Pcoq.Gram.entry_create "tactic:q_reference"
 let q_strategy_flag = Pcoq.Gram.entry_create "tactic:q_strategy_flag"
+let q_constr_matching = Pcoq.Gram.entry_create "tactic:q_constr_matching"
 end
 
 (** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 7ed45e62e5..dde877666a 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -71,6 +71,7 @@ val q_dispatch : dispatch Pcoq.Gram.entry
 val q_occurrences : occurrences Pcoq.Gram.entry
 val q_reference : Libnames.reference or_anti Pcoq.Gram.entry
 val q_strategy_flag : strategy_flag Pcoq.Gram.entry
+val q_constr_matching : constr_matching Pcoq.Gram.entry
 end
 
 (** {5 Hooks} *)
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 7c774a5c80..a284c1e756 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -115,3 +115,11 @@ type red_flag_r =
 type red_flag = red_flag_r located
 
 type strategy_flag = red_flag list located
+
+type constr_match_branch_r =
+| QConstrMatchPattern of Constrexpr.constr_expr * raw_tacexpr
+| QConstrMatchContext of Id.t option * Constrexpr.constr_expr * raw_tacexpr
+
+type constr_match_branch = constr_match_branch_r located
+
+type constr_matching = constr_match_branch list located
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 132716c37e..d38d7414fe 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -24,13 +24,21 @@ let wit_ltac1 = Arg.create "ltac1"
 
 (** Syntactic quoting of expressions. *)
 
-let control_prefix =
-  MPfile (DirPath.make (List.map Id.of_string ["Control"; "Ltac2"]))
+let prefix_gen n =
+  MPfile (DirPath.make (List.map Id.of_string [n; "Ltac2"]))
+
+let control_prefix = prefix_gen "Control"
+let pattern_prefix = prefix_gen "Pattern"
+let array_prefix = prefix_gen "Array"
 
 let kername prefix n = KerName.make2 prefix (Label.of_id (Id.of_string_soft n))
 let std_core n = kername Tac2env.std_prefix n
 let coq_core n = kername Tac2env.coq_prefix n
 let control_core n = kername control_prefix n
+let pattern_core n = kername pattern_prefix n
+
+let global_ref ?loc kn =
+  Loc.tag ?loc @@ CTacRef (AbsKn (TacConstant kn))
 
 let dummy_loc = Loc.make_loc (-1, -1)
 
@@ -226,15 +234,15 @@ let of_rewriting (loc, rew) =
   ])
 
 let of_hyp ?loc id =
-  let hyp = Loc.tag ?loc @@ CTacRef (AbsKn (TacConstant (control_core "hyp"))) in
+  let hyp = global_ref ?loc (control_core "hyp") in
   Loc.tag ?loc @@ CTacApp (hyp, [of_ident id])
 
 let of_exact_hyp ?loc id =
-  let refine = Loc.tag ?loc @@ CTacRef (AbsKn (TacConstant (control_core "refine"))) in
+  let refine = global_ref ?loc (control_core "refine") in
   Loc.tag ?loc @@ CTacApp (refine, [thunk (of_hyp ?loc id)])
 
 let of_exact_var ?loc id =
-  let refine = Loc.tag ?loc @@ CTacRef (AbsKn (TacConstant (control_core "refine"))) in
+  let refine = global_ref ?loc (control_core "refine") in
   Loc.tag ?loc @@ CTacApp (refine, [thunk (of_variable id)])
 
 let of_dispatch tacs =
@@ -296,3 +304,59 @@ let of_strategy_flag (loc, flag) =
     std_proj "rDelta", of_bool ?loc flag.rDelta;
     std_proj "rConst", of_list ?loc of_reference flag.rConst;
   ])
+
+let pattern_vars pat =
+  let rec aux () accu pat = match pat.CAst.v with
+  | Constrexpr.CPatVar id -> Id.Set.add id accu
+  | Constrexpr.CEvar (id, []) -> Id.Set.add id accu
+  | _ ->
+    Topconstr.fold_constr_expr_with_binders (fun _ () -> ()) aux () accu pat
+  in
+  aux () Id.Set.empty pat
+
+let of_constr_matching (loc, m) =
+  let check_id loc id =
+    if Tac2env.is_constructor (Libnames.qualid_of_ident id) then
+      CErrors.user_err ?loc (str "Invalid pattern binding name " ++ Id.print id)
+  in
+  let abstract_vars loc pat tac =
+    let vars = pattern_vars pat in
+    let na, tac =
+      if Id.Set.is_empty vars then (Anonymous, tac)
+      else
+        (** Trick: in order not to shadow a variable nor to choose an arbitrary
+            name, we reuse one which is going to be shadowed by the matched
+            variables anyways. *)
+        let id0 = Id.Set.choose vars in
+        let build_bindings id (n, accu) =
+          let () = check_id loc id in
+          let get = global_ref ?loc (kername array_prefix "get")  in
+          let args = [of_variable (loc, id0); of_int (loc, n)] in
+          let e = Loc.tag ?loc @@ CTacApp (get, args) in
+          let accu = (Loc.tag ?loc @@ CPatVar (Name id), None, e) :: accu in
+          (n + 1, accu)
+        in
+        let (_, bnd) = Id.Set.fold build_bindings vars (0, []) in
+        let tac = Loc.tag ?loc @@ CTacLet (false, bnd, tac) in
+        (Name id0, tac)
+    in
+    Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar na, None], tac)
+  in
+  let map (loc, p) = match p with
+  | QConstrMatchPattern (pat, tac) ->
+    let e = abstract_vars loc pat tac in
+    let pat = inj_wit ?loc wit_pattern pat in
+    constructor ?loc (pattern_core "ConstrMatchPattern") [pat; e]
+  | QConstrMatchContext (id, pat, tac) ->
+    let e = abstract_vars loc pat tac in
+    let na = match id with
+    | None -> Anonymous
+    | Some id ->
+      let () = check_id loc id in
+      Name id
+    in
+    let e = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar na, None], e) in
+    let pat = inj_wit ?loc wit_pattern pat in
+    constructor ?loc (pattern_core "ConstrMatchContext") [pat; e]
+  in
+  of_list ?loc map m
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 440759ada7..c3374ac24e 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Loc
 open Names
 open Tac2dyn
@@ -66,6 +67,8 @@ val of_dispatch : dispatch -> raw_tacexpr
 
 val of_strategy_flag : strategy_flag -> raw_tacexpr
 
+val of_constr_matching : constr_matching -> raw_tacexpr
+
 (** {5 Generic arguments} *)
 
 val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern) Arg.tag