From bd91698e1acdc5e579f904e3f52e40a57bd6cd13 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 8 Oct 2003 12:37:03 +0000 Subject: Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé incomplètement prouvé comme axiome MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4543 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/xlate.ml | 12 +++++++----- library/decl_kinds.ml | 2 ++ parsing/g_proofs.ml4 | 20 +++++++++----------- parsing/g_proofsnew.ml4 | 15 +++++++++------ parsing/g_vernac.ml4 | 3 ++- parsing/g_vernacnew.ml4 | 6 ++++-- proofs/pfedit.ml | 5 +++++ proofs/pfedit.mli | 6 ++++++ toplevel/command.ml | 25 +++++++++++++++++++------ toplevel/command.mli | 4 ++++ toplevel/vernacentries.ml | 10 ++++++---- toplevel/vernacexpr.ml | 6 +++++- translate/ppvernacnew.ml | 7 +++---- 13 files changed, 81 insertions(+), 40 deletions(-) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index b7fbd7fc8..244b0543d 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1202,7 +1202,8 @@ let xlate_thm x = CT_thm (match x with | Theorem -> "Theorem" | Remark -> "Remark" | Lemma -> "Lemma" - | Fact -> "Fact") + | Fact -> "Fact" + | Conjecture -> "Conjecture") let xlate_defn x = CT_defn (match x with @@ -1416,16 +1417,17 @@ let xlate_vernac = CT_hints(CT_ident "Unfold", CT_id_ne_list(n1, names), dblist)) - | VernacEndProof (true,None) -> + | VernacEndProof (Proved (true,None)) -> CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE) - | VernacEndProof (false,None) -> + | VernacEndProof (Proved (false,None)) -> CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Definition"), ctv_ID_OPT_NONE) - | VernacEndProof (b,Some (s, Some kind)) -> + | VernacEndProof (Proved (b,Some (s, Some kind))) -> CT_save (CT_coerce_THM_to_THM_OPT (xlate_thm kind), ctf_ID_OPT_SOME (xlate_ident s)) - | VernacEndProof (b,Some (s,None)) -> + | VernacEndProof (Proved (b,Some (s,None))) -> CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctf_ID_OPT_SOME (xlate_ident s)) + | VernacEndProof Admitted -> xlate_error "TODO: Admitted" | VernacSetOpacity (false, id :: idl) -> CT_transparent(CT_id_ne_list(loc_qualid_to_ct_ID id, List.map loc_qualid_to_ct_ID idl)) diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 10ae3d79b..a47fb9086 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -17,6 +17,7 @@ type theorem_kind = | Lemma | Fact | Remark + | Conjecture type definitionkind = | LDefinition @@ -63,6 +64,7 @@ type local_theorem_kind = LocalStatement type 'a mathematical_kind = | IsAssumption of type_as_formula_kind | IsDefinition + | IsConjecture | IsProof of 'a type global_kind = theorem_kind mathematical_kind diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 11d70529d..1cc9f038f 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -36,23 +36,21 @@ GEXTEND Gram ; command: [ [ IDENT "Goal"; c = Constr.constr -> VernacGoal c -(*VernacGoal c*) -(* | IDENT "Goal" -> VernacGoal None*) | "Proof" -> VernacProof Tacexpr.TacId | "Proof"; "with"; ta = tactic -> VernacProof ta -(* Used ?? - | IDENT "Begin" -> VernacNop -*) | IDENT "Abort" -> VernacAbort None | IDENT "Abort"; IDENT "All" -> VernacAbortAll | IDENT "Abort"; id = identref -> VernacAbort (Some id) - | "Qed" -> VernacEndProof (true,None) - | IDENT "Save" -> VernacEndProof (true,None) - | IDENT "Defined" -> VernacEndProof (false,None) - | IDENT "Defined"; id=base_ident -> VernacEndProof (false,Some (id,None)) + | IDENT "Admitted" -> VernacEndProof Admitted + | "Qed" -> VernacEndProof (Proved (true,None)) + | IDENT "Save" -> VernacEndProof (Proved (true,None)) + | IDENT "Defined" -> VernacEndProof (Proved (false,None)) + | IDENT "Defined"; id=base_ident -> + VernacEndProof (Proved (false,Some (id,None))) | IDENT "Save"; tok = thm_token; id = base_ident -> - VernacEndProof (true,Some (id,Some tok)) - | IDENT "Save"; id = base_ident -> VernacEndProof (true,Some (id,None)) + VernacEndProof (Proved (true,Some (id,Some tok))) + | IDENT "Save"; id = base_ident -> + VernacEndProof (Proved (true,Some (id,None))) | IDENT "Suspend" -> VernacSuspend | IDENT "Resume" -> VernacResume None | IDENT "Resume"; id = identref -> VernacResume (Some id) diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4 index f9f731b31..eb1b3e466 100644 --- a/parsing/g_proofsnew.ml4 +++ b/parsing/g_proofsnew.ml4 @@ -43,13 +43,16 @@ GEXTEND Gram | IDENT "Abort"; id = identref -> VernacAbort (Some id) | IDENT "Existential"; n = natural; c = constr_body -> VernacSolveExistential (n,c) - | IDENT "Qed" -> VernacEndProof (true,None) - | IDENT "Save" -> VernacEndProof (true,None) + | IDENT "Admitted" -> VernacEndProof Admitted + | IDENT "Qed" -> VernacEndProof (Proved (true,None)) + | IDENT "Save" -> VernacEndProof (Proved (true,None)) | IDENT "Save"; tok = thm_token; id = base_ident -> - VernacEndProof (true,Some (id,Some tok)) - | IDENT "Save"; id = base_ident -> VernacEndProof (true,Some (id,None)) - | IDENT "Defined" -> VernacEndProof (false,None) - | IDENT "Defined"; id=base_ident -> VernacEndProof (false,Some (id,None)) + VernacEndProof (Proved (true,Some (id,Some tok))) + | IDENT "Save"; id = base_ident -> + VernacEndProof (Proved (true,Some (id,None))) + | IDENT "Defined" -> VernacEndProof (Proved (false,None)) + | IDENT "Defined"; id=base_ident -> + VernacEndProof (Proved (false,Some (id,None))) | IDENT "Suspend" -> VernacSuspend | IDENT "Resume" -> VernacResume None | IDENT "Resume"; id = identref -> VernacResume (Some id) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 16d2ba9c5..49f8b0d85 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -108,7 +108,8 @@ GEXTEND Gram [ [ "Theorem" -> Theorem | IDENT "Lemma" -> Lemma | IDENT "Fact" -> Fact - | IDENT "Remark" -> Remark ] ] + | IDENT "Remark" -> Remark + | IDENT "Conjecture" -> Conjecture ] ] ; def_token: [ [ "Definition" -> (fun _ _ -> ()), Global, GDefinition diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index d86952e25..8e0088890 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -63,7 +63,8 @@ GEXTEND Gram ; subgoal_command: [ [ c = check_command; "." -> c - | tac = Tactic.tactic; use_dft_tac = [ "." -> false | "..." -> true ] -> + | tac = Tactic.tactic; + use_dft_tac = [ "." -> false | [ "..." | ".."; "." ] -> true ] -> (fun g -> let g = match g with Some gl -> gl | _ -> 1 in VernacSolve(g,tac,use_dft_tac)) ] ] @@ -135,7 +136,8 @@ GEXTEND Gram [ [ "Theorem" -> Theorem | IDENT "Lemma" -> Lemma | IDENT "Fact" -> Fact - | IDENT "Remark" -> Remark ] ] + | IDENT "Remark" -> Remark + | IDENT "Conjecture" -> Conjecture ] ] ; def_token: [ [ "Definition" -> (fun _ _ -> ()), Global, GDefinition diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 4f8d8b07f..7f8e74862 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -195,6 +195,11 @@ let cook_proof () = const_entry_opaque = true }, strength, ts.top_hook)) +let current_proof_statement () = + let ts = get_topstate() in + (get_current_proof_name (), ts.top_strength, + ts.top_goal.evar_concl, ts.top_hook) + (*********************************************************************) (* Abort functions *) (*********************************************************************) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 9585e7b3c..f4cc32a55 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -107,6 +107,7 @@ val set_xml_cook_proof : (pftreestate -> unit) -> unit val get_pftreestate : unit -> pftreestate (* [get_end_tac ()] returns the current tactic to apply to all new subgoal *) + val get_end_tac : unit -> tactic option (* [get_goal_context n] returns the context of the [n]th subgoal of @@ -119,6 +120,11 @@ val get_goal_context : int -> Evd.evar_map * env val get_current_goal_context : unit -> Evd.evar_map * env +(* [current_proof_statement] *) + +val current_proof_statement : + unit -> identifier * goal_kind * types * declaration_hook + (*s [get_current_proof_name ()] return the name of the current focused proof or failed if no proof is focused *) diff --git a/toplevel/command.ml b/toplevel/command.ml index 78d208437..743f1337a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -80,6 +80,9 @@ let rec adjust_conclusion a cs = function (* 1| Constant definitions *) +let definition_message id = + if_verbose message ((string_of_id id) ^ " is defined") + let constant_entry_of_com (bl,com,comtypopt,opacity) = let sigma = Evd.empty in let env = Global.env() in @@ -110,7 +113,7 @@ let declare_global_definition ident ce local = let (_,kn) = declare_constant ident (DefinitionEntry ce,IsDefinition) in if local = Local then msg_warning (pr_id ident ++ str" is declared as a global definition"); - if_verbose message ((string_of_id ident) ^ " is defined"); + definition_message ident; ConstRef kn let declare_definition ident local bl red_option c typopt hook = @@ -123,7 +126,7 @@ let declare_definition ident local bl red_option c typopt hook = let c = SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type,false) in let _ = declare_variable ident (Lib.cwd(), c, IsDefinition) in - if_verbose message ((string_of_id ident) ^ " is defined"); + definition_message ident; if Pfedit.refining () then msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ str" is not visible from current goals"); @@ -178,14 +181,15 @@ let non_type_eliminations = let declare_one_elimination ind = let (mib,mip) = Global.lookup_inductive ind in let mindstr = string_of_id mip.mind_typename in - let declare na c t = - let kn = Declare.declare_constant (id_of_string na) + let declare s c t = + let id = id_of_string s in + let kn = Declare.declare_constant id (DefinitionEntry { const_entry_body = c; const_entry_type = t; const_entry_opaque = false }, Decl_kinds.IsDefinition) in - Options.if_verbose ppnl (str na ++ str " is defined"); + definition_message id; kn in let env = Global.env () in @@ -655,7 +659,7 @@ let save id const kind hook = (Global, ConstRef kn) in hook l r; Pfedit.delete_current_proof (); - if_verbose message ((string_of_id id) ^ " is defined") + definition_message id let save_named opacity = let id,(const,persistence,hook) = Pfedit.cook_proof () in @@ -682,6 +686,15 @@ let save_anonymous_with_strength kind opacity save_ident = (* we consider that non opaque behaves as local for discharge *) save save_ident const (IsGlobal (Proof kind)) hook +let admit () = + let (id,k,typ,hook) = Pfedit.current_proof_statement () in + if k <> IsGlobal (Proof Conjecture) then + error "Only statements declared as conjecture can be admitted"; + let (_,kn) = declare_constant id (ParameterEntry typ, IsConjecture) in + hook Global (ConstRef kn); + Pfedit.delete_current_proof (); + assumption_message id + let get_current_context () = try Pfedit.get_current_goal_context () with e when Logic.catchable_exception e -> diff --git a/toplevel/command.mli b/toplevel/command.mli index 525ca0f18..c12a49485 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -74,6 +74,10 @@ val save_anonymous : bool -> identifier -> unit val save_anonymous_with_strength : theorem_kind -> bool -> identifier -> unit +(* [admit ()] aborts the current goal and save it as an assmumption *) + +val admit : unit -> unit + (* [get_current_context ()] returns the evar context and env of the current open proof if any, otherwise returns the empty evar context and the current global env *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0cb0b54e1..6665af74c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -308,9 +308,11 @@ let vernac_start_proof kind sopt (bl,t) lettop hook = (str "Proof editing mode not supported in module types"); start_proof_and_print sopt (IsGlobal (Proof kind)) (bl,t) hook -let vernac_end_proof is_opaque idopt = - if_verbose show_script (); - match idopt with +let vernac_end_proof = function + | Admitted -> admit () + | Proved (is_opaque,idopt) -> + if_verbose show_script (); + match idopt with | None -> save_named is_opaque | Some (id,None) -> save_anonymous is_opaque id | Some (id,Some kind) -> save_anonymous_with_strength kind is_opaque id @@ -1119,7 +1121,7 @@ let interp c = match c with | VernacDefinition (k,id,d,f,_) -> vernac_definition k id d f | VernacStartTheoremProof (k,id,t,top,f) -> vernac_start_proof k (Some id) t top f - | VernacEndProof (opaq,idopt) -> vernac_end_proof opaq idopt + | VernacEndProof e -> vernac_end_proof e | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,l) -> vernac_assumption stre l | VernacInductive (finite,l) -> vernac_inductive finite l diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index aa307203f..5f3ff5444 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -142,6 +142,10 @@ type local_decl_expr = type module_binder = identifier list * module_type_ast +type proof_end = + | Admitted + | Proved of opacity_flag * (identifier * theorem_kind option) option + type vernac_expr = (* Control *) | VernacList of located_vernac_expr list @@ -175,7 +179,7 @@ type vernac_expr = declaration_hook * definitionkind | VernacStartTheoremProof of theorem_kind * identifier * (local_binder list * constr_expr) * bool * declaration_hook - | VernacEndProof of opacity_flag * (identifier * theorem_kind option) option + | VernacEndProof of proof_end | VernacExactProof of constr_expr | VernacAssumption of assumption_kind * simple_binder with_coercion list | VernacInductive of inductive_flag * inductive_expr list diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index e4fa125e1..b04ff3efc 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -382,6 +382,7 @@ let pr_thm_token = function | Decl_kinds.Lemma -> str"Lemma" | Decl_kinds.Fact -> str"Fact" | Decl_kinds.Remark -> str"Remark" + | Decl_kinds.Conjecture -> str"Conjecture" let pr_require_token = function | Some true -> str "Export" @@ -630,11 +631,9 @@ let rec pr_vernac = function (match bl with | [] -> mt() | _ -> error "Statements with local binders no longer supported") -(* -pr_vbinders bl ++ spc()) -*) ++ str":" ++ spc() ++ pr_type c) - | VernacEndProof (opac,o) -> (match o with + | VernacEndProof Admitted -> str"Admitted" + | VernacEndProof (Proved (opac,o)) -> (match o with | None -> if opac then str"Qed" else str"Defined" | Some (id,th) -> (match th with | None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_id id -- cgit v1.2.3