From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 5 Oct 2005 16:12:07 +0000 (+0000)
Subject: completed support for "-nodb", now also matitaclean and its library work with that... 
X-Git-Tag: V_0_7_2_3~242
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=595d77eece3202a799e786ac5996b6b1e25fac6e;p=helm.git

completed support for "-nodb", now also matitaclean and its library work with that setting
---

diff --git a/helm/matita/dump_moo.ml b/helm/matita/dump_moo.ml
index 43d11f9bc..14dea3472 100644
--- a/helm/matita/dump_moo.ml
+++ b/helm/matita/dump_moo.ml
@@ -45,11 +45,15 @@ let _ =
         MatitaLog.error (sprintf "Can't find moo '%s', skipping it." fname)
       else begin
         printf "%s:\n" fname; flush stdout;
-        let commands = MatitaMoo.load_moo ~fname in
+        let commands, metadata = MatitaMoo.load_moo ~fname in
         List.iter
           (fun cmd ->
             printf "  %s\n" (GrafiteAstPp.pp_command cmd); flush stdout)
-          commands
+          commands;
+        List.iter
+          (fun m ->
+            printf "  %s\n" (GrafiteAstPp.pp_metadata m); flush stdout)
+          metadata
       end)
     (List.rev !moos)
 
diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 1d62cadb5..9b3267fec 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -139,8 +139,11 @@ let _ =
       CicNotationParser.print_l2_pattern;
     addDebugItem "dump moo to stderr" (fun _ ->
       let status = (MatitaScript.instance ())#status in
+      let moo, metadata = status.moo_content_rev in
       List.iter (fun cmd -> prerr_endline
-        (GrafiteAstPp.pp_command cmd)) (List.rev status.moo_content_rev));
+        (GrafiteAstPp.pp_command cmd)) (List.rev moo);
+      List.iter (fun m -> prerr_endline
+        (GrafiteAstPp.pp_metadata m)) metadata);
     addDebugItem "rotate light bulbs"
       (fun _ ->
          let nb = gui#main#hintNotebook in
diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 4e48df807..61d69cbb9 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -660,13 +660,15 @@ let disambiguate_obj status obj =
   let status = MatitaSync.set_proof_aliases status diff in
   status, cic
   
-let disambiguate_command status = function
+let disambiguate_command status =
+  function
   | GrafiteAst.Alias _
   | GrafiteAst.Default _
   | GrafiteAst.Drop _
   | GrafiteAst.Dump _
   | GrafiteAst.Include _
   | GrafiteAst.Interpretation _
+  | GrafiteAst.Metadata _
   | GrafiteAst.Notation _
   | GrafiteAst.Qed _
   | GrafiteAst.Render _
@@ -714,26 +716,29 @@ let eval_command opts status cmd =
        raise (IncludedFileNotCompiled moopath);
      !eval_from_moo_ref status moopath (fun _ _ -> ());
      !status
+  | GrafiteAst.Metadata (loc, m) ->
+      (match m with
+      | GrafiteAst.Dependency uri -> MatitaTypes.add_moo_metadata [m] status
+      | GrafiteAst.Baseuri _ -> status)
   | GrafiteAst.Set (loc, name, value) -> 
-      let value = 
-        if name = "baseuri" then
-          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
+      let status = 
+        if name = "baseuri" then begin
+          let 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
+          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]
+          end;
+          add_moo_metadata [GrafiteAst.Baseuri value] status
+        end else
+          status
       in
-      if not (MatitaMisc.is_empty value) then
-        begin
-          MatitaLog.warn ("baseuri " ^ value ^ " is not empty");
-          if opts.clean_baseuri then
-            begin 
-              MatitaLog.message ("cleaning baseuri " ^ value);
-              MatitacleanLib.clean_baseuris [value]
-            end
-        end;
       set_option status name value
   | GrafiteAst.Drop loc -> raise Drop
   | GrafiteAst.Qed loc ->
@@ -772,13 +777,20 @@ let eval_command opts status cmd =
       MatitaSync.set_proof_aliases status diff
   | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *)
   | GrafiteAst.Dump _ -> assert false   (* ZACK: to be removed *)
