Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

rewrite_db : a first attempt at using rewrite_strat for a quicker aut…

…orewrite

 rewrite_db fails if nothing has been rewritten, and it only performs
 *one* top-down pass. For the moment, use (repeat rewrite_db) for
 emulating more closely autorewrite.

 Btw, let's make Himsg.explain_ltac_call_trace robust wrt TacExtend
 with fun(ny) parts

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15522 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit 819029226c334030a540ed7570bc423c4463c6b4 1 parent 6a3ad48
letouzey authored
View
3  plugins/micromega/EnvRing.v
@@ -617,7 +617,8 @@ Qed.
(morph_opp CRmorph)
: Esimpl.
- Ltac Esimpl := autorewrite with Esimpl; rsimpl; simpl.
+ (* Quicker than autorewrite with Esimpl :-) *)
+ Ltac Esimpl := try rewrite_db Esimpl; rsimpl; simpl.
Lemma PaddC_ok c P l : (PaddC P c)@l == P@l + [c].
Proof.
View
3  plugins/setoid_ring/Ring_polynom.v
@@ -604,7 +604,8 @@ Section MakeRingPol.
(morph_opp CRmorph)
: Esimpl.
- Ltac Esimpl := autorewrite with Esimpl; rsimpl; simpl.
+ (* Quicker than autorewrite with Esimpl :-) *)
+ Ltac Esimpl := try rewrite_db Esimpl; rsimpl; simpl.
Lemma PaddC_ok c P l : (PaddC P c)@l == P@l + [c].
Proof.
View
7 tactics/rewrite.ml4
@@ -1528,9 +1528,16 @@ ARGUMENT EXTEND rewstrategy
| [ "fold" constr(c) ] -> [ StratFold c ]
END
+(* By default the strategy for "rewrite_db" is top-down *)
+
+let db_strat db = Strategies.td (Strategies.hints db)
+let cl_rewrite_clause_db db cl = cl_rewrite_clause_strat (db_strat db) cl
+
TACTIC EXTEND rewrite_strat
| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ cl_rewrite_clause_strat s (Some id) ]
| [ "rewrite_strat" rewstrategy(s) ] -> [ cl_rewrite_clause_strat s None ]
+| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ cl_rewrite_clause_db db (Some id) ]
+| [ "rewrite_db" preident(db) ] -> [ cl_rewrite_clause_db db None ]
END
let clsubstitute o c =
View
15 toplevel/himsg.ml
@@ -993,6 +993,11 @@ let explain_reduction_tactic_error = function
let explain_ltac_call_trace (nrep,last,trace,loc) =
let calls =
(nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace) in
+ let tacexpr_differ te te' =
+ (* NB: The following comparison may raise an exception
+ since a tacexpr may embed a functional part via a TacExtend *)
+ try te <> te' with Invalid_argument _ -> false
+ in
let pr_call (n,ck) =
(match ck with
| Proof_type.LtacNotationCall s -> quote (str s)
@@ -1004,11 +1009,11 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
(Pptactic.pr_glob_tactic (Global.env())
(Tacexpr.TacAtom (Loc.ghost,te)))
++ (match !otac with
- | Some te' when (Obj.magic te' <> te) ->
- strbrk " (expanded to " ++ quote
- (Pptactic.pr_tactic (Global.env())
- (Tacexpr.TacAtom (Loc.ghost,te')))
- ++ str ")"
+ | Some te' when tacexpr_differ (Obj.magic te') te ->
+ strbrk " (expanded to " ++ quote
+ (Pptactic.pr_tactic (Global.env())
+ (Tacexpr.TacAtom (Loc.ghost,te')))
+ ++ str ")"
| _ -> mt ())
| Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
let filter =
Please sign in to comment.
Something went wrong with that request. Please try again.