aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/funind/indfun.ml6
-rw-r--r--contrib/interface/xlate.ml14
-rw-r--r--contrib/subtac/subtac_command.ml3
-rw-r--r--interp/constrintern.ml2
-rw-r--r--interp/topconstr.ml2
-rw-r--r--interp/topconstr.mli2
-rw-r--r--lib/util.ml10
-rw-r--r--lib/util.mli2
-rw-r--r--parsing/g_constr.ml47
-rw-r--r--parsing/g_vernac.ml417
-rw-r--r--parsing/g_xml.ml44
-rw-r--r--parsing/ppconstr.ml6
-rw-r--r--parsing/ppvernac.ml27
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/pretyping.ml41
-rw-r--r--pretyping/rawterm.ml2
-rw-r--r--pretyping/rawterm.mli2
-rw-r--r--toplevel/command.ml21
18 files changed, 114 insertions, 56 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 2fcdd3a75..d7c045a60 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -317,7 +317,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl =
(Topconstr.names_of_local_assums args)
in
let annot =
- try Util.list_index (Name id) names - 1, Topconstr.CStructRec
+ try Some (Util.list_index (Name id) names - 1), Topconstr.CStructRec
with Not_found -> raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id))
in
(name,annot,args,types,body),(None:Vernacexpr.decl_notation)
@@ -328,7 +328,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl =
(Util.dummy_loc,"GenFixpoint",
Pp.str "the recursive argument needs to be specified")
else
- (name,(0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
+ (name,(Some 0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
| (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_->
error
("Cannot use mutual definition with well-founded recursion")
@@ -417,7 +417,7 @@ let make_graph (id:identifier) =
)
in
let rec_id =
- match List.nth nal n with |(_,Name id) -> id | _ -> anomaly ""
+ match List.nth nal (out_some n) with |(_,Name id) -> id | _ -> anomaly ""
in
(id, Some (Struct rec_id),bl,t,b)
)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index da87086e2..a78c35d1d 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -298,9 +298,11 @@ let rec decompose_last = function
let make_fix_struct (n,bl) =
let names = names_of_local_assums bl in
let nn = List.length names in
- if nn = 1 then ctv_ID_OPT_NONE
- else if n < nn then xlate_id_opt(List.nth names n)
- else xlate_error "unexpected result of parsing for Fixpoint";;
+ if nn = 1 || n = None then ctv_ID_OPT_NONE
+ else
+ let n = out_some n in
+ if n < nn then xlate_id_opt(List.nth names n)
+ else xlate_error "unexpected result of parsing for Fixpoint";;
let rec xlate_binder = function
@@ -417,7 +419,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
| CFix (_, (_, id), lm::lmi) ->
let strip_mutrec (fid, (n, ro), bl, arf, ardef) =
let (struct_arg,bl,arf,ardef) =
+ (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
+ (* By the way, how could [bl = []] happen in V8 syntax ? *)
if bl = [] then
+ let n = out_some n in
let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
(xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
else (make_fix_struct (n, bl),bl,arf,ardef) in
@@ -1875,7 +1880,10 @@ let rec xlate_vernac =
| VernacFixpoint ((lm :: lmi),boxed) ->
let strip_mutrec ((fid, (n, ro), bl, arf, ardef), ntn) =
let (struct_arg,bl,arf,ardef) =
+ (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
+ (* By the way, how could [bl = []] happen in V8 syntax ? *)
if bl = [] then
+ let n = out_some n in
let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
(xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
else (make_fix_struct (n, bl),bl,arf,ardef) in
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 1b92c6911..727ba82ae 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -200,6 +200,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
(Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)
| CWfRec r ->
+ let n = out_some n in
let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
Ppconstr.pr_binders bl ++ str " : " ++
Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
@@ -279,7 +280,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
let (lnonrec,(namerec,defrec,arrec,nvrec)) =
collect_non_rec env0 lrecnames recdef arityl nv in
- let nvrec' = Array.map fst nvrec in(* ignore rec order *)
+ let nvrec' = Array.map (function (Some n,_) -> n | _ -> 0) nvrec in(* ignore rec order *)
let declare arrec defrec =
let recvec =
Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2057eb5b2..0be6b9dc6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -793,7 +793,7 @@ let internalise sigma globalenv env allow_soapp lvar c =
RStructRec,
List.fold_left intern_local_binder (env,[]) bl
| CWfRec c ->
- let before, after = list_chop (succ n) bl in
+ let before, after = list_chop (succ (out_some n)) bl in
let ((ids',_,_),rafter) =
List.fold_left intern_local_binder (env,[]) after in
let ro = RWfRec (intern (ids', tmp_scope, scopes) c) in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 4d4e3f88a..d82c04e07 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -532,7 +532,7 @@ type constr_expr =
and fixpoint_expr =
- identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+ identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
and local_binder =
| LocalRawDef of name located * constr_expr
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 073f9ba0b..4e2017f44 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -114,7 +114,7 @@ type constr_expr =
| CDynamic of loc * Dyn.t
and fixpoint_expr =
- identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+ identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
and cofixpoint_expr =
identifier * local_binder list * constr_expr * constr_expr
diff --git a/lib/util.ml b/lib/util.ml
index 33f91b04e..8b0b1e242 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -214,6 +214,16 @@ let list_index x =
in
index_x 1
+let list_unique_index x =
+ let rec index_x n = function
+ | y::l ->
+ if x = y then
+ if List.mem x l then raise Not_found
+ else n
+ else index_x (succ n) l
+ | [] -> raise Not_found
+ in index_x 1
+
let list_fold_left_i f =
let rec it_list_f i a = function
| [] -> a
diff --git a/lib/util.mli b/lib/util.mli
index f330ef8e0..1a2fedbdf 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -100,6 +100,8 @@ val list_map2_i :
val list_map3 :
('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
val list_index : 'a -> 'a list -> int
+(* [list_unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *)
+val list_unique_index : 'a -> 'a list -> int
val list_iter_i : (int -> 'a -> unit) -> 'a list -> unit
val list_fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
val list_fold_right_and_left :
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9c39878c7..ed9e1fa06 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -59,14 +59,13 @@ let rec mkCLambdaN loc bll c =
let rec index_and_rec_order_of_annot loc bl ann =
match names_of_local_assums bl,ann with
- | [_], (None, r) -> 0, r
+ | [_], (None, r) -> Some 0, r
| lids, (Some x, ro) ->
let ids = List.map snd lids in
- (try list_index (snd x) ids - 1, ro
+ (try Some (list_index (snd x) ids - 1), ro
with Not_found ->
user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable"))
- | _ -> user_err_loc(loc,"index_of_annot",
- Pp.str "cannot guess decreasing argument of fix")
+ | _, (None, r) -> None, r
let mk_fixb (id,bl,ann,body,(loc,tyc)) =
let n,ro = index_and_rec_order_of_annot (fst id) bl ann in
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 87f388a74..0a0df6fb2 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -218,16 +218,15 @@ GEXTEND Gram
let ni =
match fst annot with
Some id ->
- (try list_index (Name id) names - 1
- with Not_found -> Util.user_err_loc
- (loc,"Fixpoint",
- Pp.str "No argument named " ++ Nameops.pr_id id))
+ (try Some (list_index (Name id) names - 1)
+ with Not_found -> Util.user_err_loc
+ (loc,"Fixpoint",
+ Pp.str "No argument named " ++ Nameops.pr_id id))
| None ->
- if List.length names > 1 then
- Util.user_err_loc
- (loc,"Fixpoint",
- Pp.str "the recursive argument needs to be specified");
- 0 in
+ (* If there is only one argument, it is the recursive one,
+ otherwise, we search the recursive index later *)
+ if List.length names = 1 then Some 0 else None
+ in
((id, (ni, snd annot), bl, type_, def),ntn) ] ]
;
corec_definition:
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 1df3d1f25..8b3661dbe 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -205,11 +205,11 @@ and interp_xml_recursionOrder x =
and interp_xml_FixFunction x =
match interp_xml_tag "FixFunction" x with
| (loc,al,[x1;x2;x3]) ->
- ((nmtoken (get_xml_attr "recIndex" al),
+ ((Some (nmtoken (get_xml_attr "recIndex" al)),
interp_xml_recursionOrder x1),
(get_xml_ident al, interp_xml_type x2, interp_xml_body x3))
| (loc,al,[x1;x2]) -> (* For backwards compatibility *)
- ((nmtoken (get_xml_attr "recIndex" al), RStructRec),
+ ((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec),
(get_xml_ident al, interp_xml_type x1, interp_xml_body x2))
| (loc,_,_) ->
user_err_loc (loc,"",str "wrong number of arguments (expect one)")
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index a95fa4bad..e4cc3cd91 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -379,11 +379,11 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) =
let ids = names_of_local_assums bl in
match ro with
CStructRec ->
- if List.length ids > 1 then
- spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}"
+ if List.length ids > 1 && n <> None then
+ spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
else mt()
| CWfRec c ->
- spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids n)) ++ str"}"
+ spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
in
pr_recursive_decl pr prd dangling_with_for id bl annot t c
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index c08b07617..f43f93bd9 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -555,18 +555,23 @@ let rec pr_vernac = function
else ([],def,type_) in
let bl = bl @ bl' in
let ids = List.flatten (List.map name_of_binder bl) in
- let name =
- try snd (List.nth ids n)
- with Failure _ ->
- warn (str "non-printable fixpoint \""++pr_id id++str"\"");
- Anonymous in
let annot =
- match (ro : Topconstr.recursion_order_expr) with
- CStructRec ->
- if List.length ids > 1 then
- spc() ++ str "{struct " ++ pr_name name ++ str"}"
- else mt()
- | CWfRec c -> spc() ++ str "{wf " ++ pr_name name ++ spc() ++ pr_lconstr_expr c ++ str"}"
+ match n with
+ | None -> mt ()
+ | Some n ->
+ let name =
+ try snd (List.nth ids n)
+ with Failure _ ->
+ warn (str "non-printable fixpoint \""++pr_id id++str"\"");
+ Anonymous in
+ match (ro : Topconstr.recursion_order_expr) with
+ CStructRec ->
+ if List.length ids > 1 then
+ spc() ++ str "{struct " ++ pr_name name ++ str"}"
+ else mt()
+ | CWfRec c ->
+ spc() ++ str "{wf " ++ pr_name name ++ spc() ++
+ pr_lconstr_expr c ++ str"}"
in
pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a815e5d2f..edbbbb329 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -421,7 +421,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) =
let v = array_map3
(fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t))
bodies tys vn in
- RRec(dl,RFix (Array.map (fun i -> i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
+ RRec(dl,RFix (Array.map (fun i -> Some i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
Array.map (fun (bl,_,_) -> bl) v,
Array.map (fun (_,_,ty) -> ty) v,
Array.map (fun (_,bd,_) -> bd) v)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f48ec7462..64ea0bbb8 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -329,18 +329,35 @@ module Pretyping_F (Coercion : Coercion.S) = struct
{ uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
ctxtv vdef in
- evar_type_fixpoint loc env isevars names ftys vdefj;
- let fixj =
- match fixkind with
- | RFix (vn,i) ->
- let fix = ((Array.map fst vn, 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 ->
- 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
- inh_conv_coerce_to_tycon loc env isevars fixj tycon
+ evar_type_fixpoint loc env isevars names ftys vdefj;
+ let fixj = match fixkind with
+ | RFix (vn,i) ->
+ let guard_indexes = 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 ->
+ 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
+ inh_conv_coerce_to_tycon loc env isevars fixj tycon
| RSort (loc,s) ->
inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 1c5900417..36edf519b 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -73,7 +73,7 @@ and rawdecl = name * rawconstr option * rawconstr
and fix_recursion_order = RStructRec | RWfRec of rawconstr
-and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int
+and fix_kind = RFix of ((int option * fix_recursion_order) array * int) | RCoFix of int
let cases_predicate_names tml =
List.flatten (List.map (function
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index cbd215d85..8ef0cb939 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -70,7 +70,7 @@ and rawdecl = name * rawconstr option * rawconstr
and fix_recursion_order = RStructRec | RWfRec of rawconstr
-and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int
+and fix_kind = RFix of ((int option * fix_recursion_order) array * int) | RCoFix of int
val cases_predicate_names :
(rawconstr * (name * (loc * inductive * name list) option)) list -> name list
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b103b8382..b70cfb62f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -457,7 +457,9 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef
and sigma = Evd.empty
and env0 = Global.env()
- and nv = Array.of_list (List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef) in
+ and nv = Array.of_list (List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef)
+ and bl = Array.of_list (List.map (fun ((_,_,bl,_,_),_) -> bl) lnameargsardef)
+ in
(* Build the recursive context and notations for the recursive types *)
let (rec_sign,rec_impls,arityl) =
List.fold_left
@@ -502,9 +504,24 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
let recvec =
Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
+ let nvrec = 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 = snd (interp_context sigma env0 bl.(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 ->
+ error "the recursive argument needs to be specified")
+ nvrec
+ in
let rec declare i fi =
let ce =
- { const_entry_body = mkFix ((Array.map fst nvrec,i),recdecls); (* ignore rec order *)
+ { const_entry_body = mkFix ((nvrec,i),recdecls); (* ignore rec order *)
const_entry_type = Some arrec.(i);
const_entry_opaque = false;
const_entry_boxed = boxed} in
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 04:25:12 +0000