X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FmatitaEngine.ml;h=83eb235fb82350d3dd2baa613580d73195c72203;hb=11a20b624a4b5ed18008678cf6cd46dd9a32634d;hp=68cb16c84fa63ca4d9d2aa711d458be4fc4ac408;hpb=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;p=helm.git diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml index 68cb16c84..83eb235fb 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,44 +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 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 = @@ -175,7 +140,7 @@ let rec get_ast status ~compiling ~asserted ~include_paths strm = 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 @@ -192,14 +157,8 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status | None -> asserted, true, status | 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 with exn when not matita_debug -> @@ -209,7 +168,7 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status in loop asserted status -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 @@ -218,7 +177,8 @@ and compile ~compiling ~asserted ~include_paths fname = 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 () @@ -279,10 +239,10 @@ and compile ~compiling ~asserted ~include_paths fname = 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 @@ -297,14 +257,17 @@ and compile ~compiling ~asserted ~include_paths fname = 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 @@ -316,13 +279,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,_,_ = @@ -336,19 +299,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)