added a flag to do the check of alredy-proved-theorem

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index c5b2fb98774702ee955193f6872a191240cea8a8..53772ccf29a9d604a7b02afb8baa7d468e329472 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -443,7 +443,7 @@ let disambiguate_command status = function
       let status,obj = disambiguate_obj status obj in
        status, TacticAst.Obj (loc,obj)
 
-let eval_command status cmd =
+let eval_command do_heavy_checks status cmd =
  let status,cmd = disambiguate_command status cmd in
   match cmd with
   | TacticAst.Default (loc, what, uris) as cmd ->
@@ -521,73 +521,99 @@ let eval_command status cmd =
      in
      let metasenv = MatitaMisc.get_proof_metasenv status in
      match obj with
-        Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
+     | Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
          let name = UriManager.name_of_uri uri in
          if not(CicPp.check name ty) then
            MatitaLog.warn ("Bad name: " ^ name);
+         if do_heavy_checks then
+           begin
+             let dbd = MatitaDb.instance () in
+             let similar = MetadataQuery.match_term ~dbd ty in
+             let convertible =
+               List.filter (
+                 fun u ->
+                   let t = CicUtil.term_of_uri u in
+                   let ty',g = 
+                     CicTypeChecker.type_of_aux' 
+                       metasenv' [] t CicUniv.empty_ugraph
+                   in
+                   fst(CicReduction.are_convertible [] ty' ty g)) 
+               similar 
+             in
+             (match convertible with
+             | [] -> ()
+             | x::_ -> 
+                 MatitaLog.warn  
+                 ("Theorem already proved: " ^ UriManager.string_of_uri x ^ 
+                  "\nPlease use a variant."));
+           end;
          assert (metasenv = metasenv');
          let goalno =
-          match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false in
+           match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false 
+         in
          let initial_proof = (Some uri, metasenv, bo, ty) in
-          { status with proof_status = Incomplete_proof (initial_proof,goalno)}
-      | _ ->
-        if metasenv <> [] then
-         command_error (
-           "metasenv not empty while giving a definition with body: " ^
-           CicMetaSubst.ppmetasenv metasenv []);
-        let status = MatitaSync.add_obj uri obj status in
-         match obj with
-            Cic.Constant _ -> status
-          | Cic.InductiveDefinition (_,_,_,attrs) ->
-             let status = generate_elimination_principles uri status in
-             let rec get_record_attrs =
-              function
-                 [] -> None
-               | (`Class (`Record fields))::_ -> Some fields
-               | _::tl -> get_record_attrs tl
-             in
-              (match get_record_attrs attrs with
-                  None -> status (* not a record *)
-                | Some fields -> generate_projections uri fields status)
-          | Cic.CurrentProof _
-          | Cic.Variable _ -> assert false
+         { status with proof_status = Incomplete_proof (initial_proof,goalno)}
+     | _ ->
+         if metasenv <> [] then
+          command_error (
+            "metasenv not empty while giving a definition with body: " ^
+            CicMetaSubst.ppmetasenv metasenv []);
+         let status = MatitaSync.add_obj uri obj status in
+          match obj with
+             Cic.Constant _ -> status
+           | Cic.InductiveDefinition (_,_,_,attrs) ->
+              let status = generate_elimination_principles uri status in
+              let rec get_record_attrs =
+               function
+                  [] -> None
+                | (`Class (`Record fields))::_ -> Some fields
+                | _::tl -> get_record_attrs tl
+              in
+               (match get_record_attrs attrs with
+                   None -> status (* not a record *)
+                 | Some fields -> generate_projections uri fields status)
+           | Cic.CurrentProof _
+           | Cic.Variable _ -> assert false
 
-let eval_executable status ex =
+let eval_executable do_heavy_checks status ex =
   match ex with
   | TacticAst.Tactical (_, tac) -> eval_tactical status tac
-  | TacticAst.Command (_, cmd) -> eval_command status cmd
+  | TacticAst.Command (_, cmd) -> eval_command do_heavy_checks status cmd
   | TacticAst.Macro (_, mac) -> 
       command_error (sprintf "The macro %s can't be in a script" 
         (TacticAstPp.pp_macro_ast mac))
 
 let eval_comment status c = status
             
-let eval_ast status st =
+let eval_ast ?(do_heavy_checks=false) status st =
   match st with
-  | TacticAst.Executable (_,ex) -> eval_executable status ex
+  | TacticAst.Executable (_,ex) -> eval_executable do_heavy_checks status ex
   | TacticAst.Comment (_,c) -> eval_comment status c
 
-let eval_from_stream status str cb =
+let eval_from_stream ?do_heavy_checks status str cb =
   let stl = CicTextualParser2.parse_statements str in
   List.iter
-   (fun ast -> cb !status ast;status := eval_ast !status ast) stl
+   (fun ast -> 
+     cb !status ast;status := eval_ast ?do_heavy_checks !status ast) 
+   stl
 ;;
 
 (* to avoid a long list of recursive functions *)
 eval_from_stream_ref := eval_from_stream;;
   
-let eval_from_stream_greedy status str cb =
+let eval_from_stream_greedy ?do_heavy_checks status str cb =
   while true do
     print_string "matita> ";
     flush stdout;
     let ast = CicTextualParser2.parse_statement str in
     cb !status ast;
-    status := eval_ast !status ast 
+    status := eval_ast ?do_heavy_checks !status ast 
   done
 ;;
 
-let eval_string status str =
-  eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
+let eval_string ?do_heavy_checks status str =
+  eval_from_stream 
+    ?do_heavy_checks status (Stream.of_string str) (fun _ _ -> ())
 
 let default_options () =
 (*