X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaEngine.ml;h=c1c1cd9078a52cd86c98ea96e4a01ebaa756224b;hb=045c74915022181e288d9a950cc485437b08d002;hp=d139ade6dfc41f9ade43ccc69e79b9cdf704c8d1;hpb=6576f1ca2692807a74122122eab132f7c983d6bb;p=helm.git

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index d139ade6d..c1c1cd907 100644
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -71,11 +71,20 @@ let cut prefix s =
   String.sub s lenp (lens-lenp)
 ;;
 
-let print_string =
+let print_string = 
  let indent = ref 0 in
- let print_string s = print_string (String.make !indent ' ' ^ s) in
- fun enter s ->
-  if enter then (print_string s; incr indent) else (decr indent; print_string s)
+ let print_string ~right_justify s =
+  let ss =
+   match right_justify with
+      None -> ""
+    | Some (ss,len_ss) ->
+       let i = 80 - !indent - len_ss - String.length s in
+       if i > 0 then String.make i ' ' ^ ss else ss
+  in
+   assert (!indent >=0);
+   print_string (String.make !indent ' ' ^ s ^ ss) in
+ fun enter ?right_justify s ->
+  if enter then (print_string ~right_justify s; incr indent) else (decr indent; print_string ~right_justify s)
 ;;
 
 let pp_times ss fname rc big_bang big_bang_u big_bang_s = 
@@ -85,8 +94,8 @@ let pp_times ss fname rc big_bang big_bang_u big_bang_s =
     let u = u -. big_bang_u in
     let s = s -. big_bang_s in
     let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
-    let rc,rcascii = 
-      if rc then "OK","Ok" else "FAIL","Fail" in
+    let rc = 
+      if rc then "OK" else "FAIL" in
     let times = 
       let fmt t = 
         let seconds = int_of_float t in
@@ -97,38 +106,25 @@ let pp_times ss fname rc big_bang big_bang_u big_bang_s =
       in
       Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s)
     in
-    let s = Printf.sprintf "%-4s %s %s\n" rc times extra in
-    print_string false (ss ^ s);
+    let s = Printf.sprintf "%-14s %s %s\n" rc times extra in
+    print_string false ~right_justify:(s,31) ss;
     flush stdout;
     HLog.message ("Compilation of "^Filename.basename fname^": "^rc)
 ;;
 
-let activate_extraction baseuri fname =
-  ()
-  (* MATITA 1.0
- if Helm_registry.get_bool "matita.extract" then
-  let mangled_baseuri =
-   let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in
-     let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in
-      String.uncapitalize baseuri in
-  let f =
-    open_out
-     (Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in
-   LibrarySync.add_object_declaration_hook
-    (fun ~add_obj ~add_coercion _ obj ->
-      output_string f (CicExportation.ppobj baseuri obj);
-      flush f; []);
-      *)
-;;
-
-
 let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
  let baseuri = status#baseuri in
  let new_aliases,new_status =
   GrafiteDisambiguate.eval_with_new_aliases status
    (fun status ->
+   let time0 = Unix.gettimeofday () in
+   let status =
      GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
-      (text,prefix_len,ast)) in
+      (text,prefix_len,ast) in
+   let time1 = Unix.gettimeofday () in
+   HLog.debug ("... grafite_engine done in " ^ string_of_float (time1 -. time0) ^ "s");
+   status
+   ) in
  let _,intermediate_states = 
   List.fold_left
    (fun (status,acc) (k,value) -> 
@@ -222,7 +218,8 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status
         let str =
          match ast with
             (GrafiteAst.Executable
-              (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,_)))) ->
+              (_,GrafiteAst.NCommand
+                (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
               GrafiteParser.parsable_statement status
                (GrafiteParser.strm_of_parsable str)
           | _ -> str
@@ -242,9 +239,17 @@ and compile ~compiling ~asserted ~include_paths fname =
   let root,baseuri,fname,_tgt = 
     Librarian.baseuri_of_script ~include_paths fname in
   if Http_getter_storage.is_read_only baseuri then assert false;
-  activate_extraction baseuri fname ;
   (* MATITA 1.0: debbo fare time_travel sulla ng_library? *)
   let status = new status baseuri in
+  (*CSC: bad, one imperative bit is still there!
+         to be moved into functional status *)
+  NCicMetaSubst.pushmaxmeta ();
+  let ocamldirname = Filename.dirname fname in
+  let ocamlfname = Filename.chop_extension (Filename.basename fname) in
+  let status,ocamlfname =
+   Common.modname_of_filename status false ocamlfname in
+  let ocamlfname = ocamldirname ^ "/" ^ ocamlfname ^ ".ml" in
+  let status = OcamlExtraction.open_file status ~baseuri ocamlfname in
   let big_bang = Unix.gettimeofday () in
   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = 
     Unix.times () 
@@ -254,7 +259,7 @@ and compile ~compiling ~asserted ~include_paths fname =
    let rex = Str.regexp ".*opt$" in
    if Str.string_match rex Sys.argv.(0) 0 then "matitac.opt"
    else "matitac" in
-  let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in
+  let s = Printf.sprintf "%s %s" cc (cut (root^"/") fname) in
   try
     (* cleanup of previously compiled objects *)
     if (not (Http_getter_storage.is_empty ~local:true baseuri))
@@ -286,6 +291,7 @@ and compile ~compiling ~asserted ~include_paths fname =
     in
     let asserted, status =
      eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
+    let status = OcamlExtraction.close_file status in
     let elapsed = Unix.time () -. time in
      (if Helm_registry.get_bool "matita.moo" then begin
        GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
@@ -302,17 +308,23 @@ and compile ~compiling ~asserted ~include_paths fname =
      HLog.message 
        (sprintf "execution of %s completed in %s." fname (hou^min^sec));
      pp_times s fname true big_bang big_bang_u big_bang_s;
-     asserted
+     (*CSC: bad, one imperative bit is still there!
+            to be moved into functional status *)
+     NCicMetaSubst.pushmaxmeta ();
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
      LexiconSync.time_travel 
        ~present:lexicon_status ~past:initial_lexicon_status;
-*))
+*)
+     asserted)
   with 
   (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
   | exn when not matita_debug ->
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
        LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
  *       *)
+      (*CSC: bad, one imperative bit is still there!
+             to be moved into functional status *)
+      NCicMetaSubst.pushmaxmeta ();
       pp_times s fname false big_bang big_bang_u big_bang_s;
       clean_exit baseuri exn
 
@@ -348,10 +360,13 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
         let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
         let asserted,children_bad =
          List.fold_left
-          (fun (asserted,b) mapath ->
-            let asserted,b1 =
-              assert_ng ~already_included ~compiling ~asserted ~include_paths
-               mapath
+          (fun (asserted,b) mapath -> 
+	    let asserted,b1 =
+              try 
+	       assert_ng ~already_included ~compiling ~asserted ~include_paths
+                mapath
+	      with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+	        asserted, true 
             in
              asserted, b || b1
               || let _,baseuri,_,_ =