]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/searchEngine/html/grammar.html
Branch V7_3_new_exportation merged.
[helm.git] / helm / searchEngine / html / grammar.html
diff --git a/helm/searchEngine/html/grammar.html b/helm/searchEngine/html/grammar.html
new file mode 100644 (file)
index 0000000..a18b27c
--- /dev/null
@@ -0,0 +1,76 @@
+<HTML>
+<HEAD>
+</HEAD>
+<BODY>
+<A NAME="string">
+<P><B>&lt;string&gt;</B>::= '"' [ "\" . | '^ " \' ] * '"'</A>
+<A NAME="path">
+<P><B>&lt;path&gt;</B>::= &lt;<A HREF="#string">string</A>&gt; [ "/" &lt;<A HREF="#string">string</A>&gt; ] *</A>
+<A NAME="string_list">
+<P><B>&lt;string_list&gt;</B>::= &lt;<A HREF="#string">string</A>&gt; [ "," &lt;<A HREF="#string">string</A>&gt; ] *</A>
+<A NAME="alpha">
+<P><B>&lt;alpha&gt;</B>::= [ 'A - Z' | 'a - z' |' :_' ] + </A>
+<A NAME="number">
+<P><B>&lt;number&gt;</B>::= [ '0 - 9' ] + </A>
+<A NAME="id">
+<P><B>&lt;id&gt;</B>::= &lt;<A HREF="#alpha">alpha</A>&gt; [ &lt;<A HREF="#alpha">alpha</A>&gt; | &lt;<A HREF="#number">number</A>&gt; ] * </A>
+<A NAME="rvar">
+<P><B>&lt;rvar&gt;</B>::= "@" &lt;<A HREF="#id">id</A>&gt; </A>
+<A NAME="svar">
+<P><B>&lt;svar&gt;</B>::= "%" &lt;<A HREF="#id">id</A>&gt; </A>
+<A NAME="vvar">
+<P><B>&lt;vvar&gt;</B>::= "$" &lt;<A HREF="#id">id</A>&gt; </A>
+<A NAME="refine">
+<P><B>&lt;refine&gt;</B>::= [ "sub" | "super" ] ? </A>
+<A NAME="qualifier">
+<P><B>&lt;qualifier&gt;</B>::= [ "inverse" ] ? &lt;<A HREF="#refine">refine</A>&gt; &lt;<A HREF="#path">path</A>&gt; </A>
+<A NAME="assign">
+<P><B>&lt;assign&gt;</B>::= &lt;<A HREF="#vvar">vvar</A>&gt; "&lt;-" &lt;<A HREF="#path">path</A>&gt; </A>
+<A NAME="attr_list">
+<P><B>&lt;attr_list&gt;</B>::= [ "attr" &lt;<A HREF="#assign">assign</A>&gt; [ "," &lt;<A HREF="#assign">assign</A>&gt;] * ] ? </A>
+<A NAME="set">
+<P><B>&lt;set&gt;</B>::= "ref" &lt;<A HREF="#val">val</A>&gt; </A><BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| "pattern" &lt;<A HREF="#val">val</A>&gt;<BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| &lt;<A HREF="#svar">svar</A>&gt;<BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| &lt;<A HREF="#rvar">rvar</A>&gt;<BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| "(" &lt;<A HREF="#set">set</A>&gt; ")"<BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| "relation" &lt;<A HREF="#qualifier">qualifier</A>&gt; &lt;<A HREF="#val">val</A>&gt; &lt;<A HREF="#attr_list">attr_list</A>&gt;<BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| "select" &lt;<A HREF="#rvar">rvar</A>&gt; "in" &lt;<A HREF="#set">set</A>&gt; "where" &lt;<A HREF="#boole">boole</A>&gt;<BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| &lt;<A HREF="#set">set</A>&gt; [ "union" | "intersect" | "diff" ] &lt;<A HREF="#set">set</A>&gt;<BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| "let" &lt;<A HREF="#svar">svar</A>&gt; "be" &lt;<A HREF="#set">set</A>&gt; "in" &lt;<A HREF="#set">set</A>&gt; <BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| "let" &lt;<A HREF="#vvar">vvar</A>&gt; "be" &lt;<A HREF="#val">val</A>&gt; "in" &lt;<A HREF="#set">set</A>&gt; <BR> </A>
+<A NAME="boole">
+<P><B>&lt;boole&gt;</B>::= [ "false" | "true" ] </A><BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| "(" &lt;<A HREF="#boole">boole</A>&gt; ")"<BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| [ "not" | "ex" ] &lt;<A HREF="#boole">boole</A>&gt; <BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| &lt;<A HREF="#boole">boole</A>&gt; [ "and" | "or" ] &lt;<A HREF="#boole">boole</A>&gt; <BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| &lt;<A HREF="#val">val</A>&gt; [ "sub" | "meet" | "eq" ] &lt;<A HREF="#val">val</A>&gt; <BR> </A>
+<A NAME="val">
+<P><B>&lt;val&gt;</B>::= "{" [ &lt;<A HREF="#string_list">string_list</A>&gt; ] ? "}" </A><BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| &lt;<A HREF="#string">string</A>&gt;<BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| "refof" &lt;<A HREF="#set">set</A>&gt;<BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| &lt;<A HREF="#rvar">rvar</A>&gt; "." &lt;<A HREF="#vvar">vvar</A>&gt;<BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| &lt;<A HREF="#vvar">vvar</A>&gt;<BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| "(" &lt;<A HREF="#val">val</A>&gt; ")"<BR>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
+| "property" &lt;<A HREF="#qualifier">qualifier</A>&gt; &lt;<A HREF="#val">val</A>&gt;</A>
+</BODY>
+</HTML>
\ No newline at end of file