]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/matitaEngine.ml
Merge branch 'declarative' into matita-lablgtk3
[helm.git] / matita / matita / matitaEngine.ml
index 2963e71c45e2cf5c8f4312b9a7c58d48f9ada72e..fea7161c157fbe7a015383d1a2a35252b40434a4 100644 (file)
@@ -1,14 +1,14 @@
 (* Copyright (C) 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
  * 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/
- *)
+*)
 
 (* $Id$ *)
 
+module G = GrafiteAst
 open Printf
 
 class status baseuri =
- object
-  inherit GrafiteTypes.status baseuri
-  inherit ApplyTransformation.status
- end
 object
+    inherit GrafiteTypes.status baseuri
+    inherit ApplyTransformation.status
 end
 
 exception TryingToAdd of string Lazy.t
 exception EnrichedWithStatus of exn * status
@@ -44,16 +45,105 @@ let debug_print = if debug then prerr_endline else ignore ;;
 
 let slash_n_RE = Pcre.regexp "\\n" ;;
 
-let pp_ast_statement status stm =
-  let stm = GrafiteAstPp.pp_statement status stm
-    ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+let first_line = ref true ;;
+
+let cases_or_induction_context stack =
+    match stack with
+     [] -> false
+    | (_g,_t,_k,_tag,p)::_tl -> try
+                            let s = List.assoc "context" p in
+                            s = "cases" || s = "induction"
+                           with
+                            Not_found -> false
+;;
+
+let has_focused_goal stack =
+    match stack with
+     [] -> false
+    | (g,_t,_k,_tag,_p)::_tl -> (List.length g) > 0
+;;
+
+let get_indentation status _statement =
+  let base_ind =
+    match status#stack with
+      [] -> 0
+    | s -> List.length(s) * 2
   in
-  let stm = Pcre.replace ~rex:slash_n_RE stm in
-  let stm =
+    if cases_or_induction_context status#stack then
+      (
+        if has_focused_goal status#stack then
+            base_ind + 2
+        else
+            base_ind
+      )
+    else
+      base_ind
+;;
+
+let pp_ind s n =
+  let rec aux s n =
+    match n with
+      0 -> s
+    | n -> " " ^ (aux s (n-1))
+  in
+    aux s n
+
+let write_ast_to_file status fname statement =
+  let indentation = get_indentation status statement in
+  let str = match statement with
+      G.Comment _ -> GrafiteAstPp.pp_statement status statement
+                       ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+    | G.Executable (_,code) ->
+      (
+        match code with
+          G.NTactic _ -> GrafiteAstPp.pp_statement status statement
+                           ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+        | G.NCommand (_,cmd) ->
+          (
+              match cmd with
+                | G.NObj (_,obj,_) ->
+                        (
+                        match obj with
+                            NotationPt.Theorem _ -> "\n" ^ GrafiteAstPp.pp_statement status statement
+                                   ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+                        |   _ -> ""
+                        )
+                | G.NQed _ -> GrafiteAstPp.pp_statement status statement
+                                   ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+                | _ -> ""
+          )
+        | _ -> ""
+      )
+  in
+    if str <> "" then
+      (
+        let s = pp_ind str indentation in
+        let flaglist = if !first_line = false then [Open_wronly; Open_append; Open_creat]
+          else (first_line := false; [Open_wronly; Open_trunc; Open_creat])
+        in
+        let out_channel =
+          Stdlib.open_out_gen flaglist 0o0644 fname in
+        let _ = Stdlib.output_string out_channel ((if str.[0] <> '\n' then s else str) ^ "\n") in
+        let _ = Stdlib.close_out out_channel in
+        str
+      )
+    else
+      str
+;;
+
+let pp_ast_statement status stm ~fname =
+  let stm = write_ast_to_file status (fname ^ ".parsed.ma") stm in
+  if stm <> "" then
+  (
+    let stm = Pcre.replace ~rex:slash_n_RE stm in
+    let stm =
       if String.length stm > 50 then String.sub stm 0 50 ^ " ..."
       else stm
-  in
+    in
     HLog.debug ("Executing: ``" ^ stm ^ "''")
+  )
+  else
+    HLog.debug ("Executing: `` Unprintable statement ''")
 ;;
 
 let clean_exit baseuri exn =
@@ -61,7 +151,7 @@ let clean_exit baseuri exn =
   raise (FailureCompiling (baseuri,exn))
 ;;
 
-let cut prefix s = 
+let cut prefix s =
   let lenp = String.length prefix in
   let lens = String.length s in
   assert (lens > lenp);
