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 [])
+let debug = false;;
+
exception NoRootFor of string
let absolutize path =
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
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
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
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
matitaMisc.mli \
matitaEngine.mli \
matitaExcPp.mli \
- matitaInit.mli \
applyTransformation.mli \
- matitaAutoGui.mli \
matitacLib.mli \
+ matitaInit.mli \
+ matitaAutoGui.mli \
matitaGtkMisc.mli \
matitaScript.mli \
matitaMathView.mli \
matitaMisc.mli \
matitaEngine.mli \
matitaExcPp.mli \
- matitaInit.mli \
applyTransformation.mli \
matitacLib.mli \
+ matitaInit.mli \
matitaWiki.mli \
$(NULL)
MAINCMLI = \
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
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,
+ "<filename> Dump with expanded macros to <filename>";
"-v",
Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true),
"Verbose mode";
(* $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 ();
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 = "<filename> Dump with expanded macros to <filename>" in
- MatitaInit.add_cmdline_spec ["-dump", Arg.String dump, dump_msg];
- main_compiler ()
+ else main_compiler ()
;;
let _ = main ()
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:[]
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
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
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 =
(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;
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)
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!";
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
;;
projects / helm.git / commitdiff