From 6a5e51c1cf9a56c74a8b53a9b8bc5aa686c9780e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 21 Aug 2008 10:31:16 +0000 Subject: [PATCH] basic support for imposed flavour in procedural object rendering --- .../acic_procedural/acic2Procedural.ml | 2 +- .../acic_procedural/acic2Procedural.mli | 2 +- .../components/binaries/transcript/grafite.ml | 2 +- helm/software/components/grafite/grafiteAst.ml | 4 ++-- helm/software/components/grafite/grafiteAstPp.ml | 15 +++++++++++++-- .../components/grafite_parser/grafiteParser.ml | 11 +++++++++-- helm/software/matita/applyTransformation.ml | 13 +++++++------ helm/software/matita/applyTransformation.mli | 16 ++++++++-------- helm/software/matita/matitaScript.ml | 4 ++-- helm/software/matita/matitacLib.ml | 10 ++++++---- 10 files changed, 50 insertions(+), 29 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index c95e815da..4d5e3a668 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -480,7 +480,7 @@ let proc_obj st = function (* interface functions ******************************************************) let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth - prefix anobj = + ?flavour prefix anobj = let st = { sorts = ids_to_inner_sorts; types = ids_to_inner_types; diff --git a/helm/software/components/acic_procedural/acic2Procedural.mli b/helm/software/components/acic_procedural/acic2Procedural.mli index 7d830447b..f0016cce2 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.mli +++ b/helm/software/components/acic_procedural/acic2Procedural.mli @@ -26,7 +26,7 @@ val procedural_of_acic_object: ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> - ?depth:int -> string -> Cic.annobj -> + ?depth:int -> ?flavour:Cic.object_flavour -> string -> Cic.annobj -> (Cic.annterm, Cic.annterm, Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) GrafiteAst.statement list diff --git a/helm/software/components/binaries/transcript/grafite.ml b/helm/software/components/binaries/transcript/grafite.ml index f6a082290..83b745980 100644 --- a/helm/software/components/binaries/transcript/grafite.ml +++ b/helm/software/components/binaries/transcript/grafite.ml @@ -83,7 +83,7 @@ let inline (kind, uri, prefix) = | T.Declarative -> G.Declarative | T.Procedural -> G.Procedural None in - command_of_macro (G.Inline (floc, kind, uri, prefix)) + command_of_macro (G.Inline (floc, kind, uri, prefix, None)) let out_alias och name uri = Printf.fprintf och "alias id \"%s\" = \"%s\".\n\n" name uri diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 5cc66743d..180d687c9 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -143,8 +143,8 @@ type 'term macro = | Check of loc * 'term | Hint of loc * bool | AutoInteractive of loc * 'term auto_params - | Inline of loc * presentation_style * string * string - (* URI or base-uri, name prefix *) + | Inline of loc * presentation_style * string * string * Cic.object_flavour option + (* URI or base-uri, name prefix, flavour *) (** To be increased each time the command type below changes, used for "safe" * marshalling *) diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index ccb061cd8..df436e709 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -258,6 +258,17 @@ let pp_macro ~term_pp = let prefix_pp prefix = if prefix = "" then "" else Printf.sprintf " \"%s\"" prefix in + let flavour_pp = function + | None -> "" + | Some `Definition -> "as definition" + | Some `MutualDefinition -> "as mutual" + | Some `Fact -> "as fact" + | Some `Lemma -> "as lemma" + | Some `Remark -> "as remark" + | Some `Theorem -> "as theorem" + | Some `Variant -> "as variant" + | Some `Axiom -> "as axiom" + in function (* Whelp *) | WInstance (_, term) -> "whelp instance " ^ term_pp term @@ -270,8 +281,8 @@ let pp_macro ~term_pp = | Hint (_, true) -> "hint rewrite" | Hint (_, false) -> "hint" | AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params - | Inline (_, style, suri, prefix) -> - Printf.sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix) + | Inline (_, style, suri, prefix, flavour) -> + Printf.sprintf "inline %s\"%s\"%s%s" (style_pp style) suri (prefix_pp prefix) (flavour_pp flavour) let pp_associativity = function | Gramext.LeftA -> "left associative" diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 26dd9b9e0..38a8667d3 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -452,6 +452,12 @@ EXTEND | [ IDENT "theorem" ] -> `Theorem ] ]; + inline_flavour: [ + [ attr = theorem_flavour -> attr + | [ IDENT "axiom" ] -> `Axiom + | [ IDENT "mutual" ] -> `MutualDefinition + ] + ]; inductive_spec: [ [ fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars; SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; @@ -502,13 +508,14 @@ EXTEND GrafiteAst.Check (loc, t) | [ IDENT "inline"]; style = OPT [ IDENT "procedural"; depth = OPT int -> depth ]; - suri = QSTRING; prefix = OPT QSTRING -> + suri = QSTRING; prefix = OPT QSTRING; + flavour = OPT [ IDENT "as"; attr = inline_flavour -> attr ]-> let style = match style with | None -> GrafiteAst.Declarative | Some depth -> GrafiteAst.Procedural depth in let prefix = match prefix with None -> "" | Some prefix -> prefix in - GrafiteAst.Inline (loc,style,suri,prefix) + GrafiteAst.Inline (loc,style,suri,prefix, flavour) | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") -> if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true) | IDENT "auto"; params = auto_params -> diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 0597fcf99..2a4624c21 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -161,7 +161,8 @@ let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm = remove_closed_substs s let txt_of_cic_object - ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n style prefix obj + ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas + n style ?flavour prefix obj = let get_aobj obj = try @@ -200,11 +201,11 @@ let txt_of_cic_object let script = Acic2Procedural.procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types - ?depth prefix aobj + ?depth ?flavour prefix aobj in "\n\n" ^ String.concat "" (List.map aux script) -let txt_of_inline_uri ~map_unicode_to_tex style suri prefix = +let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri = let print_exc = function | ProofEngineHelpers.Bad_pattern s as e -> Printexc.to_string e ^ " " ^ Lazy.force s @@ -215,7 +216,7 @@ let txt_of_inline_uri ~map_unicode_to_tex style suri prefix = let map uri = try txt_of_cic_object - ~map_unicode_to_tex 78 style prefix + ~map_unicode_to_tex 78 style ?flavour prefix (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri)) with | e -> @@ -224,7 +225,7 @@ let txt_of_inline_uri ~map_unicode_to_tex style suri prefix = in String.concat "" (List.map map sorted_uris) -let txt_of_inline_macro ~map_unicode_to_tex style name prefix = +let txt_of_inline_macro ~map_unicode_to_tex style ?flavour prefix name = let suri = if Librarian.is_uri name then name else let include_paths = @@ -235,7 +236,7 @@ let txt_of_inline_macro ~map_unicode_to_tex style name prefix = in baseuri ^ "/" in - txt_of_inline_uri ~map_unicode_to_tex style suri prefix + txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri (****************************************************************************) (* procedural_txt_of_cic_term *) diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index 4b0251743..06bea6cc6 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -64,19 +64,19 @@ val txt_of_cic_sequent_conclusion: map_unicode_to_tex:bool -> output_type:[`Pattern | `Term] -> int -> Cic.metasenv -> Cic.conjecture -> string -(* columns, rendering style, name prefix, object *) +(* columns, rendering style, flavour, name prefix, object *) val txt_of_cic_object: map_unicode_to_tex:bool -> - ?skip_thm_and_qed:bool -> - ?skip_initial_lambdas:int -> - int -> GrafiteAst.presentation_style -> string -> - Cic.obj -> + ?skip_thm_and_qed:bool -> ?skip_initial_lambdas:int -> + int -> GrafiteAst.presentation_style -> ?flavour:Cic.object_flavour -> + string -> Cic.obj -> string -(* presentation_style, uri or baseuri, name prefix *) +(* presentation_style, flavour, name prefix, uri or baseuri *) val txt_of_inline_macro: - map_unicode_to_tex:bool -> - GrafiteAst.presentation_style -> string -> string -> string + map_unicode_to_tex:bool -> GrafiteAst.presentation_style -> + ?flavour:Cic.object_flavour -> string -> string -> + string (* columns, rendering depth, context, term *) val procedural_txt_of_cic_term: diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 4fa7d9e5f..f769484c8 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -573,12 +573,12 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status ProofEngineTypes.Fail _ as exn -> raise exn (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *)) - | TA.Inline (_,style,suri,prefix) -> + | TA.Inline (_,style,suri,prefix,flavour) -> let str = ApplyTransformation.txt_of_inline_macro ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") - style suri prefix + style ?flavour prefix suri in [], str, String.length parsed_text diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index b33590a0a..99c132c11 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -259,11 +259,13 @@ let compile options fname = 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) -> + | _, GrafiteAst.Inline (_, style, suri, prefix, flavour) -> let str = - ApplyTransformation.txt_of_inline_macro style suri prefix - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") in + 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 |_-> raise exn -- 2.39.2