From 0ac236dda6f80f6dc86a7f12d8c88b25e64e3251 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 29 Nov 2005 14:53:34 +0000 Subject: [PATCH] * Part of matita that used to deal with the library moved into ocaml/library * cic_unification/coercDb.ml* ==> library/coercDb.ml* --- helm/matita/.depend | 117 +++++------- helm/matita/Makefile.in | 15 +- helm/matita/dump_moo.ml | 4 +- helm/matita/matita.ml | 8 +- helm/matita/matita.txt | 7 + helm/matita/matitaEngine.ml | 54 ++---- helm/matita/matitaExcPp.ml | 6 +- helm/matita/matitaGui.ml | 23 +-- helm/matita/matitaGuiTypes.mli | 2 +- helm/matita/matitaInit.ml | 2 +- helm/matita/matitaMathView.ml | 6 +- helm/matita/matitaMisc.ml | 70 +++---- helm/matita/matitaMisc.mli | 12 +- helm/matita/matitaScript.ml | 30 +-- helm/matita/matitaSync.ml | 178 +++--------------- helm/matita/matitaSync.mli | 7 - helm/matita/matitaTypes.ml | 22 +-- helm/matita/matitaTypes.mli | 7 +- helm/matita/matitacLib.ml | 48 ++--- helm/matita/matitaclean.ml | 17 +- helm/matita/matitadep.ml | 14 +- helm/matita/matitamakeLib.ml | 18 +- .../ocaml/METAS/meta.helm-cic_unification.src | 2 +- helm/ocaml/METAS/meta.helm-library.src | 5 + helm/ocaml/Makefile.in | 3 +- helm/ocaml/cic_unification/.depend | 7 +- helm/ocaml/cic_unification/Makefile | 1 - helm/ocaml/extlib/.depend | 2 + helm/ocaml/extlib/Makefile | 1 + helm/ocaml/extlib/hExtlib.ml | 21 +++ helm/ocaml/extlib/hExtlib.mli | 5 + .../matitaLog.ml => ocaml/extlib/hLog.ml} | 0 .../matitaLog.mli => ocaml/extlib/hLog.mli} | 0 helm/ocaml/grafite/.depend | 3 + helm/ocaml/grafite/Makefile | 1 + .../grafite/grafiteMarshal.ml} | 5 +- .../grafite/grafiteMarshal.mli} | 7 +- helm/ocaml/library/.cvsignore | 7 + helm/ocaml/library/Makefile | 14 ++ .../{cic_unification => library}/coercDb.ml | 0 .../{cic_unification => library}/coercDb.mli | 0 .../library/libraryClean.ml} | 63 ++----- helm/ocaml/library/libraryClean.mli | 26 +++ .../library/libraryDb.ml} | 2 +- .../library/libraryDb.mli} | 0 .../library/libraryMisc.ml} | 7 +- helm/ocaml/library/libraryMisc.mli | 27 +++ helm/ocaml/library/librarySync.ml | 142 ++++++++++++++ helm/ocaml/library/librarySync.mli | 31 +++ 49 files changed, 568 insertions(+), 481 deletions(-) create mode 100644 helm/ocaml/METAS/meta.helm-library.src rename helm/{matita/matitaLog.ml => ocaml/extlib/hLog.ml} (100%) rename helm/{matita/matitaLog.mli => ocaml/extlib/hLog.mli} (100%) rename helm/{matita/matitaMoo.ml => ocaml/grafite/grafiteMarshal.ml} (93%) rename helm/{matita/matitaMoo.mli => ocaml/grafite/grafiteMarshal.mli} (83%) create mode 100644 helm/ocaml/library/.cvsignore create mode 100644 helm/ocaml/library/Makefile rename helm/ocaml/{cic_unification => library}/coercDb.ml (100%) rename helm/ocaml/{cic_unification => library}/coercDb.mli (100%) rename helm/{matita/matitacleanLib.ml => ocaml/library/libraryClean.ml} (78%) create mode 100644 helm/ocaml/library/libraryClean.mli rename helm/{matita/matitaDb.ml => ocaml/library/libraryDb.ml} (98%) rename helm/{matita/matitaDb.mli => ocaml/library/libraryDb.mli} (100%) rename helm/{matita/matitacleanLib.mli => ocaml/library/libraryMisc.ml} (87%) create mode 100644 helm/ocaml/library/libraryMisc.mli create mode 100644 helm/ocaml/library/librarySync.ml create mode 100644 helm/ocaml/library/librarySync.mli diff --git a/helm/matita/.depend b/helm/matita/.depend index e10acb2be..368d18f28 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -2,100 +2,73 @@ applyTransformation.cmo: applyTransformation.cmi applyTransformation.cmx: applyTransformation.cmi disambiguatePp.cmo: disambiguatePp.cmi disambiguatePp.cmx: disambiguatePp.cmi -dump_moo.cmo: matitaMoo.cmi matitaLog.cmi buildTimeConf.cmo -dump_moo.cmx: matitaMoo.cmx matitaLog.cmx buildTimeConf.cmx -matitacleanLib.cmo: matitaSync.cmi matitaMoo.cmi matitaMisc.cmi matitaLog.cmi \ - matitaExcPp.cmi matitaDb.cmi buildTimeConf.cmo matitacleanLib.cmi -matitacleanLib.cmx: matitaSync.cmx matitaMoo.cmx matitaMisc.cmx matitaLog.cmx \ - matitaExcPp.cmx matitaDb.cmx buildTimeConf.cmx matitacleanLib.cmi -matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi \ - matitaInit.cmi matitaDb.cmi matitaclean.cmi -matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx \ - matitaInit.cmx matitaDb.cmx matitaclean.cmi -matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMoo.cmi \ - matitaLog.cmi matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ - matitaDb.cmi buildTimeConf.cmo matitacLib.cmi -matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMoo.cmx \ - matitaLog.cmx matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ - matitaDb.cmx buildTimeConf.cmx matitacLib.cmi +dump_moo.cmo: buildTimeConf.cmo +dump_moo.cmx: buildTimeConf.cmx +matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi +matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi +matitacLib.cmo: matitaTypes.cmi matitaMisc.cmi matitaInit.cmi matitaExcPp.cmi \ + matitaEngine.cmi buildTimeConf.cmo matitacLib.cmi +matitacLib.cmx: matitaTypes.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \ + matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi matitac.cmo: matitamake.cmo matitadep.cmi matitaclean.cmi matitacLib.cmi matitac.cmx: matitamake.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx -matitaDb.cmo: matitaMisc.cmi matitaDb.cmi -matitaDb.cmx: matitaMisc.cmx matitaDb.cmi -matitadep.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi matitaInit.cmi \ - matitadep.cmi -matitadep.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaInit.cmx \ - matitadep.cmi +matitadep.cmo: matitaMisc.cmi matitaInit.cmi matitadep.cmi +matitadep.cmx: matitaMisc.cmx matitaInit.cmx matitadep.cmi matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi -matitaEngine.cmo: matitacleanLib.cmi matitaTypes.cmi matitaSync.cmi \ - matitaMoo.cmi matitaMisc.cmi matitaLog.cmi matitaDisambiguator.cmi \ - matitaDb.cmi matitaEngine.cmi -matitaEngine.cmx: matitacleanLib.cmx matitaTypes.cmx matitaSync.cmx \ - matitaMoo.cmx matitaMisc.cmx matitaLog.cmx matitaDisambiguator.cmx \ - matitaDb.cmx matitaEngine.cmi -matitaExcPp.cmo: matitaTypes.cmi matitaMoo.cmi matitaDisambiguator.cmi \ - matitaExcPp.cmi -matitaExcPp.cmx: matitaTypes.cmx matitaMoo.cmx matitaDisambiguator.cmx \ - matitaExcPp.cmi +matitaEngine.cmo: matitaTypes.cmi matitaSync.cmi matitaMisc.cmi \ + matitaDisambiguator.cmi matitaEngine.cmi +matitaEngine.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx \ + matitaDisambiguator.cmx matitaEngine.cmi +matitaExcPp.cmo: matitaTypes.cmi matitaDisambiguator.cmi matitaExcPp.cmi +matitaExcPp.cmx: matitaTypes.cmx matitaDisambiguator.cmx matitaExcPp.cmi matitaGeneratedGui.cmo: matitaGeneratedGui.cmi matitaGeneratedGui.cmx: matitaGeneratedGui.cmi matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi -matitaGui.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \ - matitaScript.cmi matitaMoo.cmi matitaMisc.cmi matitaMathView.cmi \ - matitaLog.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmi matitaExcPp.cmi \ - matitaDisambiguator.cmi buildTimeConf.cmo matitaGui.cmi -matitaGui.cmx: matitamakeLib.cmx matitacleanLib.cmx matitaTypes.cmx \ - matitaScript.cmx matitaMoo.cmx matitaMisc.cmx matitaMathView.cmx \ - matitaLog.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx matitaExcPp.cmx \ - matitaDisambiguator.cmx buildTimeConf.cmx matitaGui.cmi -matitaInit.cmo: matitamakeLib.cmi matitaDb.cmi buildTimeConf.cmo \ - matitaInit.cmi -matitaInit.cmx: matitamakeLib.cmx matitaDb.cmx buildTimeConf.cmx \ - matitaInit.cmi -matitaLog.cmo: matitaLog.cmi -matitaLog.cmx: matitaLog.cmi -matitamakeLib.cmo: matitaLog.cmi buildTimeConf.cmo matitamakeLib.cmi -matitamakeLib.cmx: matitaLog.cmx buildTimeConf.cmx matitamakeLib.cmi +matitaGui.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi \ + matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi \ + matitaGeneratedGui.cmi matitaExcPp.cmi matitaDisambiguator.cmi \ + buildTimeConf.cmo matitaGui.cmi +matitaGui.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx \ + matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx \ + matitaGeneratedGui.cmx matitaExcPp.cmx matitaDisambiguator.cmx \ + buildTimeConf.cmx matitaGui.cmi +matitaInit.cmo: matitamakeLib.cmi buildTimeConf.cmo matitaInit.cmi +matitaInit.cmx: matitamakeLib.cmx buildTimeConf.cmx matitaInit.cmi +matitamakeLib.cmo: buildTimeConf.cmo matitamakeLib.cmi +matitamakeLib.cmx: buildTimeConf.cmx matitamakeLib.cmi matitamake.cmo: matitamakeLib.cmi matitaInit.cmi matitamake.cmx: matitamakeLib.cmx matitaInit.cmx matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ - matitaLog.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \ - buildTimeConf.cmo applyTransformation.cmi matitaMathView.cmi + matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi buildTimeConf.cmo \ + applyTransformation.cmi matitaMathView.cmi matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ - matitaLog.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \ - buildTimeConf.cmx applyTransformation.cmx matitaMathView.cmi + matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitaMathView.cmi matitaMisc.cmo: matitaTypes.cmi buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi -matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi matitaLog.cmi \ +matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \ matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi matitaEngine.cmi \ buildTimeConf.cmo -matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx matitaLog.cmx \ +matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \ matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx matitaEngine.cmx \ buildTimeConf.cmx -matitaMoo.cmo: matitaTypes.cmi matitaMoo.cmi -matitaMoo.cmx: matitaTypes.cmx matitaMoo.cmi -matitaScript.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \ - matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaEngine.cmi \ - matitaDisambiguator.cmi matitaDb.cmi disambiguatePp.cmi buildTimeConf.cmo \ - matitaScript.cmi -matitaScript.cmx: matitamakeLib.cmx matitacleanLib.cmx matitaTypes.cmx \ - matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaEngine.cmx \ - matitaDisambiguator.cmx matitaDb.cmx disambiguatePp.cmx buildTimeConf.cmx \ - matitaScript.cmi -matitaSync.cmo: matitaTypes.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ - disambiguatePp.cmi matitaSync.cmi -matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ - disambiguatePp.cmx matitaSync.cmi -matitaTypes.cmo: matitaLog.cmi matitaTypes.cmi -matitaTypes.cmx: matitaLog.cmx matitaTypes.cmi +matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaSync.cmi \ + matitaMisc.cmi matitaEngine.cmi matitaDisambiguator.cmi \ + disambiguatePp.cmi buildTimeConf.cmo matitaScript.cmi +matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaSync.cmx \ + matitaMisc.cmx matitaEngine.cmx matitaDisambiguator.cmx \ + disambiguatePp.cmx buildTimeConf.cmx matitaScript.cmi +matitaSync.cmo: matitaTypes.cmi disambiguatePp.cmi matitaSync.cmi +matitaSync.cmx: matitaTypes.cmx disambiguatePp.cmx matitaSync.cmi +matitaTypes.cmo: matitaTypes.cmi +matitaTypes.cmx: matitaTypes.cmi matitaDisambiguator.cmi: matitaTypes.cmi matitaEngine.cmi: matitaTypes.cmi matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaGui.cmi: matitaGuiTypes.cmi matitaDisambiguator.cmi -matitaGuiTypes.cmi: matitaTypes.cmi matitaLog.cmi matitaGeneratedGui.cmi +matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmi matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi -matitaMoo.cmi: matitaTypes.cmi matitaScript.cmi: matitaTypes.cmi matitaSync.cmi: matitaTypes.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 6d32e6eb7..32eccedd4 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -36,18 +36,14 @@ endif # objects for matita (GTK GUI) CMOS = \ buildTimeConf.cmo \ - matitaLog.cmo \ matitaTypes.cmo \ - matitaMoo.cmo \ matitaMisc.cmo \ - matitaDb.cmo \ matitamakeLib.cmo \ matitaInit.cmo \ disambiguatePp.cmo \ matitaSync.cmo \ matitaDisambiguator.cmo \ matitaExcPp.cmo \ - matitacleanLib.cmo \ matitaEngine.cmo \ matitacLib.cmo \ matitaScript.cmo \ @@ -60,18 +56,14 @@ CMOS = \ # objects for matitac (batch compiler) CCMOS = \ buildTimeConf.cmo \ - matitaLog.cmo \ matitaTypes.cmo \ - matitaMoo.cmo \ matitaMisc.cmo \ - matitaDb.cmo \ matitamakeLib.cmo \ matitaInit.cmo \ disambiguatePp.cmo \ matitaSync.cmo \ matitaDisambiguator.cmo \ matitaExcPp.cmo \ - matitacleanLib.cmo \ matitaEngine.cmo \ matitacLib.cmo \ $(NULL) @@ -84,7 +76,6 @@ DEPCMOS = $(CCMOS) CLEANCMOS = $(CCMOS) MAKECMOS = \ buildTimeConf.cmo \ - matitaLog.cmo \ matitamakeLib.cmo \ $(NULL) PROGRAMS_BYTE = matita matitac cicbrowser matitadep matitaclean matitamake dump_moo @@ -154,9 +145,9 @@ matita: $(LIB_DEPS) $(CMOS) matita.ml matita.opt: $(LIBX_DEPS) $(CMXS) matita.ml $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml -dump_moo: buildTimeConf.cmo matitaLog.cmo matitaMoo.cmo dump_moo.ml +dump_moo: buildTimeConf.cmo dump_moo.ml $(OCAMLC) $(PKGS) -linkpkg -o $@ $^ -dump_moo.opt: buildTimeConf.cmx matitaLog.cmx matitaMoo.cmx dump_moo.ml +dump_moo.opt: buildTimeConf.cmx dump_moo.ml $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ matitac: $(CLIB_DEPS) $(CCMOS) $(MAINCMOS) matitac.ml @@ -278,7 +269,7 @@ matita.opt.static: $(STATIC_LINK) $(LIBX_DEPS) $(CMXS) matita.ml $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \ $(STATIC_EXTRA_LIBS) strip $@ -dump_moo.opt.static: $(STATIC_LINK) buildTimeConf.cmx matitaLog.cmx matitaMoo.cmx dump_moo.ml +dump_moo.opt.static: $(STATIC_LINK) buildTimeConf.cmx dump_moo.ml $(STATIC_LINK) $(STATIC_CLIBS) -- \ $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ \ $(STATIC_EXTRA_CLIBS) diff --git a/helm/matita/dump_moo.ml b/helm/matita/dump_moo.ml index 14dea3472..045a7b91b 100644 --- a/helm/matita/dump_moo.ml +++ b/helm/matita/dump_moo.ml @@ -42,10 +42,10 @@ let _ = List.iter (fun fname -> if not (Sys.file_exists fname) then - MatitaLog.error (sprintf "Can't find moo '%s', skipping it." fname) + HLog.error (sprintf "Can't find moo '%s', skipping it." fname) else begin printf "%s:\n" fname; flush stdout; - let commands, metadata = MatitaMoo.load_moo ~fname in + let commands, metadata = GrafiteMarshal.load_moo ~fname in List.iter (fun cmd -> printf " %s\n" (GrafiteAstPp.pp_command cmd); flush stdout) diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 11ae70642..33e2d14c0 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -120,18 +120,18 @@ let _ = (CicEnvironment.list_obj ())); addDebugItem "print selections" (fun () -> let cicMathView = MatitaMathView.cicMathView_instance () in - List.iter MatitaLog.debug (cicMathView#string_of_selections)); + List.iter HLog.debug (cicMathView#string_of_selections)); addDebugItem "dump script status" script#dump; addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ -> Helm_registry.save_to "./foo.conf.xml"); addDebugItem "dump metasenv" (fun _ -> if script#onGoingProof () then - MatitaLog.debug (CicMetaSubst.ppmetasenv [] script#proofMetasenv)); + HLog.debug (CicMetaSubst.ppmetasenv [] script#proofMetasenv)); addDebugItem "dump coercions Db" (fun _ -> List.iter (fun (s,t,u) -> - MatitaLog.debug + HLog.debug (UriManager.name_of_uri u ^ ":" ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t)) (CoercDb.to_list ())); @@ -153,7 +153,7 @@ let _ = (MatitaTypes.get_stack (MatitaScript.current ())#status))); (* addDebugItem "ask record choice" (fun _ -> - MatitaLog.debug (string_of_int + HLog.debug (string_of_int (MatitaGtkMisc.ask_record_choice ~gui ~title:"title" ~message:"msg" ~fields:["a"; "b"; "c"] ~records:[ diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index cac073c29..f26f95c3c 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -1,3 +1,10 @@ +Ferruccio ha cambiato matita.lang: +> iforall +> iexists + +- possibile bug cut&paste di pattern profondi nelle ipotesi: secondo + me sbaglia il nome dell'ipotesi! + TODO NUCLEO - http://mowgli.cs.unibo.it:58084/proofCheck?uri=cic:/Coq/Reals/Rtopology/interior_P3.con diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 84291dcc6..0fc5f6ab8 100644 --- 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 { diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml index b79fea663..fcb022345 100644 --- a/helm/matita/matitaExcPp.ml +++ b/helm/matita/matitaExcPp.ml @@ -44,12 +44,12 @@ let rec to_string = | Unix.Unix_error (code, api, param) -> let err = Unix.error_message code in None, "Unix Error (" ^ api ^ "): " ^ err - | MatitaMoo.Corrupt_moo fname -> + | GrafiteMarshal.Corrupt_moo fname -> None, sprintf ".moo file '%s' is corrupt (shorter than expected)" fname - | MatitaMoo.Checksum_failure fname -> + | GrafiteMarshal.Checksum_failure fname -> None, sprintf "checksum failed for .moo file '%s', please recompile it'" fname - | MatitaMoo.Version_mismatch fname -> + | GrafiteMarshal.Version_mismatch fname -> None, sprintf (".moo file '%s' has been compiled by a different version of matita, " diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 3ea6b4f87..e4c107242 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -53,7 +53,7 @@ class console ~(buffer: GText.buffer) () = method debug s = buffer#insert ~iter:buffer#end_iter ~tags:[debug_tag] s method clear () = buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter - method log_callback (tag: MatitaLog.log_tag) s = + method log_callback (tag: HLog.log_tag) s = match tag with | `Debug -> self#debug (s ^ "\n") | `Error -> self#error (s ^ "\n") @@ -64,20 +64,21 @@ class console ~(buffer: GText.buffer) () = let clean_current_baseuri status = try let baseuri = MatitaTypes.get_string_option status "baseuri" in - MatitacleanLib.clean_baseuris [baseuri] + let basedir = Helm_registry.get "matita.basedir" in + LibraryClean.clean_baseuris ~basedir [baseuri] with MatitaTypes.Option_error _ -> () let ask_and_save_moo_if_needed parent fname status = + let basedir = Helm_registry.get "matita.basedir" in let save () = - let moo_fname = MatitacleanLib.obj_file_of_script fname in - MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in + let moo_fname = MatitaMisc.obj_file_of_script ~basedir fname in + GrafiteMarshal.save_moo moo_fname + status.MatitaTypes.moo_content_rev in if (MatitaScript.current ())#eos && status.MatitaTypes.proof_status = MatitaTypes.No_proof then begin - let mooname = - MatitacleanLib.obj_file_of_script fname - in + let mooname = MatitaMisc.obj_file_of_script ~basedir fname in let rc = MatitaGtkMisc.ask_confirmation ~title:"A .moo can be generated" @@ -471,7 +472,7 @@ class gui () = newDevel#toplevel#misc#hide() end else - MatitaLog.error ("The selected root does not contain " ^ + HLog.error ("The selected root does not contain " ^ match next_devel_must_contain with | Some x -> x | _ -> assert false)); @@ -569,7 +570,7 @@ class gui () = ~check:main#fullscreenMenuItem; main#fullscreenMenuItem#set_active false; (* log *) - MatitaLog.set_log_callback self#console#log_callback; + HLog.set_log_callback self#console#log_callback; GtkSignal.user_handler := (fun exn -> if not (Helm_registry.get_bool "matita.debug") then @@ -601,14 +602,14 @@ class gui () = source_buffer#place_cursor (source_buffer#get_iter (`OFFSET x')); end; - MatitaLog.error msg + HLog.error msg else raise exn); (* script *) ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- [])); let _ = match GSourceView.source_language_from_file BuildTimeConf.lang_file with | None -> - MatitaLog.warn (sprintf "can't load language file %s" + HLog.warn (sprintf "can't load language file %s" BuildTimeConf.lang_file) | Some matita_lang -> source_buffer#set_language matita_lang; diff --git a/helm/matita/matitaGuiTypes.mli b/helm/matita/matitaGuiTypes.mli index 99b90495f..52dca43f7 100644 --- a/helm/matita/matitaGuiTypes.mli +++ b/helm/matita/matitaGuiTypes.mli @@ -31,7 +31,7 @@ object method debug: string -> unit method clear: unit -> unit - method log_callback: MatitaLog.log_callback + method log_callback: HLog.log_callback end class type browserWin = diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml index d01275308..134e00e7c 100644 --- a/helm/matita/matitaInit.ml +++ b/helm/matita/matitaInit.ml @@ -65,7 +65,7 @@ let initialize_db init_status = if not (already_configured [ Db ] init_status) then begin MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - MatitaDb.create_owner_environment (); + LibraryDb.create_owner_environment (); Db::init_status end else diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 7a54049a8..15a4a126d 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -341,7 +341,7 @@ object (self) | Some ((None, _, _, _, _, _) as info) -> (* building a dummy sequent for obj *) let t = self#find_obj_conclusion id in - MatitaLog.debug (CicPp.ppterm t); + HLog.debug (CicPp.ppterm t); info, (~-1, [], t) | None -> assert false in @@ -397,7 +397,7 @@ object (self) ids_to_terms, ids_to_hypotheses, ids_to_father_ids, Hashtbl.create 1, None)); let name = "sequent_viewer.xml" in - MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name); + HLog.debug ("load_sequent: dumping MathML to ./" ^ name); ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement @@ -417,7 +417,7 @@ object (self) self#thaw | _ -> let name = "cic_browser.xml" in - MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name); + HLog.debug ("cic_browser: dumping MathML to ./" ^ name); ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement; current_mathml <- Some mathml); diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index e311973c9..077809a17 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -45,31 +45,6 @@ let is_empty buri = | Http_getter_types.Ls_object _ -> false) (Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/")) -let safe_remove fname = if Sys.file_exists fname then Sys.remove fname - -let is_dir_empty d = - try - let od = Unix.opendir d in - try - ignore (Unix.readdir od); - ignore (Unix.readdir od); - ignore (Unix.readdir od); - Unix.closedir od; - false - with End_of_file -> - Unix.closedir od; - true - with Unix.Unix_error _ -> true - -let safe_rmdir d = try Unix.rmdir d with Unix.Unix_error _ -> () - -let rec rmdir_descend d = - if is_dir_empty d then - begin - safe_rmdir d; - rmdir_descend (Filename.dirname d) - end - let absolute_path file = if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file @@ -180,13 +155,6 @@ let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n let end_ma_RE = Pcre.regexp "\\.ma$" -let obj_file_of_baseuri baseuri = - let path = - Helm_registry.get "matita.basedir" ^ "/xml" ^ - Pcre.replace ~pat:"^cic:" ~templ:"" baseuri - in - path ^ ".moo" - let list_tl_at ?(equality=(==)) e l = let rec aux = function @@ -196,3 +164,41 @@ let list_tl_at ?(equality=(==)) e l = in aux l +let baseuri_of_file file = + let uri = ref None in + let ic = open_in file in + let istream = Ulexing.from_utf8_channel ic in + (try + while true do + try + let stm = GrafiteParser.parse_statement istream in + match baseuri_of_baseuri_decl stm with + | Some buri -> + let u = strip_trailing_slash buri in + if String.length u < 5 || String.sub u 0 5 <> "cic:/" then + HLog.error (file ^ " sets an incorrect baseuri: " ^ buri); + (try + ignore(Http_getter.resolve u) + with + | Http_getter_types.Unresolvable_URI _ -> + HLog.error (file ^ " sets an unresolvable baseuri: "^buri) + | Http_getter_types.Key_not_found _ -> ()); + uri := Some u; + raise End_of_file + | None -> () + with + CicNotationParser.Parse_error err -> + HLog.error ("Unable to parse: " ^ file); + HLog.error ("Parse error: " ^ err); + () + done + with End_of_file -> close_in ic); + match !uri with + | Some uri -> uri + | None -> failwith ("No baseuri defined in " ^ file) + +let obj_file_of_script ~basedir f = + if f = "coq.ma" then BuildTimeConf.coq_notation_script else + let baseuri = baseuri_of_file f in + LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri + diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index a04258aee..253625106 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -29,15 +29,6 @@ val baseuri_of_baseuri_decl: (** check whether no objects are defined below a given baseuri *) val is_empty: string -> bool -(** removes a file if it exists *) -val safe_remove: string -> unit -(** removes a dir if it exists and is empty *) -val safe_rmdir: string -> unit -(** checks if the dir is empty *) -val is_dir_empty: string -> bool -(** removes a directory and recursively the father (if empty) *) -val rmdir_descend: string -> unit - val absolute_path: string -> string (** @return true if file is a (textual) proof script *) @@ -89,5 +80,6 @@ val singleton: (unit -> 'a) -> (unit -> 'a) (** given the base name of an image, returns its full path *) val image_path: string -> string -val obj_file_of_baseuri: string -> string +val baseuri_of_file: string -> string +val obj_file_of_script : basedir:string -> string -> string diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 756958427..d4f7d5e00 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -213,7 +213,7 @@ let eval_with_engine guistuff status user_goal parsed_text st = let disambiguate_macro_term term status user_goal = let module MD = MatitaDisambiguator in - let dbd = MatitaDb.instance () in + let dbd = LibraryDb.instance () in let metasenv = MatitaTypes.get_proof_metasenv status in let context = MatitaTypes.get_proof_context status user_goal in let interps = @@ -226,12 +226,12 @@ let disambiguate_macro_term term status user_goal = let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = let module TAPp = GrafiteAstPp in let module MQ = MetadataQuery in - let module MDB = MatitaDb in + let module MDB = LibraryDb in let module CTC = CicTypeChecker in let module CU = CicUniv in (* no idea why ocaml wants this *) let parsed_text_length = String.length parsed_text in - let dbd = MatitaDb.instance () in + let dbd = LibraryDb.instance () in match mac with (* WHELP's stuff *) | TA.WMatch (loc, term) -> @@ -296,10 +296,10 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = in [ new_status , (extra_text, ast) ], parsed_text_length | _ -> - MatitaLog.error + HLog.error "The result of the urichooser should be only 1 uri, not:\n"; List.iter ( - fun u -> MatitaLog.error (UriManager.string_of_uri u ^ "\n") + fun u -> HLog.error (UriManager.string_of_uri u ^ "\n") ) selected; assert false) | TA.Check (_,term) -> @@ -345,7 +345,7 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script = let module TAPp = GrafiteAstPp in let module MD = MatitaDisambiguator in - let module ML = MatitacleanLib in + let module ML = MatitaMisc in match ex with | TA.Command (loc, _) | TA.Tactical (loc, _, _) -> (try @@ -361,7 +361,9 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script "Do you want to redefine the corresponding "^ "part of the library?") with - | `YES -> MatitacleanLib.clean_baseuris [u] + | `YES -> + let basedir = Helm_registry.get "matita.basedir" in + LibraryClean.clean_baseuris ~basedir [u] | `NO -> () | `CANCEL -> raise MatitaTypes.Cancel); eval_with_engine @@ -519,7 +521,7 @@ object (self) *) in let s = match statement with Some s -> s | None -> self#getFuture in - MatitaLog.debug ("evaluating: " ^ first_line s ^ " ..."); + HLog.debug ("evaluating: " ^ first_line s ^ " ..."); (try aux (`Raw s) with End_of_file -> raise Margin) method private _retract offset status new_statements new_history = @@ -619,7 +621,7 @@ object (self) output_string oc (buffer#get_text ~start:buffer#start_iter ~stop:buffer#end_iter ()); close_out oc; - MatitaLog.debug ("backup " ^ f ^ " saved") + HLog.debug ("backup " ^ f ^ " saved") end method private goto_top = @@ -762,11 +764,11 @@ object (self) (* debug *) method dump () = - MatitaLog.debug "script status:"; - MatitaLog.debug ("history size: " ^ string_of_int (List.length history)); - MatitaLog.debug (sprintf "%d statements:" (List.length statements)); - List.iter MatitaLog.debug statements; - MatitaLog.debug ("Current file name: " ^ + HLog.debug "script status:"; + HLog.debug ("history size: " ^ string_of_int (List.length history)); + HLog.debug (sprintf "%d statements:" (List.length statements)); + List.iter HLog.debug statements; + HLog.debug ("Current file name: " ^ (match guistuff.filenamedata with |None,_ -> "[ no name ]" | Some f,_ -> f)); diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 74340421f..96ec76013 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -83,130 +83,44 @@ let set_proof_aliases status new_aliases = let extract_alias types uri = fst(List.fold_left ( fun (acc,i) (name, _, _, cl) -> - (name, UriManager.string_of_uri (UriManager.uri_of_uriref uri i None)) - :: + (name, UriManager.uri_of_uriref uri i None) :: (fst(List.fold_left ( fun (acc,j) (name,_) -> - (((name,UriManager.string_of_uri (UriManager.uri_of_uriref uri i - (Some j))) :: acc) , j+1) + (((name,UriManager.uri_of_uriref uri i + (Some j)) :: acc) , j+1) ) (acc,1) cl)),i+1 ) ([],0) types) let build_aliases = List.map - (fun (name,suri) -> + (fun (name,uri) -> DisambiguateTypes.Id name, - (suri, fun _ _ _ -> CicUtil.term_of_uri (UriManager.uri_of_string suri))) + (UriManager.string_of_uri uri, fun _ _ _ -> CicUtil.term_of_uri uri)) -let add_aliases_for_inductive_def status types suri = - let uri = UriManager.uri_of_string suri in +let add_aliases_for_inductive_def status types uri = let aliases = build_aliases (extract_alias types uri) in set_proof_aliases status aliases -let add_alias_for_constant status suri = - let uri = UriManager.uri_of_string suri in +let add_alias_for_constant status uri = let name = UriManager.name_of_uri uri in - let new_env = build_aliases [(name,suri)] in + let new_env = build_aliases [(name,uri)] in set_proof_aliases status new_env -let add_aliases_for_object status suri = +let add_aliases_for_object status uri = function Cic.InductiveDefinition (types,_,_,_) -> - add_aliases_for_inductive_def status types suri - | Cic.Constant _ -> add_alias_for_constant status suri + add_aliases_for_inductive_def status types uri + | Cic.Constant _ -> add_alias_for_constant status uri | Cic.Variable _ | Cic.CurrentProof _ -> assert false -let paths_and_uris_of_obj uri status = - let basedir = get_string_option status "basedir" ^ "/xml" in - let innertypesuri = UriManager.innertypesuri_of_uri uri in - let bodyuri = UriManager.bodyuri_of_uri uri in - let univgraphuri = UriManager.univgraphuri_of_uri uri in - let innertypesfilename = Str.replace_first (Str.regexp "^cic:") "" - (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in - let innertypespath = basedir ^ "/" ^ innertypesfilename in - let xmlfilename = Str.replace_first (Str.regexp "^cic:/") "" - (UriManager.string_of_uri uri) ^ ".xml.gz" in - let xmlpath = basedir ^ "/" ^ xmlfilename in - let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") "" - (UriManager.string_of_uri uri) ^ ".body.xml.gz" in - let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in - let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") "" - (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in - let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in - xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, - xmlunivgraphpath, univgraphuri - -let save_object_to_disk status uri obj ugraph univlist = - let ensure_path_exists path = - let dir = Filename.dirname path in - HExtlib.mkdir dir - in - (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *) - let annobj = Cic2acic.plain_acic_object_of_cic_object obj in - (* prepare XML *) - let xml, bodyxml = - Cic2Xml.print_object - uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj - in - let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, - xmlunivgraphpath, univgraphuri = - paths_and_uris_of_obj uri status - in - List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]); - (* now write to disk *) - ensure_path_exists xmlpath; - Xml.pp ~gzip:true xml (Some xmlpath); - CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist; - (* we return a list of uri,path we registered/created *) - (uri,xmlpath) :: - (univgraphuri,xmlunivgraphpath) :: - (* now the optional body, both write and register *) - (match bodyxml,bodyuri with - None,None -> [] - | Some bodyxml,Some bodyuri-> - ensure_path_exists xmlbodypath; - Xml.pp ~gzip:true bodyxml (Some xmlbodypath); - [bodyuri, xmlbodypath] - | _-> assert false) - -let typecheck_obj = - let profiler = HExtlib.profile "add_obj.typecheck_obj" in - fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj - -let index_obj = - let profiler = HExtlib.profile "add_obj.index_obj" in - fun ~dbd ~uri -> - profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri - let add_obj uri obj status = - let dbd = MatitaDb.instance () in - let suri = UriManager.string_of_uri uri in - if CicEnvironment.in_library uri then - command_error (sprintf "%s already defined" suri) - else begin - typecheck_obj uri obj; (* 1 *) - let _, ugraph, univlist = - CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in - try - index_obj ~dbd ~uri; (* 2 must be in the env *) - try - let new_stuff=save_object_to_disk status uri obj ugraph univlist in(*3*) - try - MatitaLog.message (sprintf "%s defined" suri); - let status = add_aliases_for_object status suri obj in - { status with objects = new_stuff @ status.objects; - proof_status = No_proof } - with exc -> - List.iter MatitaMisc.safe_remove (List.map snd new_stuff); (* -3 *) - raise exc - with exc -> - ignore(MatitaDb.remove_uri uri); (* -2 *) - raise exc - with exc -> - CicEnvironment.remove_obj uri; (* -1 *) - raise exc - end + let basedir = Helm_registry.get "matita.basedir" in + let status = + { add_aliases_for_object status uri obj with proof_status = No_proof} + in + LibrarySync.add_obj uri obj basedir; + status let add_obj = let profiler = HExtlib.profile "add_obj" in @@ -250,9 +164,6 @@ let id_list_diff l2 l1 = let diff = S.diff s2 s1 in S.fold (fun uri uris -> uri :: uris) diff [] -let remove_coercion uri = - CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri) - let time_travel ~present ~past = let objs_to_remove = urixstring_list_diff present.objects past.objects in let coercions_to_remove = uri_list_diff present.coercions past.coercions in @@ -260,17 +171,19 @@ let time_travel ~present ~past = id_list_diff present.notation_ids past.notation_ids in let debug_list = ref [] in - List.iter remove_coercion coercions_to_remove; + List.iter + (fun uri -> CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri)) + coercions_to_remove; List.iter (fun (uri,p) -> - MatitaMisc.safe_remove p; + HExtlib.safe_remove p; (try CicEnvironment.remove_obj uri with CicEnvironment.Object_not_found _ -> - MatitaLog.debug + HLog.debug (sprintf "time_travel removes from cache %s that is not in" (UriManager.string_of_uri uri))); - let l = MatitaDb.remove_uri uri in + let l = LibraryDb.remove_uri uri in debug_list := UriManager.string_of_uri uri :: !debug_list @ l) objs_to_remove; List.iter CicNotation.remove_notation notation_to_remove @@ -295,44 +208,9 @@ let time_travel ~present ~past = List.iter2 (fun x y -> if x <> y then raise Exit) l1 l2 with | Invalid_argument _ | Exit -> - MatitaLog.debug "It seems you garbaged something..."; - MatitaLog.debug "l1:"; - List.iter MatitaLog.debug l1; - MatitaLog.debug "l2:"; - List.iter MatitaLog.debug l2 + HLog.debug "It seems you garbaged something..."; + HLog.debug "l1:"; + List.iter HLog.debug l1; + HLog.debug "l2:"; + List.iter HLog.debug l2 *) - -let last_baseuri = ref "" - -let remove ?(verbose=false) uri = - let derived_uris_of_uri uri = - UriManager.innertypesuri_of_uri uri :: - UriManager.univgraphuri_of_uri uri :: - (match UriManager.bodyuri_of_uri uri with - | None -> [] - | Some u -> [u]) - in - let to_remove = - uri :: - (if UriManager.uri_is_ind uri then MatitaDb.xpointers_of_ind uri else []) @ - derived_uris_of_uri uri - in - List.iter - (fun uri -> - (try - (* WARNING: non reentrant debugging code *) - if verbose then - let baseuri = UriManager.buri_of_uri uri in - if !last_baseuri <> baseuri then - begin - MatitaLog.debug ("Removing: " ^ baseuri ^ "/*"); - last_baseuri := baseuri - end; - let file = Http_getter.resolve' uri in - MatitaMisc.safe_remove file; - MatitaMisc.rmdir_descend (Filename.dirname file) - with Http_getter_types.Key_not_found _ -> ()); - remove_coercion uri; - ignore (MatitaDb.remove_uri uri); - CicEnvironment.remove_obj uri) - to_remove diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli index f3906fb8b..1a2d8445c 100644 --- a/helm/matita/matitaSync.mli +++ b/helm/matita/matitaSync.mli @@ -43,10 +43,3 @@ val set_proof_aliases : MatitaTypes.status -> (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list -> MatitaTypes.status - - (* removes the object from DB, Disk, CoercionsDB, CicEnvironment, getter - * asserts the uri is resolved to file:// so it is only for - * user's objects - * @param verbose defaults to false *) -val remove: ?verbose:bool -> UriManager.uri -> unit - diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 8ee007d47..2d59ef95d 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -89,27 +89,27 @@ let set_metasenv metasenv status = { status with proof_status = proof_status } let dump_status status = - MatitaLog.message "status.aliases:\n"; - MatitaLog.message "status.proof_status:"; - MatitaLog.message + HLog.message "status.aliases:\n"; + HLog.message "status.proof_status:"; + HLog.message (match status.proof_status with | No_proof -> "no proof\n" | Incomplete_proof _ -> "incomplete proof\n" | Proof _ -> "proof\n" | Intermediate _ -> "Intermediate\n"); - MatitaLog.message "status.options\n"; + HLog.message "status.options\n"; StringMap.iter (fun k v -> let v = match v with | String s -> s | Int i -> string_of_int i in - MatitaLog.message (k ^ "::=" ^ v)) status.options; - MatitaLog.message "status.coercions\n"; - MatitaLog.message "status.objects:\n"; + HLog.message (k ^ "::=" ^ v)) status.options; + HLog.message "status.coercions\n"; + HLog.message "status.objects:\n"; List.iter (fun (u,_) -> - MatitaLog.message (UriManager.string_of_uri u)) status.objects + HLog.message (UriManager.string_of_uri u)) status.objects let get_option status name = try @@ -127,11 +127,7 @@ let set_option status name value = let s = Str.global_replace (Str.regexp "/$") "" s in s in - let types = - [ "baseuri", (`String, mangle_dir); - "basedir", (`String, mangle_dir); - ] - in + let types = [ "baseuri", (`String, mangle_dir); ] in let ty_and_mangler = try List.assoc name types diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index a558d10e3..321e26b99 100644 --- a/helm/matita/matitaTypes.mli +++ b/helm/matita/matitaTypes.mli @@ -52,13 +52,10 @@ type option_value = type options = option_value StringMap.t val no_options : 'a StringMap.t -type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command -type moo = ast_command list * GrafiteAst.metadata list (** *) - type status = { aliases: DisambiguateTypes.environment; (** disambiguation aliases *) multi_aliases: DisambiguateTypes.multiple_environment; - moo_content_rev: moo; + moo_content_rev: GrafiteMarshal.moo; proof_status: proof_status; (** logical status *) options: options; objects: (UriManager.uri * string) list; (** in-scope objects, with paths *) @@ -69,7 +66,7 @@ type status = { 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_content: GrafiteMarshal.ast_command list -> status -> status val add_moo_metadata: GrafiteAst.metadata list -> status -> status val dump_status : status -> unit diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 872dccace..fe22c9da7 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -52,7 +52,7 @@ let run_script is eval_function = else stm in - MatitaLog.debug ("Executing: ``" ^ stm ^ "''")) + HLog.debug ("Executing: ``" ^ stm ^ "''")) in try eval_function status is cb @@ -61,7 +61,7 @@ let run_script is eval_function = | End_of_file | CicNotationParser.Parse_error _ as exn -> raise exn | exn -> - MatitaLog.error (snd (MatitaExcPp.to_string exn)); + HLog.error (snd (MatitaExcPp.to_string exn)); raise exn let fname () = @@ -70,11 +70,11 @@ let fname () = | _ -> MatitaInit.die_usage () let pp_ocaml_mode () = - MatitaLog.message ""; - MatitaLog.message " ** Entering Ocaml mode ** "; - MatitaLog.message ""; - MatitaLog.message "Type 'go ();;' to enter an interactive matitac"; - MatitaLog.message "" + HLog.message ""; + HLog.message " ** Entering Ocaml mode ** "; + HLog.message ""; + HLog.message "Type 'go ();;' to enter an interactive matitac"; + HLog.message "" let clean_exit n = let opt_exit = @@ -87,7 +87,8 @@ let clean_exit n = | Some status -> try let baseuri = MatitaTypes.get_string_option !status "baseuri" in - MatitacleanLib.clean_baseuris ~verbose:false [baseuri]; + let basedir = Helm_registry.get "matita.basedir" in + LibraryClean.clean_baseuris ~basedir ~verbose:false [baseuri]; opt_exit n with MatitaTypes.Option_error("baseuri", "not found") -> (* no baseuri ==> nothing to clean yet *) @@ -102,23 +103,23 @@ let rec interactive_loop () = "matita.includes")) with | MatitaEngine.Drop -> pp_ocaml_mode () - | Sys.Break -> MatitaLog.error "user break!"; interactive_loop () + | Sys.Break -> HLog.error "user break!"; interactive_loop () | MatitaTypes.Command_error _ -> interactive_loop () | End_of_file -> print_newline (); clean_exit (Some 0) | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> let (x, y) = HExtlib.loc_of_floc floc in - MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); + HLog.error (sprintf "Parse error at %d-%d: %s" x y err); interactive_loop () - | exn -> MatitaLog.error (Printexc.to_string exn); interactive_loop () + | exn -> HLog.error (Printexc.to_string exn); interactive_loop () let go () = Helm_registry.load_from BuildTimeConf.matita_conf; CicNotation.load_notation BuildTimeConf.core_notation_script; Http_getter.init (); MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - MatitaDb.create_owner_environment (); + LibraryDb.create_owner_environment (); CicEnvironment.set_trust (* environment trust *) (let trust = Helm_registry.get_bool "matita.environment_trust" in fun _ -> trust); @@ -132,21 +133,21 @@ let main ~mode = let fname = fname () in status := Some (ref (Lazy.force MatitaEngine.initial_status)); Sys.catch_break true; - let origcb = MatitaLog.get_log_callback () in + let origcb = HLog.get_log_callback () in let newcb 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; + HLog.set_log_callback newcb; let matita_debug = Helm_registry.get_bool "matita.debug" in try let time = Unix.time () in if Helm_registry.get_bool "matita.quiet" then origcb `Message ("compiling " ^ Filename.basename fname ^ "...") else - MatitaLog.message (sprintf "execution of %s started:" fname); + HLog.message (sprintf "execution of %s started:" fname); let is = Ulexing.from_utf8_channel (match fname with @@ -169,28 +170,29 @@ let main ~mode = let hou = if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else "" in - let proof_status,moo_content_rev = + let proof_status,moo_content_rev,status = match !status with - | Some s -> !s.proof_status, !s.moo_content_rev + | Some s -> !s.proof_status, !s.moo_content_rev, !s | None -> assert false in if proof_status <> MatitaTypes.No_proof then begin - MatitaLog.error + HLog.error "there are still incomplete proofs at the end of the script"; clean_exit (Some 2) end else begin - let moo_fname = MatitacleanLib.obj_file_of_script fname in - MatitaMoo.save_moo moo_fname moo_content_rev; - MatitaLog.message + let basedir = Helm_registry.get "matita.basedir" in + let moo_fname = MatitaMisc.obj_file_of_script ~basedir fname in + GrafiteMarshal.save_moo moo_fname moo_content_rev; + HLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); exit 0 end with | Sys.Break -> - MatitaLog.error "user break!"; + HLog.error "user break!"; if mode = `COMPILER then clean_exit (Some ~-1) else @@ -202,7 +204,7 @@ let main ~mode = pp_ocaml_mode () | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> let (x, y) = HExtlib.loc_of_floc floc in - MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err); + HLog.error (sprintf "Parse error at %d-%d: %s" x y err); if mode = `COMPILER then clean_exit (Some 1) else diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index 5aabf7558..807f54525 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -32,10 +32,11 @@ let main () = let _ = MatitaInit.initialize_all () in let uris_to_remove = ref [] in let files_to_remove = ref [] in + let basedir = Helm_registry.get "matita.basedir" in (match Helm_registry.get_list Helm_registry.string "matita.args" with | [ "all" ] -> - MatitaDb.clean_owner_environment (); - let xmldir = Helm_registry.get "matita.basedir" ^ "/xml" in + LibraryDb.clean_owner_environment (); + let xmldir = basedir ^ "/xml" in ignore (Sys.command ("find " ^ xmldir ^ @@ -54,9 +55,9 @@ let main () = UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> files_to_remove := suri :: !files_to_remove; - let u = MatitacleanLib.baseuri_of_file suri in + let u = MatitaMisc.baseuri_of_file suri in if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin - MatitaLog.error (sprintf "File %s defines a bad baseuri: %s" + HLog.error (sprintf "File %s defines a bad baseuri: %s" suri u); exit 1 end else @@ -64,7 +65,9 @@ let main () = in uris_to_remove := uri :: !uris_to_remove) files); - MatitacleanLib.clean_baseuris !uris_to_remove; - let moos = List.map MatitacleanLib.obj_file_of_script !files_to_remove in - List.iter MatitaMisc.safe_remove moos + LibraryClean.clean_baseuris ~basedir !uris_to_remove; + let moos = + List.map (MatitaMisc.obj_file_of_script ~basedir) !files_to_remove + in + List.iter HExtlib.safe_remove moos diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 5b22cb70b..34f7744a0 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -48,12 +48,13 @@ let main () = try aux paths with Sys_error _ as exc -> - MatitaLog.error ("Unable to read " ^ path); - MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths); + HLog.error ("Unable to read " ^ path); + HLog.error ("opts.include_paths was " ^ String.concat ":" paths); raise exc in MatitaInit.load_configuration_file (); MatitaInit.parse_cmdline (); + let basedir = Helm_registry.get "matita.basedir" in List.iter (fun file -> let ic = open_in file in @@ -71,10 +72,10 @@ let main () = | GrafiteAst.IncludeDep path -> try let ma_file = if path <> "coq.ma" then find path else path in - let moo_file = MatitacleanLib.obj_file_of_script ma_file in + let moo_file = MatitaMisc.obj_file_of_script ~basedir ma_file in Hashtbl.add include_deps file moo_file with Sys_error _ -> - MatitaLog.warn + HLog.warn ("Unable to find " ^ path ^ " that is included in " ^ file)) dependencies) (Helm_registry.get_list Helm_registry.string "matita.args"); @@ -84,7 +85,8 @@ let main () = match dep with | None -> () | Some u -> - Hashtbl.add include_deps file (MatitaMisc.obj_file_of_baseuri u)) + Hashtbl.add include_deps file + (LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri:u)) uri_deps; List.iter (fun file -> @@ -92,7 +94,7 @@ let main () = let deps = List.fast_sort Pervasives.compare deps in let deps = HExtlib.list_uniq deps in let deps = file :: deps in - let moo = MatitacleanLib.obj_file_of_script file in + let moo = MatitaMisc.obj_file_of_script ~basedir file in Printf.printf "%s: %s\n" moo (String.concat " " deps); Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo) (Helm_registry.get_list Helm_registry.string "matita.args") diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml index a2640a42f..8f164b73a 100644 --- a/helm/matita/matitamakeLib.ml +++ b/helm/matita/matitamakeLib.ml @@ -25,10 +25,10 @@ let logger = fun mark -> match mark with - | `Error -> MatitaLog.error - | `Warning -> MatitaLog.warn - | `Debug -> MatitaLog.debug - | `Message -> MatitaLog.message + | `Error -> HLog.error + | `Warning -> HLog.warn + | `Debug -> HLog.debug + | `Message -> HLog.message ;; type development = @@ -192,19 +192,19 @@ let vt100 s = let rex_noendline = Pcre.regexp "\\n" in let s = Pcre.replace ~rex:rex_noendline s in let tokens = Pcre.split ~rex s in - let logger = ref MatitaLog.message in + let logger = ref HLog.message in let rec aux = function | [] -> () | s::tl -> (if Pcre.pmatch ~rex:rex_i s then - logger := MatitaLog.message + logger := HLog.message else if Pcre.pmatch ~rex:rex_w s then - logger := MatitaLog.warn + logger := HLog.warn else if Pcre.pmatch ~rex:rex_e s then - logger := MatitaLog.error + logger := HLog.error else if Pcre.pmatch ~rex:rex_d s then - logger := MatitaLog.debug + logger := HLog.debug else !logger s); aux tl diff --git a/helm/ocaml/METAS/meta.helm-cic_unification.src b/helm/ocaml/METAS/meta.helm-cic_unification.src index 6cb775dca..75e2d4d31 100644 --- a/helm/ocaml/METAS/meta.helm-cic_unification.src +++ b/helm/ocaml/METAS/meta.helm-cic_unification.src @@ -1,4 +1,4 @@ -requires="helm-cic_proof_checking" +requires="helm-cic_proof_checking helm-library" version="0.0.1" archive(byte)="cic_unification.cma" archive(native)="cic_unification.cmxa" diff --git a/helm/ocaml/METAS/meta.helm-library.src b/helm/ocaml/METAS/meta.helm-library.src new file mode 100644 index 000000000..366269cf9 --- /dev/null +++ b/helm/ocaml/METAS/meta.helm-library.src @@ -0,0 +1,5 @@ +requires="helm-grafite helm-metadata" +version="0.0.1" +archive(byte)="library.cma" +archive(native)="library.cmxa" +linkopts="" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 30c25dc19..306dc2695 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -14,12 +14,13 @@ MODULES = \ getter \ cic \ cic_proof_checking \ - cic_unification \ cic_acic \ acic_content \ content_pres \ grafite \ metadata \ + library \ + cic_unification \ whelp \ tactics \ cic_disambiguation \ diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend index 8da4518c3..1fc74e25b 100644 --- a/helm/ocaml/cic_unification/.depend +++ b/helm/ocaml/cic_unification/.depend @@ -1,14 +1,11 @@ -coercGraph.cmi: coercDb.cmi cicMetaSubst.cmo: cicMetaSubst.cmi cicMetaSubst.cmx: cicMetaSubst.cmi cicMkImplicit.cmo: cicMkImplicit.cmi cicMkImplicit.cmx: cicMkImplicit.cmi cicUnification.cmo: cicMetaSubst.cmi cicUnification.cmi cicUnification.cmx: cicMetaSubst.cmx cicUnification.cmi -coercDb.cmo: coercDb.cmi -coercDb.cmx: coercDb.cmi -coercGraph.cmo: coercDb.cmi coercGraph.cmi -coercGraph.cmx: coercDb.cmx coercGraph.cmi +coercGraph.cmo: coercGraph.cmi +coercGraph.cmx: coercGraph.cmi cicRefine.cmo: coercGraph.cmi cicUnification.cmi cicMkImplicit.cmi \ cicMetaSubst.cmi cicRefine.cmi cicRefine.cmx: coercGraph.cmx cicUnification.cmx cicMkImplicit.cmx \ diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile index caad67767..26e5d4ada 100644 --- a/helm/ocaml/cic_unification/Makefile +++ b/helm/ocaml/cic_unification/Makefile @@ -5,7 +5,6 @@ INTERFACE_FILES = \ cicMetaSubst.mli \ cicMkImplicit.mli \ cicUnification.mli \ - coercDb.mli \ coercGraph.mli \ cicRefine.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/extlib/.depend b/helm/ocaml/extlib/.depend index 249ee3196..afbba1bb5 100644 --- a/helm/ocaml/extlib/.depend +++ b/helm/ocaml/extlib/.depend @@ -2,3 +2,5 @@ hExtlib.cmo: hExtlib.cmi hExtlib.cmx: hExtlib.cmi patternMatcher.cmo: patternMatcher.cmi patternMatcher.cmx: patternMatcher.cmi +hLog.cmo: hLog.cmi +hLog.cmx: hLog.cmi diff --git a/helm/ocaml/extlib/Makefile b/helm/ocaml/extlib/Makefile index 9f6267a06..f271f6ace 100644 --- a/helm/ocaml/extlib/Makefile +++ b/helm/ocaml/extlib/Makefile @@ -4,6 +4,7 @@ PREDICATES = INTERFACE_FILES = \ hExtlib.mli \ patternMatcher.mli \ + hLog.mli \ $(NULL) IMPLEMENTATION_FILES = \ $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/extlib/hExtlib.ml b/helm/ocaml/extlib/hExtlib.ml index 6afae34a7..a0f9d8d6c 100644 --- a/helm/ocaml/extlib/hExtlib.ml +++ b/helm/ocaml/extlib/hExtlib.ml @@ -272,6 +272,27 @@ let find ?(test = fun _ -> true) path = in aux [] [path] +let safe_remove fname = if Sys.file_exists fname then Sys.remove fname + +let is_dir_empty d = + let od = Unix.opendir d in + let rec aux () = + let name = Unix.readdir od in + if name <> "." && name <> ".." then false else aux () in + let res = try aux () with End_of_file -> true in + Unix.closedir od; + res + +let safe_rmdir d = try Unix.rmdir d with Unix.Unix_error _ -> () + +let rec rmdir_descend d = + if is_dir_empty d then + begin + safe_rmdir d; + rmdir_descend (Filename.dirname d) + end + + (** {2 Exception handling} *) let finally at_end f arg = diff --git a/helm/ocaml/extlib/hExtlib.mli b/helm/ocaml/extlib/hExtlib.mli index a598ddb1a..6416afcaf 100644 --- a/helm/ocaml/extlib/hExtlib.mli +++ b/helm/ocaml/extlib/hExtlib.mli @@ -35,6 +35,11 @@ val is_dir: string -> bool (** @return true if file is a directory *) val is_regular: string -> bool (** @return true if file is a regular file *) val mkdir: string -> unit (** create dir and parents. @raise Failure *) val tilde_expand: string -> string (** bash-like (head) tilde expansion *) +val safe_remove: string -> unit (** removes a file if it exists *) +val safe_rmdir: string -> unit (** removes a dir if it exists and is empty *) +val is_dir_empty: string -> bool (** checks if the dir is empty *) +val rmdir_descend: string -> unit (** rmdir -p *) + (** find all _files_ matching test under a filesystem root *) val find: ?test:(string -> bool) -> string -> string list diff --git a/helm/matita/matitaLog.ml b/helm/ocaml/extlib/hLog.ml similarity index 100% rename from helm/matita/matitaLog.ml rename to helm/ocaml/extlib/hLog.ml diff --git a/helm/matita/matitaLog.mli b/helm/ocaml/extlib/hLog.mli similarity index 100% rename from helm/matita/matitaLog.mli rename to helm/ocaml/extlib/hLog.mli diff --git a/helm/ocaml/grafite/.depend b/helm/ocaml/grafite/.depend index c0590d25a..c5774b069 100644 --- a/helm/ocaml/grafite/.depend +++ b/helm/ocaml/grafite/.depend @@ -1,9 +1,12 @@ grafiteAstPp.cmi: grafiteAst.cmo grafiteParser.cmi: grafiteAst.cmo cicNotation.cmi: grafiteAst.cmo +grafiteMarshal.cmi: grafiteAst.cmo grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi grafiteParser.cmo: grafiteAst.cmo grafiteParser.cmi grafiteParser.cmx: grafiteAst.cmx grafiteParser.cmi cicNotation.cmo: grafiteParser.cmi grafiteAst.cmo cicNotation.cmi cicNotation.cmx: grafiteParser.cmx grafiteAst.cmx cicNotation.cmi +grafiteMarshal.cmo: grafiteAst.cmo grafiteMarshal.cmi +grafiteMarshal.cmx: grafiteAst.cmx grafiteMarshal.cmi diff --git a/helm/ocaml/grafite/Makefile b/helm/ocaml/grafite/Makefile index bc8ffc258..0ce510b20 100644 --- a/helm/ocaml/grafite/Makefile +++ b/helm/ocaml/grafite/Makefile @@ -5,6 +5,7 @@ INTERFACE_FILES = \ grafiteAstPp.mli \ grafiteParser.mli \ cicNotation.mli \ + grafiteMarshal.mli \ $(NULL) IMPLEMENTATION_FILES = \ grafiteAst.ml \ diff --git a/helm/matita/matitaMoo.ml b/helm/ocaml/grafite/grafiteMarshal.ml similarity index 93% rename from helm/matita/matitaMoo.ml rename to helm/ocaml/grafite/grafiteMarshal.ml index bdea339b7..b1601911e 100644 --- a/helm/matita/matitaMoo.ml +++ b/helm/ocaml/grafite/grafiteMarshal.ml @@ -27,6 +27,9 @@ exception Checksum_failure of string exception Corrupt_moo of string exception Version_mismatch of string +type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command +type moo = ast_command list * GrafiteAst.metadata list (** *) + let marshal_flags = [] (** .moo file format @@ -61,7 +64,7 @@ let load_moo ~fname = 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.moo) = + let (moo:moo) = Marshal.from_string marshalled 0 in moo diff --git a/helm/matita/matitaMoo.mli b/helm/ocaml/grafite/grafiteMarshal.mli similarity index 83% rename from helm/matita/matitaMoo.mli rename to helm/ocaml/grafite/grafiteMarshal.mli index 75b71a58f..663d2fa43 100644 --- a/helm/matita/matitaMoo.mli +++ b/helm/ocaml/grafite/grafiteMarshal.mli @@ -28,8 +28,11 @@ exception Checksum_failure of string exception Corrupt_moo of string exception Version_mismatch of string -val save_moo: fname:string -> MatitaTypes.moo -> unit +type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command +type moo = ast_command list * GrafiteAst.metadata list (** *) + +val save_moo: fname:string -> moo -> unit (** @raise Corrupt_moo *) -val load_moo: fname:string -> MatitaTypes.moo +val load_moo: fname:string -> moo diff --git a/helm/ocaml/library/.cvsignore b/helm/ocaml/library/.cvsignore new file mode 100644 index 000000000..f83e2a8d0 --- /dev/null +++ b/helm/ocaml/library/.cvsignore @@ -0,0 +1,7 @@ +*.cmi +*.cma +*.cmo +*.cmx +*.cmxa +*.o +*.a diff --git a/helm/ocaml/library/Makefile b/helm/ocaml/library/Makefile new file mode 100644 index 000000000..e50f03e93 --- /dev/null +++ b/helm/ocaml/library/Makefile @@ -0,0 +1,14 @@ +PACKAGE = library +PREDICATES = + +INTERFACE_FILES = \ + libraryMisc.mli \ + libraryDb.mli \ + coercDb.mli \ + librarySync.mli \ + libraryClean.mli \ + $(NULL) +IMPLEMENTATION_FILES = \ + $(INTERFACE_FILES:%.mli=%.ml) + +include ../Makefile.common diff --git a/helm/ocaml/cic_unification/coercDb.ml b/helm/ocaml/library/coercDb.ml similarity index 100% rename from helm/ocaml/cic_unification/coercDb.ml rename to helm/ocaml/library/coercDb.ml diff --git a/helm/ocaml/cic_unification/coercDb.mli b/helm/ocaml/library/coercDb.mli similarity index 100% rename from helm/ocaml/cic_unification/coercDb.mli rename to helm/ocaml/library/coercDb.mli diff --git a/helm/matita/matitacleanLib.ml b/helm/ocaml/library/libraryClean.ml similarity index 78% rename from helm/matita/matitacleanLib.ml rename to helm/ocaml/library/libraryClean.ml index a4156921d..f2ac57199 100644 --- a/helm/matita/matitacleanLib.ml +++ b/helm/ocaml/library/libraryClean.ml @@ -57,7 +57,7 @@ let one_step_depend suri = obj_tbl buri in try - let rc = HMysql.exec (MatitaDb.instance ()) query in + let rc = HMysql.exec (LibraryDb.instance ()) query in let l = ref [] in HMysql.iter rc ( fun row -> @@ -111,7 +111,7 @@ let close_uri_list uri_to_remove = inhabitants @ acc) [] buri_to_remove with HGT.Invalid_URI u -> - MatitaLog.error ("We were listing an invalid buri: " ^ u); + HLog.error ("We were listing an invalid buri: " ^ u); exit 1 in (* now we want the list of all uri that depend on them *) @@ -155,7 +155,7 @@ let close_using_moos buris = in List.iter (fun path -> - let _, metadata = MatitaMoo.load_moo ~fname:path in + let _, metadata = GrafiteMarshal.load_moo ~fname:path in let baseuri_of_current_moo = let rec aux = function | [] -> assert false @@ -192,7 +192,7 @@ let close_using_moos buris = in objects_to_remove -let clean_baseuris ?(verbose=true) buris = +let clean_baseuris ?(verbose=true) ~basedir buris = Hashtbl.clear cache_of_processed_baseuri; let buris = List.map HGM.strip_trailing_slash buris in debug_prerr "clean_baseuris called on:"; @@ -211,57 +211,28 @@ let clean_baseuris ?(verbose=true) buris = List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; List.iter (fun buri -> - MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri)) + HExtlib.safe_remove (LibraryMisc.obj_file_of_baseuri basedir buri)) (HExtlib.list_uniq (List.fast_sort Pervasives.compare (List.map (UriManager.buri_of_uri) l))); - List.iter (MatitaSync.remove ~verbose) l; + List.iter + (let last_baseuri = ref "" in + fun uri -> + let buri = UriManager.buri_of_uri uri in + if buri <> !last_baseuri then + begin + HLog.message ("Removing: " ^ buri ^ "/*"); + last_baseuri := buri + end; + LibrarySync.remove_obj uri + ) l; cleaned_no := !cleaned_no + List.length l; if !cleaned_no > 30 then begin cleaned_no := 0; List.iter (function table -> - ignore (HMysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table))) + ignore (HMysql.exec (LibraryDb.instance ()) ("OPTIMIZE TABLE " ^ table))) [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl (); MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl(); MetadataTypes.count_tbl()] end - -let baseuri_of_file file = - let uri = ref None in - let ic = open_in file in - let istream = Ulexing.from_utf8_channel ic in - (try - while true do - try - let stm = GrafiteParser.parse_statement istream in - match MatitaMisc.baseuri_of_baseuri_decl stm with - | Some buri -> - let u = MatitaMisc.strip_trailing_slash buri in - if String.length u < 5 || String.sub u 0 5 <> "cic:/" then - MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri); - (try - ignore(Http_getter.resolve u) - with - | Http_getter_types.Unresolvable_URI _ -> - MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri) - | Http_getter_types.Key_not_found _ -> ()); - uri := Some u; - raise End_of_file - | None -> () - with - CicNotationParser.Parse_error _ as exn -> - prerr_endline ("Unable to parse: " ^ file); - prerr_endline (snd (MatitaExcPp.to_string exn)); - () - done - with End_of_file -> close_in ic); - match !uri with - | Some uri -> uri - | None -> failwith ("No baseuri defined in " ^ file) - -let obj_file_of_script f = - if f = "coq.ma" then BuildTimeConf.coq_notation_script else - let baseuri = baseuri_of_file f in - MatitaMisc.obj_file_of_baseuri baseuri - diff --git a/helm/ocaml/library/libraryClean.mli b/helm/ocaml/library/libraryClean.mli new file mode 100644 index 000000000..deca8f4a7 --- /dev/null +++ b/helm/ocaml/library/libraryClean.mli @@ -0,0 +1,26 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val clean_baseuris : ?verbose:bool -> basedir:string -> string list -> unit diff --git a/helm/matita/matitaDb.ml b/helm/ocaml/library/libraryDb.ml similarity index 98% rename from helm/matita/matitaDb.ml rename to helm/ocaml/library/libraryDb.ml index e3c7041dd..389b7f483 100644 --- a/helm/matita/matitaDb.ml +++ b/helm/ocaml/library/libraryDb.ml @@ -68,7 +68,7 @@ let clean_owner_environment () = List.iter (fun suffix -> try - MatitaMisc.safe_remove (Http_getter.resolve (uri ^ suffix)) + HExtlib.safe_remove (Http_getter.resolve (uri ^ suffix)) with Http_getter_types.Key_not_found _ -> ()) [""; ".body"; ".types"]) owned_uris; diff --git a/helm/matita/matitaDb.mli b/helm/ocaml/library/libraryDb.mli similarity index 100% rename from helm/matita/matitaDb.mli rename to helm/ocaml/library/libraryDb.mli diff --git a/helm/matita/matitacleanLib.mli b/helm/ocaml/library/libraryMisc.ml similarity index 87% rename from helm/matita/matitacleanLib.mli rename to helm/ocaml/library/libraryMisc.ml index 91aa51b2a..2b6d64f63 100644 --- a/helm/matita/matitacleanLib.mli +++ b/helm/ocaml/library/libraryMisc.ml @@ -23,8 +23,7 @@ * http://helm.cs.unibo.it/ *) -val clean_baseuris : ?verbose:bool -> string list -> unit - -val baseuri_of_file: string -> string -val obj_file_of_script : string -> string +let obj_file_of_baseuri ~basedir ~baseuri = + let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in + path ^ ".moo" diff --git a/helm/ocaml/library/libraryMisc.mli b/helm/ocaml/library/libraryMisc.mli new file mode 100644 index 000000000..fc93095eb --- /dev/null +++ b/helm/ocaml/library/libraryMisc.mli @@ -0,0 +1,27 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + + +val obj_file_of_baseuri: basedir:string -> baseuri:string -> string diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml new file mode 100644 index 000000000..d853243dd --- /dev/null +++ b/helm/ocaml/library/librarySync.ml @@ -0,0 +1,142 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +exception AlreadyDefined of UriManager.uri + +let uris_of_obj uri = + let innertypesuri = UriManager.innertypesuri_of_uri uri in + let bodyuri = UriManager.bodyuri_of_uri uri in + let univgraphuri = UriManager.univgraphuri_of_uri uri in + innertypesuri,bodyuri,univgraphuri + +let paths_and_uris_of_obj uri ~basedir = + let basedir = basedir ^ "/xml" in + let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in + let innertypesfilename = Str.replace_first (Str.regexp "^cic:") "" + (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in + let innertypespath = basedir ^ "/" ^ innertypesfilename in + let xmlfilename = Str.replace_first (Str.regexp "^cic:/") "" + (UriManager.string_of_uri uri) ^ ".xml.gz" in + let xmlpath = basedir ^ "/" ^ xmlfilename in + let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") "" + (UriManager.string_of_uri uri) ^ ".body.xml.gz" in + let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in + let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") "" + (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in + let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in + xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, + xmlunivgraphpath, univgraphuri + +let save_object_to_disk ~basedir uri obj ugraph univlist = + let ensure_path_exists path = + let dir = Filename.dirname path in + HExtlib.mkdir dir + in + (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *) + let annobj = Cic2acic.plain_acic_object_of_cic_object obj in + (* prepare XML *) + let xml, bodyxml = + Cic2Xml.print_object + uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj + in + let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, + xmlunivgraphpath, univgraphuri = + paths_and_uris_of_obj uri basedir + in + List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]); + (* now write to disk *) + ensure_path_exists xmlpath; + Xml.pp ~gzip:true xml (Some xmlpath); + CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist; + (* we return a list of uri,path we registered/created *) + (uri,xmlpath) :: + (univgraphuri,xmlunivgraphpath) :: + (* now the optional body, both write and register *) + (match bodyxml,bodyuri with + None,None -> [] + | Some bodyxml,Some bodyuri-> + ensure_path_exists xmlbodypath; + Xml.pp ~gzip:true bodyxml (Some xmlbodypath); + [bodyuri, xmlbodypath] + | _-> assert false) + + +let typecheck_obj = + let profiler = HExtlib.profile "add_obj.typecheck_obj" in + fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj + +let index_obj = + let profiler = HExtlib.profile "add_obj.index_obj" in + fun ~dbd ~uri -> + profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri + +let add_obj uri obj ~basedir = + let dbd = LibraryDb.instance () in + if CicEnvironment.in_library uri then + raise (AlreadyDefined uri) + else begin + typecheck_obj uri obj; (* 1 *) + let _, ugraph, univlist = + CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in + try + index_obj ~dbd ~uri; (* 2 must be in the env *) + try + (*3*) + let new_stuff = save_object_to_disk ~basedir uri obj ugraph univlist in + try + HLog.message + (Printf.sprintf "%s defined" (UriManager.string_of_uri uri)) + with exc -> + List.iter HExtlib.safe_remove (List.map snd new_stuff); (* -3 *) + raise exc + with exc -> + ignore(LibraryDb.remove_uri uri); (* -2 *) + raise exc + with exc -> + CicEnvironment.remove_obj uri; (* -1 *) + raise exc + end + +let remove_obj uri = + let derived_uris_of_uri uri = + let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in + innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u]) + in + let to_remove = + uri :: + (if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else []) @ + derived_uris_of_uri uri + in + List.iter + (fun uri -> + (try + let file = Http_getter.resolve' uri in + HExtlib.safe_remove file; + HExtlib.rmdir_descend (Filename.dirname file) + with Http_getter_types.Key_not_found _ -> ()); + ignore (LibraryDb.remove_uri uri); + CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri); + CicEnvironment.remove_obj uri) + to_remove diff --git a/helm/ocaml/library/librarySync.mli b/helm/ocaml/library/librarySync.mli new file mode 100644 index 000000000..0e0916e4d --- /dev/null +++ b/helm/ocaml/library/librarySync.mli @@ -0,0 +1,31 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* returns a list of added URIs and their paths on disk *) +(*CSC: the path on disk should be computable from the URI!!! *) +val add_obj: UriManager.uri -> Cic.obj -> basedir:string -> unit + +(* inverse of add_obj; it does not remove the objects depending on it! *) +val remove_obj: UriManager.uri -> unit -- 2.39.2