aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/rewrite.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/rewrite.ml')
-rw-r--r--plugins/ltac/rewrite.ml98
1 files changed, 45 insertions, 53 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b84be4600c..966b11d0e7 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -17,7 +17,6 @@ open EConstr
open Vars
open Reduction
open Tacticals.New
-open Tacmach
open Tactics
open Pretype_errors
open Typeclasses
@@ -39,7 +38,7 @@ open Proofview.Notations
open Context.Named.Declaration
module NamedDecl = Context.Named.Declaration
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
(** Typeclass-based generalized rewriting. *)
@@ -56,22 +55,16 @@ let init_setoid () =
if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+let lazy_find_reference dir s =
+ let gr = lazy (Coqlib.coq_reference "generalized rewriting" dir s) in
+ fun () -> Lazy.force gr
-let try_find_global_reference dir s =
- let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in
- try Nametab.global_of_path sp
- with Not_found ->
- anomaly (str "Global reference " ++ str s ++ str " not found in generalized rewriting")
-
-let find_reference dir s =
- let gr = lazy (try_find_global_reference dir s) in
- fun () -> Lazy.force gr
+let find_reference dir s = Coqlib.coq_reference "generalized rewriting" dir s
type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
let find_global dir s =
- let gr = lazy (try_find_global_reference dir s) in
+ let gr = lazy (find_reference dir s) in
fun (evd,cstrs) ->
let sigma = Sigma.Unsafe.of_evar_map evd in
let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in
@@ -82,7 +75,7 @@ let find_global dir s =
(** Global constants. *)
-let coq_eq_ref = find_reference ["Init"; "Logic"] "eq"
+let coq_eq_ref = lazy_find_reference ["Init"; "Logic"] "eq"
let coq_eq = find_global ["Init"; "Logic"] "eq"
let coq_f_equal = find_global ["Init"; "Logic"] "f_equal"
let coq_all = find_global ["Init"; "Logic"] "all"
@@ -159,11 +152,11 @@ end) = struct
let forall_relation = find_global morphisms "forall_relation"
let pointwise_relation = find_global morphisms "pointwise_relation"
- let forall_relation_ref = find_reference morphisms "forall_relation"
- let pointwise_relation_ref = find_reference morphisms "pointwise_relation"
+ let forall_relation_ref = lazy_find_reference morphisms "forall_relation"
+ let pointwise_relation_ref = lazy_find_reference morphisms "pointwise_relation"
let respectful = find_global morphisms "respectful"
- let respectful_ref = find_reference morphisms "respectful"
+ let respectful_ref = lazy_find_reference morphisms "respectful"
let default_relation = find_global ["Classes"; "SetoidTactics"] "DefaultRelation"
@@ -175,8 +168,8 @@ end) = struct
let rewrite_relation_class = find_global relation_classes "RewriteRelation"
- let proper_class = lazy (class_info (try_find_global_reference morphisms "Proper"))
- let proper_proxy_class = lazy (class_info (try_find_global_reference morphisms "ProperProxy"))
+ let proper_class = lazy (class_info (find_reference morphisms "Proper"))
+ let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy"))
let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
@@ -242,7 +235,7 @@ end) = struct
let liftarg = mkLambda (na, ty, arg) in
let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
- else error "build_signature: no constraint can apply on a dependent argument"
+ else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument")
| _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products")
| _, [] ->
(match finalcstr with
@@ -479,7 +472,7 @@ type hypinfo = {
let get_symmetric_proof b =
if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof
-let error_no_relation () = error "Cannot find a relation to rewrite."
+let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.")
let rec decompose_app_rel env evd t =
(** Head normalize for compatibility with the old meta mechanism *)
@@ -532,7 +525,7 @@ let decompose_applied_relation env sigma (c,l) =
let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *)
match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with
| Some c -> c
- | None -> error "Cannot find an homogeneous relation to rewrite."
+ | None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.")
let rewrite_db = "rewrite"
@@ -838,7 +831,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
sigargs, r.rew_to :: typeargs')
| None ->
if not (Option.is_empty y) then
- error "Cannot rewrite inside dependent arguments of a function";
+ user_err Pp.(str "Cannot rewrite inside dependent arguments of a function");
x :: acc, x :: subst, evars, sigargs, x :: typeargs')
([], [], evars, sigargs, []) args args'
in
@@ -1426,7 +1419,7 @@ module Strategies =
let unfolded =
try Tacred.try_red_product env sigma c
with e when CErrors.noncritical e ->
- error "fold: the term is not unfoldable !"
+ user_err Pp.(str "fold: the term is not unfoldable !")
in
try
let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
@@ -1787,34 +1780,34 @@ let rec strategy_of_ast = function
(* By default the strategy for "rewrite_db" is top-down *)
-let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,Id.of_string s)),None),l)
+let mkappc s l = CAst.make @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l)
let declare_an_instance n s args =
- (((Loc.ghost,Name n),None), Explicit,
- CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, qualid_of_string s),None),
+ (((Loc.tag @@ Name n),None), Explicit,
+ CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@ qualid_of_string s),None),
args))
let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
let anew_instance global binders instance fields =
new_instance (Flags.is_universe_polymorphism ())
- binders instance (Some (true, CRecord (Loc.ghost,fields)))
+ binders instance (Some (true, CAst.make @@ CRecord (fields)))
~global ~generalize:false ~refine:false Hints.empty_hint_info
let declare_instance_refl global binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
in anew_instance global binders instance
- [(Ident (Loc.ghost,Id.of_string "reflexivity"),lemma)]
+ [(Ident (Loc.tag @@ Id.of_string "reflexivity"),lemma)]
let declare_instance_sym global binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
in anew_instance global binders instance
- [(Ident (Loc.ghost,Id.of_string "symmetry"),lemma)]
+ [(Ident (Loc.tag @@ Id.of_string "symmetry"),lemma)]
let declare_instance_trans global binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
in anew_instance global binders instance
- [(Ident (Loc.ghost,Id.of_string "transitivity"),lemma)]
+ [(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)]
let declare_relation ?(binders=[]) a aeq n refl symm trans =
init_setoid ();
@@ -1838,16 +1831,16 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
in ignore(
anew_instance global binders instance
- [(Ident (Loc.ghost,Id.of_string "PreOrder_Reflexive"), lemma1);
- (Ident (Loc.ghost,Id.of_string "PreOrder_Transitive"),lemma3)])
+ [(Ident (Loc.tag @@ Id.of_string "PreOrder_Reflexive"), lemma1);
+ (Ident (Loc.tag @@ Id.of_string "PreOrder_Transitive"),lemma3)])
| (None, Some lemma2, Some lemma3) ->
let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
in ignore(
anew_instance global binders instance
- [(Ident (Loc.ghost,Id.of_string "PER_Symmetric"), lemma2);
- (Ident (Loc.ghost,Id.of_string "PER_Transitive"),lemma3)])
+ [(Ident (Loc.tag @@ Id.of_string "PER_Symmetric"), lemma2);
+ (Ident (Loc.tag @@ Id.of_string "PER_Transitive"),lemma3)])
| (Some lemma1, Some lemma2, Some lemma3) ->
let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
@@ -1855,11 +1848,11 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
in ignore(
anew_instance global binders instance
- [(Ident (Loc.ghost,Id.of_string "Equivalence_Reflexive"), lemma1);
- (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2);
- (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)])
+ [(Ident (Loc.tag @@ Id.of_string "Equivalence_Reflexive"), lemma1);
+ (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), lemma2);
+ (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), lemma3)])
-let cHole = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None)
+let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None)
let proper_projection sigma r ty =
let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
@@ -1959,17 +1952,16 @@ let add_setoid global binders a aeq t n =
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
in ignore(
anew_instance global binders instance
- [(Ident (Loc.ghost,Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
- (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
- (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
+ [(Ident (Loc.tag @@ Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
+ (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
+ (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
let make_tactic name =
let open Tacexpr in
- let loc = Loc.ghost in
let tacpath = Libnames.qualid_of_string name in
- let tacname = Qualid (loc, tacpath) in
- TacArg (loc, TacCall (loc, tacname, []))
+ let tacname = Qualid (Loc.tag tacpath) in
+ TacArg (Loc.tag @@ TacCall (Loc.tag (tacname, [])))
let add_morphism_infer glob m n =
init_setoid ();
@@ -2012,14 +2004,14 @@ let add_morphism glob binders m s n =
let poly = Flags.is_universe_polymorphism () in
let instance_id = add_suffix n "_Proper" in
let instance =
- (((Loc.ghost,Name instance_id),None), Explicit,
- CAppExpl (Loc.ghost,
- (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
+ (((Loc.tag @@ Name instance_id),None), Explicit,
+ CAst.make @@ CAppExpl (
+ (None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
[cHole; s; m]))
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
ignore(new_instance ~global:glob poly binders instance
- (Some (true, CRecord (Loc.ghost,[])))
+ (Some (true, CAst.make @@ CRecord []))
~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
(** Bind to "rewrite" too *)
@@ -2197,7 +2189,8 @@ let setoid_transitivity c =
(transitivity_red true c)
let setoid_symmetry_in id =
- Proofview.V82.tactic (fun gl ->
+ let open Tacmach.New in
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = project gl in
let ctype = pf_unsafe_type_of gl (mkVar id) in
let binders,concl = decompose_prod_assum sigma ctype in
@@ -2205,17 +2198,16 @@ let setoid_symmetry_in id =
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
| x::y::z -> let l,res = split_last_two (y::z) in x::l, res
- | _ -> error "Cannot find an equivalence relation to rewrite."
+ | _ -> user_err Pp.(str "Cannot find an equivalence relation to rewrite.")
in
let others,(c1,c2) = split_last_two args in
let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in
let new_hyp' = mkApp (he, [| c2 ; c1 |]) in
let new_hyp = it_mkProd_or_LetIn new_hyp' binders in
- Proofview.V82.of_tactic
(tclTHENLAST
(Tactics.assert_after_replacing id new_hyp)
(tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
- gl)
+ end }
let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 21:38:54 +0000