summaryrefslogtreecommitdiff
path: root/plugins/quote
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/quote
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/quote')
-rw-r--r--plugins/quote/Quote.v87
-rw-r--r--plugins/quote/g_quote.ml431
-rw-r--r--plugins/quote/quote.ml504
-rw-r--r--plugins/quote/quote_plugin.mllib3
-rw-r--r--plugins/quote/vo.itarget1
5 files changed, 626 insertions, 0 deletions
diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v
new file mode 100644
index 00000000..11726675
--- /dev/null
+++ b/plugins/quote/Quote.v
@@ -0,0 +1,87 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id$ *)
+
+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.
+Unset Boxed Definitions.
+
+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 in |- *; 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.ml4 b/plugins/quote/g_quote.ml4
new file mode 100644
index 00000000..bdeb9844
--- /dev/null
+++ b/plugins/quote/g_quote.ml4
@@ -0,0 +1,31 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Util
+open Tacexpr
+open Quote
+
+let make_cont k x =
+ let k = TacDynamic(dummy_loc, Tacinterp.tactic_in (fun _ -> fst 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
+
+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
new file mode 100644
index 00000000..2e4d07d6
--- /dev/null
+++ b/plugins/quote/quote.ml
@@ -0,0 +1,504 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id$ *)
+
+(* The `Quote' tactic *)
+
+(* The basic idea is to automatize the inversion of interpetation 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 Pp
+open Util
+open Names
+open Term
+open Pattern
+open Matching
+open Tacmach
+open Tactics
+open Proof_trees
+open Tacexpr
+(*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 = Coqlib.gen_constant "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(
+ struct
+ type t = constr
+ let compare = (Pervasives.compare : t->t->int)
+ end)
+
+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 () = error "Quote: not a simple fixpoint"
+
+let decomp_term c = kind_of_term (strip_outer_cast 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 = string_of_id 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 typ i nargsi =
+ match kind_of_term typ with
+ | Ind(sp,0) ->
+ let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in
+ mkApp (mkConstruct ((sp,0),i+1), 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 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 *) ->
+ let i = destRel (array_last args) in
+ PMeta (Some (coerce_meta_in i))
+ | App (f,args) ->
+ PApp (snd (pattern_of_constr Evd.empty f), Array.map aux args)
+ | Cast (c,_,_) -> aux c
+ | _ -> snd (pattern_of_constr Evd.empty c)
+ in
+ aux bodyi
+
+(*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 body = Environ.constant_value (Global.env()) cst in
+ match decomp_term body with
+ | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
+ let (args3, body3) = decompose_lam body2 in
+ let nargs3 = List.length args3 in
+ begin match decomp_term 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 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 bodyi = mkRel 1 then
+ c_lhs := Some (compute_lhs (snd (List.hd args3))
+ i nargsi)
+ (* Then we test if the RHS is the RHS for variables *)
+ else begin match decompose_app bodyi with
+ | vmf, [_; _; a3; a4 ]
+ when isRel a3 & isRel a4 &
+ pf_conv_x gl vmf
+ (Lazy.force coq_varmap_find)->
+ v_lhs := Some (compute_lhs
+ (snd (List.hd args3))
+ i nargsi)
+ (* Third case: this is a normal LHS-RHS *)
+ | _ ->
+ n_lhs_rhs :=
+ (compute_lhs (snd (List.hd args3)) i nargsi,
+ compute_rhs bodyi (nargs3 + nargsi + 1))
+ :: !n_lhs_rhs
+ end)
+ lci;
+
+ if !c_lhs = None & !v_lhs = None then i_can't_do_that ();
+
+ (* The Cases predicate is a lambda; we assume no dependency *)
+ let p = match kind_of_term 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 cset t =
+ (ConstrSet.mem t cset) or
+ (match (kind_of_term t) with
+ | Cast(c,_,_) -> closed_under cset c
+ | App(f,l) -> closed_under cset f && array_for_all (closed_under 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 n=1 then []
+ else (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') or
+ (match (kind_of_term 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 rec insert c = function
+ | [] -> [c]
+ | (h::t as l) when 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)
+
+(*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 ivs lc gl =
+ Coqlib.check_required_library ["Coq";"quote";"Quote"];
+ let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.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 = matches rhs c in
+ let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1
+ in
+ Termops.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 -> Termops.subst_meta [1, c] c_lhs
+ | None -> anomaly "invalid inversion scheme for quote"
+ end
+ | Some var_lhs ->
+ begin match ivs.constant_lhs with
+ | Some c_lhs when closed_under ivs.constants c ->
+ Termops.subst_meta [1, c] c_lhs
+ | _ ->
+ begin
+ try Hashtbl.find varhash c
+ with Not_found ->
+ let newvar =
+ Termops.subst_meta [1, (path_of_int !counter)]
+ var_lhs in
+ begin
+ incr counter;
+ varlist := c :: !varlist;
+ Hashtbl.add varhash 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 quote f lid gl =
+ let f = pf_global gl f in
+ let cl = List.map (pf_global gl) lid in
+ let ivs = compute_ivs gl f cl in
+ let (p, vm) = match quote_terms ivs [(pf_concl gl)] gl with
+ | [p], vm -> (p,vm)
+ | _ -> assert false
+ in
+ match ivs.variable_lhs with
+ | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl
+ | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl
+
+let gen_quote cont c f lid gl =
+ let f = pf_global gl f in
+ let cl = List.map (pf_global gl) lid in
+ let ivs = compute_ivs gl f cl in
+ let (p, vm) = match quote_terms ivs [c] gl with
+ | [p], vm -> (p,vm)
+ | _ -> assert false
+ in
+ match ivs.variable_lhs with
+ | None -> cont (mkApp (f, [| p |])) gl
+ | Some _ -> cont (mkApp (f, [| vm; p |])) gl
+
+(*i
+
+Just testing ...
+
+#use "include.ml";;
+open Quote;;
+
+let r = raw_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.mllib b/plugins/quote/quote_plugin.mllib
new file mode 100644
index 00000000..d1b3ccbe
--- /dev/null
+++ b/plugins/quote/quote_plugin.mllib
@@ -0,0 +1,3 @@
+Quote
+G_quote
+Quote_plugin_mod
diff --git a/plugins/quote/vo.itarget b/plugins/quote/vo.itarget
new file mode 100644
index 00000000..7a44fc5a
--- /dev/null
+++ b/plugins/quote/vo.itarget
@@ -0,0 +1 @@
+Quote.vo \ No newline at end of file