aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-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
6 files changed, 41 insertions, 26 deletions
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-03-19 08:21:04 +0000