From fb3c1e60fa6c7438486658cc3a8c15abc6c729e5 Mon Sep 17 00:00:00 2001 From: glondu Date: Mon, 30 Mar 2009 15:22:23 +0000 Subject: Fix some typos and spaces git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12036 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/quote/Quote.v | 2 +- plugins/quote/quote.ml | 217 +++++++++++++++++++++++++------------------------ 2 files changed, 110 insertions(+), 109 deletions(-) (limited to 'plugins/quote') diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v index f21a678e1..11726675b 100644 --- a/plugins/quote/Quote.v +++ b/plugins/quote/Quote.v @@ -17,7 +17,7 @@ Declare ML Module "quote_plugin". 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 : Type -> Type. varmap_find : (A:Type)A -> index -> (varmap A) -> A. The first arg. of varmap_find is the default value to take diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 9141dc2f5..c2193fb48 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -10,20 +10,20 @@ (* The `Quote' tactic *) -(* The basic idea is to automatize the inversion of interpetation functions - in 2-level approach +(* 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' + 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)} + 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 f. + The problem is then inverting the function \texttt{f}. The tactic works when: @@ -43,24 +43,24 @@ 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 variables map containing the binding $i + (\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 + 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 of the + 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. + 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. - + 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: + \texttt{L}. In particular, \texttt{f} must verify: \begin{verbatim} (f (Cvar i)) = (varmap_find vm default_value i) @@ -71,18 +71,18 @@ 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 - variables map defined in module \texttt{Quote}. - + 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 map 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 f. + 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 @@ -92,17 +92,17 @@ interpretation of either a variable or a constant. If it is a constant, return \texttt{Cconst} applied to that - constant. + constant. - If not, it is a variable. Look in the hashtable + If not, it is a variable. Look in the hashtable if this leaf has been already encountered. If not, increment - the variables counter and add an entry to the hashtable; then + the variable counter and add an entry to the hashtable; then return \texttt{(Cvar !variables\_counter)} \end{itemize} *) -(*i*) +(*i*) open Pp open Util open Names @@ -134,19 +134,20 @@ let coq_End_idx = lazy (constant ["Quote"] "End_idx") For a function like: \begin{verbatim} - Fixpoint interp[vm:(varmap Prop); f:form] := - Cases f of - | (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 + 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: +corresponding scheme will be: \begin{verbatim} - {normal_lhs_rhs = + {normal_lhs_rhs = [ "(f_and ?1 ?2)", "?1 /\ ?2"; "(f_or ?1 ?2)", " ?1 \/ ?2";]; return_type = "Prop"; @@ -156,17 +157,17 @@ corresponding scheme will be: } \end{verbatim} -If there is no constructor for variables in the type \texttt{form}, +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) +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 + struct type t = constr let compare = (Pervasives.compare : t->t->int) end) @@ -179,7 +180,7 @@ type inversion_scheme = { 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 + [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]. *) @@ -191,7 +192,7 @@ let decomp_term c = kind_of_term (strip_outer_cast c) ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive type [typ] *) -let coerce_meta_out id = +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 = @@ -199,7 +200,7 @@ let coerce_meta_in n = let compute_lhs typ i nargsi = match kind_of_term typ with - | Ind(sp,0) -> + | 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 () @@ -208,14 +209,14 @@ let compute_lhs typ i nargsi = replaced by meta-variables ?i corresponding to those in the LHS *) let compute_rhs bodyi index_of_f = - let rec aux c = + 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 + | 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 (pattern_of_constr f, Array.map aux args) - | Cast (c,_,_) -> aux c + | Cast (c,_,_) -> aux c | _ -> pattern_of_constr c in aux bodyi @@ -235,34 +236,34 @@ let compute_ivs gl f cs = and v_lhs = ref (None : constr option) and c_lhs = ref (None : constr option) in Array.iteri - (fun i ci -> + (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 + 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 + else begin match decompose_app bodyi with | vmf, [_; _; a3; a4 ] when isRel a3 & isRel a4 & - pf_conv_x gl vmf + pf_conv_x gl vmf (Lazy.force coq_varmap_find)-> - v_lhs := Some (compute_lhs + 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) + 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 *) @@ -270,14 +271,14 @@ let compute_ivs gl f cs = | 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 () + + | _ -> i_can't_do_that () end |_ -> i_can't_do_that () @@ -287,23 +288,23 @@ let compute_ivs gl f cs = function \item handle the case of simple mutual inductive (for example terms and lists of terms) formulas with the corresponding mutual - recursvive interpretation functions. + 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) +(* 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 + | 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: @@ -317,35 +318,35 @@ let rec closed_under cset t = 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 + 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 + if n > size_of_a then empty - else if n > semi_size_of_a + 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 + 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)] + {\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 = +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 [] + 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 + 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)) @@ -359,29 +360,29 @@ let path_of_int n = (* [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) = +let rec subterm gl (t : constr) (t' : constr) = (pf_conv_x gl t t') or - (match (kind_of_term t) with + (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 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 -> 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. + to store leafs that are already encountered. The type of arguments is:\\ [ivs : inversion_scheme]\\ [lc: constr list]\\ @@ -392,55 +393,55 @@ let quote_terms ivs lc gl = 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 = + let rec aux c = + let rec auxl l = match l with | (lhs, rhs)::tail -> - begin try + 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 -> + 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 -> + | 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)] + | _ -> + begin + try Hashtbl.find varhash c + with Not_found -> + let newvar = + Termops.subst_meta [1, (path_of_int !counter)] var_lhs in - begin + begin incr counter; varlist := c :: !varlist; Hashtbl.add varhash c newvar; newvar end end - end + end end - in - auxl ivs.normal_lhs_rhs + in + auxl ivs.normal_lhs_rhs in - let lp = List.map aux lc in - (lp, (btree_of_array (Array.of_list (List.rev !varlist)) + 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 the - conclusion of current goal. Ring for example needs that, but Ring doesn't - uses Quote yet. *) - +(*s actually we could "quote" a list of terms instead of the conclusion of + current goal. 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 @@ -453,7 +454,7 @@ let quote f lid gl = | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl -(*i +(*i Just testing ... @@ -463,13 +464,13 @@ open Quote;; let r = raw_constr_of_string;; let ivs = { - normal_lhs_rhs = + 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") + constant_lhs = (r "nat") };; let t1 = r "True/\(True /\ ~False)";; @@ -479,7 +480,7 @@ quote_term ivs () t1;; quote_term ivs () t2;; let ivs2 = - normal_lhs_rhs = + normal_lhs_rhs = [ r "(f_and ?1 ?2)", r "?1/\?2"; r "(f_not ?1)", r "~?1" r "True", r "f_true"]; -- cgit v1.2.3