Adding necessary primitives to do pattern-matching over constr.

8 files changed, 122 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 2561b7b6ec..e3ad3987bd 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -28,5 +28,6 @@ theories/Array.v
 theories/Control.v
 theories/Message.v
 theories/Constr.v
+theories/Pattern.v
 theories/Std.v
 theories/Ltac2.v
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index cd227a78f1..d7d376f88a 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -27,6 +27,7 @@ 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 pattern_of_qualid loc id =
   if Tac2env.is_constructor (snd id) then CPatRef (loc, RelId id, [])
@@ -109,6 +110,7 @@ GEXTEND Gram
       | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_constr !@loc c
       | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_open_constr !@loc c
       | IDENT "ident"; ":"; "("; c = Prim.ident; ")" -> inj_ident !@loc c
+      | IDENT "pattern"; ":"; "("; c = Constr.lconstr_pattern; ")" -> inj_pattern !@loc c
     ] ]
   ;
   let_clause:
diff --git a/src/tac2core.ml b/src/tac2core.ml
index f29cc8c89e..ab1eaec9d9 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -26,6 +26,7 @@ let val_tag t = match val_tag t with
 
 let val_constr = val_tag (topwit Stdarg.wit_constr)
 let val_ident = val_tag (topwit Stdarg.wit_ident)
+let val_pattern = Val.create "ltac2:pattern"
 let val_pp = Val.create "ltac2:pp"
 let val_sort = Val.create "ltac2:sort"
 let val_cast = Val.create "ltac2:cast"
@@ -51,6 +52,7 @@ let t_array = coq_core "array"
 let t_unit = coq_core "unit"
 let t_list = coq_core "list"
 let t_constr = coq_core "constr"
+let t_pattern = coq_core "pattern"
 let t_ident = coq_core "ident"
 let t_option = coq_core "option"
 
@@ -121,6 +123,9 @@ let to_constr c = to_ext val_constr c
 let of_ident c = of_ext val_ident c
 let to_ident c = to_ext val_ident c
 
+let of_pattern c = of_ext val_pattern c
+let to_pattern c = to_ext val_pattern c
+
 (** FIXME: handle backtrace in Ltac2 exceptions *)
 let of_exn c = match fst c with
 | LtacError (kn, c) -> ValOpn (kn, c)
@@ -178,6 +183,9 @@ let err_outofbounds =
 let err_notfound =
   LtacError (coq_core "Not_found", [||])
 
+let err_matchfailure =
+  LtacError (coq_core "Match_failure", [||])
+
 (** Helper functions *)
 
 let thaw f = interp_app f [v_unit]
@@ -464,6 +472,54 @@ let prm_constr_kind : ml_tactic = function
   end
 | _ -> assert false
 
+(** Patterns *)
+
+let prm_pattern_matches : ml_tactic = function
+| [pat; c] ->
+  let pat = Value.to_pattern pat in
+  let c = Value.to_constr c in
+  pf_apply begin fun env sigma ->
+    let ans =
+      try Some (Constr_matching.matches env sigma pat c)
+      with Constr_matching.PatternMatchingFailure -> None
+    in
+    begin match ans with
+    | None -> Proofview.tclZERO err_matchfailure
+    | Some ans ->
+      let ans = Id.Map.bindings ans in
+      let of_pair (id, c) = Value.of_tuple [| Value.of_ident id; Value.of_constr c |] in
+      return (Value.of_list (List.map of_pair ans))
+    end
+  end
+| _ -> assert false
+
+let prm_pattern_matches_subterm : ml_tactic = function
+| [pat; c] ->
+  let pat = Value.to_pattern pat in
+  let c = Value.to_constr c in
+  let open Constr_matching in
+  let rec of_ans s = match IStream.peek s with
+  | IStream.Nil -> Proofview.tclZERO err_matchfailure
+  | IStream.Cons ({ m_sub = (_, sub); m_ctx }, s) ->
+    let ans = Id.Map.bindings sub in
+    let of_pair (id, c) = Value.of_tuple [| Value.of_ident id; Value.of_constr c |] in
+    let ans = Value.of_tuple [| Value.of_constr m_ctx; Value.of_list (List.map of_pair ans) |] in
+    Proofview.tclOR (return ans) (fun _ -> of_ans s)
+  in
+  pf_apply begin fun env sigma ->
+    let ans = Constr_matching.match_appsubterm env sigma pat c in
+    of_ans ans
+  end
+| _ -> assert false
+
+let prm_pattern_instantiate : ml_tactic = function
+| [ctx; c] ->
+  let ctx = EConstr.Unsafe.to_constr (Value.to_constr ctx) in
+  let c = EConstr.Unsafe.to_constr (Value.to_constr c) in
+  let ans = Termops.subst_meta [Constr_matching.special_meta, c] ctx in
+  return (Value.of_constr (EConstr.of_constr ans))
+| _ -> assert false
+
 (** Error *)
 
 let prm_throw : ml_tactic = function
