summaryrefslogtreecommitdiff
path: root/plugins/quote
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/quote')
-rw-r--r--plugins/quote/Quote.v7
-rw-r--r--plugins/quote/g_quote.ml46
-rw-r--r--plugins/quote/quote.ml33
3 files changed, 23 insertions, 23 deletions
diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v
index 55bb8bae..2206aedf 100644
--- a/plugins/quote/Quote.v
+++ b/plugins/quote/Quote.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Quote.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
Declare ML Module "quote_plugin".
(***********************************************************************
@@ -28,7 +26,6 @@ Declare ML Module "quote_plugin".
***********************************************************************)
Set Implicit Arguments.
-Unset Boxed Definitions.
Section variables_map.
@@ -70,7 +67,7 @@ Fixpoint index_lt (n m:index) {struct m} : bool :=
end.
Lemma index_eq_prop : forall n m:index, index_eq n m = true -> n = m.
- simple induction n; simple induction m; simpl in |- *; intros.
+ simple induction n; simple induction m; simpl; intros.
rewrite (H i0 H1); reflexivity.
discriminate.
discriminate.
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 3c51223a..09b780fd 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,14 +8,12 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_quote.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Util
open Tacexpr
open Quote
let make_cont k x =
- let k = TacDynamic(dummy_loc, Tacinterp.tactic_in (fun _ -> fst k)) in
+ let k = TacDynamic(dummy_loc, Tacinterp.tactic_in (fun _ -> k)) in
let x = TacDynamic(dummy_loc, Pretyping.constr_in x) in
let tac = <:tactic<let cont := $k in cont $x>> in
Tacinterp.interp tac
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index baba7e1b..216a719d 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: quote.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(* The `Quote' tactic *)
(* The basic idea is to automatize the inversion of interpetation functions
@@ -111,7 +109,6 @@ open Pattern
open Matching
open Tacmach
open Tactics
-open Proof_trees
open Tacexpr
(*i*)
@@ -169,7 +166,7 @@ exchange ?1 and ?2 in the example above)
module ConstrSet = Set.Make(
struct
type t = constr
- let compare = (Pervasives.compare : t->t->int)
+ let compare = constr_ord
end)
type inversion_scheme = {
@@ -211,7 +208,7 @@ let compute_lhs typ i nargsi =
let compute_rhs bodyi index_of_f =
let rec aux c =
match kind_of_term c with
- | App (j, args) when j = mkRel (index_of_f) (* recursive call *) ->
+ | App (j, args) when isRel j && destRel j = index_of_f (* recursive call *) ->
let i = destRel (array_last args) in
PMeta (Some (coerce_meta_in i))
| App (f,args) ->
@@ -224,7 +221,10 @@ let compute_rhs bodyi index_of_f =
(*s Now the function [compute_ivs] itself *)
let compute_ivs gl f cs =
- let cst = try destConst f with _ -> i_can't_do_that () in
+ let cst =
+ try destConst f
+ with e when Errors.noncritical e -> i_can't_do_that ()
+ in
let body = Environ.constant_value (Global.env()) cst in
match decomp_term body with
| Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
@@ -243,7 +243,7 @@ let compute_ivs gl f cs =
(* REL nargsi+1 to REL nargsi + nargs3 are arguments of f *)
(* REL 1 to REL nargsi are argsi (reverse order) *)
(* First we test if the RHS is the RHS for constants *)
- if bodyi = mkRel 1 then
+ if isRel bodyi && destRel bodyi = 1 then
c_lhs := Some (compute_lhs (snd (List.hd args3))
i nargsi)
(* Then we test if the RHS is the RHS for variables *)
@@ -373,13 +373,19 @@ let rec subterm gl (t : constr) (t' : constr) =
let rec sort_subterm gl l =
let rec insert c = function
| [] -> [c]
- | (h::t as l) when c = h -> l (* Avoid doing the same work twice *)
+ | (h::t as l) when eq_constr c h -> l (* Avoid doing the same work twice *)
| h::t -> if subterm gl c h then c::h::t else h::(insert c t)
in
match l with
| [] -> []
| h::t -> insert h (sort_subterm gl t)
+module Constrhash = Hashtbl.Make
+ (struct type t = constr
+ let equal = eq_constr
+ let hash = hash_constr
+ end)
+
(*s Now we are able to do the inversion itself.
We destructurate the term and use an imperative hashtable
to store leafs that are already encountered.
@@ -387,10 +393,9 @@ let rec sort_subterm gl l =
[ivs : inversion_scheme]\\
[lc: constr list]\\
[gl: goal sigma]\\ *)
-
let quote_terms ivs lc gl =
Coqlib.check_required_library ["Coq";"quote";"Quote"];
- let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+ let varhash = (Constrhash.create 17 : constr Constrhash.t) in
let varlist = ref ([] : constr list) in (* list of variables *)
let counter = ref 1 in (* number of variables created + 1 *)
let rec aux c =
@@ -417,7 +422,7 @@ let quote_terms ivs lc gl =
Termops.subst_meta [1, c] c_lhs
| _ ->
begin
- try Hashtbl.find varhash c
+ try Constrhash.find varhash c
with Not_found ->
let newvar =
Termops.subst_meta [1, (path_of_int !counter)]
@@ -425,7 +430,7 @@ let quote_terms ivs lc gl =
begin
incr counter;
varlist := c :: !varlist;
- Hashtbl.add varhash c newvar;
+ Constrhash.add varhash c newvar;
newvar
end
end
@@ -473,7 +478,7 @@ Just testing ...
#use "include.ml";;
open Quote;;
-let r = raw_constr_of_string;;
+let r = glob_constr_of_string;;
let ivs = {
normal_lhs_rhs =
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-29 04:49:38 +0000