]> matita.cs.unibo.it Git - helm.git/blob - helm/xmltheory/XmlTheory/README
Main code clean-up.
[helm.git] / 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 >]