From 134014e54c374789b38b6c53945f63d21ddbacb0 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 27 Apr 2009 15:51:31 +0000 Subject: [PATCH] matitacLib: bugfix in .moo generation applyTransformation.ml: highlevel prettyprinter disabled when reconstructing inductive types (was re-enabled by mistake) procedural/Makefile.common: bugfix in entry names matitaEngine: unused callback removed lexiconAstPp: output bugfix The first reconstructed .ma's form library now compile :))))))) --- .../components/lexicon/lexiconAstPp.ml | 9 ++-- helm/software/matita/applyTransformation.ml | 4 +- .../contribs/procedural/Makefile.common | 13 +++--- helm/software/matita/matitaEngine.ml | 5 --- helm/software/matita/matitaEngine.mli | 3 -- helm/software/matita/matitacLib.ml | 41 ++++++++----------- 6 files changed, 31 insertions(+), 44 deletions(-) diff --git a/helm/software/components/lexicon/lexiconAstPp.ml b/helm/software/components/lexicon/lexiconAstPp.ml index 02383f4b8..c11e4f094 100644 --- a/helm/software/components/lexicon/lexiconAstPp.ml +++ b/helm/software/components/lexicon/lexiconAstPp.ml @@ -58,7 +58,7 @@ let pp_argument_pattern = function sprintf "%s%s" (Buffer.contents eta_buf) name let pp_interpretation dsc symbol arg_patterns cic_appl_pattern = - sprintf "interpretation \"%s\" '%s %s = %s" + sprintf "interpretation \"%s\" '%s %s = %s." dsc symbol (String.concat " " (List.map pp_argument_pattern arg_patterns)) (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern) @@ -69,7 +69,7 @@ let pp_dir_opt = function | Some `RightToLeft -> "< " let pp_notation dir_opt l1_pattern assoc prec l2_pattern = - sprintf "notation %s\"%s\" %s %s for %s" + sprintf "notation %s\"%s\" %s %s for %s." (pp_dir_opt dir_opt) (pp_l1_pattern l1_pattern) (pp_associativity assoc) @@ -79,12 +79,11 @@ let pp_notation dir_opt l1_pattern assoc prec l2_pattern = let pp_command = function | Include (_,_,mode,path) -> (* not precise, since path is absolute *) if mode = WithPreferences then - "include \"" ^ path ^ "\".\n" + "include \"" ^ path ^ "\"." else - "include' \"" ^ path ^ "\".\n" + "include' \"" ^ path ^ "\"." | Alias (_,s) -> pp_alias s | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) -> pp_interpretation dsc symbol arg_patterns cic_appl_pattern | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) -> pp_notation dir_opt l1_pattern assoc prec l2_pattern - diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 2309d8fb0..5ae773c49 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -177,13 +177,13 @@ let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm = let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in remove_closed_substs s -let enable_notations x = () (* function +let enable_notations = function | true -> CicNotation.set_active_notations (List.map fst (CicNotation.get_all_notations ())) | false -> CicNotation.set_active_notations [] -*) + let txt_of_cic_object ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n style ?flavour prefix obj diff --git a/helm/software/matita/contribs/procedural/Makefile.common b/helm/software/matita/contribs/procedural/Makefile.common index 9d322ddc0..92225d77d 100644 --- a/helm/software/matita/contribs/procedural/Makefile.common +++ b/helm/software/matita/contribs/procedural/Makefile.common @@ -18,15 +18,18 @@ $(DIR).opt opt all.opt: $(H)$(RM) $(LOG) $(H)$(BIN)matitac.opt $(MATITAOPTIONS) 2>> $(LOG) -%.ma %.mma: +%.ma: $(H)$(RM) $(LOG) - $(H)$(BIN)matitac $(MATITAOPTIONS) $@ 2>> $(LOG) -%.ma.opt: + $(H)$(BIN)matitac $(MATITAOPTIONS) $*.mma 2>> $(LOG) +%.mo: $(H)$(RM) $(LOG) - $(H)$(BIN)matitac.opt $(MATITAOPTIONS) $*.ma 2>> $(LOG) -%.mma.opt: + $(H)$(BIN)matitac $(MATITAOPTIONS) $*.ma 2>> $(LOG) +%.ma.opt: $(H)$(RM) $(LOG) $(H)$(BIN)matitac.opt $(MATITAOPTIONS) $*.mma 2>> $(LOG) +%.mo.opt: + $(H)$(RM) $(LOG) + $(H)$(BIN)matitac.opt $(MATITAOPTIONS) $*.ma 2>> $(LOG) clean: $(H)$(BIN)matitaclean $(MATITAOPTIONS) diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index 7e5b20860..e2bb6feb9 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -129,10 +129,6 @@ let eval_ast ?do_heavy_checks lexicon_status exception TryingToAdd of string exception EnrichedWithStatus of exn * LexiconEngine.status * GrafiteTypes.status -let out = ref ignore - -let set_callback f = out := f - let eval_from_stream ~first_statement_only ~include_paths ?do_heavy_checks ?(enforce_no_new_aliases=true) ?(watch_statuses=fun _ _ -> ()) lexicon_status grafite_status str cb @@ -160,7 +156,6 @@ let eval_from_stream ~first_statement_only ~include_paths false, lexicon_status, grafite_status, (((grafite_status,lexicon_status),None)::statuses) | GrafiteParser.LSome ast -> - !out ast; cb grafite_status ast; let new_statuses = eval_ast ?do_heavy_checks lexicon_status diff --git a/helm/software/matita/matitaEngine.mli b/helm/software/matita/matitaEngine.mli index 9429b00e6..d5dcddd61 100644 --- a/helm/software/matita/matitaEngine.mli +++ b/helm/software/matita/matitaEngine.mli @@ -57,6 +57,3 @@ val eval_from_stream : GrafiteAst.statement -> unit) -> ((GrafiteTypes.status * LexiconEngine.status) * (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list - -(* this callback is called on every grafite command *) -val set_callback: (GrafiteParser.ast_statement -> unit) -> unit diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 7a6d48663..6c3749db3 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -31,10 +31,6 @@ open GrafiteTypes 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 = @@ -60,7 +56,6 @@ 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 pp_statement stm = @@ -75,33 +70,31 @@ let dump f = let nl () = output_string och (pp_statement nl_ast) in MatitaMisc.out_preamble och; let grafite_parser_cb status = function - | G.Executable (_, G.Macro (_, G.Inline _)) -> () - | stm -> + | G.Executable (_, G.Macro (_, G.Inline (_, style, uri, prefix, flavour))) -> + let str = + ApplyTransformation.txt_of_inline_macro style prefix uri + ?flavour + ~map_unicode_to_tex: + (Helm_registry.get_bool "matita.paste_unicode_as_tex") + in + output_string och str + | stm -> output_string och (pp_statement stm); nl (); nl () in let lexicon_parser_cb status cmd = output_string och (pp_lexicon cmd); nl (); nl () in -(* - let matita_engine_cb = function - | G.Executable (_, G.Macro (_, G.Inline _)) - | G.Executable (_, G.Command (_, G.Include _)) -> () - | ast -> -*) - let matitac_lib_cb = output_string och in begin fun () -> + Helm_registry.set_bool "matita.moo" false; GrafiteParser.set_grafite_callback grafite_parser_cb; - GrafiteParser.set_lexicon_callback lexicon_parser_cb; -(* - MatitaEngine.set_callback matita_engine_cb; -*) - set_callback matitac_lib_cb + GrafiteParser.set_lexicon_callback lexicon_parser_cb end, begin fun x -> close_out och; GrafiteParser.set_grafite_callback (fun _ _ -> ()); GrafiteParser.set_lexicon_callback (fun _ _ -> ()); - set_callback ignore; x + Helm_registry.set_bool "matita.moo" true; + x end ;; @@ -243,18 +236,19 @@ let compile atstart options fname = | [] -> lexicon_status, grafite_status | ((grafite,lexicon),None)::_ -> lexicon, grafite | ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l) - with MatitaEngine.EnrichedWithStatus (GrafiteEngine.Macro (floc, f), lexicon, grafite) as exn -> match f (get_macro_context (Some grafite)) with | _, GrafiteAst.Inline (_, style, suri, prefix, flavour) -> - let str = +(* + 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 lexicon grafite |_-> raise exn in @@ -275,8 +269,7 @@ let compile atstart options fname = *) 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; -- 2.39.2