From: Enrico Tassi Date: Thu, 10 Jan 2008 10:46:32 +0000 (+0000) Subject: beginning to see the light X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=refs%2Fheads%2Fno-baseuri;p=helm.git beginning to see the light --- diff --git a/components/grafite_parser/dependenciesParser.ml b/components/grafite_parser/dependenciesParser.ml index 2f7c5ec0c..32ee44491 100644 --- a/components/grafite_parser/dependenciesParser.ml +++ b/components/grafite_parser/dependenciesParser.ml @@ -41,26 +41,29 @@ let parse_dependencies lexbuf = CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf) in let rec parse acc = - try - (parser - | [< '("QSTRING", s) >] -> - (* because of alias id qstring = qstring :-( *) - (try - parse (UriDep (UriManager.uri_of_string s) :: acc) - with - UriManager.IllFormedUri _ -> parse acc) - | [< '("URI", u) >] -> - parse (UriDep (UriManager.uri_of_string u) :: acc) - | [< '("IDENT", "include"); '("QSTRING", fname) >] -> - parse (IncludeDep fname :: acc) - | [< '("IDENT", "include'"); '("QSTRING", fname) >] -> - parse (IncludeDep fname :: acc) - | [< '("EOI", _) >] -> acc - | [< 'tok >] -> parse acc - | [< >] -> acc) tok_stream - with - Stream.Error _ -> parse acc - | CicNotationLexer.Error _ -> parse acc + let continue, acc = + try + (parser + | [< '("QSTRING", s) >] -> + (* because of alias id qstring = qstring :-( *) + (try + true, (UriDep (UriManager.uri_of_string s) :: acc) + with + UriManager.IllFormedUri _ -> true, acc) + | [< '("URI", u) >] -> + true, (UriDep (UriManager.uri_of_string u) :: acc) + | [< '("IDENT", "include"); '("QSTRING", fname) >] -> + true, (IncludeDep fname :: acc) + | [< '("IDENT", "include'"); '("QSTRING", fname) >] -> + true, (IncludeDep fname :: acc) + | [< '("EOI", _) >] -> false, acc + | [< 'tok >] -> true, acc + | [< >] -> false, acc) tok_stream + with + Stream.Error _ -> false, acc + | CicNotationLexer.Error _ -> true, acc + in + if continue then parse acc else acc in List.rev (parse []) diff --git a/components/library/librarian.ml b/components/library/librarian.ml index cc3c96999..db6b81574 100644 --- a/components/library/librarian.ml +++ b/components/library/librarian.ml @@ -1,3 +1,5 @@ +let debug = false;; + exception NoRootFor of string let absolutize path = @@ -91,7 +93,8 @@ let baseuri_of_script ~include_paths file = in let extra_buri = substract lpath lroot in let chop name = - assert(Filename.check_suffix name ".ma"); + assert(Filename.check_suffix name ".ma" || + Filename.check_suffix name ".mma"); try Filename.chop_extension name with Invalid_argument "Filename.chop_extension" -> name in @@ -147,7 +150,7 @@ module type Format = module Make = functor (F:Format) -> struct - let prerr_endline _ = ();; + let prerr_endline s = if debug then prerr_endline ("make: "^s);; let younger_s_t a b = match F.mtime_of_source_object a, F.mtime_of_target_object b with diff --git a/matita/.depend b/matita/.depend index a0134082f..97149bc33 100644 --- a/matita/.depend +++ b/matita/.depend @@ -15,9 +15,9 @@ matitacLib.cmo: matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmo \ matitacLib.cmx: matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \ applyTransformation.cmx matitacLib.cmi matitac.cmo: matitadep.cmi matitaclean.cmi matitacLib.cmi matitaWiki.cmo \ - matitaMisc.cmi matitaInit.cmi matitaEngine.cmi + matitaMisc.cmi matitaInit.cmi matitac.cmx: matitadep.cmx matitaclean.cmx matitacLib.cmx matitaWiki.cmx \ - matitaMisc.cmx matitaInit.cmx matitaEngine.cmx + matitaMisc.cmx matitaInit.cmx matitadep.cmo: matitaInit.cmi matitadep.cmi matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi @@ -34,8 +34,10 @@ matitaGui.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMathView.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \ matitaExcPp.cmx matitaAutoGui.cmx buildTimeConf.cmx matitaGui.cmi -matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmo matitaInit.cmi -matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi +matitaInit.cmo: matitacLib.cmi matitaExcPp.cmi matitaEngine.cmi \ + buildTimeConf.cmo matitaInit.cmi +matitaInit.cmx: matitacLib.cmx matitaExcPp.cmx matitaEngine.cmx \ + buildTimeConf.cmx matitaInit.cmi matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \ buildTimeConf.cmo applyTransformation.cmi matitaMathView.cmi diff --git a/matita/Makefile b/matita/Makefile index a9cf7141d..97d74fdc4 100644 --- a/matita/Makefile +++ b/matita/Makefile @@ -33,10 +33,10 @@ MLI = \ matitaMisc.mli \ matitaEngine.mli \ matitaExcPp.mli \ - matitaInit.mli \ applyTransformation.mli \ - matitaAutoGui.mli \ matitacLib.mli \ + matitaInit.mli \ + matitaAutoGui.mli \ matitaGtkMisc.mli \ matitaScript.mli \ matitaMathView.mli \ @@ -47,9 +47,9 @@ CMLI = \ matitaMisc.mli \ matitaEngine.mli \ matitaExcPp.mli \ - matitaInit.mli \ applyTransformation.mli \ matitacLib.mli \ + matitaInit.mli \ matitaWiki.mli \ $(NULL) MAINCMLI = \ diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml index 03de96b5f..cf96c5ba1 100644 --- a/matita/matitaInit.ml +++ b/matita/matitaInit.ml @@ -162,6 +162,65 @@ let usage () = try Filename.chop_extension basename with Invalid_argument _ -> basename in try Hashtbl.find usages usage_key with Not_found -> default_usage +;; + +let dump f = + let module G = GrafiteAst in + let module L = LexiconAst in + let module H = HExtlib in + Helm_registry.set_bool "matita.moo" false; + let floc = H.dummy_floc in + let nl_ast = G.Comment (floc, G.Note (floc, "")) in + let och = open_out f in + let atexit () = close_out och in + let out_comment och s = + let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in + Printf.fprintf och "%s%s%s\n\n" "(*" s "*)" + in + let out_line_comment och s = + let l = 70 - String.length s in + let s = Printf.sprintf " %s %s" s (String.make l '*') in + out_comment och s + in + let out_preamble och (path, lines) = + let ich = open_in path in + let rec print i = + if i > 0 then + let s = input_line ich in + begin Printf.fprintf och "%s\n" s; print (pred i) end + in + print lines; + out_line_comment och "This file was automatically generated: do not edit" + in + let pp_ast_statement st = + GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + ~lazy_term_pp:CicNotationPp.pp_term + ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st + in + let nl () = output_string och (pp_ast_statement nl_ast) in + let rt_base_dir = Filename.dirname Sys.argv.(0) in + let path = Filename.concat rt_base_dir "matita.ma.templ" in + let lines = 14 in + out_preamble och (path, lines); + let grafite_parser_cb fname = + let ast = G.Executable + (floc, G.Command (floc, G.Include (floc, fname))) in + output_string och (pp_ast_statement ast); nl (); nl () + in + let matita_engine_cb = function + | G.Executable (_, G.Macro (_, G.Inline _)) + | G.Executable (_, G.Command (_, G.Include _)) -> () + | ast -> + output_string och (pp_ast_statement ast); nl (); nl () + in + let matitac_lib_cb = output_string och in + GrafiteParser.set_callback grafite_parser_cb; + MatitaEngine.set_callback matita_engine_cb; + MatitacLib.set_callback matitac_lib_cb; + at_exit atexit +;; let extra_cmdline_specs = ref [] let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs @@ -214,6 +273,8 @@ let parse_cmdline init_status = Helm_registry.set_bool "matita.system" true), ("Act on the system library instead of the user one" ^ "\n WARNING: not for the casual user"); + "-dump", Arg.String dump, + " Dump with expanded macros to "; "-v", Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true), "Verbose mode"; diff --git a/matita/matitac.ml b/matita/matitac.ml index 2f2987388..5d0ed9a35 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -25,65 +25,6 @@ (* $Id$ *) -module G = GrafiteAst -module L = LexiconAst -module H = HExtlib - -(* from transcript *) - -let out_comment och s = - let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in - Printf.fprintf och "%s%s%s\n\n" "(*" s "*)" - -let out_line_comment och s = - let l = 70 - String.length s in - let s = Printf.sprintf " %s %s" s (String.make l '*') in - out_comment och s - -let out_preamble och (path, lines) = - let ich = open_in path in - let rec print i = - if i > 0 then - let s = input_line ich in - begin Printf.fprintf och "%s\n" s; print (pred i) end - in - print lines; - out_line_comment och "This file was automatically generated: do not edit" - -let pp_ast_statement st = - GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) st - -let dump f = - Helm_registry.set_bool "matita.moo" false; - let floc = H.dummy_floc in - let nl_ast = G.Comment (floc, G.Note (floc, "")) in - let och = open_out f in - let atexit () = close_out och in - let nl () = output_string och (pp_ast_statement nl_ast) in - let rt_base_dir = Filename.dirname Sys.argv.(0) in - let path = Filename.concat rt_base_dir "matita.ma.templ" in - let lines = 14 in - out_preamble och (path, lines); - let grafite_parser_cb fname = - let ast = G.Executable (floc, G.Command (floc, G.Include (floc, fname))) in - output_string och (pp_ast_statement ast); nl (); nl () - in - let matita_engine_cb = function - | G.Executable (_, G.Macro (_, G.Inline _)) - | G.Executable (_, G.Command (_, G.Include _)) -> () - | ast -> - output_string och (pp_ast_statement ast); nl (); nl () - in - let matitac_lib_cb = output_string och in - GrafiteParser.set_callback grafite_parser_cb; - MatitaEngine.set_callback matita_engine_cb; - MatitacLib.set_callback matitac_lib_cb; - at_exit atexit -;; - (* compiler ala pascal/java using make *) let main_compiler () = MatitaInit.initialize_all (); @@ -124,10 +65,7 @@ let main () = if Pcre.pmatch ~pat:"^matitadep" bin then Matitadep.main () else if Pcre.pmatch ~pat:"^matitaclean" bin then Matitaclean.main () else if Pcre.pmatch ~pat:"^matitawiki" bin then MatitaWiki.main () - else - let dump_msg = " Dump with expanded macros to " in - MatitaInit.add_cmdline_spec ["-dump", Arg.String dump, dump_msg]; - main_compiler () + else main_compiler () ;; let _ = main () diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index 5495a6f78..fb4f3770f 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -107,10 +107,11 @@ let get_include_paths options = include_paths ;; -let rec compile options fname = +let compile options fname = let matita_debug = Helm_registry.get_bool "matita.debug" in let include_paths = get_include_paths options in - let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in + let root,baseuri,fname,_tgt = + Librarian.baseuri_of_script ~include_paths fname in let grafite_status = GrafiteSync.init baseuri in let lexicon_status = CicNotation2.load_notation ~include_paths:[] @@ -125,7 +126,8 @@ let rec compile options fname = LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in let lexicon_fname= - LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~baseuri ~writable:true + LibraryMisc.lexicon_file_of_baseuri + ~must_exist:false ~baseuri ~writable:true in if Http_getter_storage.is_read_only baseuri then HLog.error @@ -150,7 +152,8 @@ let rec compile options fname = HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri); if not (Helm_registry.get_bool "matita.verbose") then (let cc = - if Str.string_match(Str.regexp ".*opt$") Sys.argv.(0) 0 then "matitac.opt" + let rex = Str.regexp ".*opt$" in + if Str.string_match rex Sys.argv.(0) 0 then "matitac.opt" else "matitac" in let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in @@ -161,13 +164,29 @@ let rec compile options fname = else pp_ast_statement in let grafite_status, lexicon_status = + let rec aux_for_dump x = + try match MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths - lexicon_status grafite_status buf print_cb + lexicon_status grafite_status buf x with - | [] -> raise End_of_file + | [] -> grafite_status, lexicon_status | ((grafite,lexicon),None)::_ -> grafite, lexicon | ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l) + + with MatitaEngine.EnrichedWithLexiconStatus + (GrafiteEngine.Macro (floc, f), lex_status) as exn -> + match f (get_macro_context (Some 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; + aux_for_dump x + |_-> raise exn + in + aux_for_dump print_cb in let elapsed = Unix.time () -. time in let proof_status,moo_content_rev,lexicon_content_rev = @@ -178,10 +197,12 @@ let rec compile options fname = (HLog.error "there are still incomplete proofs at the end of the script"; pp_times fname false big_bang; - LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status; + LexiconSync.time_travel + ~present:lexicon_status ~past:initial_lexicon_status; clean_exit baseuri false) else - (if Helm_registry.get_bool "matita.moo" then begin + (if not (Helm_registry.get_bool "matita.moo" && + Filename.check_suffix fname ".mma") then begin (* FG: we do not generate .moo when dumping .mma files *) GrafiteMarshal.save_moo moo_fname moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; @@ -197,31 +218,19 @@ let rec compile options fname = HLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); pp_times fname true big_bang; - LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status; + LexiconSync.time_travel + ~present:lexicon_status ~past:initial_lexicon_status; true) with (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *) | AttemptToInsertAnAlias lexicon_status -> pp_times fname false big_bang; - LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status; + LexiconSync.time_travel + ~present:lexicon_status ~past:initial_lexicon_status; clean_exit baseuri false | MatitaEngine.EnrichedWithLexiconStatus (exn, lex_stat) -> (match exn with | Sys.Break -> HLog.error "user break!" - | GrafiteEngine.Macro (floc, f) -> - (try - match f (get_macro_context (Some 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 - (* the output of compilation is wrong in this way!! *) - !out str; ignore(compile options fname) - | _ -> - let x, y = HExtlib.loc_of_floc floc in - HLog.error (sprintf "A macro has been found at %d-%d" x y) - with exn -> HLog.error (snd (MatitaExcPp.to_string exn))) | 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) @@ -229,10 +238,6 @@ let rec compile options fname = LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status; pp_times fname false big_bang; clean_exit baseuri false - | End_of_file -> (* this is CSC stuff ... or can only happen on empty files *) - HLog.error "End_of_file"; - pp_times fname false big_bang; - clean_exit baseuri false | Sys.Break as exn -> if matita_debug then raise exn; HLog.error "user break!"; @@ -240,7 +245,8 @@ let rec compile options fname = clean_exit baseuri false | exn -> if matita_debug then raise exn; - HLog.error ("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn)); + HLog.error + ("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn)); pp_times fname false big_bang; clean_exit baseuri false ;;