X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FmatitaEngine.ml;h=3757b177f1706dc3fc290c8f402a20af3a51dbe0;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=913ba87f6a835e8269bdd3973297ed7b81ddff03;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml index 913ba87f6..3757b177f 100644 --- a/matitaB/matita/matitaEngine.ml +++ b/matitaB/matita/matitaEngine.ml @@ -29,10 +29,10 @@ module G = GrafiteAst 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 @@ -116,36 +116,9 @@ let activate_extraction baseuri fname = ;; -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 _,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 + GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status ast' ;; let baseuri_of_script ~include_paths fname = @@ -162,55 +135,61 @@ 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 - asserted, false, status + 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 -> + (* 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 () @@ -243,6 +222,7 @@ and compile ~compiling ~asserted ~include_paths fname = (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)) @@ -253,6 +233,7 @@ and compile ~compiling ~asserted ~include_paths 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) @@ -269,6 +250,11 @@ and compile ~compiling ~asserted ~include_paths fname = 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; + let origbuf = Ulexing.from_utf8_channel (open_in fname) in + let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in + 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 @@ -276,21 +262,24 @@ and compile ~compiling ~asserted ~include_paths fname = *)) with (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *) - | exn when not matita_debug -> + | exn when not matita_debug -> (* MATITA 1.0: debbo fare time_travel sulla ng_library? LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status; * *) 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 @@ -302,13 +291,13 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath = 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,_,_ = @@ -322,19 +311,54 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath = 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)