-  | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
-      let status' = add_moo_content [stm] status in
+  | GrafiteAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm ->
+      let status = add_moo_content [stm] status in
+      let uris =
+        List.map
+          (fun uri -> GrafiteAst.Dependency (UriManager.buri_of_uri uri))
+          (CicNotationUtil.find_appl_pattern_uris cic_appl_pattern)
+      in
       let diff =
        [DisambiguateTypes.Symbol (symbol, 0),
          DisambiguateChoices.lookup_symbol_by_dsc symbol dsc]
       in
-      MatitaSync.set_proof_aliases status' diff
+      let status = MatitaSync.set_proof_aliases status diff in
+      let status = MatitaTypes.add_moo_metadata uris status in
+      status
   | GrafiteAst.Notation _ as stm -> add_moo_content [stm] status
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
@@ -871,7 +883,6 @@ let eval_executable opts status ex =
 
 let eval_comment status c = status
             
-
 let eval_ast 
   ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st 
 =
@@ -884,21 +895,30 @@ let eval_ast
   | GrafiteAst.Executable (_,ex) -> eval_executable opts status ex
   | GrafiteAst.Comment (_,c) -> eval_comment status c
 
-let eval_from_moo ?do_heavy_checks ?include_paths ?clean_baseuri status fname
-  cb
+let eval_from_moo ?do_heavy_checks ?include_paths ?clean_baseuri status fname cb
 =
-  let moo = MatitaMoo.load_moo fname in
+  let ast_of_cmd cmd =
+    GrafiteAst.Executable (DisambiguateTypes.dummy_floc,
+      GrafiteAst.Command (DisambiguateTypes.dummy_floc,
+        (GrafiteAst.reash_cmd_uris cmd)))
+  in
+  let moo, metadata = MatitaMoo.load_moo fname in
   List.iter 
     (fun ast -> 
+      let ast = ast_of_cmd ast in
+      cb !status ast;
+      status :=
+        eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast)
+    moo;
+  List.iter
+    (fun m ->
       let ast =
-        GrafiteAst.Executable (DisambiguateTypes.dummy_floc,
-          GrafiteAst.Command (DisambiguateTypes.dummy_floc,
-            (GrafiteAst.reash_cmd_uris ast)))
+        ast_of_cmd (GrafiteAst.Metadata (DisambiguateTypes.dummy_floc, m))
       in
       cb !status ast;
       status :=
         eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast)
-    moo
+    metadata
 
 let eval_from_stream 
   ?do_heavy_checks ?include_paths ?clean_baseuri status str cb 
@@ -952,7 +972,7 @@ let initial_status =
   lazy {
     aliases = DisambiguateTypes.Environment.empty;
     multi_aliases = DisambiguateTypes.Environment.empty;
-    moo_content_rev = [];
+    moo_content_rev = [], [];
     proof_status = No_proof;
     options = default_options ();
     objects = [];
diff --git a/helm/matita/matitaMoo.ml b/helm/matita/matitaMoo.ml
index ea5c748bd..bdea339b7 100644
--- a/helm/matita/matitaMoo.ml
+++ b/helm/matita/matitaMoo.ml
@@ -34,16 +34,19 @@ let marshal_flags = []
  *   structure. Different magic numbers stand for incompatible data structures
  * - an integer -- checksum -- denoting the hash value (computed with
  *   Hashtbl.hash) of the string representation of the dumped data structur
- * - marshalled list of GrafiteAst.command
+ * - marshalled pair: first component is a list of GrafiteAst.command (real moo
+ *   content), second component is a list of GrafiteAst.metadata
  *)
 
-let save_moo ~fname moo =
+let save_moo ~fname (moo, metadata) =
  let oc = open_out fname in
- let marshalled_moo = Marshal.to_string (List.rev moo) marshal_flags in
- let checksum = Hashtbl.hash marshalled_moo in
+ let marshalled = 
+   Marshal.to_string (List.rev moo, List.rev metadata) marshal_flags 
+ in
+ let checksum = Hashtbl.hash marshalled in
  output_binary_int oc GrafiteAst.magic;
  output_binary_int oc checksum;
- output_string oc marshalled_moo;
+ output_string oc marshalled;
  close_out oc
 
 let load_moo ~fname =
