exception AttemptToInsertAnAlias of LexiconEngine.status
-let out = ref ignore
-let set_callback f = out := f
-
-
let slash_n_RE = Pcre.regexp "\\n" ;;
let pp_ast_statement grafite_status stm =
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 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 =
+ let pp_statement stm =
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
+ ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) stm
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 ()
+ let pp_lexicon = LexiconAstPp.pp_command in
+ let och = open_out f in
+ let nl () = output_string och (pp_statement nl_ast) in
+ MatitaMisc.out_preamble och;
+ let grafite_parser_cb = function
+ | G.Executable (_, G.Macro (_, G.Inline (_, uri, params))) ->
+ let str =
+ ApplyTransformation.txt_of_inline_macro params uri
+ ~map_unicode_to_tex:
+ (Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ in
+ output_string och str
+ | G.Executable (loc, G.Command (_, G.Include (_, false, _, _))) -> ()
+ | stm ->
+ output_string och (pp_statement stm); 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 ()
+ let lexicon_parser_cb cmd =
+ output_string och (pp_lexicon cmd); nl (); nl ()
in
- let matitac_lib_cb = output_string och in
- GrafiteParser.set_callback grafite_parser_cb;
- MatitaEngine.set_callback matita_engine_cb;
- set_callback matitac_lib_cb;
- fun x ->
+ begin fun () ->
+ Helm_registry.set_bool "matita.moo" false;
+ GrafiteParser.set_grafite_callback grafite_parser_cb;
+ GrafiteParser.set_lexicon_callback lexicon_parser_cb
+ end,
+ begin fun x ->
close_out och;
- GrafiteParser.set_callback ignore;
- MatitaEngine.set_callback ignore;
- set_callback ignore; x
+ GrafiteParser.set_grafite_callback (fun _ -> ());
+ GrafiteParser.set_lexicon_callback (fun _ -> ());
+ Helm_registry.set_bool "matita.moo" true;
+ x
+ end
;;
let get_macro_context = function
- | Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> []
+ | Some status when status#proof_status = GrafiteTypes.No_proof -> []
| Some status ->
let stack = GrafiteTypes.get_stack status in
let goal = Continuationals.Stack.find_goal stack in
let f =
open_out
(Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in
- LibrarySync.set_object_declaration_hook
- (fun _ obj ->
+ LibrarySync.add_object_declaration_hook
+ (fun ~add_obj ~add_coercion _ obj ->
output_string f (CicExportation.ppobj baseuri obj);
- flush f);
+ flush f; []);
;;
-let compile options fname =
+let compile atstart 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
if Http_getter_storage.is_read_only baseuri then assert false;
activate_extraction baseuri fname ;
- let grafite_status = GrafiteSync.init baseuri in
let lexicon_status =
- CicNotation2.load_notation ~include_paths:[]
+ CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status)
BuildTimeConf.core_notation_script
in
+ atstart (); (* FG: do not invoke before loading the core notation script *)
+ let grafite_status = GrafiteSync.init lexicon_status baseuri in
let big_bang = Unix.gettimeofday () in
let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} =
Unix.times ()
if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
else pp_ast_statement
in
- let grafite_status, lexicon_status =
- let rec aux_for_dump x =
+ let grafite_status =
+ let rec aux_for_dump x grafite_status =
try
match
MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
- lexicon_status grafite_status buf x
+ grafite_status buf x
with
- | [] -> 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, flavour) ->
- let str =
+ | [] -> grafite_status
+ | (g,None)::_ -> g
+ | (g,Some _)::_ ->
+ raise (AttemptToInsertAnAlias (g :> LexiconEngine.status))
+ with MatitaEngine.EnrichedWithStatus
+ (GrafiteEngine.Macro (floc, f), grafite) as exn ->
+ match f (get_macro_context (Some grafite)) with
+ | _, GrafiteAst.Inline (_, _suri, _params) ->
+(*
+ let str =
ApplyTransformation.txt_of_inline_macro style prefix suri
?flavour
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
in
!out str;
- aux_for_dump x
+*)
+ aux_for_dump x grafite
|_-> raise exn
in
- aux_for_dump print_cb
+ aux_for_dump print_cb grafite_status
in
let elapsed = Unix.time () -. time in
let proof_status,moo_content_rev,lexicon_content_rev =
- grafite_status.proof_status, grafite_status.moo_content_rev,
- lexicon_status.LexiconEngine.lexicon_content_rev
+ grafite_status#proof_status, grafite_status#moo_content_rev,
+ grafite_status#lstatus.LexiconEngine.lexicon_content_rev
in
if proof_status <> GrafiteTypes.No_proof then
(HLog.error
*)
clean_exit baseuri false)
else
- (if not (Helm_registry.get_bool "matita.moo" &&
- Filename.check_suffix fname ".mma") then begin
+ (if Helm_registry.get_bool "matita.moo" 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;
+ NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+ grafite_status#dump
end;
let tm = Unix.gmtime elapsed in
let sec = string_of_int tm.Unix.tm_sec ^ "''" in
~present:lexicon_status ~past:initial_lexicon_status;
*)
clean_exit baseuri false
- | MatitaEngine.EnrichedWithLexiconStatus (exn, lex_stat) as exn' ->
+ | MatitaEngine.EnrichedWithStatus (exn, _grafite) as exn' ->
(match exn with
| Sys.Break -> HLog.error "user break!"
| 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)
| exn when matita_debug -> raise exn'
- | exn -> HLog.error (snd (MatitaExcPp.to_string exn)));
-(* LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status;
+ | exn -> HLog.error (snd (MatitaExcPp.to_string exn))
+ );
+(* LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
* *)
pp_times fname false big_bang big_bang_u big_bang_s;
clean_exit baseuri false
let root_and_target_of opts mafile =
try
let include_paths = get_include_paths opts in
- let root,baseuri,_,_ =
+ let root,baseuri,_,relpath =
Librarian.baseuri_of_script ~include_paths mafile
in
let obj_writeable, obj_read_only =
LibraryMisc.obj_file_of_baseuri
~must_exist:false ~baseuri ~writable:false
in
- Some root, obj_writeable, obj_read_only
- with Librarian.NoRootFor x -> None, "", ""
+ Some root, relpath, obj_writeable, obj_read_only
+ with Librarian.NoRootFor x -> None, "", "", ""
;;
let mtime_of_source_object s =
with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
;;
+(* FG: a problem was noticed in relising memory between subsequent *)
+(* invocations of the compiler. The following might help *)
+ let compact r = Gc.compact (); r
+
let build options fname =
- let compile opts fname =
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
+ let compile atstart opts fname =
try
GrafiteSync.push ();
GrafiteParser.push ();
- let rc = compile opts fname in
+ let rc = compile atstart opts fname in
GrafiteParser.pop ();
GrafiteSync.pop ();
rc
GrafiteParser.pop ();
GrafiteSync.pop ();
false
- | exn ->
+ | exn when not matita_debug ->
HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
assert false
in
if Filename.check_suffix fname ".mma" then
let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
- let atexit = dump generated in
- let res = compile options fname in
- let r = atexit res in
+ let atstart, atexit = dump generated in
+ let res = compile atstart options fname in
+ let r = compact (atexit res) in
if r then r else begin
- Sys.remove generated;
- Printf.printf "rm %s\n" generated; flush stdout; r
+(* Sys.remove generated; *)
+ Printf.printf "rm %s\n" generated; flush stdout; r
end
else
- compile options fname
+ compact (compile ignore options fname)
;;
let load_deps_file = Librarian.load_deps_file;;
projects / helm.git / blobdiff