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)
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
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 _
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 ->
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 =
let eval_comment status c = status
-
let eval_ast
?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st
=
| 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
lazy {
aliases = DisambiguateTypes.Environment.empty;
multi_aliases = DisambiguateTypes.Environment.empty;
- moo_content_rev = [];
+ moo_content_rev = [], [];
proof_status = No_proof;
options = default_options ();
objects = [];
* 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 =
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))
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
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
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 **)
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;
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
(fun (u,_) ->
MatitaLog.message (UriManager.string_of_uri u)) status.objects
-
let get_option status name =
try
StringMap.find name status.options
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
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
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;
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
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
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
*)
val clean_baseuris : ?verbose:bool -> string list -> unit
+
projects / helm.git / commitdiff