]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_library/check.ml
dependencies between statuses simplified
[helm.git] / helm / software / components / ng_library / check.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 (* $Id$ *)
13
14 let debug = true
15 let ignore_exc = false
16 let rank_all_dependencies = false
17 let trust_environment = false
18 let print_object = true
19
20 let indent = ref 0;;
21
22 let load_graph, get_graph =
23  let oldg = ref CicUniv.empty_ugraph in
24   (function uri -> 
25     let _,g = CicEnvironment.get_obj !oldg uri in
26      oldg := g),
27   (function _ -> !oldg)
28 ;;
29
30 let logger =
31     let do_indent () = String.make !indent ' ' in  
32     (function 
33       | `Start_type_checking s ->
34           if debug then
35            prerr_endline (do_indent () ^ "Start: " ^ NUri.string_of_uri s); 
36           incr indent
37       | `Type_checking_completed s ->
38           decr indent;
39           if debug then
40            prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s)
41       | `Type_checking_interrupted s ->
42           decr indent;
43           if debug then
44            prerr_endline (do_indent () ^ "Break: " ^ NUri.string_of_uri s)
45       | `Type_checking_failed s ->
46           decr indent;
47           if debug then
48            prerr_endline (do_indent () ^ "Fail: " ^ NUri.string_of_uri s)
49       | `Trust_obj s ->
50           if debug then
51            prerr_endline (do_indent () ^ "Trust: " ^ NUri.string_of_uri s))
52 ;;
53
54 let mk_type n = 
55   if n = 0 then
56      [`Type, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
57   else
58      [`Type, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
59 ;;
60 let mk_cprop n = 
61   if n = 0 then 
62     [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
63   else
64     [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
65 ;;
66
67
68 let _ =
69   let do_old_logging = ref true in
70   HelmLogger.register_log_callback
71    (fun ?append_NL html_msg ->
72      if !do_old_logging then
73       prerr_endline (HelmLogger.string_of_html_msg html_msg));
74   CicParser.impredicative_set := false;
75   NCicTypeChecker.set_logger logger;
76   Helm_registry.load_from "conf.xml";
77   let alluris = 
78     try
79       let s = Sys.argv.(1) in
80       if s = "-alluris" then
81        begin
82         let uri_re = Str.regexp ".*\\(ind\\|con\\)$" in
83         let uris = Http_getter.getalluris () in
84         let alluris = List.filter (fun u -> Str.string_match uri_re u 0) uris in
85         let oc = open_out "alluris.txt" in
86         List.iter (fun s -> output_string oc (s^"\n")) alluris;
87         close_out oc; 
88         []
89        end
90       else [s]
91     with Invalid_argument _ -> 
92       let r = ref [] in
93       let ic = open_in "alluris.txt" in
94       try while true do r := input_line ic :: !r; done; []
95       with _ -> List.rev !r
96   in
97   let alluris = 
98     HExtlib.filter_map
99       (fun u -> try Some (UriManager.uri_of_string u) with _ -> None) alluris 
100   in
101   (* brutal *)
102   prerr_endline "computing graphs to load...";
103   let roots_alluris = 
104    if not rank_all_dependencies then
105     alluris
106    else (
107     let dbd = HSql.quick_connect (LibraryDb.parse_dbd_conf ()) in
108      MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
109     let uniq l = 
110      HExtlib.list_uniq (List.sort UriManager.compare l) in
111     let who_uses u = 
112      uniq (List.map (fun (uri,_) -> UriManager.strip_xpointer uri)
113       (MetadataDeps.inverse_deps ~dbd u)) in
114     let rec fix acc l = 
115      let acc, todo = 
116       List.fold_left (fun (acc,todo) x ->
117         let w = who_uses x in
118         if w = [] then (x::acc,todo) else (acc,uniq (todo@w)))
119       (acc,[]) l
120      in
121      if todo = [] then uniq acc else fix acc todo
122     in
123      fix [] alluris)
124   in
125   prerr_endline "generating Coq graphs...";
126   CicEnvironment.set_trust (fun _ -> trust_environment);
127   List.iter
128    (fun u ->
129      prerr_endline (" - " ^ UriManager.string_of_uri u);
130      try
131        ignore(CicTypeChecker.typecheck u);
132      with 
133      | CicTypeChecker.AssertFailure s
134      | CicTypeChecker.TypeCheckerFailure s ->
135         prerr_endline (Lazy.force s);
136         assert false
137     ) roots_alluris;
138   prerr_endline "loading...";
139   List.iter 
140     (fun u -> 
141        prerr_endline ("  - "^UriManager.string_of_uri u);
142        try load_graph u with exn -> ())
143     roots_alluris;
144   prerr_endline "finished....";
145   let lll, uuu =(CicUniv.do_rank (get_graph ())) in
146   CicUniv.print_ugraph (get_graph ());
147   let lll = List.sort compare lll in
148   List.iter (fun k -> 
149     prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int (CicUniv.get_rank k))) uuu;
150   let _ = 
151     try
152     let rec aux = function
153       | a::(b::_ as tl) ->
154          NCicEnvironment.add_lt_constraint (mk_type a) (mk_type b);
155          NCicEnvironment.add_lt_constraint (mk_type a) (mk_cprop b);
156          aux tl
157       | _ -> ()
158     in
159        aux lll
160     with NCicEnvironment.BadConstraint s as e ->
161       prerr_endline (Lazy.force s); raise e
162   in
163   prerr_endline "ranked....";
164   prerr_endline (NCicEnvironment.pp_constraints ());
165   HExtlib.profiling_enabled := false;
166   List.iter (fun uu ->
167     let uu= OCic2NCic.nuri_of_ouri uu in
168     indent := 0;
169     let o = NCicLibrary.get_obj uu in
170     if print_object then prerr_endline (NCicPp.ppobj o); 
171     try 
172       NCicEnvironment.check_and_add_obj o
173     with 
174     exn ->
175       let rec aux = function
176        | NCicTypeChecker.AssertFailure s 
177        | NCicTypeChecker.TypeCheckerFailure s
178        | NCicEnvironment.ObjectNotFound s
179        | NCicEnvironment.BadConstraint s as e-> 
180           prerr_endline ("######### " ^ Lazy.force s);
181           if not ignore_exc then raise e
182        | NCicEnvironment.BadDependency (s,x) as e -> 
183           prerr_endline ("######### " ^ Lazy.force s);
184           aux x;
185           if not ignore_exc then raise e
186        | e -> raise e
187       in
188        aux exn
189     )
190     alluris;
191   NCicEnvironment.invalidate ();
192   Gc.compact ();
193   HExtlib.profiling_enabled := true;
194   NCicTypeChecker.set_logger (fun _ -> ());
195   do_old_logging := false;
196   prerr_endline "typechecking, first with the new and then with the old kernel";
197   let prima = Unix.gettimeofday () in
198   List.iter 
199     (fun u ->
200       let u= OCic2NCic.nuri_of_ouri u in
201       indent := 0;
202       ignore (NCicEnvironment.get_checked_obj u))
203     alluris;
204   let dopo = Unix.gettimeofday () in
205   Gc.compact ();
206   let dopo2 = Unix.gettimeofday () in
207   Printf.eprintf "NEW typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -.  dopo);
208   CicEnvironment.invalidate ();
209   Gc.compact ();
210   let prima = Unix.gettimeofday () in
211   List.iter (fun u -> ignore (CicTypeChecker.typecheck u)) alluris;
212   let dopo = Unix.gettimeofday () in
213   Gc.compact ();
214   let dopo2 = Unix.gettimeofday () in
215   Printf.eprintf "OLD typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -. dopo)
216 ;;