+let clean_exit baseuri exn =
+ LibraryClean.clean_baseuris ~verbose:false [baseuri];
+ raise (FailureCompiling (baseuri,exn))
+;;
+
+let cut prefix s =
+ let lenp = String.length prefix in
+ let lens = String.length s in
+ assert (lens > lenp);
+ assert (String.sub s 0 lenp = prefix);
+ 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 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 =
+ if rc then "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" in
+ 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
+ let seconds = seconds mod 60 in
+ Printf.sprintf "%dm%02d.%02ds" minutes seconds cents
+ in
+ Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s)
+ in
+ let s = Printf.sprintf "%-14s %s %s\n" rc times extra in
+ print_string false ~right_justify:(s,31) ss;
+ flush stdout;
+ HLog.message ("Compilation of "^Filename.basename fname^": "^rc)
+;;
+
+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
+ (new_status,None)::intermediate_states
+;;
+
+let baseuri_of_script ~include_paths fname =
+ 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 _ ->
+ raise (Failure ("File not found: "^fname))
+;;
+
+(* given a path to a ma file inside the include_paths, returns the
+ new include_paths associated to that file *)
+let read_include_paths ~include_paths:_ file =
+ try
+ let root, _buri, _fname, _tgt =
+ Librarian.baseuri_of_script ~include_paths:[] file in
+ let includes =
+ try
+ Str.split (Str.regexp " ")
+ (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+ with Not_found -> []
+ in
+ let rc = root :: includes in
+ List.iter (HLog.debug) rc; rc
+ with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+ []
+;;
+
+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
+ ->
+ 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 _)))) ->
+ 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))
+ in
+ if stop then asserted,status else loop asserted status str