@@ -69,33 +159,33 @@ let cut prefix s =
   String.sub s lenp (lens-lenp)
 ;;
 
-let print_string = 
- let indent = ref 0 in
- 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 print_string =
 let indent = ref 0 in
 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 = 
+let pp_times ss fname rc big_bang big_bang_u big_bang_s =
   if not (Helm_registry.get_bool "matita.verbose") then
     let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
     let r = Unix.gettimeofday () -. big_bang in
     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 = 
+    let rc =
       if rc then "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" in
-    let times = 
-      let fmt t = 
+    let times =
+      let fmt t =
         let seconds = int_of_float t in
         let cents = int_of_float ((t -. floor t) *. 100.0) in
         let minutes = seconds / 60 in
@@ -111,51 +201,51 @@ let pp_times ss fname rc big_bang big_bang_u big_bang_s =
 ;;
 
 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
-   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) -> 
-     let v = GrafiteAst.description_of_alias value in
-     let b =
-      try
-       let NReference.Ref (uri,_) = NReference.reference_of_string v in
-        NUri.baseuri_of_uri uri = baseuri
-      with
-       NReference.IllFormedReference _ ->
-        false (* v is a description, not a URI *)
-     in
-      if b then 
-       status,acc
-      else
-       let status =
-        GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false
-         GrafiteAst.WithPreferences [k,value]
-       in
-        status, (status ,Some (k,value))::acc
-   ) (status,[]) new_aliases (* WARNING: this must be the old status! *)
- in
 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
+         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) ->
+         let v = GrafiteAst.description_of_alias value in
+         let b =
+           try
+             let NReference.Ref (uri,_) = NReference.reference_of_string v in
+             NUri.baseuri_of_uri uri = baseuri
+           with
+             NReference.IllFormedReference _ ->
+             false (* v is a description, not a URI *)
+         in
+         if b then
+           status,acc
+         else
+           let status =
+             GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false
+               GrafiteAst.WithPreferences [k,value]
+           in
+           status, (status ,Some (k,value))::acc
+      ) (status,[]) new_aliases (* WARNING: this must be the old status! *)
 in
   (new_status,None)::intermediate_states
 ;;
 
 let baseuri_of_script ~include_paths fname =
- try Librarian.baseuri_of_script ~include_paths fname
- with
-   Librarian.NoRootFor _ -> 
 try Librarian.baseuri_of_script ~include_paths fname
 with
+    Librarian.NoRootFor _ ->
     HLog.error ("The included file '"^fname^"' has no root file,");
     HLog.error "please create it.";
     raise (Failure ("No root file for "^fname))
-  | Librarian.FileNotFound _ -> 
+  | Librarian.FileNotFound _ ->
     raise (Failure ("File not found: "^fname))
 ;;
 
@@ -173,68 +263,68 @@ let read_include_paths ~include_paths:_ file =
    in
    let rc = root :: includes in
     List.iter (HLog.debug) rc; rc
- with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
-  []
 with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+    []
 ;;
 
-let rec get_ast status ~compiling ~asserted ~include_paths strm = 
+let rec get_ast status ~compiling ~asserted ~include_paths strm =
   match GrafiteParser.parse_statement status strm with
