Introducing the change tactic.

10 files changed, 99 insertions, 43 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index a979b1e9b8..557e2bcb9a 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -378,7 +378,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_conversion q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag
           q_destruction_arg q_reference q_with_bindings q_constr_matching
           q_goal_matching q_hintdb q_move_location q_pose q_assert;
   anti:
@@ -585,6 +585,16 @@ GEXTEND Gram
   q_induction_clause:
     [ [ cl = induction_clause -> cl ] ]
   ;
+  conversion:
+    [ [ c = Constr.constr ->
+        Loc.tag ~loc:!@loc @@ QConvert c
+      | c1 = Constr.constr; "with"; c2 = Constr.constr ->
+        Loc.tag ~loc:!@loc @@ QConvertWith (c1, c2)
+    ] ]
+  ;
+  q_conversion:
+    [ [ c = conversion -> c ] ]
+  ;
   orient:
     [ [ "->" -> Loc.tag ~loc:!@loc (Some true)
       | "<-" -> Loc.tag ~loc:!@loc (Some false)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 9ef88a7d56..ce53b781f5 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -1160,6 +1160,7 @@ let () = add_expr_scope "intropattern" q_intropattern Tac2quote.of_intro_pattern
 let () = add_expr_scope "intropatterns" q_intropatterns Tac2quote.of_intro_patterns
 let () = add_expr_scope "destruction_arg" q_destruction_arg Tac2quote.of_destruction_arg
 let () = add_expr_scope "induction_clause" q_induction_clause Tac2quote.of_induction_clause
+let () = add_expr_scope "conversion" q_conversion Tac2quote.of_conversion
 let () = add_expr_scope "rewriting" q_rewriting Tac2quote.of_rewriting
 let () = add_expr_scope "clause" q_clause Tac2quote.of_clause
 let () = add_expr_scope "hintdb" q_hintdb Tac2quote.of_hintdb
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index b803278929..3ac3d14ef3 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -30,6 +30,7 @@ let q_intropattern = Pcoq.Gram.entry_create "tactic:q_intropattern"
 let q_intropatterns = Pcoq.Gram.entry_create "tactic:q_intropatterns"
 let q_destruction_arg = Pcoq.Gram.entry_create "tactic:q_destruction_arg"
 let q_induction_clause = Pcoq.Gram.entry_create "tactic:q_induction_clause"
+let q_conversion = Pcoq.Gram.entry_create "tactic:q_conversion"
 let q_rewriting = Pcoq.Gram.entry_create "tactic:q_rewriting"
 let q_clause = Pcoq.Gram.entry_create "tactic:q_clause"
 let q_dispatch = Pcoq.Gram.entry_create "tactic:q_dispatch"
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index b2a2dd4846..a92e149a85 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -70,6 +70,7 @@ val q_intropattern : intro_pattern Pcoq.Gram.entry
 val q_intropatterns : intro_pattern list located Pcoq.Gram.entry
 val q_destruction_arg : destruction_arg Pcoq.Gram.entry
 val q_induction_clause : induction_clause Pcoq.Gram.entry
+val q_conversion : conversion Pcoq.Gram.entry
 val q_rewriting : rewriting Pcoq.Gram.entry
 val q_clause : clause Pcoq.Gram.entry
 val q_dispatch : dispatch Pcoq.Gram.entry
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 229cece7c4..ad52884ca6 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -84,6 +84,12 @@ type induction_clause_r = {
 
 type induction_clause = induction_clause_r located
 
+type conversion_r =
+| QConvert of Constrexpr.constr_expr
+| QConvertWith of Constrexpr.constr_expr * Constrexpr.constr_expr
+
+type conversion = conversion_r located
+
 type multi_r =
 | QPrecisely of int located
 | QUpTo of int located
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 1275c939c5..399c1199bd 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -208,6 +208,62 @@ let of_induction_clause (loc, cl) =
     std_proj "indcl_in", in_;
   ])
 
+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
+  | 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 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
+  Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar na, None], tac)
+
+let of_pattern p =
+  inj_wit ?loc:p.CAst.loc wit_pattern p
+
+let of_conversion (loc, c) = match c with
+| QConvert c ->
+  let pat = of_option ?loc of_pattern None in
+  let c = Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar Anonymous, None], of_constr c) in
+  of_tuple ?loc [pat; c]
+| QConvertWith (pat, c) ->
+  let vars = pattern_vars pat in
+  let pat = of_option ?loc of_pattern (Some pat) in
+  let c = of_constr c in
+  (** Order is critical here *)
+  let vars = List.map (fun id -> Name id) (Id.Set.elements vars) in
+  let c = abstract_vars loc vars c in
+  of_tuple [pat; c]
+
 let of_repeat (loc, r) = match r with
 | QPrecisely n -> std_constructor ?loc "Precisely" [of_int n]
 | QUpTo n -> std_constructor ?loc "UpTo" [of_int n]
@@ -307,45 +363,6 @@ 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
-  | 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 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
-  Loc.tag ?loc @@ CTacFun ([Loc.tag ?loc @@ CPatVar na, None], tac)
-
 let extract_name ?loc oid = match oid with
 | None -> Anonymous
 | Some id ->
@@ -378,9 +395,6 @@ let of_constr_matching (loc, m) =
   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)
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 403d333f38..3f6c9a55e5 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -51,6 +51,8 @@ val of_destruction_arg : destruction_arg -> raw_tacexpr
 
 val of_induction_clause : induction_clause -> raw_tacexpr
 
+val of_conversion : conversion -> raw_tacexpr
+
 val of_rewriting : rewriting -> raw_tacexpr
 
 val of_occurrences : occurrences -> raw_tacexpr
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 99fa0370e1..60b6e70d58 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -467,6 +467,13 @@ let () = define_red2 "eval_native" begin fun where c ->
   Tac2tactics.eval_native where c
 end
 
+let () = define_prim3 "tac_change" begin fun pat c cl ->
+  let pat = Value.to_option (fun p -> Value.to_pattern p) pat in
+  let c = Value.to_fun1 (array constr) constr c in
+  let cl = to_clause cl in
+  Tac2tactics.change pat c cl
+end
+
 let () = define_prim4 "tac_rewrite" begin fun ev rw cl by ->
   let ev = Value.to_bool ev in
   let rw = Value.to_list to_rewriting rw in
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index c68fdf9a7a..5a5b259ee7 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -150,6 +150,18 @@ let split_with_bindings ev bnd =
   let bnd = mk_bindings bnd in
   Tactics.split_with_bindings ev [bnd]
 
+let change pat c cl =
+  let open Tac2ffi in
+  Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let c subst sigma =
+    let subst = Array.map_of_list snd (Id.Map.bindings subst) in
+    delayed_of_tactic (Tac2ffi.app_fun1 c (array constr) constr subst) env sigma
+  in
+  let cl = mk_clause cl in
+  Tactics.change pat c cl
+  end
+
 let rewrite ev rw cl by =
   let map_rw (orient, repeat, c) =
     let c = c >>= fun c -> return (mk_with_bindings c) in
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 3d64e7ec8c..7a4624ba2c 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -38,6 +38,8 @@ val left_with_bindings  : evars_flag -> bindings -> unit tactic
 val right_with_bindings : evars_flag -> bindings -> unit tactic
 val split_with_bindings : evars_flag -> bindings -> unit tactic
 
+val change : Pattern.constr_pattern option -> (constr array, constr) Tac2ffi.fun1 -> clause -> unit tactic
+
 val rewrite :
   evars_flag -> rewriting list -> clause -> unit tactic option -> unit tactic