From: Claudio Sacerdoti Coen Date: Mon, 23 Jun 2003 15:58:50 +0000 (+0000) Subject: Branch V7_3_new_exportation merged. X-Git-Tag: V7_3_new_exportation_merged~2 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=dedb202eeeac7293c51dbf31a302d0d3dd24af95 Branch V7_3_new_exportation merged. --- diff --git a/helm/searchEngine/html/aliaslist.html b/helm/searchEngine/html/aliaslist.html new file mode 100644 index 000000000..d030ea41e --- /dev/null +++ b/helm/searchEngine/html/aliaslist.html @@ -0,0 +1,89 @@ + + + + + +
+alias + +
+
+ +
+
+
+ + diff --git a/helm/searchEngine/html/almost_blank.html b/helm/searchEngine/html/almost_blank.html new file mode 100644 index 000000000..05204a549 --- /dev/null +++ b/helm/searchEngine/html/almost_blank.html @@ -0,0 +1,5 @@ + + +Are you lost? Consult the on-line manual + + diff --git a/helm/searchEngine/html/blank.html b/helm/searchEngine/html/blank.html new file mode 100644 index 000000000..3334d0b61 --- /dev/null +++ b/helm/searchEngine/html/blank.html @@ -0,0 +1,4 @@ + + + + diff --git a/helm/searchEngine/html/boole.html b/helm/searchEngine/html/boole.html new file mode 100644 index 000000000..67024321b --- /dev/null +++ b/helm/searchEngine/html/boole.html @@ -0,0 +1,77 @@ + + + + + +

+ +

+

Select one of the following:

+
+
+ ( [boole] )
+ [boole]
+ [boole] [boole]
+ [val] +[val]
+
+ +
+ + \ No newline at end of file diff --git a/helm/searchEngine/html/constraints_choice_template.html b/helm/searchEngine/html/constraints_choice_template.html new file mode 100644 index 000000000..c81a8d74d --- /dev/null +++ b/helm/searchEngine/html/constraints_choice_template.html @@ -0,0 +1,18 @@ + + + Refine the Constraints + + + +
+ You can now proceed using the default generated constraints or you + can refine them by hand before going on.

+ + + @FORM@ +
+
+ + diff --git a/helm/searchEngine/html/editor.html b/helm/searchEngine/html/editor.html new file mode 100644 index 000000000..1e6afe7d0 --- /dev/null +++ b/helm/searchEngine/html/editor.html @@ -0,0 +1,122 @@ + + + + + + + +
+
+ +
 +
+
+
+
+ + + + + + diff --git a/helm/searchEngine/html/editorpdq.html b/helm/searchEngine/html/editorpdq.html new file mode 100644 index 000000000..21e803906 --- /dev/null +++ b/helm/searchEngine/html/editorpdq.html @@ -0,0 +1,90 @@ + + + + + +
+ Your list of alias. + +
+
Your expression.
+ + + +
+ + + diff --git a/helm/searchEngine/html/expnamedsubst.html b/helm/searchEngine/html/expnamedsubst.html new file mode 100644 index 000000000..3db7acaba --- /dev/null +++ b/helm/searchEngine/html/expnamedsubst.html @@ -0,0 +1,78 @@ + + + + + +You must now enter a list of named_subst. A named_subst is an Id or a Varuri followed by ":=" followed by an expression. +You may enter as many of them as you want (even none), after each one click the button "add" or press enter and it will be added. When you are done, click "done". +
+
+ Insert here the Id or the Uri you want to add. + +
+ +
+ +
+ + diff --git a/helm/searchEngine/html/expr.html b/helm/searchEngine/html/expr.html new file mode 100644 index 000000000..3e302b8b2 --- /dev/null +++ b/helm/searchEngine/html/expr.html @@ -0,0 +1,60 @@ + + + + + +You are entering an expression. Select one of the following. +
+\[Genid][Expr].[Expr]
+![Genid]:[Expr].[Expr]
+[Expr]->[Expr]
+([Expr])->[Expr]
+
+ ( [Expr list] )
+
+ +
+ + \ No newline at end of file diff --git a/helm/searchEngine/html/genid.html b/helm/searchEngine/html/genid.html new file mode 100644 index 000000000..1ca94c4cf --- /dev/null +++ b/helm/searchEngine/html/genid.html @@ -0,0 +1,27 @@ + + + + + +You are now entering a Genid. It may be a simple Id, or an Uri followed by nothing or by an Exp_Named_Subst. +
+ Insert here the Id +
+ Or insert here the Uri. The uri may not be a Conuri.
+ +
+ + diff --git a/helm/searchEngine/html/grammar.html b/helm/searchEngine/html/grammar.html new file mode 100644 index 000000000..a18b27cd7 --- /dev/null +++ b/helm/searchEngine/html/grammar.html @@ -0,0 +1,76 @@ + + + + + +