-     (GrafiteAst.Executable
+    (GrafiteAst.Executable
        (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
-     ->
-       let already_included = NCicLibrary.get_transitively_included status in
-       let asserted,_ =
-        assert_ng ~already_included ~compiling ~asserted ~include_paths
-         mafilename
-       in
-        asserted,cmd
-   | cmd -> asserted,cmd
+    ->
+    let already_included = NCicLibrary.get_transitively_included status in
+    let asserted,_ =
+      assert_ng ~already_included ~compiling ~asserted ~include_paths
+        mafilename
+    in
+    asserted,cmd
+  | cmd -> asserted,cmd
 
 and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb =
- let matita_debug = Helm_registry.get_bool "matita.debug" in
- let rec loop asserted status str =
-  let asserted,stop,status,str = 
-   try
-     let cont =
-       try Some (get_ast status ~compiling ~asserted ~include_paths str)
-       with End_of_file -> None in
-     match cont with
-     | None -> asserted, true, status, str
-     | Some (asserted,ast) ->
-        cb status ast;
-        let new_statuses =
-          eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
-        let status =
-         match new_statuses with
-            [s,None] -> s
-          | _::(_,Some (_,value))::_ ->
-                raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
-          | _ -> assert false in
-        (* CSC: complex patch to re-build the lexer since the tokens may
-           have changed. Note: this way we loose look-ahead tokens.
-           Hence the "include" command must be terminated (no look-ahead) *)
-        let str =
-         match ast with
-            (GrafiteAst.Executable
-              (_,GrafiteAst.NCommand
-                (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
 let matita_debug = Helm_registry.get_bool "matita.debug" in
 let rec loop asserted status str =
+    let asserted,stop,status,str =
+      try
+        let cont =
+          try Some (get_ast status ~compiling ~asserted ~include_paths str)
+          with End_of_file -> None in
+        match cont with
+        | None -> asserted, true, status, str
+        | Some (asserted,ast) ->
+          cb status ast;
+          let new_statuses =
+            eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
+          let status =
+            match new_statuses with
+              [s,None] -> s
+            | _::(_,Some (_,value))::_ ->
+              raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
+            | _ -> assert false in
+          (* CSC: complex patch to re-build the lexer since the tokens may
+             have changed. Note: this way we loose look-ahead tokens.
+             Hence the "include" command must be terminated (no look-ahead) *)
+          let str =
+            match ast with
+              (GrafiteAst.Executable
+                 (_,GrafiteAst.NCommand
+                    (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
               GrafiteParser.parsable_statement status
-               (GrafiteParser.strm_of_parsable str)
-          | _ -> str
-        in
-         asserted, false, status, str
-   with exn when not matita_debug ->
-     raise (EnrichedWithStatus (exn, status))
+                (GrafiteParser.strm_of_parsable str)
+            | _ -> str
+          in
+          asserted, false, status, str
+      with exn when not matita_debug ->
+        raise (EnrichedWithStatus (exn, status))
+    in
+    if stop then asserted,status else loop asserted status str
   in
-  if stop then asserted,status else loop asserted status str
- in
   loop asserted status str
 
 and compile ~compiling ~asserted ~include_paths fname =
   if List.mem fname compiling then raise (CircularDependency fname);
   let compiling = fname::compiling in
   let matita_debug = Helm_registry.get_bool "matita.debug" in
-  let root,baseuri,fname,_tgt = 
+  let root,baseuri,fname,_tgt =
     Librarian.baseuri_of_script ~include_paths fname in
   if Http_getter_storage.is_read_only baseuri then assert false;
   (* MATITA 1.0: debbo fare time_travel sulla ng_library? *)
@@ -245,154 +335,154 @@ and compile ~compiling ~asserted ~include_paths fname =
   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
+    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 () 
+  let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} =
+    Unix.times ()
   in
   let time = Unix.time () in
-  let cc = 
-   let rex = Str.regexp ".*opt$" in
-   if Str.string_match rex Sys.argv.(0) 0 then "matitac.opt"
-   else "matitac" in
+  let cc =
+    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 %s" cc (cut (root^"/") fname) in
   try
     (* cleanup of previously compiled objects *)
     if (not (Http_getter_storage.is_empty ~local:true baseuri))
-      then begin
+    then begin
       HLog.message ("baseuri " ^ baseuri ^ " is not empty");
       HLog.message ("cleaning baseuri " ^ baseuri);
       LibraryClean.clean_baseuris [baseuri];
     end;
     HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri);
     if not (Helm_registry.get_bool "matita.verbose") then
-     (print_string true (s ^ "\n"); flush stdout);
+      (print_string true (s ^ "\n"); flush stdout);
     (* we dalay this error check until we print 'matitac file ' *)
     assert (Http_getter_storage.is_empty ~local:true baseuri);
     (* create dir for XML files *)
     if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
-              ~default:false) 
+              ~default:false)
     then
-      HExtlib.mkdir 
-        (Filename.dirname 
-          (Http_getter.filename ~local:true ~writable:true (baseuri ^
-          "foo.con")));
+      HExtlib.mkdir
+        (Filename.dirname
+           (Http_getter.filename ~local:true ~writable:true (baseuri ^
+                                                             "foo.con")));
     let buf =
-     GrafiteParser.parsable_statement status
-      (Ulexing.from_utf8_channel (open_in fname))
+      GrafiteParser.parsable_statement status
+        (Ulexing.from_utf8_channel (open_in fname))
     in
     let print_cb =
-      if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
-      else pp_ast_statement
+      if not (Helm_registry.get_bool "matita.verbose") then fun _ _ -> ()
+      else pp_ast_statement ~fname
     in
     let asserted, status =
-     eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
+      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)
-        status
-     end;
+    (if Helm_registry.get_bool "matita.moo" then begin
+        GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+          status
+      end;
      let tm = Unix.gmtime elapsed in
      let sec = string_of_int tm.Unix.tm_sec ^ "''" in
-     let min = 
-       if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min^"' ") else "" 
+     let min =
+       if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min^"' ") else ""
      in
-     let hou = 
+     let hou =
        if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour^"h ") else ""
      in
-     HLog.message 
+     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;
      (*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;
-*)
+     (* MATITA 1.0: debbo fare time_travel sulla ng_library?
+          LexiconSync.time_travel
+            ~present:lexicon_status ~past:initial_lexicon_status;
+     *)
      asserted)
-  with 
+  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
+    (* 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
 
 and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
- let root,baseuri,fullmapath,_ =
-  Librarian.baseuri_of_script ~include_paths mapath in
- if List.mem fullmapath asserted then asserted,false
- else
-  begin
-   let include_paths =
-    let includes =
-     try
-      Str.split (Str.regexp " ") 
-       (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
-     with Not_found -> []
-    in
-     root::includes @
-      Helm_registry.get_list Helm_registry.string "matita.includes" in
-   let baseuri = NUri.uri_of_string baseuri in
-   let ngtime_of baseuri =
-    let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
-    try
-     Some (Unix.stat ngpath).Unix.st_mtime
-    with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
-   let matime =
-    try (Unix.stat fullmapath).Unix.st_mtime
-    with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false
-   in
-   let ngtime = ngtime_of baseuri in
-   let asserted,to_be_compiled =
-    match ngtime with
-       Some ngtime ->
-        let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
-        let asserted,children_bad =
-         List.fold_left
-          (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,_,_ =
-                   (*CSC: bug here? include_paths should be empty and
-                          mapath should be absolute *)
-                   Librarian.baseuri_of_script ~include_paths mapath in
-                 let baseuri = NUri.uri_of_string baseuri in
-                  (match ngtime_of baseuri with
-                      Some child_ngtime -> child_ngtime > ngtime
-                    | None -> assert false)
-          ) (asserted,false) preamble
+  let root,baseuri,fullmapath,_ =
+    Librarian.baseuri_of_script ~include_paths mapath in
+  if List.mem fullmapath asserted then asserted,false
+  else
+    begin
+      let include_paths =
+        let includes =
+          try
+            Str.split (Str.regexp " ")
+              (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+          with Not_found -> []
         in
-         asserted, children_bad || matime > ngtime
-     | None -> asserted,true
-   in
-    if not to_be_compiled then fullmapath::asserted,false
-    else
-     if List.mem baseuri already_included then
-       (* maybe recompiling it I would get the same... *)
-       raise (AlreadyLoaded (lazy mapath))
-     else
-      let asserted = compile ~compiling ~asserted ~include_paths fullmapath in
-       fullmapath::asserted,true
-  end
+        root::includes @
+        Helm_registry.get_list Helm_registry.string "matita.includes" in
+      let baseuri = NUri.uri_of_string baseuri in
+      let ngtime_of baseuri =
+        let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
+        try
+          Some (Unix.stat ngpath).Unix.st_mtime
+        with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
+      let matime =
+        try (Unix.stat fullmapath).Unix.st_mtime
+        with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false
+      in
+      let ngtime = ngtime_of baseuri in
+      let asserted,to_be_compiled =
+        match ngtime with
+          Some ngtime ->
+          let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
+          let asserted,children_bad =
+            List.fold_left
+              (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,_,_ =
+                                (*CSC: bug here? include_paths should be empty and
+                                       mapath should be absolute *)
+                                Librarian.baseuri_of_script ~include_paths mapath in
+                           let baseuri = NUri.uri_of_string baseuri in
+                           (match ngtime_of baseuri with
+                              Some child_ngtime -> child_ngtime > ngtime
+                            | None -> assert false)
+              ) (asserted,false) preamble
+          in
+          asserted, children_bad || matime > ngtime
+        | None -> asserted,true
+      in
+      if not to_be_compiled then fullmapath::asserted,false
+      else
+      if List.mem baseuri already_included then
+        (* maybe recompiling it I would get the same... *)
+        raise (AlreadyLoaded (lazy mapath))
+      else
+        let asserted = compile ~compiling ~asserted ~include_paths fullmapath in
+        fullmapath::asserted,true
+    end
 ;;
 
 let assert_ng ~include_paths mapath =
- snd (assert_ng ~include_paths ~already_included:[] ~compiling:[] ~asserted:[]
-  mapath)
 snd (assert_ng ~include_paths ~already_included:[] ~compiling:[] ~asserted:[]
+         mapath)
 let get_ast status ~include_paths strm =
- snd (get_ast status ~compiling:[] ~asserted:[] ~include_paths strm)
 snd (get_ast status ~compiling:[] ~asserted:[] ~include_paths strm)