diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 8 | ||||
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/comDefinition.ml | 4 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 10 | ||||
| -rw-r--r-- | vernac/comSearch.ml | 140 | ||||
| -rw-r--r-- | vernac/comSearch.mli | 14 | ||||
| -rw-r--r-- | vernac/declare.ml | 1025 | ||||
| -rw-r--r-- | vernac/declare.mli | 312 | ||||
| -rw-r--r-- | vernac/declareObl.ml | 578 | ||||
| -rw-r--r-- | vernac/declareObl.mli | 164 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 66 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 321 | ||||
| -rw-r--r-- | vernac/lemmas.mli | 45 | ||||
| -rw-r--r-- | vernac/locality.ml | 12 | ||||
| -rw-r--r-- | vernac/locality.mli | 5 | ||||
| -rw-r--r-- | vernac/obligations.ml | 388 | ||||
| -rw-r--r-- | vernac/obligations.mli | 8 | ||||
| -rw-r--r-- | vernac/pfedit.ml | 2 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 81 | ||||
| -rw-r--r-- | vernac/proof_global.ml | 1 | ||||
| -rw-r--r-- | vernac/record.ml | 14 | ||||
| -rw-r--r-- | vernac/search.ml | 180 | ||||
| -rw-r--r-- | vernac/search.mli | 32 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 3 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 113 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 15 | ||||
| -rw-r--r-- | vernac/vernacinterp.ml | 4 |
28 files changed, 1910 insertions, 1639 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 5323c9f1c6..bb640a83f6 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -385,7 +385,7 @@ let build_beq_scheme mode kn = Vars.substl subst cores.(i) in create_input fix), - UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())) + UState.from_env (Global.env ())) let beq_scheme_kind = declare_mutual_scheme_object "_beq" @@ -707,7 +707,7 @@ let make_bl_scheme mode mind = let lnonparrec,lnamesparrec = (* TODO subst *) context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal = compute_bl_goal ind lnamesparrec nparrec in - let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = UState.from_env (Global.env ()) in let side_eff = side_effect_of_mode mode in let bl_goal = EConstr.of_constr bl_goal in let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal @@ -840,7 +840,7 @@ let make_lb_scheme mode mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal = compute_lb_goal ind lnamesparrec nparrec in - let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = UState.from_env (Global.env ()) in let side_eff = side_effect_of_mode mode in let lb_goal = EConstr.of_constr lb_goal in let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal @@ -1010,7 +1010,7 @@ let make_eq_decidability mode mind = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let u = Univ.Instance.empty in - let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in + let uctx = UState.from_env (Global.env ()) in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let side_eff = side_effect_of_mode mode in diff --git a/vernac/classes.ml b/vernac/classes.ml index 55af2e1a7d..21e2afe6a9 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -345,7 +345,7 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term let hook = Declare.Hook.make hook in let uctx = Evd.evar_universe_context sigma in let scope, kind = Declare.Global Declare.ImportDefaultBehavior, Decls.Instance in - let _ : DeclareObl.progress = + let _ : Declare.Obls.progress = Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls in () diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 95f3955309..d56917271c 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -126,8 +126,8 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in - let _ : DeclareObl.progress = + let term, ty, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in + let _ : Declare.Obls.progress = Obligations.add_definition ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls in () diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 4e9e24b119..4aa46e0a86 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -273,7 +273,7 @@ let collect_evars_of_term evd c ty = evars (Evd.from_ctx (Evd.evar_universe_context evd)) let do_program_recursive ~scope ~poly fixkind fixl = - let cofix = fixkind = DeclareObl.IsCoFixpoint in + let cofix = fixkind = Declare.Obls.IsCoFixpoint in let (env, rec_sign, udecl, evd), fix, info = interp_recursive ~cofix ~program_mode:true fixl in @@ -314,8 +314,8 @@ let do_program_recursive ~scope ~poly fixkind fixl = end in let uctx = Evd.evar_universe_context evd in let kind = match fixkind with - | DeclareObl.IsFixpoint _ -> Decls.Fixpoint - | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint + | Declare.Obls.IsFixpoint _ -> Decls.Fixpoint + | Declare.Obls.IsCoFixpoint -> Decls.CoFixpoint in let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~udecl ~uctx ntns fixkind @@ -345,7 +345,7 @@ let do_fixpoint ~scope ~poly l = | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> 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 fixkind = Declare.Obls.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 @@ -355,4 +355,4 @@ let do_fixpoint ~scope ~poly l = 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 + do_program_recursive ~scope ~poly Declare.Obls.IsCoFixpoint fixl diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml new file mode 100644 index 0000000000..9de8d6fbc3 --- /dev/null +++ b/vernac/comSearch.ml @@ -0,0 +1,140 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Interpretation of search commands *) + +open CErrors +open Names +open Util +open Pp +open Printer +open Search +open Vernacexpr +open Goptions + +let global_module qid = + try Nametab.full_name_module qid + with Not_found -> + user_err ?loc:qid.CAst.loc ~hdr:"global_module" + (str "Module/section " ++ Ppconstr.pr_qualid qid ++ str " not found.") + +let interp_search_restriction = function + | SearchOutside l -> (List.map global_module l, true) + | SearchInside l -> (List.map global_module l, false) + +let kind_searcher = Decls.(function + (* Kinds referring to the keyword introducing the object *) + | IsAssumption _ + | IsDefinition (Definition | Example | Fixpoint | CoFixpoint | Method | StructureComponent | Let) + | IsProof _ + | IsPrimitive as k -> Inl k + (* Kinds referring to the status of the object *) + | IsDefinition (Coercion | SubClass | IdentityCoercion as k') -> + let coercions = Coercionops.coercions () in + Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Coercionops.coe_value gr && + (k' <> SubClass && k' <> IdentityCoercion || c.Coercionops.coe_is_identity)) coercions) + | IsDefinition CanonicalStructure -> + let canonproj = Recordops.canonical_projections () in + Inr (fun gr -> List.exists (fun c -> GlobRef.equal (snd c).Recordops.o_ORIGIN gr) canonproj) + | IsDefinition Scheme -> + let schemes = DeclareScheme.all_schemes () in + Inr (fun gr -> Indset.exists (fun c -> GlobRef.equal (GlobRef.IndRef c) gr) schemes) + | IsDefinition Instance -> + let instances = Typeclasses.all_instances () in + Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Typeclasses.is_impl gr) instances)) + +let interp_search_item env sigma = + function + | SearchSubPattern ((where,head),pat) -> + let _,pat = Constrintern.intern_constr_pattern env sigma pat in + GlobSearchSubPattern (where,head,pat) + | SearchString ((Anywhere,false),s,None) when Id.is_valid s -> + GlobSearchString s + | SearchString ((where,head),s,sc) -> + (try + let ref = + Notation.interp_notation_as_global_reference + ~head:false (fun _ -> true) s sc in + GlobSearchSubPattern (where,head,Pattern.PRef ref) + with UserError _ -> + user_err ~hdr:"interp_search_item" + (str "Unable to interpret " ++ quote (str s) ++ str " as a reference.")) + | SearchKind k -> + match kind_searcher k with + | Inl k -> GlobSearchKind k + | Inr f -> GlobSearchFilter f + +let rec interp_search_request env sigma = function + | b, SearchLiteral i -> b, GlobSearchLiteral (interp_search_item env sigma i) + | b, SearchDisjConj l -> b, GlobSearchDisjConj (List.map (List.map (interp_search_request env sigma)) l) + +(* 05f22a5d6d5b8e3e80f1a37321708ce401834430 introduced the + `search_output_name_only` option to avoid excessive printing when + searching. + + The motivation was to make search usable for IDE completion, + however, it is still too slow due to the non-indexed nature of the + underlying search mechanism. + + In the future we should deprecate the option and provide a fast, + indexed name-searching interface. +*) +let search_output_name_only = ref false + +let () = + declare_bool_option + { optdepr = false; + optkey = ["Search";"Output";"Name";"Only"]; + optread = (fun () -> !search_output_name_only); + optwrite = (:=) search_output_name_only } + +let deprecated_searchhead = + CWarnings.create + ~name:"deprecated-searchhead" + ~category:"deprecated" + (fun () -> Pp.str("SearchHead is deprecated. Use the headconcl: clause of Search instead.")) + +let interp_search env sigma s r = + let r = interp_search_restriction r in + let get_pattern c = snd (Constrintern.intern_constr_pattern env sigma c) in + let warnlist = ref [] in + let pr_search ref kind env c = + let pr = pr_global ref in + let pp = if !search_output_name_only + then pr + else begin + let open Impargs in + let impls = implicits_of_global ref in + let impargs = select_stronger_impargs impls in + let impargs = List.map binding_kind_of_status impargs in + if List.length impls > 1 || + List.exists Glob_term.(function Explicit -> false | MaxImplicit | NonMaxImplicit -> true) + (List.skipn_at_least (Termops.nb_prod_modulo_zeta Evd.(from_env env) (EConstr.of_constr c)) impargs) + then warnlist := pr :: !warnlist; + let pc = pr_ltype_env env Evd.(from_env env) ~impargs c in + hov 2 (pr ++ str":" ++ spc () ++ pc) + end + in Feedback.msg_notice pp + in + (match s with + | SearchPattern c -> + (Search.search_pattern env sigma (get_pattern c) r |> Search.prioritize_search) pr_search + | SearchRewrite c -> + (Search.search_rewrite env sigma (get_pattern c) r |> Search.prioritize_search) pr_search + | SearchHead c -> + deprecated_searchhead (); + (Search.search_by_head env sigma (get_pattern c) r |> Search.prioritize_search) pr_search + | Search sl -> + (Search.search env sigma (List.map (interp_search_request env Evd.(from_env env)) sl) r |> + Search.prioritize_search) pr_search); + if !warnlist <> [] then + Feedback.msg_notice (str "(" ++ + hov 0 (strbrk "use \"About\" for full details on the implicit arguments of " ++ + pr_enum (fun x -> x) !warnlist ++ str ")")) diff --git a/vernac/comSearch.mli b/vernac/comSearch.mli new file mode 100644 index 0000000000..42f59984ff --- /dev/null +++ b/vernac/comSearch.mli @@ -0,0 +1,14 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Interpretation of search commands *) + +val interp_search : Environ.env -> Evd.evar_map -> + Vernacexpr.searchable -> Vernacexpr.search_restriction -> unit diff --git a/vernac/declare.ml b/vernac/declare.ml index c3f95c5297..c77d4909da 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -120,7 +120,7 @@ let get_open_goals ps = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + List.length shelf -type import_status = ImportDefaultBehavior | ImportNeedQualified +type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeedQualified (** Declaration of constants and parameters *) @@ -155,6 +155,8 @@ type proof_object = ; uctx: UState.t } +let get_po_name { name } = name + let private_poly_univs = Goptions.declare_bool_option_and_ref ~depr:false @@ -847,23 +849,6 @@ let get_current_context pf = let p = get_proof pf in Proof.get_proof_context p -module Proof = struct - type nonrec t = t - let get_proof = get_proof - let get_proof_name = get_proof_name - let get_used_variables = get_used_variables - let get_universe_decl = get_universe_decl - let get_initial_euctx = get_initial_euctx - let map_proof = map_proof - let map_fold_proof = map_fold_proof - let map_fold_proof_endline = map_fold_proof_endline - let set_endline_tactic = set_endline_tactic - let set_used_variables = set_used_variables - let compact = compact_the_proof - let update_global_env = update_global_env - let get_open_goals = get_open_goals -end - let declare_definition_scheme ~internal ~univs ~role ~name c = let kind = Decls.(IsDefinition Scheme) in let entry = pure_definition_entry ~univs c in @@ -876,7 +861,7 @@ let _ = Abstract.declare_abstract := declare_abstract let declare_universe_context = DeclareUctx.declare_universe_context -type locality = Discharge | Global of import_status +type locality = Locality.locality = | Discharge | Global of import_status (* Hooks naturally belong here as they apply to both definitions and lemmas *) module Hook = struct @@ -1022,25 +1007,20 @@ let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry -let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = +let prepare_obligation ~name ~types ~body sigma = + let env = Global.env () in + let types = match types with + | Some t -> t + | None -> Retyping.get_type_of env sigma body + in let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false - sigma (fun nf -> nf body, Option.map nf types) + sigma (fun nf -> nf body, nf types) in - let univs = Evd.check_univ_decl ~poly sigma udecl in - let ce = definition_entry ?opaque ?inline ?types ~univs body in - let env = Global.env () in - let (c,ctx), sideff = Future.force ce.proof_entry_body in - assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private); - assert(Univ.ContextSet.is_empty ctx); RetrieveObl.check_evars env sigma; - let c = EConstr.of_constr c in - let typ = match ce.proof_entry_type with - | Some t -> EConstr.of_constr t - | None -> Retyping.get_type_of env sigma c - in - let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in + let body, types = EConstr.(of_constr body, of_constr types) in + let obls, _, body, cty = RetrieveObl.retrieve_obligations env name sigma 0 body types in let uctx = Evd.evar_universe_context sigma in - c, cty, uctx, obls + body, cty, uctx, obls let prepare_parameter ~poly ~udecl ~types sigma = let env = Global.env () in @@ -1053,3 +1033,980 @@ let prepare_parameter ~poly ~udecl ~types sigma = (* Compat: will remove *) exception AlreadyDeclared = DeclareUniv.AlreadyDeclared + +module Obls = struct + +open Constr + +type 'a obligation_body = DefinedObl of 'a | TermObl of constr + +module Obligation = struct + type t = + { obl_name : Id.t + ; obl_type : types + ; obl_location : Evar_kinds.t Loc.located + ; obl_body : pconstant obligation_body option + ; obl_status : bool * Evar_kinds.obligation_definition_status + ; obl_deps : Int.Set.t + ; obl_tac : unit Proofview.tactic option } + + let set_type ~typ obl = {obl with obl_type = typ} + let set_body ~body obl = {obl with obl_body = Some body} +end + +type obligations = {obls : Obligation.t array; remaining : int} +type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint + +module ProgramDecl = struct + type t = + { prg_name : Id.t + ; prg_body : constr + ; prg_type : constr + ; prg_ctx : UState.t + ; prg_univdecl : UState.universe_decl + ; prg_obligations : obligations + ; prg_deps : Id.t list + ; prg_fixkind : fixpoint_kind option + ; prg_implicits : Impargs.manual_implicits + ; prg_notations : Vernacexpr.decl_notation list + ; prg_poly : bool + ; prg_scope : locality + ; prg_kind : Decls.definition_object_kind + ; prg_reduce : constr -> constr + ; prg_hook : Hook.t option + ; prg_opaque : bool } + + open Obligation + + let make ?(opaque = false) ?hook n ~udecl ~uctx ~impargs ~poly ~scope ~kind b + t deps fixkind notations obls reduce = + let obls', b = + match b with + | None -> + assert (Int.equal (Array.length obls) 0); + let n = Nameops.add_suffix n "_obligation" in + ( [| { obl_name = n + ; obl_body = None + ; obl_location = Loc.tag Evar_kinds.InternalHole + ; obl_type = t + ; obl_status = (false, Evar_kinds.Expand) + ; obl_deps = Int.Set.empty + ; obl_tac = None } |] + , mkVar n ) + | Some b -> + ( Array.mapi + (fun i (n, t, l, o, d, tac) -> + { obl_name = n + ; obl_body = None + ; obl_location = l + ; obl_type = t + ; obl_status = o + ; obl_deps = d + ; obl_tac = tac }) + obls + , b ) + in + let ctx = UState.make_flexible_nonalgebraic uctx in + { prg_name = n + ; prg_body = b + ; prg_type = reduce t + ; prg_ctx = ctx + ; prg_univdecl = udecl + ; prg_obligations = {obls = obls'; remaining = Array.length obls'} + ; prg_deps = deps + ; prg_fixkind = fixkind + ; prg_notations = notations + ; prg_implicits = impargs + ; prg_poly = poly + ; prg_scope = scope + ; prg_kind = kind + ; prg_reduce = reduce + ; prg_hook = hook + ; prg_opaque = opaque } + + let set_uctx ~uctx prg = {prg with prg_ctx = uctx} +end + +open Obligation +open ProgramDecl + +(* Saving an obligation *) + +(* XXX: Is this the right place for this? *) +let it_mkLambda_or_LetIn_or_clean t ctx = + let open Context.Rel.Declaration in + let fold t decl = + if is_local_assum decl then Term.mkLambda_or_LetIn decl t + else if Vars.noccurn 1 t then Vars.subst1 mkProp t + else Term.mkLambda_or_LetIn decl t + in + Context.Rel.fold_inside fold ctx ~init:t + +(* XXX: Is this the right place for this? *) +let decompose_lam_prod c ty = + let open Context.Rel.Declaration in + let rec aux ctx c ty = + match (Constr.kind c, Constr.kind ty) with + | LetIn (x, b, t, c), LetIn (x', b', t', ty) + when Constr.equal b b' && Constr.equal t t' -> + let ctx' = Context.Rel.add (LocalDef (x, b', t')) ctx in + aux ctx' c ty + | _, LetIn (x', b', t', ty) -> + let ctx' = Context.Rel.add (LocalDef (x', b', t')) ctx in + aux ctx' (lift 1 c) ty + | LetIn (x, b, t, c), _ -> + let ctx' = Context.Rel.add (LocalDef (x, b, t)) ctx in + aux ctx' c (lift 1 ty) + | Lambda (x, b, t), Prod (x', b', t') + (* By invariant, must be convertible *) -> + let ctx' = Context.Rel.add (LocalAssum (x, b')) ctx in + aux ctx' t t' + | Cast (c, _, _), _ -> aux ctx c ty + | _, _ -> (ctx, c, ty) + in + aux Context.Rel.empty c ty + +(* XXX: What's the relation of this with Abstract.shrink ? *) +let shrink_body c ty = + let ctx, b, ty = + match ty with + | None -> + let ctx, b = Term.decompose_lam_assum c in + (ctx, b, None) + | Some ty -> + let ctx, b, ty = decompose_lam_prod c ty in + (ctx, b, Some ty) + in + let b', ty', n, args = + List.fold_left + (fun (b, ty, i, args) decl -> + if Vars.noccurn 1 b && Option.cata (Vars.noccurn 1) true ty then + (Vars.subst1 mkProp b, Option.map (Vars.subst1 mkProp) ty, succ i, args) + else + let open Context.Rel.Declaration in + let args = if is_local_assum decl then mkRel i :: args else args in + ( Term.mkLambda_or_LetIn decl b + , Option.map (Term.mkProd_or_LetIn decl) ty + , succ i + , args )) + (b, ty, 1, []) ctx + in + (ctx, b', ty', Array.of_list args) + +(***********************************************************************) +(* Saving an obligation *) +(***********************************************************************) + +let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] + +let add_hint local prg cst = + let locality = if local then Goptions.OptLocal else Goptions.OptExport in + Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst) + +(* true = hide obligations *) +let get_hide_obligations = + Goptions.declare_bool_option_and_ref + ~depr:true + ~key:["Hide"; "Obligations"] + ~value:false + +let declare_obligation prg obl ~uctx ~types ~body = + let univs = UState.univ_entry ~poly:prg.prg_poly uctx in + let body = prg.prg_reduce body in + let types = Option.map prg.prg_reduce types in + match obl.obl_status with + | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)}) + | force, Evar_kinds.Define opaque -> + let opaque = (not force) && opaque in + let poly = prg.prg_poly in + let ctx, body, ty, args = + if not poly then shrink_body body types + else ([], body, types, [||]) + in + let ce = definition_entry ?types:ty ~opaque ~univs body in + (* ppedrot: seems legit to have obligations as local *) + let constant = + declare_constant ~name:obl.obl_name + ~local:ImportNeedQualified + ~kind:Decls.(IsProof Property) + (DefinitionEntry ce) + in + if not opaque then + add_hint (Locality.make_section_locality None) prg constant; + definition_message obl.obl_name; + let body = + match univs with + | Entries.Polymorphic_entry (_, uctx) -> + Some (DefinedObl (constant, Univ.UContext.instance uctx)) + | Entries.Monomorphic_entry _ -> + Some + (TermObl + (it_mkLambda_or_LetIn_or_clean + (mkApp (mkConst constant, args)) + ctx)) + in + (true, {obl with obl_body = body}) + +(* Updating the obligation meta-info on close *) + +let not_transp_msg = + Pp.( + str "Obligation should be transparent but was declared opaque." + ++ spc () + ++ str "Use 'Defined' instead.") + +let pperror cmd = CErrors.user_err ~hdr:"Program" cmd +let err_not_transp () = pperror not_transp_msg + +module ProgMap = Id.Map + +module StateFunctional = struct + + type t = ProgramDecl.t CEphemeron.key ProgMap.t + + let _empty = ProgMap.empty + + let pending pm = + ProgMap.filter + (fun _ v -> (CEphemeron.get v).prg_obligations.remaining > 0) + pm + + let num_pending pm = pending pm |> ProgMap.cardinal + + let first_pending pm = + pending pm |> ProgMap.choose_opt + |> Option.map (fun (_, v) -> CEphemeron.get v) + + let get_unique_open_prog pm name : (_, Id.t list) result = + match name with + | Some n -> + Option.cata + (fun p -> Ok (CEphemeron.get p)) + (Error []) (ProgMap.find_opt n pm) + | None -> ( + let n = num_pending pm in + match n with + | 0 -> Error [] + | 1 -> Option.cata (fun p -> Ok p) (Error []) (first_pending pm) + | _ -> + let progs = Id.Set.elements (ProgMap.domain pm) in + Error progs ) + + let add t key prg = ProgMap.add key (CEphemeron.create prg) t + + let fold t ~f ~init = + let f k v acc = f k (CEphemeron.get v) acc in + ProgMap.fold f t init + + let all pm = ProgMap.bindings pm |> List.map (fun (_,v) -> CEphemeron.get v) + let find m t = ProgMap.find_opt t m |> Option.map CEphemeron.get +end + +module State = struct + + type t = StateFunctional.t + + open StateFunctional + + let prg_ref, prg_tag = + Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" + + let num_pending () = num_pending !prg_ref + let first_pending () = first_pending !prg_ref + let get_unique_open_prog id = get_unique_open_prog !prg_ref id + let add id prg = prg_ref := add !prg_ref id prg + let fold ~f ~init = fold !prg_ref ~f ~init + let all () = all !prg_ref + let find id = find !prg_ref id + +end + +(* In all cases, the use of the map is read-only so we don't expose the ref *) +let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] + +let check_solved_obligations ~what_for : unit = + if not (ProgMap.is_empty !State.prg_ref) then + let keys = map_keys !State.prg_ref in + let have_string = if Int.equal (List.length keys) 1 then " has " else " have " in + CErrors.user_err ~hdr:"Program" + Pp.( + str "Unsolved obligations when closing " + ++ what_for ++ str ":" ++ spc () + ++ prlist_with_sep spc (fun x -> Id.print x) keys + ++ str have_string + ++ str "unsolved obligations" ) + +let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) +let progmap_remove pm prg = ProgMap.remove prg.prg_name pm +let progmap_replace prg' pm = map_replace prg'.prg_name prg' pm +let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0 + +let obligations_message rem = + Format.asprintf "%s %s remaining" + (if rem > 0 then string_of_int rem else "No more") + (CString.plural rem "obligation") + |> Pp.str |> Flags.if_verbose Feedback.msg_info + +type progress = Remain of int | Dependent | Defined of GlobRef.t + +let get_obligation_body expand obl = + match obl.obl_body with + | None -> None + | Some c -> ( + if expand && snd obl.obl_status == Evar_kinds.Expand then + match c with + | DefinedObl pc -> Some (Environ.constant_value_in (Global.env ()) pc) + | TermObl c -> Some c + else + match c with DefinedObl pc -> Some (mkConstU pc) | TermObl c -> Some c ) + +let obl_substitution expand obls deps = + Int.Set.fold + (fun x acc -> + let xobl = obls.(x) in + match get_obligation_body expand xobl with + | None -> acc + | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc) + deps [] + +let rec intset_to = function + | -1 -> Int.Set.empty + | n -> Int.Set.add n (intset_to (pred n)) + +let obligation_substitution expand prg = + let obls = prg.prg_obligations.obls in + let ints = intset_to (pred (Array.length obls)) in + obl_substitution expand obls ints + +let hide_obligation () = + Coqlib.check_required_library ["Coq"; "Program"; "Tactics"]; + UnivGen.constr_of_monomorphic_global + (Coqlib.lib_ref "program.tactics.obligation") + +(* XXX: Is this the right place? *) +let rec prod_app t n = + match + Constr.kind + (EConstr.Unsafe.to_constr + (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) + (* FIXME *) + with + | Prod (_, _, b) -> Vars.subst1 n b + | LetIn (_, b, t, b') -> prod_app (Vars.subst1 b b') n + | _ -> + CErrors.user_err ~hdr:"prod_app" + Pp.(str "Needed a product, but didn't find one" ++ fnl ()) + +(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) +let prod_applist t nL = List.fold_left prod_app t nL + +let replace_appvars subst = + let rec aux c = + let f, l = decompose_app c in + if isVar f then + try + let c' = List.map (Constr.map aux) l in + let t, b = Id.List.assoc (destVar f) subst in + mkApp + ( delayed_force hide_obligation + , [|prod_applist t c'; Term.applistc b c'|] ) + with Not_found -> Constr.map aux c + else Constr.map aux c + in + Constr.map aux + +let subst_prog subst prg = + if get_hide_obligations () then + ( replace_appvars subst prg.prg_body + , replace_appvars subst (* Termops.refresh_universes *) prg.prg_type ) + else + let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in + ( Vars.replace_vars subst' prg.prg_body + , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type ) + +let stm_get_fix_exn = ref (fun _ x -> x) + +let declare_definition prg = + let varsubst = obligation_substitution true prg in + let sigma = Evd.from_ctx prg.prg_ctx in + let body, types = subst_prog varsubst prg in + let body, types = EConstr.(of_constr body, Some (of_constr types)) in + (* All these should be grouped into a struct a some point *) + let opaque, poly, udecl, hook = + (prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook) + in + let name, scope, kind, impargs = + ( prg.prg_name + , prg.prg_scope + , Decls.(IsDefinition prg.prg_kind) + , prg.prg_implicits ) + in + let fix_exn = !stm_get_fix_exn () in + let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in + (* XXX: This is doing normalization twice *) + let kn = + declare_definition ~name ~scope ~kind ~impargs ?hook ~obls + ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma + in + let pm = progmap_remove !State.prg_ref prg in + State.prg_ref := pm; + kn + +let rec lam_index n t acc = + match Constr.kind t with + | Lambda ({Context.binder_name = Name n'}, _, _) when Id.equal n n' -> acc + | Lambda (_, _, b) -> lam_index n b (succ acc) + | _ -> raise Not_found + +let compute_possible_guardness_evidences n fixbody fixtype = + match n with + | Some {CAst.loc; v = n} -> [lam_index n fixbody 0] + | None -> + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual + fixpoints ?) *) + let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (* FIXME *) in + let ctx = fst (Term.decompose_prod_n_assum m fixtype) in + List.map_i (fun i _ -> i) 0 ctx + +let declare_mutual_definition l = + let len = List.length l in + let first = List.hd l in + let defobl x = + let oblsubst = obligation_substitution true x in + let subs, typ = subst_prog oblsubst x in + let env = Global.env () in + let sigma = Evd.from_ctx x.prg_ctx in + let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in + let term = + snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) + in + let typ = + snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) + in + let term = EConstr.to_constr sigma term in + let typ = EConstr.to_constr sigma typ in + let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in + let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in + (def, oblsubst) + in + let defs, obls = + List.fold_right + (fun x (defs, obls) -> + let xdef, xobls = defobl x in + (xdef :: defs, xobls @ obls)) + l ([], []) + in + (* let fixdefs = List.map reduce_fix fixdefs in *) + let fixdefs, fixrs, fixtypes, fixitems = + List.fold_right2 + (fun (d, r, typ, impargs) name (a1, a2, a3, a4) -> + ( d :: a1 + , r :: a2 + , typ :: a3 + , Recthm.{name; typ; impargs; args = []} :: a4 )) + defs first.prg_deps ([], [], [], []) + in + let fixkind = Option.get first.prg_fixkind in + let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in + let rvec = Array.of_list fixrs in + let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in + let rec_declaration = (Array.map2 Context.make_annot namevec rvec, arrrec, recvec) in + let possible_indexes = + match fixkind with + | IsFixpoint wfl -> + Some (List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes) + | IsCoFixpoint -> None + in + (* In the future we will pack all this in a proper record *) + let poly, scope, ntns, opaque = + (first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque) + in + let kind = + if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) + else Decls.(IsDefinition CoFixpoint) + in + (* Declare the recursive definitions *) + let udecl = UState.default_univ_decl in + let kns = + declare_mutually_recursive ~scope ~opaque ~kind ~udecl ~ntns + ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly + ~restrict_ucontext:false fixitems + in + (* Only for the first constant *) + let dref = List.hd kns in + Hook.( + call ?hook:first.prg_hook {S.uctx = first.prg_ctx; obls; scope; dref}); + let pm = List.fold_left progmap_remove !State.prg_ref l in + State.prg_ref := pm; + dref + +let update_obls prg obls rem = + let prg_obligations = {obls; remaining = rem} in + let prg' = {prg with prg_obligations} in + let pm = progmap_replace prg' !State.prg_ref in + State.prg_ref := pm; + obligations_message rem; + if rem > 0 then Remain rem + else + match prg'.prg_deps with + | [] -> + let kn = declare_definition prg' in + let pm = progmap_remove !State.prg_ref prg' in + State.prg_ref := pm; + Defined kn + | l -> + let progs = + List.map (fun x -> CEphemeron.get (ProgMap.find x pm)) prg'.prg_deps + in + if List.for_all (fun x -> obligations_solved x) progs then + let kn = declare_mutual_definition progs in + Defined kn + else Dependent + +let dependencies obls n = + let res = ref Int.Set.empty in + Array.iteri + (fun i obl -> + if (not (Int.equal i n)) && Int.Set.mem n obl.obl_deps then + res := Int.Set.add i !res) + obls; + !res + +let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto = + let obls = Array.copy obls in + let () = obls.(num) <- obl in + let prg = {prg with prg_ctx = uctx} in + let _progress = update_obls prg obls (pred rem) in + let () = + if pred rem > 0 then + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then + let _progress = auto (Some prg.prg_name) deps None in + () + else () + else () + in + () + +type obligation_resolver = + Id.t option + -> Int.Set.t + -> unit Proofview.tactic option + -> progress + +type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver} + +let obligation_terminator entries uctx {name; num; auto} = + match entries with + | [entry] -> + let env = Global.env () in + let ty = entry.proof_entry_type in + let body, uctx = inline_private_constants ~uctx env entry in + let sigma = Evd.from_ctx uctx in + Inductiveops.control_only_guard (Global.env ()) sigma + (EConstr.of_constr body); + (* Declare the obligation ourselves and drop the hook *) + let prg = Option.get (State.find name) in + let {obls; remaining = rem} = prg.prg_obligations in + let obl = obls.(num) in + let status = + match (obl.obl_status, entry.proof_entry_opaque) with + | (_, Evar_kinds.Expand), true -> err_not_transp () + | (true, _), true -> err_not_transp () + | (false, _), true -> Evar_kinds.Define true + | (_, Evar_kinds.Define true), false -> Evar_kinds.Define false + | (_, status), false -> status + in + let obl = {obl with obl_status = (false, status)} in + let uctx = if prg.prg_poly then uctx else UState.union prg.prg_ctx uctx in + let defined, obl = declare_obligation prg obl ~body ~types:ty ~uctx in + let prg_ctx = + if prg.prg_poly then + (* Polymorphic *) + (* We merge the new universes and constraints of the + polymorphic obligation with the existing ones *) + UState.union prg.prg_ctx uctx + else if + (* The first obligation, if defined, + declares the univs of the constant, + each subsequent obligation declares its own additional + universes and constraints if any *) + defined + then + UState.from_env (Global.env ()) + else uctx + in + update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto + | _ -> + CErrors.anomaly + Pp.( + str + "[obligation_terminator] close_proof returned more than one proof \ + term") + +(* Similar to the terminator but for the admitted path; this assumes + the admitted constant was already declared. + + FIXME: There is duplication of this code with obligation_terminator + and Obligations.admit_obligations *) +let obligation_admitted_terminator {name; num; auto} ctx' dref = + let prg = Option.get (State.find name) in + let {obls; remaining = rem} = prg.prg_obligations in + let obl = obls.(num) in + let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in + let transparent = Environ.evaluable_constant cst (Global.env ()) in + let () = + match obl.obl_status with + | true, Evar_kinds.Expand | true, Evar_kinds.Define true -> + if not transparent then err_not_transp () + | _ -> () + in + let inst, ctx' = + if not prg.prg_poly (* Not polymorphic *) then + (* The universe context was declared globally, we continue + from the new global environment. *) + let ctx = UState.from_env (Global.env ()) in + let ctx' = UState.merge_subst ctx (UState.subst ctx') in + (Univ.Instance.empty, ctx') + else + (* We get the right order somehow, but surely it could be enforced in a clearer way. *) + let uctx = UState.context ctx' in + (Univ.UContext.instance uctx, ctx') + in + let obl = {obl with obl_body = Some (DefinedObl (cst, inst))} in + let () = if transparent then add_hint true prg cst in + update_program_decl_on_defined prg obls num obl ~uctx:ctx' rem ~auto + +end + +(************************************************************************) +(* Commom constant saving path, for both Qed and Admitted *) +(************************************************************************) + +(* Support for mutually proved theorems *) + +module Proof_ending = struct + + type t = + | Regular + | End_obligation of Obls.obligation_qed_info + | End_derive of { f : Id.t; name : Id.t } + | End_equations of + { hook : Constant.t list -> Evd.evar_map -> unit + ; i : Id.t + ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list + ; sigma : Evd.evar_map + } + +end + +type lemma_possible_guards = int list list + +module Info = struct + + type t = + { hook : Hook.t option + ; proof_ending : Proof_ending.t CEphemeron.key + (* This could be improved and the CEphemeron removed *) + ; scope : locality + ; kind : Decls.logical_kind + (* thms and compute guard are specific only to start_lemma_with_initialization + regular terminator *) + ; thms : Recthm.t list + ; compute_guard : lemma_possible_guards + } + + let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Global ImportDefaultBehavior) + ?(kind=Decls.(IsProof Lemma)) ?(compute_guard=[]) ?(thms=[]) () = + { hook + ; compute_guard + ; proof_ending = CEphemeron.create proof_ending + ; thms + ; scope + ; kind + } + + (* This is used due to a deficiency on the API, should fix *) + let add_first_thm ~info ~name ~typ ~impargs = + let thms = + { Recthm.name + ; impargs + ; typ = EConstr.Unsafe.to_constr typ + ; args = [] } :: info.thms + in + { info with thms } + +end + +(* XXX: this should be unified with the code for non-interactive + mutuals previously on this file. *) +module MutualEntry : sig + + val declare_variable + : info:Info.t + -> uctx:UState.t + -> Entries.parameter_entry + -> Names.GlobRef.t list + + val declare_mutdef + (* Common to all recthms *) + : info:Info.t + -> uctx:UState.t + -> Evd.side_effects proof_entry + -> Names.GlobRef.t list + +end = struct + + (* XXX: Refactor this with the code in [Declare.declare_mutdef] *) + let guess_decreasing env possible_indexes ((body, ctx), eff) = + let open Constr in + match Constr.kind body with + | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> + let env = Safe_typing.push_private_constants env eff.Evd.seff_private in + let indexes = Pretyping.search_guard env possible_indexes fixdecls in + (mkFix ((indexes,0),fixdecls), ctx), eff + | _ -> (body, ctx), eff + + let select_body i t = + let open Constr in + match Constr.kind t with + | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) + | CoFix (0,decls) -> mkCoFix (i,decls) + | _ -> + CErrors.anomaly + Pp.(str "Not a proof by induction: " ++ + Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".") + + let declare_mutdef ~uctx ~info pe i Recthm.{ name; impargs; typ; _} = + let { Info.hook; scope; kind; compute_guard; _ } = info in + (* if i = 0 , we don't touch the type; this is for compat + but not clear it is the right thing to do. + *) + let pe, ubind = + if i > 0 && not (CList.is_empty compute_guard) + then Internal.map_entry_type pe ~f:(fun _ -> Some typ), UnivNames.empty_binders + else pe, UState.universe_binders uctx + in + (* We when compute_guard was [] in the previous step we should not + substitute the body *) + let pe = match compute_guard with + | [] -> pe + | _ -> + Internal.map_entry_body pe + ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) + in + declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe + + let declare_mutdef ~info ~uctx const = + let pe = match info.Info.compute_guard with + | [] -> + (* Not a recursive statement *) + const + | possible_indexes -> + (* Try all combinations... not optimal *) + let env = Global.env() in + Internal.map_entry_body const + ~f:(guess_decreasing env possible_indexes) + in + List.map_i (declare_mutdef ~info ~uctx pe) 0 info.Info.thms + + let declare_variable ~info ~uctx pe = + let { Info.scope; hook } = info in + List.map_i ( + fun i { Recthm.name; typ; impargs } -> + declare_assumption ~name ~scope ~hook ~impargs ~uctx pe + ) 0 info.Info.thms + +end + +(************************************************************************) +(* Admitting a lemma-like constant *) +(************************************************************************) + +(* Admitted *) +let get_keep_admitted_vars = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Keep"; "Admitted"; "Variables"] + ~value:true + +let compute_proof_using_for_admitted proof typ pproofs = + if not (get_keep_admitted_vars ()) then None + else match get_used_variables proof, pproofs with + | Some _ as x, _ -> x + | None, pproof :: _ -> + let env = Global.env () in + let ids_typ = Environ.global_vars_set env typ in + (* [pproof] is evar-normalized by [partial_proof]. We don't + count variables appearing only in the type of evars. *) + let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in + Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) + | _ -> None + +let finish_admitted ~info ~uctx pe = + let cst = MutualEntry.declare_variable ~info ~uctx pe in + (* If the constant was an obligation we need to update the program map *) + match CEphemeron.get info.Info.proof_ending with + | Proof_ending.End_obligation oinfo -> + Obls.obligation_admitted_terminator oinfo uctx (List.hd cst) + | _ -> () + +let save_lemma_admitted ~proof ~info = + let udecl = get_universe_decl proof in + let Proof.{ poly; entry } = Proof.data (get_proof proof) in + let typ = match Proofview.initial_goals entry with + | [typ] -> snd typ + | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.") + in + let typ = EConstr.Unsafe.to_constr typ in + let iproof = get_proof proof in + let pproofs = Proof.partial_proof iproof in + let sec_vars = compute_proof_using_for_admitted proof typ pproofs in + let uctx = get_initial_euctx proof in + let univs = UState.check_univ_decl ~poly uctx udecl in + finish_admitted ~info ~uctx (sec_vars, (typ, univs), None) + +(************************************************************************) +(* Saving a lemma-like constant *) +(************************************************************************) + +let finish_proved po info = + match po with + | { entries=[const]; uctx } -> + let _r : Names.GlobRef.t list = MutualEntry.declare_mutdef ~info ~uctx const in + () + | _ -> + CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term") + +let finish_derived ~f ~name ~entries = + (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *) + + let f_def, lemma_def = + match entries with + | [_;f_def;lemma_def] -> + f_def, lemma_def + | _ -> assert false + in + (* The opacity of [f_def] is adjusted to be [false], as it + must. Then [f] is declared in the global environment. *) + let f_def = Internal.set_opacity ~opaque:false f_def in + let f_kind = Decls.(IsDefinition Definition) in + let f_def = DefinitionEntry f_def in + let f_kn = declare_constant ~name:f ~kind:f_kind f_def in + let f_kn_term = Constr.mkConst f_kn in + (* In the type and body of the proof of [suchthat] there can be + references to the variable [f]. It needs to be replaced by + references to the constant [f] declared above. This substitution + performs this precise action. *) + let substf c = Vars.replace_vars [f,f_kn_term] c in + (* Extracts the type of the proof of [suchthat]. *) + let lemma_pretype typ = + match typ with + | Some t -> Some (substf t) + | None -> assert false (* Declare always sets type here. *) + in + (* The references of [f] are subsituted appropriately. *) + let lemma_def = Internal.map_entry_type lemma_def ~f:lemma_pretype in + (* The same is done in the body of the proof. *) + let lemma_def = Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in + let lemma_def = DefinitionEntry lemma_def in + let _ : Names.Constant.t = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in + () + +let finish_proved_equations ~kind ~hook i proof_obj types sigma0 = + + let obls = ref 1 in + let sigma, recobls = + CList.fold_left2_map (fun sigma (_evar_env, ev, _evi, local_context, _type) entry -> + let id = + match Evd.evar_ident ev sigma0 with + | Some id -> id + | None -> let n = !obls in incr obls; Nameops.add_suffix i ("_obligation_" ^ string_of_int n) + in + let entry, args = Internal.shrink_entry local_context entry in + let cst = declare_constant ~name:id ~kind (DefinitionEntry entry) in + let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in + let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in + sigma, cst) sigma0 + types proof_obj.entries + in + hook recobls sigma + +let finalize_proof proof_obj proof_info = + let open Proof_ending in + match CEphemeron.default proof_info.Info.proof_ending Regular with + | Regular -> + finish_proved proof_obj proof_info + | End_obligation oinfo -> + Obls.obligation_terminator proof_obj.entries proof_obj.uctx oinfo + | End_derive { f ; name } -> + finish_derived ~f ~name ~entries:proof_obj.entries + | End_equations { hook; i; types; sigma } -> + finish_proved_equations ~kind:proof_info.Info.kind ~hook i proof_obj types sigma + +let err_save_forbidden_in_place_of_qed () = + CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode") + +let process_idopt_for_save ~idopt info = + match idopt with + | None -> info + | Some { CAst.v = save_name } -> + (* Save foo was used; we override the info in the first theorem *) + let thms = + match info.Info.thms, CEphemeron.default info.Info.proof_ending Proof_ending.Regular with + | [ { Recthm.name; _} as decl ], Proof_ending.Regular -> + [ { decl with Recthm.name = save_name } ] + | _ -> + err_save_forbidden_in_place_of_qed () + in { info with Info.thms } + +let save_lemma_proved ~proof ~info ~opaque ~idopt = + (* Env and sigma are just used for error printing in save_remaining_recthms *) + let proof_obj = close_proof ~opaque ~keep_body_ucst_separate:false proof in + let proof_info = process_idopt_for_save ~idopt info in + finalize_proof proof_obj proof_info + +(***********************************************************************) +(* Special case to close a lemma without forcing a proof *) +(***********************************************************************) +let save_lemma_admitted_delayed ~proof ~info = + let { entries; uctx } = proof in + if List.length entries <> 1 then + CErrors.user_err Pp.(str "Admitted does not support multiple statements"); + let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in + let poly = match proof_entry_universes with + | Entries.Monomorphic_entry _ -> false + | Entries.Polymorphic_entry (_, _) -> true in + let typ = match proof_entry_type with + | None -> CErrors.user_err Pp.(str "Admitted requires an explicit statement"); + | Some typ -> typ in + let ctx = UState.univ_entry ~poly uctx in + let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in + finish_admitted ~uctx ~info (sec_vars, (typ, ctx), None) + +let save_lemma_proved_delayed ~proof ~info ~idopt = + (* vio2vo calls this but with invalid info, we have to workaround + that to add the name to the info structure *) + if CList.is_empty info.Info.thms then + let name = get_po_name proof in + let info = Info.add_first_thm ~info ~name ~typ:EConstr.mkSet ~impargs:[] in + finalize_proof proof info + else + let info = process_idopt_for_save ~idopt info in + finalize_proof proof info + +module Proof = struct + type nonrec t = t + let get_proof = get_proof + let get_proof_name = get_proof_name + let map_proof = map_proof + let map_fold_proof = map_fold_proof + let map_fold_proof_endline = map_fold_proof_endline + let set_endline_tactic = set_endline_tactic + let set_used_variables = set_used_variables + let compact = compact_the_proof + let update_global_env = update_global_env + let get_open_goals = get_open_goals +end diff --git a/vernac/declare.mli b/vernac/declare.mli index 340c035d1d..647896e2f5 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -17,9 +17,9 @@ open Entries environment. It also updates some accesory tables such as [Nametab] (name resolution), [Impargs], and [Notations]. *) -(** We provide two kind of fuctions: +(** We provide two kind of functions: - - one go functions, that will register a constant in one go, suited + - one-go functions, that will register a constant in one go, suited for non-interactive definitions where the term is given. - two-phase [start/declare] functions which will create an @@ -29,6 +29,13 @@ open Entries Internally, these functions mainly differ in that usually, the first case doesn't require setting up the tactic engine. + Note that the API in this file is still in a state of flux, don't + hesitate to contact the maintainers if you have any question. + + Additionally, this file does contain some low-level functions, marked + as such; these functions are unstable and should not be used unless you + already know what they are doing. + *) (** [Declare.Proof.t] Construction of constants using interactive proofs. *) @@ -41,11 +48,6 @@ module Proof : sig val get_proof : t -> Proof.t val get_proof_name : t -> Names.Id.t - (** XXX: These 3 are only used in lemmas *) - val get_used_variables : t -> Names.Id.Set.t option - val get_universe_decl : t -> UState.universe_decl - val get_initial_euctx : t -> UState.t - val map_proof : (Proof.t -> Proof.t) -> t -> t val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a @@ -97,39 +99,33 @@ val start_dependent_proof (** Proof entries represent a proof that has been finished, but still not registered with the kernel. - XXX: Scheduled for removal from public API, don't rely on it *) -type 'a proof_entry = private { - proof_entry_body : 'a Entries.const_entry_body; - (* List of section variables *) - proof_entry_secctx : Id.Set.t option; - (* State id on which the completion of type checking is reported *) - proof_entry_feedback : Stateid.t option; - proof_entry_type : Constr.types option; - proof_entry_universes : Entries.universes_entry; - proof_entry_opaque : bool; - proof_entry_inline_code : bool; -} - -(** XXX: Scheduled for removal from public API, don't rely on it *) -type proof_object = private - { name : Names.Id.t - (** name of the proof *) - ; entries : Evd.side_effects proof_entry list - (** list of the proof terms (in a form suitable for definitions). *) - ; uctx: UState.t - (** universe state *) - } + XXX: This is an internal, low-level API and could become scheduled + for removal from the public API, use higher-level declare APIs + instead *) +type 'a proof_entry + +(** XXX: This is an internal, low-level API and could become scheduled + for removal from the public API, use higher-level declare APIs + instead *) +type proof_object + +(** Used by the STM only to store info, should go away *) +val get_po_name : proof_object -> Id.t val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t -> proof_object (** Declaration of local constructions (Variable/Hypothesis/Local) *) -(** XXX: Scheduled for removal from public API, don't rely on it *) +(** XXX: This is an internal, low-level API and could become scheduled + for removal from the public API, use higher-level declare APIs + instead *) type variable_declaration = | SectionLocalDef of Evd.side_effects proof_entry | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; } -(** XXX: Scheduled for removal from public API, don't rely on it *) +(** XXX: This is an internal, low-level API and could become scheduled + for removal from the public API, use higher-level declare APIs + instead *) type 'a constant_entry = | DefinitionEntry of 'a proof_entry | ParameterEntry of parameter_entry @@ -144,7 +140,9 @@ val declare_variable (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... - XXX: Scheduled for removal from public API, use `DeclareDef` instead *) + XXX: This is an internal, low-level API and could become scheduled + for removal from the public API, use higher-level declare APIs + instead *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool @@ -160,7 +158,7 @@ val definition_entry -> constr -> Evd.side_effects proof_entry -type import_status = ImportDefaultBehavior | ImportNeedQualified +type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeedQualified (** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns @@ -169,7 +167,9 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified internal specify if the constant has been created by the kernel or by the user, and in the former case, if its errors should be silent - XXX: Scheduled for removal from public API, use `DeclareDef` instead *) + XXX: This is an internal, low-level API and could become scheduled + for removal from the public API, use higher-level declare APIs + instead *) val declare_constant : ?local:import_status -> name:Id.t @@ -177,17 +177,6 @@ val declare_constant -> Evd.side_effects constant_entry -> Constant.t -(** [inline_private_constants ~sideff ~uctx env ce] will inline the - constants in [ce]'s body and return the body plus the updated - [UState.t]. - - XXX: Scheduled for removal from public API, don't rely on it *) -val inline_private_constants - : uctx:UState.t - -> Environ.env - -> Evd.side_effects proof_entry - -> Constr.t * UState.t - (** Declaration messages *) (** XXX: Scheduled for removal from public API, do not use *) @@ -201,13 +190,6 @@ val check_exists : Id.t -> unit module Internal : sig - val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry - val map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entry - (* Overriding opacity is indeed really hacky *) - val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry - - val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list - type constant_obj val objConstant : constant_obj Libobject.Dyn.tag @@ -233,6 +215,7 @@ val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output Returns [false] if an unsafe tactic has been used. *) val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool +(** Semantics of this function is a bit dubious, use with care *) val build_by_tactic : ?side_eff:bool -> Environ.env @@ -260,7 +243,7 @@ val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env environment and empty evar_map. *) val get_current_context : Proof.t -> Evd.evar_map * Environ.env -(** Temporarily re-exported for 3rd party code; don't use *) +(** XXX: Temporarily re-exported for 3rd party code; don't use *) val build_constant_by_tactic : name:Names.Id.t -> ?opaque:opacity_flag -> @@ -270,11 +253,12 @@ val build_constant_by_tactic : EConstr.types -> unit Proofview.tactic -> Evd.side_effects proof_entry * bool * UState.t +[@@ocaml.deprecated "This function is deprecated, used newer API in declare"] val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit [@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"] -type locality = Discharge | Global of import_status +type locality = Locality.locality = Discharge | Global of import_status (** Declaration hooks *) module Hook : sig @@ -303,7 +287,9 @@ module Hook : sig val call : ?hook:t -> S.t -> unit end -(** Declare an interactively-defined constant *) +(** XXX: This is an internal, low-level API and could become scheduled + for removal from the public API, use higher-level declare APIs + instead *) val declare_entry : name:Id.t -> scope:locality @@ -361,6 +347,8 @@ module Recthm : sig } end +type lemma_possible_guards = int list list + val declare_mutually_recursive : opaque:bool -> scope:locality @@ -370,19 +358,16 @@ val declare_mutually_recursive -> udecl:UState.universe_decl -> ntns:Vernacexpr.decl_notation list -> rec_declaration:Constr.rec_declaration - -> possible_indexes:int list list option + -> possible_indexes:lemma_possible_guards option -> ?restrict_ucontext:bool (** XXX: restrict_ucontext should be always true, this seems like a bug in obligations, so this parameter should go away *) -> Recthm.t list -> Names.GlobRef.t list +(** Prepare API, to be removed once we provide the corresponding 1-step API *) val prepare_obligation - : ?opaque:bool - -> ?inline:bool - -> name:Id.t - -> poly:bool - -> udecl:UState.universe_decl + : name:Id.t -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map @@ -397,3 +382,208 @@ val prepare_parameter (* Compat: will remove *) exception AlreadyDeclared of (string option * Names.Id.t) + +module Obls : sig + +type 'a obligation_body = DefinedObl of 'a | TermObl of constr + +module Obligation : sig + type t = private + { obl_name : Id.t + ; obl_type : types + ; obl_location : Evar_kinds.t Loc.located + ; obl_body : pconstant obligation_body option + ; obl_status : bool * Evar_kinds.obligation_definition_status + ; obl_deps : Int.Set.t + ; obl_tac : unit Proofview.tactic option } + + val set_type : typ:Constr.types -> t -> t + val set_body : body:pconstant obligation_body -> t -> t +end + +type obligations = {obls : Obligation.t array; remaining : int} +type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint + +(* Information about a single [Program {Definition,Lemma,..}] declaration *) +module ProgramDecl : sig + type t = private + { prg_name : Id.t + ; prg_body : constr + ; prg_type : constr + ; prg_ctx : UState.t + ; prg_univdecl : UState.universe_decl + ; prg_obligations : obligations + ; prg_deps : Id.t list + ; prg_fixkind : fixpoint_kind option + ; prg_implicits : Impargs.manual_implicits + ; prg_notations : Vernacexpr.decl_notation list + ; prg_poly : bool + ; prg_scope : locality + ; prg_kind : Decls.definition_object_kind + ; prg_reduce : constr -> constr + ; prg_hook : Hook.t option + ; prg_opaque : bool } + + val make : + ?opaque:bool + -> ?hook:Hook.t + -> Names.Id.t + -> udecl:UState.universe_decl + -> uctx:UState.t + -> impargs:Impargs.manual_implicits + -> poly:bool + -> scope:locality + -> kind:Decls.definition_object_kind + -> Constr.constr option + -> Constr.types + -> Names.Id.t list + -> fixpoint_kind option + -> Vernacexpr.decl_notation list + -> RetrieveObl.obligation_info + -> (Constr.constr -> Constr.constr) + -> t + + val set_uctx : uctx:UState.t -> t -> t +end + +(** [declare_obligation prg obl ~uctx ~types ~body] Save an obligation + [obl] for program definition [prg] *) +val declare_obligation : + ProgramDecl.t + -> Obligation.t + -> uctx:UState.t + -> types:Constr.types option + -> body:Constr.types + -> bool * Obligation.t + +module State : sig + + val num_pending : unit -> int + val first_pending : unit -> ProgramDecl.t option + + (** Returns [Error duplicate_list] if not a single program is open *) + val get_unique_open_prog : + Id.t option -> (ProgramDecl.t, Id.t list) result + + (** Add a new obligation *) + val add : Id.t -> ProgramDecl.t -> unit + + val fold : f:(Id.t -> ProgramDecl.t -> 'a -> 'a) -> init:'a -> 'a + + val all : unit -> ProgramDecl.t list + + val find : Id.t -> ProgramDecl.t option + + (* Internal *) + type t + val prg_tag : t Summary.Dyn.tag +end + +val declare_definition : ProgramDecl.t -> Names.GlobRef.t + +(** Resolution status of a program *) +type progress = + | Remain of int (** n obligations remaining *) + | Dependent (** Dependent on other definitions *) + | Defined of GlobRef.t (** Defined as id *) + +type obligation_resolver = + Id.t option + -> Int.Set.t + -> unit Proofview.tactic option + -> progress + +type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver} + +(** [update_obls prg obls n progress] What does this do? *) +val update_obls : + ProgramDecl.t -> Obligation.t array -> int -> progress + +(** Check obligations are properly solved before closing the + [what_for] section / module *) +val check_solved_obligations : what_for:Pp.t -> unit + +(** { 2 Util } *) + +val obl_substitution : + bool + -> Obligation.t array + -> Int.Set.t + -> (Id.t * (Constr.types * Constr.types)) list + +val dependencies : Obligation.t array -> int -> Int.Set.t + +(* This is a hack to make it possible for Obligations to craft a Qed + * behind the scenes. The fix_exn the Stm attaches to the Future proof + * is not available here, so we provide a side channel to get it *) +val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) ref + +end + +(** Creating high-level proofs with an associated constant *) +module Proof_ending : sig + + type t = + | Regular + | End_obligation of Obls.obligation_qed_info + | End_derive of { f : Id.t; name : Id.t } + | End_equations of + { hook : Constant.t list -> Evd.evar_map -> unit + ; i : Id.t + ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list + ; sigma : Evd.evar_map + } + +end + +module Info : sig + type t + val make + : ?hook: Hook.t + (** Callback to be executed at the end of the proof *) + -> ?proof_ending : Proof_ending.t + (** Info for special constants *) + -> ?scope : locality + (** locality *) + -> ?kind:Decls.logical_kind + (** Theorem, etc... *) + -> ?compute_guard:lemma_possible_guards + -> ?thms:Recthm.t list + (** Both of those are internal, used by the upper layers but will + become handled natively here in the future *) + -> unit + -> t + + (* Internal; used to initialize non-mutual proofs *) + val add_first_thm : + info:t + -> name:Id.t + -> typ:EConstr.t + -> impargs:Impargs.manual_implicits + -> t +end + +val save_lemma_proved + : proof:Proof.t + -> info:Info.t + -> opaque:opacity_flag + -> idopt:Names.lident option + -> unit + +val save_lemma_admitted : + proof:Proof.t + -> info:Info.t + -> unit + +(** Special cases for delayed proofs, in this case we must provide the + proof information so the proof won't be forced. *) +val save_lemma_admitted_delayed : + proof:proof_object + -> info:Info.t + -> unit + +val save_lemma_proved_delayed + : proof:proof_object + -> info:Info.t + -> idopt:Names.lident option + -> unit diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml deleted file mode 100644 index 9ea54f5d8f..0000000000 --- a/vernac/declareObl.ml +++ /dev/null @@ -1,578 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Util -open Names -open Environ -open Context -open Constr -open Vars -open Entries - -type 'a obligation_body = DefinedObl of 'a | TermObl of constr - -module Obligation = struct - type t = - { obl_name : Id.t - ; obl_type : types - ; obl_location : Evar_kinds.t Loc.located - ; obl_body : pconstant obligation_body option - ; obl_status : bool * Evar_kinds.obligation_definition_status - ; obl_deps : Int.Set.t - ; obl_tac : unit Proofview.tactic option } - - let set_type ~typ obl = { obl with obl_type = typ } - let set_body ~body obl = { obl with obl_body = Some body } - -end - -type obligations = - { obls : Obligation.t array - ; remaining : int } - -type fixpoint_kind = - | IsFixpoint of lident option list - | IsCoFixpoint - -module ProgramDecl = struct - - type t = - { prg_name : Id.t - ; prg_body : constr - ; prg_type : constr - ; prg_ctx : UState.t - ; prg_univdecl : UState.universe_decl - ; prg_obligations : obligations - ; prg_deps : Id.t list - ; prg_fixkind : fixpoint_kind option - ; prg_implicits : Impargs.manual_implicits - ; prg_notations : Vernacexpr.decl_notation list - ; prg_poly : bool - ; prg_scope : Declare.locality - ; prg_kind : Decls.definition_object_kind - ; prg_reduce : constr -> constr - ; prg_hook : Declare.Hook.t option - ; prg_opaque : bool - } - - open Obligation - - let make ?(opaque = false) ?hook n ~udecl ~uctx ~impargs - ~poly ~scope ~kind b t deps fixkind notations obls reduce = - let obls', b = - match b with - | None -> - assert(Int.equal (Array.length obls) 0); - let n = Nameops.add_suffix n "_obligation" in - [| { obl_name = n; obl_body = None; - obl_location = Loc.tag Evar_kinds.InternalHole; obl_type = t; - obl_status = false, Evar_kinds.Expand; obl_deps = Int.Set.empty; - obl_tac = None } |], - mkVar n - | Some b -> - Array.mapi - (fun i (n, t, l, o, d, tac) -> - { obl_name = n ; obl_body = None; - obl_location = l; obl_type = t; obl_status = o; - obl_deps = d; obl_tac = tac }) - obls, b - in - let ctx = UState.make_flexible_nonalgebraic uctx in - { prg_name = n - ; prg_body = b - ; prg_type = reduce t - ; prg_ctx = ctx - ; prg_univdecl = udecl - ; prg_obligations = { obls = obls' ; remaining = Array.length obls' } - ; prg_deps = deps - ; prg_fixkind = fixkind - ; prg_notations = notations - ; prg_implicits = impargs - ; prg_poly = poly - ; prg_scope = scope - ; prg_kind = kind - ; prg_reduce = reduce - ; prg_hook = hook - ; prg_opaque = opaque - } - - let set_uctx ~uctx prg = {prg with prg_ctx = uctx} -end - -open Obligation -open ProgramDecl - -(* Saving an obligation *) - -(* XXX: Is this the right place for this? *) -let it_mkLambda_or_LetIn_or_clean t ctx = - let open Context.Rel.Declaration in - let fold t decl = - if is_local_assum decl then Term.mkLambda_or_LetIn decl t - else if noccurn 1 t then subst1 mkProp t - else Term.mkLambda_or_LetIn decl t - in - Context.Rel.fold_inside fold ctx ~init:t - -(* XXX: Is this the right place for this? *) -let decompose_lam_prod c ty = - let open Context.Rel.Declaration in - let rec aux ctx c ty = - match (Constr.kind c, Constr.kind ty) with - | LetIn (x, b, t, c), LetIn (x', b', t', ty) - when Constr.equal b b' && Constr.equal t t' -> - let ctx' = Context.Rel.add (LocalDef (x, b', t')) ctx in - aux ctx' c ty - | _, LetIn (x', b', t', ty) -> - let ctx' = Context.Rel.add (LocalDef (x', b', t')) ctx in - aux ctx' (lift 1 c) ty - | LetIn (x, b, t, c), _ -> - let ctx' = Context.Rel.add (LocalDef (x, b, t)) ctx in - aux ctx' c (lift 1 ty) - | Lambda (x, b, t), Prod (x', b', t') - (* By invariant, must be convertible *) -> - let ctx' = Context.Rel.add (LocalAssum (x, b')) ctx in - aux ctx' t t' - | Cast (c, _, _), _ -> aux ctx c ty - | _, _ -> (ctx, c, ty) - in - aux Context.Rel.empty c ty - -(* XXX: What's the relation of this with Abstract.shrink ? *) -let shrink_body c ty = - let ctx, b, ty = - match ty with - | None -> - let ctx, b = Term.decompose_lam_assum c in - (ctx, b, None) - | Some ty -> - let ctx, b, ty = decompose_lam_prod c ty in - (ctx, b, Some ty) - in - let b', ty', n, args = - List.fold_left - (fun (b, ty, i, args) decl -> - if noccurn 1 b && Option.cata (noccurn 1) true ty then - (subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args) - else - let open Context.Rel.Declaration in - let args = if is_local_assum decl then mkRel i :: args else args in - ( Term.mkLambda_or_LetIn decl b - , Option.map (Term.mkProd_or_LetIn decl) ty - , succ i - , args ) ) - (b, ty, 1, []) ctx - in - (ctx, b', ty', Array.of_list args) - -(***********************************************************************) -(* Saving an obligation *) -(***********************************************************************) - -let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] - -let add_hint local prg cst = - let locality = if local then Goptions.OptLocal else Goptions.OptExport in - Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst) - -(* true = hide obligations *) -let get_hide_obligations = - Goptions.declare_bool_option_and_ref - ~depr:true - ~key:["Hide"; "Obligations"] - ~value:false - -let declare_obligation prg obl body ty uctx = - let body = prg.prg_reduce body in - let ty = Option.map prg.prg_reduce ty in - match obl.obl_status with - | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)}) - | force, Evar_kinds.Define opaque -> - let opaque = (not force) && opaque in - let poly = prg.prg_poly in - let ctx, body, ty, args = - if not poly then shrink_body body ty - else ([], body, ty, [||]) - in - let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in - - (* ppedrot: seems legit to have obligations as local *) - let constant = - Declare.declare_constant ~name:obl.obl_name - ~local:Declare.ImportNeedQualified ~kind:Decls.(IsProof Property) - (Declare.DefinitionEntry ce) - in - if not opaque then - add_hint (Locality.make_section_locality None) prg constant; - Declare.definition_message obl.obl_name; - let body = - match uctx with - | Polymorphic_entry (_, uctx) -> - Some (DefinedObl (constant, Univ.UContext.instance uctx)) - | Monomorphic_entry _ -> - Some - (TermObl - (it_mkLambda_or_LetIn_or_clean - (mkApp (mkConst constant, args)) - ctx)) - in - (true, {obl with obl_body = body}) - -(* Updating the obligation meta-info on close *) - -let not_transp_msg = - Pp.( - str "Obligation should be transparent but was declared opaque." - ++ spc () - ++ str "Use 'Defined' instead.") - -let pperror cmd = CErrors.user_err ~hdr:"Program" cmd -let err_not_transp () = pperror not_transp_msg - -module ProgMap = Id.Map - -let from_prg, program_tcc_summary_tag = - Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" - -(* In all cases, the use of the map is read-only so we don't expose the ref *) -let get_prg_info_map () = !from_prg - -let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] - -let check_can_close sec = - if not (ProgMap.is_empty !from_prg) then - let keys = map_keys !from_prg in - CErrors.user_err ~hdr:"Program" - Pp.( - str "Unsolved obligations when closing " - ++ Id.print sec ++ str ":" ++ spc () - ++ prlist_with_sep spc (fun x -> Id.print x) keys - ++ ( str (if Int.equal (List.length keys) 1 then " has " else " have ") - ++ str "unsolved obligations" )) - -let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) -let prgmap_op f = from_prg := f !from_prg -let progmap_remove prg = prgmap_op (ProgMap.remove prg.prg_name) -let progmap_add n prg = prgmap_op (ProgMap.add n prg) -let progmap_replace prg = prgmap_op (map_replace prg.prg_name prg) - -let obligations_solved prg = Int.equal prg.prg_obligations.remaining 0 - -let obligations_message rem = - if rem > 0 then - if Int.equal rem 1 then - Flags.if_verbose Feedback.msg_info - Pp.(int rem ++ str " obligation remaining") - else - Flags.if_verbose Feedback.msg_info - Pp.(int rem ++ str " obligations remaining") - else - Flags.if_verbose Feedback.msg_info Pp.(str "No more obligations remaining") - -type progress = Remain of int | Dependent | Defined of GlobRef.t - -let get_obligation_body expand obl = - match obl.obl_body with - | None -> None - | Some c -> ( - if expand && snd obl.obl_status == Evar_kinds.Expand then - match c with - | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc) - | TermObl c -> Some c - else - match c with DefinedObl pc -> Some (mkConstU pc) | TermObl c -> Some c ) - -let obl_substitution expand obls deps = - Int.Set.fold - (fun x acc -> - let xobl = obls.(x) in - match get_obligation_body expand xobl with - | None -> acc - | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc ) - deps [] - -let rec intset_to = function - | -1 -> Int.Set.empty - | n -> Int.Set.add n (intset_to (pred n)) - -let obligation_substitution expand prg = - let obls = prg.prg_obligations.obls in - let ints = intset_to (pred (Array.length obls)) in - obl_substitution expand obls ints - -let hide_obligation () = - Coqlib.check_required_library ["Coq"; "Program"; "Tactics"]; - UnivGen.constr_of_monomorphic_global - (Coqlib.lib_ref "program.tactics.obligation") - -(* XXX: Is this the right place? *) -let rec prod_app t n = - match - Constr.kind - (EConstr.Unsafe.to_constr - (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) - (* FIXME *) - with - | Prod (_, _, b) -> subst1 n b - | LetIn (_, b, t, b') -> prod_app (subst1 b b') n - | _ -> - CErrors.user_err ~hdr:"prod_app" - Pp.(str "Needed a product, but didn't find one" ++ fnl ()) - -(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) -let prod_applist t nL = List.fold_left prod_app t nL - -let replace_appvars subst = - let rec aux c = - let f, l = decompose_app c in - if isVar f then - try - let c' = List.map (Constr.map aux) l in - let t, b = Id.List.assoc (destVar f) subst in - mkApp - ( delayed_force hide_obligation - , [|prod_applist t c'; Term.applistc b c'|] ) - with Not_found -> Constr.map aux c - else Constr.map aux c - in - Constr.map aux - -let subst_prog subst prg = - if get_hide_obligations () then - ( replace_appvars subst prg.prg_body - , replace_appvars subst (* Termops.refresh_universes *) prg.prg_type ) - else - let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in - ( Vars.replace_vars subst' prg.prg_body - , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type ) - -let get_fix_exn, stm_get_fix_exn = Hook.make () - -let declare_definition prg = - let varsubst = obligation_substitution true prg in - let sigma = Evd.from_ctx prg.prg_ctx in - let body, types = subst_prog varsubst prg in - let body, types = EConstr.(of_constr body, Some (of_constr types)) in - (* All these should be grouped into a struct a some point *) - let opaque, poly, udecl, hook = prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook in - let name, scope, kind, impargs = prg.prg_name, prg.prg_scope, Decls.(IsDefinition prg.prg_kind), prg.prg_implicits in - let fix_exn = Hook.get get_fix_exn () in - let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in - (* XXX: This is doing normalization twice *) - let () = progmap_remove prg in - let kn = - Declare.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls - ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma - in - kn - -let rec lam_index n t acc = - match Constr.kind t with - | Lambda ({binder_name=Name n'}, _, _) when Id.equal n n' -> acc - | Lambda (_, _, b) -> lam_index n b (succ acc) - | _ -> raise Not_found - -let compute_possible_guardness_evidences n fixbody fixtype = - match n with - | Some {CAst.loc; v = n} -> [lam_index n fixbody 0] - | None -> - (* If recursive argument was not given by user, we try all args. - An earlier approach was to look only for inductive arguments, - but doing it properly involves delta-reduction, and it finally - doesn't seem to worth the effort (except for huge mutual - fixpoints ?) *) - let m = - Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) - (* FIXME *) - in - let ctx = fst (Term.decompose_prod_n_assum m fixtype) in - List.map_i (fun i _ -> i) 0 ctx - -let declare_mutual_definition l = - let len = List.length l in - let first = List.hd l in - let defobl x = - let oblsubst = obligation_substitution true x in - let subs, typ = subst_prog oblsubst x in - let env = Global.env () in - let sigma = Evd.from_ctx x.prg_ctx in - let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in - let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in - let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in - let term = EConstr.to_constr sigma term in - let typ = EConstr.to_constr sigma typ in - let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in - let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in - def, oblsubst - in - let defs, obls = - List.fold_right (fun x (defs, obls) -> - let xdef, xobls = defobl x in - (xdef :: defs, xobls @ obls)) l ([], []) - in - (* let fixdefs = List.map reduce_fix fixdefs in *) - let fixdefs, fixrs, fixtypes, fixitems = - List.fold_right2 (fun (d,r,typ,impargs) name (a1,a2,a3,a4) -> - d :: a1, r :: a2, typ :: a3, - Declare.Recthm.{ name; typ; impargs; args = [] } :: a4 - ) defs first.prg_deps ([],[],[],[]) - in - let fixkind = Option.get first.prg_fixkind in - let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in - let rvec = Array.of_list fixrs in - let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in - let rec_declaration = (Array.map2 make_annot namevec rvec, arrrec, recvec) in - let possible_indexes = - match fixkind with - | IsFixpoint wfl -> - Some (List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes) - | IsCoFixpoint -> None - in - (* In the future we will pack all this in a proper record *) - let poly, scope, ntns, opaque = first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque in - let kind = if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) else Decls.(IsDefinition CoFixpoint) in - (* Declare the recursive definitions *) - let udecl = UState.default_univ_decl in - let kns = - Declare.declare_mutually_recursive ~scope ~opaque ~kind - ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly - ~restrict_ucontext:false fixitems - in - (* Only for the first constant *) - let dref = List.hd kns in - Declare.Hook.(call ?hook:first.prg_hook { S.uctx = first.prg_ctx; obls; scope; dref }); - List.iter progmap_remove l; - dref - -let update_obls prg obls rem = - let prg_obligations = { obls; remaining = rem } in - let prg' = {prg with prg_obligations} in - progmap_replace prg'; - obligations_message rem; - if rem > 0 then Remain rem - else - match prg'.prg_deps with - | [] -> - let kn = declare_definition prg' in - progmap_remove prg'; - Defined kn - | l -> - let progs = - List.map - (fun x -> CEphemeron.get (ProgMap.find x !from_prg)) - prg'.prg_deps - in - if List.for_all (fun x -> obligations_solved x) progs then - let kn = declare_mutual_definition progs in - Defined kn - else Dependent - -let dependencies obls n = - let res = ref Int.Set.empty in - Array.iteri - (fun i obl -> - if (not (Int.equal i n)) && Int.Set.mem n obl.obl_deps then - res := Int.Set.add i !res ) - obls; - !res - -let update_program_decl_on_defined prg obls num obl ~uctx rem ~auto = - let obls = Array.copy obls in - let () = obls.(num) <- obl in - let prg = { prg with prg_ctx = uctx } in - let () = ignore (update_obls prg obls (pred rem)) in - if pred rem > 0 then begin - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then - ignore (auto (Some prg.prg_name) deps None) - end - -type obligation_qed_info = - { name : Id.t - ; num : int - ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress - } - -let obligation_terminator entries uctx { name; num; auto } = - match entries with - | [entry] -> - let env = Global.env () in - let ty = entry.Declare.proof_entry_type in - let body, uctx = Declare.inline_private_constants ~uctx env entry in - let sigma = Evd.from_ctx uctx in - Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); - (* Declare the obligation ourselves and drop the hook *) - let prg = CEphemeron.get (ProgMap.find name !from_prg) in - let { obls; remaining=rem } = prg.prg_obligations in - let obl = obls.(num) in - let status = - match obl.obl_status, entry.Declare.proof_entry_opaque with - | (_, Evar_kinds.Expand), true -> err_not_transp () - | (true, _), true -> err_not_transp () - | (false, _), true -> Evar_kinds.Define true - | (_, Evar_kinds.Define true), false -> - Evar_kinds.Define false - | (_, status), false -> status - in - let obl = { obl with obl_status = false, status } in - let uctx = - if prg.prg_poly then uctx - else UState.union prg.prg_ctx uctx - in - let univs = UState.univ_entry ~poly:prg.prg_poly uctx in - let (defined, obl) = declare_obligation prg obl body ty univs in - let prg_ctx = - if prg.prg_poly then (* Polymorphic *) - (* We merge the new universes and constraints of the - polymorphic obligation with the existing ones *) - UState.union prg.prg_ctx uctx - else - (* The first obligation, if defined, - declares the univs of the constant, - each subsequent obligation declares its own additional - universes and constraints if any *) - if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) - else uctx - in - update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto - | _ -> - CErrors.anomaly - Pp.( - str - "[obligation_terminator] close_proof returned more than one proof \ - term") - -(* Similar to the terminator but for interactive paths, as the - terminator is only called in interactive proof mode *) -let obligation_hook prg obl num auto { Declare.Hook.S.uctx = ctx'; dref; _ } = - let { obls; remaining=rem } = prg.prg_obligations in - let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in - let transparent = evaluable_constant cst (Global.env ()) in - let () = match obl.obl_status with - (true, Evar_kinds.Expand) - | (true, Evar_kinds.Define true) -> - if not transparent then err_not_transp () - | _ -> () - in - let inst, ctx' = - if not prg.prg_poly (* Not polymorphic *) then - (* The universe context was declared globally, we continue - from the new global environment. *) - let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in - let ctx' = UState.merge_subst ctx (UState.subst ctx') in - Univ.Instance.empty, ctx' - else - (* We get the right order somehow, but surely it could be enforced in a clearer way. *) - let uctx = UState.context ctx' in - Univ.UContext.instance uctx, ctx' - in - let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in - let () = if transparent then add_hint true prg cst in - update_program_decl_on_defined prg obls num obl ~uctx:ctx' rem ~auto diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli deleted file mode 100644 index 03f0a57bcb..0000000000 --- a/vernac/declareObl.mli +++ /dev/null @@ -1,164 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Constr - -type 'a obligation_body = DefinedObl of 'a | TermObl of constr - -module Obligation : sig - - type t = private - { obl_name : Id.t - ; obl_type : types - ; obl_location : Evar_kinds.t Loc.located - ; obl_body : pconstant obligation_body option - ; obl_status : bool * Evar_kinds.obligation_definition_status - ; obl_deps : Int.Set.t - ; obl_tac : unit Proofview.tactic option } - - val set_type : typ:Constr.types -> t -> t - val set_body : body:pconstant obligation_body -> t -> t - -end - -type obligations = - { obls : Obligation.t array - ; remaining : int } - -type fixpoint_kind = - | IsFixpoint of lident option list - | IsCoFixpoint - -(* Information about a single [Program {Definition,Lemma,..}] declaration *) -module ProgramDecl : sig - - type t = private - { prg_name : Id.t - ; prg_body : constr - ; prg_type : constr - ; prg_ctx : UState.t - ; prg_univdecl : UState.universe_decl - ; prg_obligations : obligations - ; prg_deps : Id.t list - ; prg_fixkind : fixpoint_kind option - ; prg_implicits : Impargs.manual_implicits - ; prg_notations : Vernacexpr.decl_notation list - ; prg_poly : bool - ; prg_scope : Declare.locality - ; prg_kind : Decls.definition_object_kind - ; prg_reduce : constr -> constr - ; prg_hook : Declare.Hook.t option - ; prg_opaque : bool - } - - val make : - ?opaque:bool - -> ?hook:Declare.Hook.t - -> Names.Id.t - -> udecl:UState.universe_decl - -> uctx:UState.t - -> impargs:Impargs.manual_implicits - -> poly:bool - -> scope:Declare.locality - -> kind:Decls.definition_object_kind - -> Constr.constr option - -> Constr.types - -> Names.Id.t list - -> fixpoint_kind option - -> Vernacexpr.decl_notation list - -> ( Names.Id.t - * Constr.types - * Evar_kinds.t Loc.located - * (bool * Evar_kinds.obligation_definition_status) - * Int.Set.t - * unit Proofview.tactic option ) - array - -> (Constr.constr -> Constr.constr) - -> t - - val set_uctx : uctx:UState.t -> t -> t -end - -val declare_obligation : - ProgramDecl.t - -> Obligation.t - -> Constr.types - -> Constr.types option - -> Entries.universes_entry - -> bool * Obligation.t -(** [declare_obligation] Save an obligation *) - -module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set - -val declare_definition : ProgramDecl.t -> Names.GlobRef.t - -(** Resolution status of a program *) -type progress = - | Remain of int - (** n obligations remaining *) - | Dependent - (** Dependent on other definitions *) - | Defined of GlobRef.t - (** Defined as id *) - -type obligation_qed_info = - { name : Id.t - ; num : int - ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress - } - -val obligation_terminator - : Evd.side_effects Declare.proof_entry list - -> UState.t - -> obligation_qed_info -> unit -(** [obligation_terminator] part 2 of saving an obligation, proof mode *) - -val obligation_hook - : ProgramDecl.t - -> Obligation.t - -> Int.t - -> (Names.Id.t option -> Int.Set.t -> 'a option -> 'b) - -> Declare.Hook.S.t - -> unit -(** [obligation_hook] part 2 of saving an obligation, non-interactive mode *) - -val update_obls : - ProgramDecl.t - -> Obligation.t array - -> int - -> progress -(** [update_obls prg obls n progress] What does this do? *) - -(** { 2 Util } *) - -(** Check obligations are properly solved before closing a section *) -val check_can_close : Id.t -> unit - -val get_prg_info_map : unit -> ProgramDecl.t CEphemeron.key ProgMap.t - -val program_tcc_summary_tag : - ProgramDecl.t CEphemeron.key Id.Map.t Summary.Dyn.tag - -val obl_substitution : - bool - -> Obligation.t array - -> Int.Set.t - -> (ProgMap.key * (Constr.types * Constr.types)) list - -val dependencies : Obligation.t array -> int -> Int.Set.t - -val err_not_transp : unit -> unit -val progmap_add : ProgMap.key -> ProgramDecl.t CEphemeron.key -> unit - -(* This is a hack to make it possible for Obligations to craft a Qed - * behind the scenes. The fix_exn the Stm attaches to the Future proof - * is not available here, so we provide a side channel to get it *) -val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 42259cee10..45bf61d79e 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -35,11 +35,16 @@ open Attributes let query_command = Entry.create "vernac:query_command" +let search_query = Entry.create "vernac:search_query" +let search_queries = Entry.create "vernac:search_queries" + let subprf = Entry.create "vernac:subprf" let quoted_attributes = Entry.create "vernac:quoted_attributes" let class_rawexpr = Entry.create "vernac:class_rawexpr" let thm_token = Entry.create "vernac:thm_token" +let def_token = Entry.create "vernac:def_token" +let assumption_token = Entry.create "vernac:assumption_token" let def_body = Entry.create "vernac:def_body" let decl_notations = Entry.create "vernac:decl_notations" let record_field = Entry.create "vernac:record_field" @@ -70,6 +75,13 @@ let test_hash_ident = to_entry "test_hash_ident" begin lk_kw "#" >> lk_ident >> check_no_space end + +let test_id_colon = + let open Pcoq.Lookahead in + to_entry "test_id_colon" begin + lk_ident >> lk_kw ":" + end + } GRAMMAR EXTEND Gram @@ -183,7 +195,7 @@ let name_of_ident_decl : ident_decl -> name_decl = (* Gallina declarations *) GRAMMAR EXTEND Gram - GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion + GLOBAL: gallina gallina_ext thm_token def_token assumption_token def_body of_type_with_opt_coercion record_field decl_notations rec_definition ident_decl univ_decl; gallina: @@ -810,7 +822,7 @@ GRAMMAR EXTEND Gram END GRAMMAR EXTEND Gram - GLOBAL: command query_command class_rawexpr gallina_ext; + GLOBAL: command query_command class_rawexpr gallina_ext search_query search_queries; gallina_ext: [ [ IDENT "Export"; "Set"; table = option_table; v = option_setting -> @@ -915,7 +927,7 @@ GRAMMAR EXTEND Gram { fun g -> VernacSearch (SearchPattern c,g, l) } | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." -> { fun g -> VernacSearch (SearchRewrite c,g, l) } - | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> + | IDENT "Search"; s = search_query; l = search_queries; "." -> { let (sl,m) = l in fun g -> VernacSearch (Search (s::sl),g, m) } ] ] ; @@ -1012,16 +1024,50 @@ GRAMMAR EXTEND Gram positive_search_mark: [ [ "-" -> { false } | -> { true } ] ] ; - searchabout_query: - [ [ b = positive_search_mark; s = ne_string; sc = OPT scope_delimiter -> - { (b, SearchString (s,sc)) } - | b = positive_search_mark; p = constr_pattern -> - { (b, SearchSubPattern p) } + search_query: + [ [ b = positive_search_mark; s = search_item -> { (b, SearchLiteral s) } + | b = positive_search_mark; "["; l = LIST1 (LIST1 search_query) SEP "|"; "]" -> { (b, SearchDisjConj l) } + ] ] + ; + search_item: + [ [ test_id_colon; where = search_where; ":"; s = ne_string; sc = OPT scope_delimiter -> + { SearchString (where,s,sc) } + | IDENT "is"; ":"; kl = logical_kind -> + { SearchKind kl } + | s = ne_string; sc = OPT scope_delimiter -> + { SearchString ((Anywhere,false),s,sc) } + | test_id_colon; where = search_where; ":"; p = constr_pattern -> + { SearchSubPattern (where,p) } + | p = constr_pattern -> + { SearchSubPattern ((Anywhere,false),p) } ] ] ; - searchabout_queries: + logical_kind: + [ [ k = thm_token -> { IsProof k } + | k = assumption_token -> { IsAssumption (snd k) } + | k = IDENT "Context" -> { IsAssumption Context } + | k = extended_def_token -> { IsDefinition k } + | IDENT "Primitive" -> { IsPrimitive } ] ] + ; + extended_def_token: + [ [ k = def_token -> { snd k } + | IDENT "Coercion" -> { Coercion } + | IDENT "Instance" -> { Instance } + | IDENT "Scheme" -> { Scheme } + | IDENT "Canonical" -> { CanonicalStructure } + | IDENT "Field" -> { StructureComponent } + | IDENT "Method" -> { Method } ] ] + ; + search_where: + [ [ IDENT "head" -> { Anywhere, true } + | IDENT "hyp" -> { InHyp, false } + | IDENT "concl" -> { InConcl, false } + | IDENT "headhyp" -> { InHyp, true } + | IDENT "headconcl" -> { InConcl, true } ] ] + ; + search_queries: [ [ m = ne_in_or_out_modules -> { ([],m) } - | s = searchabout_query; l = searchabout_queries -> + | s = search_query; l = search_queries -> { let (sl,m) = l in (s::sl,m) } | -> { ([],SearchOutside []) } ] ] diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 838496c595..10d63ff2ff 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -12,7 +12,6 @@ file command.ml, Aug 2009 *) open Util -open Names module NamedDecl = Context.Named.Declaration @@ -21,44 +20,8 @@ module NamedDecl = Context.Named.Declaration type lemma_possible_guards = int list list -module Proof_ending = struct - - type t = - | Regular - | End_obligation of DeclareObl.obligation_qed_info - | End_derive of { f : Id.t; name : Id.t } - | End_equations of - { hook : Constant.t list -> Evd.evar_map -> unit - ; i : Id.t - ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list - ; sigma : Evd.evar_map - } - -end - -module Info = struct - - type t = - { hook : Declare.Hook.t option - ; proof_ending : Proof_ending.t CEphemeron.key - (* This could be improved and the CEphemeron removed *) - ; scope : Declare.locality - ; kind : Decls.logical_kind - (* thms and compute guard are specific only to start_lemma_with_initialization + regular terminator *) - ; thms : Declare.Recthm.t list - ; compute_guard : lemma_possible_guards - } - - let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Declare.Global Declare.ImportDefaultBehavior) - ?(kind=Decls.(IsProof Lemma)) () = - { hook - ; compute_guard = [] - ; proof_ending = CEphemeron.create proof_ending - ; thms = [] - ; scope - ; kind - } -end +module Proof_ending = Declare.Proof_ending +module Info = Declare.Info (* Proofs with a save constant function *) type t = @@ -96,15 +59,6 @@ let initialize_named_context_for_proof () = let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val -let add_first_thm ~info ~name ~typ ~impargs = - let thms = - { Declare.Recthm.name - ; impargs - ; typ = EConstr.Unsafe.to_constr typ - ; args = [] } :: info.Info.thms - in - { info with Info.thms } - (* Starting a goal *) let start_lemma ~name ~poly ?(udecl=UState.default_univ_decl) @@ -114,7 +68,7 @@ let start_lemma ~name ~poly let sign = initialize_named_context_for_proof () in let goals = [ Global.env_of_context sign , c ] in let proof = Declare.start_proof sigma ~name ~udecl ~poly goals in - let info = add_first_thm ~info ~name ~typ:c ~impargs in + let info = Declare.Info.add_first_thm ~info ~name ~typ:c ~impargs in { proof; info } (* Note that proofs opened by start_dependent lemma cannot be closed @@ -162,276 +116,15 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua match thms with | [] -> CErrors.anomaly (Pp.str "No proof to start.") | { Declare.Recthm.name; typ; impargs; _} :: thms -> - let info = - Info.{ hook - ; compute_guard - ; proof_ending = CEphemeron.create Proof_ending.Regular - ; thms - ; scope - ; kind - } in + let info = Info.make ?hook ~scope ~kind ~compute_guard ~thms () in (* start_lemma has the responsibility to add (name, impargs, typ) to thms, once Info.t is more refined this won't be necessary *) let lemma = start_lemma ~name ~impargs ~poly ~udecl ~info sigma (EConstr.of_constr typ) in pf_map (Declare.Proof.map_proof (fun p -> pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)) lemma -(************************************************************************) -(* Commom constant saving path, for both Qed and Admitted *) -(************************************************************************) - -(* Support for mutually proved theorems *) - -(* XXX: Most of this does belong to Declare, due to proof_entry manip *) -module MutualEntry : sig - - val declare_variable - : info:Info.t - -> uctx:UState.t - -> Entries.parameter_entry - -> Names.GlobRef.t list - - val declare_mutdef - (* Common to all recthms *) - : info:Info.t - -> uctx:UState.t - -> Evd.side_effects Declare.proof_entry - -> Names.GlobRef.t list - -end = struct - - (* XXX: Refactor this with the code in [Declare.declare_mutdef] *) - let guess_decreasing env possible_indexes ((body, ctx), eff) = - let open Constr in - match Constr.kind body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> - let env = Safe_typing.push_private_constants env eff.Evd.seff_private in - let indexes = Pretyping.search_guard env possible_indexes fixdecls in - (mkFix ((indexes,0),fixdecls), ctx), eff - | _ -> (body, ctx), eff - - let select_body i t = - let open Constr in - match Constr.kind t with - | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) - | CoFix (0,decls) -> mkCoFix (i,decls) - | _ -> - CErrors.anomaly - Pp.(str "Not a proof by induction: " ++ - Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".") - - let declare_mutdef ~uctx ~info pe i Declare.Recthm.{ name; impargs; typ; _} = - let { Info.hook; scope; kind; compute_guard; _ } = info in - (* if i = 0 , we don't touch the type; this is for compat - but not clear it is the right thing to do. - *) - let pe, ubind = - if i > 0 && not (CList.is_empty compute_guard) - then Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ), UnivNames.empty_binders - else pe, UState.universe_binders uctx - in - (* We when compute_guard was [] in the previous step we should not - substitute the body *) - let pe = match compute_guard with - | [] -> pe - | _ -> - Declare.Internal.map_entry_body pe - ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) - in - Declare.declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe - - let declare_mutdef ~info ~uctx const = - let pe = match info.Info.compute_guard with - | [] -> - (* Not a recursive statement *) - const - | possible_indexes -> - (* Try all combinations... not optimal *) - let env = Global.env() in - Declare.Internal.map_entry_body const - ~f:(guess_decreasing env possible_indexes) - in - List.map_i (declare_mutdef ~info ~uctx pe) 0 info.Info.thms - - let declare_variable ~info ~uctx pe = - let { Info.scope; hook } = info in - List.map_i ( - fun i { Declare.Recthm.name; typ; impargs } -> - Declare.declare_assumption ~name ~scope ~hook ~impargs ~uctx pe - ) 0 info.Info.thms - -end - -(************************************************************************) -(* Admitting a lemma-like constant *) -(************************************************************************) - -(* Admitted *) -let get_keep_admitted_vars = - Goptions.declare_bool_option_and_ref - ~depr:false - ~key:["Keep"; "Admitted"; "Variables"] - ~value:true - -let compute_proof_using_for_admitted proof typ pproofs = - if not (get_keep_admitted_vars ()) then None - else match Declare.Proof.get_used_variables proof, pproofs with - | Some _ as x, _ -> x - | None, pproof :: _ -> - let env = Global.env () in - let ids_typ = Environ.global_vars_set env typ in - (* [pproof] is evar-normalized by [partial_proof]. We don't - count variables appearing only in the type of evars. *) - let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in - Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) - | _ -> None - -let finish_admitted ~info ~uctx pe = - let _r : Names.GlobRef.t list = MutualEntry.declare_variable ~info ~uctx pe in - () - -let save_lemma_admitted ~(lemma : t) : unit = - let udecl = Declare.Proof.get_universe_decl lemma.proof in - let Proof.{ poly; entry } = Proof.data (Declare.Proof.get_proof lemma.proof) in - let typ = match Proofview.initial_goals entry with - | [typ] -> snd typ - | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.") - in - let typ = EConstr.Unsafe.to_constr typ in - let proof = Declare.Proof.get_proof lemma.proof in - let pproofs = Proof.partial_proof proof in - let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in - let uctx = Declare.Proof.get_initial_euctx lemma.proof in - let univs = UState.check_univ_decl ~poly uctx udecl in - finish_admitted ~info:lemma.info ~uctx (sec_vars, (typ, univs), None) - -(************************************************************************) -(* Saving a lemma-like constant *) -(************************************************************************) - -let finish_proved po info = - let open Declare in - match po with - | { entries=[const]; uctx } -> - let _r : Names.GlobRef.t list = MutualEntry.declare_mutdef ~info ~uctx const in - () - | _ -> - CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term") - -let finish_derived ~f ~name ~entries = - (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *) - - let f_def, lemma_def = - match entries with - | [_;f_def;lemma_def] -> - f_def, lemma_def - | _ -> assert false - in - (* The opacity of [f_def] is adjusted to be [false], as it - must. Then [f] is declared in the global environment. *) - let f_def = Declare.Internal.set_opacity ~opaque:false f_def in - let f_kind = Decls.(IsDefinition Definition) in - let f_def = Declare.DefinitionEntry f_def in - let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in - let f_kn_term = Constr.mkConst f_kn in - (* In the type and body of the proof of [suchthat] there can be - references to the variable [f]. It needs to be replaced by - references to the constant [f] declared above. This substitution - performs this precise action. *) - let substf c = Vars.replace_vars [f,f_kn_term] c in - (* Extracts the type of the proof of [suchthat]. *) - let lemma_pretype typ = - match typ with - | Some t -> Some (substf t) - | None -> assert false (* Declare always sets type here. *) - in - (* The references of [f] are subsituted appropriately. *) - let lemma_def = Declare.Internal.map_entry_type lemma_def ~f:lemma_pretype in - (* The same is done in the body of the proof. *) - let lemma_def = Declare.Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in - let lemma_def = Declare.DefinitionEntry lemma_def in - let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in - () - -let finish_proved_equations ~kind ~hook i proof_obj types sigma0 = - - let obls = ref 1 in - let sigma, recobls = - CList.fold_left2_map (fun sigma (_evar_env, ev, _evi, local_context, _type) entry -> - let id = - match Evd.evar_ident ev sigma0 with - | Some id -> id - | None -> let n = !obls in incr obls; Nameops.add_suffix i ("_obligation_" ^ string_of_int n) - in - let entry, args = Declare.Internal.shrink_entry local_context entry in - let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in - let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in - let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in - sigma, cst) sigma0 - types proof_obj.Declare.entries - in - hook recobls sigma - -let finalize_proof proof_obj proof_info = - let open Declare in - let open Proof_ending in - match CEphemeron.default proof_info.Info.proof_ending Regular with - | Regular -> - finish_proved proof_obj proof_info - | End_obligation oinfo -> - DeclareObl.obligation_terminator proof_obj.entries proof_obj.uctx oinfo - | End_derive { f ; name } -> - finish_derived ~f ~name ~entries:proof_obj.entries - | End_equations { hook; i; types; sigma } -> - finish_proved_equations ~kind:proof_info.Info.kind ~hook i proof_obj types sigma - -let err_save_forbidden_in_place_of_qed () = - CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode") - -let process_idopt_for_save ~idopt info = - match idopt with - | None -> info - | Some { CAst.v = save_name } -> - (* Save foo was used; we override the info in the first theorem *) - let thms = - match info.Info.thms, CEphemeron.default info.Info.proof_ending Proof_ending.Regular with - | [ { Declare.Recthm.name; _} as decl ], Proof_ending.Regular -> - [ { decl with Declare.Recthm.name = save_name } ] - | _ -> - err_save_forbidden_in_place_of_qed () - in { info with Info.thms } +let save_lemma_admitted ~lemma = + Declare.save_lemma_admitted ~proof:lemma.proof ~info:lemma.info let save_lemma_proved ~lemma ~opaque ~idopt = - (* Env and sigma are just used for error printing in save_remaining_recthms *) - let proof_obj = Declare.close_proof ~opaque ~keep_body_ucst_separate:false lemma.proof in - let proof_info = process_idopt_for_save ~idopt lemma.info in - finalize_proof proof_obj proof_info - -(***********************************************************************) -(* Special case to close a lemma without forcing a proof *) -(***********************************************************************) -let save_lemma_admitted_delayed ~proof ~info = - let open Declare in - let { entries; uctx } = proof in - if List.length entries <> 1 then - CErrors.user_err Pp.(str "Admitted does not support multiple statements"); - let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in - let poly = match proof_entry_universes with - | Entries.Monomorphic_entry _ -> false - | Entries.Polymorphic_entry (_, _) -> true in - let typ = match proof_entry_type with - | None -> CErrors.user_err Pp.(str "Admitted requires an explicit statement"); - | Some typ -> typ in - let ctx = UState.univ_entry ~poly uctx in - let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in - finish_admitted ~uctx ~info (sec_vars, (typ, ctx), None) - -let save_lemma_proved_delayed ~proof ~info ~idopt = - (* vio2vo calls this but with invalid info, we have to workaround - that to add the name to the info structure *) - if CList.is_empty info.Info.thms then - let info = add_first_thm ~info ~name:proof.Declare.name ~typ:EConstr.mkSet ~impargs:[] in - finalize_proof proof info - else - let info = process_idopt_for_save ~idopt info in - finalize_proof proof info + Declare.save_lemma_proved ~proof:lemma.proof ~info:lemma.info ~opaque ~idopt diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index b1462f1ce5..4787a940da 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -28,39 +28,8 @@ val pf_fold : (Declare.Proof.t -> 'a) -> t -> 'a val by : unit Proofview.tactic -> t -> t * bool (** [by tac l] apply a tactic to [l] *) -(** Creating high-level proofs with an associated constant *) -module Proof_ending : sig - - type t = - | Regular - | End_obligation of DeclareObl.obligation_qed_info - | End_derive of { f : Id.t; name : Id.t } - | End_equations of - { hook : Constant.t list -> Evd.evar_map -> unit - ; i : Id.t - ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list - ; sigma : Evd.evar_map - } - -end - -module Info : sig - - type t - - val make - : ?hook: Declare.Hook.t - (** Callback to be executed at the end of the proof *) - -> ?proof_ending : Proof_ending.t - (** Info for special constants *) - -> ?scope : Declare.locality - (** locality *) - -> ?kind:Decls.logical_kind - (** Theorem, etc... *) - -> unit - -> t - -end +module Proof_ending = Declare.Proof_ending +module Info = Declare.Info (** Starts the proof of a constant *) val start_lemma @@ -99,6 +68,7 @@ val start_lemma_with_initialization (** {4 Saving proofs} *) val save_lemma_admitted : lemma:t -> unit + val save_lemma_proved : lemma:t -> opaque:Declare.opacity_flag @@ -110,12 +80,3 @@ module Internal : sig val get_info : t -> Info.t (** Only needed due to the Declare compatibility layer. *) end - -(** Special cases for delayed proofs, in this case we must provide the - proof information so the proof won't be forced. *) -val save_lemma_admitted_delayed : proof:Declare.proof_object -> info:Info.t -> unit -val save_lemma_proved_delayed - : proof:Declare.proof_object - -> info:Info.t - -> idopt:Names.lident option - -> unit diff --git a/vernac/locality.ml b/vernac/locality.ml index f62eed5e41..3953e54f52 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -10,9 +10,12 @@ (** * Managing locality *) +type import_status = ImportDefaultBehavior | ImportNeedQualified +type locality = Discharge | Global of import_status + let importability_of_bool = function - | true -> Declare.ImportNeedQualified - | false -> Declare.ImportDefaultBehavior + | true -> ImportNeedQualified + | false -> ImportDefaultBehavior (** Positioning locality for commands supporting discharging and export outside of modules *) @@ -34,15 +37,14 @@ let warn_local_declaration = strbrk "available without qualification when imported.") let enforce_locality_exp locality_flag discharge = - let open Declare in let open Vernacexpr in match locality_flag, discharge with | Some b, NoDischarge -> Global (importability_of_bool b) - | None, NoDischarge -> Global Declare.ImportDefaultBehavior + | None, NoDischarge -> Global ImportDefaultBehavior | None, DoDischarge when not (Global.sections_are_opened ()) -> (* If a Let/Variable is defined outside a section, then we consider it as a local definition *) warn_local_declaration (); - Global Declare.ImportNeedQualified + Global ImportNeedQualified | None, DoDischarge -> Discharge | Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case") | Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case") diff --git a/vernac/locality.mli b/vernac/locality.mli index bf65579efd..81da895568 100644 --- a/vernac/locality.mli +++ b/vernac/locality.mli @@ -10,6 +10,9 @@ (** * Managing locality *) +type import_status = ImportDefaultBehavior | ImportNeedQualified +type locality = Discharge | Global of import_status + (** * Positioning locality for commands supporting discharging and export outside of modules *) @@ -20,7 +23,7 @@ val make_locality : bool option -> bool val make_non_locality : bool option -> bool -val enforce_locality_exp : bool option -> Vernacexpr.discharge -> Declare.locality +val enforce_locality_exp : bool option -> Vernacexpr.discharge -> locality val enforce_locality : bool option -> bool (** For commands whose default is to not discharge but to export: diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 5e746afc74..a8eac8fd2d 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -9,39 +9,56 @@ (************************************************************************) open Printf - open Names open Pp -open CErrors open Util (* For the records fields, opens should go away one these types are private *) -open DeclareObl -open DeclareObl.Obligation -open DeclareObl.ProgramDecl - -let pperror cmd = CErrors.user_err ~hdr:"Program" cmd -let error s = pperror (str s) +open Declare.Obls +open Declare.Obls.Obligation +open Declare.Obls.ProgramDecl let reduce c = let env = Global.env () in let sigma = Evd.from_env env in EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota env sigma (EConstr.of_constr c)) -exception NoObligations of Id.t option - let explain_no_obligations = function Some ident -> str "No obligations for program " ++ Id.print ident | None -> str "No obligations remaining" -let assumption_message = Declare.assumption_message +module Error = struct + + let no_obligations n = + CErrors.user_err (explain_no_obligations n) + + let ambiguous_program id ids = + CErrors.user_err + Pp.(str "More than one program with unsolved obligations: " ++ prlist Id.print ids + ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print id ++ str "\"") + + let unknown_obligation num = + CErrors.user_err (Pp.str (sprintf "Unknown obligation number %i" (succ num))) + + let already_solved num = + CErrors.user_err + ( str "Obligation" ++ spc () ++ int num ++ str "already" ++ spc () + ++ str "solved." ) + + let depends num rem = + CErrors.user_err + ( str "Obligation " ++ int num + ++ str " depends on obligation(s) " + ++ pr_sequence (fun x -> int (succ x)) rem) + +end let default_tactic = ref (Proofview.tclUNIT ()) let evar_of_obligation o = Evd.make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) let subst_deps expand obls deps t = - let osubst = DeclareObl.obl_substitution expand obls deps in + let osubst = Declare.Obls.obl_substitution expand obls deps in (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) let subst_deps_obl obls obl = @@ -50,56 +67,6 @@ let subst_deps_obl obls obl = open Evd -let map_cardinal m = - let i = ref 0 in - ProgMap.iter (fun _ v -> - if (CEphemeron.get v).prg_obligations.remaining > 0 then incr i) m; - !i - -exception Found of ProgramDecl.t CEphemeron.key - -let map_first m = - try - ProgMap.iter (fun _ v -> - if (CEphemeron.get v).prg_obligations.remaining > 0 then - raise (Found v)) m; - assert(false) - with Found x -> x - -let get_prog name = - let prg_infos = get_prg_info_map () in - match name with - Some n -> - (try CEphemeron.get (ProgMap.find n prg_infos) - with Not_found -> raise (NoObligations (Some n))) - | None -> - (let n = map_cardinal prg_infos in - match n with - 0 -> raise (NoObligations None) - | 1 -> CEphemeron.get (map_first prg_infos) - | _ -> - let progs = Id.Set.elements (ProgMap.domain prg_infos) in - let prog = List.hd progs in - let progs = prlist_with_sep pr_comma Id.print progs in - user_err - (str "More than one program with unsolved obligations: " ++ progs - ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print prog ++ str "\"")) - -let get_any_prog () = - let prg_infos = get_prg_info_map () in - let n = map_cardinal prg_infos in - if n > 0 then CEphemeron.get (map_first prg_infos) - else raise (NoObligations None) - -let get_prog_err n = - try get_prog n with NoObligations id -> pperror (explain_no_obligations id) - -let get_any_prog_err () = - try get_any_prog () with NoObligations id -> pperror (explain_no_obligations id) - -let all_programs () = - ProgMap.fold (fun k p l -> p :: l) (get_prg_info_map ()) [] - let is_defined obls x = not (Option.is_empty obls.(x).obl_body) let deps_remaining obls deps = @@ -109,7 +76,6 @@ let deps_remaining obls deps = else x :: acc) deps [] - let goal_kind = Decls.(IsDefinition Definition) let goal_proof_kind = Decls.(IsProof Lemma) @@ -119,19 +85,19 @@ let kind_of_obligation o = | Evar_kinds.Expand -> goal_kind | _ -> goal_proof_kind -let rec string_of_list sep f = function - [] -> "" - | x :: [] -> f x - | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl - (* Solve an obligation using tactics, return the corresponding proof term *) -let warn_solve_errored = CWarnings.create ~name:"solve_obligation_error" ~category:"tactics" (fun err -> - Pp.seq [str "Solve Obligations tactic returned error: "; err; fnl (); - str "This will become an error in the future"]) +let warn_solve_errored = + CWarnings.create ~name:"solve_obligation_error" ~category:"tactics" + (fun err -> + Pp.seq + [ str "Solve Obligations tactic returned error: " + ; err + ; fnl () + ; str "This will become an error in the future" ]) let solve_by_tac ?loc name evi t poly uctx = + (* the status is dropped. *) try - (* the status is dropped. *) let env = Global.env () in let body, types, _univs, _, uctx = Declare.build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in @@ -140,7 +106,7 @@ let solve_by_tac ?loc name evi t poly uctx = with | Refiner.FailError (_, s) as exn -> let _ = Exninfo.capture exn in - user_err ?loc ~hdr:"solve_obligation" (Lazy.force s) + CErrors.user_err ?loc ~hdr:"solve_obligation" (Lazy.force s) (* If the proof is open we absorb the error and leave the obligation open *) | Proof.OpenProof _ -> None @@ -149,17 +115,24 @@ let solve_by_tac ?loc name evi t poly uctx = warn_solve_errored ?loc err; None +let get_unique_prog prg = + match State.get_unique_open_prog prg with + | Ok prg -> prg + | Error [] -> + Error.no_obligations None + | Error ((id :: _) as ids) -> + Error.ambiguous_program id ids + let rec solve_obligation prg num tac = let user_num = succ num in let { obls; remaining=rem } = prg.prg_obligations in let obl = obls.(num) in let remaining = deps_remaining obls obl.obl_deps in let () = - if not (Option.is_empty obl.obl_body) then - pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved."); - if not (List.is_empty remaining) then - pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " - ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining)); + if not (Option.is_empty obl.obl_body) + then Error.already_solved user_num; + if not (List.is_empty remaining) + then Error.depends user_num remaining in let obl = subst_deps_obl obls obl in let scope = Declare.(Global Declare.ImportNeedQualified) in @@ -167,9 +140,11 @@ let rec solve_obligation prg num tac = let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n oblset tac = auto_solve_obligations n ~oblset tac in - let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in - let hook = Declare.Hook.make (DeclareObl.obligation_hook prg obl num auto) in - let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in + let proof_ending = + Declare.Proof_ending.End_obligation + {Declare.Obls.name = prg.prg_name; num; auto} + in + let info = Lemmas.Info.make ~proof_ending ~scope ~kind () in let poly = prg.prg_poly in let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in let lemma = fst @@ Lemmas.by !default_tactic lemma in @@ -178,15 +153,14 @@ let rec solve_obligation prg num tac = and obligation (user_num, name, typ) tac = let num = pred user_num in - let prg = get_prog_err name in + let prg = get_unique_prog name in let { obls; remaining } = prg.prg_obligations in - if num >= 0 && num < Array.length obls then - let obl = obls.(num) in - match obl.obl_body with - | None -> solve_obligation prg num tac - | Some r -> error "Obligation already solved" - else error (sprintf "Unknown obligation number %i" (succ num)) - + if num >= 0 && num < Array.length obls then + let obl = obls.(num) in + match obl.obl_body with + | None -> solve_obligation prg num tac + | Some r -> Error.already_solved num + else Error.unknown_obligation num and solve_obligation_by_tac prg obls i tac = let obl = obls.(i) in @@ -208,18 +182,16 @@ and solve_obligation_by_tac prg obls i tac = match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac prg.prg_poly (Evd.evar_universe_context evd) with | None -> None - | Some (t, ty, ctx) -> - let prg = ProgramDecl.set_uctx ~uctx:ctx prg in + | Some (t, ty, uctx) -> + let prg = ProgramDecl.set_uctx ~uctx prg in (* Why is uctx not used above? *) - let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in - let def, obl' = declare_obligation prg obl t ty uctx in + let def, obl' = declare_obligation prg obl ~body:t ~types:ty ~uctx in obls.(i) <- obl'; if def && not prg.prg_poly then ( (* Declare the term constraints with the first obligation only *) - let evd = Evd.from_env (Global.env ()) in - let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in - let ctx' = Evd.evar_universe_context evd in - Some (ProgramDecl.set_uctx ~uctx:ctx' prg)) + let uctx_global = UState.from_env (Global.env ()) in + let uctx = UState.merge_subst uctx_global (UState.subst uctx) in + Some (ProgramDecl.set_uctx ~uctx prg)) else Some prg else None @@ -233,121 +205,163 @@ and solve_prg_obligations prg ?oblset tac = | Some s -> set := s; (fun i -> Int.Set.mem i !set) in - let prg = - Array.fold_left_i (fun i prg x -> - if p i then - match solve_obligation_by_tac prg obls' i tac with - | None -> prg - | Some prg -> - let deps = dependencies obls i in - set := Int.Set.union !set deps; - decr rem; - prg - else prg) - prg obls' + let (), prg = + Array.fold_left_i + (fun i ((), prg) x -> + if p i then ( + match solve_obligation_by_tac prg obls' i tac with + | None -> (), prg + | Some prg -> + let deps = dependencies obls i in + set := Int.Set.union !set deps; + decr rem; + (), prg) + else (), prg) + ((), prg) obls' in update_obls prg obls' !rem and solve_obligations n tac = - let prg = get_prog_err n in + let prg = get_unique_prog n in solve_prg_obligations prg tac and solve_all_obligations tac = - ProgMap.iter (fun k v -> ignore(solve_prg_obligations (CEphemeron.get v) tac)) (get_prg_info_map ()) + State.fold ~init:() ~f:(fun k v () -> + let _ = solve_prg_obligations v tac in ()) and try_solve_obligation n prg tac = - let prg = get_prog prg in + let prg = get_unique_prog prg in let {obls; remaining } = prg.prg_obligations in let obls' = Array.copy obls in - match solve_obligation_by_tac prg obls' n tac with - | Some prg' -> ignore(update_obls prg' obls' (pred remaining)) - | None -> () + match solve_obligation_by_tac prg obls' n tac with + | Some prg' -> + let _r = update_obls prg' obls' (pred remaining) in + () + | None -> () and try_solve_obligations n tac = - try ignore (solve_obligations n tac) with NoObligations _ -> () + let _ = solve_obligations n tac in + () and auto_solve_obligations n ?oblset tac : progress = - Flags.if_verbose Feedback.msg_info (str "Solving obligations automatically..."); - try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent + Flags.if_verbose Feedback.msg_info + (str "Solving obligations automatically..."); + let prg = get_unique_prog n in + solve_prg_obligations prg ?oblset tac open Pp -let show_obligations_of_prg ?(msg=true) prg = + +let show_single_obligation i n obls x = + let x = subst_deps_obl obls x in + let env = Global.env () in + let sigma = Evd.from_env env in + let msg = + str "Obligation" ++ spc () + ++ int (succ i) + ++ spc () ++ str "of" ++ spc () ++ Id.print n ++ str ":" ++ spc () + ++ hov 1 (Printer.pr_constr_env env sigma x.obl_type + ++ str "." ++ fnl ()) in + Feedback.msg_info msg + +let show_obligations_of_prg ?(msg = true) prg = let n = prg.prg_name in let {obls; remaining} = prg.prg_obligations in let showed = ref 5 in if msg then Feedback.msg_info (int remaining ++ str " obligation(s) remaining: "); - Array.iteri (fun i x -> - match x.obl_body with - | None -> - if !showed > 0 then ( - decr showed; - let x = subst_deps_obl obls x in - let env = Global.env () in - let sigma = Evd.from_env env in - Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ - str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++ - hov 1 (Printer.pr_constr_env env sigma x.obl_type ++ - str "." ++ fnl ()))) - | Some _ -> ()) + Array.iteri + (fun i x -> + match x.obl_body with + | None -> + if !showed > 0 then begin + decr showed; + show_single_obligation i n obls x + end + | Some _ -> ()) obls -let show_obligations ?(msg=true) n = - let progs = match n with - | None -> all_programs () +let show_obligations ?(msg = true) n = + let progs = + match n with + | None -> + State.all () | Some n -> - try [ProgMap.find n (get_prg_info_map ())] - with Not_found -> raise (NoObligations (Some n)) - in List.iter (fun x -> show_obligations_of_prg ~msg (CEphemeron.get x)) progs + (match State.find n with + | Some prg -> [prg] + | None -> Error.no_obligations (Some n)) + in + List.iter (fun x -> show_obligations_of_prg ~msg x) progs let show_term n = - let prg = get_prog_err n in + let prg = get_unique_prog n in let n = prg.prg_name in let env = Global.env () in let sigma = Evd.from_env env in - (Id.print n ++ spc () ++ str":" ++ spc () ++ - Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl () - ++ Printer.pr_constr_env env sigma prg.prg_body) + Id.print n ++ spc () ++ str ":" ++ spc () + ++ Printer.pr_constr_env env sigma prg.prg_type + ++ spc () ++ str ":=" ++ fnl () + ++ Printer.pr_constr_env env sigma prg.prg_body -let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl) - ?(impargs=[]) ~poly ?(scope=Declare.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic - ?(reduce=reduce) ?hook ?(opaque = false) obls = +let msg_generating_obl name obls = + let len = Array.length obls in let info = Id.print name ++ str " has type-checked" in + Feedback.msg_info + (if len = 0 then info ++ str "." + else + info ++ str ", generating " ++ int len ++ + str (String.plural len " obligation")) + +let add_definition ~name ?term t ~uctx ?(udecl = UState.default_univ_decl) + ?(impargs = []) ~poly + ?(scope = Declare.Global Declare.ImportDefaultBehavior) + ?(kind = Decls.Definition) ?tactic ?(reduce = reduce) ?hook + ?(opaque = false) obls = let prg = ProgramDecl.make ~opaque name ~udecl term t ~uctx [] None [] obls ~impargs ~poly ~scope ~kind reduce ?hook in let {obls;_} = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( - Flags.if_verbose Feedback.msg_info (info ++ str "."); - let cst = DeclareObl.declare_definition prg in + Flags.if_verbose (msg_generating_obl name) obls; + let cst = Declare.Obls.declare_definition prg in Defined cst) - else ( - let len = Array.length obls in - let () = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in - progmap_add name (CEphemeron.create prg); - let res = auto_solve_obligations (Some name) tactic in - match res with - | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some name)) (); res - | _ -> res) - -let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic - ~poly ?(scope=Declare.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce) - ?hook ?(opaque = false) notations fixkind = - let deps = List.map (fun ({ Declare.Recthm.name; _ }, _, _) -> name) l in - List.iter - (fun ({ Declare.Recthm.name; typ; impargs; _ }, b, obls) -> - let prg = ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps (Some fixkind) - notations obls ~impargs ~poly ~scope ~kind reduce ?hook - in progmap_add name (CEphemeron.create prg)) l; - let _defined = - List.fold_left (fun finished x -> - if finished then finished + else + let () = Flags.if_verbose (msg_generating_obl name) obls in + let () = State.add name prg in + let res = auto_solve_obligations (Some name) tactic in + match res with + | Remain rem -> + Flags.if_verbose (show_obligations ~msg:false) (Some name); + res + | _ -> res + +let add_mutual_definitions l ~uctx ?(udecl = UState.default_univ_decl) + ?tactic ~poly ?(scope = Declare.Global Declare.ImportDefaultBehavior) + ?(kind = Decls.Definition) ?(reduce = reduce) ?hook ?(opaque = false) + notations fixkind = + let deps = List.map (fun ({Declare.Recthm.name; _}, _, _) -> name) l in + let pm = + List.fold_left + (fun () ({Declare.Recthm.name; typ; impargs; _}, b, obls) -> + let prg = + ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps + (Some fixkind) notations obls ~impargs ~poly ~scope ~kind reduce + ?hook + in + State.add name prg) + () l + in + let pm, _defined = + List.fold_left + (fun (pm, finished) x -> + if finished then (pm, finished) else let res = auto_solve_obligations (Some x) tactic in - match res with - | Defined _ -> - (* If one definition is turned into a constant, - the whole block is defined. *) true - | _ -> false) - false deps - in () + match res with + | Defined _ -> + (* If one definition is turned into a constant, + the whole block is defined. *) + (pm, true) + | _ -> (pm, false)) + (pm, false) deps + in + pm let admit_prog prg = let {obls; remaining} = prg.prg_obligations in @@ -359,39 +373,41 @@ let admit_prog prg = let x = subst_deps_obl obls x in let ctx = UState.univ_entry ~poly:false prg.prg_ctx in let kn = Declare.declare_constant ~name:x.obl_name ~local:Declare.ImportNeedQualified - (Declare.ParameterEntry (None,(x.obl_type,ctx),None)) ~kind:Decls.(IsAssumption Conjectural) + (Declare.ParameterEntry (None, (x.obl_type, ctx), None)) ~kind:Decls.(IsAssumption Conjectural) in - assumption_message x.obl_name; + Declare.assumption_message x.obl_name; obls.(i) <- Obligation.set_body ~body:(DefinedObl (kn, Univ.Instance.empty)) x | Some _ -> ()) obls; - ignore(DeclareObl.update_obls prg obls 0) + Declare.Obls.update_obls prg obls 0 +(* get_any_prog *) let rec admit_all_obligations () = - let prg = try Some (get_any_prog ()) with NoObligations _ -> None in + let prg = State.first_pending () in match prg with | None -> () | Some prg -> - admit_prog prg; + let _prog = admit_prog prg in admit_all_obligations () let admit_obligations n = match n with | None -> admit_all_obligations () | Some _ -> - let prg = get_prog_err n in - admit_prog prg + let prg = get_unique_prog n in + let _ = admit_prog prg in + () let next_obligation n tac = let prg = match n with - | None -> get_any_prog_err () - | Some _ -> get_prog_err n + | None -> State.first_pending () |> Option.get + | Some _ -> get_unique_prog n in let {obls; remaining} = prg.prg_obligations in let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in let i = match Array.findi is_open obls with - | Some i -> i - | None -> anomaly (Pp.str "Could not find a solvable obligation.") + | Some i -> i + | None -> CErrors.anomaly (Pp.str "Could not find a solvable obligation.") in solve_obligation prg i tac diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 89ed4c3498..102a17b216 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -84,7 +84,7 @@ val add_definition : -> ?hook:Declare.Hook.t -> ?opaque:bool -> RetrieveObl.obligation_info - -> DeclareObl.progress + -> Declare.Obls.progress (* XXX: unify with MutualEntry *) @@ -102,7 +102,7 @@ val add_mutual_definitions : -> ?hook:Declare.Hook.t -> ?opaque:bool -> Vernacexpr.decl_notation list - -> DeclareObl.fixpoint_kind + -> Declare.Obls.fixpoint_kind -> unit (** Implementation of the [Obligation] command *) @@ -117,7 +117,7 @@ val next_obligation : (** Implementation of the [Solve Obligation] command *) val solve_obligations : - Names.Id.t option -> unit Proofview.tactic option -> DeclareObl.progress + Names.Id.t option -> unit Proofview.tactic option -> Declare.Obls.progress val solve_all_obligations : unit Proofview.tactic option -> unit @@ -132,7 +132,5 @@ val show_obligations : ?msg:bool -> Names.Id.t option -> unit val show_term : Names.Id.t option -> Pp.t val admit_obligations : Names.Id.t option -> unit -exception NoObligations of Names.Id.t option - val explain_no_obligations : Names.Id.t option -> Pp.t val check_program_libraries : unit -> unit diff --git a/vernac/pfedit.ml b/vernac/pfedit.ml index e6c66ee503..150311ffaa 100644 --- a/vernac/pfedit.ml +++ b/vernac/pfedit.ml @@ -15,5 +15,5 @@ let build_by_tactic ?side_eff env ~uctx ~poly ~typ tac = b, t, safe, uctx [@@ocaml.deprecated "Use [Proof.build_by_tactic]"] -let build_constant_by_tactic = Declare.build_constant_by_tactic +let build_constant_by_tactic = Declare.build_constant_by_tactic [@ocaml.warning "-3"] [@@ocaml.deprecated "Use [Proof.build_constant_by_tactic]"] diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index b97cdfa51c..2c52c605b5 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -108,6 +108,38 @@ open Pputils let sep = fun _ -> spc() let sep_v2 = fun _ -> str"," ++ spc() + let string_of_theorem_kind = let open Decls in function + | Theorem -> "Theorem" + | Lemma -> "Lemma" + | Fact -> "Fact" + | Remark -> "Remark" + | Property -> "Property" + | Proposition -> "Proposition" + | Corollary -> "Corollary" + + let string_of_definition_object_kind = let open Decls in function + | Definition -> "Definition" + | Example -> "Example" + | Coercion -> "Coercion" + | SubClass -> "SubClass" + | CanonicalStructure -> "Canonical Structure" + | Instance -> "Instance" + | Let -> "Let" + | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> + CErrors.anomaly (Pp.str "Internal definition kind.") + + let string_of_assumption_kind = let open Decls in function + | Definitional -> "Parameter" + | Logical -> "Axiom" + | Conjectural -> "Conjecture" + | Context -> "Context" + + let string_of_logical_kind = let open Decls in function + | IsAssumption k -> string_of_assumption_kind k + | IsDefinition k -> string_of_definition_object_kind k + | IsProof k -> string_of_theorem_kind k + | IsPrimitive -> "Primitive" + let pr_notation_entry = function | InConstrEntry -> keyword "constr" | InCustomEntry s -> keyword "custom" ++ spc () ++ str s @@ -148,14 +180,28 @@ open Pputils | SearchOutside [] -> mt() | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l - let pr_search (b,c) = - (if b then str "-" else mt()) ++ - match c with - | SearchSubPattern p -> + let pr_search_where = function + | Anywhere, false -> mt () + | Anywhere, true -> str "head:" + | InHyp, true -> str "headhyp:" + | InHyp, false -> str "hyp:" + | InConcl, true -> str "headconcl:" + | InConcl, false -> str "concl:" + + let pr_search_item = function + | SearchSubPattern (where,p) -> let env = Global.env () in let sigma = Evd.from_env env in - pr_constr_pattern_expr env sigma p - | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc + pr_search_where where ++ pr_constr_pattern_expr env sigma p + | SearchString (where,s,sc) -> pr_search_where where ++ qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc + | SearchKind kind -> str "is:" ++ str (string_of_logical_kind kind) + + let rec pr_search_request = function + | SearchLiteral a -> pr_search_item a + | SearchDisjConj l -> str "[" ++ prlist_with_sep spc (prlist_with_sep pr_bar pr_search_default) l ++ str "]" + + and pr_search_default (b, s) = + (if b then mt() else str "-") ++ pr_search_request s let pr_search a gopt b pr_p = pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt @@ -165,7 +211,7 @@ open Pputils | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b | Search sl -> - keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search sl ++ pr_in_out_modules b + keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_default sl ++ pr_in_out_modules b let pr_option_ref_value = function | Goptions.QualidRefValue id -> pr_qualid id @@ -386,15 +432,6 @@ open Pputils prlist_with_sep pr_semicolon (pr_params pr_c) *) -let string_of_theorem_kind = let open Decls in function - | Theorem -> "Theorem" - | Lemma -> "Lemma" - | Fact -> "Fact" - | Remark -> "Remark" - | Property -> "Property" - | Proposition -> "Proposition" - | Corollary -> "Corollary" - let pr_thm_token k = keyword (string_of_theorem_kind k) let pr_syntax_modifier = let open Gramlib.Gramext in function @@ -611,18 +648,6 @@ let string_of_theorem_kind = let open Decls in function with Not_found -> hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") - -let string_of_definition_object_kind = let open Decls in function - | Definition -> "Definition" - | Example -> "Example" - | Coercion -> "Coercion" - | SubClass -> "SubClass" - | CanonicalStructure -> "Canonical Structure" - | Instance -> "Instance" - | Let -> "Let" - | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> - CErrors.anomaly (Pp.str "Internal definition kind.") - let pr_vernac_expr v = let return = tag_vernac v in let env = Global.env () in diff --git a/vernac/proof_global.ml b/vernac/proof_global.ml index 54d1db44a4..0c5bc39020 100644 --- a/vernac/proof_global.ml +++ b/vernac/proof_global.ml @@ -10,3 +10,4 @@ let get_proof = Declare.Proof.get_proof type opacity_flag = Declare.opacity_flag = | Opaque [@ocaml.deprecated "Use [Declare.Opaque]"] | Transparent [@ocaml.deprecated "Use [Declare.Transparent]"] +[@@ocaml.deprecated "Use [Declare.opacity_flag]"] diff --git a/vernac/record.ml b/vernac/record.ml index 36254780cd..9d99036273 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -223,7 +223,7 @@ let warn_cannot_define_projection = (* If a projection is not definable, we throw an error if the user asked it to be a coercion. Otherwise, we just print an info message. The user might still want to name the field of the record. *) -let warning_or_error coe indsp err = +let warning_or_error ~info coe indsp err = let st = match err with | MissingProj (fi,projs) -> let s,have = if List.length projs > 1 then "s","were" else "","was" in @@ -246,7 +246,7 @@ let warning_or_error coe indsp err = | _ -> (Id.print fi ++ strbrk " cannot be defined because it is not typable.") in - if coe then user_err ~hdr:"structure" st; + if coe then user_err ~hdr:"structure" ~info st; warn_cannot_define_projection (hov 0 st) type field_status = @@ -352,8 +352,9 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f let kind = Decls.IsDefinition kind in let kn = try declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) - with Type_errors.TypeError (ctx,te) when not primitive -> - raise (NotDefinable (BadTypedProj (fid,ctx,te))) + with Type_errors.TypeError (ctx,te) as exn when not primitive -> + let _, info = Exninfo.capture exn in + Exninfo.iraise (NotDefinable (BadTypedProj (fid,ctx,te)),info) in Declare.definition_message fid; let term = match p_opt with @@ -374,8 +375,9 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f end; let i = if is_local_assum decl then i+1 else i in (Some kn::sp_projs, i, Projection term::subst) - with NotDefinable why -> - warning_or_error flags.pf_subclass indsp why; + with NotDefinable why as exn -> + let _, info = Exninfo.capture exn in + warning_or_error ~info flags.pf_subclass indsp why; (None::sp_projs,i,NoProjection fi::subst) in (nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst)) diff --git a/vernac/search.ml b/vernac/search.ml index 8b54b696f2..2a21184c1e 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -17,11 +17,14 @@ open Libobject open Environ open Pattern open Libnames +open Vernacexpr module NamedDecl = Context.Named.Declaration -type filter_function = GlobRef.t -> env -> constr -> bool -type display_function = GlobRef.t -> env -> constr -> unit +type filter_function = + GlobRef.t -> Decls.logical_kind option -> env -> Evd.evar_map -> constr -> bool +type display_function = + GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit (* This option restricts the output of [SearchPattern ...], etc. to the names of the symbols matching the @@ -29,9 +32,15 @@ query, separated by a newline. This type of output is useful for editors (like emacs), to generate a list of completion candidates without having to parse through the types of all symbols. *) -type glob_search_about_item = - | GlobSearchSubPattern of constr_pattern +type glob_search_item = + | GlobSearchSubPattern of glob_search_where * bool * constr_pattern | GlobSearchString of string + | GlobSearchKind of Decls.logical_kind + | GlobSearchFilter of (GlobRef.t -> bool) + +type glob_search_request = + | GlobSearchLiteral of glob_search_item + | GlobSearchDisjConj of (bool * glob_search_request) list list module SearchBlacklist = Goptions.MakeStringTable @@ -52,25 +61,9 @@ module SearchBlacklist = let iter_constructors indsp u fn env nconstr = for i = 1 to nconstr do let typ = Inductiveops.type_of_constructor env ((indsp, i), u) in - fn (GlobRef.ConstructRef (indsp, i)) env typ + fn (GlobRef.ConstructRef (indsp, i)) None env typ done -let iter_named_context_name_type f = - List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl)) - -let get_current_or_goal_context ?pstate glnum = - match pstate with - | None -> let env = Global.env () in Evd.(from_env env, env) - | Some p -> Declare.get_goal_context p glnum - -(* General search over hypothesis of a goal *) -let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) = - let env = Global.env () in - let iter_hyp idh typ = fn (GlobRef.VarRef idh) env typ in - let evmap,e = get_current_or_goal_context ?pstate glnum in - let pfctxt = named_context e in - iter_named_context_name_type iter_hyp pfctxt - (* FIXME: this is a Libobject hack that should be replaced with a proper registration mechanism. *) module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> unit end) @@ -80,9 +73,8 @@ let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with | exception Not_found -> () (* General search over declarations *) -let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = - let env = Global.env () in - List.iter (fun d -> fn (GlobRef.VarRef (NamedDecl.get_id d)) env (NamedDecl.get_type d)) +let generic_search env (fn : GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit) = + List.iter (fun d -> fn (GlobRef.VarRef (NamedDecl.get_id d)) None env (NamedDecl.get_type d)) (Environ.named_context env); let iter_obj (sp, kn) lobj = match lobj with | AtomicObject o -> @@ -91,7 +83,8 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = let cst = Global.constant_of_delta_kn kn in let gr = GlobRef.ConstRef cst in let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in - fn gr env typ + let kind = Dumpglob.constant_kind cst in + fn gr (Some kind) env typ end @@ DynHandle.add DeclareInd.Internal.objInductive begin fun _ -> let mind = Global.mind_of_delta_kn kn in @@ -101,7 +94,7 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let i = (ind, u) in let typ = Inductiveops.type_of_inductive env i in - let () = fn (GlobRef.IndRef ind) env typ in + let () = fn (GlobRef.IndRef ind) None env typ in let len = Array.length mip.mind_user_lc in iter_constructors ind u fn env len in @@ -115,12 +108,6 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = try Declaremods.iter_all_segments iter_obj with Not_found -> () -let generic_search ?pstate glnumopt fn = - (match glnumopt with - | None -> () - | Some glnum -> iter_hypothesis ?pstate glnum fn); - iter_declarations fn - (** This module defines a preference on constrs in the form of a [compare] function (preferred constr must be big for this functions, so preferences such as small constr must use a reversed @@ -132,7 +119,7 @@ module ConstrPriority = struct (* The priority is memoised here. Because of the very localised use of this module, it is not worth it making a convenient interface. *) - type t = GlobRef.t * Environ.env * Constr.t * priority + type t = GlobRef.t * Decls.logical_kind option * Environ.env * Constr.t * priority and priority = int module ConstrSet = CSet.Make(Constr) @@ -154,10 +141,10 @@ module ConstrPriority = struct let num_symbols t = ConstrSet.(cardinal (symbols empty t)) - let priority t : priority = + let priority gref t : priority = -(3*(num_symbols t) + size t) - let compare (_,_,_,p1) (_,_,_,p2) = + let compare (_,_,_,_,p1) (_,_,_,_,p2) = pervasives_compare p1 p2 end @@ -172,16 +159,16 @@ let rec iter_priority_queue q fn = with Heap.EmptyHeap -> None end in match next with - | Some (gref,env,t,_) -> - fn gref env t; + | Some (gref,kind,env,t,_) -> + fn gref kind env t; iter_priority_queue (PriorityQueue.remove q) fn | None -> () let prioritize_search seq fn = let acc = ref PriorityQueue.empty in - let iter gref env t = - let p = ConstrPriority.priority t in - acc := PriorityQueue.add (gref,env,t,p) !acc + let iter gref kind env t = + let p = ConstrPriority.priority gref t in + acc := PriorityQueue.add (gref,kind,env,t,p) !acc in let () = seq iter in iter_priority_queue !acc fn @@ -211,12 +198,12 @@ let full_name_of_reference ref = DirPath.to_string dir ^ "." ^ Id.to_string id (** Whether a reference is blacklisted *) -let blacklist_filter ref env typ = +let blacklist_filter ref kind env sigma typ = let name = full_name_of_reference ref in let is_not_bl str = not (String.string_contains ~where:name ~what:str) in CString.Set.for_all is_not_bl (SearchBlacklist.v ()) -let module_filter (mods, outside) ref env typ = +let module_filter (mods, outside) ref kind env sigma typ = let sp = Nametab.path_of_global ref in let sl = dirpath sp in let is_outside md = not (is_dirpath_prefix_of md sl) in @@ -226,25 +213,42 @@ let module_filter (mods, outside) ref env typ = let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref) -let search_filter query gr env typ = match query with -| GlobSearchSubPattern pat -> - Constr_matching.is_matching_appsubterm ~closed:false env (Evd.from_env env) pat (EConstr.of_constr typ) +let search_filter query gr kind env sigma typ = match query with +| GlobSearchSubPattern (where,head,pat) -> + let open Context.Rel.Declaration in + let collect_hyps ctx = + List.fold_left (fun acc d -> match get_value d with + | None -> get_type d :: acc + | Some b -> b :: get_type d :: acc) [] ctx in + let typl= match where with + | InHyp -> collect_hyps (fst (Term.decompose_prod_assum typ)) + | InConcl -> [snd (Term.decompose_prod_assum typ)] + | Anywhere -> + if head then + let ctx, ccl = Term.decompose_prod_assum typ in ccl :: collect_hyps ctx + else [typ] in + List.exists (fun typ -> + let f = + if head then Constr_matching.is_matching_head + else Constr_matching.is_matching_appsubterm ~closed:false in + f env sigma pat (EConstr.of_constr typ)) typl | GlobSearchString s -> String.string_contains ~where:(name_of_reference gr) ~what:s - +| GlobSearchKind k -> (match kind with None -> false | Some k' -> k = k') +| GlobSearchFilter f -> f gr (** SearchPattern *) -let search_pattern ?pstate gopt pat mods pr_search = - let filter ref env typ = - module_filter mods ref env typ && - pattern_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) && - blacklist_filter ref env typ +let search_pattern env sigma pat mods pr_search = + let filter ref kind env typ = + module_filter mods ref kind env sigma typ && + pattern_filter pat ref env sigma (EConstr.of_constr typ) && + blacklist_filter ref kind env sigma typ in - let iter ref env typ = - if filter ref env typ then pr_search ref env typ + let iter ref kind env typ = + if filter ref kind env typ then pr_search ref kind env typ in - generic_search ?pstate gopt iter + generic_search env iter (** SearchRewrite *) @@ -256,47 +260,49 @@ let rewrite_pat1 pat = let rewrite_pat2 pat = PApp (PRef (eq ()), [| PMeta None; PMeta None; pat |]) -let search_rewrite ?pstate gopt pat mods pr_search = +let search_rewrite env sigma pat mods pr_search = let pat1 = rewrite_pat1 pat in let pat2 = rewrite_pat2 pat in - let filter ref env typ = - module_filter mods ref env typ && - (pattern_filter pat1 ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) || - pattern_filter pat2 ref env (Evd.from_env env) (EConstr.of_constr typ)) && - blacklist_filter ref env typ + let filter ref kind env typ = + module_filter mods ref kind env sigma typ && + (pattern_filter pat1 ref env sigma (EConstr.of_constr typ) || + pattern_filter pat2 ref env sigma (EConstr.of_constr typ)) && + blacklist_filter ref kind env sigma typ in - let iter ref env typ = - if filter ref env typ then pr_search ref env typ + let iter ref kind env typ = + if filter ref kind env typ then pr_search ref kind env typ in - generic_search ?pstate gopt iter + generic_search env iter (** Search *) -let search_by_head ?pstate gopt pat mods pr_search = - let filter ref env typ = - module_filter mods ref env typ && - head_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) && - blacklist_filter ref env typ +let search_by_head env sigma pat mods pr_search = + let filter ref kind env typ = + module_filter mods ref kind env sigma typ && + head_filter pat ref env sigma (EConstr.of_constr typ) && + blacklist_filter ref kind env sigma typ in - let iter ref env typ = - if filter ref env typ then pr_search ref env typ + let iter ref kind env typ = + if filter ref kind env typ then pr_search ref kind env typ in - generic_search ?pstate gopt iter + generic_search env iter (** Search *) -let search ?pstate gopt items mods pr_search = - let filter ref env typ = +let search env sigma items mods pr_search = + let filter ref kind env typ = let eqb b1 b2 = if b1 then b2 else not b2 in - module_filter mods ref env typ && - List.for_all - (fun (b,i) -> eqb b (search_filter i ref env typ)) items && - blacklist_filter ref env typ + module_filter mods ref kind env sigma typ && + let rec aux = function + | GlobSearchLiteral i -> search_filter i ref kind env sigma typ + | GlobSearchDisjConj l -> List.exists (List.for_all aux') l + and aux' (b,s) = eqb b (aux s) in + List.for_all aux' items && blacklist_filter ref kind env sigma typ in - let iter ref env typ = - if filter ref env typ then pr_search ref env typ + let iter ref kind env typ = + if filter ref kind env typ then pr_search ref kind env typ in - generic_search ?pstate gopt iter + generic_search env iter type search_constraint = | Name_Pattern of Str.regexp @@ -311,7 +317,7 @@ type 'a coq_object = { coq_object_object : 'a; } -let interface_search ?pstate = +let interface_search env sigma = let rec extract_flags name tpe subtpe mods blacklist = function | [] -> (name, tpe, subtpe, mods, blacklist) | (Name_Pattern regexp, b) :: l -> @@ -325,7 +331,7 @@ let interface_search ?pstate = | (Include_Blacklist, b) :: l -> extract_flags name tpe subtpe mods b l in - fun ?glnum flags -> + fun flags -> let (name, tpe, subtpe, mods, blacklist) = extract_flags [] [] [] [] false flags in @@ -337,12 +343,12 @@ let interface_search ?pstate = toggle (Str.string_match regexp id 0) flag in let match_type (pat, flag) = - toggle (Constr_matching.is_matching env (Evd.from_env env) pat (EConstr.of_constr constr)) flag + toggle (Constr_matching.is_matching env sigma pat (EConstr.of_constr constr)) flag in let match_subtype (pat, flag) = toggle (Constr_matching.is_matching_appsubterm ~closed:false - env (Evd.from_env env) pat (EConstr.of_constr constr)) flag + env sigma pat (EConstr.of_constr constr)) flag in let match_module (mdl, flag) = toggle (Libnames.is_dirpath_prefix_of mdl path) flag @@ -351,7 +357,7 @@ let interface_search ?pstate = List.for_all match_type tpe && List.for_all match_subtype subtpe && List.for_all match_module mods && - (blacklist || blacklist_filter ref env constr) + (blacklist || blacklist_filter ref kind env sigma constr) in let ans = ref [] in let print_function ref env constr = @@ -377,8 +383,8 @@ let interface_search ?pstate = } in ans := answer :: !ans; in - let iter ref env typ = + let iter ref kind env typ = if filter_function ref env typ then print_function ref env typ in - let () = generic_search ?pstate glnum iter in + let () = generic_search env iter in !ans diff --git a/vernac/search.mli b/vernac/search.mli index d3b8444b5f..09847f4e03 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -12,15 +12,24 @@ open Names open Constr open Environ open Pattern +open Vernacexpr (** {6 Search facilities. } *) -type glob_search_about_item = - | GlobSearchSubPattern of constr_pattern +type glob_search_item = + | GlobSearchSubPattern of glob_search_where * bool * constr_pattern | GlobSearchString of string + | GlobSearchKind of Decls.logical_kind + | GlobSearchFilter of (GlobRef.t -> bool) -type filter_function = GlobRef.t -> env -> constr -> bool -type display_function = GlobRef.t -> env -> constr -> unit +type glob_search_request = + | GlobSearchLiteral of glob_search_item + | GlobSearchDisjConj of (bool * glob_search_request) list list + +type filter_function = + GlobRef.t -> Decls.logical_kind option -> env -> Evd.evar_map -> constr -> bool +type display_function = + GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit (** {6 Generic filter functions} *) @@ -30,7 +39,7 @@ val blacklist_filter : filter_function val module_filter : DirPath.t list * bool -> filter_function (** Check whether a reference pertains or not to a set of modules *) -val search_filter : glob_search_about_item -> filter_function +val search_filter : glob_search_item -> filter_function (** {6 Specialized search functions} @@ -38,13 +47,13 @@ val search_filter : glob_search_about_item -> filter_function goal and the global environment for things matching [pattern] and satisfying module exclude/include clauses of [modinout]. *) -val search_by_head : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool +val search_by_head : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search_rewrite : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool +val search_rewrite : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search_pattern : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool +val search_pattern : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search : ?pstate:Declare.Proof.t -> int option -> (bool * glob_search_about_item) list +val search : env -> Evd.evar_map -> (bool * glob_search_request) list -> DirPath.t list * bool -> display_function -> unit type search_constraint = @@ -65,12 +74,11 @@ type 'a coq_object = { coq_object_object : 'a; } -val interface_search : ?pstate:Declare.Proof.t -> ?glnum:int -> (search_constraint * bool) list -> - constr coq_object list +val interface_search : env -> Evd.evar_map -> (search_constraint * bool) list -> constr coq_object list (** {6 Generic search function} *) -val generic_search : ?pstate:Declare.Proof.t -> int option -> display_function -> unit +val generic_search : env -> display_function -> unit (** This function iterates over all hypothesis of the goal numbered [glnum] (if present) and all known declarations. *) diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 2d8734ff7f..a28d8f605b 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -404,6 +404,7 @@ let with_output_to_file fname func input = let channel = open_out (String.concat "." [fname; "out"]) in let old_fmt = !std_ft, !err_ft, !deep_ft in let new_ft = Format.formatter_of_out_channel channel in + set_gp new_ft (get_gp !std_ft); std_ft := new_ft; err_ft := new_ft; deep_ft := new_ft; @@ -412,6 +413,7 @@ let with_output_to_file fname func input = std_ft := Util.pi1 old_fmt; err_ft := Util.pi2 old_fmt; deep_ft := Util.pi3 old_fmt; + Format.pp_print_flush new_ft (); close_out channel; output with reraise -> @@ -419,6 +421,7 @@ let with_output_to_file fname func input = std_ft := Util.pi1 old_fmt; err_ft := Util.pi2 old_fmt; deep_ft := Util.pi3 old_fmt; + Format.pp_print_flush new_ft (); close_out channel; Exninfo.iraise reraise diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 618a61f487..1cad052bce 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -16,7 +16,6 @@ Metasyntax DeclareUniv RetrieveObl Declare -DeclareObl ComHints Canonical RecLemmas @@ -32,6 +31,7 @@ ComPrimitive ComAssumption DeclareInd Search +ComSearch Prettyp ComInductive ComFixpoint diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 09201d727d..106fed124e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -576,10 +576,14 @@ let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt let env = Global.env () in let sigma = Evd.from_env env in Some (snd (Hook.get f_interp_redexp env sigma r)) in - let do_definition = - ComDefinition.(if program_mode then do_definition_program else do_definition) in - do_definition ~name:name.v - ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook + if program_mode then + ComDefinition.do_definition_program ~name:name.v + ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook + else + let () = + ComDefinition.do_definition ~name:name.v + ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook in + () (* NB: pstate argument to use combinators easily *) let vernac_start_proof ~atts kind l = @@ -1054,10 +1058,21 @@ let vernac_end_section {CAst.loc; v} = let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set (* Dispatcher of the "End" command *) +let msg_of_subsection ss id = + let kind = + match ss with + | Lib.OpenedModule (false,_,_,_) -> "module" + | Lib.OpenedModule (true,_,_,_) -> "module type" + | Lib.OpenedSection _ -> "section" + | _ -> "unknown" + in + Pp.str kind ++ spc () ++ Id.print id let vernac_end_segment ({v=id} as lid) = - DeclareObl.check_can_close lid.v; - match Lib.find_opening_node id with + let ss = Lib.find_opening_node id in + let what_for = msg_of_subsection ss lid.v in + Declare.Obls.check_solved_obligations ~what_for; + match ss with | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid | Lib.OpenedSection _ -> vernac_end_section lid @@ -1762,91 +1777,17 @@ let vernac_print ~pstate ~atts = | PrintStrategy r -> print_strategy r | PrintRegistered -> print_registered () -let global_module qid = - try Nametab.full_name_module qid - with Not_found -> - user_err ?loc:qid.CAst.loc ~hdr:"global_module" - (str "Module/section " ++ pr_qualid qid ++ str " not found.") - -let interp_search_restriction = function - | SearchOutside l -> (List.map global_module l, true) - | SearchInside l -> (List.map global_module l, false) - -open Search - -let interp_search_about_item env sigma = - function - | SearchSubPattern pat -> - let _,pat = Constrintern.intern_constr_pattern env sigma pat in - GlobSearchSubPattern pat - | SearchString (s,None) when Id.is_valid s -> - GlobSearchString s - | SearchString (s,sc) -> - try - let ref = - Notation.interp_notation_as_global_reference - ~head:false (fun _ -> true) s sc in - GlobSearchSubPattern (Pattern.PRef ref) - with UserError _ -> - user_err ~hdr:"interp_search_about_item" - (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component") - -(* 05f22a5d6d5b8e3e80f1a37321708ce401834430 introduced the - `search_output_name_only` option to avoid excessive printing when - searching. - - The motivation was to make search usable for IDE completion, - however, it is still too slow due to the non-indexed nature of the - underlying search mechanism. - - In the future we should deprecate the option and provide a fast, - indexed name-searching interface. -*) -let search_output_name_only = ref false - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Search";"Output";"Name";"Only"]; - optread = (fun () -> !search_output_name_only); - optwrite = (:=) search_output_name_only } - let vernac_search ~pstate ~atts s gopt r = + let open ComSearch in let gopt = query_command_selector gopt in - let r = interp_search_restriction r in - let env,gopt = + let sigma, env = match gopt with | None -> (* 1st goal by default if it exists, otherwise no goal at all *) - (try snd (get_goal_or_global_context ~pstate 1) , Some 1 - with _ -> Global.env (),None) + (try get_goal_or_global_context ~pstate 1 + with _ -> let env = Global.env () in (Evd.from_env env, env)) (* if goal selector is given and wrong, then let exceptions be raised. *) - | Some g -> snd (get_goal_or_global_context ~pstate g) , Some g - in - let get_pattern c = snd (Constrintern.intern_constr_pattern env Evd.(from_env env) c) in - let pr_search ref env c = - let pr = pr_global ref in - let pp = if !search_output_name_only - then pr - else begin - let open Impargs in - let impargs = select_stronger_impargs (implicits_of_global ref) in - let impargs = List.map binding_kind_of_status impargs in - let pc = pr_ltype_env env Evd.(from_env env) ~impargs c in - hov 2 (pr ++ str":" ++ spc () ++ pc) - end - in Feedback.msg_notice pp - in - (match s with - | SearchPattern c -> - (Search.search_pattern ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search - | SearchRewrite c -> - (Search.search_rewrite ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search - | SearchHead c -> - (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search - | Search sl -> - (Search.search ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> - Search.prioritize_search) pr_search); - Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)") + | Some g -> get_goal_or_global_context ~pstate g in + interp_search env sigma s r let vernac_locate ~pstate = let open Constrexpr in function | LocateAny {v=AN qid} -> Prettyp.print_located_qualid qid diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index b622fd9801..0fdf9e2a7b 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -61,15 +61,22 @@ type printable = | PrintStrategy of qualid or_by_notation option | PrintRegistered -type search_about_item = - | SearchSubPattern of constr_pattern_expr - | SearchString of string * scope_name option +type glob_search_where = InHyp | InConcl | Anywhere + +type search_item = + | SearchSubPattern of (glob_search_where * bool) * constr_pattern_expr + | SearchString of (glob_search_where * bool) * string * scope_name option + | SearchKind of Decls.logical_kind + +type search_request = + | SearchLiteral of search_item + | SearchDisjConj of (bool * search_request) list list type searchable = | SearchPattern of constr_pattern_expr | SearchRewrite of constr_pattern_expr | SearchHead of constr_pattern_expr - | Search of (bool * search_about_item) list + | Search of (bool * search_request) list type locatable = | LocateAny of qualid or_by_notation diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 19d41c4770..7d25e6b852 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -225,9 +225,9 @@ let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option = let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in let () = match pe with | Admitted -> - Lemmas.save_lemma_admitted_delayed ~proof ~info + Declare.save_lemma_admitted_delayed ~proof ~info | Proved (_,idopt) -> - Lemmas.save_lemma_proved_delayed ~proof ~info ~idopt in + Declare.save_lemma_proved_delayed ~proof ~info ~idopt in stack let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } = |