From: Enrico Tassi Date: Mon, 5 Oct 2009 11:28:05 +0000 (+0000) Subject: new ng_library module X-Git-Tag: make_still_working~3384 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a18562238677261e3d0b590e046290a14fe62e74;hp=1fbc5fd1d3e29b6b95e2613d10760e3bfd3e213f;p=helm.git new ng_library module --- diff --git a/helm/software/components/METAS/meta.helm-grafite_engine.src b/helm/software/components/METAS/meta.helm-grafite_engine.src index 45a02a30b..e23e0d0a7 100644 --- a/helm/software/components/METAS/meta.helm-grafite_engine.src +++ b/helm/software/components/METAS/meta.helm-grafite_engine.src @@ -1,4 +1,4 @@ -requires="helm-library helm-grafite helm-tactics helm-ng_tactics helm-ng_refiner" +requires="helm-library helm-grafite helm-tactics helm-ng_tactics helm-ng_library" version="0.0.1" archive(byte)="grafite_engine.cma" archive(native)="grafite_engine.cmxa" diff --git a/helm/software/components/METAS/meta.helm-lexicon.src b/helm/software/components/METAS/meta.helm-lexicon.src index 741fd603e..a98593133 100644 --- a/helm/software/components/METAS/meta.helm-lexicon.src +++ b/helm/software/components/METAS/meta.helm-lexicon.src @@ -1,4 +1,4 @@ -requires="helm-content_pres helm-cic_disambiguation camlp5.gramlib" +requires="helm-content_pres helm-ng_library helm-cic_disambiguation camlp5.gramlib" version="0.0.1" archive(byte)="lexicon.cma" archive(native)="lexicon.cmxa" diff --git a/helm/software/components/METAS/meta.helm-ng_library.src b/helm/software/components/METAS/meta.helm-ng_library.src new file mode 100644 index 000000000..94402278d --- /dev/null +++ b/helm/software/components/METAS/meta.helm-ng_library.src @@ -0,0 +1,5 @@ +requires="helm-ng_refiner" +version="0.0.1" +archive(byte)="ng_library.cma" +archive(native)="ng_library.cmxa" +linkopts="" diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile index 7035411f3..25169744f 100644 --- a/helm/software/components/Makefile +++ b/helm/software/components/Makefile @@ -27,6 +27,7 @@ MODULES = \ acic_content \ grafite \ ng_refiner \ + ng_library \ ng_cic_content \ content_pres \ cic_unification \ @@ -44,6 +45,7 @@ MODULES = \ tptp_grafite \ ng_kernel \ ng_refiner \ + ng_library \ $(NULL) METAS = $(MODULES:%=METAS/META.helm-%) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index ea5afab4c..5ae6e92ed 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -487,7 +487,8 @@ let inject_unification_hint = = let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n) in - NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint + NCicLibrary.Serializer.register + "unification_hints" basic_eval_unification_hint ;; let eval_unification_hint status t n = @@ -514,7 +515,7 @@ let inject_constraint = let u2 = refresh_uri_in_universe u2 in basic_eval_add_constraint (u1,u2) in - NRstatus.Serializer.register "constraints" basic_eval_add_constraint + NCicLibrary.Serializer.register "constraints" basic_eval_add_constraint ;; let eval_add_constraint status u1 u2 = @@ -980,7 +981,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status status in let status = - NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) + NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) status in let status = GrafiteTypes.add_moo_content diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml index 550cb93c4..2f103cf83 100644 --- a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml +++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml @@ -294,7 +294,7 @@ let record_ncoercion = let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term = List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l in - NRstatus.Serializer.register "ncoercion" aux_l + NCicLibrary.Serializer.register "ncoercion" aux_l ;; let basic_eval_and_record_ncoercion infos status = diff --git a/helm/software/components/grafite_parser/nEstatus.ml b/helm/software/components/grafite_parser/nEstatus.ml index 306eca9d6..ebfd686cd 100644 --- a/helm/software/components/grafite_parser/nEstatus.ml +++ b/helm/software/components/grafite_parser/nEstatus.ml @@ -14,13 +14,13 @@ class type g_status = object inherit LexiconEngine.g_status - inherit NRstatus.g_dumpable_status + inherit NCicLibrary.g_dumpable_status end class status = object (self) inherit LexiconEngine.status - inherit NRstatus.dumpable_status + inherit NCicLibrary.dumpable_status method set_estatus : 'status. #g_status as 'status -> 'self = fun o -> (self#set_lexicon_engine_status o)#set_dumpable_status o end diff --git a/helm/software/components/grafite_parser/nEstatus.mli b/helm/software/components/grafite_parser/nEstatus.mli index 8e361407f..cc356aa46 100644 --- a/helm/software/components/grafite_parser/nEstatus.mli +++ b/helm/software/components/grafite_parser/nEstatus.mli @@ -14,13 +14,13 @@ class type g_status = object inherit LexiconEngine.g_status - inherit NRstatus.g_dumpable_status + inherit NCicLibrary.g_dumpable_status end class status : object ('self) inherit LexiconEngine.status - inherit NRstatus.dumpable_status + inherit NCicLibrary.dumpable_status inherit g_status method set_estatus: #g_status -> 'self end diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 159cee382..fa6e42064 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -8,7 +8,6 @@ nCicPp.cmi: nUri.cmi nReference.cmi nCic.cmo nCicReduction.cmi: nCic.cmo nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmo nCicUntrusted.cmi: nCic.cmo -nCicLibrary.cmi: nUri.cmi nReference.cmi nCic.cmo nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -47,9 +46,3 @@ nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicReduction.cmi nCicEnvironment.cmi nCic.cmo nCicUntrusted.cmi nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi -nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nReference.cmi nCicUtils.cmi \ - nCicUntrusted.cmi nCicPp.cmi nCicEnvironment.cmi nCic2OCic.cmi nCic.cmo \ - nCicLibrary.cmi -nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCicUtils.cmx \ - nCicUntrusted.cmx nCicPp.cmx nCicEnvironment.cmx nCic2OCic.cmx nCic.cmx \ - nCicLibrary.cmi diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt index 01056b468..7720472e8 100644 --- a/helm/software/components/ng_kernel/.depend.opt +++ b/helm/software/components/ng_kernel/.depend.opt @@ -8,7 +8,6 @@ nCicPp.cmi: nUri.cmi nReference.cmi nCic.cmx nCicReduction.cmi: nCic.cmx nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx nCicUntrusted.cmi: nCic.cmx -nCicLibrary.cmi: nUri.cmi nReference.cmi nCic.cmx nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -47,9 +46,3 @@ nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicReduction.cmi nCicEnvironment.cmi nCic.cmx nCicUntrusted.cmi nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi -nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nReference.cmi nCicUtils.cmi \ - nCicUntrusted.cmi nCicPp.cmi nCicEnvironment.cmi nCic2OCic.cmi nCic.cmx \ - nCicLibrary.cmi -nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCicUtils.cmx \ - nCicUntrusted.cmx nCicPp.cmx nCicEnvironment.cmx nCic2OCic.cmx nCic.cmx \ - nCicLibrary.cmi diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index d533c8f73..50ecd2b47 100644 --- a/helm/software/components/ng_kernel/Makefile +++ b/helm/software/components/ng_kernel/Makefile @@ -12,8 +12,7 @@ INTERFACE_FILES = \ nCicPp.mli \ nCicReduction.mli \ nCicTypeChecker.mli \ - nCicUntrusted.mli \ - nCicLibrary.mli + nCicUntrusted.mli IMPLEMENTATION_FILES = \ nCic.ml $(INTERFACE_FILES:%.mli=%.ml) @@ -23,13 +22,6 @@ EXTRA_OBJECTS_TO_CLEAN = %.cmi: OCAMLOPTIONS += -w Ae %.cmx: OCAMLOPTIONS += -w Ae -all: rt check -%: %.ml $(PACKAGE).cma - $(OCAMLC) -package helm-$(PACKAGE) -linkpkg -o $@ $< -all.opt opt: rt.opt check.opt -%.opt: %.ml $(PACKAGE).cmxa - $(OCAMLOPT) -package helm-$(PACKAGE) -linkpkg -o $@ $< - depend.dot: $(IMPLEMENTATION_FILES) $(INTERFACE_FILES) ocamldoc -o depend.dot -rectypes -I ../extlib/ -I ../cic -I ../cic_proof_checking/ -I ../urimanager/ -I ../logger/ -I ../registry/ -I ../getter/ -I ../hmysql/ -I ../library/ -I ../metadata/ -dot nUri.ml nReference.ml nCic.ml nCicPp.ml nCicEnvironment.ml nCicSubstitution.ml nCicReduction.ml nCicTypeChecker.ml nCicUtils.ml nCicLibrary.ml cat depend.dot | grep -v "^}$$" > /tmp/depend.dot && mv /tmp/depend.dot . diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml deleted file mode 100644 index 8f014d4d2..000000000 --- a/helm/software/components/ng_kernel/check.ml +++ /dev/null @@ -1,216 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id$ *) - -let debug = true -let ignore_exc = false -let rank_all_dependencies = false -let trust_environment = false -let print_object = true - -let indent = ref 0;; - -let load_graph, get_graph = - let oldg = ref CicUniv.empty_ugraph in - (function uri -> - let _,g = CicEnvironment.get_obj !oldg uri in - oldg := g), - (function _ -> !oldg) -;; - -let logger = - let do_indent () = String.make !indent ' ' in - (function - | `Start_type_checking s -> - if debug then - prerr_endline (do_indent () ^ "Start: " ^ NUri.string_of_uri s); - incr indent - | `Type_checking_completed s -> - decr indent; - if debug then - prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s) - | `Type_checking_interrupted s -> - decr indent; - if debug then - prerr_endline (do_indent () ^ "Break: " ^ NUri.string_of_uri s) - | `Type_checking_failed s -> - decr indent; - if debug then - prerr_endline (do_indent () ^ "Fail: " ^ NUri.string_of_uri s) - | `Trust_obj s -> - if debug then - prerr_endline (do_indent () ^ "Trust: " ^ NUri.string_of_uri s)) -;; - -let mk_type n = - if n = 0 then - [`Type, NUri.uri_of_string ("cic:/matita/pts/Type.univ")] - else - [`Type, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")] -;; -let mk_cprop n = - if n = 0 then - [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")] - else - [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")] -;; - - -let _ = - let do_old_logging = ref true in - HelmLogger.register_log_callback - (fun ?append_NL html_msg -> - if !do_old_logging then - prerr_endline (HelmLogger.string_of_html_msg html_msg)); - CicParser.impredicative_set := false; - NCicTypeChecker.set_logger logger; - Helm_registry.load_from "conf.xml"; - let alluris = - try - let s = Sys.argv.(1) in - if s = "-alluris" then - begin - let uri_re = Str.regexp ".*\\(ind\\|con\\)$" in - let uris = Http_getter.getalluris () in - let alluris = List.filter (fun u -> Str.string_match uri_re u 0) uris in - let oc = open_out "alluris.txt" in - List.iter (fun s -> output_string oc (s^"\n")) alluris; - close_out oc; - [] - end - else [s] - with Invalid_argument _ -> - let r = ref [] in - let ic = open_in "alluris.txt" in - try while true do r := input_line ic :: !r; done; [] - with _ -> List.rev !r - in - let alluris = - HExtlib.filter_map - (fun u -> try Some (UriManager.uri_of_string u) with _ -> None) alluris - in - (* brutal *) - prerr_endline "computing graphs to load..."; - let roots_alluris = - if not rank_all_dependencies then - alluris - else ( - let dbd = HSql.quick_connect (LibraryDb.parse_dbd_conf ()) in - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - let uniq l = - HExtlib.list_uniq (List.sort UriManager.compare l) in - let who_uses u = - uniq (List.map (fun (uri,_) -> UriManager.strip_xpointer uri) - (MetadataDeps.inverse_deps ~dbd u)) in - let rec fix acc l = - let acc, todo = - List.fold_left (fun (acc,todo) x -> - let w = who_uses x in - if w = [] then (x::acc,todo) else (acc,uniq (todo@w))) - (acc,[]) l - in - if todo = [] then uniq acc else fix acc todo - in - fix [] alluris) - in - prerr_endline "generating Coq graphs..."; - CicEnvironment.set_trust (fun _ -> trust_environment); - List.iter - (fun u -> - prerr_endline (" - " ^ UriManager.string_of_uri u); - try - ignore(CicTypeChecker.typecheck u); - with - | CicTypeChecker.AssertFailure s - | CicTypeChecker.TypeCheckerFailure s -> - prerr_endline (Lazy.force s); - assert false - ) roots_alluris; - prerr_endline "loading..."; - List.iter - (fun u -> - prerr_endline (" - "^UriManager.string_of_uri u); - try load_graph u with exn -> ()) - roots_alluris; - prerr_endline "finished...."; - let lll, uuu =(CicUniv.do_rank (get_graph ())) in - CicUniv.print_ugraph (get_graph ()); - let lll = List.sort compare lll in - List.iter (fun k -> - prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int (CicUniv.get_rank k))) uuu; - let _ = - try - let rec aux = function - | a::(b::_ as tl) -> - NCicEnvironment.add_lt_constraint (mk_type a) (mk_type b); - NCicEnvironment.add_lt_constraint (mk_type a) (mk_cprop b); - aux tl - | _ -> () - in - aux lll - with NCicEnvironment.BadConstraint s as e -> - prerr_endline (Lazy.force s); raise e - in - prerr_endline "ranked...."; - prerr_endline (NCicEnvironment.pp_constraints ()); - HExtlib.profiling_enabled := false; - List.iter (fun uu -> - let uu= OCic2NCic.nuri_of_ouri uu in - indent := 0; - let o = NCicLibrary.get_obj uu in - if print_object then prerr_endline (NCicPp.ppobj o); - try - NCicEnvironment.check_and_add_obj o - with - exn -> - let rec aux = function - | NCicTypeChecker.AssertFailure s - | NCicTypeChecker.TypeCheckerFailure s - | NCicEnvironment.ObjectNotFound s - | NCicEnvironment.BadConstraint s as e-> - prerr_endline ("######### " ^ Lazy.force s); - if not ignore_exc then raise e - | NCicEnvironment.BadDependency (s,x) as e -> - prerr_endline ("######### " ^ Lazy.force s); - aux x; - if not ignore_exc then raise e - | e -> raise e - in - aux exn - ) - alluris; - NCicEnvironment.invalidate (); - Gc.compact (); - HExtlib.profiling_enabled := true; - NCicTypeChecker.set_logger (fun _ -> ()); - do_old_logging := false; - prerr_endline "typechecking, first with the new and then with the old kernel"; - let prima = Unix.gettimeofday () in - List.iter - (fun u -> - let u= OCic2NCic.nuri_of_ouri u in - indent := 0; - ignore (NCicEnvironment.get_checked_obj u)) - alluris; - let dopo = Unix.gettimeofday () in - Gc.compact (); - let dopo2 = Unix.gettimeofday () in - Printf.eprintf "NEW typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -. dopo); - CicEnvironment.invalidate (); - Gc.compact (); - let prima = Unix.gettimeofday () in - List.iter (fun u -> ignore (CicTypeChecker.typecheck u)) alluris; - let dopo = Unix.gettimeofday () in - Gc.compact (); - let dopo2 = Unix.gettimeofday () in - Printf.eprintf "OLD typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -. dopo) -;; diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml deleted file mode 100644 index e7d7c3b11..000000000 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ /dev/null @@ -1,344 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id$ *) - -exception LibraryOutOfSync of string Lazy.t - -let magic = 2;; - -let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);; - -let refresh_uri_in_universe = - List.map (fun (x,u) -> x, refresh_uri u) -;; - -let rec refresh_uri_in_term = - function - | NCic.Meta (i,(n,NCic.Ctx l)) -> - NCic.Meta (i,(n,NCic.Ctx (List.map refresh_uri_in_term l))) - | NCic.Meta _ as t -> t - | NCic.Const (NReference.Ref (u,spec)) -> - NCic.Const (NReference.reference_of_spec (refresh_uri u) spec) - | NCic.Sort (NCic.Type l) -> NCic.Sort (NCic.Type (refresh_uri_in_universe l)) - | NCic.Match (NReference.Ref (uri,spec),outtype,term,pl) -> - let r = NReference.reference_of_spec (refresh_uri uri) spec in - let outtype = refresh_uri_in_term outtype in - let term = refresh_uri_in_term term in - let pl = List.map refresh_uri_in_term pl in - NCic.Match (r,outtype,term,pl) - | t -> NCicUtils.map (fun _ _ -> ()) () (fun _ -> refresh_uri_in_term) t -;; - -let refresh_uri_in_obj (uri,height,metasenv,subst,obj_kind) = - assert (metasenv = []); - assert (subst = []); - refresh_uri uri,height,metasenv,subst, - NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind -;; - -let path_of_baseuri ?(no_suffix=false) baseuri = - let uri = NUri.string_of_uri baseuri in - let path = String.sub uri 4 (String.length uri - 4) in - let path = Helm_registry.get "matita.basedir" ^ path in - let dirname = Filename.dirname path in - HExtlib.mkdir dirname; - if no_suffix then - path - else - path ^ ".ng" -;; - -let require_path path = - let ch = open_in path in - let mmagic,dump = Marshal.from_channel ch in - close_in ch; - if mmagic <> magic then - raise (LibraryOutOfSync (lazy "The library is out of sync with the implementation. Please recompile the library.")) - else - dump -;; - -let require0 ~baseuri = require_path (path_of_baseuri baseuri);; - -let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";; - - -type timestamp = - [ `Obj of NUri.uri * NCic.obj - | `Constr of NCic.universe * NCic.universe] list * - (NUri.uri * string * NReference.reference) list * - NCic.obj NUri.UriMap.t * - NUri.uri list -;; - -let time0 = [],[],NUri.UriMap.empty,[];; -let storage = ref [];; -let local_aliases = ref [];; -let cache = ref NUri.UriMap.empty;; -let includes = ref [];; - -let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps= - let global_aliases = ref [] in - let rev_includes_map = ref NUri.UriMap.empty in - let store_db () = - let ch = open_out (db_path ()) in - Marshal.to_channel ch (magic,(!global_aliases,!rev_includes_map)) []; - close_out ch in - let load_db () = - HExtlib.mkdir (Helm_registry.get "matita.basedir"); - try - let ga,im = require_path (db_path ()) in - let ga = - List.map - (fun (uri,name,NReference.Ref (uri2,spec)) -> - refresh_uri uri,name,NReference.reference_of_spec (refresh_uri uri2) spec - ) ga in - let im = - NUri.UriMap.fold - (fun u l im -> NUri.UriMap.add (refresh_uri u) (List.map refresh_uri l) im - ) im NUri.UriMap.empty - in - global_aliases := ga; - rev_includes_map := im - with - Sys_error _ -> () in - let get_deps u = - let get_deps_one_step u = - try NUri.UriMap.find u !rev_includes_map with Not_found -> [] in - let rec aux res = - function - [] -> res - | he::tl -> - if List.mem he res then - aux res tl - else - aux (he::res) (get_deps_one_step he @ tl) - in - aux [] [u] in - let remove_deps u = - rev_includes_map := NUri.UriMap.remove u !rev_includes_map; - rev_includes_map := - NUri.UriMap.map - (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !rev_includes_map; - store_db () - in - load_db, - (fun ga -> global_aliases := ga; store_db ()), - (fun () -> !global_aliases), - (fun u l -> - rev_includes_map := NUri.UriMap.add u (l @ get_deps u) !rev_includes_map; - store_db ()), - get_deps, - remove_deps -;; - -let init = load_db;; - -class type g_status = - object - method timestamp: timestamp - end - -class status = - object - val timestamp = (time0 : timestamp) - method timestamp = timestamp - method set_timestamp v = {< timestamp = v >} - method set_library_status - : 'status. #g_status as 'status -> 'self - = fun o -> {< timestamp = o#timestamp >} - end - -let time_travel status = - let sto,ali,cac,inc = status#timestamp in - let diff_len = List.length !storage - List.length sto in - let to_be_deleted,_ = HExtlib.split_nth diff_len !storage in - if List.length to_be_deleted > 0 then - NCicEnvironment.invalidate_item (HExtlib.list_last to_be_deleted); - storage := sto; local_aliases := ali; cache := cac; includes := inc -;; - -let serialize ~baseuri dump = - let ch = open_out (path_of_baseuri baseuri) in - Marshal.to_channel ch (magic,dump) []; - close_out ch; - List.iter - (function - | `Obj (uri,obj) -> - let ch = open_out (path_of_baseuri uri) in - Marshal.to_channel ch (magic,obj) []; - close_out ch - | `Constr _ -> () - ) !storage; - set_global_aliases (!local_aliases @ get_global_aliases ()); - List.iter (fun u -> add_deps u [baseuri]) !includes; - time_travel (new status) -;; - -module type Serializer = - sig - type status - type obj - val register: - string -> - ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> - ('a -> obj) - val serialize: baseuri:NUri.uri -> obj list -> unit - val require: baseuri:NUri.uri -> status -> status - end - -module Serializer(S: sig type status end) = - struct - type status = S.status - type obj = string * Obj.t - - let require1 = ref (fun _ -> assert false (* unknown data*)) - let already_registered = ref [] - - let register tag require = - assert (not (List.mem tag !already_registered)); - already_registered := tag :: !already_registered; - let old_require1 = !require1 in - require1 := - (fun (tag',data) as x -> - if tag=tag' then - require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term - else - old_require1 x); - (fun x -> tag,Obj.repr x) - - let serialize = serialize - - let require ~baseuri status = - includes := baseuri::!includes; - let dump = require0 ~baseuri in - List.fold_right !require1 dump status -end - -let decompile ~baseuri = - let baseuris = get_deps baseuri in - List.iter (fun baseuri -> - remove_deps baseuri; - HExtlib.safe_remove (path_of_baseuri baseuri); - let basepath = path_of_baseuri ~no_suffix:true baseuri in - try - let od = Unix.opendir basepath in - let rec aux names = - try - let name = Unix.readdir od in - if name <> "." && name <> ".." then aux (name::names) else aux names - with - End_of_file -> names in - let names = List.map (fun name -> basepath ^ "/" ^ name) (aux []) in - Unix.closedir od; - List.iter Unix.unlink names; - HExtlib.rmdir_descend basepath; - set_global_aliases - (List.filter - (fun (_,_,NReference.Ref (nuri,_)) -> - Filename.dirname (NUri.string_of_uri nuri) <> NUri.string_of_uri baseuri - ) (get_global_aliases ())) - with - Unix.Unix_error _ -> () (* raised by Unix.opendir, we hope :-) *) - ) baseuris -;; - -LibraryClean.set_decompile_cb - (fun ~baseuri -> decompile ~baseuri:(NUri.uri_of_string baseuri));; - -let fetch_obj uri = - let obj = require0 ~baseuri:uri in - refresh_uri_in_obj obj -;; - -let resolve name = - try - HExtlib.filter_map - (fun (_,name',nref) -> if name'=name then Some nref else None) - (!local_aliases @ get_global_aliases ()) - with - Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name)) -;; - -let aliases_of uri = - HExtlib.filter_map - (fun (uri',_,nref) -> - if NUri.eq uri' uri then Some nref else None) !local_aliases -;; - -let add_obj status ((u,_,_,_,_) as obj) = - NCicEnvironment.check_and_add_obj obj; - storage := (`Obj (u,obj))::!storage; - let _,height,_,_,obj = obj in - let references = - match obj with - NCic.Constant (_,name,None,_,_) -> - [u,name,NReference.reference_of_spec u NReference.Decl] - | NCic.Constant (_,name,Some _,_,_) -> - [u,name,NReference.reference_of_spec u (NReference.Def height)] - | NCic.Fixpoint (is_ind,fl,_) -> - HExtlib.list_mapi - (fun (_,name,recno,_,_) i -> - if is_ind then - u,name,NReference.reference_of_spec u(NReference.Fix(i,recno,height)) - else - u,name,NReference.reference_of_spec u (NReference.CoFix i)) fl - | NCic.Inductive (inductive,leftno,il,_) -> - List.flatten - (HExtlib.list_mapi - (fun (_,iname,_,cl) i -> - HExtlib.list_mapi - (fun (_,cname,_) j-> - u,cname, - NReference.reference_of_spec u (NReference.Con (i,j+1,leftno)) - ) cl @ - [u,iname, - NReference.reference_of_spec u - (NReference.Ind (inductive,i,leftno))] - ) il) - in - local_aliases := references @ !local_aliases; - status#set_timestamp (!storage,!local_aliases,!cache,!includes) -;; - -let add_constraint status u1 u2 = - NCicEnvironment.add_lt_constraint u1 u2; - storage := (`Constr (u1,u2)) :: !storage; - status#set_timestamp (!storage,!local_aliases,!cache,!includes) -;; - -let get_obj u = - try - List.assq u - (HExtlib.filter_map - (function `Obj (u,o) -> Some (u,o) | _ -> None ) - !storage) - with Not_found -> - try fetch_obj u - with Sys_error _ -> - try NUri.UriMap.find u !cache - with Not_found -> - let ouri = NCic2OCic.ouri_of_nuri u in - try - let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in - let l = OCic2NCic.convert_obj ouri o in - List.iter (fun (u,_,_,_,_ as o) -> cache:= NUri.UriMap.add u o !cache) l; - HExtlib.list_last l - with CicEnvironment.Object_not_found u -> - raise (NCicEnvironment.ObjectNotFound - (lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u)))) -;; - -let clear_cache () = cache := NUri.UriMap.empty;; - -NCicEnvironment.set_get_obj get_obj;; -NCicPp.set_get_obj get_obj;; diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli deleted file mode 100644 index 6dc7dde43..000000000 --- a/helm/software/components/ng_kernel/nCicLibrary.mli +++ /dev/null @@ -1,63 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id$ *) - -exception LibraryOutOfSync of string Lazy.t - -type timestamp - -class type g_status = - object - method timestamp: timestamp - end - -class status : - object ('self) - inherit g_status - method set_timestamp: timestamp -> 'self - method set_library_status: #g_status -> 'self - end - -(* it also checks it and add it to the environment *) -val add_obj: #status as 'status -> NCic.obj -> 'status -val add_constraint: - #status as 'status -> NCic.universe -> NCic.universe -> 'status -val aliases_of: NUri.uri -> NReference.reference list -val resolve: string -> NReference.reference list -(* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *) -val get_obj: NUri.uri -> NCic.obj (* changes the current timestamp *) - -val clear_cache : unit -> unit - -val time_travel: #status -> unit -val decompile: baseuri:NUri.uri -> unit - -module type Serializer = - sig - type status - type obj - val register: - string -> - ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> - ('a -> obj) - val serialize: baseuri:NUri.uri -> obj list -> unit - val require: baseuri:NUri.uri -> status -> status - end - -module Serializer(S: sig type status end): Serializer with type status= S.status - -val init: unit -> unit - -(* CSC: only required during old-to-NG phase, to be deleted *) -val refresh_uri: NUri.uri -> NUri.uri - -(* EOF *) diff --git a/helm/software/components/ng_kernel/rt.ml b/helm/software/components/ng_kernel/rt.ml deleted file mode 100644 index 997bc2e3c..000000000 --- a/helm/software/components/ng_kernel/rt.ml +++ /dev/null @@ -1,42 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -(* $Id$ *) - -let _ = - Helm_registry.load_from "conf.xml"; - CicParser.impredicative_set := false; - let u = UriManager.uri_of_string Sys.argv.(1) in - let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph u in - prerr_endline "VECCHIO"; - prerr_endline (CicPp.ppobj o); - let l = OCic2NCic.convert_obj u o in - prerr_endline "OGGETTI:........................................."; - List.iter (fun o -> prerr_endline (NCicPp.ppobj o)) l; - prerr_endline "/OGGETTI:........................................."; - let objs = - List.flatten - (List.map NCic2OCic.convert_nobj l) in - List.iter - (fun (u,o) -> - prerr_endline ("round trip: " ^ UriManager.string_of_uri u); - prerr_endline (CicPp.ppobj o); - prerr_endline "tipo......."; - try CicTypeChecker.typecheck_obj u o - with - CicTypeChecker.TypeCheckerFailure s - | CicTypeChecker.AssertFailure s -> - prerr_endline (Lazy.force s) - | CicEnvironment.Object_not_found uri -> - prerr_endline - ("CicEnvironment: Object not found " ^ UriManager.string_of_uri uri)) - objs; -;; diff --git a/helm/software/components/ng_library/.depend b/helm/software/components/ng_library/.depend new file mode 100644 index 000000000..c76001c01 --- /dev/null +++ b/helm/software/components/ng_library/.depend @@ -0,0 +1,2 @@ +nCicLibrary.cmo: nCicLibrary.cmi +nCicLibrary.cmx: nCicLibrary.cmi diff --git a/helm/software/components/ng_library/.depend.opt b/helm/software/components/ng_library/.depend.opt new file mode 100644 index 000000000..c76001c01 --- /dev/null +++ b/helm/software/components/ng_library/.depend.opt @@ -0,0 +1,2 @@ +nCicLibrary.cmo: nCicLibrary.cmi +nCicLibrary.cmx: nCicLibrary.cmi diff --git a/helm/software/components/ng_library/Makefile b/helm/software/components/ng_library/Makefile new file mode 100644 index 000000000..ee8fbad13 --- /dev/null +++ b/helm/software/components/ng_library/Makefile @@ -0,0 +1,24 @@ +PACKAGE = ng_library +PREDICATES = + +INTERFACE_FILES = \ + nCicLibrary.mli + +IMPLEMENTATION_FILES = \ + $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = +%.cmo: OCAMLOPTIONS += -w Ae +%.cmi: OCAMLOPTIONS += -w Ae +%.cmx: OCAMLOPTIONS += -w Ae + +all: rt check +%: %.ml $(PACKAGE).cma + $(OCAMLC) -package helm-$(PACKAGE) -linkpkg -o $@ $< +all.opt opt: rt.opt check.opt +%.opt: %.ml $(PACKAGE).cmxa + $(OCAMLOPT) -package helm-$(PACKAGE) -linkpkg -o $@ $< + +include ../../Makefile.defs +include ../Makefile.common + diff --git a/helm/software/components/ng_library/check.ml b/helm/software/components/ng_library/check.ml new file mode 100644 index 000000000..8f014d4d2 --- /dev/null +++ b/helm/software/components/ng_library/check.ml @@ -0,0 +1,216 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id$ *) + +let debug = true +let ignore_exc = false +let rank_all_dependencies = false +let trust_environment = false +let print_object = true + +let indent = ref 0;; + +let load_graph, get_graph = + let oldg = ref CicUniv.empty_ugraph in + (function uri -> + let _,g = CicEnvironment.get_obj !oldg uri in + oldg := g), + (function _ -> !oldg) +;; + +let logger = + let do_indent () = String.make !indent ' ' in + (function + | `Start_type_checking s -> + if debug then + prerr_endline (do_indent () ^ "Start: " ^ NUri.string_of_uri s); + incr indent + | `Type_checking_completed s -> + decr indent; + if debug then + prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s) + | `Type_checking_interrupted s -> + decr indent; + if debug then + prerr_endline (do_indent () ^ "Break: " ^ NUri.string_of_uri s) + | `Type_checking_failed s -> + decr indent; + if debug then + prerr_endline (do_indent () ^ "Fail: " ^ NUri.string_of_uri s) + | `Trust_obj s -> + if debug then + prerr_endline (do_indent () ^ "Trust: " ^ NUri.string_of_uri s)) +;; + +let mk_type n = + if n = 0 then + [`Type, NUri.uri_of_string ("cic:/matita/pts/Type.univ")] + else + [`Type, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")] +;; +let mk_cprop n = + if n = 0 then + [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")] + else + [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")] +;; + + +let _ = + let do_old_logging = ref true in + HelmLogger.register_log_callback + (fun ?append_NL html_msg -> + if !do_old_logging then + prerr_endline (HelmLogger.string_of_html_msg html_msg)); + CicParser.impredicative_set := false; + NCicTypeChecker.set_logger logger; + Helm_registry.load_from "conf.xml"; + let alluris = + try + let s = Sys.argv.(1) in + if s = "-alluris" then + begin + let uri_re = Str.regexp ".*\\(ind\\|con\\)$" in + let uris = Http_getter.getalluris () in + let alluris = List.filter (fun u -> Str.string_match uri_re u 0) uris in + let oc = open_out "alluris.txt" in + List.iter (fun s -> output_string oc (s^"\n")) alluris; + close_out oc; + [] + end + else [s] + with Invalid_argument _ -> + let r = ref [] in + let ic = open_in "alluris.txt" in + try while true do r := input_line ic :: !r; done; [] + with _ -> List.rev !r + in + let alluris = + HExtlib.filter_map + (fun u -> try Some (UriManager.uri_of_string u) with _ -> None) alluris + in + (* brutal *) + prerr_endline "computing graphs to load..."; + let roots_alluris = + if not rank_all_dependencies then + alluris + else ( + let dbd = HSql.quick_connect (LibraryDb.parse_dbd_conf ()) in + MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); + let uniq l = + HExtlib.list_uniq (List.sort UriManager.compare l) in + let who_uses u = + uniq (List.map (fun (uri,_) -> UriManager.strip_xpointer uri) + (MetadataDeps.inverse_deps ~dbd u)) in + let rec fix acc l = + let acc, todo = + List.fold_left (fun (acc,todo) x -> + let w = who_uses x in + if w = [] then (x::acc,todo) else (acc,uniq (todo@w))) + (acc,[]) l + in + if todo = [] then uniq acc else fix acc todo + in + fix [] alluris) + in + prerr_endline "generating Coq graphs..."; + CicEnvironment.set_trust (fun _ -> trust_environment); + List.iter + (fun u -> + prerr_endline (" - " ^ UriManager.string_of_uri u); + try + ignore(CicTypeChecker.typecheck u); + with + | CicTypeChecker.AssertFailure s + | CicTypeChecker.TypeCheckerFailure s -> + prerr_endline (Lazy.force s); + assert false + ) roots_alluris; + prerr_endline "loading..."; + List.iter + (fun u -> + prerr_endline (" - "^UriManager.string_of_uri u); + try load_graph u with exn -> ()) + roots_alluris; + prerr_endline "finished...."; + let lll, uuu =(CicUniv.do_rank (get_graph ())) in + CicUniv.print_ugraph (get_graph ()); + let lll = List.sort compare lll in + List.iter (fun k -> + prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int (CicUniv.get_rank k))) uuu; + let _ = + try + let rec aux = function + | a::(b::_ as tl) -> + NCicEnvironment.add_lt_constraint (mk_type a) (mk_type b); + NCicEnvironment.add_lt_constraint (mk_type a) (mk_cprop b); + aux tl + | _ -> () + in + aux lll + with NCicEnvironment.BadConstraint s as e -> + prerr_endline (Lazy.force s); raise e + in + prerr_endline "ranked...."; + prerr_endline (NCicEnvironment.pp_constraints ()); + HExtlib.profiling_enabled := false; + List.iter (fun uu -> + let uu= OCic2NCic.nuri_of_ouri uu in + indent := 0; + let o = NCicLibrary.get_obj uu in + if print_object then prerr_endline (NCicPp.ppobj o); + try + NCicEnvironment.check_and_add_obj o + with + exn -> + let rec aux = function + | NCicTypeChecker.AssertFailure s + | NCicTypeChecker.TypeCheckerFailure s + | NCicEnvironment.ObjectNotFound s + | NCicEnvironment.BadConstraint s as e-> + prerr_endline ("######### " ^ Lazy.force s); + if not ignore_exc then raise e + | NCicEnvironment.BadDependency (s,x) as e -> + prerr_endline ("######### " ^ Lazy.force s); + aux x; + if not ignore_exc then raise e + | e -> raise e + in + aux exn + ) + alluris; + NCicEnvironment.invalidate (); + Gc.compact (); + HExtlib.profiling_enabled := true; + NCicTypeChecker.set_logger (fun _ -> ()); + do_old_logging := false; + prerr_endline "typechecking, first with the new and then with the old kernel"; + let prima = Unix.gettimeofday () in + List.iter + (fun u -> + let u= OCic2NCic.nuri_of_ouri u in + indent := 0; + ignore (NCicEnvironment.get_checked_obj u)) + alluris; + let dopo = Unix.gettimeofday () in + Gc.compact (); + let dopo2 = Unix.gettimeofday () in + Printf.eprintf "NEW typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -. dopo); + CicEnvironment.invalidate (); + Gc.compact (); + let prima = Unix.gettimeofday () in + List.iter (fun u -> ignore (CicTypeChecker.typecheck u)) alluris; + let dopo = Unix.gettimeofday () in + Gc.compact (); + let dopo2 = Unix.gettimeofday () in + Printf.eprintf "OLD typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -. dopo) +;; diff --git a/helm/software/components/ng_library/nCicLibrary.ml b/helm/software/components/ng_library/nCicLibrary.ml new file mode 100644 index 000000000..6987ec1aa --- /dev/null +++ b/helm/software/components/ng_library/nCicLibrary.ml @@ -0,0 +1,378 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id$ *) + +exception LibraryOutOfSync of string Lazy.t + +let magic = 2;; + +let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);; + +let refresh_uri_in_universe = + List.map (fun (x,u) -> x, refresh_uri u) +;; + +let rec refresh_uri_in_term = + function + | NCic.Meta (i,(n,NCic.Ctx l)) -> + NCic.Meta (i,(n,NCic.Ctx (List.map refresh_uri_in_term l))) + | NCic.Meta _ as t -> t + | NCic.Const (NReference.Ref (u,spec)) -> + NCic.Const (NReference.reference_of_spec (refresh_uri u) spec) + | NCic.Sort (NCic.Type l) -> NCic.Sort (NCic.Type (refresh_uri_in_universe l)) + | NCic.Match (NReference.Ref (uri,spec),outtype,term,pl) -> + let r = NReference.reference_of_spec (refresh_uri uri) spec in + let outtype = refresh_uri_in_term outtype in + let term = refresh_uri_in_term term in + let pl = List.map refresh_uri_in_term pl in + NCic.Match (r,outtype,term,pl) + | t -> NCicUtils.map (fun _ _ -> ()) () (fun _ -> refresh_uri_in_term) t +;; + +let refresh_uri_in_obj (uri,height,metasenv,subst,obj_kind) = + assert (metasenv = []); + assert (subst = []); + refresh_uri uri,height,metasenv,subst, + NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind +;; + +let path_of_baseuri ?(no_suffix=false) baseuri = + let uri = NUri.string_of_uri baseuri in + let path = String.sub uri 4 (String.length uri - 4) in + let path = Helm_registry.get "matita.basedir" ^ path in + let dirname = Filename.dirname path in + HExtlib.mkdir dirname; + if no_suffix then + path + else + path ^ ".ng" +;; + +let require_path path = + let ch = open_in path in + let mmagic,dump = Marshal.from_channel ch in + close_in ch; + if mmagic <> magic then + raise (LibraryOutOfSync (lazy "The library is out of sync with the implementation. Please recompile the library.")) + else + dump +;; + +let require0 ~baseuri = require_path (path_of_baseuri baseuri);; + +let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";; + + +type timestamp = + [ `Obj of NUri.uri * NCic.obj + | `Constr of NCic.universe * NCic.universe] list * + (NUri.uri * string * NReference.reference) list * + NCic.obj NUri.UriMap.t * + NUri.uri list +;; + +let time0 = [],[],NUri.UriMap.empty,[];; +let storage = ref [];; +let local_aliases = ref [];; +let cache = ref NUri.UriMap.empty;; +let includes = ref [];; + +let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps= + let global_aliases = ref [] in + let rev_includes_map = ref NUri.UriMap.empty in + let store_db () = + let ch = open_out (db_path ()) in + Marshal.to_channel ch (magic,(!global_aliases,!rev_includes_map)) []; + close_out ch in + let load_db () = + HExtlib.mkdir (Helm_registry.get "matita.basedir"); + try + let ga,im = require_path (db_path ()) in + let ga = + List.map + (fun (uri,name,NReference.Ref (uri2,spec)) -> + refresh_uri uri,name,NReference.reference_of_spec (refresh_uri uri2) spec + ) ga in + let im = + NUri.UriMap.fold + (fun u l im -> NUri.UriMap.add (refresh_uri u) (List.map refresh_uri l) im + ) im NUri.UriMap.empty + in + global_aliases := ga; + rev_includes_map := im + with + Sys_error _ -> () in + let get_deps u = + let get_deps_one_step u = + try NUri.UriMap.find u !rev_includes_map with Not_found -> [] in + let rec aux res = + function + [] -> res + | he::tl -> + if List.mem he res then + aux res tl + else + aux (he::res) (get_deps_one_step he @ tl) + in + aux [] [u] in + let remove_deps u = + rev_includes_map := NUri.UriMap.remove u !rev_includes_map; + rev_includes_map := + NUri.UriMap.map + (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !rev_includes_map; + store_db () + in + load_db, + (fun ga -> global_aliases := ga; store_db ()), + (fun () -> !global_aliases), + (fun u l -> + rev_includes_map := NUri.UriMap.add u (l @ get_deps u) !rev_includes_map; + store_db ()), + get_deps, + remove_deps +;; + +let init = load_db;; + +class type g_status = + object + inherit NRstatus.g_status + method timestamp: timestamp + end + +class status = + object + inherit NRstatus.status + val timestamp = (time0 : timestamp) + method timestamp = timestamp + method set_timestamp v = {< timestamp = v >} + method set_library_status + : 'status. #g_status as 'status -> 'self + = fun o -> {< timestamp = o#timestamp >} + end + + +module type SerializerT = + sig + type status + type obj + val register: + string -> + ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> + ('a -> obj) + val serialize: baseuri:NUri.uri -> obj list -> unit + val require: baseuri:NUri.uri -> status -> status + end + +let time_travel status = + let sto,ali,cac,inc = status#timestamp in + let diff_len = List.length !storage - List.length sto in + let to_be_deleted,_ = HExtlib.split_nth diff_len !storage in + if List.length to_be_deleted > 0 then + NCicEnvironment.invalidate_item (HExtlib.list_last to_be_deleted); + storage := sto; local_aliases := ali; cache := cac; includes := inc +;; + +let serialize ~baseuri dump = + let ch = open_out (path_of_baseuri baseuri) in + Marshal.to_channel ch (magic,dump) []; + close_out ch; + List.iter + (function + | `Obj (uri,obj) -> + let ch = open_out (path_of_baseuri uri) in + Marshal.to_channel ch (magic,obj) []; + close_out ch + | `Constr _ -> () + ) !storage; + set_global_aliases (!local_aliases @ get_global_aliases ()); + List.iter (fun u -> add_deps u [baseuri]) !includes; + time_travel (new status) +;; + +module SerializerF(S: sig type status end) = + struct + type status = S.status + type obj = string * Obj.t + + let require1 = ref (fun _ -> assert false (* unknown data*)) + let already_registered = ref [] + + let register tag require = + assert (not (List.mem tag !already_registered)); + already_registered := tag :: !already_registered; + let old_require1 = !require1 in + require1 := + (fun (tag',data) as x -> + if tag=tag' then + require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term + else + old_require1 x); + (fun x -> tag,Obj.repr x) + + let serialize = serialize + + let require ~baseuri status = + includes := baseuri::!includes; + let dump = require0 ~baseuri in + List.fold_right !require1 dump status +end + +type sstatus = status + +module Serializer = + struct + include SerializerF(struct type status = sstatus end) + + let require ~baseuri status = + let rstatus = require ~baseuri (status : #status :> status) in + let status = status#set_coerc_db (rstatus#coerc_db) in + let status = status#set_uhint_db (rstatus#uhint_db) in + let status = status#set_timestamp (rstatus#timestamp) in + status + end + +class type g_dumpable_status = + object + inherit g_status + method dump: Serializer.obj list + end + +class dumpable_status = + object(self) + inherit status + val dump = ([] : Serializer.obj list) + method dump = dump + method set_dump v = {< dump = v >} + method set_dumpable_status : 'status. #g_dumpable_status as 'status -> 'self + = fun o -> (self#set_dump o#dump)#set_coercion_status o + end + + +let decompile ~baseuri = + let baseuris = get_deps baseuri in + List.iter (fun baseuri -> + remove_deps baseuri; + HExtlib.safe_remove (path_of_baseuri baseuri); + let basepath = path_of_baseuri ~no_suffix:true baseuri in + try + let od = Unix.opendir basepath in + let rec aux names = + try + let name = Unix.readdir od in + if name <> "." && name <> ".." then aux (name::names) else aux names + with + End_of_file -> names in + let names = List.map (fun name -> basepath ^ "/" ^ name) (aux []) in + Unix.closedir od; + List.iter Unix.unlink names; + HExtlib.rmdir_descend basepath; + set_global_aliases + (List.filter + (fun (_,_,NReference.Ref (nuri,_)) -> + Filename.dirname (NUri.string_of_uri nuri) <> NUri.string_of_uri baseuri + ) (get_global_aliases ())) + with + Unix.Unix_error _ -> () (* raised by Unix.opendir, we hope :-) *) + ) baseuris +;; + +LibraryClean.set_decompile_cb + (fun ~baseuri -> decompile ~baseuri:(NUri.uri_of_string baseuri));; + +let fetch_obj uri = + let obj = require0 ~baseuri:uri in + refresh_uri_in_obj obj +;; + +let resolve name = + try + HExtlib.filter_map + (fun (_,name',nref) -> if name'=name then Some nref else None) + (!local_aliases @ get_global_aliases ()) + with + Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name)) +;; + +let aliases_of uri = + HExtlib.filter_map + (fun (uri',_,nref) -> + if NUri.eq uri' uri then Some nref else None) !local_aliases +;; + +let add_obj status ((u,_,_,_,_) as obj) = + NCicEnvironment.check_and_add_obj obj; + storage := (`Obj (u,obj))::!storage; + let _,height,_,_,obj = obj in + let references = + match obj with + NCic.Constant (_,name,None,_,_) -> + [u,name,NReference.reference_of_spec u NReference.Decl] + | NCic.Constant (_,name,Some _,_,_) -> + [u,name,NReference.reference_of_spec u (NReference.Def height)] + | NCic.Fixpoint (is_ind,fl,_) -> + HExtlib.list_mapi + (fun (_,name,recno,_,_) i -> + if is_ind then + u,name,NReference.reference_of_spec u(NReference.Fix(i,recno,height)) + else + u,name,NReference.reference_of_spec u (NReference.CoFix i)) fl + | NCic.Inductive (inductive,leftno,il,_) -> + List.flatten + (HExtlib.list_mapi + (fun (_,iname,_,cl) i -> + HExtlib.list_mapi + (fun (_,cname,_) j-> + u,cname, + NReference.reference_of_spec u (NReference.Con (i,j+1,leftno)) + ) cl @ + [u,iname, + NReference.reference_of_spec u + (NReference.Ind (inductive,i,leftno))] + ) il) + in + local_aliases := references @ !local_aliases; + status#set_timestamp (!storage,!local_aliases,!cache,!includes) +;; + +let add_constraint status u1 u2 = + NCicEnvironment.add_lt_constraint u1 u2; + storage := (`Constr (u1,u2)) :: !storage; + status#set_timestamp (!storage,!local_aliases,!cache,!includes) +;; + +let get_obj u = + try + List.assq u + (HExtlib.filter_map + (function `Obj (u,o) -> Some (u,o) | _ -> None ) + !storage) + with Not_found -> + try fetch_obj u + with Sys_error _ -> + try NUri.UriMap.find u !cache + with Not_found -> + let ouri = NCic2OCic.ouri_of_nuri u in + try + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in + let l = OCic2NCic.convert_obj ouri o in + List.iter (fun (u,_,_,_,_ as o) -> cache:= NUri.UriMap.add u o !cache) l; + HExtlib.list_last l + with CicEnvironment.Object_not_found u -> + raise (NCicEnvironment.ObjectNotFound + (lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u)))) +;; + +let clear_cache () = cache := NUri.UriMap.empty;; + +NCicEnvironment.set_get_obj get_obj;; +NCicPp.set_get_obj get_obj;; diff --git a/helm/software/components/ng_library/nCicLibrary.mli b/helm/software/components/ng_library/nCicLibrary.mli new file mode 100644 index 000000000..e155aaf4a --- /dev/null +++ b/helm/software/components/ng_library/nCicLibrary.mli @@ -0,0 +1,82 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id$ *) + +exception LibraryOutOfSync of string Lazy.t + +type timestamp + +class type g_status = + object + method timestamp: timestamp + inherit NRstatus.g_status + end + +class status : + object ('self) + inherit g_status + method set_timestamp: timestamp -> 'self + method set_library_status: #g_status -> 'self + end + +(* it also checks it and add it to the environment *) +val add_obj: #status as 'status -> NCic.obj -> 'status +val add_constraint: + #status as 'status -> NCic.universe -> NCic.universe -> 'status +val aliases_of: NUri.uri -> NReference.reference list +val resolve: string -> NReference.reference list +(* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *) +val get_obj: NUri.uri -> NCic.obj (* changes the current timestamp *) + +val clear_cache : unit -> unit + +val time_travel: #status -> unit +val decompile: baseuri:NUri.uri -> unit + +module type SerializerT = + sig + type status + type obj + val register: + string -> + ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> + ('a -> obj) + val serialize: baseuri:NUri.uri -> obj list -> unit + val require: baseuri:NUri.uri -> status -> status + end + +val init: unit -> unit + +module Serializer: + sig + include SerializerT with type status = status + val require: baseuri:NUri.uri -> (#status as 'status) -> 'status + end + +class type g_dumpable_status = + object + inherit g_status + method dump: Serializer.obj list + end + +class dumpable_status : + object ('self) + inherit status + inherit g_dumpable_status + method set_dump: Serializer.obj list -> 'self + method set_dumpable_status: #g_dumpable_status -> 'self + end + +(* CSC: only required during old-to-NG phase, to be deleted *) +val refresh_uri: NUri.uri -> NUri.uri + +(* EOF *) diff --git a/helm/software/components/ng_library/rt.ml b/helm/software/components/ng_library/rt.ml new file mode 100644 index 000000000..997bc2e3c --- /dev/null +++ b/helm/software/components/ng_library/rt.ml @@ -0,0 +1,42 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id$ *) + +let _ = + Helm_registry.load_from "conf.xml"; + CicParser.impredicative_set := false; + let u = UriManager.uri_of_string Sys.argv.(1) in + let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph u in + prerr_endline "VECCHIO"; + prerr_endline (CicPp.ppobj o); + let l = OCic2NCic.convert_obj u o in + prerr_endline "OGGETTI:........................................."; + List.iter (fun o -> prerr_endline (NCicPp.ppobj o)) l; + prerr_endline "/OGGETTI:........................................."; + let objs = + List.flatten + (List.map NCic2OCic.convert_nobj l) in + List.iter + (fun (u,o) -> + prerr_endline ("round trip: " ^ UriManager.string_of_uri u); + prerr_endline (CicPp.ppobj o); + prerr_endline "tipo......."; + try CicTypeChecker.typecheck_obj u o + with + CicTypeChecker.TypeCheckerFailure s + | CicTypeChecker.AssertFailure s -> + prerr_endline (Lazy.force s) + | CicEnvironment.Object_not_found uri -> + prerr_endline + ("CicEnvironment: Object not found " ^ UriManager.string_of_uri uri)) + objs; +;; diff --git a/helm/software/components/ng_refiner/Makefile b/helm/software/components/ng_refiner/Makefile index 9e0959c0d..7ff8f5fd0 100644 --- a/helm/software/components/ng_refiner/Makefile +++ b/helm/software/components/ng_refiner/Makefile @@ -18,33 +18,6 @@ EXTRA_OBJECTS_TO_CLEAN = %.cmi: OCAMLOPTIONS += -w Ae %.cmx: OCAMLOPTIONS += -w Ae -all: rt check -%: %.ml $(PACKAGE).cma - $(OCAMLC) -package helm-$(PACKAGE) -linkpkg -o $@ $< -all.opt opt: rt.opt check.opt -%.opt: %.ml $(PACKAGE).cmxa - $(OCAMLOPT) -package helm-$(PACKAGE) -linkpkg -o $@ $< - -depend.dot: $(IMPLEMENTATION_FILES) $(INTERFACE_FILES) - ocamldoc -o depend.dot -rectypes -I ../extlib/ -I ../cic -I ../cic_proof_checking/ -I ../urimanager/ -I ../logger/ -I ../registry/ -I ../getter/ -I ../hmysql/ -I ../library/ -I ../metadata/ -dot nUri.ml nReference.ml nCic.ml nCicPp.ml nCicEnvironment.ml nCicSubstitution.ml nCicReduction.ml nCicTypeChecker.ml nCicUtils.ml nCicLibrary.ml - cat depend.dot | grep -v "^}$$" > /tmp/depend.dot && mv /tmp/depend.dot . - for i in `cat depend.dot | grep darkturquoise | cut -d '"' -f 2`; do j=`echo $$i | sed s/^N/n/g`; size=`cat $$j.ml | wc -l`; funs=`cat $$j.mli | grep "^val " | wc -l`; size=`expr $$size - 13`; echo "\"$$i\" [ label=\"$$i\\n$$size lines,\\n$$funs functions\"];"; done >> depend.dot - echo "}" >> depend.dot - cat depend.dot | grep -v "darkturquoise" > /tmp/depend.dot && mv /tmp/depend.dot . - cat depend.dot - tred < depend.dot > /tmp/depend.dot && mv /tmp/depend.dot . - cat depend.dot | grep -v "^}$$" > /tmp/depend.dot && mv /tmp/depend.dot . - echo " NCicEnvironment -> NCicTypeChecker;" >> depend.dot - cat depend.dot | grep -v "NCicEnvironment -> NCic;" > /tmp/depend.dot && mv /tmp/depend.dot . - echo "NCicLibrary [ style=dashed ];" >> depend.dot - echo "NCicPp [ style=dashed ];" >> depend.dot - echo "}" >> depend.dot - cat depend.dot | grep -v "rotate" > /tmp/depend.dot && mv /tmp/depend.dot . - -depend.png depend.eps: depend.dot - dot -Tpng > depend.png < depend.dot - dot -Tps > depend.eps < depend.dot - include ../../Makefile.defs include ../Makefile.common diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml index 68fdf4f50..9a6fd4ef2 100644 --- a/helm/software/components/ng_refiner/nRstatus.ml +++ b/helm/software/components/ng_refiner/nRstatus.ml @@ -11,46 +11,7 @@ (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *) -class type g_status = - object - inherit NCicCoercion.g_status - inherit NCicLibrary.g_status - end +class type g_status = NCicCoercion.status -class status = - object (self) - inherit NCicCoercion.status - inherit NCicLibrary.status - method set_rstatus : 'status. #g_status as 'status -> 'self - = fun o -> (self#set_coercion_status o)#set_library_status o - end +class status = NCicCoercion.status -type sstatus = status - -module Serializer = - struct - include NCicLibrary.Serializer(struct type status = sstatus end) - - let require ~baseuri status = - let rstatus = require ~baseuri (status : #status :> status) in - let status = status#set_coerc_db (rstatus#coerc_db) in - let status = status#set_uhint_db (rstatus#uhint_db) in - let status = status#set_timestamp (rstatus#timestamp) in - status - end - -class type g_dumpable_status = - object - inherit g_status - method dump: Serializer.obj list - end - -class dumpable_status = - object(self) - inherit status - val dump = ([] : Serializer.obj list) - method dump = dump - method set_dump v = {< dump = v >} - method set_dumpable_status : 'status. #g_dumpable_status as 'status -> 'self - = fun o -> (self#set_dump o#dump)#set_rstatus o - end diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli index 40974aac2..631e629e5 100644 --- a/helm/software/components/ng_refiner/nRstatus.mli +++ b/helm/software/components/ng_refiner/nRstatus.mli @@ -11,36 +11,7 @@ (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *) -class type g_status = - object - inherit NCicCoercion.g_status - inherit NCicLibrary.g_status - end +class type g_status = NCicCoercion.status -class status : - object ('self) - inherit NCicCoercion.status - inherit NCicLibrary.status - inherit g_status - method set_rstatus: #g_status -> 'self - end +class status : NCicCoercion.status -module Serializer: - sig - include NCicLibrary.Serializer with type status = status - val require: baseuri:NUri.uri -> (#status as 'status) -> 'status - end - -class type g_dumpable_status = - object - inherit g_status - method dump: Serializer.obj list - end - -class dumpable_status : - object ('self) - inherit status - inherit g_dumpable_status - method set_dump: Serializer.obj list -> 'self - method set_dumpable_status: #g_dumpable_status -> 'self - end diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index b6bba823f..e47b1b713 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -88,7 +88,7 @@ let save_moo grafite_status = GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname grafite_status#lstatus.LexiconEngine.lexicon_content_rev; - NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) + NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) grafite_status#dump | _ -> clean_current_baseuri grafite_status ;; diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index f9c9af359..ba6840ee5 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -251,7 +251,7 @@ let main () = in GrafiteMarshal.save_moo moo_fname moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; - NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump; + NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump; exit 0 end with diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 6d01fc460..0b8b58c0d 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -274,7 +274,7 @@ let compile atstart options fname = (* FG: we do not generate .moo when dumping .mma files *) GrafiteMarshal.save_moo moo_fname moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; - NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) + NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) grafite_status#dump end; let tm = Unix.gmtime elapsed in