X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=94efb904f4a9da6685225c612673edb9c4a0f30f;hb=86f3b0d7706062defe2b0b361cb8344e025826c0;hp=b20755d870bb4a87def160f7f57d05e9ee7c12e4;hpb=fddf15f1e9d253316bdcb854c2ff7ec64144bde8;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index b20755d87..94efb904f 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -7,6 +7,8 @@ exception Drop;;
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
 
+type options = { do_heavy_checks: bool ; include_paths: string list }
+
 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   * names as long as they are available, then it fallbacks to name generation
   * using FreshNamesGenerator module *)
@@ -410,7 +412,7 @@ let disambiguate_obj status obj =
     | TacticAst.Record (_,name,_,_) ->
        Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
     | TacticAst.Inductive _ -> assert false
-    | _ -> None in
+    | TacticAst.Theorem _ -> None in
   let (aliases, metasenv, cic, _) =
     match
       MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
@@ -443,7 +445,23 @@ let disambiguate_command status = function
       let status,obj = disambiguate_obj status obj in
        status, TacticAst.Obj (loc,obj)
 
-let eval_command status cmd =
+let try_open_in paths path =
+  let rec aux = function
+  | [] -> open_in path
+  | p :: tl ->
+      try
+        open_in (p ^ "/" ^ path)
+      with Sys_error _ -> aux tl
+  in
+  try
+    aux paths
+  with Sys_error _ as exc ->
+    MatitaLog.error ("Unable to read " ^ path);
+    MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths);
+    raise exc
+;;
+       
+let eval_command opts status cmd =
  let status,cmd = disambiguate_command status cmd in
   match cmd with
   | TacticAst.Default (loc, what, uris) as cmd ->
@@ -452,14 +470,18 @@ let eval_command status cmd =
         (TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
   | TacticAst.Include (loc, path) ->
      let path = MatitaMisc.obj_file_of_script path in
-     let stream = Stream.of_channel (open_in path) in
+     let stream = Stream.of_channel (try_open_in opts.include_paths path) in
      let status = ref status in
       !eval_from_stream_ref status stream (fun _ _ -> ());
       !status
   | TacticAst.Set (loc, name, value) -> 
       let value = 
         if name = "baseuri" then
-          MatitaMisc.strip_trailing_slash value
+          let v = MatitaMisc.strip_trailing_slash value in
+          try
+            ignore (String.index v ' ');
+            command_error "baseuri can't contain spaces"
+          with Not_found -> v
         else
           value
       in
@@ -517,70 +539,104 @@ 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 opts.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 opts status ex =
   match ex with
   | TacticAst.Tactical (_, tac) -> eval_tactical status tac
-  | TacticAst.Command (_, cmd) -> eval_command status cmd
+  | TacticAst.Command (_, cmd) -> eval_command opts 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) ?(include_paths=[]) status st =
+  let opts = 
+    {do_heavy_checks = do_heavy_checks ; include_paths = include_paths}
+  in
   match st with
-  | TacticAst.Executable (_,ex) -> eval_executable status ex
+  | TacticAst.Executable (_,ex) -> eval_executable opts status ex
   | TacticAst.Comment (_,c) -> eval_comment status c
 
-let eval_from_stream status str cb =
+let eval_from_stream ?do_heavy_checks ?include_paths 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 ?include_paths !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 ?include_paths 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 ?include_paths !status ast 
   done
 ;;
 
-let eval_string status str =
-  eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
+let eval_string ?do_heavy_checks ?include_paths status str =
+  eval_from_stream 
+    ?do_heavy_checks ?include_paths status (Stream.of_string str) (fun _ _ ->())
 
 let default_options () =
 (*
@@ -593,7 +649,7 @@ let default_options () =
 *)
   let options =
     StringMap.add "basedir"
-      (String (Helm_registry.get "matita.basedir" ))
+      (String (Helm_registry.get "matita.basedir"))
       no_options
   in
   options