X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitacLib.ml;h=bed0819db85d0bfe20a9427bf7659d1a75aaf432;hb=8ee0e6f729105eaf1907de0baef22e170b0d17b3;hp=52ad776e71d3a2fe91a07c5107b28dea21baa3ff;hpb=68d46ac40a575f3fce5958fb2776b38739703951;p=helm.git diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index 52ad776e7..bed0819db 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -35,9 +35,12 @@ let out = ref ignore let set_callback f = out := f -let pp_ast_statement = - GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term - ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) +let pp_ast_statement st = + GrafiteAstPp.pp_statement + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + ~term_pp:CicNotationPp.pp_term + ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st (** {2 Initialization} *) @@ -78,7 +81,8 @@ let run_script is eval_function = with | GrafiteEngine.Drop | End_of_file - | CicNotationParser.Parse_error _ as exn -> raise exn + | CicNotationParser.Parse_error _ + | GrafiteEngine.Macro _ as exn -> raise exn | exn -> if not matita_debug then HLog.error (snd (MatitaExcPp.to_string exn)) ; @@ -120,7 +124,15 @@ let clean_exit n = with GrafiteTypes.Option_error("baseuri", "not found") -> (* no baseuri ==> nothing to clean yet *) opt_exit n - + +let get_macro_context = function + | Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> [] + | Some status -> + let stack = GrafiteTypes.get_stack status in + let goal = Continuationals.Stack.find_goal stack in + GrafiteTypes.get_proof_context status goal + | None -> assert false + let rec interactive_loop () = let str = Ulexing.from_utf8_channel stdin in try @@ -131,16 +143,20 @@ let rec interactive_loop () = with | GrafiteEngine.Drop -> pp_ocaml_mode () | GrafiteEngine.Macro (floc, f) -> - begin match snd (f []) with - | GrafiteAst.Inline (_, style, suri, prefix) -> - let str = ApplyTransformation.txt_of_inline_macro style suri prefix in - !out str - | _ -> () - end; - let x, y = HExtlib.loc_of_floc floc in - HLog.error - (sprintf "A macro has been found in a script at %d-%d" x y); - interactive_loop () + begin match f (get_macro_context !grafite_status) with + | _, GrafiteAst.Inline (_, style, suri, prefix) -> + let str = + ApplyTransformation.txt_of_inline_macro style suri prefix + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + in + !out str; + interactive_loop () + | _ -> + let x, y = HExtlib.loc_of_floc floc in + HLog.error (sprintf "A macro has been found in a script at %d-%d" x y); + interactive_loop () + end | Sys.Break -> HLog.error "user break!"; interactive_loop () | GrafiteTypes.Command_error _ -> interactive_loop () | End_of_file -> @@ -215,11 +231,105 @@ let pp_times fname bench_mode rc big_bang = end ;; +let rec compiler_loop fname big_bang mode buf = + let include_paths = + Helm_registry.get_list Helm_registry.string "matita.includes" in + let clean_baseuri = not (Helm_registry.get_bool "matita.preserve") in + let matita_debug = Helm_registry.get_bool "matita.debug" in + let bench_mode = Helm_registry.get_bool "matita.bench" in + try + run_script buf + (MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths + ~clean_baseuri) + with + | End_of_file -> () + | Sys.Break as exn -> + if matita_debug then raise exn; + HLog.error "user break!"; + pp_times fname bench_mode false big_bang; + if mode = `COMPILER then + clean_exit (Some ~-1) + else + pp_ocaml_mode () + | GrafiteEngine.Drop -> + if mode = `COMPILER then + begin + pp_times fname bench_mode false big_bang; + clean_exit (Some 1) + end + else + pp_ocaml_mode () + | GrafiteEngine.Macro (floc, f) -> + begin match f (get_macro_context !grafite_status) with + | _, GrafiteAst.Inline (_, style, suri, prefix) -> + let str = + ApplyTransformation.txt_of_inline_macro style suri prefix + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") in + !out str; + compiler_loop fname big_bang mode buf + | _ -> + let x, y = HExtlib.loc_of_floc floc in + HLog.error (sprintf "A macro has been found in a script at %d-%d" x y); + if mode = `COMPILER then + begin + pp_times fname bench_mode false big_bang; + clean_exit (Some 1) + end + else + pp_ocaml_mode () + end + | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> + let (x, y) = HExtlib.loc_of_floc floc in + HLog.error (sprintf "Parse error at %d-%d: %s" x y err); + if mode = `COMPILER then + begin + pp_times fname bench_mode false big_bang; + clean_exit (Some 1) + end + else + pp_ocaml_mode () + | exn -> + if matita_debug then raise exn; + if mode = `COMPILER then + begin + pp_times fname bench_mode false big_bang; + clean_exit (Some 3) + end + else + pp_ocaml_mode () + let main ~mode = let big_bang = Unix.gettimeofday () in MatitaInit.initialize_all (); (* must be called after init since args are set by cmdline parsing *) let fname = fname () in + if false then + (let basename = Filename.basename (Filename.chop_extension fname) in + let baseuri = + (* This does not work yet :-( + let baseuri = + GrafiteTypes.get_string_option + (match !grafite_status with None -> assert false | Some s -> s) + "baseuri" in*) + lazy + (fst (DependenciesParser.baseuri_of_script ~include_paths:[] fname)) in + let mangled_baseuri = + lazy + ( let baseuri = Lazy.force baseuri in + let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in + let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in + String.uncapitalize baseuri + ) in + let f = + lazy + (open_out + (Filename.dirname fname ^ "/" ^ Lazy.force mangled_baseuri ^ ".ml")) in + LibrarySync.set_object_declaration_hook + (fun _ obj -> + output_string (Lazy.force f) + (CicExportation.ppobj (Lazy.force baseuri) obj); + flush (Lazy.force f))); let system_mode = Helm_registry.get_bool "matita.system" in let bench_mode = Helm_registry.get_bool "matita.bench" in if bench_mode then @@ -241,25 +351,17 @@ let main ~mode = if Helm_registry.get_int "matita.verbosity" < 1 then HLog.set_log_callback newcb; if bench_mode then MatitaMisc.shutup (); - let matita_debug = Helm_registry.get_bool "matita.debug" in - try let time = Unix.time () in if Helm_registry.get_int "matita.verbosity" < 1 && not bench_mode then origcb `Message ("compiling " ^ Filename.basename fname ^ "...") else HLog.message (sprintf "execution of %s started:" fname); - let is = - Ulexing.from_utf8_channel - (match fname with - | "stdin" -> stdin - | fname -> open_in fname) in - let include_paths = - Helm_registry.get_list Helm_registry.string "matita.includes" in - (try - run_script is - (MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths - ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve"))) - with End_of_file -> ()); + let ich = match fname with + | "stdin" -> stdin + | fname -> open_in fname + in + let buf = Ulexing.from_utf8_channel ich in + compiler_loop fname big_bang mode buf; let elapsed = Unix.time () -. time in let tm = Unix.gmtime elapsed in let sec = string_of_int tm.Unix.tm_sec ^ "''" in @@ -269,10 +371,10 @@ let main ~mode = let hou = if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else "" in - let proof_status,moo_content_rev,metadata,lexicon_content_rev = + let proof_status,moo_content_rev,lexicon_content_rev = match !lexicon_status,!grafite_status with | Some ss, Some s -> - s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata, + s.proof_status, s.moo_content_rev, ss.LexiconEngine.lexicon_content_rev | _,_ -> assert false in @@ -295,63 +397,13 @@ let main ~mode = LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in - let metadata_fname = - LibraryMisc.metadata_file_of_baseuri - ~must_exist:false ~baseuri ~writable:true - in - GrafiteMarshal.save_moo moo_fname moo_content_rev; - LibraryNoDb.save_metadata metadata_fname metadata; - LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; +(* FG: we do not generate .moo when dumping .mma files *) + if Helm_registry.get_bool "matita.moo" then begin + GrafiteMarshal.save_moo moo_fname moo_content_rev; + LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; + end; HLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); pp_times fname bench_mode true big_bang; exit 0 end - with - | Sys.Break as exn -> - if matita_debug then raise exn; - HLog.error "user break!"; - pp_times fname bench_mode false big_bang; - if mode = `COMPILER then - clean_exit (Some ~-1) - else - pp_ocaml_mode () - | GrafiteEngine.Drop -> - if mode = `COMPILER then - begin - pp_times fname bench_mode false big_bang; - clean_exit (Some 1) - end - else - pp_ocaml_mode () - | GrafiteEngine.Macro (floc,_) -> - let x, y = HExtlib.loc_of_floc floc in - HLog.error - (sprintf "A macro has been found in a script at %d-%d" x y); - if mode = `COMPILER then - begin - pp_times fname bench_mode false big_bang; - clean_exit (Some 1) - end - else - pp_ocaml_mode () - | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> - let (x, y) = HExtlib.loc_of_floc floc in - HLog.error (sprintf "Parse error at %d-%d: %s" x y err); - if mode = `COMPILER then - begin - pp_times fname bench_mode false big_bang; - clean_exit (Some 1) - end - else - pp_ocaml_mode () - | exn -> - if matita_debug then raise exn; - if mode = `COMPILER then - begin - pp_times fname bench_mode false big_bang; - clean_exit (Some 3) - end - else - pp_ocaml_mode () -