aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/g_indfun.mlg6
-rw-r--r--plugins/funind/glob_term_to_relation.ml6
-rw-r--r--plugins/funind/glob_termops.ml2
-rw-r--r--plugins/funind/indfun.ml91
-rw-r--r--plugins/funind/plugin_base.dune2
5 files changed, 54 insertions, 53 deletions
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/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 275b58f0aa..45a4e61846 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -317,7 +317,7 @@ let build_constructors_of_type ind' argl =
Impargs.implicits_of_global constructref
in
let cst_narg =
- Inductiveops.constructor_nallargs_env
+ Inductiveops.constructor_nallargs
(Global.env ())
construct
in
@@ -330,7 +330,7 @@ let build_constructors_of_type ind' argl =
let pat_as_term =
mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
in
- cases_pattern_of_glob_constr Anonymous pat_as_term
+ cases_pattern_of_glob_constr (Global.env()) Anonymous pat_as_term
)
ind.Declarations.mind_consnames
@@ -415,7 +415,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function
mkGVar id
| PatCstr(constr,patternl,_) ->
let cst_narg =
- Inductiveops.constructor_nallargs_env
+ Inductiveops.constructor_nallargs
(Global.env ())
constr
in
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 13ff19a46b..7b758da8e8 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -361,7 +361,7 @@ let rec pattern_to_term pt = DAst.with_val (function
mkGVar id
| PatCstr(constr,patternl,_) ->
let cst_narg =
- Inductiveops.constructor_nallargs_env
+ Inductiveops.constructor_nallargs
(Global.env ())
constr
in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a5c19f3217..6494e90a03 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -382,8 +382,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
let _ =
List.map_i
(fun i x ->
- let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in
- let env = Global.env () in
+ let env = Global.env () in
+ let princ = Indrec.lookup_eliminator env (ind_kn,i) (InProp) in
let evd = ref (Evd.from_env env) in
let evd',uprinc = Evd.fresh_global env !evd princ in
let _ = evd := evd' in
@@ -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/funind/plugin_base.dune b/plugins/funind/plugin_base.dune
index 002eb28eea..6ccf15df29 100644
--- a/plugins/funind/plugin_base.dune
+++ b/plugins/funind/plugin_base.dune
@@ -1,5 +1,5 @@
(library
(name recdef_plugin)
- (public_name coq.plugins.recdef)
+ (public_name coq.plugins.funind)
(synopsis "Coq's functional induction plugin")
(libraries coq.plugins.extraction))
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 20:27:06 +0000