From d68f695b5a953c50bcf5e80182ef317682de1a05 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Jul 2019 14:01:38 +0200 Subject: [vernacexpr] Refactor fixpoint AST. We turn the tuples used for (co)-fixpoints into records, cleaning up their users. More cleanup is be possible, in particular a few functions can now shared among co and fixpoints, also `structured_fixpoint_expr` could like be folded into the new record. Feedback on the naming of the records fields is welcome. This is a step towards cleaning up code in `funind`, as it is the main consumer of this data structure, as it does quite a bit of fixpoint manipulation. cc: #6019 --- vernac/comFixpoint.ml | 71 ++++++++++++++++++++++--------------------- vernac/comFixpoint.mli | 51 +++++++++++++++---------------- vernac/comProgramFixpoint.ml | 36 ++++++++++------------ vernac/comProgramFixpoint.mli | 4 +-- vernac/declareObl.ml | 5 +-- vernac/declareObl.mli | 5 +-- vernac/g_vernac.mlg | 16 +++++----- vernac/obligations.mli | 2 +- vernac/ppvernac.ml | 22 +++++++------- vernac/ppvernac.mli | 2 +- vernac/pvernac.mli | 2 +- vernac/vernacentries.ml | 8 ++--- vernac/vernacexpr.ml | 21 ++++++++----- 13 files changed, 121 insertions(+), 124 deletions(-) (limited to 'vernac') 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 -- cgit v1.2.3 From d407d1f3f2f877fca8673eaf0470b3390e55dbaa Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Jul 2019 18:55:05 +0200 Subject: [vernacexpr] Remove duplicate fixpoint record. We continue over the previous commit and remove redundant `structured_fixpoint_expr` record in favor of the one used in the AST. This removes some term-shuffling, tho we still have discrepancies related to adjustments on the recursive annotation. --- vernac/comFixpoint.ml | 74 ++++++++++++++++++------------------------- vernac/comFixpoint.mli | 30 +++++------------- vernac/comProgramFixpoint.ml | 22 +++++++------ vernac/comProgramFixpoint.mli | 10 ++++++ vernac/g_vernac.mlg | 5 +-- vernac/ppvernac.ml | 8 ++--- vernac/vernacentries.ml | 4 +-- vernac/vernacexpr.ml | 3 +- 8 files changed, 71 insertions(+), 85 deletions(-) (limited to 'vernac') diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index b7da4f964d..74c9bc2886 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -107,27 +107,20 @@ 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 : 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 + let before, after = + if not cofix + then split_at_annot fix.Vernacexpr.binders fix.Vernacexpr.rec_order + else [], fix.Vernacexpr.binders in let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in let sigma, (impl_env', ((env'', ctx'), imps')) = interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after in - let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in + let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) let interp_fix_ccl ~program_mode sigma impls (env,_) fix = - let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.fix_type in + let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.Vernacexpr.rtype in let r = Retyping.relevance_of_type env sigma c in sigma, (c, r, impl) @@ -136,7 +129,7 @@ let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl = Option.cata (fun body -> let env = push_rel_context ctx env_rec in let sigma, body = interp_casted_constr_evars ~program_mode env sigma ~impls body ccl in - sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.fix_body + sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.Vernacexpr.body_def let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx @@ -168,16 +161,16 @@ 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 = +let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen list) = let open Context.Named.Declaration in let open EConstr in let env = Global.env() in - let fixnames = List.map (fun fix -> fix.fix_name) fixl in + let fixnames = List.map (fun fix -> fix.Vernacexpr.fname.CAst.v) fixl in (* Interp arities allowing for unresolved types *) let all_universes = List.fold_right (fun sfe acc -> - match sfe.fix_univs , acc with + match sfe.Vernacexpr.univs , acc with | None , acc -> acc | x , None -> x | Some ls , Some us -> @@ -223,7 +216,7 @@ let interp_recursive ~program_mode ~cofix fixl = (* 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 + let notations = List.map_append (fun { Vernacexpr.notations } -> 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)) @@ -318,35 +311,28 @@ let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v | _ -> user_err Pp.(str "Well-founded induction requires Program Fixpoint or Function.") -let extract_fixpoint_components ~structonly l = - 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 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 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 = - 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 +(* This is a special case: if there's only one binder, we pick it as + the recursive argument if none is provided. *) +let adjust_rec_order ~structonly binders rec_order = + 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 + Option.map (extract_decreasing_argument ~structonly) rec_order let check_safe () = let open Declarations in let flags = Environ.typing_flags (Global.env ()) in flags.check_universes && flags.check_guarded -let do_fixpoint_common l = - let fixl = extract_fixpoint_components ~structonly:true l in - let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl in +let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) = + let fixl = List.map (fun fix -> + Vernacexpr.{ fix + with rec_order = adjust_rec_order ~structonly:true fix.binders fix.rec_order }) fixl in + let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl in fixl, ntns, fix, List.map compute_possible_guardness_evidences info @@ -361,9 +347,9 @@ let do_fixpoint ~scope ~poly l = declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () -let do_cofixpoint_common l = - let fixl = extract_cofixpoint_components l in - let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl in +let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) = + let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in + let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in interp_fixpoint ~cofix:true fixl, ntns let do_cofixpoint_interactive ~scope ~poly l = diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 1018c463c6..4f8e9018de 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -10,7 +10,6 @@ open Names open Constr -open Constrexpr open Vernacexpr (** {6 Fixpoints and cofixpoints} *) @@ -33,24 +32,20 @@ val do_cofixpoint : (** 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 - ; fix_notations : decl_notation list - } - (** Typing global fixpoints and cofixpoint_expr *) +val adjust_rec_order + : structonly:bool + -> Constrexpr.local_binder_expr list + -> Constrexpr.recursion_order_expr option + -> lident option + (** Exported for Program *) 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 -> + lident option fix_expr_gen list -> (* env / signature / univs / evar_map *) (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (* names / defs / types *) @@ -60,20 +55,11 @@ val interp_recursive : (** Exported for Funind *) -(** Extracting the semantical components out of the raw syntax of - (co)fixpoints declarations *) - -val extract_fixpoint_components - : structonly:bool -> fixpoint_expr list -> structured_fixpoint_expr 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 val interp_fixpoint : cofix:bool - -> structured_fixpoint_expr list + -> lident option fix_expr_gen list -> recursive_preentry * UState.universe_decl * UState.t * (EConstr.rel_context * Impargs.manual_implicits * int option) list diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 0104c99e41..c6e68effd7 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -289,19 +289,19 @@ let do_program_recursive ~scope ~poly fixkind fixl = | DeclareObl.IsFixpoint _ -> Decls.Fixpoint | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint in - let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl in + let ntns = List.map_append (fun { Vernacexpr.notations } -> 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 { Vernacexpr.rec_order } -> rec_order) l in match g, l with | [Some { CAst.v = CWfRec (n,r) }], - [ Vernacexpr.{id_decl=({CAst.v=id},pl);binders;rtype;body_def;notations} ] -> + [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] -> let recarg = mkIdentC n.CAst.v in - build_wellfounded (id, pl, binders, rtype, out_def body_def) poly r recarg notations + build_wellfounded (id, univs, binders, rtype, out_def body_def) poly r recarg notations | [Some { CAst.v = CMeasureRec (n, m, r) }], - [Vernacexpr.{id_decl=({CAst.v=id},pl); binders; rtype; body_def; notations }] -> + [Vernacexpr.{fname={CAst.v=id}; univs; 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 -> @@ -311,13 +311,15 @@ 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, binders, rtype, out_def body_def) poly + build_wellfounded (id, univs, 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 = 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 + let annots = List.map (fun fix -> + Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in + let fixkind = DeclareObl.IsFixpoint annots in + let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in + do_program_recursive ~scope ~poly fixkind l | _, _ -> user_err ~hdr:"do_program_fixpoint" @@ -332,7 +334,7 @@ let do_fixpoint ~scope ~poly l = do_program_fixpoint ~scope ~poly l; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () -let do_cofixpoint ~scope ~poly l = - let fixl = extract_cofixpoint_components l in +let do_cofixpoint ~scope ~poly fixl = + let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl 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 fa3d2b7020..a851e4dff5 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* { c } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 835f5e0b75..e25118e0a8 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -419,12 +419,12 @@ 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 { id_decl; rec_order; binders; rtype; body_def; notations } = + let pr_rec_definition { fname; univs; 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) binders rec_order in - pr_ident_decl id_decl ++ pr_binders_arg binders ++ annot + pr_ident_decl (fname,univs) ++ 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 @@ -858,8 +858,8 @@ let string_of_definition_object_kind = let open Decls in function | DoDischarge -> keyword "Let" ++ spc () | NoDischarge -> str "" in - let pr_onecorec {id_decl; binders; rtype; body_def; notations } = - pr_ident_decl id_decl ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++ + let pr_onecorec {fname; univs; binders; rtype; body_def; notations } = + pr_ident_decl (fname,univs) ++ 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 diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0205a653c5..6c048c7d83 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 { id_decl = (lid,_) } -> Dumpglob.dump_definition lid false "def") l; + List.iter (fun { fname } -> Dumpglob.dump_definition fname 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 { id_decl = (lid,_) } -> Dumpglob.dump_definition lid false "def") l; + List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") l; enforce_locality_exp atts.DefAttributes.locality discharge let vernac_cofixpoint_interactive ~atts discharge l = diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 8b8123bd30..6f09d9a39b 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -131,7 +131,8 @@ type definition_expr = type decl_notation = lstring * constr_expr * scope_name option type 'a fix_expr_gen = - { id_decl : ident_decl + { fname : lident + ; univs : universe_decl_expr option ; rec_order : 'a ; binders : local_binder_expr list ; rtype : constr_expr -- cgit v1.2.3