summaryrefslogtreecommitdiff
path: root/plugins/quote
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/quote')
-rw-r--r--plugins/quote/Quote.v5
-rw-r--r--plugins/quote/g_quote.ml46
-rw-r--r--plugins/quote/quote.ml28
3 files changed, 18 insertions, 21 deletions
diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v
index 55bb8bae..e2d8e67e 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-2010 *)
(* \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.
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 3c51223a..1f4ea97f 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-2010 *)
(* \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..fbb75420 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-2010 *)
(* \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) ->
@@ -243,7 +240,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 +370,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 +390,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 +419,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 +427,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 +475,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 =