helm/xmltheory/XmlTheory/xmltheoryentries.ml

   1 (*********************)
   2 (* Utility functions *)
   3 (*********************)
   4
   5 let fail () =
   6  Pp.warning "XmlTheory: AST not recognized"
   7 ;;
   8
   9 (* name is the name of the function to hook *)
  10 (* hook is an hook partial-function to recognize particular inputs *)
  11 let set_hook name hook =
  12  let module V = Vernacinterp in
  13   let old = V.vinterp_map name in
  14    V.vinterp_add name
  15     (fun l () ->
  16       old l () ;
  17       hook l
  18     )
  19 ;;
  20
  21
  22 (*****************************************************)
  23 (* Vernacular administrative commands for the module *)
  24 (*****************************************************)
  25
  26 let header =
  27 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ^
  28 "<!DOCTYPE Theory SYSTEM \"http://www.cs.unibo.it/helm/dtd/maththeory.dtd\">\n"
  29 ;;
  30
  31 (*Vecchio, ma funzionante
  32 let module V = Vernacinterp in
  33  V.vinterp_add "XMLTHEORYBEGIN"
  34   (function
  35       [V.VARG_STRING curi ; V.VARG_STRING filename] ->
  36        fun () ->
  37         IXml.reset_output filename ;
  38         IXml.output (Xml.xml_cdata header) ;
  39         IXml.open_non_empty_element "Theory" ["uri","cic:" ^ curi]
  40     | _ -> V.bad_vernac_args "XMLTHEORYBEGIN"
  41   )
  42 ;;
  43 *)
  44
  45 let module V = Vernacinterp in
  46 let module L = Library in
  47 let module S = System in
  48 let module N = Names in
  49  V.vinterp_add "XMLTHEORYBEGIN"
  50   (function
  51       [V.VARG_IDENTIFIER id ; V.VARG_STRING root_dir] ->
  52        fun () ->
  53         let s = N.string_of_id id in
  54          let lpe,_ =
  55           S.find_file_in_path (L.get_load_path ()) (s^".v")
  56          in
  57           let curi = "/" ^ String.concat "/" lpe.S.coq_dirpath in
  58           let dirname = root_dir ^ curi in
  59            Unix.system ("mkdir -p " ^ dirname) ;
  60           let filename = dirname ^ "/" ^ s ^ ".theory" in
  61            IXml.reset_output filename ;
  62            IXml.output (Xml.xml_cdata header) ;
  63            IXml.open_non_empty_element "Theory" ["uri","cic:" ^ curi ^ "/" ^ s]
  64     | _ -> V.bad_vernac_args "XMLTHEORYBEGIN"
  65   )
  66 ;;
  67
  68 let module V = Vernacinterp in
  69  V.vinterp_add "XMLTHEORYEND"
  70   (function
  71       [] ->
  72        fun () ->
  73         IXml.close_non_empty_element () ;
  74         IXml.print_output ()
  75     | _ -> V.bad_vernac_args "XMLTHEORYEND"
  76   )
  77 ;;
  78
  79
  80 (**********************************************************)
  81 (* All the vernacular commands on which one is interested *)
  82 (* should be overridden here                              *)
  83 (**********************************************************)
  84
  85 let module V = Vernacinterp in
  86 let module N = Names in
  87 let module S = System in
  88 let module L = Library in
  89  set_hook "Require"
  90   (function
  91       [V.VARG_STRING import; V.VARG_STRING specif; V.VARG_IDENTIFIER id] ->
  92        (* id is the identifier of the module, but we need the absolute *)
  93        (* identifier as an URI.                                        *)
  94        (* E.g.: Logic ==> theory:/Coq/Init/Logic.theory                *)
  95         let name = N.string_of_id id in
  96          let ({S.coq_dirpath = coq_dirpath},_) = L.module_filename name in
  97           let uri =
  98            "theory:/" ^ (String.concat "/" coq_dirpath) ^ "/" ^ name ^ ".theory"
  99           in
 100            IXml.output
 101             (Xml.xml_nempty "vernacular" []
 102              (Xml.xml_empty
 103                "Require"
 104                ["import",import; "specif",specif; "uri",uri]
 105              )
 106             )
 107     | _ -> fail ()
 108    )
 109 ;;
 110
 111 let module V = Vernacinterp in
 112 let module T = Nametab in
 113 let module N = Names in
 114  set_hook "HintsResolve"
 115   (function
 116       (V.VARG_VARGLIST l)::lh ->
 117         IXml.output
 118          (Xml.xml_nempty "vernacular" []
 119           (Xml.xml_nempty
 120             "HintsResolve" []
 121             [< Xml.xml_nempty "dbs" []
 122                 (List.fold_right
 123                   (function
 124                       (V.VARG_IDENTIFIER x) ->
 125                         (function i ->
 126                           [< Xml.xml_empty "db" ["name",N.string_of_id x];
 127                              i
 128                           >]
 129                         )
 130                     | _ -> Vernacinterp.bad_vernac_args "HintsResolve"
 131                   )
 132                 l [<>]) ;
 133                Xml.xml_nempty "hints" []
 134                 (List.fold_right
 135                   (function
 136                       (V.VARG_QUALID x) ->
 137                         (function i ->
 138                           [< Xml.xml_empty "hint" ["name",T.string_of_qualid x];
 139                              i
 140                           >]
 141                         )
 142                     | _ -> Vernacinterp.bad_vernac_args "HintsResolve"
 143                   )
 144                 lh [<>]
 145                 )
 146             >]
 147           )
 148          )
 149     | _ -> fail ()
 150   )
 151 ;;
 152
 153 let module V = Vernacinterp in
 154  set_hook "IMPLICIT_ARGS_ON"
 155   (function
 156       [] ->
 157         IXml.output
 158          (Xml.xml_nempty "vernacular" []
 159           (Xml.xml_empty
 160             "ImplicitArguments"
 161             ["status","ON"]
 162           )
 163          )
 164     | _ -> fail ()
 165   )
 166 ;;
 167
 168 let module V = Vernacinterp in
 169  set_hook "DEFINITION"
 170   (function
 171       (* Coq anomaly: a Local definition is a Definition at the syntax *)
 172       (* level but a Variable at the logical level. Here we have to    *)
 173       (* recognize the two cases and treat them differently            *)
 174       (V.VARG_STRING "LOCAL":: V.VARG_IDENTIFIER id:: V.VARG_CONSTR c:: rest) ->
 175         IXml.output
 176          (Xml.xml_nempty "VARIABLES" ["as","LOCAL"]
 177            (Xml.xml_empty
 178              "VARIABLE"
 179              ["uri",Names.string_of_id id ^ ".var"]
 180            )
 181          )
 182     | (V.VARG_STRING kind:: V.VARG_IDENTIFIER id:: V.VARG_CONSTR c :: rest) ->
 183         IXml.output
 184          (Xml.xml_empty
 185            "DEFINITION"
 186            ["uri", Names.string_of_id id ^ ".con" ; "as",kind]
 187          )
 188     | _ -> fail ()
 189   )
 190 ;;
 191
 192 let module V = Vernacinterp in
 193  set_hook "BeginSection"
 194   (function
 195       [V.VARG_IDENTIFIER id] ->
 196         IXml.open_non_empty_element "SECTION" ["uri", Names.string_of_id id]
 197     | _ -> fail ()
 198   )
 199 ;;
 200
 201 let module V = Vernacinterp in
 202  set_hook "EndSection"
 203   (function
 204       [V.VARG_IDENTIFIER id] ->
 205         IXml.close_non_empty_element ()
 206     | _ -> fail ()
 207   )
 208 ;;
 209
 210 let module V = Vernacinterp in
 211  set_hook "StartProof"
 212   (function
 213       [V.VARG_STRING kind;V.VARG_IDENTIFIER s;V.VARG_CONSTR com] ->
 214        IXml.output
 215         (Xml.xml_empty
 216           "THEOREM"
 217           ["uri", Names.string_of_id s ^ ".con"; "as",kind]
 218         )
 219     | _ -> fail ()
 220   )
 221 ;;
 222
 223 let module V = Vernacinterp in
 224  set_hook "MUTUALINDUCTIVE"
 225   (function
 226       [V.VARG_STRING f; V.VARG_VARGLIST indl] ->
 227         (* we need the name of the first inductive defined *)
 228         (* type in the block to get the URI                *)
 229         let name =
 230          match indl with
 231             (V.VARG_VARGLIST ((V.VARG_IDENTIFIER name)::_))::_ -> name
 232           | _ -> assert false
 233         in
 234          IXml.output
 235           (Xml.xml_empty
 236             "DEFINITION"
 237             ["uri", Names.string_of_id name ^ ".ind"; "as",f]
 238           )
 239     | _ -> fail ()
 240   )
 241 ;;
 242
 243 let module V = Vernacinterp in
 244  set_hook "VARIABLE"
 245   (function
 246       [V.VARG_STRING kind; V.VARG_BINDERLIST slcl] ->
 247        (* here we need all the names *)
 248        let names =
 249         List.flatten (List.map fst slcl)
 250        in
 251         IXml.output
 252          (Xml.xml_nempty "VARIABLES" ["as",kind]
 253           (List.fold_right
 254             (fun name s ->
 255               [< (Xml.xml_empty
 256                    "VARIABLE"
 257                    ["uri",Names.string_of_id name ^ ".var"]
 258                  ) ; s
 259               >]
 260             ) names [<>]
 261           )
 262          )
 263     | _ -> fail ()
 264   )
 265 ;;
 266
 267 let module V = Vernacinterp in
 268 let module T = Nametab in
 269 let module N = Names in
 270  set_hook "COERCION"
 271   (function
 272       [V.VARG_STRING kind; V.VARG_STRING identity; V.VARG_QUALID qid;
 273        V.VARG_QUALID qids; V.VARG_QUALID qidt] ->
 274         (* let's substitute empty strings with non-empty strings *)
 275         (* to get a stricter DTD                                 *)
 276         let remove_empty_string s = if s = "" then "UNSPECIFIED" else s in
 277         let kind     = remove_empty_string kind     in
 278         let identity = remove_empty_string identity in
 279          IXml.output
 280           (Xml.xml_nempty "vernacular" []
 281            (Xml.xml_empty
 282              "Coercion"
 283              ["kind",kind; "identity",identity ; "name",T.string_of_qualid qid ;
 284               "source",T.string_of_qualid qids;"target",T.string_of_qualid qidt]
 285            )
 286           )
 287     | _ -> fail ()
 288   )
 289 ;;
 290
 291 let module V = Vernacinterp in
 292  set_hook "MUTUALRECURSIVE"
 293   (function
 294       [V.VARG_VARGLIST lmi] ->
 295         (* we need the name of the first inductive defined *)
 296         (* type in the block to get the URI                *)
 297         let name =
 298          match lmi with
 299             (V.VARG_VARGLIST ((V.VARG_IDENTIFIER name)::_))::_ -> name
 300           | _ -> assert false
 301         in
 302          IXml.output
 303           (Xml.xml_empty
 304             "DEFINITION"
 305             ["uri", Names.string_of_id name ^ ".con" ; "as","Fixpoint"]
 306           )
 307      | _ -> fail ()
 308   )
 309 ;;
 310
 311 let module V = Vernacinterp in
 312  set_hook "MUTUALCORECURSIVE"
 313   (function
 314       [V.VARG_VARGLIST lmi] ->
 315         (* we need the name of the first inductive defined *)
 316         (* type in the block to get the URI                *)
 317         let name =
 318          match lmi with
 319             (V.VARG_VARGLIST ((V.VARG_IDENTIFIER name)::_))::_ -> name
 320           | _ -> assert false
 321         in
 322          IXml.output
 323           (Xml.xml_empty
 324             "DEFINITION"
 325             ["uri", Names.string_of_id name ^ ".con" ; "as","CoFixpoint"]
 326           )
 327      | _ -> fail ()
 328   )
 329 ;;
 330
 331 let module V = Vernacinterp in
 332  set_hook "RECORD"
 333   (function
 334       [V.VARG_STRING coe;
 335        V.VARG_IDENTIFIER struc;
 336        V.VARG_BINDERLIST binders;
 337        V.VARG_CONSTR sort;
 338        V.VARG_VARGLIST namec;
 339        V.VARG_VARGLIST cfs] ->
 340          IXml.output
 341           (Xml.xml_empty
 342             "DEFINITION"
 343             ["uri", Names.string_of_id struc ^ ".ind" ; "as","Record"]
 344           )
 345      | _ -> fail ()
 346   )
 347 ;;
 348
 349 let module V = Vernacinterp in
 350  set_hook "PARAMETER"
 351   (function
 352       [V.VARG_STRING kind; V.VARG_BINDERLIST slcl] ->
 353        (* here we need all the names *)
 354        let names =
 355         List.flatten (List.map fst slcl)
 356        in
 357         IXml.output
 358          (Xml.xml_nempty "AXIOMS" ["as",kind]
 359           (List.fold_right
 360             (fun name s ->
 361               [< (Xml.xml_empty
 362                    "AXIOM"
 363                    ["uri",Names.string_of_id name ^ ".con"]
 364                  ) ; s
 365               >]
 366             ) names [<>]
 367           )
 368          )
 369     | _ -> fail ()
 370   )
 371 ;;