Stubs for goal matching: quotation and matching function.

12 files changed, 459 insertions, 53 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index c92a242637..be6c2de5a9 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -376,7 +376,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_pose q_assert;
+          q_goal_matching q_hintdb q_move_location q_pose q_assert;
   anti:
     [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
   ;
@@ -682,14 +682,12 @@ GEXTEND Gram
   ;
   match_pattern:
     [ [ IDENT "context";  id = OPT Prim.ident;
-          "["; pat = Constr.lconstr_pattern; "]" -> (Some id, pat)
-      | pat = Constr.lconstr_pattern -> (None, pat) ] ]
+          "["; pat = Constr.lconstr_pattern; "]" -> Loc.tag ~loc:!@loc @@ QConstrMatchContext (id, pat)
+      | pat = Constr.lconstr_pattern -> Loc.tag ~loc:!@loc @@ QConstrMatchPattern 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)
+        Loc.tag ~loc:!@loc @@ (mp, tac)
     ] ]
   ;
   match_list:
@@ -699,6 +697,29 @@ GEXTEND Gram
   q_constr_matching:
     [ [ m = match_list -> m ] ]
   ;
+  gmatch_hyp_pattern:
+    [ [ na = Prim.name; ":"; pat = match_pattern -> (na, pat) ] ]
+  ;
+  gmatch_pattern:
+    [ [ "["; hl = LIST0 gmatch_hyp_pattern SEP ","; "|-"; p = match_pattern; "]" ->
+        Loc.tag ~loc:!@loc @@ {
+          q_goal_match_concl = p;
+          q_goal_match_hyps = hl;
+        }
+    ] ]
+  ;
+  gmatch_rule:
+    [ [ mp = gmatch_pattern; "=>"; tac = tac2expr ->
+        Loc.tag ~loc:!@loc @@ (mp, tac)
+    ] ]
+  ;
+  gmatch_list:
+    [ [ mrl = LIST1 gmatch_rule SEP "|" -> Loc.tag ~loc:!@loc @@ mrl
+      | "|"; mrl = LIST1 gmatch_rule SEP "|" -> Loc.tag ~loc:!@loc @@ mrl ] ]
+  ;
+  q_goal_matching:
+    [ [ m = gmatch_list -> m ] ]
+  ;
   move_location:
     [ [ "at"; IDENT "top" -> Loc.tag ~loc:!@loc @@ QMoveFirst
       | "at"; IDENT "bottom" -> Loc.tag ~loc:!@loc @@ QMoveLast
diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack
index a2237f4d26..40b91e4b53 100644
--- a/src/ltac2_plugin.mlpack
+++ b/src/ltac2_plugin.mlpack
@@ -6,6 +6,7 @@ Tac2intern
 Tac2interp
 Tac2entries
 Tac2quote
+Tac2match
 Tac2core
 Tac2tactics
 Tac2stdlib
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 468fddaddf..c4502f8eae 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -528,6 +528,12 @@ end
 
 (** Patterns *)
 
+let empty_context = EConstr.mkMeta Constr_matching.special_meta
+
+let () = define0 "pattern_empty_context" begin
+  return (Value.of_constr empty_context)
+end
+
 let () = define2 "pattern_matches" pattern constr begin fun pat c ->
   pf_apply begin fun env sigma ->
     let ans =
@@ -592,6 +598,25 @@ let () = define2 "pattern_matches_subterm_vect" pattern constr begin fun pat c -
   end
 end
 
+let () = define3 "pattern_matches_goal" bool (list (pair bool pattern)) (pair bool pattern) begin fun rev hp cp ->
+  assert_focussed >>= fun () ->
+  Proofview.Goal.enter_one begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let concl = Proofview.Goal.concl gl in
+  let mk_pattern (b, pat) = if b then Tac2match.MatchContext pat else Tac2match.MatchPattern pat in
+  let r = (List.map mk_pattern hp, mk_pattern cp) in
+  Tac2match.match_goal env sigma concl ~rev r >>= fun (hyps, ctx, subst) ->
+    let of_ctxopt ctx = Value.of_constr (Option.default empty_context ctx) in
+    let hids = Value.of_array Value.of_ident (Array.map_of_list fst hyps) in
+    let hctx = Value.of_array of_ctxopt (Array.map_of_list snd hyps) in
+    let subs = Value.of_array Value.of_constr (Array.map_of_list snd (Id.Map.bindings subst)) in
+    let cctx = of_ctxopt ctx in
+    let ans = Value.of_tuple [| hids; hctx; subs; cctx |] in
+    Proofview.tclUNIT ans
+  end
+end
+
 let () = define2 "pattern_instantiate" constr constr begin fun ctx c ->
   let ctx = EConstr.Unsafe.to_constr ctx in
   let c = EConstr.Unsafe.to_constr c in
@@ -1146,6 +1171,7 @@ let () = add_expr_scope "move_location" q_move_location Tac2quote.of_move_locati
 let () = add_expr_scope "pose" q_pose Tac2quote.of_pose
 let () = add_expr_scope "assert" q_assert Tac2quote.of_assertion
 let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_matching
+let () = add_expr_scope "goal_matching" q_goal_matching Tac2quote.of_goal_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 f24c409ad7..04bf21f656 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -37,6 +37,7 @@ 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"
+let q_goal_matching = Pcoq.Gram.entry_create "tactic:q_goal_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"
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 7bd512651c..b2a2dd4846 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -77,6 +77,7 @@ 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
+val q_goal_matching : goal_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
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 19d4259b55..b0c56cdf45 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -272,6 +272,16 @@ let to_tuple = function
 | ValBlk (0, cl) -> cl
 | _ -> assert false
 
+let of_pair f g (x, y) = ValBlk (0, [|f x; g y|])
+let to_pair f g = function
+| ValBlk (0, [|x; y|]) -> (f x, g y)
+| _ -> assert false
+let pair r0 r1 = {
+  r_of = (fun p -> of_pair r0.r_of r1.r_of p);
+  r_to = (fun p -> to_pair r0.r_to r1.r_to p);
+  r_id = false;
+}
+
 let of_array f vl = ValBlk (0, Array.map f vl)
 let to_array f = function
 | ValBlk (0, vl) -> Array.map f vl
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index 9c3b512036..6d4867a453 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -109,6 +109,8 @@ val array : 'a repr -> 'a array repr
 val of_tuple : valexpr array -> valexpr
 val to_tuple : valexpr -> valexpr array
 
+val pair : 'a repr -> 'b repr -> ('a * 'b) repr
+
 val of_option : ('a -> valexpr) -> 'a option -> valexpr
 val to_option : (valexpr -> 'a) -> valexpr -> 'a option
 val option : 'a repr -> 'a option repr
diff --git a/src/tac2match.ml b/src/tac2match.ml
new file mode 100644
index 0000000000..7a22e91b6b
--- /dev/null
+++ b/src/tac2match.ml
@@ -0,0 +1,232 @@
+(************************************************************************)
+(*  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 Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
+
+type context = EConstr.t
+
+type result = {
+  subst : Pattern.patvar_map ;
+}
+
+type match_pattern =
+| MatchPattern of Pattern.constr_pattern
+| MatchContext of Pattern.constr_pattern
+
+(** TODO: handle definitions *)
+type match_context_hyps = match_pattern
+
+type match_rule = match_context_hyps list * match_pattern
+
+(** {6 Utilities} *)
+
+(** Tests whether the substitution [s] is empty. *)
+let is_empty_subst = Id.Map.is_empty
+
+(** {6 Non-linear patterns} *)
+
+
+(** The patterns of Ltac are not necessarily linear. Non-linear
+    pattern are partially handled by the {!Matching} module, however
+    goal patterns are not primitive to {!Matching}, hence we must deal
+    with non-linearity between hypotheses and conclusion. Subterms are
+    considered equal up to the equality implemented in
+    [equal_instances]. *)
+(* spiwack: it doesn't seem to be quite the same rule for non-linear
+   term patterns and non-linearity between hypotheses and/or
+   conclusion. Indeed, in [Matching], matching is made modulo
+   syntactic equality, and here we merge modulo conversion. It may be
+   a good idea to have an entry point of [Matching] with a partial
+   substitution as argument instead of merging substitution here. That
+   would ensure consistency. *)
+let equal_instances env sigma c1 c2 =
+  (* How to compare instances? Do we want the terms to be convertible?
+     unifiable? Do we want the universe levels to be relevant? 
+     (historically, conv_x is used) *)
+  Reductionops.is_conv env sigma c1 c2
+
+(** Merges two substitutions. Raises [Not_coherent_metas] when
+    encountering two instances of the same metavariable which are not
+    equal according to {!equal_instances}. *)
+exception Not_coherent_metas
+let verify_metas_coherence env sigma s1 s2 =
+  let merge id oc1 oc2 = match oc1, oc2 with
+    | None, None -> None
+    | None, Some c | Some c, None -> Some c
+    | Some c1, Some c2 ->
+        if equal_instances env sigma c1 c2 then Some c1
+        else raise Not_coherent_metas
+  in
+  Id.Map.merge merge s1 s2
+
+let matching_error =
+  CErrors.UserError (Some "tactic matching" , Pp.str "No matching clauses for match.")
+
+let imatching_error = (matching_error, Exninfo.null)
+
+(** A functor is introduced to share the environment and the
+    evar_map. They do not change and it would be a pity to introduce
+    closures everywhere just for the occasional calls to
+    {!equal_instances}. *)
+module type StaticEnvironment = sig
+  val env : Environ.env
+  val sigma : Evd.evar_map
+end
+module PatternMatching (E:StaticEnvironment) = struct
+
+
+  (** {6 The pattern-matching monad } *)
+
+
+  (** To focus on the algorithmic portion of pattern-matching, the
+      bookkeeping is relegated to a monad: the composition of the
+      bactracking monad of {!IStream.t} with a "writer" effect. *)
+  (* spiwack: as we don't benefit from the various stream optimisations
+     of Haskell, it may be costly to give the monad in direct style such as
+     here. We may want to use some continuation passing style. *)
+  type 'a tac = 'a Proofview.tactic
+  type 'a m = { stream : 'r. ('a -> result -> 'r tac) -> result -> 'r tac }
+
+  (** The empty substitution. *)
+  let empty_subst = Id.Map.empty
+
+  (** Composes two substitutions using {!verify_metas_coherence}. It
+      must be a monoid with neutral element {!empty_subst}. Raises
+      [Not_coherent_metas] when composition cannot be achieved. *)
+  let subst_prod s1 s2 =
+    if is_empty_subst s1 then s2
+    else if is_empty_subst s2 then s1
+    else verify_metas_coherence E.env E.sigma s1 s2
+
+  (** Merge two writers (and ignore the first value component). *)
+  let merge m1 m2 =
+    try Some {
+      subst = subst_prod m1.subst m2.subst;
+    }
+    with Not_coherent_metas -> None
+
+  (** Monadic [return]: returns a single success with empty substitutions. *)
+  let return (type a) (lhs:a) : a m =
+    { stream = fun k ctx -> k lhs ctx }
+
+  (** Monadic bind: each success of [x] is replaced by the successes
+      of [f x]. The substitutions of [x] and [f x] are composed,
+      dropping the apparent successes when the substitutions are not
+      coherent. *)
+  let (>>=) (type a) (type b) (m:a m) (f:a -> b m) : b m =
+    { stream = fun k ctx -> m.stream (fun x ctx -> (f x).stream k ctx) ctx }
+
+  (** A variant of [(>>=)] when the first argument returns [unit]. *)
+  let (<*>) (type a) (m:unit m) (y:a m) : a m =
+    { stream = fun k ctx -> m.stream (fun () ctx -> y.stream k ctx) ctx }
+
+  (** Failure of the pattern-matching monad: no success. *)
+  let fail (type a) : a m = { stream = fun _ _ -> Proofview.tclZERO matching_error }
+
+  let run (m : 'a m) =
+    let ctx = {
+      subst = empty_subst ;
+    } in
+    let eval x ctx = Proofview.tclUNIT (x, ctx) in
+    m.stream eval ctx
+
+  (** Chooses in a list, in the same order as the list *)
+  let rec pick (l:'a list) (e, info) : 'a m = match l with
+  | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e }
+  | x :: l ->
+    { stream = fun k ctx -> Proofview.tclOR (k x ctx) (fun e -> (pick l e).stream k ctx) }
+
+  let pick l = pick l imatching_error
+
+  let put_subst subst : unit m =
+    let s = { subst } in
+    { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s }
+
+  (** {6 Pattern-matching} *)
+
+  let pattern_match_term pat term = 
+    match pat with
+    | MatchPattern p ->
+        begin 
+          try
+            put_subst (Constr_matching.matches E.env E.sigma p term) <*>
+            return None
+          with Constr_matching.PatternMatchingFailure -> fail
+        end
+    | MatchContext p ->
+
+      let rec map s (e, info) =
+        { stream = fun k ctx -> match IStream.peek s with
+          | IStream.Nil -> Proofview.tclZERO ~info e
+          | IStream.Cons ({ Constr_matching.m_sub = (_, subst); m_ctx }, s) ->
+            let nctx = { subst } in
+            match merge ctx nctx with
+            | None -> (map s (e, info)).stream k ctx
+            | Some nctx -> Proofview.tclOR (k (Some m_ctx) nctx) (fun e -> (map s e).stream k ctx)
+        }
+      in
+      map (Constr_matching.match_appsubterm E.env E.sigma p term) imatching_error
+
+  let hyp_match_type pat hyps =
+    pick hyps >>= fun decl ->
+    let id = NamedDecl.get_id decl in
+    pattern_match_term pat (NamedDecl.get_type decl) >>= fun ctx ->
+    return (id, ctx)
+
+  let hyp_match_body_and_type bodypat typepat hyps =
+    pick hyps >>= function
+      | LocalDef (id,body,hyp) ->
+          pattern_match_term bodypat body >>= fun ctx_body ->
+          pattern_match_term typepat hyp >>= fun ctx_typ ->
+          return (id, ctx_body, ctx_typ)
+      | LocalAssum (id,hyp) -> fail
+
+  let hyp_match pat hyps =
+    match pat with
+    | typepat ->
+        hyp_match_type typepat hyps
+(*     | Def ((_,hypname),bodypat,typepat) -> *)
+(*         hyp_match_body_and_type hypname bodypat typepat hyps *)
+
+  (** [hyp_pattern_list_match pats hyps lhs], matches the list of
+      patterns [pats] against the hypotheses in [hyps], and eventually
+      returns [lhs]. *)
+  let rec hyp_pattern_list_match pats hyps accu =
+    match pats with
+    | pat::pats ->
+        hyp_match pat hyps >>= fun (matched_hyp, hyp_ctx) ->
+        let select_matched_hyp decl = Id.equal (NamedDecl.get_id decl) matched_hyp in
+        let hyps = CList.remove_first select_matched_hyp hyps in
+        hyp_pattern_list_match pats hyps ((matched_hyp, hyp_ctx) :: accu)
+    | [] -> return accu
+
+  let rule_match_goal hyps concl = function
+    | (hyppats,conclpat) ->
+        (* the rules are applied from the topmost one (in the concrete
+           syntax) to the bottommost. *)
+        let hyppats = List.rev hyppats in
+        pattern_match_term conclpat concl >>= fun ctx_concl ->
+        hyp_pattern_list_match hyppats hyps [] >>= fun hyps ->
+        return (hyps, ctx_concl)
+
+end
+
+let match_goal env sigma concl ~rev rule =
+  let open Proofview.Notations in
+  let hyps = EConstr.named_context env in
+  let hyps = if rev then List.rev hyps else hyps in
+  let module E = struct
+    let env = env
+    let sigma = sigma
+  end in
+  let module M = PatternMatching(E) in
+  M.run (M.rule_match_goal hyps concl rule) >>= fun ((hyps, ctx_concl), subst) ->
+  Proofview.tclUNIT (hyps, ctx_concl, subst.subst)
diff --git a/src/tac2match.mli b/src/tac2match.mli
new file mode 100644
index 0000000000..cf64542f40
--- /dev/null
+++ b/src/tac2match.mli
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*  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 EConstr
+
+(** This file extends Matching with the main logic for Ltac2 match goal. *)
+
+type context = EConstr.t
+
+type match_pattern =
+| MatchPattern of Pattern.constr_pattern
+| MatchContext of Pattern.constr_pattern
+
+(** TODO: handle definitions *)
+type match_context_hyps = match_pattern
+
+type match_rule = match_context_hyps list * match_pattern
+
+val match_goal:
+  Environ.env ->
+  Evd.evar_map ->
+  constr ->
+  rev:bool ->
+  match_rule ->
+    ((Id.t * context option) list * (** List of hypotheses matching: name + context *)
+    context option * (** Context for conclusion *)
+    Pattern.patvar_map (** Pattern variable substitution *)) Proofview.tactic
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index cb43a980de..229cece7c4 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -118,14 +118,27 @@ 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_pattern_r =
+| QConstrMatchPattern of Constrexpr.constr_expr
+| QConstrMatchContext of Id.t option * Constrexpr.constr_expr
 
-type constr_match_branch = constr_match_branch_r located
+type constr_match_pattern = constr_match_pattern_r located
+
+type constr_match_branch = (constr_match_pattern * raw_tacexpr) located
 
 type constr_matching = constr_match_branch list located
 
+type goal_match_pattern_r = {
+  q_goal_match_concl : constr_match_pattern;
+  q_goal_match_hyps : (Name.t located * constr_match_pattern) list;
+}
+
+type goal_match_pattern = goal_match_pattern_r located
+
+type goal_match_branch = (goal_match_pattern * raw_tacexpr) located
+
+type goal_matching = goal_match_branch list located
+
 type hintdb_r =
 | QHintAll
 | QHintDbs of Id.t located or_anti list
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index e967067161..9728c3af93 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -307,62 +307,126 @@ let of_hintdb (loc, hdb) = match hdb with
 | QHintAll -> of_option ?loc (fun l -> of_list (fun id -> of_anti of_ident id) l) None
 | QHintDbs ids -> of_option ?loc (fun l -> of_list (fun id -> of_anti of_ident id) l) (Some ids)
 
+let check_pattern_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)
+
 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
+  | Constrexpr.CPatVar id
+  | Constrexpr.CEvar (id, []) ->
+    let () = check_pattern_id ?loc:pat.CAst.loc id in
+    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)
+let abstract_vars loc vars tac =
+  let get_name = function Name id -> Some id | Anonymous -> None in
+  let def = try Some (List.find_map get_name vars) with Not_found -> None in
+  let na, tac = match def with
+  | None -> (Anonymous, tac)
+  | Some id0 ->
+      (** 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 build_bindings (n, accu) na = match na with
+      | Anonymous -> (n + 1, accu)
+      | Name _ ->
+        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 na, None, e) :: accu in
+        (n + 1, accu)
+      in
+      let (_, bnd) = List.fold_left build_bindings (0, []) vars in
+      let tac = Loc.tag ?loc @@ CTacLet (false, bnd, tac) in
+      (Name id0, 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
+  Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar na, None], tac)
+
+let extract_name ?loc oid = match oid with
+| None -> Anonymous
+| Some id ->
+  let () = check_pattern_id ?loc id in
+  Name id
+
+(** For every branch in the matching, generate a corresponding term of type
+    [(match_kind * pattern * (context -> constr array -> 'a))]
+    where the function binds the names from the pattern to the contents of the
+    constr array. *)
+let of_constr_matching (loc, m) =
+  let map (loc, ((ploc, pat), tac)) =
+    let (knd, pat, na) = match pat with
+    | QConstrMatchPattern pat ->
+      let knd = constructor ?loc (pattern_core "MatchPattern") [] in
+      (knd, pat, Anonymous)
+    | QConstrMatchContext (id, pat) ->
+      let na = extract_name ?loc id in
+      let knd = constructor ?loc (pattern_core "MatchContext") [] in
+      (knd, pat, na)
     in
+    let vars = pattern_vars pat in
+    (** Order of elements is crucial here! *)
+    let vars = Id.Set.elements vars in
+    let vars = List.map (fun id -> Name id) vars in
+    let e = abstract_vars loc vars tac 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]
+    let pat = inj_wit ?loc:ploc wit_pattern pat in
+    of_tuple [knd; pat; e]
   in
   of_list ?loc map m
 
+let of_pattern p =
+  inj_wit ?loc:p.CAst.loc wit_pattern p
+
+(** From the patterns and the body of the branch, generate:
+    - a goal pattern: (constr_match list * constr_match)
+    - a branch function (ident array -> context array -> constr array -> context -> 'a)
+*)
+let of_goal_matching (loc, gm) =
+  let mk_pat (loc, p) = match p with
+  | QConstrMatchPattern pat ->
+    let knd = constructor ?loc (pattern_core "MatchPattern") [] in
+    (Anonymous, pat, knd)
+  | QConstrMatchContext (id, pat) ->
+    let na = extract_name ?loc id in
+    let knd = constructor ?loc (pattern_core "MatchContext") [] in
+    (na, pat, knd)
+  in
+  let mk_gpat (loc, p) =
+    let concl_pat = p.q_goal_match_concl in
+    let hyps_pats = p.q_goal_match_hyps in
+    let (concl_ctx, concl_pat, concl_knd) = mk_pat concl_pat in
+    let vars = pattern_vars concl_pat in
+    let map accu (na, pat) =
+      let (ctx, pat, knd) = mk_pat pat in
+      let vars = pattern_vars pat in
+      (Id.Set.union vars accu, (na, ctx, pat, knd))
+    in
+    let (vars, hyps_pats) = List.fold_left_map map vars hyps_pats in
+    let map (_, _, pat, knd) = of_tuple [knd; of_pattern pat] in
+    let concl = of_tuple [concl_knd; of_pattern concl_pat] in
+    let r = of_tuple [of_list ?loc map hyps_pats; concl] in
+    let hyps = List.map (fun ((_, na), _, _, _) -> na) hyps_pats in
+    let map (_, na, _, _) = na in
+    let hctx = List.map map hyps_pats in
+    (** Order of elements is crucial here! *)
+    let vars = Id.Set.elements vars in
+    let subst = List.map (fun id -> Name id) vars in
+    (r, hyps, hctx, subst, concl_ctx)
+  in
+  let map (loc, (pat, tac)) =
+    let (pat, hyps, hctx, subst, cctx) = mk_gpat pat in
+    let tac = abstract_vars loc hyps tac in
+    let tac = abstract_vars loc hctx tac in
+    let tac = abstract_vars loc subst tac in
+    let tac = abstract_vars loc [cctx] tac in
+    of_tuple ?loc [pat; tac]
+  in
+  of_list ?loc map gm
+
 let of_move_location (loc, mv) = match mv with
 | QMoveAfter id -> std_constructor ?loc "MoveAfter" [of_anti of_ident id]
 | QMoveBefore id -> std_constructor ?loc "MoveBefore" [of_anti of_ident id]
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 148e6818dd..403d333f38 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -80,6 +80,8 @@ val of_assertion : assertion -> raw_tacexpr
 
 val of_constr_matching : constr_matching -> raw_tacexpr
 
+val of_goal_matching : goal_matching -> raw_tacexpr
+
 (** {5 Generic arguments} *)
 
 val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern) Arg.tag