aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrexpr.ml8
-rw-r--r--interp/constrexpr_ops.ml15
-rw-r--r--interp/constrextern.ml22
-rw-r--r--interp/constrintern.ml67
-rw-r--r--interp/notation_ops.ml2
-rw-r--r--interp/notation_term.ml2
-rw-r--r--parsing/g_constr.mlg14
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--plugins/funind/g_indfun.mlg6
-rw-r--r--plugins/funind/indfun.ml87
-rw-r--r--plugins/ssr/ssrparser.mlg4
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/glob_ops.ml16
-rw-r--r--pretyping/glob_term.ml19
-rw-r--r--pretyping/patternops.ml24
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--printing/ppconstr.ml17
-rw-r--r--printing/ppconstr.mli2
-rw-r--r--printing/proof_diffs.ml12
-rw-r--r--vernac/comFixpoint.ml25
-rw-r--r--vernac/comFixpoint.mli2
-rw-r--r--vernac/comProgramFixpoint.ml32
-rw-r--r--vernac/obligations.ml4
-rw-r--r--vernac/obligations.mli2
-rw-r--r--vernac/vernacexpr.ml2
25 files changed, 191 insertions, 201 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 7a14a4e708..653bb68f30 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -134,16 +134,16 @@ and branch_expr =
(cases_pattern_expr list list * constr_expr) CAst.t
and fix_expr =
- lident * (lident option * recursion_order_expr) *
+ lident * (recursion_order_expr CAst.t) option *
local_binder_expr list * constr_expr * constr_expr
and cofix_expr =
lident * local_binder_expr list * constr_expr * constr_expr
and recursion_order_expr =
- | CStructRec
- | CWfRec of constr_expr
- | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
+ | CStructRec of lident
+ | CWfRec of lident * constr_expr
+ | CMeasureRec of lident option * constr_expr * constr_expr option (** argument, measure, relation *)
(* Anonymous defs allowed ?? *)
and local_binder_expr =
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 60610b92b8..db860e0c3b 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -196,10 +196,9 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} =
List.equal (List.equal cases_pattern_expr_eq) p1 p2 &&
constr_expr_eq e1 e2
-and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) =
+and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) =
(eq_ast Id.equal id1 id2) &&
- Option.equal (eq_ast Id.equal) j1 j2 &&
- recursion_order_expr_eq r1 r2 &&
+ Option.equal (eq_ast recursion_order_expr_eq) r1 r2 &&
List.equal local_binder_eq bl1 bl2 &&
constr_expr_eq a1 a2 &&
constr_expr_eq b1 b2
@@ -211,9 +210,11 @@ and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) =
constr_expr_eq b1 b2
and recursion_order_expr_eq r1 r2 = match r1, r2 with
- | CStructRec, CStructRec -> true
- | CWfRec e1, CWfRec e2 -> constr_expr_eq e1 e2
- | CMeasureRec (e1, o1), CMeasureRec (e2, o2) ->
+ | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2
+ | CWfRec (i1,e1), CWfRec (i2,e2) ->
+ constr_expr_eq e1 e2
+ | CMeasureRec (i1, e1, o1), CMeasureRec (i2, e2, o2) ->
+ Option.equal (eq_ast Id.equal) i1 i2 &&
constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2
| _ -> false
@@ -349,7 +350,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
(f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po
| CFix (_,l) ->
let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_) -> g id) l n in
- List.fold_right (fun (_,(_,o),lb,t,c) acc ->
+ List.fold_right (fun (_,ro,lb,t,c) acc ->
fold_local_binders g f n'
(fold_local_binders g f n acc t lb) c lb) l acc
| CCoFix (_,_) ->
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b89b6b5765..3b169edaab 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -938,13 +938,12 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
let (assums,ids,bl) = extern_local_binder scopes vars bl in
let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
- let n =
- match fst nv.(i) with
- | None -> None
- | Some x -> Some (CAst.make @@ Name.get_id (List.nth assums x))
- in
- let ro = extern_recursion_order scopes vars (snd nv.(i)) in
- ((CAst.make fi), (n, ro), bl, extern_typ scopes vars0 ty,
+ let n =
+ match nv.(i) with
+ | None -> None
+ | Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x)))
+ in
+ ((CAst.make fi), n, bl, extern_typ scopes vars0 ty,
extern false scopes vars1 def)) idv
in
CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl)
@@ -1159,13 +1158,6 @@ and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function
let lonely_seen = add_lonely keyrule lonely_seen in
extern_notation allscopes lonely_seen vars t rules
-and extern_recursion_order scopes vars = function
- GStructRec -> CStructRec
- | GWfRec c -> CWfRec (extern true scopes vars c)
- | GMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m,
- Option.map (extern true scopes vars) r)
-
-
let extern_glob_constr vars c =
extern false (InConstrEntrySomeLevel,(None,[])) vars c
@@ -1294,7 +1286,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
let v = Array.map3
(fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t))
bl tl ln in
- GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi),
+ GRec(GFix (Array.map (fun i -> Some i) ln,i),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/interp/constrintern.ml b/interp/constrintern.ml
index 3329ba2047..c0801067ce 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1845,51 +1845,44 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
in
apply_impargs c env imp subscopes l loc
- | CFix ({ CAst.loc = locid; v = iddef}, dl) ->
+ | CFix ({ CAst.loc = locid; v = iddef}, dl) ->
let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in
let dl = Array.of_list dl in
- let n =
- try List.index0 Id.equal iddef lf
+ let n =
+ try List.index0 Id.equal iddef lf
with Not_found ->
- raise (InternalizationError (locid,UnboundFixName (false,iddef)))
- in
- let idl_temp = Array.map
- (fun (id,(n,order),bl,ty,_) ->
- let intern_ro_arg f =
- let before, after = split_at_annot bl n in
- let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
- let ro = f (intern env') in
- let n' = Option.map (fun _ -> List.count (fun c -> match DAst.get c with
- | GLocalAssum _ -> true
- | _ -> false (* remove let-ins *))
- rbefore) n in
- n', ro, List.fold_left intern_local_binder (env',rbefore) after
- in
- let n, ro, (env',rbl) =
- match order with
- | CStructRec ->
- intern_ro_arg (fun _ -> GStructRec)
- | CWfRec c ->
- intern_ro_arg (fun f -> GWfRec (f c))
- | CMeasureRec (m,r) ->
- intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r))
- in
- let bl = List.rev (List.map glob_local_binder_of_extended rbl) in
- ((n, ro), bl, intern_type env' ty, env')) dl in
+ raise (InternalizationError (locid,UnboundFixName (false,iddef)))
+ in
+ let idl_temp = Array.map
+ (fun (id,recarg,bl,ty,_) ->
+ let recarg = Option.map (function { CAst.v = v } -> match v with
+ | CStructRec i -> i
+ | _ -> anomaly Pp.(str "Non-structural recursive argument in non-program fixpoint")) recarg
+ in
+ let before, after = split_at_annot bl recarg in
+ let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
+ let n = Option.map (fun _ -> List.count (fun c -> match DAst.get c with
+ | GLocalAssum _ -> true
+ | _ -> false (* remove let-ins *))
+ rbefore) recarg in
+ let (env',rbl) = List.fold_left intern_local_binder (env',rbefore) after in
+ let bl = List.rev (List.map glob_local_binder_of_extended rbl) in
+ (n, bl, intern_type env' ty, env')) dl in
let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
- let env'' = List.fold_left_i (fun i en name ->
- let (_,bli,tyi,_) = idl_temp.(i) in
- let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
- push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
- en (CAst.make @@ Name name)) 0 env' lf in
- (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
- DAst.make ?loc @@
- GRec (GFix
- (Array.map (fun (ro,_,_,_) -> ro) idl,n),
+ let env'' = List.fold_left_i (fun i en name ->
+ let (_,bli,tyi,_) = idl_temp.(i) in
+ let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
+ push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
+ en (CAst.make @@ Name name)) 0 env' lf in
+ (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
+ DAst.make ?loc @@
+ GRec (GFix
+ (Array.map (fun (ro,_,_,_) -> ro) idl,n),
Array.of_list lf,
Array.map (fun (_,bl,_,_) -> bl) idl,
Array.map (fun (_,_,ty,_) -> ty) idl,
Array.map (fun (_,_,_,bd) -> bd) idl)
+
| CCoFix ({ CAst.loc = locid; v = iddef }, dl) ->
let lf = List.map (fun ({CAst.v = id},_,_,_) -> id) dl in
let dl = Array.of_list dl in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 9801e56ca1..7f084fffdd 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -957,7 +957,7 @@ let match_fix_kind fk1 fk2 =
match (fk1,fk2) with
| GCoFix n1, GCoFix n2 -> Int.equal n1 n2
| GFix (nl1,n1), GFix (nl2,n2) ->
- let test (n1, _) (n2, _) = match n1, n2 with
+ let test n1 n2 = match n1, n2 with
| _, None -> true
| Some id1, Some id2 -> Int.equal id1 id2
| _ -> false
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 6fe20486dc..5024f5c26f 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -38,7 +38,7 @@ type notation_constr =
notation_constr * notation_constr
| NIf of notation_constr * (Name.t * notation_constr option) *
notation_constr * notation_constr
- | NRec of fix_kind * Id.t array *
+ | NRec of glob_fix_kind * Id.t array *
(Name.t * notation_constr option * notation_constr) list array *
notation_constr array * notation_constr array
| NSort of glob_sort
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 0586dda555..7786155092 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -56,10 +56,10 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) : fix_expr =
(id,ann,bl,ty,body)
let mk_cofixb (id,bl,ann,body,(loc,tyc)) : cofix_expr =
- let _ = Option.map (fun { CAst.loc = aloc } ->
+ Option.iter (fun { CAst.loc = aloc } ->
CErrors.user_err ?loc:aloc
~hdr:"Constr:mk_cofixb"
- (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
+ (Pp.str"Annotation forbidden in cofix expression.")) ann;
let ty = match tyc with
Some ty -> ty
| None -> CAst.make @@ CHole (None, IntroAnonymous, None) in
@@ -440,10 +440,10 @@ GRAMMAR EXTEND Gram
] ]
;
fixannot:
- [ [ "{"; IDENT "struct"; id=identref; "}" -> { (Some id, CStructRec) }
- | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> { (id, CWfRec rel) }
+ [ [ "{"; IDENT "struct"; id=identref; "}" -> { CStructRec id }
+ | "{"; IDENT "wf"; rel=constr; id=identref; "}" -> { CWfRec(id,rel) }
| "{"; IDENT "measure"; m=constr; id=OPT identref;
- rel=OPT constr; "}" -> { (id, CMeasureRec (m,rel)) }
+ rel=OPT constr; "}" -> { CMeasureRec (id,m,rel) }
] ]
;
impl_name_head:
@@ -452,9 +452,9 @@ GRAMMAR EXTEND Gram
binders_fixannot:
[ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot ->
{ (assum na :: fst bl), snd bl }
- | f = fixannot -> { [], f }
+ | f = fixannot -> { [], Some (CAst.make ~loc f) }
| b = binder; bl = binders_fixannot -> { b @ fst bl, snd bl }
- | -> { [], (None, CStructRec) }
+ | -> { [], None }
] ]
;
open_binders:
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 5d8897cb47..84d19730fa 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -191,7 +191,7 @@ module Constr :
val binder : local_binder_expr list Entry.t (* closed_binder or variable *)
val binders : local_binder_expr list Entry.t (* list of binder *)
val open_binders : local_binder_expr list Entry.t
- val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Entry.t
+ val binders_fixannot : (local_binder_expr list * recursion_order_expr CAst.t option) Entry.t
val typeclass_constraint : (lname * bool * constr_expr) Entry.t
val record_declaration : constr_expr Entry.t
val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 4e8cf80ed2..a3973732ad 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -179,8 +179,10 @@ let () =
VERNAC COMMAND EXTEND Function
| ![ proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
=> { let hard = List.exists (function
- | _,((_,(_,(CMeasureRec _|CWfRec _)),_,_,_),_) -> true
- | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
+ | _,((_,(Some { CAst.v = CMeasureRec _ }
+ | Some { CAst.v = CWfRec _}),_,_,_),_) -> true
+ | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_)
+ | _,((_,None,_,_,_),_) -> false) recsl in
match
Vernac_classifier.classify_vernac
(Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e582362e25..6494e90a03 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -469,11 +469,6 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
CAst.(with_val (fun x -> x))
(Constrexpr_ops.names_of_local_assums args)
in
- match wf_arg with
- | None ->
- if Int.equal (List.length names) 1 then 1
- else error "Recursive argument must be specified"
- | Some wf_arg ->
List.index Name.equal (Name wf_arg) names
in
let unbounded_eq =
@@ -575,7 +570,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
in
wf_rel_with_mes,false
in
- register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes (Some wf_arg)
+ register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg
using_lemmas args ret_type body
let map_option f = function
@@ -623,15 +618,15 @@ and rebuild_nal aux bk bl' nal typ =
let rebuild_bl aux bl typ = rebuild_bl aux bl typ
let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
- let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in
+ let fixl,ntns = ComFixpoint.extract_fixpoint_components ~structonly:false fixpoint_exprl in
let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in
let constr_expr_typel =
with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
let fixpoint_exprl_with_new_bl =
- List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ ->
+ List.map2 (fun ((lna,rec_order_opt,bl,ret_typ,opt_body),notation_list) fix_typ ->
let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in
- (((lna,(rec_arg_opt,rec_order),new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+ (((lna,rec_order_opt,new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
)
fixpoint_exprl constr_expr_typel
in
@@ -643,7 +638,7 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive
List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl;
let pstate, _is_struct =
match fixpoint_exprl with
- | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] ->
+ | [((_,Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)},_,_,_),_) as fixpoint_expr] ->
let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
@@ -665,9 +660,9 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive
true
in
if register_built
- then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, false
+ then register_wf name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false
else pstate, false
- |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] ->
+ |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] ->
let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
| [e] -> e
@@ -692,9 +687,9 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive
then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true
else pstate, true
| _ ->
- List.iter (function ((_na,(_,ord),_args,_body,_type),_not) ->
+ List.iter (function ((_na,ord,_args,_body,_type),_not) ->
match ord with
- | Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _ ->
+ | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } ->
error
("Cannot use mutual definition with well-founded recursion or measure")
| _ -> ()
@@ -869,38 +864,42 @@ let make_graph ~pstate (f_ref : GlobRef.t) =
)
()
in
- let (nal_tas,b,t) = get_args extern_body extern_type in
- let expr_list =
- match b.CAst.v with
- | Constrexpr.CFix(l_id,fixexprl) ->
- let l =
- List.map
- (fun (id,(n,recexp),bl,t,b) ->
- let { CAst.loc; v=rec_id } = Option.get n in
- let new_args =
- List.flatten
- (List.map
- (function
- | Constrexpr.CLocalDef (na,_,_)-> []
- | Constrexpr.CLocalAssum (nal,_,_) ->
- List.map
- (fun {CAst.loc;v=n} -> CAst.make ?loc @@
- CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None))
- nal
- | Constrexpr.CLocalPattern _ -> assert false
- )
- nal_tas
- )
- in
- let b' = add_args id.CAst.v new_args b in
- ((((id,None), ( Some CAst.(make rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
- )
- fixexprl
- in
- l
+ let (nal_tas,b,t) = get_args extern_body extern_type in
+ let expr_list =
+ match b.CAst.v with
+ | Constrexpr.CFix(l_id,fixexprl) ->
+ let l =
+ List.map
+ (fun (id,recexp,bl,t,b) ->
+ let { CAst.loc; v=rec_id } = match Option.get recexp with
+ | { CAst.v = CStructRec id } -> id
+ | { CAst.v = CWfRec (id,_) } -> id
+ | { CAst.v = CMeasureRec (oid,_,_) } -> Option.get oid
+ in
+ let new_args =
+ List.flatten
+ (List.map
+ (function
+ | Constrexpr.CLocalDef (na,_,_)-> []
+ | Constrexpr.CLocalAssum (nal,_,_) ->
+ List.map
+ (fun {CAst.loc;v=n} -> CAst.make ?loc @@
+ CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None))
+ nal
+ | Constrexpr.CLocalPattern _ -> assert false
+ )
+ nal_tas
+ )
+ in
+ let b' = add_args id.CAst.v new_args b in
+ ((((id,None), ( Some (CAst.make (CStructRec (CAst.make rec_id)))),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+ )
+ fixexprl
+ in
+ l
| _ ->
let id = Label.to_id (Constant.label c) in
- [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
+ [((CAst.make id,None),None,nal_tas,t,Some b),[]]
in
let mp = Constant.modpath c in
let pstate = do_generate_principle ~pstate [c,Univ.Instance.empty] error_error false false expr_list in
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 7cd62f4ead..f44962f213 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1200,7 +1200,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
| [BFcast], { v = CCast (c, Glob_term.CastConv t) } ->
[Bcast t], c
| BFrec (has_str, has_cast) :: h,
- { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } ->
+ { v = CFix ( _, [_, Some {CAst.v = CStructRec locn}, bl, t, c]) } ->
let bs = format_local_binders h bl in
let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in
bs @ bstr @ (if has_cast then [Bcast t] else []), c
@@ -1424,7 +1424,7 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS (ident * ssrfwd) PRINTED BY { pr_ssrfixfwd }
| [] -> CErrors.user_err (Pp.str "Bad structural argument") in
loop (names_of_local_assums lb) in
let h' = BFrec (has_struct, has_cast) :: binders_fmts bs in
- let fix = CAst.make ~loc @@ CFix (lid, [lid, (Some i, CStructRec), lb, t', c']) in
+ let fix = CAst.make ~loc @@ CFix (lid, [lid, (Some (CAst.make (CStructRec i))), lb, t', c']) in
id, ((fk, h'), { ac with body = fix }) }
END
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index eaa5736336..062e3ca8b2 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -653,7 +653,7 @@ let detype_fix detype flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
let v = Array.map3
(fun c t i -> share_names detype flags (i+1) [] def_avoid def_env sigma c (lift n t))
bodies tys vn in
- GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
+ GRec(GFix (Array.map (fun i -> Some i) (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/glob_ops.ml b/pretyping/glob_ops.ml
index 6da168711c..85b9faac77 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -106,19 +106,9 @@ let glob_decl_eq f (na1, bk1, c1, t1) (na2, bk2, c2, t2) =
Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
Option.equal f c1 c2 && f t1 t2
-let fix_recursion_order_eq f o1 o2 = match o1, o2 with
- | GStructRec, GStructRec -> true
- | GWfRec c1, GWfRec c2 -> f c1 c2
- | GMeasureRec (c1, o1), GMeasureRec (c2, o2) ->
- f c1 c2 && Option.equal f o1 o2
- | (GStructRec | GWfRec _ | GMeasureRec _), _ -> false
-
-let fix_kind_eq f k1 k2 = match k1, k2 with
+let fix_kind_eq k1 k2 = match k1, k2 with
| GFix (a1, i1), GFix (a2, i2) ->
- let eq (i1, o1) (i2, o2) =
- Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2
- in
- Int.equal i1 i2 && Array.equal eq a1 a2
+ Int.equal i1 i2 && Array.equal (Option.equal Int.equal) a1 a2
| GCoFix i1, GCoFix i2 -> Int.equal i1 i2
| (GFix _ | GCoFix _), _ -> false
@@ -150,7 +140,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
f m1 m2 && Name.equal pat1 pat2 &&
Option.equal f p1 p2 && f c1 c2 && f t1 t2
| GRec (kn1, id1, decl1, t1, c1), GRec (kn2, id2, decl2, t2, c2) ->
- fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 &&
+ fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 &&
Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 &&
Array.equal f c1 c2 && Array.equal f t1 t2
| GSort s1, GSort s2 -> glob_sort_eq s1 s2
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index c57cf88cc6..02cb294f6d 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -41,6 +41,12 @@ type glob_constraint = glob_level * Univ.constraint_type * glob_level
type sort_info = (Libnames.qualid * int) option list
type glob_sort = sort_info glob_sort_gen
+type glob_recarg = int option
+
+and glob_fix_kind =
+ | GFix of (glob_recarg array * int)
+ | GCoFix of int
+
(** Casts *)
type 'a cast_type =
@@ -78,7 +84,7 @@ type 'a glob_constr_r =
(** [GCases(style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *)
| GLetTuple of Name.t list * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g
| GIf of 'a glob_constr_g * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g
- | GRec of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array *
+ | GRec of glob_fix_kind * Id.t array * 'a glob_decl_g list array *
'a glob_constr_g array * 'a glob_constr_g array
| GSort of glob_sort
| GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
@@ -88,15 +94,6 @@ and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g
-and 'a fix_recursion_order_g =
- | GStructRec
- | GWfRec of 'a glob_constr_g
- | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option
-
-and 'a fix_kind_g =
- | GFix of ((int option * 'a fix_recursion_order_g) array * int)
- | GCoFix of int
-
and 'a predicate_pattern_g =
Name.t * (inductive * Name.t list) CAst.t option
(** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *)
@@ -117,9 +114,7 @@ type tomatch_tuples = [ `any ] tomatch_tuples_g
type cases_clause = [ `any ] cases_clause_g
type cases_clauses = [ `any ] cases_clauses_g
type glob_decl = [ `any ] glob_decl_g
-type fix_kind = [ `any ] fix_kind_g
type predicate_pattern = [ `any ] predicate_pattern_g
-type fix_recursion_order = [ `any ] fix_recursion_order_g
type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b29afd1fd2..c788efda48 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -470,17 +470,19 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
PCase (info, pred, pat_of_raw metas vars c, brs)
| GRec (GFix (ln,n), ids, decls, tl, cl) ->
- if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then
- err ?loc (Pp.str "\"struct\" annotation is expected.")
- else
- let ln = Array.map (fst %> Option.get) ln in
- let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
- let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in
- let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in
- let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in
- let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in
- let names = Array.map (fun id -> Name id) ids in
- PFix ((ln,n), (names, tl, cl))
+ let get_struct_arg = function
+ | Some n -> n
+ | None -> err ?loc (Pp.str "\"struct\" annotation is expected.")
+ (* TODO why can't the annotation be omitted? *)
+ in
+ let ln = Array.map get_struct_arg ln in
+ let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
+ let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in
+ let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in
+ let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in
+ let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in
+ let names = Array.map (fun id -> Name id) ids in
+ PFix ((ln,n), (names, tl, cl))
| GRec (GCoFix n, ids, decls, tl, cl) ->
let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0f7676cd19..48d981082c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -607,10 +607,10 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env
fixpoints ?) *)
let possible_indexes =
Array.to_list (Array.mapi
- (fun i (n,_) -> match n with
+ (fun i annot -> match annot with
| Some n -> [n]
| None -> List.map_i (fun i _ -> i) 0 ctxtv.(i))
- vn)
+ vn)
in
let fixdecls = (names,ftys,fdefs) in
let indexes = esearch_guard ?loc !!env sigma possible_indexes fixdecls in
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 0ae3de7321..4dc3ba8789 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -399,12 +399,12 @@ let tag_var = tag Tag.variable
pr_opt_type_spc pr t ++ str " :=" ++
pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
- let pr_guard_annot pr_aux bl (n,ro) =
- match n with
+ let pr_guard_annot pr_aux bl ro =
+ match ro with
| None -> mt ()
- | Some {loc; v = id} ->
+ | Some {loc; v = ro} ->
match (ro : Constrexpr.recursion_order_expr) with
- | CStructRec ->
+ | CStructRec { v = id } ->
let names_of_binder = function
| CLocalAssum (nal,_,_) -> nal
| CLocalDef (_,_,_) -> []
@@ -413,10 +413,11 @@ let tag_var = tag Tag.variable
if List.length ids > 1 then
spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}"
else mt()
- | CWfRec c ->
- spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_id id ++ str"}"
- | CMeasureRec (m,r) ->
- spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ spc() ++ pr_id id++
+ | CWfRec (id,c) ->
+ spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_lident id ++ str"}"
+ | CMeasureRec (id,m,r) ->
+ spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++
+ match id with None -> mt() | Some id -> spc () ++ pr_lident id ++
(match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}"
let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) =
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index db1687a49b..2e00b12899 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -37,7 +37,7 @@ val pr_glob_level : Glob_term.glob_level -> Pp.t
val pr_glob_sort : Glob_term.glob_sort -> Pp.t
val pr_guard_annot : (constr_expr -> Pp.t) ->
local_binder_expr list ->
- lident option * recursion_order_expr ->
+ recursion_order_expr CAst.t option ->
Pp.t
val pr_record_body : (qualid * constr_expr) list -> Pp.t
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index d042a1d650..f378a5d2dd 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -438,18 +438,18 @@ let match_goals ot nt =
| _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (2)")
in
let recursion_order_expr ogname exp exp2 =
- match exp, exp2 with
- | CStructRec, CStructRec -> ()
- | CWfRec c, CWfRec c2 ->
+ match exp.CAst.v, exp2.CAst.v with
+ | CStructRec _, CStructRec _ -> ()
+ | CWfRec (_,c), CWfRec (_,c2) ->
constr_expr ogname c c2
- | CMeasureRec (m,r), CMeasureRec (m2,r2) ->
+ | CMeasureRec (_,m,r), CMeasureRec (_,m2,r2) ->
constr_expr ogname m m2;
constr_expr_opt ogname r r2
| _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (3)")
in
let fix_expr ogname exp exp2 =
- let (l,(lo,ro),lb,ce1,ce2), (l2,(lo2,ro2),lb2,ce12,ce22) = exp,exp2 in
- recursion_order_expr ogname ro ro2;
+ let (l,ro,lb,ce1,ce2), (l2,ro2,lb2,ce12,ce22) = exp,exp2 in
+ Option.iter2 (recursion_order_expr ogname) ro ro2;
iter2 (local_binder_expr ogname) lb lb2;
constr_expr ogname ce1 ce12;
constr_expr ogname ce2 ce22
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 2aadbd224f..1912646ffd 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -329,16 +329,27 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c
List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
pstate
-let extract_decreasing_argument limit = function
- | (na,CStructRec) -> na
- | (na,_) when not limit -> na
+let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with
+ | CStructRec na -> na
+ | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na
+ | CMeasureRec (None,_,_) when not structonly ->
+ user_err Pp.(str "Decreasing argument must be specificed in measure clause.")
| _ -> user_err Pp.(str
- "Only structural decreasing is supported for a non-Program Fixpoint")
+ "Well-founded induction requires Program Fixpoint or Function.")
-let extract_fixpoint_components limit l =
+let extract_fixpoint_components ~structonly l =
let fixl, ntnl = List.split l in
let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) ->
- let ann = extract_decreasing_argument limit ann in
+ (* This is a special case: if there's only one binder, we pick it as the
+ recursive argument if none is provided. *)
+ let ann = Option.map (fun ann -> match bl, ann with
+ | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
+ CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
+ | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
+ CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
+ | _, x -> x) ann
+ in
+ let ann = Option.map (extract_decreasing_argument ~structonly) ann in
{fix_name = id; fix_annot = ann; fix_univs = pl;
fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
fixl, List.flatten ntnl
@@ -356,7 +367,7 @@ let check_safe () =
flags.check_universes && flags.check_guarded
let do_fixpoint ~ontop local poly l =
- let fixl, ntns = extract_fixpoint_components true l in
+ let fixl, ntns = extract_fixpoint_components ~structonly:true l in
let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
let possible_indexes =
List.map compute_possible_guardness_evidences info in
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 15ff5f4498..5937842f17 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -62,7 +62,7 @@ val interp_recursive :
(** Extracting the semantical components out of the raw syntax of
(co)fixpoints declarations *)
-val extract_fixpoint_components : bool ->
+val extract_fixpoint_components : structonly:bool ->
(fixpoint_expr * decl_notation list) list ->
structured_fixpoint_expr list * decl_notation list
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 350b2d2945..20a2db7ca2 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -85,7 +85,7 @@ let rec telescope sigma l =
let nf_evar_context sigma ctx =
List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
-let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
+let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
let open EConstr in
let open Vars in
let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
@@ -304,22 +304,26 @@ let do_program_recursive local poly fixkind fixl ntns =
let do_program_fixpoint local poly l =
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
match g, l with
- | [(n, CWfRec r)], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
- let recarg =
- match n with
- | Some n -> mkIdentC n.CAst.v
- | None ->
- user_err ~hdr:"do_program_fixpoint"
- (str "Recursive argument required for well-founded fixpoints")
- in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn
+ | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
+ let recarg = mkIdentC n.CAst.v in
+ build_wellfounded (id, pl, bl, typ, out_def def) poly r recarg ntn
- | [(n, CMeasureRec (m, r))], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
- build_wellfounded (id, pl, n, bl, typ, out_def def) poly
+ | [Some { CAst.v = CMeasureRec (n, m, r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
+ (* We resolve here a clash between the syntax of Program Fixpoint and the one of funind *)
+ let r = match n, r with
+ | Some id, None ->
+ let loc = id.CAst.loc in
+ Some (CAst.make ?loc @@ CRef(qualid_of_ident ?loc id.CAst.v,None))
+ | Some _, Some _ ->
+ user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.")
+ | _, _ -> r
+ in
+ build_wellfounded (id, pl, bl, typ, out_def def) poly
(Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn
- | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
- let fixl,ntns = extract_fixpoint_components true l in
- let fixkind = Obligations.IsFixpoint g in
+ | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
+ let fixl,ntns = extract_fixpoint_components ~structonly:true l in
+ let fixkind = Obligations.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in
do_program_recursive local poly fixkind fixl ntns
| _, _ ->
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 07194578c1..1b1c618dc7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -295,7 +295,7 @@ type obligation =
type obligations = (obligation array * int)
type fixpoint_kind =
- | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of lident option list
| IsCoFixpoint
type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -486,7 +486,7 @@ let rec lam_index n t acc =
lam_index n b (succ acc)
| _ -> raise Not_found
-let compute_possible_guardness_evidences (n,_) fixbody fixtype =
+let compute_possible_guardness_evidences n fixbody fixtype =
match n with
| Some { CAst.loc; v = n } -> [lam_index n fixbody 0]
| None ->
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index b1b7b1ec90..d25daeed9c 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -70,7 +70,7 @@ type notations =
(lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
type fixpoint_kind =
- | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
+ | IsFixpoint of lident option list
| IsCoFixpoint
val add_mutual_definitions :
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index ebfc473522..8eacaed2eb 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -129,7 +129,7 @@ type definition_expr =
* constr_expr option
type fixpoint_expr =
- ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option
+ ident_decl * recursion_order_expr CAst.t option * local_binder_expr list * constr_expr * constr_expr option
type cofixpoint_expr =
ident_decl * local_binder_expr list * constr_expr * constr_expr option
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:37:02 +0000