open GrafiteTypes
open Printf
-class status baseuri =
+class status uid baseuri =
object
- inherit GrafiteTypes.status baseuri
- inherit ApplyTransformation.status
+ inherit GrafiteTypes.status uid baseuri
+ inherit ApplyTransformation.status uid
end
exception TryingToAdd of string Lazy.t
;;
-let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
+let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast as ast') =
let baseuri = status#baseuri in
- (*
- let new_aliases,new_status =
- GrafiteDisambiguate.eval_with_new_aliases status
- (fun status ->
- GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
- (text,prefix_len,ast)) in
- *)
- let new_status =
- GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
- (text,prefix_len,ast) 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
- *)
- [new_status,None]
+ GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status ast'
;;
let baseuri_of_script ~include_paths fname =
let rec get_ast status ~compiling ~asserted ~include_paths strm =
match GrafiteParser.parse_statement status strm with
(GrafiteAst.Executable
- (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
+ (loc,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
+ ?uid:status#user 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 =
- let asserted,stop,status =
+ 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
+ | 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
+ eval_ast ~include_paths ?do_heavy_checks status ("",0,ast)
+ in
+ 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
+ asserted, false, status, str
with exn when not matita_debug ->
+ (* prerr_endline ("EnrichedWithStatus: " ^ Printexc.to_string exn); *)
raise (EnrichedWithStatus (exn, status))
in
- if stop then asserted,status else loop asserted status
+ if stop then asserted,status else loop asserted status str
in
- loop asserted status
+ loop asserted status str
-and compile ~compiling ~asserted ~include_paths fname =
+and compile ~compiling ~asserted ~include_paths ~outch ?uid 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 matita_debug = true in
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
+ (* FIXME: currently hardcoded to single user mode *)
+ let status = new status uid baseuri in
let big_bang = Unix.gettimeofday () in
let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} =
Unix.times ()
(Filename.dirname
(Http_getter.filename ~local:true ~writable:true (baseuri ^
"foo.con")));
+ prerr_endline ("trying to compile " ^ fname);
let buf =
GrafiteParser.parsable_statement status
(Ulexing.from_utf8_channel (open_in fname))
in
let asserted, status =
eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
+ prerr_endline ("end compile of " ^ fname);
let elapsed = Unix.time () -. time in
(if Helm_registry.get_bool "matita.moo" then begin
GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
HLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
pp_times fname true big_bang big_bang_u big_bang_s;
- (* XXX: update script -- currently to stdout *)
let origbuf = Ulexing.from_utf8_channel (open_in fname) in
- let outfile = open_out (fname ^ ".mad") in
let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in
- ignore (SmallLexer.mk_small_printer interpr outfile origbuf);
- close_out outfile;
+ let outstr = ref "" in
+ ignore (SmallLexer.mk_small_printer interpr outstr origbuf);
+ Printf.fprintf outch "%s" !outstr;
asserted
(* MATITA 1.0: debbo fare time_travel sulla ng_library?
LexiconSync.time_travel
pp_times fname false big_bang big_bang_u big_bang_s;
clean_exit baseuri exn
-and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
+and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid mapath =
let _,baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
if List.mem fullmapath asserted then asserted,false
else
begin
let baseuri = NUri.uri_of_string baseuri in
let ngtime_of baseuri =
- let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
+ let ngpath = NCicLibrary.ng_path_of_baseuri uid baseuri in
+ let uid = match uid with Some u -> "Some " ^ u | _ -> "None" in
+ (* prerr_endline ("uid = " ^ uid);
+ prerr_endline ("ngpath = " ^ ngpath); *)
try
Some (Unix.stat ngpath).Unix.st_mtime
with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
let asserted,to_be_compiled =
match ngtime with
Some ngtime ->
- let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
+ let preamble = GrafiteTypes.Serializer.dependencies_of uid 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
+ ?uid mapath
in
asserted, b || b1
|| let _,baseuri,_,_ =
asserted, children_bad || matime > ngtime
| None -> asserted,true
in
+ (* prerr_endline ("asserted = " ^ (String.concat "," asserted)); *)
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
+ let outch, is_file_ch =
+ match outch with
+ | None -> open_out (fullmapath ^ ".mad"), true
+ | Some c -> c, false
+ in
+ (* prerr_endline ("compiling " ^ fullmapath); *)
+ let asserted = compile ~compiling ~asserted ~include_paths ~outch ?uid fullmapath in
+ if is_file_ch then close_out outch;
fullmapath::asserted,true
end
;;
-let assert_ng ~include_paths mapath =
+let eos status s =
+ let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" in
+ let rec is_there_only_comments status s =
+ if Pcre.pmatch ~rex:only_dust_RE s then raise End_of_file;
+ let strm =
+ GrafiteParser.parsable_statement status
+ (Ulexing.from_utf8_string s) in
+ match GrafiteParser.parse_statement status strm with
+ | GrafiteAst.Comment (loc,_) ->
+ let _,parsed_text_length = HExtlib.utf8_parsed_text s loc in
+ (* CSC: why +1 in the following lines ???? *)
+ let parsed_text_length = parsed_text_length + 1 in
+ let remain_len = String.length s - parsed_text_length in
+ let next = String.sub s parsed_text_length remain_len in
+ is_there_only_comments status next
+ | GrafiteAst.Executable _ -> false
+ in
+ try is_there_only_comments status s
+ with
+ | NCicLibrary.IncludedFileNotCompiled _
+ | HExtlib.Localized _
+ | CicNotationParser.Parse_error _ -> false
+ | End_of_file -> true
+ | Invalid_argument "Array.make" -> false
+;;
+
+
+let assert_ng ~include_paths ?outch mapath =
snd (assert_ng ~include_paths ~already_included:[] ~compiling:[] ~asserted:[]
- mapath)
+ ?outch mapath)
let get_ast status ~include_paths strm =
snd (get_ast status ~compiling:[] ~asserted:[] ~include_paths strm)
projects / helm.git / blobdiff