From 622b14b04e2076d75c283363969dab7d28380bfb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Sep 2008 10:06:51 +0000 Subject: [PATCH] new directory for the newGeneration refiner --- .../components/METAS/meta.helm-ng_refiner.src | 5 + helm/software/components/ng_refiner/Makefile | 44 ++++ helm/software/components/ng_refiner/check.ml | 215 ++++++++++++++++++ helm/software/components/ng_refiner/rt.ml | 43 ++++ 4 files changed, 307 insertions(+) create mode 100644 helm/software/components/METAS/meta.helm-ng_refiner.src create mode 100644 helm/software/components/ng_refiner/Makefile create mode 100644 helm/software/components/ng_refiner/check.ml create mode 100644 helm/software/components/ng_refiner/rt.ml diff --git a/helm/software/components/METAS/meta.helm-ng_refiner.src b/helm/software/components/METAS/meta.helm-ng_refiner.src new file mode 100644 index 000000000..b866e9e56 --- /dev/null +++ b/helm/software/components/METAS/meta.helm-ng_refiner.src @@ -0,0 +1,5 @@ +requires="helm-ng_kernel" +version="0.0.1" +archive(byte)="ng_refiner.cma" +archive(native)="ng_refiner.cmxa" +linkopts="" diff --git a/helm/software/components/ng_refiner/Makefile b/helm/software/components/ng_refiner/Makefile new file mode 100644 index 000000000..a59a0a210 --- /dev/null +++ b/helm/software/components/ng_refiner/Makefile @@ -0,0 +1,44 @@ +PACKAGE = ng_refiner +PREDICATES = + +INTERFACE_FILES = \ + nRefiner.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 $@ $< + +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/check.ml b/helm/software/components/ng_refiner/check.ml new file mode 100644 index 000000000..c1ce42607 --- /dev/null +++ b/helm/software/components/ng_refiner/check.ml @@ -0,0 +1,215 @@ +(* + ||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 = false + +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 + [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")] + else + [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")] +;; +let mk_cprop n = + if n = 0 then + [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")] + else + [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^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; + NCicPp.set_ppterm NCicPp.trivial_pp_term; + 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 + 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_constraint true (mk_type a) (mk_type b); + NCicEnvironment.add_constraint true (mk_cprop a) (mk_cprop b); + NCicEnvironment.add_constraint true (mk_cprop a) (mk_type b); + NCicEnvironment.add_constraint true (mk_type a) (mk_cprop b); + NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a); + NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a); + aux tl + | [a] -> + NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a); + NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a); + | _ -> () + 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 + NCicTypeChecker.typecheck_obj o + with + | NCicTypeChecker.AssertFailure s + | NCicTypeChecker.TypeCheckerFailure s + | NCicEnvironment.ObjectNotFound s + | NCicEnvironment.BadConstraint s + | NCicEnvironment.BadDependency s as e -> + prerr_endline ("######### " ^ Lazy.force s); + if not ignore_exc then raise e + ) + 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; + NCicTypeChecker.typecheck_obj (NCicLibrary.get_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_refiner/rt.ml b/helm/software/components/ng_refiner/rt.ml new file mode 100644 index 000000000..3843d5a78 --- /dev/null +++ b/helm/software/components/ng_refiner/rt.ml @@ -0,0 +1,43 @@ +(* + ||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; + NCicPp.set_ppterm NCicPp.trivial_pp_term; + 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; +;; -- 2.39.2