diff options
| -rw-r--r-- | .github/CODEOWNERS | 2 | ||||
| -rw-r--r-- | CHANGES | 10 | ||||
| -rw-r--r-- | CREDITS | 2 | ||||
| -rw-r--r-- | META.coq.in | 14 | ||||
| -rw-r--r-- | Makefile.common | 5 | ||||
| -rw-r--r-- | Makefile.dev | 1 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/detailed-tactic-examples.rst | 212 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 20 | ||||
| -rw-r--r-- | plugins/quote/Quote.v | 86 | ||||
| -rw-r--r-- | plugins/quote/g_quote.mlg | 46 | ||||
| -rw-r--r-- | plugins/quote/quote.ml | 540 | ||||
| -rw-r--r-- | plugins/quote/quote_plugin.mlpack | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring_base.v | 1 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring_tac.v | 1 | ||||
| -rw-r--r-- | test-suite/output/Quote.v | 36 |
15 files changed, 14 insertions, 964 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index d9136ee24b..bac6ccd823 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -168,8 +168,6 @@ /plugins/syntax/ @ppedrot # Secondary maintainer @maximedenes -/plugins/quote/ @herbelin - /plugins/rtauto/ @PierreCorbineau # Secondary maintainer @herbelin @@ -1,3 +1,13 @@ +Changes beyond 8.9 +================== + +Plugins + +- The quote plugin (https://coq.inria.fr/distrib/V8.8.1/refman/proof-engine/detailed-tactic-examples.html#quote) + was removed. If some users are interested in maintaining this plugin + externally, the Coq development team can provide assistance for extracting + the plugin and setting up a new repository. + Changes from 8.8.2 to 8.9+beta1 =============================== @@ -50,8 +50,6 @@ plugins/nsatz developed by Loïc Pottier (INRIA-Marelle, 2009-2011) plugins/omega developed by Pierre Crégut (France Telecom R&D, 1996) -plugins/quote - developed by Patrick Loiseleur (LRI, 1997-1999) plugins/romega developed by Pierre Crégut (France Telecom R&D, 2001-2004) plugins/rtauto diff --git a/META.coq.in b/META.coq.in index e942267ad7..a7bf08ec49 100644 --- a/META.coq.in +++ b/META.coq.in @@ -325,24 +325,12 @@ package "plugins" ( archive(native) = "micromega_plugin.cmx" ) - package "quote" ( - - description = "Coq quote plugin" - version = "8.10" - - requires = "coq.plugins.ltac" - directory = "quote" - - archive(byte) = "quote_plugin.cmo" - archive(native) = "quote_plugin.cmx" - ) - package "newring" ( description = "Coq newring plugin" version = "8.10" - requires = "coq.plugins.quote" + requires = "" directory = "setoid_ring" archive(byte) = "newring_plugin.cmo" diff --git a/Makefile.common b/Makefile.common index 09457ced7b..69dea1d284 100644 --- a/Makefile.common +++ b/Makefile.common @@ -95,7 +95,7 @@ CORESRCDIRS:=\ tactics vernac stm toplevel PLUGINDIRS:=\ - omega romega micromega quote \ + omega romega micromega \ setoid_ring extraction \ cc funind firstorder derive \ rtauto nsatz syntax btauto \ @@ -131,7 +131,6 @@ GRAMMARCMA:=grammar/grammar.cma OMEGACMO:=plugins/omega/omega_plugin.cmo ROMEGACMO:=plugins/romega/romega_plugin.cmo MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo -QUOTECMO:=plugins/quote/quote_plugin.cmo RINGCMO:=plugins/setoid_ring/newring_plugin.cmo NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo @@ -152,7 +151,7 @@ SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo SSRCMO:=plugins/ssr/ssreflect_plugin.cmo PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \ - $(QUOTECMO) $(RINGCMO) \ + $(RINGCMO) \ $(EXTRACTIONCMO) \ $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \ diff --git a/Makefile.dev b/Makefile.dev index 7fc1076a8f..2a7e61126a 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -171,7 +171,6 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \ OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO)) ROMEGAVO:=$(filter plugins/romega/%, $(PLUGINSVO)) MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO)) -QUOTEVO:=$(filter plugins/quote/%, $(PLUGINSVO)) RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO)) NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO)) FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO)) diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 72dd79d930..bd16b70d02 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -417,218 +417,8 @@ the optional tactic of the ``Hint Rewrite`` command. Qed. -.. _quote: - -quote ------ - -The tactic ``quote`` allows using Barendregt’s so-called 2-level approach -without writing any ML code. Suppose you have a language ``L`` of -'abstract terms' and a type ``A`` of 'concrete terms' and a function ``f : L -> A``. -If ``L`` is a simple inductive datatype and ``f`` a simple fixpoint, -``quote f`` will replace the head of current goal by a convertible term of -the form ``(f t)``. ``L`` must have a constructor of type: ``A -> L``. - -Here is an example: - -.. coqtop:: in reset - - Require Import Quote. - -.. coqtop:: all - - Parameters A B C : Prop. - -.. coqtop:: all - - Inductive formula : Type := - | f_and : formula -> formula -> formula (* binary constructor *) - | f_or : formula -> formula -> formula - | f_not : formula -> formula (* unary constructor *) - | f_true : formula (* 0-ary constructor *) - | f_const : Prop -> formula (* constructor for constants *). - -.. coqtop:: all - - Fixpoint interp_f (f:formula) : Prop := - match f with - | f_and f1 f2 => interp_f f1 /\ interp_f f2 - | f_or f1 f2 => interp_f f1 \/ interp_f f2 - | f_not f1 => ~ interp_f f1 - | f_true => True - | f_const c => c - end. - -.. coqtop:: all - - Goal A /\ (A \/ True) /\ ~ B /\ (A <-> A). - -.. coqtop:: all - - quote interp_f. - -The algorithm to perform this inversion is: try to match the term with -right-hand sides expression of ``f``. If there is a match, apply the -corresponding left-hand side and call yourself recursively on sub- -terms. If there is no match, we are at a leaf: return the -corresponding constructor (here ``f_const``) applied to the term. - -When ``quote`` is not able to perform inversion properly, it will error out with -:exn:`quote: not a simple fixpoint`. - - -Introducing variables map -~~~~~~~~~~~~~~~~~~~~~~~~~ - -The normal use of quote is to make proofs by reflection: one defines a -function ``simplify : formula -> formula`` and proves a theorem -``simplify_ok: (f:formula)(interp_f (simplify f)) -> (interp_f f)``. Then, -one can simplify formulas by doing: - -.. coqtop:: in - - quote interp_f. - apply simplify_ok. - compute. - -But there is a problem with leafs: in the example above one cannot -write a function that implements, for example, the logical -simplifications :math:`A \wedge A \rightarrow A` or :math:`A \wedge -\lnot A \rightarrow \mathrm{False}`. This is because ``Prop`` is -impredicative. - -It is better to use that type of formulas: - -.. coqtop:: in reset - - Require Import Quote. - -.. coqtop:: in - - Parameters A B C : Prop. - -.. coqtop:: all - - Inductive formula : Set := - | f_and : formula -> formula -> formula - | f_or : formula -> formula -> formula - | f_not : formula -> formula - | f_true : formula - | f_atom : index -> formula. - -``index`` is defined in module ``Quote``. Equality on that type is -decidable so we are able to simplify :math:`A \wedge A` into :math:`A` -at the abstract level. - -When there are variables, there are bindings, and ``quote`` also -provides a type ``(varmap A)`` of bindings from index to any set -``A``, and a function ``varmap_find`` to search in such maps. The -interpretation function also has another argument, a variables map: - -.. coqtop:: all - - Fixpoint interp_f (vm:varmap Prop) (f:formula) {struct f} : Prop := - match f with - | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2 - | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2 - | f_not f1 => ~ interp_f vm f1 - | f_true => True - | f_atom i => varmap_find True i vm - end. - -``quote`` handles this second case properly: - -.. coqtop:: all - - Goal A /\ (B \/ A) /\ (A \/ ~ B). - -.. coqtop:: all - - quote interp_f. - -It builds ``vm`` and ``t`` such that ``(f vm t)`` is convertible with the -conclusion of current goal. - - -Combining variables and constants -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -One can have both variables and constants in abstracts terms; for -example, this is the case for the :tacn:`ring` tactic. Then one must provide to -``quote`` a list of *constructors of constants*. For example, if the list -is ``[O S]`` then closed natural numbers will be considered as constants -and other terms as variables. - -.. coqtop:: in reset - - Require Import Quote. - -.. coqtop:: in - - Parameters A B C : Prop. - -.. coqtop:: in - - Inductive formula : Type := - | f_and : formula -> formula -> formula - | f_or : formula -> formula -> formula - | f_not : formula -> formula - | f_true : formula - | f_const : Prop -> formula (* constructor for constants *) - | f_atom : index -> formula. - -.. coqtop:: in - - Fixpoint interp_f (vm:varmap Prop) (f:formula) {struct f} : Prop := - match f with - | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2 - | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2 - | f_not f1 => ~ interp_f vm f1 - | f_true => True - | f_const c => c - | f_atom i => varmap_find True i vm - end. - -.. coqtop:: in - - Goal A /\ (A \/ True) /\ ~ B /\ (C <-> C). - -.. coqtop:: all - - quote interp_f [ A B ]. - - -.. coqtop:: all - - Undo. - -.. coqtop:: all - - quote interp_f [ B C iff ]. - -.. warning:: - Since functional inversion is undecidable in the general case, - don’t expect miracles from it! - -.. tacv:: quote @ident in @term using @tactic - - ``tactic`` must be a functional tactic (starting with ``fun x =>``) and - will be called with the quoted version of term according to ``ident``. - -.. tacv:: quote @ident [{+ @ident}] in @term using @tactic - - Same as above, but will use the additional ``ident`` list to chose - which subterms are constants (see above). - -.. seealso:: - Comments from the source file ``plugins/quote/quote.ml`` - -.. seealso:: - The :tacn:`ring` tactic. - - Using the tactic language ---------------------------- +------------------------- About the cardinality of the set of natural numbers diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 62a482096c..fb121c82ec 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4217,26 +4217,6 @@ available after a ``Require Import FunInd``. functional inversion, this variant allows choosing which :n:`@qualid` is inverted. -.. tacn:: quote @ident - :name: quote - -This kind of inversion has nothing to do with the tactic :tacn:`inversion` -above. This tactic does :g:`change (@ident t)`, where `t` is a term built in -order to ensure the convertibility. In other words, it does inversion of the -function :n:`@ident`. This function must be a fixpoint on a simple recursive -datatype: see :ref:`quote` for the full details. - - -.. exn:: quote: not a simple fixpoint. - - Happens when quote is not able to perform inversion properly. - - -.. tacv:: quote @ident {* @ident} - - All terms that are built only with :n:`{* @ident}` will be considered by quote - as constants rather than variables. - Classical tactics ----------------- diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v deleted file mode 100644 index 2d3d9170c1..0000000000 --- a/plugins/quote/Quote.v +++ /dev/null @@ -1,86 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -Declare ML Module "quote_plugin". - -(*********************************************************************** - The "abstract" type index is defined to represent variables. - - index : Set - index_eq : index -> bool - index_eq_prop: (n,m:index)(index_eq n m)=true -> n=m - index_lt : index -> bool - varmap : Type -> Type. - varmap_find : (A:Type)A -> index -> (varmap A) -> A. - - The first arg. of varmap_find is the default value to take - if the object is not found in the varmap. - - index_lt defines a total well-founded order, but we don't prove that. - -***********************************************************************) - -Set Implicit Arguments. - -Section variables_map. - -Variable A : Type. - -Inductive varmap : Type := - | Empty_vm : varmap - | Node_vm : A -> varmap -> varmap -> varmap. - -Inductive index : Set := - | Left_idx : index -> index - | Right_idx : index -> index - | End_idx : index. - -Fixpoint varmap_find (default_value:A) (i:index) (v:varmap) {struct v} : A := - match i, v with - | End_idx, Node_vm x _ _ => x - | Right_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v2 - | Left_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v1 - | _, _ => default_value - end. - -Fixpoint index_eq (n m:index) {struct m} : bool := - match n, m with - | End_idx, End_idx => true - | Left_idx n', Left_idx m' => index_eq n' m' - | Right_idx n', Right_idx m' => index_eq n' m' - | _, _ => false - end. - -Fixpoint index_lt (n m:index) {struct m} : bool := - match n, m with - | End_idx, Left_idx _ => true - | End_idx, Right_idx _ => true - | Left_idx n', Right_idx m' => true - | Right_idx n', Right_idx m' => index_lt n' m' - | Left_idx n', Left_idx m' => index_lt n' m' - | _, _ => false - end. - -Lemma index_eq_prop : forall n m:index, index_eq n m = true -> n = m. - simple induction n; simple induction m; simpl; intros. - rewrite (H i0 H1); reflexivity. - discriminate. - discriminate. - discriminate. - rewrite (H i0 H1); reflexivity. - discriminate. - discriminate. - discriminate. - reflexivity. -Qed. - -End variables_map. - -Unset Implicit Arguments. diff --git a/plugins/quote/g_quote.mlg b/plugins/quote/g_quote.mlg deleted file mode 100644 index 749903c3ad..0000000000 --- a/plugins/quote/g_quote.mlg +++ /dev/null @@ -1,46 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -{ - -open Ltac_plugin -open Names -open Tacexpr -open Geninterp -open Quote -open Stdarg -open Tacarg - -} - -DECLARE PLUGIN "quote_plugin" - -{ - -let cont = Id.of_string "cont" -let x = Id.of_string "x" - -let make_cont (k : Val.t) (c : EConstr.t) = - let c = Tacinterp.Value.of_constr c in - let tac = TacCall (Loc.tag (Locus.ArgVar CAst.(make cont), [Reference (Locus.ArgVar CAst.(make x))])) in - let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in - Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac)) - -} - -TACTIC EXTEND quote -| [ "quote" ident(f) ] -> { quote f [] } -| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> { quote f lc } -| [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] -> - { gen_quote (make_cont k) c f [] } -| [ "quote" ident(f) "[" ne_ident_list(lc) "]" - "in" constr(c) "using" tactic(k) ] -> - { gen_quote (make_cont k) c f lc } -END diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml deleted file mode 100644 index 7464b42dc5..0000000000 --- a/plugins/quote/quote.ml +++ /dev/null @@ -1,540 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* The `Quote' tactic *) - -(* The basic idea is to automatize the inversion of interpretation functions - in 2-level approach - - Examples are given in \texttt{theories/DEMOS/DemoQuote.v} - - Suppose you have a langage \texttt{L} of 'abstract terms' - and a type \texttt{A} of 'concrete terms' - and a function \texttt{f : L -> (varmap A L) -> A}. - - Then, the tactic \texttt{quote f} will replace an - expression \texttt{e} of type \texttt{A} by \texttt{(f vm t)} - such that \texttt{e} and \texttt{(f vm t)} are convertible. - - The problem is then inverting the function \texttt{f}. - - The tactic works when: - - \begin{itemize} - \item L is a simple inductive datatype. The constructors of L may - have one of the three following forms: - - \begin{enumerate} - \item ordinary recursive constructors like: \verb|Cplus : L -> L -> L| - \item variable leaf like: \verb|Cvar : index -> L| - \item constant leaf like \verb|Cconst : A -> L| - \end{enumerate} - - The definition of \texttt{L} must contain at most one variable - leaf and at most one constant leaf. - - When there are both a variable leaf and a constant leaf, there is - an ambiguity on inversion. The term t can be either the - interpretation of \texttt{(Cconst t)} or the interpretation of - (\texttt{Cvar}~$i$) in a variable map containing the binding $i - \rightarrow$~\texttt{t}. How to discriminate between these - choices? - - To solve the dilemma, one gives to \texttt{quote} a list of - \emph{constant constructors}: a term will be considered as a - constant if it is either a constant constructor or the - application of a constant constructor to constants. For example - the list \verb+[S, O]+ defines the closed natural - numbers. \texttt{(S (S O))} is a constant when \texttt{(S x)} is - not. - - The definition of constants vary for each application of the - tactic, so it can even be different for two applications of - \texttt{quote} with the same function. - - \item \texttt{f} is a quite simple fixpoint on - \texttt{L}. In particular, \texttt{f} must verify: - -\begin{verbatim} - (f (Cvar i)) = (varmap_find vm default_value i) -\end{verbatim} -\begin{verbatim} - (f (Cconst c)) = c -\end{verbatim} - - where \texttt{index} and \texttt{varmap\_find} are those defined - the \texttt{Quote} module. \emph{The tactic won't work with - user's own variables map!!} It is mandatory to use the - variable map defined in module \texttt{Quote}. - - \end{itemize} - - The method to proceed is then clear: - - \begin{itemize} - \item Start with an empty hashtable of "registed leafs" - that maps constr to integers and a "variable counter" equal to 0. - \item Try to match the term with every right hand side of the - definition of \texttt{f}. - - If there is one match, returns the correponding left hand - side and call yourself recursively to get the arguments of this - left hand side. - - If there is no match, we are at a leaf. That is the - interpretation of either a variable or a constant. - - If it is a constant, return \texttt{Cconst} applied to that - constant. - - If not, it is a variable. Look in the hashtable - if this leaf has been already encountered. If not, increment - the variable counter and add an entry to the hashtable; then - return \texttt{(Cvar !variables\_counter)} - \end{itemize} -*) - - -(*i*) -open CErrors -open Util -open Names -open Constr -open EConstr -open Pattern -open Patternops -open Constr_matching -open Tacmach -open Proofview.Notations -(*i*) - -(*s First, we need to access some Coq constants - We do that lazily, because this code can be linked before - the constants are loaded in the environment *) - -let constant dir s = - EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "Quote" ("quote"::dir) s - -let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm") -let coq_Node_vm = lazy (constant ["Quote"] "Node_vm") -let coq_varmap_find = lazy (constant ["Quote"] "varmap_find") -let coq_Right_idx = lazy (constant ["Quote"] "Right_idx") -let coq_Left_idx = lazy (constant ["Quote"] "Left_idx") -let coq_End_idx = lazy (constant ["Quote"] "End_idx") - -(*s Then comes the stuff to decompose the body of interpetation function - and pre-compute the inversion data. - -For a function like: - -\begin{verbatim} - Fixpoint interp (vm:varmap Prop) (f:form) := - match f with - | f_and f1 f1 f2 => (interp f1) /\ (interp f2) - | f_or f1 f1 f2 => (interp f1) \/ (interp f2) - | f_var i => varmap_find Prop default_v i vm - | f_const c => c - end. -\end{verbatim} - -With the constant constructors \texttt{C1}, \dots, \texttt{Cn}, the -corresponding scheme will be: - -\begin{verbatim} - {normal_lhs_rhs = - [ "(f_and ?1 ?2)", "?1 /\ ?2"; - "(f_or ?1 ?2)", " ?1 \/ ?2";]; - return_type = "Prop"; - constants = Some [C1,...Cn]; - variable_lhs = Some "(f_var ?1)"; - constant_lhs = Some "(f_const ?1)" - } -\end{verbatim} - -If there is no constructor for variables in the type \texttt{form}, -then [variable_lhs] is [None]. Idem for constants and -[constant_lhs]. Both cannot be equal to [None]. - -The metas in the RHS must correspond to those in the LHS (one cannot -exchange ?1 and ?2 in the example above) - -*) - -module ConstrSet = Set.Make(Constr) - -type inversion_scheme = { - normal_lhs_rhs : (constr * constr_pattern) list; - variable_lhs : constr option; - return_type : constr; - constants : ConstrSet.t; - constant_lhs : constr option } - -(*s [compute_ivs gl f cs] computes the inversion scheme associated to - [f:constr] with constants list [cs:constr list] in the context of - goal [gl]. This function uses the auxiliary functions - [i_can't_do_that], [decomp_term], [compute_lhs] and [compute_rhs]. *) - -let i_can't_do_that () = user_err Pp.(str "Quote: not a simple fixpoint") - -let decomp_term sigma c = EConstr.kind sigma (Termops.strip_outer_cast sigma c) - -(*s [compute_lhs typ i nargsi] builds the term \texttt{(C ?nargsi ... - ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive - type [typ] *) - -let coerce_meta_out id = - let s = Id.to_string id in - int_of_string (String.sub s 1 (String.length s - 1)) -let coerce_meta_in n = - Id.of_string ("M" ^ string_of_int n) - -let compute_lhs sigma typ i nargsi = - match EConstr.kind sigma typ with - | Ind((sp,0),u) -> - let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in - mkApp (mkConstructU (((sp,0),i+1),u), argsi) - | _ -> i_can't_do_that () - -(*s This function builds the pattern from the RHS. Recursive calls are - replaced by meta-variables ?i corresponding to those in the LHS *) - -let compute_rhs env sigma bodyi index_of_f = - let rec aux c = - match EConstr.kind sigma c with - | App (j, args) when isRel sigma j && Int.equal (destRel sigma j) index_of_f (* recursive call *) -> - let i = destRel sigma (Array.last args) in - PMeta (Some (coerce_meta_in i)) - | App (f,args) -> - PApp (pattern_of_constr env sigma (EConstr.to_constr sigma f), Array.map aux args) - | Cast (c,_,_) -> aux c - | _ -> pattern_of_constr env sigma (EConstr.to_constr sigma c) - in - aux bodyi - -(*s Now the function [compute_ivs] itself *) - -let compute_ivs f cs gl = - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let (cst, u) = try destConst sigma f with DestKO -> i_can't_do_that () in - let u = EInstance.kind sigma u in - let body = Environ.constant_value_in (Global.env()) (cst, u) in - let body = EConstr.of_constr body in - match decomp_term sigma body with - | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> - let (args3, body3) = decompose_lam sigma body2 in - let nargs3 = List.length args3 in - let is_conv = Reductionops.is_conv env sigma in - begin match decomp_term sigma body3 with - | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *) - let n_lhs_rhs = ref [] - and v_lhs = ref (None : constr option) - and c_lhs = ref (None : constr option) in - Array.iteri - (fun i ci -> - let argsi, bodyi = decompose_lam sigma ci in - let nargsi = List.length argsi in - (* REL (narg3 + nargsi + 1) is f *) - (* 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 isRel sigma bodyi && Int.equal (destRel sigma bodyi) 1 then - c_lhs := Some (compute_lhs sigma (snd (List.hd args3)) - i nargsi) - (* Then we test if the RHS is the RHS for variables *) - else begin match decompose_app sigma bodyi with - | vmf, [_; _; a3; a4 ] - when isRel sigma a3 && isRel sigma a4 && is_conv vmf - (Lazy.force coq_varmap_find) -> - v_lhs := Some (compute_lhs sigma - (snd (List.hd args3)) - i nargsi) - (* Third case: this is a normal LHS-RHS *) - | _ -> - n_lhs_rhs := - (compute_lhs sigma (snd (List.hd args3)) i nargsi, - compute_rhs env sigma bodyi (nargs3 + nargsi + 1)) - :: !n_lhs_rhs - end) - lci; - - if Option.is_empty !c_lhs && Option.is_empty !v_lhs then i_can't_do_that (); - - (* The Cases predicate is a lambda; we assume no dependency *) - let p = match EConstr.kind sigma p with - | Lambda (_,_,p) -> Termops.pop p - | _ -> p - in - - { normal_lhs_rhs = List.rev !n_lhs_rhs; - variable_lhs = !v_lhs; - return_type = p; - constants = List.fold_right ConstrSet.add cs ConstrSet.empty; - constant_lhs = !c_lhs } - - | _ -> i_can't_do_that () - end - |_ -> i_can't_do_that () - -(* TODO for that function: -\begin{itemize} -\item handle the case where the return type is an argument of the - function -\item handle the case of simple mutual inductive (for example terms - and lists of terms) formulas with the corresponding mutual - recursvive interpretation functions. -\end{itemize} -*) - -(*s Stuff to build variables map, currently implemented as complete -binary search trees (see file \texttt{Quote.v}) *) - -(* First the function to distinghish between constants (closed terms) - and variables (open terms) *) - -let rec closed_under sigma cset t = - (ConstrSet.mem (EConstr.Unsafe.to_constr t) cset) || - (match EConstr.kind sigma t with - | Cast(c,_,_) -> closed_under sigma cset c - | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l - | _ -> false) - -(*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete - binary search tree containing the [ci], that is: - -\begin{verbatim} - c1 - / \ - c2 c3 - / \ - c4 c5 -\end{verbatim} - -The second argument is a constr (the common type of the [ci]) -*) - -let btree_of_array a ty = - let size_of_a = Array.length a in - let semi_size_of_a = size_of_a lsr 1 in - let node = Lazy.force coq_Node_vm - and empty = mkApp (Lazy.force coq_Empty_vm, [| ty |]) in - let rec aux n = - if n > size_of_a - then empty - else if n > semi_size_of_a - then mkApp (node, [| ty; a.(n-1); empty; empty |]) - else mkApp (node, [| ty; a.(n-1); aux (2*n); aux (2*n+1) |]) - in - aux 1 - -(*s [btree_of_array] and [path_of_int] verify the following invariant:\\ - {\tt (varmap\_find A dv }[(path_of_int n)] [(btree_of_array a ty)] - = [a.(n)]\\ - [n] must be [> 0] *) - -let path_of_int n = - (* returns the list of digits of n in reverse order with - initial 1 removed *) - let rec digits_of_int n = - if Int.equal n 1 then [] - else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1)) - in - List.fold_right - (fun b c -> mkApp ((if b then Lazy.force coq_Right_idx - else Lazy.force coq_Left_idx), - [| c |])) - (List.rev (digits_of_int n)) - (Lazy.force coq_End_idx) - -(*s The tactic works with a list of subterms sharing the same - variables map. We need to sort terms in order to avoid than - strange things happen during replacement of terms by their - 'abstract' counterparties. *) - -(* [subterm t t'] tests if constr [t'] occurs in [t] *) -(* This function does not descend under binders (lambda and Cases) *) - -let rec subterm gl (t : constr) (t' : constr) = - (pf_conv_x gl t t') || - (match EConstr.kind (project gl) t with - | App (f,args) -> Array.exists (fun t -> subterm gl t t') args - | Cast(t,_,_) -> (subterm gl t t') - | _ -> false) - -(*s We want to sort the list according to reverse subterm order. *) -(* Since it's a partial order the algoritm of Sort.list won't work !! *) - -let rec sort_subterm gl l = - let sigma = project gl in - let rec insert c = function - | [] -> [c] - | (h::t as l) when EConstr.eq_constr sigma 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(Constr) - -let subst_meta subst c = - let subst = List.map (fun (i, c) -> i, EConstr.Unsafe.to_constr c) subst in - EConstr.of_constr (Termops.subst_meta subst (EConstr.Unsafe.to_constr c)) - -(*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. - The type of arguments is:\\ - [ivs : inversion_scheme]\\ - [lc: constr list]\\ - [gl: goal sigma]\\ *) -let quote_terms env sigma ivs lc = - Coqlib.check_required_library ["Coq";"quote";"Quote"]; - 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 = - let rec auxl l = - match l with - | (lhs, rhs)::tail -> - begin try - let s1 = Id.Map.bindings (matches env sigma rhs c) in - let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1 - in - subst_meta s2 lhs - with PatternMatchingFailure -> auxl tail - end - | [] -> - begin match ivs.variable_lhs with - | None -> - begin match ivs.constant_lhs with - | Some c_lhs -> subst_meta [1, c] c_lhs - | None -> anomaly (Pp.str "invalid inversion scheme for quote.") - end - | Some var_lhs -> - begin match ivs.constant_lhs with - | Some c_lhs when closed_under sigma ivs.constants c -> - subst_meta [1, c] c_lhs - | _ -> - begin - try Constrhash.find varhash (EConstr.Unsafe.to_constr c) - with Not_found -> - let newvar = - subst_meta [1, (path_of_int !counter)] - var_lhs in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash (EConstr.Unsafe.to_constr c) newvar; - newvar - end - end - end - end - in - auxl ivs.normal_lhs_rhs - in - let lp = List.map aux lc in - (lp, (btree_of_array (Array.of_list (List.rev !varlist)) - ivs.return_type )) - -(*s actually we could "quote" a list of terms instead of a single - term. Ring for example needs that, but Ring doesn't use Quote - yet. *) - -let pf_constrs_of_globals l = - let rec aux l acc = - match l with - [] -> Proofview.tclUNIT (List.rev acc) - | hd :: tl -> - Tacticals.New.pf_constr_of_global hd >>= fun g -> aux tl (g :: acc) - in aux l [] - -let quote f lid = - Proofview.Goal.enter begin fun gl -> - let fg = Tacmach.New.pf_global f gl in - let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in - Tacticals.New.pf_constr_of_global fg >>= fun f -> - pf_constrs_of_globals clg >>= fun cl -> - Proofview.Goal.nf_enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let ivs = compute_ivs f (List.map (EConstr.to_constr sigma) cl) gl in - let concl = Proofview.Goal.concl gl in - let quoted_terms = quote_terms env sigma ivs [concl] in - let (p, vm) = match quoted_terms with - | [p], vm -> (p,vm) - | _ -> assert false - in - match ivs.variable_lhs with - | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast - | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast - end - end - -let gen_quote cont c f lid = - Proofview.Goal.enter begin fun gl -> - let fg = Tacmach.New.pf_global f gl in - let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in - Tacticals.New.pf_constr_of_global fg >>= fun f -> - pf_constrs_of_globals clg >>= fun cl -> - Proofview.Goal.nf_enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let cl = List.map (EConstr.to_constr sigma) cl in - let ivs = compute_ivs f cl gl in - let quoted_terms = quote_terms env sigma ivs [c] in - let (p, vm) = match quoted_terms with - | [p], vm -> (p,vm) - | _ -> assert false - in - match ivs.variable_lhs with - | None -> cont (mkApp (f, [| p |])) - | Some _ -> cont (mkApp (f, [| vm; p |])) - end - end - -(*i - -Just testing ... - -#use "include.ml";; -open Quote;; - -let r = glob_constr_of_string;; - -let ivs = { - normal_lhs_rhs = - [ r "(f_and ?1 ?2)", r "?1/\?2"; - r "(f_not ?1)", r "~?1"]; - variable_lhs = Some (r "(f_atom ?1)"); - return_type = r "Prop"; - constants = ConstrSet.empty; - constant_lhs = (r "nat") -};; - -let t1 = r "True/\(True /\ ~False)";; -let t2 = r "True/\~~False";; - -quote_term ivs () t1;; -quote_term ivs () t2;; - -let ivs2 = - normal_lhs_rhs = - [ r "(f_and ?1 ?2)", r "?1/\?2"; - r "(f_not ?1)", r "~?1" - r "True", r "f_true"]; - variable_lhs = Some (r "(f_atom ?1)"); - return_type = r "Prop"; - constants = ConstrSet.empty; - constant_lhs = (r "nat") - -i*) diff --git a/plugins/quote/quote_plugin.mlpack b/plugins/quote/quote_plugin.mlpack deleted file mode 100644 index 2e9be09d8d..0000000000 --- a/plugins/quote/quote_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -Quote -G_quote diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v index a9b4d9d6f4..920b13ef49 100644 --- a/plugins/setoid_ring/Ring_base.v +++ b/plugins/setoid_ring/Ring_base.v @@ -12,7 +12,6 @@ ring tactic. Abstract rings need more theory, depending on ZArith_base. *) -Require Import Quote. Declare ML Module "newring_plugin". Require Export Ring_theory. Require Export Ring_tac. diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index e8efb362e2..26fef99bb2 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -15,7 +15,6 @@ Require Import Ring_polynom. Require Import BinList. Require Export ListTactics. Require Import InitialRing. -Require Import Quote. Declare ML Module "newring_plugin". diff --git a/test-suite/output/Quote.v b/test-suite/output/Quote.v deleted file mode 100644 index 2c373d5052..0000000000 --- a/test-suite/output/Quote.v +++ /dev/null @@ -1,36 +0,0 @@ -Require Import Quote. - -Parameter A B : Prop. - -Inductive formula : Type := - | f_and : formula -> formula -> formula - | f_or : formula -> formula -> formula - | f_not : formula -> formula - | f_true : formula - | f_atom : index -> formula - | f_const : Prop -> formula. - -Fixpoint interp_f (vm: - varmap Prop) (f:formula) {struct f} : Prop := - match f with - | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2 - | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2 - | f_not f1 => ~ interp_f vm f1 - | f_true => True - | f_atom i => varmap_find True i vm - | f_const c => c - end. - -Goal A \/ B -> A /\ (B \/ A) /\ (A \/ ~ B). -intro H. -match goal with - | H : ?a \/ ?b |- _ => quote interp_f in a using (fun x => idtac x; change (x \/ b) in H) -end. -match goal with - |- ?g => quote interp_f [ A ] in g using (fun x => idtac x) -end. -quote interp_f. -Show. -simpl; quote interp_f [ A ]. -Show. -Admitted. |