From 595d77eece3202a799e786ac5996b6b1e25fac6e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 5 Oct 2005 16:12:07 +0000 Subject: [PATCH] completed support for "-nodb", now also matitaclean and its library work with that setting --- helm/matita/dump_moo.ml | 8 +++- helm/matita/matita.ml | 5 ++- helm/matita/matitaEngine.ml | 82 +++++++++++++++++++++------------- helm/matita/matitaMoo.ml | 21 +++++---- helm/matita/matitaMoo.mli | 4 +- helm/matita/matitaSync.ml | 21 +++++++-- helm/matita/matitaTypes.ml | 65 ++++++++++++++++++--------- helm/matita/matitaTypes.mli | 10 +++-- helm/matita/matitacLib.ml | 6 +-- helm/matita/matitaclean.ml | 2 +- helm/matita/matitacleanLib.ml | 82 +++++++++++++++++++++++++++++++--- helm/matita/matitacleanLib.mli | 1 + 12 files changed, 222 insertions(+), 85 deletions(-) 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 (** *) 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 + -- 2.39.2