@@ -642,6 +698,10 @@ let () = Tac2env.define_primitive (pname "constr_type") prm_constr_type
 let () = Tac2env.define_primitive (pname "constr_equal") prm_constr_equal
 let () = Tac2env.define_primitive (pname "constr_kind") prm_constr_kind
 
+let () = Tac2env.define_primitive (pname "pattern_matches") prm_pattern_matches
+let () = Tac2env.define_primitive (pname "pattern_matches_subterm") prm_pattern_matches_subterm
+let () = Tac2env.define_primitive (pname "pattern_instantiate") prm_pattern_instantiate
+
 let () = Tac2env.define_primitive (pname "int_equal") prm_int_equal
 let () = Tac2env.define_primitive (pname "int_compare") prm_int_compare
 let () = Tac2env.define_primitive (pname "int_neg") prm_int_neg
@@ -739,6 +799,14 @@ let () =
   define_ml_object Stdarg.wit_ident obj
 
 let () =
+  let interp _ c = return (Val.Dyn (val_pattern, c)) in
+  let obj = {
+    ml_type = t_pattern;
+    ml_interp = interp;
+  } in
+  define_ml_object Tac2env.wit_pattern obj
+
+let () =
   let interp ist env sigma concl tac =
     let fold id (Val.Dyn (tag, v)) (accu : environment) : environment =
       match Val.eq tag val_valexpr with
@@ -752,6 +820,19 @@ let () =
   in
   Pretyping.register_constr_interp0 wit_ltac2 interp
 
+(** Patterns *)
+
+let () =
+  let intern ist c =
+    let _, pat = Constrintern.intern_constr_pattern ist.Genintern.genv ~as_type:false c in
+    ist, pat
+  in
+  Genintern.register_intern0 wit_pattern intern
+
+let () =
+  let subst s c = Patternops.subst_pattern s c in
+  Genintern.register_subst0 wit_pattern subst
+
 (** Built-in notation scopes *)
 
 let add_scope s f =
diff --git a/src/tac2env.ml b/src/tac2env.ml
index 6e47e78a9d..2094898ced 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -242,6 +242,7 @@ let coq_prefix =
 (** Generic arguments *)
 
 let wit_ltac2 = Genarg.make0 "ltac2"
+let wit_pattern = Genarg.make0 "ltac2:pattern"
 
 let is_constructor qid =
   let (_, id) = repr_qualid qid in
diff --git a/src/tac2env.mli b/src/tac2env.mli
index 8ab9656cb9..e26109b691 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -110,6 +110,8 @@ val coq_prefix : ModPath.t
 
 val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type
 
+val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern, Pattern.constr_pattern) genarg_type
+
 (** {5 Helper functions} *)
 
 val is_constructor : qualid -> bool
diff --git a/theories/Init.v b/theories/Init.v
index c0a73576d3..803e48e352 100644
--- a/theories/Init.v
+++ b/theories/Init.v
@@ -27,6 +27,7 @@ Ltac2 Type constant.
 Ltac2 Type inductive.
 Ltac2 Type constructor.
 Ltac2 Type projection.
+Ltac2 Type pattern.
 Ltac2 Type constr.
 
 Ltac2 Type message.
@@ -56,3 +57,6 @@ Ltac2 Type exn ::= [ Not_focussed ].
 
 Ltac2 Type exn ::= [ Not_found ].
 (** Used when something is missing. *)
+
+Ltac2 Type exn ::= [ Match_failure ].
+(** Used to signal a pattern didn't match a term. *)
diff --git a/theories/Ltac2.v b/theories/Ltac2.v
index 0d6c8f232a..9aaee850cd 100644
--- a/theories/Ltac2.v
+++ b/theories/Ltac2.v
@@ -15,4 +15,5 @@ Require Ltac2.Array.
 Require Ltac2.Message.
 Require Ltac2.Constr.
 Require Ltac2.Control.
+Require Ltac2.Pattern.
 Require Ltac2.Std.
diff --git a/theories/Pattern.v b/theories/Pattern.v
new file mode 100644
index 0000000000..c2ba4162e8
--- /dev/null
+++ b/theories/Pattern.v
@@ -0,0 +1,30 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+
+Ltac2 Type t := pattern.
+
+Ltac2 Type context.
+
+Ltac2 @ external matches : t -> constr -> (ident * constr) list :=
+  "ltac2" "pattern_matches".
+(** If the term matches the pattern, returns the bound variables. If it doesn't,
+    fail with [Match_failure]. Panics if not focussed. *)
+
+Ltac2 @ external matches_subterm : t -> constr -> context * ((ident * constr) list) :=
+  "ltac2" "pattern_matches_subterm".
+(** Returns a stream of results corresponding to all of the subterms of the term
+    that matches the pattern as in [matches]. The stream is encoded as a
+    backtracking value whose last exception is [Match_failure]. The additional
+    value compared to [matches] is the context of the match, to be filled with
+    the instantiate function. *)
+
+Ltac2 @ external instantiate : context -> constr -> constr :=
+  "ltac2" "pattern_instantiate".
+(** Fill the hole of a context with the given term. *)