diff options
| -rw-r--r-- | plugins/funind/g_indfun.mlg | 10 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 295 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 7 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 8 | ||||
| -rw-r--r-- | vernac/comFixpoint.ml | 71 | ||||
| -rw-r--r-- | vernac/comFixpoint.mli | 51 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 36 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.mli | 4 | ||||
| -rw-r--r-- | vernac/declareObl.ml | 5 | ||||
| -rw-r--r-- | vernac/declareObl.mli | 5 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 16 | ||||
| -rw-r--r-- | vernac/obligations.mli | 2 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 22 | ||||
| -rw-r--r-- | vernac/ppvernac.mli | 2 | ||||
| -rw-r--r-- | vernac/pvernac.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 8 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 21 |
17 files changed, 278 insertions, 287 deletions
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 5f859b3e4b..a7ef5fe884 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -148,7 +148,7 @@ END module Vernac = Pvernac.Vernac_ module Tactic = Pltac -type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located +type function_rec_definition_loc_argtype = Vernacexpr.fixpoint_expr Loc.located let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) = Genarg.create_arg "function_rec_definition_loc" @@ -175,10 +175,10 @@ let () = let is_proof_termination_interactively_checked recsl = List.exists (function - | _,((_,( Some { CAst.v = CMeasureRec _ } - | Some { CAst.v = CWfRec _}),_,_,_),_) -> true - | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_) - | _,((_,None,_,_,_),_) -> false) recsl + | _,( Vernacexpr.{ rec_order = Some { CAst.v = CMeasureRec _ } } + | Vernacexpr.{ rec_order = Some { CAst.v = CWfRec _} }) -> true + | _, Vernacexpr.{ rec_order = Some { CAst.v = CStructRec _ } } + | _, Vernacexpr.{ rec_order = None } -> false) recsl let classify_as_Fixpoint recsl = Vernac_classifier.classify_vernac diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6e19ef4804..aaaf7d5ce7 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -157,17 +157,16 @@ let interp_casted_constr_with_implicits env sigma impls c = and not as a constr *) -let build_newrecursive - lnameargsardef = +let build_newrecursive lnameargsardef = let env0 = Global.env() in let sigma = Evd.from_env env0 in let (rec_sign,rec_impls) = List.fold_left - (fun (env,impls) (({CAst.v=recname},_),bl,arityc,_) -> - let arityc = Constrexpr_ops.mkCProdN bl arityc in + (fun (env,impls) { Vernacexpr.id_decl=({CAst.v=recname},_); binders; rtype } -> + let arityc = Constrexpr_ops.mkCProdN binders rtype in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evd = Evd.from_env env0 in - let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd binders in let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in let open Context.Named.Declaration in let r = Sorts.Relevant in (* TODO relevance *) @@ -175,26 +174,18 @@ let build_newrecursive (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) - let f (_,bl,_,def) = - let def = abstract_glob_constr def bl in - interp_casted_constr_with_implicits - rec_sign sigma rec_impls def + let f { Vernacexpr.binders; body_def } = + match body_def with + | Some body_def -> + let def = abstract_glob_constr body_def binders in + interp_casted_constr_with_implicits + rec_sign sigma rec_impls def + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in States.with_state_protection (List.map f) lnameargsardef in recdef,rec_impls -let build_newrecursive l = - let l' = List.map - (fun ((fixna,_,bll,ar,body_opt),lnot) -> - match body_opt with - | Some body -> - (fixna,bll,ar,body) - | None -> user_err ~hdr:"Function" (str "Body of Function must be given") - ) l - in - build_newrecursive l' - let error msg = user_err Pp.(str msg) (* Checks whether or not the mutual bloc is recursive *) @@ -237,8 +228,8 @@ let rec local_binders_length = function | Constrexpr.CLocalAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl | Constrexpr.CLocalPattern _::bl -> assert false -let prepare_body ((name,_,args,types,_),_) rt = - let n = local_binders_length args in +let prepare_body { Vernacexpr.id_decl; binders; rtype } rt = + let n = local_binders_length binders in (* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_glob_constr rt); *) let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') @@ -336,13 +327,13 @@ let error_error names e = | _ -> raise e let generate_principle (evd:Evd.evar_map ref) pconstants on_error - is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof + is_general do_built (fix_rec_l : Vernacexpr.fixpoint_expr list) recdefs interactive_proof (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int -> Tacmach.tactic) : unit = - let names = List.map (function (({CAst.v=name},_),_,_,_,_),_ -> name) fix_rec_l in + let names = List.map (function { Vernacexpr.id_decl = {CAst.v=name},_} -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in - let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in + let funs_types = List.map (function { Vernacexpr.rtype } -> rtype) fix_rec_l in try (* We then register the Inductive graphs of the functions *) Glob_term_to_relation.build_inductive !evd pconstants funs_args funs_types recdefs; @@ -359,7 +350,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error locate_ind f_R_mut) in - let fname_kn (((fname,_),_,_,_,_),_) = + let fname_kn { Vernacexpr.id_decl=(fname,_) } = let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in locate_with_msg (pr_qualid f_ref++str ": Not an inductive type!") @@ -398,20 +389,22 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error with e when CErrors.noncritical e -> on_error names e -let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = +let register_struct is_rec (fixpoint_exprl: Vernacexpr.fixpoint_expr list) = match fixpoint_exprl with - | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec -> - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + | [ { Vernacexpr.id_decl=({ CAst.v=fname },pl); binders; rtype; body_def } ] when not is_rec -> + let body = match body_def with + | Some body -> body + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in ComDefinition.do_definition ~program_mode:false ~name:fname ~poly:false ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:Decls.Definition pl - bl None body (Some ret_type); + binders None body (Some rtype); let evd,rev_pconstants = List.fold_left - (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> + (fun (evd,l) { Vernacexpr.id_decl=({CAst.v=fname},_) } -> let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in @@ -427,7 +420,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ComFixpoint.do_fixpoint ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl; let evd,rev_pconstants = List.fold_left - (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> + (fun (evd,l) { Vernacexpr.id_decl=({CAst.v=fname},_) } -> let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in @@ -607,87 +600,91 @@ 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 ~structonly:false fixpoint_exprl in - let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in +let recompute_binder_list fixpoint_exprl = + let fixl = ComFixpoint.extract_fixpoint_components ~structonly:false fixpoint_exprl in + let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl 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_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_order_opt,new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) - ) - fixpoint_exprl constr_expr_typel + List.map2 (fun ({ Vernacexpr.binders } as fp) fix_typ -> + let binders, rtype = rebuild_bl [] binders fix_typ in + { fp with Vernacexpr.binders; rtype } + ) fixpoint_exprl constr_expr_typel in fixpoint_exprl_with_new_bl let do_generate_principle_aux pconstants on_error register_built interactive_proof - (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Lemmas.t option = - List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; + (fixpoint_exprl : Vernacexpr.fixpoint_expr list) : Lemmas.t option = + List.iter (fun { Vernacexpr.notations } -> + if not (List.is_empty notations) + then error "Function does not support notations for now") fixpoint_exprl; let lemma, _is_struct = match fixpoint_exprl with - | [((_,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 - | _ -> assert false - in - let fixpoint_exprl = [fixpoint_expr] in - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - let recdefs,rec_impls = build_newrecursive fixpoint_exprl in - let using_lemmas = [] in - let pre_hook pconstants = - generate_principle - (ref (Evd.from_env (Global.env ()))) - pconstants - on_error - true - register_built - fixpoint_exprl - recdefs - true - in - if register_built - then register_wf interactive_proof name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false - else None, false - |[((_,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 - | _ -> assert false - in - let fixpoint_exprl = [fixpoint_expr] in - let recdefs,rec_impls = build_newrecursive fixpoint_exprl in - let using_lemmas = [] in - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - let pre_hook pconstants = - generate_principle - (ref (Evd.from_env (Global.env ()))) - pconstants - on_error - true - register_built - fixpoint_exprl - recdefs - true - in - if register_built - then register_mes interactive_proof 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 None, true + | [{ Vernacexpr.rec_order = Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)} } as fixpoint_expr] -> + let { Vernacexpr.id_decl = ({CAst.v=name},pl); binders; rtype; body_def } as fixpoint_expr = + match recompute_binder_list [fixpoint_expr] with + | [e] -> e + | _ -> assert false + in + let fixpoint_exprl = [fixpoint_expr] in + let body = match body_def with + | Some body -> body + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let using_lemmas = [] in + let pre_hook pconstants = + generate_principle + (ref (Evd.from_env (Global.env ()))) + pconstants + on_error + true + register_built + fixpoint_exprl + recdefs + true + in + if register_built + then register_wf interactive_proof name rec_impls wf_rel wf_x.CAst.v using_lemmas binders rtype body pre_hook, false + else None, false + |[{ Vernacexpr.rec_order=Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)} } as fixpoint_expr] -> + let { Vernacexpr.id_decl = ({CAst.v=name},pl); binders; rtype; body_def} as fixpoint_expr = + match recompute_binder_list [fixpoint_expr] with + | [e] -> e + | _ -> assert false + in + let fixpoint_exprl = [fixpoint_expr] in + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let using_lemmas = [] in + let body = match body_def with + | Some body -> body + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + let pre_hook pconstants = + generate_principle + (ref (Evd.from_env (Global.env ()))) + pconstants + on_error + true + register_built + fixpoint_exprl + recdefs + true + in + if register_built + then register_mes interactive_proof name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas binders rtype body pre_hook, true + else None, true | _ -> - List.iter (function ((_na,ord,_args,_body,_type),_not) -> - match ord with - | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } -> - error - ("Cannot use mutual definition with well-founded recursion or measure") - | _ -> () + List.iter (function { Vernacexpr.rec_order } -> + match rec_order with + | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } -> + error + ("Cannot use mutual definition with well-founded recursion or measure") + | _ -> () ) fixpoint_exprl; let fixpoint_exprl = recompute_binder_list fixpoint_exprl in let fix_names = - List.map (function ((({CAst.v=name},_),_,_,_,_),_) -> name) fixpoint_exprl + List.map (function { Vernacexpr.id_decl=({CAst.v=name},_) } -> name) fixpoint_exprl in (* ok all the expressions are structural *) let recdefs,rec_impls = build_newrecursive fixpoint_exprl in @@ -845,59 +842,59 @@ let make_graph (f_ref : GlobRef.t) = | None -> error "Cannot build a graph over an axiom!" | Some (body, _, _) -> let env = Global.env () in - let extern_body,extern_type = - with_full_print (fun () -> - (Constrextern.extern_constr false env sigma (EConstr.of_constr body), - Constrextern.extern_type false env sigma - (EConstr.of_constr (*FIXME*) c_body.const_type) - ) + let extern_body,extern_type = + with_full_print (fun () -> + (Constrextern.extern_constr false env sigma (EConstr.of_constr body), + Constrextern.extern_type false env sigma + (EConstr.of_constr (*FIXME*) c_body.const_type) ) - () - 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,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 + 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 - l - | _ -> - let id = Label.to_id (Constant.label c) in - [((CAst.make id,None),None,nal_tas,t,Some b),[]] - in - let mp = Constant.modpath c in - let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error false false expr_list in - assert (Option.is_empty pstate); - (* We register the infos *) - List.iter - (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) - expr_list) + let b' = add_args id.CAst.v new_args b in + { Vernacexpr.id_decl=(id,None) + ; rec_order = Some (CAst.make (CStructRec (CAst.make rec_id))) + ; binders = nal_tas@bl; rtype=t; body_def=Some b'; notations = []} + ) fixexprl in + l + | _ -> + let id = Label.to_id (Constant.label c) in + [{ Vernacexpr.id_decl=(CAst.make id,None); rec_order = None; binders=nal_tas; rtype=t; body_def=Some b; notations=[]}] + in + let mp = Constant.modpath c in + let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error false false expr_list in + assert (Option.is_empty pstate); + (* We register the infos *) + List.iter + (fun { Vernacexpr.id_decl=({CAst.v=id},_) } -> + add_Function false (Constant.make2 mp (Label.of_id id))) + expr_list) (* *************** statically typed entrypoints ************************* *) diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 3bc52272ac..bfc9686ae5 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -5,12 +5,9 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit -val do_generate_principle : - (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit +val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit -val do_generate_principle_interactive : - (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - Lemmas.t +val do_generate_principle_interactive : Vernacexpr.fixpoint_expr list -> Lemmas.t val functional_induction : bool -> diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index aaba36287a..11ff6e9df9 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -106,8 +106,8 @@ let classify_vernac e = else GuaranteesOpacity in let ids, open_proof = - List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) -> - id::l, b || p = None) ([],false) l in + List.fold_left (fun (l,b) {Vernacexpr.id_decl=({CAst.v=id},_); body_def} -> + id::l, b || body_def = None) ([],false) l in if open_proof then VtStartProof (guarantee,ids) else VtSideff (ids, VtLater) @@ -118,8 +118,8 @@ let classify_vernac e = else GuaranteesOpacity in let ids, open_proof = - List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) -> - id::l, b || p = None) ([],false) l in + List.fold_left (fun (l,b) { Vernacexpr.id_decl=({CAst.v=id},_); body_def } -> + id::l, b || body_def = None) ([],false) l in if open_proof then VtStartProof (guarantee,ids) else VtSideff (ids, VtLater) diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 3f13d772ab..b7da4f964d 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -107,14 +107,15 @@ let check_mutuality env evd isfix fixl = warn_non_full_mutual (x,xge,y,yge,isfix,rest) | _ -> () -type structured_fixpoint_expr = { - fix_name : Id.t; - fix_univs : universe_decl_expr option; - fix_annot : lident option; - fix_binders : local_binder_expr list; - fix_body : constr_expr option; - fix_type : constr_expr -} +type structured_fixpoint_expr = + { fix_name : Id.t + ; fix_univs : Constrexpr.universe_decl_expr option + ; fix_annot : lident option + ; fix_binders : local_binder_expr list + ; fix_body : constr_expr option + ; fix_type : constr_expr + ; fix_notations : Vernacexpr.decl_notation list + } let interp_fix_context ~program_mode ~cofix env sigma fix = let before, after = if not cofix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in @@ -167,7 +168,7 @@ type recursive_preentry = let fix_proto sigma = Evarutil.new_global sigma (Coqlib.lib_ref "program.tactic.fix_proto") -let interp_recursive ~program_mode ~cofix fixl notations = +let interp_recursive ~program_mode ~cofix fixl = let open Context.Named.Declaration in let open EConstr in let env = Global.env() in @@ -222,6 +223,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = (* Interp bodies with rollback because temp use of notations/implicit *) let sigma, fixdefs = Metasyntax.with_syntax_protection (fun () -> + let notations = List.map_append (fun { fix_notations } -> fix_notations) fixl in List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations; List.fold_left4_map (fun sigma fixctximpenv -> interp_fix_body ~program_mode env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls)) @@ -248,8 +250,8 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) = let fixtypes = List.map EConstr.(to_constr evd) fixtypes in Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes) -let interp_fixpoint ~cofix l ntns = - let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l ntns in +let interp_fixpoint ~cofix l = + let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in check_recursive true env evd fix; let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) @@ -317,28 +319,25 @@ let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v "Well-founded induction requires Program Fixpoint or Function.") 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 open Vernacexpr in + List.map (fun { id_decl=({CAst.v=id},pl); rec_order; binders; rtype; body_def; notations } -> (* 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 + recursive argument if none is provided. *) + let rec_order = Option.map (fun rec_order -> match binders, rec_order 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) rec_order 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 + let rec_order = Option.map (extract_decreasing_argument ~structonly) rec_order in + { fix_name = id; fix_annot = rec_order; fix_univs = pl; + fix_binders = binders; fix_body = body_def; fix_type = rtype; fix_notations = notations }) l let extract_cofixpoint_components l = - let fixl, ntnl = List.split l in - List.map (fun (({CAst.v=id},pl),bl,typ,def) -> - {fix_name = id; fix_annot = None; fix_univs = pl; - fix_binders = bl; fix_body = def; fix_type = typ}) fixl, - List.flatten ntnl + List.map (fun { Vernacexpr.id_decl=({CAst.v=id},pl); binders; rtype; body_def; notations} -> + {fix_name = id; fix_annot = None; fix_univs = pl; + fix_binders = binders; fix_body = body_def; fix_type = rtype; fix_notations = notations}) l let check_safe () = let open Declarations in @@ -346,8 +345,9 @@ let check_safe () = flags.check_universes && flags.check_guarded let do_fixpoint_common l = - let fixl, ntns = extract_fixpoint_components ~structonly:true l in - let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in + let fixl = extract_fixpoint_components ~structonly:true l in + let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl in + let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl in fixl, ntns, fix, List.map compute_possible_guardness_evidences info let do_fixpoint_interactive ~scope ~poly l : Lemmas.t = @@ -362,16 +362,17 @@ let do_fixpoint ~scope ~poly l = if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () let do_cofixpoint_common l = - let fixl,ntns = extract_cofixpoint_components l in - ntns, interp_fixpoint ~cofix:true fixl ntns + let fixl = extract_cofixpoint_components l in + let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl in + interp_fixpoint ~cofix:true fixl, ntns let do_cofixpoint_interactive ~scope ~poly l = - let ntns, cofix = do_cofixpoint_common l in + let cofix, ntns = do_cofixpoint_common l in let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); lemma let do_cofixpoint ~scope ~poly l = - let ntns, cofix = do_cofixpoint_common l in + let cofix, ntns = do_cofixpoint_common l in declare_fixpoint_generic ~scope ~poly cofix ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 982d316605..1018c463c6 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -18,29 +18,30 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint_interactive : - scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> Lemmas.t + scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t val do_fixpoint : - scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint_interactive : - scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t + scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t val do_cofixpoint : - scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit (************************************************************************) (** Internal API *) (************************************************************************) -type structured_fixpoint_expr = { - fix_name : Id.t; - fix_univs : Constrexpr.universe_decl_expr option; - fix_annot : lident option; - fix_binders : local_binder_expr list; - fix_body : constr_expr option; - fix_type : constr_expr -} +type structured_fixpoint_expr = + { fix_name : Id.t + ; fix_univs : Constrexpr.universe_decl_expr option + ; fix_annot : lident option + ; fix_binders : local_binder_expr list + ; fix_body : constr_expr option + ; fix_type : constr_expr + ; fix_notations : decl_notation list + } (** Typing global fixpoints and cofixpoint_expr *) @@ -49,8 +50,7 @@ val interp_recursive : (* Misc arguments *) program_mode:bool -> cofix:bool -> (* Notations of the fixpoint / should that be folded in the previous argument? *) - structured_fixpoint_expr list -> decl_notation list -> - + structured_fixpoint_expr list -> (* env / signature / univs / evar_map *) (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (* names / defs / types *) @@ -63,22 +63,19 @@ val interp_recursive : (** Extracting the semantical components out of the raw syntax of (co)fixpoints declarations *) -val extract_fixpoint_components : structonly:bool -> - (fixpoint_expr * decl_notation list) list -> - structured_fixpoint_expr list * decl_notation list +val extract_fixpoint_components + : structonly:bool -> fixpoint_expr list -> structured_fixpoint_expr list -val extract_cofixpoint_components : - (cofixpoint_expr * decl_notation list) list -> - structured_fixpoint_expr list * decl_notation list +val extract_cofixpoint_components + : cofixpoint_expr list -> structured_fixpoint_expr list -type recursive_preentry = - Id.t list * Sorts.relevance list * constr option list * types list +type recursive_preentry = Id.t list * Sorts.relevance list * constr option list * types list -val interp_fixpoint : - cofix:bool -> - structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * UState.universe_decl * UState.t * - (EConstr.rel_context * Impargs.manual_implicits * int option) list +val interp_fixpoint + : cofix:bool + -> structured_fixpoint_expr list + -> recursive_preentry * UState.universe_decl * UState.t * + (EConstr.rel_context * Impargs.manual_implicits * int option) list (** Very private function, do not use *) val compute_possible_guardness_evidences : diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 0fd65ad9b4..0104c99e41 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -244,10 +244,10 @@ let collect_evars_of_term evd c ty = Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) -let do_program_recursive ~scope ~poly fixkind fixl ntns = +let do_program_recursive ~scope ~poly fixkind fixl = let cofix = fixkind = DeclareObl.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = - interp_recursive ~cofix ~program_mode:true fixl ntns + interp_recursive ~cofix ~program_mode:true fixl in (* Program-specific code *) (* Get the interesting evars, those that were not instantiated *) @@ -289,16 +289,19 @@ let do_program_recursive ~scope ~poly fixkind fixl ntns = | DeclareObl.IsFixpoint _ -> Decls.Fixpoint | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint in + let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl in Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind let do_program_fixpoint ~scope ~poly l = - let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in + let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in match g, l with - | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> + | [Some { CAst.v = CWfRec (n,r) }], + [ Vernacexpr.{id_decl=({CAst.v=id},pl);binders;rtype;body_def;notations} ] -> let recarg = mkIdentC n.CAst.v in - build_wellfounded (id, pl, bl, typ, out_def def) poly r recarg ntn + build_wellfounded (id, pl, binders, rtype, out_def body_def) poly r recarg notations - | [Some { CAst.v = CMeasureRec (n, m, r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> + | [Some { CAst.v = CMeasureRec (n, m, r) }], + [Vernacexpr.{id_decl=({CAst.v=id},pl); binders; rtype; body_def; notations }] -> (* 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 -> @@ -308,25 +311,18 @@ let do_program_fixpoint ~scope ~poly l = 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 + build_wellfounded (id, pl, binders, rtype, out_def body_def) poly + (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations | _, _ 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 = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in - do_program_recursive ~scope ~poly fixkind fixl ntns + let fixl = extract_fixpoint_components ~structonly:true l in + let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in + do_program_recursive ~scope ~poly fixkind fixl | _, _ -> user_err ~hdr:"do_program_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") -let extract_cofixpoint_components l = - let fixl, ntnl = List.split l in - List.map (fun (({CAst.v=id},pl),bl,typ,def) -> - {fix_name = id; fix_annot = None; fix_univs = pl; - fix_binders = bl; fix_body = def; fix_type = typ}) fixl, - List.flatten ntnl - let check_safe () = let open Declarations in let flags = Environ.typing_flags (Global.env ()) in @@ -337,6 +333,6 @@ let do_fixpoint ~scope ~poly l = if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () let do_cofixpoint ~scope ~poly l = - let fixl,ntns = extract_cofixpoint_components l in - do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl ntns; + let fixl = extract_cofixpoint_components l in + do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli index f25abb95c3..fa3d2b7020 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -4,8 +4,8 @@ open Vernacexpr val do_fixpoint : (* When [false], assume guarded. *) - scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint : (* When [false], assume guarded. *) - scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 0c45ff11d7..c5cbb095ca 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -29,9 +29,6 @@ type obligation = type obligations = obligation array * int -type notations = - (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list - type fixpoint_kind = | IsFixpoint of lident option list | IsCoFixpoint @@ -46,7 +43,7 @@ type program_info = ; prg_deps : Id.t list ; prg_fixkind : fixpoint_kind option ; prg_implicits : Impargs.manual_implicits - ; prg_notations : notations + ; prg_notations : Vernacexpr.decl_notation list ; prg_poly : bool ; prg_scope : DeclareDef.locality ; prg_kind : Decls.definition_object_kind diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index a8dd5040cb..2a8fa734b3 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -24,9 +24,6 @@ type obligation = type obligations = obligation array * int -type notations = - (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list - type fixpoint_kind = | IsFixpoint of lident option list | IsCoFixpoint @@ -41,7 +38,7 @@ type program_info = ; prg_deps : Id.t list ; prg_fixkind : fixpoint_kind option ; prg_implicits : Impargs.manual_implicits - ; prg_notations : notations + ; prg_notations : Vernacexpr.decl_notation list ; prg_poly : bool ; prg_scope : DeclareDef.locality ; prg_kind : Decls.definition_object_kind diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 2b475f1ef9..678d4436d2 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -402,16 +402,18 @@ GRAMMAR EXTEND Gram ; (* (co)-fixpoints *) rec_definition: - [ [ id = ident_decl; + [ [ id_decl = ident_decl; bl = binders_fixannot; - ty = type_cstr; - def = OPT [":="; def = lconstr -> { def } ]; ntn = decl_notation -> - { let bl, annot = bl in ((id,annot,bl,ty,def),ntn) } ] ] + rtype = type_cstr; + body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation -> + { let binders, rec_order = bl in + {id_decl; rec_order; binders; rtype; body_def; notations} + } ] ] ; corec_definition: - [ [ id = ident_decl; bl = binders; ty = type_cstr; - def = OPT [":="; def = lconstr -> { def }]; ntn = decl_notation -> - { ((id,bl,ty,def),ntn) } ] ] + [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr; + body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation -> + { {id_decl; rec_order=(); binders; rtype; body_def; notations} } ] ] ; type_cstr: [ [ ":"; c=lconstr -> { c } diff --git a/vernac/obligations.mli b/vernac/obligations.mli index f97bc784c3..e5facd5fb6 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -69,7 +69,7 @@ val add_mutual_definitions -> ?kind:Decls.definition_object_kind -> ?reduce:(constr -> constr) -> ?hook:DeclareDef.Hook.t -> ?opaque:bool - -> DeclareObl.notations + -> Vernacexpr.decl_notation list -> DeclareObl.fixpoint_kind -> unit val obligation diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index e676fe94db..835f5e0b75 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -419,15 +419,15 @@ let string_of_theorem_kind = let open Decls in function | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") - let pr_rec_definition ((iddecl,ro,bl,type_,def),ntn) = + let pr_rec_definition { id_decl; rec_order; binders; rtype; body_def; notations } = let env = Global.env () in let sigma = Evd.from_env env in let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in - let annot = pr_guard_annot (pr_lconstr_expr env sigma) bl ro in - pr_ident_decl iddecl ++ pr_binders_arg bl ++ annot - ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) type_ - ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) def - ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn + let annot = pr_guard_annot (pr_lconstr_expr env sigma) binders rec_order in + pr_ident_decl id_decl ++ pr_binders_arg binders ++ annot + ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) rtype + ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) body_def + ++ prlist (pr_decl_notation @@ pr_constr env sigma) notations let pr_statement head (idpl,(bl,c)) = let env = Global.env () in @@ -858,11 +858,11 @@ let string_of_definition_object_kind = let open Decls in function | DoDischarge -> keyword "Let" ++ spc () | NoDischarge -> str "" in - let pr_onecorec ((iddecl,bl,c,def),ntn) = - pr_ident_decl iddecl ++ spc() ++ pr_binders env sigma bl ++ spc() ++ str":" ++ - spc() ++ pr_lconstr_expr env sigma c ++ - pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) def ++ - prlist (pr_decl_notation @@ pr_constr env sigma) ntn + let pr_onecorec {id_decl; binders; rtype; body_def; notations } = + pr_ident_decl id_decl ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++ + spc() ++ pr_lconstr_expr env sigma rtype ++ + pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) body_def ++ + prlist (pr_decl_notation @@ pr_constr env sigma) notations in return ( hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++ diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli index d4d49a09a3..9ade5afb87 100644 --- a/vernac/ppvernac.mli +++ b/vernac/ppvernac.mli @@ -14,7 +14,7 @@ val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t (** Prints a fixpoint body *) -val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t +val pr_rec_definition : Vernacexpr.fixpoint_expr -> Pp.t (** Prints a vernac expression without dot *) val pr_vernac_expr : Vernacexpr.vernac_expr -> Pp.t diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index c9eb979a90..3bd252ecef 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -23,7 +23,7 @@ module Vernac_ : val command : vernac_expr Entry.t val syntax : vernac_expr Entry.t val vernac_control : vernac_control Entry.t - val rec_definition : (fixpoint_expr * decl_notation list) Entry.t + val rec_definition : fixpoint_expr Entry.t val noedit_mode : vernac_expr Entry.t val command_entry : vernac_expr Entry.t val main_entry : vernac_control option Entry.t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 46ddf214ab..0205a653c5 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -772,7 +772,7 @@ let vernac_inductive ~atts cum lo finite indl = let vernac_fixpoint_common ~atts discharge l = if Dumpglob.dump () then - List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; + List.iter (fun { id_decl = (lid,_) } -> Dumpglob.dump_definition lid false "def") l; enforce_locality_exp atts.DefAttributes.locality discharge let vernac_fixpoint_interactive ~atts discharge l = @@ -793,7 +793,7 @@ let vernac_fixpoint ~atts discharge l = let vernac_cofixpoint_common ~atts discharge l = if Dumpglob.dump () then - List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; + List.iter (fun { id_decl = (lid,_) } -> Dumpglob.dump_definition lid false "def") l; enforce_locality_exp atts.DefAttributes.locality discharge let vernac_cofixpoint_interactive ~atts discharge l = @@ -2358,7 +2358,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacInductive (cum, priv, finite, l) -> VtDefault(fun () -> vernac_inductive ~atts cum priv finite l) | VernacFixpoint (discharge, l) -> - let opens = List.exists (fun ((_,_,_,_,p),_) -> Option.is_empty p) l in + let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in if opens then VtOpenProof (fun () -> with_def_attributes ~atts vernac_fixpoint_interactive discharge l) @@ -2366,7 +2366,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with VtDefault (fun () -> with_def_attributes ~atts vernac_fixpoint discharge l) | VernacCoFixpoint (discharge, l) -> - let opens = List.exists (fun ((_,_,_,p),_) -> Option.is_empty p) l in + let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in if opens then VtOpenProof(fun () -> with_def_attributes ~atts vernac_cofixpoint_interactive discharge l) else diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index ee1f839b8d..8b8123bd30 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -128,18 +128,25 @@ type definition_expr = | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option -type fixpoint_expr = - ident_decl * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr option +type decl_notation = lstring * constr_expr * scope_name option + +type 'a fix_expr_gen = + { id_decl : ident_decl + ; rec_order : 'a + ; binders : local_binder_expr list + ; rtype : constr_expr + ; body_def : constr_expr option + ; notations : decl_notation list + } -type cofixpoint_expr = - ident_decl * local_binder_expr list * constr_expr * constr_expr option +type fixpoint_expr = recursion_order_expr option fix_expr_gen +type cofixpoint_expr = unit fix_expr_gen type local_decl_expr = | AssumExpr of lname * constr_expr | DefExpr of lname * constr_expr * constr_expr option type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *) -type decl_notation = lstring * constr_expr * scope_name option type simple_binder = lident list * constr_expr type class_binder = lident * constr_expr list type 'a with_coercion = coercion_flag * 'a @@ -283,8 +290,8 @@ type nonrec vernac_expr = | VernacAssumption of (discharge * Decls.assumption_object_kind) * Declaremods.inline * (ident_decl list * constr_expr) with_coercion list | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_flag * (inductive_expr * decl_notation list) list - | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list - | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list + | VernacFixpoint of discharge * fixpoint_expr list + | VernacCoFixpoint of discharge * cofixpoint_expr list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list |