]> matita.cs.unibo.it Git - helm.git/commitdiff
* fix in optional argument for ocaml binding
authorLuca Padovani <luca.padovani@unito.it>
Fri, 23 May 2003 09:24:55 +0000 (09:24 +0000)
committerLuca Padovani <luca.padovani@unito.it>
Fri, 23 May 2003 09:24:55 +0000 (09:24 +0000)
* fix in tml->mmlp stylehseet

helm/DEVEL/mathml_editor/doc/spec.tex
helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.cc
helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.h
helm/DEVEL/mathml_editor/ocaml/i_mathml_editor.ml
helm/DEVEL/mathml_editor/ocaml/mathml_editor.ml
helm/DEVEL/mathml_editor/ocaml/mathml_editor.mli
helm/DEVEL/mathml_editor/ocaml/ml_mathml_editor.c
helm/DEVEL/mathml_editor/xsl/tml-mmlp.xsl

index a55f950c00cca5d19040031a01788b8ba670b015..a9ccdc2637a59eefd9bc8c2f311e9073670eb86a 100644 (file)
@@ -858,6 +858,7 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
 \newcommand{\FSEM}[2]{\mathcal{F}\llbracket#1\rrbracket(#2)}
 \newcommand{\PARENT}[1]{\mathit{parent}(#1)}
 \newcommand{\CHILDREN}[1]{\mathit{children}(#1)}
+\newcommand{\CHILD}[1]{\mathit{child}(#1)}
 \newcommand{\ANCESTORS}[1]{\mathit{ancestors}(#1)}
 \newcommand{\DESCENDANTS}[1]{\mathit{descendants}(#1)}
 \newcommand{\HASATTRIBUTE}[2]{\mathit{hasAttribute}(#1,#2)}
@@ -870,15 +871,18 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
 \newcommand{\PREDICATE}[1]{\mathit{predicate}(#1)}
 \newcommand{\IFV}[3]{\begin{array}[t]{@{}l}\mathbf{if}~#1~\mathbf{then}\\\quad#2\\\mathbf{else}\\\quad#3\end{array}}
 \newcommand{\IFH}[3]{\mathbf{if}~#1~\mathbf{then}~#2~\mathbf{else}~#3}
-\newcommand{\TRUE}{\mathit{true}}
-\newcommand{\FALSE}{\mathit{false}}
+\newcommand{\TRUE}{\mathbf{true}}
+\newcommand{\FALSE}{\mathbf{false}}
 \newcommand{\FUN}[2]{\lambda#1.#2}
 \newcommand{\LET}[3]{\mathbf{let}~#1=#2~\mathbf{in}~#3}
+\newcommand{\REC}[2]{\mathbf{rec}~#1=#2}
 \newcommand{\APPLY}[2]{(#1\;#2)}
+\newcommand{\APPLYX}[3]{(#1\;#2\;#3)}
 \newcommand{\AND}{\wedge}
 \newcommand{\OR}{\vee}
 \newcommand{\AAND}{\,\vec{\AND}\,}
 \newcommand{\AOR}{\,\vec{\OR}\,}
+\newcommand{\MATCH}[4]{\begin{array}[t]{@{}c@{~\to~}l@{}l@{}}\multicolumn{2}{@{}l@{}}{\mathbf{match}~#1~\mathbf{with}}\\\phantom{|}\quad\{#2\}&#3\\|\quad\emptyset&#4\end{array}}
 
 \[
 \begin{array}{rcl}
@@ -891,29 +895,23 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
   \CSEM{c_1\&c_2}{x} &=& \CSEM{c_1}{x} \cap \CSEM{c_2}{x}\\
   \CSEM{c_1\mid c_2}{x} &=& \CSEM{c_1}{x} \cup \CSEM{c_2}{x}\\
   \CSEM{c+}{x} &=& \CSEM{c}{x} \cup \CSEM{c+}{\CSEM{c}{x}}\\
-  \CSEM{c?}{x} &=& \CSEM{.\mid c}{x}\\
+  \CSEM{c?}{x} &=& \{x\}\cup\CSEM{c}{x}\\
   \CSEM{c*}{x} &=& \CSEM{{c+}?}{x}\\[3ex]
   \QSEM{c}{x} &=& \CSEM{c}{x}\ne\emptyset\\
   \QSEM{!c}{x} &=& \CSEM{c}{x}=\emptyset\\
-  \QSEM{.}{x} &=& \TRUE\\
-  \QSEM{\langle*\rangle}{x} &=& \ISELEMENT{x}\\
-  \QSEM{\langle n\rangle}{x} &=& \ISELEMENT{x}\wedge\NAME{x}=n\\
-  \QSEM{@n}{x} &=& \ISELEMENT{x}\wedge\HASATTRIBUTE{x}{n}\\
-  \QSEM{@n=v}{x} &=& \ISELEMENT{x}\wedge\ATTRIBUTE{x}{n}=v\\
-  \QSEM{[p_1\#p_2]}{x} &=& \ISELEMENT{x}\wedge\LSEM{p_1}{\PREV{x}}\wedge\RSEM{p_2}{\NEXT{x}}\\[3ex]
+  \QSEM{\langle*\rangle}{x} &=& \TRUE\\
+  \QSEM{\langle n\rangle}{x} &=& \NAME{x}=n\\
+  \QSEM{@n}{x} &=& \HASATTRIBUTE{x}{n}\\
+  \QSEM{@n=v}{x} &=& \ATTRIBUTE{x}{n}=v\\
+  \QSEM{[p_1\#p_2]}{x} &=& \LSEM{p_1}{\PREV{x}}\wedge\RSEM{p_2}{\NEXT{x}}\\[3ex]
   \LSEM{}{\alpha} &=& \TRUE\\
   \LSEM{\cent}{\alpha} &=& \alpha=\emptyset\\
-  \LSEM{p\;q}{\emptyset} &=& \mathit{false}\\
+  \LSEM{p\;q}{\emptyset} &=& \FALSE\\
   \LSEM{p\;q}{\{x\}} &=& \QSEM{q}{x}\wedge\LSEM{p}{\PREV{x}}\\[3ex]
   \RSEM{}{\alpha} &=& \TRUE\\
   \RSEM{\$}{\alpha} &=& \alpha=\emptyset\\
-  \RSEM{q\;p}{\emptyset} &=& \mathit{false}\\
-  \RSEM{q\;p}{\{x\}} &=& \QSEM{q}{x}\wedge\RSEM{p}{\NEXT{x}}\\
-\end{array}
-\]
-
-\[
-\begin{array}{rcl}
+  \RSEM{q\;p}{\emptyset} &=& \FALSE\\
+  \RSEM{q\;p}{\{x\}} &=& \QSEM{q}{x}\wedge\RSEM{p}{\NEXT{x}}\\[3ex]
   \PREDICATE{q} &=& \TRUE\\
   \PREDICATE{..} &=& \FALSE\\
   \PREDICATE{/} &=& \FALSE\\
@@ -929,27 +927,47 @@ cursor with \ONODE{}, append $\tadvance$ after the \ONODE{} node
 
 \[
 \begin{array}{rcl}
-  \PSEM{q} &=& \FUN{x}{\QSEM{q}{x}} \\
-  \PSEM{..} &=& \FUN{x}{\PARENT{x}\ne\emptyset}\\
-  \PSEM{/} &=& \FUN{x}{\CHILDREN{x}\ne\emptyset}\\
-  \PSEM{c_1\;c_2} &=& \IFV{\PREDICATE{c_1}}{\FUN{x}{(\PSEM{c_1}\;x)\wedge(\PSEM{c_2}\;x)}}{\FSEM{c_1}{\PSEM{c_2},\FUN{\_}{\FALSE}}}\\
+  \PSEM{q} &=& \FUN{x}{\APPLY{\QSEM{q}{}}{x}} \\
+  \PSEM{..} &=& \FUN{x}{\neg\APPLY{\mathit{null}}{\PARENT{x}}}\\
+  \PSEM{/} &=& \FUN{x}{\neg\APPLY{\mathit{null}}{\CHILD{x}}}\\
   \PSEM{(c)} &=& \PSEM{c}\\
+  \PSEM{\{c:\alpha\}} &=& \FUN{x}{\APPLY{\PSEM{c}}{x}\AAND\APPLY{\alpha}{x}}\\
+  \PSEM{c_1\;c_2} &=& \IFV{\PREDICATE{c_1}}{\FUN{x}{(\PSEM{c_1}\;x)\wedge(\PSEM{c_2}\;x)}}{\FSEM{c_1}{\PSEM{c_2},\FUN{\_}{\FALSE}}}\\
   \PSEM{c_1\&c_2} &=& \IFV{\PREDICATE{c_1}\wedge\PREDICATE{c_2}}{\FUN{x}{(\PSEM{c_1}\;x)\wedge(\PSEM{c_2}\;x)}}{\FSEM{c_1\&c_2}{\FUN{\_}{\TRUE},\FUN{\_}{\FALSE}}}\\
   \PSEM{c_1\mid c_2} &=& \FUN{x}{(\PSEM{c_1}\;x)\vee(\PSEM{c_2}\;x)}\\
   \PSEM{c+} &=& \PSEM{c}\\
   \PSEM{c?} &=& \FUN{\_}{\TRUE}\\
   \PSEM{c*} &=& \FUN{\_}{\TRUE}\\[3ex]
   \FSEM{q}{t,f} &=& \FUN{x}{(\APPLY{\PSEM{q}}{x}\AAND\APPLY{t}{x})\AOR\APPLY{f}{x}}\\
-  \FSEM{..}{t,f} &=& \FUN{x}{\LET{\{y\}}{\PARENT{x}}{\APPLY{t}{y}\AOR\APPLY{f}{x}}}\\
-  \FSEM{/}{t,f} &=& \FUN{x}{(\vee_{y\in\CHILDREN{x}} \APPLY{t}{y})\AOR\APPLY{f}{x}}\\
+  \FSEM{..}{t,f} &=& \FUN{x}{\MATCH{\PARENT{x}}{y}{\APPLY{t}{y}}{\APPLY{f}{x}}}\\
+%  \FSEM{/}{t,f} &=& \FUN{x}{(\vee_{y\in\CHILDREN{x}} \APPLY{t}{y})\AOR\APPLY{f}{x}}\\
+  \FSEM{/}{t,f} &=& \FUN{x}{\APPLYX{\mathit{exists}}{t}{\CHILD{x}}\AOR\APPLY{f}{x}}\\
   \FSEM{(c)}{t,f} &=& \FSEM{c}{t,f}\\
-  \FSEM{c_1\;c_2}{t,f} &=& \FSEM{c_1}{\FSEM{c_2}{t,\FUN{\_}{\FALSE}},f}\\
-  \FSEM{c_1\&c_2}{t,f} &=& \FUN{x}{\APPLY{\FSEM{c_1}{\FUN{y}{\APPLY{t}{y}\AAND\APPLY{\FSEM{c_2}{\FUN{z}{z=y},\FUN{\_}{\FALSE}}}{x}},f}}{x}}\\
+  \FSEM{\{c:\alpha\}}{t,f} &=& \FSEM{c}{\FUN{x}{\PSEM{c}\AAND\APPLY{\alpha}{x}\AAND\APPLY{t}{x},f}}\\
+  \FSEM{c_1\;c_2}{t,f} &=& \FUN{x}{\APPLY{\FSEM{c_1}{\FSEM{c_2}{t,\FUN{\_}{\APPLY{f}{x}}},f}}{x}}\\
+  \FSEM{c_1\&c_2}{t,f} &=& \FUN{x}{\APPLY{\FSEM{c_1}{\FUN{y}{\APPLY{\FSEM{c_2}{\FUN{z}{(y=z)\AAND\APPLY{t}{z}},\FUN{\_}{\APPLY{f}{x}}}}{x}},f}}{x}}\\
   \FSEM{c_1\mid c_2}{t,f} &=& \FSEM{c_1}{t,\FSEM{c_2}{t,f}}\\
   \FSEM{c+}{t,f} &=& \FSEM{c}{\FSEM{c+}{t,t},f}\\
   \FSEM{c?}{t,f} &=& \FSEM{c}{t,t}\\
-  \FSEM{c*}{t,f} &=& \FSEM{{c+}?}{t,f}\\
+  \FSEM{c*}{t,f} &=& \FSEM{{c+}?}{t,f}\\[3ex]
+  \QSEM{c}{} &=& \PSEM{c}\\
+  \QSEM{!c}{} &=& \FUN{x}{\neg\APPLY{\PSEM{c}}{x}}\\
+  \QSEM{\langle*\rangle}{} &=& \FUN{\_}{\TRUE}\\
+  \QSEM{\langle n\rangle}{} &=& \FUN{x}{\NAME{x}=n}\\
+  \QSEM{@n}{} &=& \FUN{x}{\HASATTRIBUTE{x}{n}}\\
+  \QSEM{@n=v}{} &=& \FUN{x}{\ATTRIBUTE{x}{n}=v}\\
+  \QSEM{[p_1\#p_2]}{} &=& \FUN{x}{\APPLY{\LSEM{p_1}{}}{\PREV{x}}\wedge\APPLY{\RSEM{p_2}{}}{\NEXT{x}}}\\[3ex]
+  \LSEM{}{} &=& \FUN{\_}{\TRUE}\\
+  \LSEM{\cent}{} &=& \mathit{null}\\
+  \LSEM{p\;q}{} &=& \FUN{x}{\MATCH{x}{y}{\QSEM{q}{y}\AAND\APPLY{\LSEM{p}}{\PREV{y}}}{\FALSE}}\\
+  \RSEM{}{} &=& \FUN{\_}{\TRUE}\\
+  \RSEM{\$}{} &=& \mathit{null}\\
+  \RSEM{p\;q}{} &=& \FUN{x}{\MATCH{x}{y}{\QSEM{q}{y}\AAND\APPLY{\RSEM{p}}{\NEXT{y}}}{\FALSE}}\\
+  \mathit{null} &=& \FUN{x}{\MATCH{x}{\_}{\FALSE}{\TRUE}}\\
+  \mathit{exists} &=& \FUN{t}{\REC{a}{\FUN{x}{\MATCH{x}{y}{\APPLY{t}{y}\AOR\APPLY{a}{\NEXT{x}}}{\FALSE}}}}
 \end{array}
 \]
 
+
+
 \end{document}
index 14bab319d455df313b45d9c146889739a6979bb4..8ab2a05cc095c6ee6fdb3c6d9b9c41fb5004ce52 100644 (file)
@@ -29,6 +29,7 @@
 #include "TDictionary.hh"
 #include "CMathMLFactoryXSLT.hh"
 #include "TPushLexer.hh"
+#include "LPushLexer.hh"
 #include "TPushParser.hh"
 
 class CCallbackLogger : public ALogger
@@ -59,7 +60,7 @@ CCallbackLogger::message(Level l, const std::string& s)
 
 struct Editor
 {
-  Editor(const char*, const char*, const char*, void (*)(int, const char*, void*), void*);
+  Editor(const char*, const char*, const char*, void (*)(int, const char*, void*), void*, bool);
   ~Editor();
 
   ALogger*        logger;
@@ -72,7 +73,7 @@ struct Editor
 };
 
 Editor::Editor(const char* dict_uri, const char* mml_uri, const char* tex_uri,
-              void (*cb)(int, const char*, void*), void* data)
+              void (*cb)(int, const char*, void*), void* data, bool alt)
 {
   assert(dict_uri);
   assert(mml_uri);
@@ -88,7 +89,8 @@ Editor::Editor(const char* dict_uri, const char* mml_uri, const char* tex_uri,
   tml_tex = new DOMX::XSLTStylesheet(tex);
   factory = new CMathMLFactoryXSLT(*logger, *tml_mml);
   parser = new TPushParser(*logger, *factory, *dictionary);
-  lexer = new TPushLexer(*logger, *parser);
+  if (alt) lexer = new LPushLexer(*logger, *parser);
+  else lexer = new TPushLexer(*logger, *parser);
 }
 
 Editor::~Editor()
@@ -121,13 +123,14 @@ c_mathml_editor_get_default_tex_stylesheet_path()
 }
 
 extern "C" Editor*
-c_mathml_editor_new(const char* dictionary_uri,
+c_mathml_editor_new(bool alt,
+                   const char* dictionary_uri,
                    const char* tml_mml_uri,
                    const char* tml_tex_uri,
                    void (*log_message_cb)(int, const char*, void*),
                    void* user_data)
 {
-  return new Editor(dictionary_uri, tml_mml_uri, tml_tex_uri, log_message_cb, user_data);
+  return new Editor(dictionary_uri, tml_mml_uri, tml_tex_uri, log_message_cb, user_data, alt);
 }
 
 extern "C" void
index 7c41ece31087129d30ee4b9525fc3b3bfe65abbe..cb01155adf9747b7d988387b3561677eb921c82c 100644 (file)
@@ -33,7 +33,7 @@ typedef struct Editor Editor;
 const char*    c_mathml_editor_get_default_dictionary_path(void);
 const char*    c_mathml_editor_get_default_mathml_stylesheet_path(void);
 const char*    c_mathml_editor_get_default_tex_stylesheet_path(void);
-Editor*        c_mathml_editor_new(const char*, const char*, const char*, void (*)(int, const char*, void*), void*);
+Editor*        c_mathml_editor_new(int, const char*, const char*, const char*, void (*)(int, const char*, void*), void*);
 void           c_mathml_editor_destroy(Editor*);
 int            c_mathml_editor_freeze(Editor*);
 int            c_mathml_editor_thaw(Editor*);
index c98c2fbe128dae895b4d7a00cec8d9bd7888072a..d865898d614bb74a811a5a3f2a50c3f0ef8e922f 100644 (file)
@@ -34,13 +34,15 @@ external get_default_mathml_stylesheet_path : unit -> string
 external get_default_tex_stylesheet_path : unit -> string
   = "ml_mathml_editor_get_default_tex_stylesheet_path"
 
-external create : 
+external raw_create : 
+  alt_lexer:bool ->
   dictionary_uri: string ->
   mml_uri: string -> 
-  tex_uri: string ->
+  tml_uri: string ->
   log:(int -> string -> unit) ->
   t
   = "ml_mathml_editor_new"
+let create ?(alt_lexer=false) = raw_create ~alt_lexer
 
 external freeze : editor:t -> bool
   = "ml_mathml_editor_freeze"
index 04adc9450b6dc0081e877b7491b62dc2c29dd6bb..a49ea436e452e90cf9fece827567a60b5a4cbc56 100644 (file)
@@ -32,8 +32,8 @@ let default_mathml_stylesheet_path = I_mathml_editor.get_default_mathml_styleshe
 let default_tex_stylesheet_path = I_mathml_editor.get_default_tex_stylesheet_path ()
 ;;
 
-let create ~dictionary_uri ~mml_uri ~tml_uri ~log =
-  I_mathml_editor.create dictionary_uri mml_uri tml_uri log
+let create ?(alt_lexer=false) ~dictionary_uri ~mml_uri ~tml_uri ~log =
+  I_mathml_editor.create ~alt_lexer ~dictionary_uri ~mml_uri ~tml_uri ~log
 ;;
 
 let freeze = I_mathml_editor.freeze
index f294fcfdd34f66fad9815277d8060f9488f42adc..aa0278522d6f98c87c9322025dcac2c0359378f0 100644 (file)
@@ -28,6 +28,7 @@ val default_mathml_stylesheet_path : string
 val default_tex_stylesheet_path : string
 
 val create :
+  ?alt_lexer:bool ->
   dictionary_uri: string ->
   mml_uri: string ->
   tml_uri: string ->
index e4cda57e137532beced8e8ba77b83feb18d7795f..c74dfd01cf4b02aebe237e61dd447353389c28ec 100644 (file)
@@ -88,7 +88,8 @@ ml_mathml_editor_get_default_tex_stylesheet_path(value unit)
 }
 
 value
-ml_mathml_editor_new(value dictionary_uri,
+ml_mathml_editor_new(value alt,
+                    value dictionary_uri,
                     value tml_mml_uri,
                     value tml_tex_uri,
                     value log_message_cb)
@@ -106,7 +107,8 @@ ml_mathml_editor_new(value dictionary_uri,
   value v = alloc_custom(&ops, sizeof(ml_Editor*), 0, 1);
   ml_Editor** ml_editor_ref = (ml_Editor**) Data_custom_val(v);
   ml_Editor* ml_editor = *ml_editor_ref = malloc(sizeof(ml_Editor));
-  ml_editor->c_editor = c_mathml_editor_new(String_val(dictionary_uri),
+  ml_editor->c_editor = c_mathml_editor_new(Bool_val(alt),
+                                           String_val(dictionary_uri),
                                            String_val(tml_mml_uri),
                                            String_val(tml_tex_uri),
                                            ml_mathml_editor_log_callback,
index 9694df75fbcac111aac2df1a9653fffc9b320a14..cd4ee601fc516f044ff3bc07aa91065b635b347e 100644 (file)
     </m:mstyle>
   </xsl:template>
 
+  <xsl:template match="tml:c[@name='_']">
+<!-- _ -->
+    <m:mi>
+      <xsl:if test="@id">
+        <xsl:attribute name="xref">
+          <xsl:value-of select="@id"/>
+        </xsl:attribute>
+      </xsl:if>
+      <xsl:text>_</xsl:text>
+    </m:mi>
+  </xsl:template>
+
   <xsl:template match="tml:c[@name=',']">
 <!-- , -->
     <m:mspace width="thinmathspace">