helm/xmltheory/XmlTheory/README

   1 Here we show the procedure to follow to add the recognition of
   2 a new syntactical form.
   3
   4 Form to recognize in the model:
   5
   6 Lemma existsDec : (l:(list A)){(list_exists l)}+{~(list_exists l)}.
   7
   8 1. cd V7 ; grep "Lemma" */*.ml4
   9    the result should be one or a few files. In this case the
  10    only file is parsing/g_vernac.ml4. In the case of many files,
  11    only one is the good one.
  12 2. open the file and search for Lemma:
  13    thm_tok:
  14     [ [ "Theorem" -> <:ast< "THEOREM" >>
  15       | IDENT "Lemma" -> <:ast< "LEMMA" >>
  16       | IDENT "Fact" -> <:ast< "FACT" >>
  17       | IDENT "Remark" -> <:ast< "REMARK" >>
  18       | IDENT "Decl" -> <:ast< "DECL" >> ] ]
  19
  20    so a Lemma is mapped into an ast of phylum thm_tok.
  21    Let's search for thm_tok. Many occurrences are found,
  22    but the only one that matches the form to recognize is
  23
  24   gallina:
  25     (* Definition, Goal *)
  26     [ [ thm = thm_tok; id = identarg; ":"; c = constrarg ->
  27           <:ast< (StartProof $thm $id $c) >>
  28
  29   So the ast created is tagged StartProof
  30 3. grep "StartProof" */*.ml   (usually toplevel/...)
  31    Open the file and search for StartProof.
  32    This is found:
  33     let _ =
  34   add "StartProof"
  35     (function
  36        | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR com] ->
  37            ...
  38 4. edit xmltheoryentries.ml and copy the entry for another rule,
  39    substituting StartProof as the parameter for set_hook and
  40    using the above match (with V. added where appropriate) after function:
  41
  42 let module V = Vernacinterp in
  43  set_hook "StartProof"
  44   (function
  45       [V.VARG_STRING kind;V.VARG_IDENTIFIER s;V.VARG_CONSTR com] ->
  46        ???
  47     | _ -> fail ()
  48   )
  49 ;;
  50
  51     Finally, write OCaml code to print to XML the availables interesting
  52     infos. In our case the code becomes
  53
  54 let module V = Vernacinterp in
  55  set_hook "StartProof"
  56   (function
  57       [V.VARG_STRING kind;V.VARG_IDENTIFIER s;V.VARG_CONSTR com] ->
  58        IXml.output
  59         (Xml.xml_empty
  60           "THEOREM"
  61           ["uri", Names.string_of_id s ^ ".con"; "as",kind]
  62         )
  63     | _ -> fail ()
  64   )
  65 ;;
  66
  67      IXml.output should always be present and the code inside
  68      (that is simply XML written in OCaml form) should be changed.
  69      The syntax is
  70         Xml.xml_empty "name" ["att1","value1" ; ... ; "attn","valuen"]
  71      to create an empty element name with attributes att1 ... attn.
  72      To create a non-empty element, use
  73         Xml.xml_nempty "name" ["att1","value1" ; ... ; "attn","valuen"]
  74          stream
  75      where stream is an OCaml stream of other XML elements, as:
  76        * another Xml.xml_nempty
  77        * an Xml.xml_empty
  78        * [< stream1 ; ... ; streamk >]