exception EnrichedWithStatus of exn * GrafiteTypes.status
exception AlreadyLoaded of string Lazy.t
exception FailureCompiling of string * exn
+exception CircularDependency of string
let debug = false ;;
let debug_print = if debug then prerr_endline else ignore ;;
String.sub s lenp (lens-lenp)
;;
-(*MATITA 1.0 assert false;; (* chiamare enrich_include_paths *)*)
-let enrich_include_paths ~include_paths =
- include_paths @ Helm_registry.get_list Helm_registry.string "matita.includes"
-;;
-
let activate_extraction baseuri fname =
()
(* MATITA 1.0
(new_status,None)::intermediate_states
;;
-let rec get_ast status ~include_paths strm =
+let rec get_ast status ~compiling ~include_paths strm =
match GrafiteParser.parse_statement status strm with
(GrafiteAst.Executable
(_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
HLog.error "please create it.";
raise (Failure ("No root file for "^mafilename))
in
- ignore (assert_ng ~include_paths ~root tgt);
+ ignore (assert_ng ~compiling ~include_paths ~root tgt);
cmd
| cmd -> cmd
-and eval_from_stream ~include_paths ?do_heavy_checks status str cb =
+and eval_from_stream ~compiling ~include_paths ?do_heavy_checks status str cb =
let matita_debug = Helm_registry.get_bool "matita.debug" in
let rec loop status =
let stop,status =
try
let cont =
- try Some (get_ast status ~include_paths str)
+ try Some (get_ast status ~compiling ~include_paths str)
with End_of_file -> None in
match cont with
| None -> true, status
in
loop status
-and compile ~include_paths fname =
+and compile ~compiling ~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 =
Librarian.baseuri_of_script ~include_paths fname in
(Filename.dirname
(Http_getter.filename ~local:true ~writable:true (baseuri ^
"foo.con")));
- let buf = Ulexing.from_utf8_channel (open_in fname) in
+ let grammar = CicNotationParser.level2_ast_grammar grafite_status in
+ let buf =
+ Grammar.parsable grammar
+ (Obj.magic (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
in
let grafite_status =
- eval_from_stream ~include_paths grafite_status buf print_cb in
+ eval_from_stream ~compiling ~include_paths grafite_status buf print_cb 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)
(* BIG BUG: if a file recursively includes itself, anything can happen,
* from divergence to inclusion of an old copy of itself *)
-and assert_ng ~include_paths ~root mapath =
- let root',baseuri,_,_ = Librarian.baseuri_of_script ~include_paths mapath in
+and assert_ng ~compiling ~include_paths ~root mapath =
+ let root',baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
assert (root=root');
let baseuri = NUri.uri_of_string baseuri in
let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
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 mapath).Unix.st_mtime
- with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = mapath -> assert false
+ try (Unix.stat fullmapath).Unix.st_mtime
+ with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false
in
let to_be_compiled =
match ngtime with
Some ngtime ->
let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
- let children_bad= List.exists (assert_ng ~include_paths ~root) preamble in
+ let children_bad =
+ List.exists (assert_ng ~compiling ~include_paths ~root) preamble
+ in
children_bad || matime > ngtime
| None -> true
in
(* maybe recompiling it I would get the same... *)
raise (AlreadyLoaded (lazy mapath))
else
- (compile ~include_paths mapath; true)
+ (compile ~compiling ~include_paths fullmapath; true)
+;;
+
+let assert_ng = assert_ng ~compiling:[]
+let get_ast = get_ast ~compiling:[]