diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 14 | ||||
| -rw-r--r-- | lib/util.ml | 8 | ||||
| -rw-r--r-- | lib/util.mli | 3 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 66 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 5 | ||||
| -rw-r--r-- | toplevel/command.ml | 57 |
7 files changed, 114 insertions, 45 deletions
@@ -1,6 +1,12 @@ Changes from V8.1 to V8.2 ========================= +Language + +- If a fixpoint is not written with an explicit { struct ... }, then + all arguments are tried successively (from left to right) until one is + found that satisfies the structural decreasing condition. + Commands - Added option Global to "Implicit Arguments" and "Arguments Scope" for diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 424e5047da..8ee30b8fb8 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -1329,9 +1329,8 @@ syntactical constraints on a special argument called the decreasing argument. They are needed to ensure that the {\tt Fixpoint} definition always terminates. The point of the {\tt \{struct \ident {\tt \}}} annotation is to let the user tell the system which argument decreases -along the recursive calls. This annotation may be left implicit for -fixpoints where only one argument has an inductive type. For instance, -one can define the addition function as : +along the recursive calls. For instance, one can define the addition +function as : \begin{coq_example} Fixpoint add (n m:nat) {struct n} : nat := @@ -1341,6 +1340,15 @@ Fixpoint add (n m:nat) {struct n} : nat := end. \end{coq_example} +The {\tt \{struct \ident {\tt \}}} annotation may be left implicit, in +this case the system try successively arguments from left to right +until it finds one that satisfies the decreasing condition. Note that +some fixpoints may have several arguments that fit as decreasing +arguments, and this choice influences the reduction of the +fixpoint. Hence an explicit annotation must be used if the leftmost +decreasing argument is not the desired one. Writing explicit +annotations can also speed up type-checking of large mutual fixpoints. + The {\tt match} operator matches a value (here \verb:n:) with the various constructors of its (inductive) type. The remaining arguments give the respective values to be returned, as functions of the diff --git a/lib/util.ml b/lib/util.ml index a1c011ce1b..590d649931 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -445,6 +445,14 @@ let list_fold_map' f l e = let list_map_assoc f = List.map (fun (x,a) -> (x,f a)) +(* list_combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *) + +let rec list_combinations = function + | [] -> [[]] + | l::ll -> + let res = list_combinations ll in + list_map_append (fun x -> List.map (fun l -> x::l) res) l + (* Arrays *) let array_exists f v = diff --git a/lib/util.mli b/lib/util.mli index 5c59708211..c315ecd0ac 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -138,6 +138,9 @@ val list_join_map : ('a -> 'b list) -> 'a list -> 'b list val list_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list val list_fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list +(* list_combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *) +val list_combinations : 'a list list -> 'a list list + (*s Arrays. *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3aefeeb077..c5742268b1 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -43,6 +43,34 @@ open Inductiveops (************************************************************************) +(* An auxiliary function for searching for fixpoint guard indexes *) + +exception Found of int array + +let search_guard loc env possible_indexes fixdefs = + (* Standard situation with only one possibility for each fix. *) + (* We treat it separately in order to get proper error msg. *) + if List.for_all (fun l->1=List.length l) possible_indexes then + let indexes = Array.of_list (List.map List.hd possible_indexes) in + let fix = ((indexes, 0),fixdefs) in + (try check_fix env fix with + | e -> if loc = dummy_loc then raise e else Stdpp.raise_with_loc loc e); + indexes + else + (* we now search recursively amoungst all combinations *) + (try + List.iter + (fun l -> + let indexes = Array.of_list l in + let fix = ((indexes, 0),fixdefs) in + try check_fix env fix; raise (Found indexes) + with TypeError _ -> ()) + (list_combinations possible_indexes); + let errmsg = "cannot guess decreasing argument of fix" in + if loc = dummy_loc then error errmsg else + user_err_loc (loc,"search_guard", Pp.str errmsg) + with Found indexes -> indexes) + (* To embed constr in rawconstr *) let ((constr_in : constr -> Dyn.t), (constr_out : Dyn.t -> constr)) = create "constr" @@ -266,6 +294,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct | RProp c -> judge_of_prop_contents c | RType _ -> judge_of_new_Type () + exception Found of fixpoint + (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [(evars_of isevars)] and *) (* the type constraint tycon *) @@ -342,28 +372,22 @@ module Pretyping_F (Coercion : Coercion.S) = struct evar_type_fixpoint loc env isevars names ftys vdefj; let fixj = match fixkind with | RFix (vn,i) -> - let guard_indexes = Array.mapi + (* First, let's find the guard indexes. *) + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual + fixpoints ?) *) + let possible_indexes = Array.to_list (Array.mapi (fun i (n,_) -> match n with - | Some n -> n - | None -> - (* Recursive argument was not given by the user : We - check that there is only one inductive argument *) - let ctx = ctxtv.(i) in - let isIndApp t = - isInd (fst (decompose_app (strip_head_cast t))) in - (* This could be more precise (e.g. do some delta) *) - let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in - try (list_unique_index true lb) - 1 - with Not_found -> - Util.user_err_loc - (loc,"pretype", - Pp.str "cannot guess decreasing argument of fix")) - vn - in - let fix = ((guard_indexes, i),(names,ftys,Array.map j_val vdefj)) in - (try check_fix env fix with e -> Stdpp.raise_with_loc loc e); - make_judge (mkFix fix) ftys.(i) - | RCoFix i -> + | Some n -> [n] + | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i)) + vn) + in + let fixdecls = (names,ftys,Array.map j_val vdefj) in + let indexes = search_guard loc env possible_indexes fixdecls in + make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) + | RCoFix i -> let cofix = (i,(names,ftys,Array.map j_val vdefj)) in (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e); make_judge (mkCoFix cofix) ftys.(i) in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 0b9b47b7a7..64144f9a4d 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -18,6 +18,11 @@ open Rawterm open Evarutil (*i*) +(* An auxiliary function for searching for fixpoint guard indexes *) + +val search_guard : + Util.loc -> env -> int list list -> rec_declaration -> int array + type typing_constraint = OfType of types option | IsType type var_map = (identifier * unsafe_judgment) list diff --git a/toplevel/command.ml b/toplevel/command.ml index 6c4fe20571..05166b21fa 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -452,13 +452,27 @@ let build_mutual l finite = (* 3c| Fixpoints and co-fixpoints *) -let recursive_message = function +let pr_rank = function + | 0 -> str "1st" + | 1 -> str "2nd" + | 2 -> str "3rd" + | n -> str ((string_of_int n)^"th") + +let recursive_message indexes = function | [] -> anomaly "no recursive definition" - | [id] -> pr_id id ++ str " is recursively defined" + | [id] -> pr_id id ++ str " is recursively defined" ++ + (match indexes with + | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" + | _ -> mt ()) | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ - spc () ++ str "are recursively defined") - -let corecursive_message = function + spc () ++ str "are recursively defined" ++ + match indexes with + | Some a -> spc () ++ str "(decreasing respectively on " ++ + prlist_with_sep pr_coma pr_rank (Array.to_list a) ++ + str " arguments)" + | None -> mt ()) + +let corecursive_message _ = function | [] -> error "no corecursive definition" | [id] -> pr_id id ++ str " is corecursively defined" | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ @@ -572,19 +586,18 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs = let names = List.map (fun id -> Name id) fixnames in (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) -let compute_guardness_evidence (n,_) fixl fixtype = +let compute_possible_guardness_evidences (n,_) fixl fixtype = match n with - | Some n -> n + | Some n -> [n] | None -> - (* Recursive argument was not given by the user : - We check that there is only one inductive argument *) + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual + fixpoints ?) *) let m = local_binders_length fixl.fix_binders in let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in - let isIndApp t = isInd (fst (decompose_app (strip_head_cast t))) in - (* This could be more precise (e.g. do some delta) *) - let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in - try (list_unique_index true lb) - 1 - with Not_found -> error "the recursive argument needs to be specified" + list_map_i (fun i _ -> i) 0 ctx let interp_recursive fixkind l boxed = let env = Global.env() in @@ -618,18 +631,20 @@ let interp_recursive fixkind l boxed = (* Build the fix declaration block *) let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in - let fixdecls = + let indexes, fixdecls = match fixkind with | IsFixpoint wfl -> - let fixwf = list_map3 compute_guardness_evidence wfl fixl fixtypes in - list_map_i (fun i _ -> mkFix ((Array.of_list fixwf,i),fixdecls)) 0 l + let possible_indexes = + list_map3 compute_possible_guardness_evidences wfl fixl fixtypes in + let indexes = search_guard dummy_loc env possible_indexes fixdecls in + Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l | IsCoFixpoint -> - list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l + None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l in (* Declare the recursive definitions *) ignore (list_map3 (declare_fix boxed kind) fixnames fixdecls fixtypes); - if_verbose ppnl (recursive_message kind fixnames); + if_verbose ppnl (recursive_message kind indexes fixnames); (* Declare notations *) List.iter (declare_interning_data ([],[])) notations @@ -680,7 +695,7 @@ let build_induction_scheme lnamedepindsort = ConstRef kn :: lrecref in let _ = List.fold_right2 declare listdecl lrecnames [] in - if_verbose ppnl (recursive_message Fixpoint lrecnames) + if_verbose ppnl (recursive_message Fixpoint None lrecnames) let build_scheme l = let ischeme,escheme = split_scheme l in @@ -745,7 +760,7 @@ let build_combined_scheme name schemes = const_entry_opaque = false; const_entry_boxed = Options.boxed_definitions() } in let _ = declare_constant (snd name) (DefinitionEntry ce, IsDefinition Scheme) in - if_verbose ppnl (recursive_message Fixpoint [snd name]) + if_verbose ppnl (recursive_message Fixpoint None [snd name]) (* 4| Goal declaration *) |