+++ /dev/null
-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 >]