Ajout du Let pour le langage de tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 90 insertions, 22 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 56077f36e..b6824dac7 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -19,9 +19,15 @@ open Declare
 (* strength * strength -> bool *)
 
 let stre_gt = function
-  | (NeverDischarge,NeverDischarge) -> false
-  | (NeverDischarge,x) -> false
-  | (x,NeverDischarge) -> true
+(*  | (x,y) when (x = NeverDischarge || x = NotDeclare)
+            && (y = NeverDischarge || y = NotDeclare) -> false
+  | (x,_) when x = NeverDischarge || x = NotDeclare -> false
+  | (_,x) when x = NeverDischarge || x = NotDeclare -> true*)
+
+  | (NeverDischarge,_) -> false
+  | (NotDeclare,_) -> false
+  | (_,NeverDischarge) -> true
+  | (_,NotDeclare) -> true
   | (DischargeAt sp1,DischargeAt sp2) ->
       dirpath_prefix_of sp1 sp2 (* was sp_gt but don't understand why - HH *)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 68d045512..d1b9ba4fe 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -17,6 +17,8 @@ open Ast
 open Library
 open Libobject
 open Astterm
+open Proof_type
+open Tacmach
 
 let mkCastC(c,t) = ope("CAST",[c;t])
 let mkLambdaC(x,a,b) = ope("LAMBDA",[a;slam(Some (string_of_id x),b)])
@@ -77,6 +79,9 @@ let definition_body_red red_option ident (local,n) com comtypeopt =
         end
 	else
 	  declare_global_definition ident ce' n true
+    | NotDeclare ->
+      anomalylabstrm "Command.definition_body_red"
+        [<'sTR "Strength NotDeclare not for Definition, only for Let" >]
 
 let definition_body = definition_body_red None
 
@@ -113,6 +118,9 @@ let hypothesis_def_var is_refining ident n c =
         end
 	else
 	  declare_global_assumption ident c
+    | NotDeclare ->
+      anomalylabstrm "Command.hypothesis_def_var"
+        [<'sTR "Strength NotDeclare not for Variable, only for Let" >]
 
 (* 3| Mutual Inductive definitions *)
 
@@ -413,33 +421,52 @@ let start_proof_com sopt stre com =
   in
   Pfedit.start_proof id stre sign (interp_type Evd.empty env com)
 
-let save_named opacity =
-  let id,(const,strength) = Pfedit.cook_proof () in
+let apply_tac_not_declare id pft = function
+  | None -> error "Type of Let missing"
+  | Some typ ->
+    let cutt = vernac_tactic ("Cut",[Constr typ])
+    and exat = vernac_tactic ("Exact",[Constr pft]) in
+    Pfedit.delete_current_proof ();
+    Pfedit.by (tclTHENS cutt [introduction id;exat])
+
+let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const)
+  strength =
   begin match strength with
     | DischargeAt disch_sp when Lib.is_section_p disch_sp ->
 	let c = constr_of_constr_entry const in
 	declare_variable id (SectionLocalDef c,strength,opacity)
-    | _ ->
-	declare_constant id (ConstantEntry const,strength,opacity)
+    | NeverDischarge | DischargeAt _ ->
+        declare_constant id (ConstantEntry const,strength,opacity)
+    | NotDeclare -> apply_tac_not_declare id pft tpo
   end;
-  Pfedit.delete_current_proof ();
-  if Options.is_verbose() then message ((string_of_id id) ^ " is defined")
+  if not (strength = NotDeclare) then
+  begin
+    Pfedit.delete_current_proof ();
+    if Options.is_verbose() then
+      message ((string_of_id id) ^ " is defined")
+  end
 
-let save_anonymous opacity save_ident strength =
-  let id,(const,_) = Pfedit.cook_proof () in
+let save_named opacity =
+  let id,(const,strength) = Pfedit.cook_proof () in
+  save opacity id const strength
+
+let save_anonymous_with_strength opacity save_ident id const strength =
   if atompart_of_id id <> "Unnamed_thm" then
     message("Overriding name "^(string_of_id id)^" and using "^save_ident);
-  declare_constant 
-    (id_of_string save_ident) (ConstantEntry const,strength,opacity);
-  Pfedit.delete_current_proof ();
-  if Options.is_verbose() then message (save_ident ^ " is defined")
+  save opacity (id_of_string save_ident) const strength
 
-let save_anonymous_thm opacity id =
-  save_anonymous opacity id NeverDischarge
+let save_anonymous opacity save_ident =
+  let id,(const,strength) = Pfedit.cook_proof () in
+  save_anonymous_with_strength opacity save_ident id const strength
+
+let save_anonymous_thm opacity save_ident =
+  let id,(const,_) = Pfedit.cook_proof () in
+  save_anonymous_with_strength opacity save_ident id const NeverDischarge
 
-let save_anonymous_remark opacity id =
-  let path = try List.tl (List.tl (Lib.cwd())) with Failure _ -> [] in
-  save_anonymous opacity id (make_strength path)
+let save_anonymous_remark opacity save_ident =
+  let id,(const,_) = Pfedit.cook_proof ()
+  and path = try List.tl (List.tl (Lib.cwd())) with Failure _ -> [] in
+  save_anonymous_with_strength opacity save_ident id const (make_strength path)
 
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
diff --git a/toplevel/command.mli b/toplevel/command.mli
index abd42a87e..44bf29266 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -51,6 +51,11 @@ fails if the proof is not completed *)
 
 val save_named : bool -> unit
 
+(* [save_anonymous b name] behaves as [save_named] but declares the theorem
+under the name [name] and respects the strength of the declaration *)
+
+val save_anonymous : bool -> string -> unit
+
 (* [save_anonymous_thm b name] behaves as [save_named] but declares the
 theorem under the name [name] and gives it the strength of a theorem *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7f3485e4e..a37cfcf0b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -3,6 +3,7 @@
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
+open Declarations
 open Pp
 open Util
 open Options
@@ -498,6 +499,24 @@ let _ =
        | _ -> bad_vernac_args "DefinedNamed")
 
 let _ =
+  add "DefinedAnonymous"
+    (function 
+       | [VARG_IDENTIFIER id] -> 
+	   (fun () -> 
+	      if not(is_silent()) then show_script();
+              save_anonymous false (string_of_id id))
+       | _ -> bad_vernac_args "DefinedAnonymous")
+
+let _ =
+  add "SaveAnonymous"
+    (function 
+       | [VARG_IDENTIFIER id] -> 
+	   (fun () -> 
+	      if not(is_silent()) then show_script();
+              save_anonymous true (string_of_id id))
+       | _ -> bad_vernac_args "SaveAnonymous")
+
+let _ =
   add "SaveAnonymousThm"
     (function 
        | [VARG_IDENTIFIER id] -> 
@@ -741,6 +760,7 @@ let _ =
              | "REMARK" -> make_strength_0 ()
              | "DEFINITION" -> NeverDischarge
              | "LET" -> make_strength_2 ()
+	     | "LETTOP" -> NotDeclare
              | "LOCAL" -> make_strength_0 ()
              | _       -> anomaly "Unexpected string"
            in 
@@ -769,6 +789,7 @@ let _ =
              | "REMARK" -> (make_strength_0(),true)
              | "DEFINITION" -> (NeverDischarge,false)
              | "LET" -> (make_strength_1(),false)
+	     | "LETTOP" -> (NeverDischarge,false)
              | "LOCAL" -> (make_strength_0(),false)
              | _       -> anomaly "Unexpected string" 
 	   in
@@ -780,10 +801,19 @@ let _ =
                      if not (is_silent()) then show_open_subgoals();
                      List.iter Vernacinterp.call calls;
                      if not (is_silent()) then show_script();
-                     save_named opacity)
+                     if not (kind = "LETTOP") then
+                       save_named opacity
+                     else
+                       let csr = interp_type Evd.empty (Global.env ()) com
+                       and (_,({const_entry_body = pft;
+                                const_entry_type = _},_)) = cook_proof () in
+                       let cutt = vernac_tactic ("Cut",[Constr csr])
+                       and exat = vernac_tactic ("Exact",[Constr pft]) in
+                       delete_proof s;
+                       by (tclTHENS cutt [introduction s;exat]))
 		  ()
               with e ->
-            	if is_unsafe "proof" then begin
+            	if (is_unsafe "proof") && not (kind = "LETTOP") then begin
                   mSGNL [< 'sTR "Warning: checking of theorem "; pr_id s;
                            'sPC; 'sTR "failed";
                            'sTR "... converting to Axiom" >];