<string>::= '"' [ "\" . | '^ " \' ] * '"' + +

<path>::= <string> [ "/" <string> ] * + +

<string_list>::= <string> [ "," <string> ] * + +

<alpha>::= [ 'A - Z' | 'a - z' |' :_' ] + + +

<number>::= [ '0 - 9' ] + + +

<id>::= <alpha> [ <alpha> | <number> ] * + +

<rvar>::= "@" <id> + +

<svar>::= "%" <id> + +

<vvar>::= "$" <id> + +

<refine>::= [ "sub" | "super" ] ? + +

<qualifier>::= [ "inverse" ] ? <refine> <path> + +

<assign>::= <vvar> "<-" <path> + +

<attr_list>::= [ "attr" <assign> [ "," <assign>] * ] ? + +

<set>::= "ref" <val>
+                 +| "pattern" <val>
+                 +| <svar>
+                 +| <rvar>
+                 +| "(" <set> ")"
+                 +| "relation" <qualifier> <val> <attr_list>
+                 +| "select" <rvar> "in" <set> "where" <boole>
+                 +| <set> [ "union" | "intersect" | "diff" ] <set>
+                 +| "let" <svar> "be" <set> "in" <set>
+                 +| "let" <vvar> "be" <val> "in" <set>
+ +

<boole>::= [ "false" | "true" ]
+                    +| "(" <boole> ")"
+                    +| [ "not" | "ex" ] <boole>
+                    +| <boole> [ "and" | "or" ] <boole>
+                    +| <val> [ "sub" | "meet" | "eq" ] <val>
+ +

<val>::= "{" [ <string_list> ] ? "}"
+                 +| <string>
+                 +| "refof" <set>
+                 +| <rvar> "." <vvar>
+                 +| <vvar>
+                 +| "(" <val> ")"
+                 +| "property" <qualifier> <val> + + \ No newline at end of file diff --git a/helm/searchEngine/html/grammarpdq.html b/helm/searchEngine/html/grammarpdq.html new file mode 100644 index 000000000..bd3835bf9 --- /dev/null +++ b/helm/searchEngine/html/grammarpdq.html @@ -0,0 +1,38 @@ + + + + + + +

<Id>::= [ 'A-Z' | 'a-z' ][ 'A-Z' | 'a-z' | '0-9' | \- | _ | \' ]* + +

<Uri>::= <Conuri> | <Varuri> | <Indtyuri> | <Indconuri> + +

<Conuri>::= "cic:/" [<Id> "/" ]*<Id> ".con" + +

<Varuri>::= "cic:/" [<Id> "/" ]*<Id> ".var" + +

<Indtyuri>::= "cic:/" [<Id> "/" ]*<Id> ".ind#1/" ['0-9']+ + +

<Indconuri>::= "cic:/" [<Id> "/" ]*<Id> ".ind#1/" ['0-9']+ "/" ['0-9']+ + +

<Exp_Named_Subst>::= "{" [ [ [<Id> | <Varuri> ] ":=" <Expression> ";" ]* [ [<Id> | <Varuri> ] ":=" <Expression> ] ]? "}" + +

<Alias>::= "alias" <Id> <Uri> + +

<Genid>::= [ <Id> | <Varuri> | <Indtyuri> | <Indconuri> ] <Exp_Named_Subst> + +

<Expr>::= "\" <Genid> [ ":" | ":=" ] <Expr>"."<Expr> +
            +::= "!" <Genid> ":" <Expr>"."<Expr> +
            +::= <Expr>"->"<Expr> +
            +::= "(" <Expr> ")" "->"<Expr> +
            +::= "(" <Expr> [ " " <Expr>]* ")" +
            +::= "Prop" | "Set" | "Type" | "?" | <Uri> | <Id> + + \ No newline at end of file diff --git a/helm/searchEngine/html/index.html b/helm/searchEngine/html/index.html new file mode 100644 index 000000000..e7b73b5d2 --- /dev/null +++ b/helm/searchEngine/html/index.html @@ -0,0 +1,636 @@ + + + + + + diff --git a/helm/searchEngine/html/loc_obj.html b/helm/searchEngine/html/loc_obj.html new file mode 100644 index 000000000..b6b5222e3 --- /dev/null +++ b/helm/searchEngine/html/loc_obj.html @@ -0,0 +1,29 @@ + + + + + +

+ +Insert here the name of the object you want to search. +
+ +
+ + diff --git a/helm/searchEngine/html/manual/alias.jpg b/helm/searchEngine/html/manual/alias.jpg new file mode 100644 index 000000000..0f57638e2 Binary files /dev/null and b/helm/searchEngine/html/manual/alias.jpg differ diff --git a/helm/searchEngine/html/manual/ex1.jpg b/helm/searchEngine/html/manual/ex1.jpg new file mode 100644 index 000000000..8e75c08e2 Binary files /dev/null and b/helm/searchEngine/html/manual/ex1.jpg differ diff --git a/helm/searchEngine/html/manual/frames.jpg b/helm/searchEngine/html/manual/frames.jpg new file mode 100644 index 000000000..994b7ae5e Binary files /dev/null and b/helm/searchEngine/html/manual/frames.jpg differ diff --git a/helm/searchEngine/html/manual/index.html b/helm/searchEngine/html/manual/index.html new file mode 100644 index 000000000..8efa276fc --- /dev/null +++ b/helm/searchEngine/html/manual/index.html @@ -0,0 +1,40 @@ + + +Search Engine Interface Online Manual + + +

Search Engine Interface Online Manual

+

Index

+1. Roles of the frames
+2. How to compose a low-level query
+3. How to compose a pre-defined query
+

1. Roles of the frames

 +

+The interface is composed by five frames, as you can see below.

+

+Each frame has its own role, in particular:

+

+

2. How to compose a low-level query

 +

+In order to compose a low-level query, you must click the "compose a query" button in the main page. Here's what you'll get:

+Being "set" the main production of MathQL, at the beginning frame 1 is empty and frame 2 contains the menu for "set". You should choose one option by clicking on its radio button and then press "compose". The interface will perform a syntax check of what you entered and should something be wrong a message will appear, otherwise the query will be updated. Afterwards, the query will appear in frame 1 and in frame 3, and frame 2 will display the menu of the first production found in the new query string. For example, in the picture below you see the interface after the selection of the 10th production inserting "positions" as the requested identifier. As you can see, frame 2 now displays the "val" menu.

+

+Now your options include following the instructions in frame 2, choosing a different production by clicking on a link in frame 1, or manually modifying the query by writing the changes in the textarea in frame 3 and then clicking "apply changes". Obviously "undo" and "redo" buttons will allow you to recover from mistakes; just DON'T use "back","forward" and "refresh" buttons on your browser since they will cause unpredictable errors. Once the query is completed, the "submit the query" button will display the results in frame 2.

+

3. How to compose a pre-defined query

 +

+There are actually three pre-defined queries, Locate Object, Search Pattern and Match Conclusion. By clicking on "submit a pre-defined query" in the main page, a small menu with the three options will appear in frame 2.
+Locate Object is very simple, you must enter the name of the object to search in the text box and click "display results".
+Search Pattern, which takes a CIC term and finds theorems which have it as thesis, and Match Conclusion which takes a CIC term and finds theorems which have it as conclusion, have an identical interface, being the only difference in the output. +First thing to do is to insert a list of aliases (you may skip this step since the search engine will ask you later about ambiguous interpretations of your query if you don't know objects names, for example), then you must compose the CIC term. Composing a CIC term is pretty much the same thing as composing a MathQL query, except that the term is usually so short that there is no need for links, undo buttons and the like. While composing the term, you may modify your list of aliases (i.e. add or remove them) anytime by clicking "edit" in the frame 3. When the query is completed, the "submit" button will display the results in frame 2, and the server will ask you to solve ambiguities, thus adding aliases to your list. Once a result is displayed, you may want to submit a different query but keep your aliases; in this case, just click "new expression" in frame 3. The "edit" button will work even in this phase.

+

+

+ + + diff --git a/helm/searchEngine/html/mat_con.html b/helm/searchEngine/html/mat_con.html new file mode 100644 index 000000000..5fab87356 --- /dev/null +++ b/helm/searchEngine/html/mat_con.html @@ -0,0 +1,10 @@ + + + + + + + diff --git a/helm/searchEngine/html/paginacollink.html b/helm/searchEngine/html/paginacollink.html new file mode 100644 index 000000000..83f41bcf9 --- /dev/null +++ b/helm/searchEngine/html/paginacollink.html @@ -0,0 +1,13 @@ + + + + + +Query composer + + diff --git a/helm/searchEngine/html/pdq.html b/helm/searchEngine/html/pdq.html new file mode 100644 index 000000000..b4f5fe6c7 --- /dev/null +++ b/helm/searchEngine/html/pdq.html @@ -0,0 +1,75 @@ + + + + + + diff --git a/helm/searchEngine/html/query_choice.html b/helm/searchEngine/html/query_choice.html new file mode 100644 index 000000000..3e1932ad2 --- /dev/null +++ b/helm/searchEngine/html/query_choice.html @@ -0,0 +1,33 @@ + + + + + +
+ +
+ Locate Object
+ Match Conclusion
+ Search Pattern
+ Locate Inductive Principle +
+
+ + + diff --git a/helm/searchEngine/html/set.html b/helm/searchEngine/html/set.html new file mode 100644 index 000000000..a07088957 --- /dev/null +++ b/helm/searchEngine/html/set.html @@ -0,0 +1,178 @@ + + + + + +

+ +

+

Select one of the following:

+
+ ref [val]
+ pattern [val]
+ +
+ +
+ ( [set] )
+ relation + + + +[val] +
+ select @ +in [set] where [boole]
[set] + +[set]
+ let % be [set] in [set]
+ let $ be [val] in [set]
+
+ +