diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/assumptions.ml | 3 | ||||
| -rw-r--r-- | vernac/assumptions.mli | 2 | ||||
| -rw-r--r-- | vernac/attributes.ml | 9 | ||||
| -rw-r--r-- | vernac/attributes.mli | 10 | ||||
| -rw-r--r-- | vernac/classes.ml | 3 | ||||
| -rw-r--r-- | vernac/dune | 1 | ||||
| -rw-r--r-- | vernac/egramml.mli | 4 | ||||
| -rw-r--r-- | vernac/explainErr.ml | 2 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 9 | ||||
| -rw-r--r-- | vernac/himsg.ml | 23 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 68 | ||||
| -rw-r--r-- | vernac/lemmas.mli | 4 | ||||
| -rw-r--r-- | vernac/obligations.ml | 103 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 6 | ||||
| -rw-r--r-- | vernac/pvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 86 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 79 | ||||
| -rw-r--r-- | vernac/vernacextend.ml | 67 | ||||
| -rw-r--r-- | vernac/vernacextend.mli | 72 |
19 files changed, 329 insertions, 224 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 6beac2032d..3ca2a4ad6b 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -294,7 +294,6 @@ let traverse current t = let type_of_constant cb = cb.Declarations.const_type let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = - let (idts, knst) = st in (** Only keep the transitive dependencies *) let (_, graph, ax2ty) = traverse (label_of gr) t in let fold obj _ accu = match obj with @@ -316,7 +315,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let t = type_of_constant cb in let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (Constant kn,l)) t accu - else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then + else if add_opaque && (Declareops.is_opaque cb || not (TransparentState.is_transparent_constant st kn)) then let t = type_of_constant cb in ContextObjectMap.add (Opaque kn) t accu else if add_transparent then diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index aead345d8c..536185f4aa 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -28,5 +28,5 @@ val traverse : on which a term relies (together with their type). The above warning of {!traverse} also applies. *) val assumptions : - ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> + ?add_opaque:bool -> ?add_transparent:bool -> TransparentState.t -> GlobRef.t -> constr -> types ContextObjectMap.t diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 88638b295b..bc0b0310b3 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -9,7 +9,14 @@ (************************************************************************) open CErrors -open Vernacexpr + +(** The type of parsing attribute data *) +type vernac_flags = vernac_flag list +and vernac_flag = string * vernac_flag_value +and vernac_flag_value = + | VernacFlagEmpty + | VernacFlagLeaf of string + | VernacFlagList of vernac_flags let unsupported_attributes = function | [] -> () diff --git a/vernac/attributes.mli b/vernac/attributes.mli index c81082d5ad..c2dde4cbcc 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -8,7 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Vernacexpr +(** The type of parsing attribute data *) +type vernac_flags = vernac_flag list +and vernac_flag = string * vernac_flag_value +and vernac_flag_value = + | VernacFlagEmpty + | VernacFlagLeaf of string + | VernacFlagList of vernac_flags type +'a attribute (** The type of attributes. When parsing attributes if an ['a @@ -80,7 +86,7 @@ val parse_with_extra : 'a attribute -> vernac_flags -> vernac_flags * 'a (** * Defining attributes. *) -type 'a key_parser = 'a option -> Vernacexpr.vernac_flag_value -> 'a +type 'a key_parser = 'a option -> vernac_flag_value -> 'a (** A parser for some key in an attribute. It is given a nonempty ['a option] when the attribute is multiply set for some command. diff --git a/vernac/classes.ml b/vernac/classes.ml index b0dba2485a..95e46b252b 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -188,8 +188,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id ] in ignore (Pfedit.by init_refine) - else if Flags.is_auto_intros () then - ignore (Pfedit.by (Tactics.auto_intros_tac ids)); + else ignore (Pfedit.by (Tactics.auto_intros_tac ids)); (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) () let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = diff --git a/vernac/dune b/vernac/dune index 4673251002..45b567d631 100644 --- a/vernac/dune +++ b/vernac/dune @@ -3,7 +3,6 @@ (synopsis "Coq's Vernacular Language") (public_name coq.vernac) (wrapped false) - (flags :standard -open Gramlib) (libraries tactics parsing)) (rule diff --git a/vernac/egramml.mli b/vernac/egramml.mli index a90ef97e7d..3689f60383 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -21,10 +21,10 @@ type 's grammar_prod_item = ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item val extend_vernac_command_grammar : - Vernacexpr.extend_name -> vernac_expr Pcoq.Entry.t option -> + extend_name -> vernac_expr Pcoq.Entry.t option -> vernac_expr grammar_prod_item list -> unit -val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list +val get_extend_vernac_rule : extend_name -> vernac_expr grammar_prod_item list val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index e6803443b3..befb4d7ccf 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -29,7 +29,7 @@ exception EvaluatedError of Pp.t * exn option let explain_exn_default = function (* Basic interaction exceptions *) | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") - | Plexing.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") + | Gramlib.Plexing.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err)) | Sys_error msg -> hov 0 (str "System error: " ++ guill msg) | Out_of_memory -> hov 0 (str "Out of memory.") diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 1d0a5ab0a3..3cdf81ced0 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -30,6 +30,7 @@ open Pcoq.Prim open Pcoq.Constr open Pcoq.Module open Pvernac.Vernac_ +open Attributes let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] let _ = List.iter CLexer.add_keyword vernac_kw @@ -989,8 +990,9 @@ GRAMMAR EXTEND Gram | IDENT "Scope"; s = IDENT -> { PrintScope s } | IDENT "Visibility"; s = OPT IDENT -> { PrintVisibility s } | IDENT "Implicit"; qid = smart_global -> { PrintImplicit qid } - | IDENT "Universes"; fopt = OPT ne_string -> { PrintUniverses (false, fopt) } - | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> { PrintUniverses (true, fopt) } + | b = [ IDENT "Sorted" -> { true } | -> { false } ]; IDENT "Universes"; + g = OPT printunivs_subgraph; fopt = OPT ne_string -> + { PrintUniverses (b, g, fopt) } | IDENT "Assumptions"; qid = smart_global -> { PrintAssumptions (false, false, qid) } | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, false, qid) } | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (false, true, qid) } @@ -1000,6 +1002,9 @@ GRAMMAR EXTEND Gram | IDENT "Registered" -> { PrintRegistered } ] ] ; + printunivs_subgraph: + [ [ IDENT "Subgraph"; "("; l = LIST0 reference; ")" -> { l } ] ] + ; class_rawexpr: [ [ IDENT "Funclass" -> { FunClass } | IDENT "Sortclass" -> { SortClass } diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ba31f73030..6c7117b513 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -884,8 +884,6 @@ let explain_not_match_error = function let status b = if b then str"polymorphic" else str"monomorphic" in str "a " ++ status b ++ str" declaration was expected, but a " ++ status (not b) ++ str" declaration was found" - | IncompatibleInstances -> - str"polymorphic universe instances do not match" | IncompatibleUniverses incon -> str"the universe constraints are inconsistent: " ++ Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon @@ -894,11 +892,22 @@ let explain_not_match_error = function quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t1) ++ spc () ++ str "compared to " ++ spc () ++ quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2) - | IncompatibleConstraints cst -> - str " the expected (polymorphic) constraints do not imply " ++ - let cst = Univ.UContext.constraints (Univ.AUContext.repr cst) in - (** FIXME: provide a proper naming for the bound variables *) - quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst) + | IncompatibleConstraints { got; expect } -> + let open Univ in + let pr_auctx auctx = + let sigma = Evd.from_ctx + (UState.of_binders + (UnivNames.universe_binders_with_opt_names auctx None)) + in + let uctx = AUContext.repr auctx in + Printer.pr_universe_instance_constraints sigma + (UContext.instance uctx) + (UContext.constraints uctx) + in + str "incompatible polymorphic binders: got" ++ spc () ++ h 0 (pr_auctx got) ++ spc() ++ + str "but expected" ++ spc() ++ h 0 (pr_auctx expect) ++ + (if not (Int.equal (AUContext.size got) (AUContext.size expect)) then mt() else + fnl() ++ str "(incompatible constraints)") let explain_signature_mismatch l spec why = str "Signature components for label " ++ Label.print l ++ diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 3b041b7065..de020926f6 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -306,17 +306,18 @@ let universe_proof_terminator compute_guard hook = | Admitted (id,k,pe,ctx) -> admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) (); Feedback.feedback Feedback.AddedAxiom - | Proved (opaque,idopt,proof) -> - let is_opaque, export_seff = match opaque with - | Transparent -> false, true - | Opaque -> true, false - in - let (id,(const,univs,persistence)) = Pfedit.cook_this_proof proof in - let const = {const with const_entry_opaque = is_opaque} in - let id = match idopt with - | None -> id - | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in - save ~export_seff id const univs compute_guard persistence (hook (Some univs)) + | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) -> + let is_opaque, export_seff = match opaque with + | Transparent -> false, true + | Opaque -> true, false + in + let const = {const with const_entry_opaque = is_opaque} in + let id = match idopt with + | None -> id + | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in + save ~export_seff id const universes compute_guard persistence (hook (Some universes)) + | Proved (opaque,idopt, _ ) -> + CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term") end let standard_proof_terminator compute_guard hook = @@ -330,7 +331,7 @@ let initialize_named_context_for_proof () = let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val -let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = +let start_proof id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook = let terminator = match terminator with | None -> standard_proof_terminator compute_guard hook | Some terminator -> terminator compute_guard hook @@ -340,19 +341,21 @@ let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard= | Some sign -> sign | None -> initialize_named_context_for_proof () in - Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator + let goals = [ Global.env_of_context sign , c ] in + Proof_global.start_proof sigma id ?pl kind goals terminator -let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = +let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook = let terminator = match terminator with | None -> universe_proof_terminator compute_guard hook | Some terminator -> terminator compute_guard hook in - let sign = + let sign = match sign with | Some sign -> sign | None -> initialize_named_context_for_proof () in - Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator + let goals = [ Global.env_of_context sign , c ] in + Proof_global.start_proof sigma id ?pl kind goals terminator let rec_tac_initializer finite guard thms snl = if finite then @@ -372,22 +375,17 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook = let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in let init_tac,guard = match recguard with | Some (finite,guard,init_tac) -> - let rec_tac = rec_tac_initializer finite guard thms snl in - Some (match init_tac with - | None -> - if Flags.is_auto_intros () then - Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms) - else - rec_tac + let rec_tac = rec_tac_initializer finite guard thms snl in + Some (match init_tac with + | None -> + Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms) | Some tacl -> - Tacticals.New.tclTHENS rec_tac - (if Flags.is_auto_intros () then - List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms - else - tacl)),guard + Tacticals.New.tclTHENS rec_tac + List.(map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms) + ),guard | None -> - let () = match thms with [_] -> () | _ -> assert false in - (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in + let () = match thms with [_] -> () | _ -> assert false in + Some (intro_tac (List.hd thms)), [] in match thms with | [] -> anomaly (Pp.str "No proof to start.") | (id,(t,(_,imps)))::other_thms -> @@ -408,7 +406,11 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook = List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; call_hook (fun exn -> exn) hook strength ref) thms_data in - start_proof_univs id ~pl:decl kind sigma t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard + start_proof_univs id ~pl:decl kind sigma t (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard; + ignore (Proof_global.with_current_proof (fun _ p -> + match init_tac with + | None -> p,(true,[]) + | Some tac -> Proof.run_tactic Global.(env ()) tac p)) let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in @@ -418,8 +420,8 @@ let start_proof_com ?inference_hook kind thms hook = let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in let flags = all_and_fail_flags in - let flags = { flags with use_hook = inference_hook } in - let evd = solve_remaining_evars flags env evd Evd.empty in + let hook = inference_hook in + let evd = solve_remaining_evars ?hook flags env evd Evd.empty in let ids = List.map RelDecl.get_name ctx in check_name_freshness (pi1 kind) id; (* XXX: The nf_evar is critical !! *) diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 195fcbf4ca..246d8cbe6d 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -18,13 +18,13 @@ val call_hook : Future.fix_exn -> declaration_hook -> Decl_kinds.locality -> Glo val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> declaration_hook -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> + ?compute_guard:Proof_global.lemma_possible_guards -> declaration_hook -> unit val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> declaration_hook) -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> + ?compute_guard:Proof_global.lemma_possible_guards -> (UState.t option -> declaration_hook) -> unit val start_proof_com : diff --git a/vernac/obligations.ml b/vernac/obligations.ml index c2805674e4..8baf391c70 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -826,26 +826,41 @@ let rec string_of_list sep f = function | 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 solve_by_tac name evi t poly ctx = +let solve_by_tac ?loc name evi t poly ctx = let id = name in (* spiwack: the status is dropped. *) - let (entry,_,ctx') = Pfedit.build_constant_by_tactic - id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in - let env = Global.env () in - let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in - let body, () = Future.force entry.const_entry_body in - let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in - Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); - (fst body), entry.const_entry_type, Evd.evar_universe_context ctx' + try + let (entry,_,ctx') = + Pfedit.build_constant_by_tactic + id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in + let env = Global.env () in + let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in + let body, () = Future.force entry.const_entry_body in + let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in + Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); + Some (fst body, entry.const_entry_type, Evd.evar_universe_context ctx') + with + | Refiner.FailError (_, s) as exn -> + let _ = CErrors.push exn in + 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 + | e when CErrors.noncritical e -> + let err = CErrors.print e in + warn_solve_errored ?loc err; + None let obligation_terminator name num guard hook auto pf = let open Proof_global in let term = Lemmas.universe_proof_terminator guard hook in match pf with | Admitted _ -> apply_terminator term pf - | Proved (opq, id, proof) -> - let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in + | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin let env = Global.env () in let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in let ty = entry.Entries.const_entry_type in @@ -904,6 +919,9 @@ let obligation_terminator name num guard hook auto pf = with e when CErrors.noncritical e -> let e = CErrors.push e in pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) + end + | Proved (_, _, _ ) -> + CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term") let obligation_hook prg obl num auto ctx' _ gr = let obls, rem = prg.prg_obligations in @@ -987,41 +1005,34 @@ and solve_obligation_by_tac prg obls i tac = match obl.obl_body with | Some _ -> None | None -> - try - if List.is_empty (deps_remaining obls obl.obl_deps) then - let obl = subst_deps_obl obls obl in - let tac = - match tac with - | Some t -> t - | None -> - match obl.obl_tac with - | Some t -> t - | None -> !default_tactic - in - let evd = Evd.from_ctx prg.prg_ctx in - let evd = Evd.update_sigma_env evd (Global.env ()) in - let t, ty, ctx = - solve_by_tac obl.obl_name (evar_of_obligation obl) tac - (pi2 prg.prg_kind) (Evd.evar_universe_context evd) - in - let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in - let prg = {prg with prg_ctx = ctx} in - let def, obl' = declare_obligation prg obl t ty uctx in - obls.(i) <- obl'; - if def && not (pi2 prg.prg_kind) 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 {prg with prg_ctx = ctx'}) - else Some prg - else None - with e when CErrors.noncritical e -> - let (e, _) = CErrors.push e in - match e with - | Refiner.FailError (_, s) -> - user_err ?loc:(fst obl.obl_location) ~hdr:"solve_obligation" (Lazy.force s) - | e -> None (* FIXME really ? *) + if List.is_empty (deps_remaining obls obl.obl_deps) then + let obl = subst_deps_obl obls obl in + let tac = + match tac with + | Some t -> t + | None -> + match obl.obl_tac with + | Some t -> t + | None -> !default_tactic + in + let evd = Evd.from_ctx prg.prg_ctx in + let evd = Evd.update_sigma_env evd (Global.env ()) in + match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac + (pi2 prg.prg_kind) (Evd.evar_universe_context evd) with + | None -> None + | Some (t, ty, ctx) -> + let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let prg = {prg with prg_ctx = ctx} in + let def, obl' = declare_obligation prg obl t ty uctx in + obls.(i) <- obl'; + if def && not (pi2 prg.prg_kind) 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 {prg with prg_ctx = ctx'}) + else Some prg + else None and solve_prg_obligations prg ?oblset tac = let obls, rem = prg.prg_obligations in diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 1c1faca599..2ddd210365 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -492,12 +492,13 @@ open Pputils keyword "Print Hint *" | PrintHintDbName s -> keyword "Print HintDb" ++ spc () ++ str s - | PrintUniverses (b, fopt) -> + | PrintUniverses (b, g, fopt) -> let cmd = if b then "Print Sorted Universes" else "Print Universes" in - keyword cmd ++ pr_opt str fopt + let pr_subgraph = prlist_with_sep spc pr_qualid in + keyword cmd ++ pr_opt pr_subgraph g ++ pr_opt str fopt | PrintName (qid,udecl) -> keyword "Print" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list udecl | PrintModuleType qid -> @@ -1213,6 +1214,7 @@ open Pputils let rec pr_vernac_flag (k, v) = let k = keyword k in + let open Attributes in match v with | VernacFlagEmpty -> k | VernacFlagLeaf v -> k ++ str " = " ++ qs v diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index b2fa8ec99f..4761e4bbc2 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -42,7 +42,7 @@ module Vernac_ = let command_entry_ref = ref noedit_mode let command_entry = Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.Entry.parse_token !command_entry_ref strm) + (fun strm -> Gram.Entry.parse_token_stream !command_entry_ref strm) end diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1fab35b650..a78329ad1d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -319,7 +319,7 @@ let print_registered () = hov 0 (prlist_with_sep fnl pr_lib_ref @@ Coqlib.get_lib_refs ()) -let dump_universes_gen g s = +let dump_universes_gen prl g s = let output = open_out s in let output_constraint, close = if Filename.check_suffix s ".dot" || Filename.check_suffix s ".gv" then begin @@ -344,10 +344,12 @@ let dump_universes_gen g s = | Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=" - in Printf.fprintf output "%s %s %s ;\n" left kind right + in + Printf.fprintf output "%s %s %s ;\n" left kind right end, (fun () -> close_out output) end in + let output_constraint k l r = output_constraint k (prl l) (prl r) in try UGraph.dump_universes output_constraint g; close (); @@ -357,6 +359,36 @@ let dump_universes_gen g s = close (); iraise reraise +let universe_subgraph ?loc g univ = + let open Univ in + let sigma = Evd.from_env (Global.env()) in + let univs_of q = + let q = Glob_term.(GType (UNamed q)) in + (* this function has a nice error message for not found univs *) + LSet.singleton (Pretyping.interp_known_glob_level ?loc sigma q) + in + let univs = List.fold_left (fun univs q -> LSet.union univs (univs_of q)) LSet.empty g in + let csts = UGraph.constraints_for ~kept:(LSet.add Level.prop (LSet.add Level.set univs)) univ in + let univ = LSet.fold UGraph.add_universe_unconstrained univs UGraph.initial_universes in + UGraph.merge_constraints csts univ + +let print_universes ?loc ~sort ~subgraph dst = + let univ = Global.universes () in + let univ = match subgraph with + | None -> univ + | Some g -> universe_subgraph ?loc g univ + in + let univ = if sort then UGraph.sort_universes univ else univ in + let pr_remaining = + if Global.is_joined_environment () then mt () + else str"There may remain asynchronous universe constraints" + in + let prl = UnivNames.pr_with_global_universes in + begin match dst with + | None -> UGraph.pr_universes prl univ ++ pr_remaining + | Some s -> dump_universes_gen (fun u -> Pp.string_of_ppcmds (prl u)) univ s + end + (*********************) (* "Locate" commands *) @@ -457,8 +489,7 @@ let start_proof_and_print k l hook = Evarutil.is_ground_term sigma concl) then raise Exit; let c, _, ctx = - Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) - concl (Tacticals.New.tclCOMPLETE tac) + Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) concl tac in Evd.set_universe_context sigma ctx, EConstr.of_constr c with Logic_monad.TacticFailure e when Logic.catchable_exception e -> user_err Pp.(str "The statement obligations could not be resolved \ @@ -1064,15 +1095,30 @@ let vernac_restore_state file = (* Commands *) let vernac_create_hintdb ~module_local id b = - Hints.create_hint_db module_local id full_transparent_state b - -let vernac_remove_hints ~module_local dbs ids = - Hints.remove_hints module_local dbs (List.map Smartlocate.global_with_alias ids) + Hints.create_hint_db module_local id TransparentState.full b + +let warn_implicit_core_hint_db = + CWarnings.create ~name:"implicit-core-hint-db" ~category:"deprecated" + (fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. " + ++ strbrk"Please specify a hint database.") + +let vernac_remove_hints ~module_local dbnames ids = + let dbnames = + if List.is_empty dbnames then + (warn_implicit_core_hint_db (); ["core"]) + else dbnames + in + Hints.remove_hints module_local dbnames (List.map Smartlocate.global_with_alias ids) -let vernac_hints ~atts lb h = +let vernac_hints ~atts dbnames h = + let dbnames = + if List.is_empty dbnames then + (warn_implicit_core_hint_db (); ["core"]) + else dbnames + in let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in let local = enforce_module_locality local in - Hints.add_hints ~local lb (Hints.interp_hints poly h) + Hints.add_hints ~local dbnames (Hints.interp_hints poly h) let vernac_syntactic_definition ~module_local lid x y = Dumpglob.dump_definition lid false "syndef"; @@ -1421,14 +1467,6 @@ let _ = let _ = declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "automatic introduction of variables"; - optkey = ["Automatic";"Introduction"]; - optread = Flags.is_auto_intros; - optwrite = Flags.make_auto_intros } - -let _ = - declare_bool_option { optdepr = false; optname = "coercion printing"; optkey = ["Printing";"Coercions"]; @@ -1826,17 +1864,7 @@ let vernac_print ~atts env sigma = | PrintCoercionPaths (cls,clt) -> Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt) | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma - | PrintUniverses (b, dst) -> - let univ = Global.universes () in - let univ = if b then UGraph.sort_universes univ else univ in - let pr_remaining = - if Global.is_joined_environment () then mt () - else str"There may remain asynchronous universe constraints" - in - begin match dst with - | None -> UGraph.pr_universes UnivNames.pr_with_global_universes univ ++ pr_remaining - | Some s -> dump_universes_gen univ s - end + | PrintUniverses (sort, subgraph, dst) -> print_universes ~sort ~subgraph dst | PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r) | PrintHintGoal -> Hints.pr_applicable_hint () | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 594e9eca48..122005e011 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -45,7 +45,7 @@ type printable = | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr | PrintCanonicalConversions - | PrintUniverses of bool * string option + | PrintUniverses of bool * qualid list option * string option | PrintHint of qualid or_by_notation | PrintHintGoal | PrintHintDbName of string @@ -219,13 +219,6 @@ type section_subset_expr = {b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command. *) -type extend_name = - (** Name of the vernac entry where the tactic is defined, typically found - after the VERNAC EXTEND statement in the source. *) - string * - (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch - is given an offset, starting from zero. *) - int (* This type allows registering the inlining of constants in native compiler. It will be extended with primitive inductive types and operators *) @@ -253,6 +246,14 @@ type vernac_argument_status = { implicit_status : vernac_implicit_status; } +type extend_name = + (** Name of the vernac entry where the tactic is defined, typically found + after the VERNAC EXTEND statement in the source. *) + string * + (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch + is given an offset, starting from zero. *) + int + type nonrec vernac_expr = | VernacLoad of verbose_flag * string @@ -395,71 +396,11 @@ type nonrec vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list -type vernac_flags = vernac_flag list -and vernac_flag = string * vernac_flag_value -and vernac_flag_value = - | VernacFlagEmpty - | VernacFlagLeaf of string - | VernacFlagList of vernac_flags - type vernac_control = - | VernacExpr of vernac_flags * vernac_expr + | VernacExpr of Attributes.vernac_flags * vernac_expr (* boolean is true when the `-time` batch-mode command line flag was set. the flag is used to print differently in `-time` vs `Time foo` *) | VernacTime of bool * vernac_control CAst.t | VernacRedirect of string * vernac_control CAst.t | VernacTimeout of int * vernac_control | VernacFail of vernac_control - -(* A vernac classifier provides information about the exectuion of a - command: - - - vernac_when: encodes if the vernac may alter the parser [thus - forcing immediate execution], or if indeed it is pure and parsing - can continue without its execution. - - - vernac_type: if it is starts, ends, continues a proof or - alters the global state or is a control command like BackTo or is - a query like Check. - - The classification works on the assumption that we have 3 states: - parsing, execution (global enviroment, etc...), and proof - state. For example, commands that only alter the proof state are - considered safe to delegate to a worker. - -*) -type vernac_type = - (* Start of a proof *) - | VtStartProof of vernac_start - (* Command altering the global state, bad for parallel - processing. *) - | VtSideff of vernac_sideff_type - (* End of a proof *) - | VtQed of vernac_qed_type - (* A proof step *) - | VtProofStep of proof_step - (* To be removed *) - | VtProofMode of string - (* Queries are commands assumed to be "pure", that is to say, they - don't modify the interpretation state. *) - | VtQuery - (* To be removed *) - | VtMeta - | VtUnknown -and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) -and vernac_start = string * opacity_guarantee * Id.t list -and vernac_sideff_type = Id.t list -and opacity_guarantee = - | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) - | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) -and proof_step = { (* TODO: inline with OCaml 4.03 *) - parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; - proof_block_detection : proof_block_name option -} -and solving_tac = bool (* a terminator *) -and anon_abstracting_tac = bool (* abstracting anonymously its result *) -and proof_block_name = string (* open type of delimiters *) -type vernac_when = - | VtNow - | VtLater -type vernac_classification = vernac_type * vernac_when diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 5fba586298..3a321ecdb4 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -12,7 +12,43 @@ open Util open Pp open CErrors -type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t +type vernac_type = + (* Start of a proof *) + | VtStartProof of vernac_start + (* Command altering the global state, bad for parallel + processing. *) + | VtSideff of vernac_sideff_type + (* End of a proof *) + | VtQed of vernac_qed_type + (* A proof step *) + | VtProofStep of { + parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; + proof_block_detection : proof_block_name option + } + (* To be removed *) + | VtProofMode of string + (* Queries are commands assumed to be "pure", that is to say, they + don't modify the interpretation state. *) + | VtQuery + (* To be removed *) + | VtMeta + | VtUnknown +and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) +and vernac_start = string * opacity_guarantee * Names.Id.t list +and vernac_sideff_type = Names.Id.t list +and opacity_guarantee = + | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) + | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) +and solving_tac = bool (** a terminator *) +and anon_abstracting_tac = bool (** abstracting anonymously its result *) +and proof_block_name = string (** open type of delimiters *) + +type vernac_when = + | VtNow + | VtLater +type vernac_classification = vernac_type * vernac_when + +type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t type plugin_args = Genarg.raw_generic_argument list @@ -68,10 +104,23 @@ let call opn converted_args ~atts ~st = (** VERNAC EXTEND registering *) -type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification +type classifier = Genarg.raw_generic_argument list -> vernac_classification + +(** Classifiers *) +let classifiers : classifier array String.Map.t ref = ref String.Map.empty + +let get_vernac_classifier (name, i) args = + (String.Map.find name !classifiers).(i) args + +let declare_vernac_classifier name f = + classifiers := String.Map.add name f !classifiers + +let classify_as_query = VtQuery, VtLater +let classify_as_sideeff = VtSideff [], VtLater +let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater type (_, _) ty_sig = -| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig +| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig @@ -124,7 +173,7 @@ let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s | TUentry a -> Aentry (Pcoq.genarg_grammar (Genarg.ExtraArg a)) | TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (Genarg.ExtraArg a), string_of_int i) -let rec untype_grammar : type r s. (r, s) ty_sig -> Vernacexpr.vernac_expr Egramml.grammar_prod_item list = function +let rec untype_grammar : type r s. (r, s) ty_sig -> 'a Egramml.grammar_prod_item list = function | TyNil -> [] | TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty | TyNonTerminal (tu, ty) -> @@ -132,16 +181,6 @@ let rec untype_grammar : type r s. (r, s) ty_sig -> Vernacexpr.vernac_expr Egram let symb = untype_user_symbol tu in Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty -let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol - -let classifiers : classifier array String.Map.t ref = ref String.Map.empty - -let get_vernac_classifier (name, i) args = - (String.Map.find name !classifiers).(i) args - -let declare_vernac_classifier name f = - classifiers := String.Map.add name f !classifiers - let vernac_extend ~command ?classifier ?entry ext = let get_classifier (TyML (_, ty, _, cl)) = match cl with | Some cl -> untype_classifier ty cl diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index bb94f3a6a9..7feaccd9a3 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -8,20 +8,75 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(** Vernacular Extension data *) + +(* A vernac classifier provides information about the exectuion of a + command: + + - vernac_when: encodes if the vernac may alter the parser [thus + forcing immediate execution], or if indeed it is pure and parsing + can continue without its execution. + + - vernac_type: if it is starts, ends, continues a proof or + alters the global state or is a control command like BackTo or is + a query like Check. + + The classification works on the assumption that we have 3 states: + parsing, execution (global enviroment, etc...), and proof + state. For example, commands that only alter the proof state are + considered safe to delegate to a worker. + +*) +type vernac_type = + (* Start of a proof *) + | VtStartProof of vernac_start + (* Command altering the global state, bad for parallel + processing. *) + | VtSideff of vernac_sideff_type + (* End of a proof *) + | VtQed of vernac_qed_type + (* A proof step *) + | VtProofStep of { + parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; + proof_block_detection : proof_block_name option + } + (* To be removed *) + | VtProofMode of string + (* Queries are commands assumed to be "pure", that is to say, they + don't modify the interpretation state. *) + | VtQuery + (* To be removed *) + | VtMeta + | VtUnknown +and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) +and vernac_start = string * opacity_guarantee * Names.Id.t list +and vernac_sideff_type = Names.Id.t list +and opacity_guarantee = + | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) + | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) +and solving_tac = bool (** a terminator *) +and anon_abstracting_tac = bool (** abstracting anonymously its result *) +and proof_block_name = string (** open type of delimiters *) + +type vernac_when = + | VtNow + | VtLater +type vernac_classification = vernac_type * vernac_when + (** Interpretation of extended vernac phrases. *) -type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t +type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t type plugin_args = Genarg.raw_generic_argument list -val call : Vernacexpr.extend_name -> plugin_args -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t +val call : Vernacexpr.extend_name -> plugin_args -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t (** {5 VERNAC EXTEND} *) -type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification +type classifier = Genarg.raw_generic_argument list -> vernac_classification type (_, _) ty_sig = -| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig +| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> @@ -32,7 +87,7 @@ type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> (** Wrapper to dynamically extend vernacular commands. *) val vernac_extend : command:string -> - ?classifier:(string -> Vernacexpr.vernac_classification) -> + ?classifier:(string -> vernac_classification) -> ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t -> ty_ml list -> unit @@ -55,6 +110,9 @@ val vernac_argument_extend : name:string -> 'a vernac_argument -> ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t (** {5 STM classifiers} *) +val get_vernac_classifier : Vernacexpr.extend_name -> classifier -val get_vernac_classifier : - Vernacexpr.extend_name -> classifier +(** Standard constant classifiers *) +val classify_as_query : vernac_classification +val classify_as_sideeff : vernac_classification +val classify_as_proofstep : vernac_classification |