* Part of matita that used to deal with the library moved into ocaml/library

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 84291dcc6582866cdfa31c06d5683cbb4130788d..0fc5f6ab81552d67b66463e753033082e2962373 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -62,7 +62,7 @@ let tactic_of_ast ast =
   | GrafiteAst.Assumption _ -> Tactics.assumption
   | GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
       AutoTactic.auto_tac ?depth ?width ?paramodulation ?full
-        ~dbd:(MatitaDb.instance ()) ()
+        ~dbd:(LibraryDb.instance ()) ()
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
@@ -80,7 +80,7 @@ let tactic_of_ast ast =
         | GrafiteAst.Ident _            -> assert false
       in
       let user_types = List.rev_map to_type types in
-      let dbd = MatitaDb.instance () in
+      let dbd = LibraryDb.instance () in
       let mk_fresh_name_callback = namer_of names in
       Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
   | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
@@ -114,7 +114,7 @@ let tactic_of_ast ast =
   | GrafiteAst.Fourier _ -> Tactics.fourier
   | GrafiteAst.FwdSimpl (_, hyp, names) -> 
      Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names)
-      ~dbd:(MatitaDb.instance ()) hyp
+      ~dbd:(LibraryDb.instance ()) hyp
   | GrafiteAst.Generalize (_,pattern,ident) ->
      let names = match ident with None -> [] | Some id -> [id] in
      Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern 
@@ -165,7 +165,7 @@ let disambiguate_term ?context status_ref goal term =
   in
   let (diff, metasenv, cic, _) =
     singleton
-      (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
+      (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
         ~aliases:status.aliases ~universe:(Some status.multi_aliases)
         ~context ~metasenv:(MatitaTypes.get_proof_metasenv status) term)
   in
@@ -184,7 +184,7 @@ let disambiguate_lazy_term status_ref term =
     let status = !status_ref in
     let (diff, metasenv, cic, ugraph) =
       singleton
-        (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
+        (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
           ~initial_ugraph:ugraph ~aliases:status.aliases
           ~universe:(Some status.multi_aliases) ~context ~metasenv term)
     in
@@ -660,12 +660,12 @@ let generate_projections uri fields status =
        MatitaSync.add_obj uri obj status
      with
         CicTypeChecker.TypeCheckerFailure s ->
-         MatitaLog.message 
+         HLog.message 
           ("Unable to create projection " ^ name ^ " cause: " ^ (Lazy.force s));
          status
       | CicEnvironment.Object_not_found uri ->
          let depend = UriManager.name_of_uri uri in
-          MatitaLog.message 
+          HLog.message 
            ("Unable to create projection " ^ name ^ " because it requires " ^ depend);
          status
   ) status projections
@@ -683,7 +683,7 @@ let disambiguate_obj status obj =
     | CicNotationPt.Theorem _ -> None in
   let (diff, metasenv, cic, _) =
     singleton
-      (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
+      (MatitaDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
         ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj)
   in
   let proof_status =
@@ -739,15 +739,15 @@ let eval_command opts status cmd =
   let status,cmd = disambiguate_command status cmd in
   let cmd,notation_ids' = CicNotation.process_notation cmd in
   let status =
-    { status with notation_ids = notation_ids' @ status.notation_ids }
-  in
+    { status with notation_ids = notation_ids' @ status.notation_ids } in
+  let basedir = Helm_registry.get "matita.basedir" in
   match cmd with
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
      add_moo_content [cmd] status
   | GrafiteAst.Include (loc, path) ->
      let absolute_path = make_absolute opts.include_paths path in
-     let moopath = MatitacleanLib.obj_file_of_script absolute_path in
+     let moopath = MatitaMisc.obj_file_of_script ~basedir absolute_path in
      let status = ref status in
      if not (Sys.file_exists moopath) then
        raise (IncludedFileNotCompiled moopath);
@@ -768,9 +768,9 @@ let eval_command opts status cmd =
             with Not_found -> v
           in
           if not (MatitaMisc.is_empty value) && opts.clean_baseuri then begin
-            MatitaLog.warn ("baseuri " ^ value ^ " is not empty");
-            MatitaLog.message ("cleaning baseuri " ^ value);
-            MatitacleanLib.clean_baseuris [value]
+            HLog.warn ("baseuri " ^ value ^ " is not empty");
+            HLog.message ("cleaning baseuri " ^ value);
+            LibraryClean.clean_baseuris ~basedir [value]
           end;
           add_moo_metadata [GrafiteAst.Baseuri value] status
         end else
@@ -845,14 +845,14 @@ let eval_command opts status cmd =
      | Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
          let name = UriManager.name_of_uri uri in
          if not(CicPp.check name ty) then
-           MatitaLog.error ("Bad name: " ^ name);
+           HLog.error ("Bad name: " ^ name);
          if opts.do_heavy_checks then
            begin
-             let dbd = MatitaDb.instance () in
+             let dbd = LibraryDb.instance () in
              let similar = Whelp.match_term ~dbd ty in
              let similar_len = List.length similar in
              if similar_len> 30 then
-               (MatitaLog.message
+               (HLog.message
                  ("Duplicate check will compare your theorem with " ^ 
                    string_of_int similar_len ^ 
                    " theorems, this may take a while."));
@@ -870,7 +870,7 @@ let eval_command opts status cmd =
              (match convertible with
              | [] -> ()
              | x::_ -> 
-                 MatitaLog.warn  
+                 HLog.warn  
                  ("Theorem already proved: " ^ UriManager.string_of_uri x ^ 
                   "\nPlease use a variant."));
            end;
@@ -943,7 +943,7 @@ let eval_from_moo ?do_heavy_checks ?include_paths ?clean_baseuri status fname cb
       GrafiteAst.Command (DisambiguateTypes.dummy_floc,
         (GrafiteAst.reash_cmd_uris cmd)))
   in
-  let moo, metadata = MatitaMoo.load_moo fname in
+  let moo, metadata = GrafiteMarshal.load_moo fname in
   List.iter 
     (fun ast -> 
       let ast = ast_of_cmd ast in
@@ -993,21 +993,7 @@ let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str =
     ?do_heavy_checks ?include_paths ?clean_baseuri status
       (Ulexing.from_utf8_string str) (fun _ _ -> ())
 
-let default_options () =
-(*
-  let options =
-    StringMap.add "baseuri"
-      (String
-        (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
-      no_options
-  in
-*)
-  let options =
-    StringMap.add "basedir"
-      (String (Helm_registry.get "matita.basedir"))
-      no_options
-  in
-  options
+let default_options () = no_options
 
 let initial_status =
   lazy {