Initial revision

[helm.git] / helm / xmltheory / XmlTheory / README

diff --git a/helm/xmltheory/XmlTheory/README b/helm/xmltheory/XmlTheory/README
new file mode 100644 (file)
index 0000000..ce4c86c
--- /dev/null
+++ b/helm/xmltheory/XmlTheory/README
@@ -0,0 +1,78 @@
+Here we show the procedure to follow to add the recognition of
+a new syntactical form.
+
+Form to recognize in the model:
+
+Lemma existsDec : (l:(list A)){(list_exists l)}+{~(list_exists l)}.
+
+1. cd V7 ; grep "Lemma" */*.ml4
+   the result should be one or a few files. In this case the
+   only file is parsing/g_vernac.ml4. In the case of many files,
+   only one is the good one.
+2. open the file and search for Lemma:
+   thm_tok:
+    [ [ "Theorem" -> <:ast< "THEOREM" >>
+      | IDENT "Lemma" -> <:ast< "LEMMA" >>
+      | IDENT "Fact" -> <:ast< "FACT" >>
+      | IDENT "Remark" -> <:ast< "REMARK" >>
+      | IDENT "Decl" -> <:ast< "DECL" >> ] ]
+
+   so a Lemma is mapped into an ast of phylum thm_tok.
+   Let's search for thm_tok. Many occurrences are found,
+   but the only one that matches the form to recognize is
+
+  gallina:
+    (* Definition, Goal *)
+    [ [ thm = thm_tok; id = identarg; ":"; c = constrarg ->
+          <:ast< (StartProof $thm $id $c) >>
+
+  So the ast created is tagged StartProof
+3. grep "StartProof" */*.ml   (usually toplevel/...)
+   Open the file and search for StartProof.
+   This is found:
+    let _ =
+  add "StartProof"
+    (function
+       | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR com] ->
+           ...
+4. edit xmltheoryentries.ml and copy the entry for another rule,
+   substituting StartProof as the parameter for set_hook and
+   using the above match (with V. added where appropriate) after function:
+
+let module V = Vernacinterp in
+ set_hook "StartProof"
+  (function
+      [V.VARG_STRING kind;V.VARG_IDENTIFIER s;V.VARG_CONSTR com] ->
+       ???
+    | _ -> fail ()
+  )
+;;
+
+    Finally, write OCaml code to print to XML the availables interesting
+    infos. In our case the code becomes
+
+let module V = Vernacinterp in
+ set_hook "StartProof"
+  (function
+      [V.VARG_STRING kind;V.VARG_IDENTIFIER s;V.VARG_CONSTR com] ->
+       IXml.output
+        (Xml.xml_empty
+          "THEOREM"
+          ["uri", Names.string_of_id s ^ ".con"; "as",kind]
+        )
+    | _ -> fail ()
+  )
+;;
+
+     IXml.output should always be present and the code inside
+     (that is simply XML written in OCaml form) should be changed.
+     The syntax is
+        Xml.xml_empty "name" ["att1","value1" ; ... ; "attn","valuen"]
+     to create an empty element name with attributes att1 ... attn.
+     To create a non-empty element, use
+        Xml.xml_nempty "name" ["att1","value1" ; ... ; "attn","valuen"]
+         stream
+     where stream is an OCaml stream of other XML elements, as:
+       * another Xml.xml_nempty 
+       * an Xml.xml_empty
+       * [< stream1 ; ... ; streamk >]