@@ -55,11 +58,11 @@ let load_moo ~fname =
         let moo_magic = input_binary_int ic in
         if moo_magic <> GrafiteAst.magic then raise (Version_mismatch fname);
         let moo_checksum = input_binary_int ic in
-        let marshalled_moo = HExtlib.input_all ic in
-        let checksum = Hashtbl.hash marshalled_moo in
+        let marshalled = HExtlib.input_all ic in
+        let checksum = Hashtbl.hash marshalled in
         if checksum <> moo_checksum then raise (Checksum_failure fname);
-        let (moo: MatitaTypes.ast_command list) =
-          Marshal.from_string marshalled_moo 0
+        let (moo: MatitaTypes.moo) =
+          Marshal.from_string marshalled 0
         in
         moo
       with End_of_file -> raise (Corrupt_moo fname))
diff --git a/helm/matita/matitaMoo.mli b/helm/matita/matitaMoo.mli
index 3959a120a..75b71a58f 100644
--- a/helm/matita/matitaMoo.mli
+++ b/helm/matita/matitaMoo.mli
@@ -28,8 +28,8 @@ exception Checksum_failure of string
 exception Corrupt_moo of string
 exception Version_mismatch of string
 
-val save_moo: fname:string -> MatitaTypes.ast_command list -> unit
+val save_moo: fname:string -> MatitaTypes.moo -> unit
 
   (** @raise Corrupt_moo *)
-val load_moo: fname:string -> MatitaTypes.ast_command list
+val load_moo: fname:string -> MatitaTypes.moo
 
diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 754197bb7..cbf305261 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -47,6 +47,18 @@ let alias_diff =
  fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status
 
 let set_proof_aliases status new_aliases =
+ let commands_of_aliases =
+   List.map
+    (fun alias -> GrafiteAst.Alias (DisambiguateTypes.dummy_floc, alias))
+ in
+ let deps_of_aliases =
+   HExtlib.filter_map
+    (function
+    | GrafiteAst.Ident_alias (_, suri) ->
+        let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in
+        Some (GrafiteAst.Dependency buri)
+    | _ -> None)
+ in
  let aliases =
   List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
    status.aliases new_aliases in
@@ -59,9 +71,12 @@ let set_proof_aliases status new_aliases =
  if new_aliases = [] then
    new_status
  else
-   add_moo_content
-    (DisambiguatePp.commands_of_domain_and_codomain_items_list new_aliases)
-    new_status
+   let aliases = 
+     DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases
+   in
+   let status = add_moo_content (commands_of_aliases aliases) new_status in
+   let status = add_moo_metadata (deps_of_aliases aliases) status in
+   status
 
 (** given a uri and a type list (the contructors types) builds a list of pairs
  *  (name,uri) that is used to generate automatic aliases **)
diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 5df68ea86..8b4cb1f9d 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -58,11 +58,12 @@ type options = option_value StringMap.t
 let no_options = StringMap.empty
 
 type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+type moo = ast_command list * GrafiteAst.metadata list
 
 type status = {
   aliases: DisambiguateTypes.environment;
   multi_aliases: DisambiguateTypes.multiple_environment;
-  moo_content_rev: ast_command list;
+  moo_content_rev: moo;
   proof_status: proof_status;
   options: options;
   objects: (UriManager.uri * string) list;
@@ -80,26 +81,6 @@ let set_metasenv metasenv status =
   in
   { status with proof_status = proof_status }
 
-let add_moo_content cmds status =
-  let content = status.moo_content_rev in
-  let content' =
-    List.fold_right
-      (fun cmd acc ->
-(*         prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
-        match cmd with
-        | GrafiteAst.Interpretation _
-        | GrafiteAst.Default _ ->
-            if List.mem cmd content then acc
-            else cmd :: acc
-        | GrafiteAst.Alias _ -> (* move Alias as the last inserted one *)
-            cmd :: (List.filter ((<>) cmd) acc)
-        | _ -> cmd :: acc)
-      cmds content
-  in
-(*   prerr_endline ("new moo content: " ^ String.concat " " (List.map
-    GrafiteAstPp.pp_command content')); *)
-  { status with moo_content_rev = content' }
-
 let dump_status status = 
   MatitaLog.message "status.aliases:\n";
   MatitaLog.message
@@ -125,7 +106,6 @@ let dump_status status =
     (fun (u,_) -> 
       MatitaLog.message (UriManager.string_of_uri u)) status.objects 
   
-
 let get_option status name =
   try
     StringMap.find name status.options
@@ -166,6 +146,47 @@ let set_option status name value =
   else
     { status with options = StringMap.add name value status.options }
 
+let add_moo_content cmds status =
+  let content, metadata = status.moo_content_rev in
+  let content' =
+    List.fold_right
+      (fun cmd acc ->
+(*         prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
+        match cmd with
+        | GrafiteAst.Interpretation _
+        | GrafiteAst.Default _ ->
+            if List.mem cmd content then acc
+            else cmd :: acc
+        | GrafiteAst.Alias _ -> (* move Alias as the last inserted one *)
+            cmd :: (List.filter ((<>) cmd) acc)
+        | _ -> cmd :: acc)
+      cmds content
+  in
+(*   prerr_endline ("new moo content: " ^ String.concat " " (List.map
+    GrafiteAstPp.pp_command content')); *)
+  { status with moo_content_rev = content', metadata }
+
+let add_moo_metadata new_metadata status =
+  let content, metadata = status.moo_content_rev in
+  let metadata' =
+    List.fold_left
+      (fun acc m ->
+        match m with
+        | GrafiteAst.Dependency buri ->
+            let is_self = (* self dependency *)
+              try
+                get_string_option status "baseuri" = buri
+              with Option_error _ -> false  (* baseuri not yet set *)
+            in
+            if is_self
+              || List.exists (GrafiteAst.eq_metadata m) metadata (* duplicate *)
+            then acc
+            else m :: acc
+        | _ -> m :: acc)
+      metadata new_metadata
+  in
+  { status with moo_content_rev = content, metadata' }
+
   (* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
 class type console =
   object
diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 51744f152..144c0c1f2 100644
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -48,21 +48,23 @@ type options = option_value StringMap.t
 val no_options : 'a StringMap.t
 
 type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+type moo = ast_command list * GrafiteAst.metadata list  (** <moo, metadata> *)
 
 type status = {
-  aliases: DisambiguateTypes.environment;   (** disambiguation aliases *)
+  aliases: DisambiguateTypes.environment;         (** disambiguation aliases *)
   multi_aliases: DisambiguateTypes.multiple_environment;
-  moo_content_rev: ast_command list;
-  proof_status: proof_status;
+  moo_content_rev: moo;
+  proof_status: proof_status;                             (** logical status *)
   options: options;
   objects: (UriManager.uri * string) list;  (** in-scope objects, with paths *)
-  notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
+  notation_ids: CicNotation.notation_id list;      (** in-scope notation ids *)
 }
 
 val set_metasenv: Cic.metasenv -> status -> status
 
   (** list is not reversed, head command will be the first emitted *)
 val add_moo_content: ast_command list -> status -> status
+val add_moo_metadata: GrafiteAst.metadata list -> status -> status
 
 val dump_status : status -> unit
 val get_option : status -> StringMap.key -> option_value
diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 0db34ea88..a10594ab2 100644
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -134,9 +134,9 @@ let main ~mode =
   Sys.catch_break true;
   let origcb = MatitaLog.get_log_callback () in
   let newcb tag s =
-        match tag with
-        | `Debug | `Message -> ()
-        | `Warning | `Error -> origcb tag s
+    match tag with
+    | `Debug | `Message -> ()
+    | `Warning | `Error -> origcb tag s
   in
   if Helm_registry.get_bool "matita.quiet" then
     MatitaLog.set_log_callback newcb;
diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml
index e15f736dc..9a5d1bf01 100644
--- a/helm/matita/matitaclean.ml
+++ b/helm/matita/matitaclean.ml
@@ -30,7 +30,7 @@ module TA = GrafiteAst
 
 let _ = MatitaInit.initialize_all ()
 
-let main uri_to_remove = MatitacleanLib.clean_baseuris uri_to_remove
+let main = MatitacleanLib.clean_baseuris
 
 let _ =
   let uris_to_remove = ref [] in
diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml
index 2d1cbfdef..e8a1fd29a 100644
--- a/helm/matita/matitacleanLib.ml
+++ b/helm/matita/matitacleanLib.ml
@@ -52,7 +52,8 @@ let one_step_depend suri =
         let buri = HMysql.escape buri in
         let obj_tbl = MetadataTypes.obj_tbl () in
         sprintf 
-          "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'"
+        ("SELECT source, h_occurrence FROM %s WHERE " ^^ 
+         "h_occurrence REGEXP '^%s[^/]*$'")
             obj_tbl buri
       in
       try 
@@ -123,29 +124,96 @@ let close_uri_list uri_to_remove =
   in
   uri_to_remove, depend
 
-let rec close uris next =
+let rec close_using_db uris next =
   match next with
   | [] -> uris
-  | l -> let uris, next = close_uri_list l in close uris next @ uris
+  | l -> let uris, next = close_uri_list l in close_using_db uris next @ uris
   
 let cleaned_no = ref 0;;
 
+  (** TODO repellent code ... *)
+let moo_root_dir = lazy (
+  let url =
+    List.assoc "cic:/matita/"
+      (List.map
+        (fun pair ->
+          match
+            Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair)
+          with
+          | [a;b] -> a, b
+          | _ -> assert false)
+        (Helm_registry.get_list Helm_registry.string "getter.prefix"))
+  in
+  String.sub url 7 (String.length url - 7)  (* remove heading "file:///" *)
+)
+
+let close_using_moos buris =
+  let rev_deps = Hashtbl.create 97 in
+  let all_moos =
+    HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo")
+      (Lazy.force moo_root_dir)
+  in
+  List.iter
+    (fun path -> 
+      let _, metadata = MatitaMoo.load_moo ~fname:path in
+      let baseuri_of_current_moo = 
+        let rec aux = function 
+          | [] -> assert false
+          | GrafiteAst.Baseuri buri::_ -> buri
+          | _ :: tl -> aux tl
+        in
+        aux metadata
+      in
+      let deps = 
+        HExtlib.filter_map 
+          (function 
+          | GrafiteAst.Dependency buri -> Some buri
+          | _ -> None ) 
+        metadata
+      in
+      List.iter 
+        (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_moo) deps)
+  all_moos;
+  let buris_to_remove = 
+    HExtlib.list_uniq  
+      (List.fast_sort Pervasives.compare 
+        (List.flatten (List.map (Hashtbl.find_all rev_deps) buris)))
+  in
+  let objects_to_remove = 
+    let objs_of_buri buri =
+      HExtlib.filter_map 
+        (function 
+        | Http_getter_types.Ls_object o ->
+            Some (buri ^ "/" ^ o.Http_getter_types.uri)
+        | _ -> None) 
+      (Http_getter.ls buri)
+    in
+    List.flatten (List.map objs_of_buri (buris @ buris_to_remove))
+  in
+  objects_to_remove
+
 let clean_baseuris ?(verbose=true) buris =
   Hashtbl.clear cache_of_processed_baseuri;
   let buris = List.map HGM.strip_trailing_slash buris in
   debug_prerr "clean_baseuris called on:";
   if debug then
     List.iter debug_prerr buris; 
-  let l = close [] buris in
+  let l = 
+    if Helm_registry.get_bool "db.nodb" then
+      close_using_moos buris
+    else
+      close_using_db [] buris 
+  in
   let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
   let l = List.map UriManager.uri_of_string l in
   debug_prerr "clean_baseuri will remove:";
   if debug then
     List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; 
-  Hashtbl.iter
-   (fun buri _ ->
+  List.iter
+   (fun buri ->
      MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri)) 
-   cache_of_processed_baseuri;
+   (HExtlib.list_uniq (List.fast_sort Pervasives.compare
+     (List.map (UriManager.buri_of_uri) l)));
   List.iter (MatitaSync.remove ~verbose) l;
   cleaned_no := !cleaned_no + List.length l;
   if !cleaned_no > 30 then
diff --git a/helm/matita/matitacleanLib.mli b/helm/matita/matitacleanLib.mli
index f4ce6de57..2d8095fb2 100644
--- a/helm/matita/matitacleanLib.mli
+++ b/helm/matita/matitacleanLib.mli
@@ -24,3 +24,4 @@
  *)
 
 val clean_baseuris : ?verbose:bool -> string list -> unit
+