basic support for imposed flavour in procedural object rendering

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index c95e815daad5e4755f77f026f6df0c35ea6be0c1..4d5e3a668f9724267e68f2b1b3f1562e78a0b806 100644 (file)
--- 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 7d830447b6963f16ed3274e2124268dc75e5cc8d..f0016cce20c355ec8772769884d7fd110c4d6d6c 100644 (file)
--- 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 f6a08229013bd03ef0bb944feef917e458f242f5..83b745980ead119f83b76191ced70b16a2649013 100644 (file)
--- 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 5cc66743d7bdffa4ab8de2de7b8b3465ea3c169c..180d687c9282d314814e579e1a1ad6b14d18461b 100644 (file)
--- 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 ccb061cd89efa61e2b406e43b3798d585ee16ddb..df436e7097cefe67fb842f59414a9f3258ad6b12 100644 (file)
--- 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 26dd9b9e050ddb2707997ee69ea7cfb43978d3f0..38a8667d304ae511da33b6abf47971f178922726 100644 (file)
--- 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<def>>; 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 0597fcf99bc30f75c36a91f86944ff96f960f57b..2a4624c217b7531ae14bd7b42fcdd8c3a106c9cd 100644 (file)
--- 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 4b0251743407291e890801475b023135f2fc9c21..06bea6cc6b187719667c3ba5e63df5cbca096e96 100644 (file)
--- 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 4fa7d9e5f5389fb0c148de50a5672b2c86c4e5f1..f769484c87706e9d615a7f9aa508b5ba1d9430db 100644 (file)
--- 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 b33590a0ae95127a7afb7ae0dff0576342626cb0..99c132c11d27cf2a6f951ef71087bc26aadaf172 100644 (file)
--- 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