From: Luca Padovani Date: Fri, 23 May 2003 09:24:55 +0000 (+0000) Subject: * fix in optional argument for ocaml binding X-Git-Tag: submitted~36 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4b7e162d67a8d748f95c557e2a76ee9625a06291;p=helm.git * fix in optional argument for ocaml binding * fix in tml->mmlp stylehseet --- diff --git a/helm/DEVEL/mathml_editor/doc/spec.tex b/helm/DEVEL/mathml_editor/doc/spec.tex index a55f950c0..a9ccdc263 100644 --- a/helm/DEVEL/mathml_editor/doc/spec.tex +++ b/helm/DEVEL/mathml_editor/doc/spec.tex @@ -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\}\\|\quad\emptyset\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} diff --git a/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.cc b/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.cc index 14bab319d..8ab2a05cc 100644 --- a/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.cc +++ b/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.cc @@ -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 diff --git a/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.h b/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.h index 7c41ece31..cb01155ad 100644 --- a/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.h +++ b/helm/DEVEL/mathml_editor/ocaml/c_mathml_editor.h @@ -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*); diff --git a/helm/DEVEL/mathml_editor/ocaml/i_mathml_editor.ml b/helm/DEVEL/mathml_editor/ocaml/i_mathml_editor.ml index c98c2fbe1..d865898d6 100644 --- a/helm/DEVEL/mathml_editor/ocaml/i_mathml_editor.ml +++ b/helm/DEVEL/mathml_editor/ocaml/i_mathml_editor.ml @@ -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" diff --git a/helm/DEVEL/mathml_editor/ocaml/mathml_editor.ml b/helm/DEVEL/mathml_editor/ocaml/mathml_editor.ml index 04adc9450..a49ea436e 100644 --- a/helm/DEVEL/mathml_editor/ocaml/mathml_editor.ml +++ b/helm/DEVEL/mathml_editor/ocaml/mathml_editor.ml @@ -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 diff --git a/helm/DEVEL/mathml_editor/ocaml/mathml_editor.mli b/helm/DEVEL/mathml_editor/ocaml/mathml_editor.mli index f294fcfdd..aa0278522 100644 --- a/helm/DEVEL/mathml_editor/ocaml/mathml_editor.mli +++ b/helm/DEVEL/mathml_editor/ocaml/mathml_editor.mli @@ -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 -> diff --git a/helm/DEVEL/mathml_editor/ocaml/ml_mathml_editor.c b/helm/DEVEL/mathml_editor/ocaml/ml_mathml_editor.c index e4cda57e1..c74dfd01c 100644 --- a/helm/DEVEL/mathml_editor/ocaml/ml_mathml_editor.c +++ b/helm/DEVEL/mathml_editor/ocaml/ml_mathml_editor.c @@ -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, diff --git a/helm/DEVEL/mathml_editor/xsl/tml-mmlp.xsl b/helm/DEVEL/mathml_editor/xsl/tml-mmlp.xsl index 9694df75f..cd4ee601f 100644 --- a/helm/DEVEL/mathml_editor/xsl/tml-mmlp.xsl +++ b/helm/DEVEL/mathml_editor/xsl/tml-mmlp.xsl @@ -918,6 +918,18 @@ + + + + + + + + + _ + + +