helm/ocaml/cic_acic/cic2Xml.ml

   1 (* Copyright (C) 2000-2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (*CSC codice cut & paste da cicPp e xmlcommand *)
  27
  28 exception NotImplemented;;
  29
  30 let dtdname ~ask_dtd_to_the_getter dtd =
  31  if ask_dtd_to_the_getter then
  32   Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd
  33  else
  34   "http://mowgli.cs.unibo.it/dtd/" ^ dtd
  35 ;;
  36
  37 let param_attribute_of_params params =
  38  String.concat " " (List.map UriManager.string_of_uri params)
  39 ;;
  40
  41 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
  42 let print_term ?ids_to_inner_sorts =
  43  let find_sort name id =
  44   match ids_to_inner_sorts with
  45      None -> []
  46    | Some ids_to_inner_sorts ->
  47       [None,name,Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)]
  48  in
  49  let rec aux =
  50   let module C = Cic in
  51   let module X = Xml in
  52   let module U = UriManager in
  53     function
  54        C.ARel (id,idref,n,b) ->
  55         let sort = find_sort "sort" id in
  56          X.xml_empty "REL"
  57           (sort @
  58            [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ;
  59            None,"idref",idref])
  60      | C.AVar (id,uri,exp_named_subst) ->
  61         let sort = find_sort "sort" id in
  62          aux_subst uri
  63           (X.xml_empty "VAR"
  64             (sort @ [None,"uri",U.string_of_uri uri;None,"id",id]))
  65           exp_named_subst
  66      | C.AMeta (id,n,l) ->
  67         let sort = find_sort "sort" id in
  68          X.xml_nempty "META"
  69           (sort @ [None,"no",(string_of_int n) ; None,"id",id])
  70           (List.fold_left
  71             (fun i t ->
  72               match t with
  73                  Some t' ->
  74                   [< i ; X.xml_nempty "substitution" [] (aux t') >]
  75                | None ->
  76                   [< i ; X.xml_empty "substitution" [] >]
  77             ) [< >] l)
  78      | C.ASort (id,s) ->
  79         let string_of_sort s =
  80           Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)
  81         in
  82          X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id]
  83      | C.AImplicit _ -> raise NotImplemented
  84      | C.AProd (last_id,_,_,_) as prods ->
  85         let rec eat_prods =
  86          function
  87             C.AProd (id,n,s,t) ->
  88              let prods,t' = eat_prods t in
  89               (id,n,s)::prods,t'
  90           | t -> [],t
  91         in
  92          let prods,t = eat_prods prods in
  93           let sort = find_sort "type" last_id in
  94            X.xml_nempty "PROD" sort
  95             [< List.fold_left
  96                 (fun i (id,binder,s) ->
  97                   let sort = find_sort "type" (Cic2acic.source_id_of_id id) in
  98                    let attrs =
  99                     sort @ ((None,"id",id)::
 100                      match binder with
 101                         C.Anonymous -> []
 102                       | C.Name b -> [None,"binder",b])
 103                    in
 104                     [< i ; X.xml_nempty "decl" attrs (aux s) >]
 105                 ) [< >] prods ;
 106                X.xml_nempty "target" [] (aux t)
 107             >]
 108      | C.ACast (id,v,t) ->
 109         let sort = find_sort "sort" id in
 110          X.xml_nempty "CAST" (sort @ [None,"id",id])
 111           [< X.xml_nempty "term" [] (aux v) ;
 112              X.xml_nempty "type" [] (aux t)
 113           >]
 114      | C.ALambda (last_id,_,_,_) as lambdas ->
 115         let rec eat_lambdas =
 116          function
 117             C.ALambda (id,n,s,t) ->
 118              let lambdas,t' = eat_lambdas t in
 119               (id,n,s)::lambdas,t'
 120           | t -> [],t
 121         in
 122          let lambdas,t = eat_lambdas lambdas in
 123           let sort = find_sort "sort" last_id in
 124            X.xml_nempty "LAMBDA" sort
 125             [< List.fold_left
 126                 (fun i (id,binder,s) ->
 127                   let sort = find_sort "type" (Cic2acic.source_id_of_id id) in
 128                    let attrs =
 129                     sort @ ((None,"id",id)::
 130                      match binder with
 131                         C.Anonymous -> []
 132                       | C.Name b -> [None,"binder",b])
 133                    in
 134                     [< i ; X.xml_nempty "decl" attrs (aux s) >]
 135                 ) [< >] lambdas ;
 136                X.xml_nempty "target" [] (aux t)
 137             >]
 138      | C.ALetIn (xid,C.Anonymous,s,t) ->
 139        assert false
 140      | C.ALetIn (last_id,C.Name _,_,_) as letins ->
 141         let rec eat_letins =
 142          function
 143             C.ALetIn (id,n,s,t) ->
 144              let letins,t' = eat_letins t in
 145               (id,n,s)::letins,t'
 146           | t -> [],t
 147         in
 148          let letins,t = eat_letins letins in
 149           let sort = find_sort "sort" last_id in
 150            X.xml_nempty "LETIN" sort
 151             [< List.fold_left
 152                 (fun i (id,binder,s) ->
 153                   let sort = find_sort "sort" id in
 154                    let attrs =
 155                     sort @ ((None,"id",id)::
 156                      match binder with
 157                         C.Anonymous -> []
 158                       | C.Name b -> [None,"binder",b])
 159                    in
 160                     [< i ; X.xml_nempty "def" attrs (aux s) >]
 161                 ) [< >] letins ;
 162                X.xml_nempty "target" [] (aux t)
 163             >]
 164      | C.AAppl (id,li) ->
 165         let sort = find_sort "sort" id in
 166          X.xml_nempty "APPLY" (sort @ [None,"id",id])
 167           [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
 168           >]
 169      | C.AConst (id,uri,exp_named_subst) ->
 170         let sort = find_sort "sort" id in
 171          aux_subst uri
 172           (X.xml_empty "CONST"
 173             (sort @ [None,"uri",(U.string_of_uri uri) ; None,"id",id])
 174           ) exp_named_subst
 175      | C.AMutInd (id,uri,i,exp_named_subst) ->
 176         aux_subst uri
 177          (X.xml_empty "MUTIND"
 178            [None, "uri", (U.string_of_uri uri) ;
 179             None, "noType", (string_of_int i) ;
 180             None, "id", id]
 181          ) exp_named_subst
 182      | C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
 183         let sort = find_sort "sort" id in
 184          aux_subst uri
 185           (X.xml_empty "MUTCONSTRUCT"
 186             (sort @
 187              [None,"uri", (U.string_of_uri uri) ;
 188               None,"noType",(string_of_int i) ;
 189               None,"noConstr",(string_of_int j) ;
 190               None,"id",id])
 191           ) exp_named_subst
 192      | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
 193         let sort = find_sort "sort" id in
 194          X.xml_nempty "MUTCASE"
 195           (sort @
 196            [None,"uriType",(U.string_of_uri uri) ;
 197             None,"noType", (string_of_int typeno) ;
 198             None,"id", id])
 199           [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
 200              X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
 201              List.fold_right
 202               (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
 203               patterns [<>]
 204           >]
 205      | C.AFix (id, no, funs) ->
 206         let sort = find_sort "sort" id in
 207          X.xml_nempty "FIX"
 208           (sort @ [None,"noFun", (string_of_int no) ; None,"id",id])
 209           [< List.fold_right
 210               (fun (id,fi,ai,ti,bi) i ->
 211                 [< X.xml_nempty "FixFunction"
 212                     [None,"id",id ; None,"name", fi ;
 213                      None,"recIndex", (string_of_int ai)]
 214                     [< X.xml_nempty "type" [] [< aux ti >] ;
 215                        X.xml_nempty "body" [] [< aux bi >]
 216                     >] ;
 217                    i
 218                 >]
 219               ) funs [<>]
 220           >]
 221      | C.ACoFix (id,no,funs) ->
 222         let sort = find_sort "sort" id in
 223          X.xml_nempty "COFIX"
 224           (sort @ [None,"noFun", (string_of_int no) ; None,"id",id])
 225           [< List.fold_right
 226               (fun (id,fi,ti,bi) i ->
 227                 [< X.xml_nempty "CofixFunction" [None,"id",id ; None,"name", fi]
 228                     [< X.xml_nempty "type" [] [< aux ti >] ;
 229                        X.xml_nempty "body" [] [< aux bi >]
 230                     >] ;
 231                    i
 232                 >]
 233               ) funs [<>]
 234           >]
 235  and aux_subst buri target subst =
 236 (*CSC: I have now no way to assign an ID to the explicit named substitution *)
 237   let id = None in
 238    if subst = [] then
 239     target
 240    else
 241     Xml.xml_nempty "instantiate"
 242      (match id with None -> [] | Some id -> [None,"id",id])
 243      [< target ;
 244         List.fold_left
 245          (fun i (uri,arg) ->
 246            let relUri =
 247             let buri_frags =
 248              Str.split (Str.regexp "/") (UriManager.string_of_uri buri) in
 249             let uri_frags =
 250              Str.split (Str.regexp "/") (UriManager.string_of_uri uri)  in
 251              let rec find_relUri buri_frags uri_frags =
 252               match buri_frags,uri_frags with
 253                  [_], _ -> String.concat "/" uri_frags
 254                | he1::tl1, he2::tl2 ->
 255                   assert (he1 = he2) ;
 256                   find_relUri tl1 tl2
 257                | _,_ -> assert false (* uri is not relative to buri *)
 258              in
 259               find_relUri buri_frags uri_frags
 260            in
 261             [< i ; Xml.xml_nempty "arg" [None,"relUri", relUri] (aux arg) >]
 262          ) [<>] subst
 263      >]
 264   in
 265    aux
 266 ;;
 267
 268 let xml_of_attrs attributes =
 269   let class_of = function
 270     | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"]
 271     | `Elim s ->
 272         Xml.xml_nempty "class" [None,"value","elim"]
 273          [< Xml.xml_empty
 274              "SORT" [None,"value",
 275                       (Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)) ;
 276                      None,"id","elimination_sort"] >]
 277     | `Record field_names ->
 278         Xml.xml_nempty "class" [None,"value","record"]
 279          (List.fold_right
 280            (fun (name,coercion) res ->
 281              [< Xml.xml_empty "field"
 282                 [None,"name",if coercion then name ^ " coercion" else name];
 283               res >]
 284            ) field_names [<>])
 285     | `Projection -> Xml.xml_empty "class" [None,"value","projection"]
 286   in
 287   let flavour_of = function
 288     | `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"]
 289     | `Fact -> Xml.xml_empty "flavour" [None, "value", "fact"]
 290     | `Lemma -> Xml.xml_empty "flavour" [None, "value", "lemma"]
 291     | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"]
 292     | `Theorem -> Xml.xml_empty "flavour" [None, "value", "theorem"]
 293     | `Variant -> Xml.xml_empty "flavour" [None, "value", "variant"]
 294   in
 295   let xml_attr_of = function
 296     | `Generated -> Xml.xml_empty "generated" []
 297     | `Class c -> class_of c
 298     | `Flavour f -> flavour_of f
 299   in
 300   let xml_attrs =
 301    List.fold_right
 302     (fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>]
 303   in
 304    Xml.xml_nempty "attributes" [] xml_attrs
 305
 306 let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
 307  let module C = Cic in
 308  let module X = Xml in
 309  let module U = UriManager in
 310   let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in
 311    match obj with
 312        C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) ->
 313         let params' = param_attribute_of_params params in
 314         let xml_attrs = xml_of_attrs obj_attrs in
 315         let xml_for_current_proof_body =
 316 (*CSC: Should the CurrentProof also have the list of variables it depends on? *)
 317 (*CSC: I think so. Not implemented yet.                                       *)
 318          X.xml_nempty "CurrentProof"
 319           [None,"of",UriManager.string_of_uri uri ; None,"id", id]
 320           [< xml_attrs;
 321             List.fold_left
 322               (fun i (cid,n,canonical_context,t) ->
 323                 [< i ;
 324                    X.xml_nempty "Conjecture"
 325                     [None,"id",cid ; None,"no",(string_of_int n)]
 326                     [< List.fold_left
 327                         (fun i (hid,t) ->
 328                           [< (match t with
 329                                  Some (n,C.ADecl t) ->
 330                                   X.xml_nempty "Decl"
 331                                    (match n with
 332                                        C.Name n' ->
 333                                         [None,"id",hid;None,"name",n']
 334                                      | C.Anonymous -> [None,"id",hid])
 335                                    (print_term ?ids_to_inner_sorts t)
 336                                | Some (n,C.ADef t) ->
 337                                   X.xml_nempty "Def"
 338                                    (match n with
 339                                        C.Name n' ->
 340                                         [None,"id",hid;None,"name",n']
 341                                      | C.Anonymous -> [None,"id",hid])
 342                                    (print_term ?ids_to_inner_sorts t)
 343                               | None -> X.xml_empty "Hidden" [None,"id",hid]
 344                              ) ;
 345                              i
 346                           >]
 347                         ) [< >] canonical_context ;
 348                        X.xml_nempty "Goal" []
 349                         (print_term ?ids_to_inner_sorts t)
 350                     >]
 351                 >])
 352               [< >] conjectures ;
 353              X.xml_nempty "body" [] (print_term ?ids_to_inner_sorts bo) >]
 354         in
 355         let xml_for_current_proof_type =
 356          X.xml_nempty "ConstantType"
 357           [None,"name",n ; None,"params",params' ; None,"id", id]
 358           (print_term ?ids_to_inner_sorts ty)
 359         in
 360         let xmlbo =
 361          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 362             X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^ dtdname ^ "\">\n");
 363             xml_for_current_proof_body
 364          >] in
 365         let xmlty =
 366          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 367             X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
 368             xml_for_current_proof_type
 369          >]
 370         in
 371          xmlty, Some xmlbo
 372      | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) ->
 373         let params' = param_attribute_of_params params in
 374         let xml_attrs = xml_of_attrs obj_attrs in
 375         let xmlbo =
 376          match bo with
 377             None -> None
 378           | Some bo ->
 379              Some
 380               [< X.xml_cdata
 381                   "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 382                  X.xml_cdata
 383                   ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
 384                  X.xml_nempty "ConstantBody"
 385                   [None,"for",UriManager.string_of_uri uri ;
 386                    None,"params",params' ; None,"id", id]
 387                   [< print_term ?ids_to_inner_sorts bo >]
 388               >]
 389         in
 390         let xmlty =
 391          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 392             X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
 393              X.xml_nempty "ConstantType"
 394               [None,"name",n ; None,"params",params' ; None,"id", id]
 395               [< xml_attrs; print_term ?ids_to_inner_sorts ty >]
 396          >]
 397         in
 398          xmlty, xmlbo
 399      | C.AVariable (id,n,bo,ty,params,obj_attrs) ->
 400         let params' = param_attribute_of_params params in
 401         let xml_attrs = xml_of_attrs obj_attrs in
 402         let xmlbo =
 403          match bo with
 404             None -> [< >]
 405           | Some bo ->
 406              X.xml_nempty "body" [] [< print_term ?ids_to_inner_sorts bo >]
 407         in
 408         let aobj =
 409          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 410             X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
 411              X.xml_nempty "Variable"
 412               [None,"name",n ; None,"params",params' ; None,"id", id]
 413               [< xml_attrs; xmlbo;
 414                  X.xml_nempty "type" [] (print_term ?ids_to_inner_sorts ty)
 415               >]
 416          >]
 417         in
 418          aobj, None
 419      | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) ->
 420         let params' = param_attribute_of_params params in
 421         let xml_attrs = xml_of_attrs obj_attrs in
 422          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 423             X.xml_cdata
 424              ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
 425             X.xml_nempty "InductiveDefinition"
 426              [None,"noParams",string_of_int nparams ;
 427               None,"id",id ;
 428               None,"params",params']
 429              [< xml_attrs;
 430                 (List.fold_left
 431                   (fun i (id,typename,finite,arity,cons) ->
 432                     [< i ;
 433                        X.xml_nempty "InductiveType"
 434                         [None,"id",id ; None,"name",typename ;
 435                          None,"inductive",(string_of_bool finite)
 436                         ]
 437                         [< X.xml_nempty "arity" []
 438                             (print_term ?ids_to_inner_sorts arity) ;
 439                            (List.fold_left
 440                             (fun i (name,lc) ->
 441                               [< i ;
 442                                  X.xml_nempty "Constructor"
 443                                   [None,"name",name]
 444                                   (print_term ?ids_to_inner_sorts lc)
 445                               >]) [<>] cons
 446                            )
 447                         >]
 448                     >]
 449                   ) [< >] tys
 450                 )
 451              >]
 452          >], None
 453 ;;
 454
 455 let
 456  print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types
 457   ~ask_dtd_to_the_getter
 458 =
 459  let module C2A = Cic2acic in
 460  let module X = Xml in
 461   let dtdname = dtdname ~ask_dtd_to_the_getter "cictypes.dtd" in
 462    [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 463       X.xml_cdata
 464        ("<!DOCTYPE InnerTypes SYSTEM \"" ^ dtdname ^ "\">\n") ;
 465       X.xml_nempty "InnerTypes" [None,"of",UriManager.string_of_uri curi]
 466        (Hashtbl.fold
 467          (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
 468            [< x ;
 469               X.xml_nempty "TYPE" [None,"of",id]
 470                [< X.xml_nempty "synthesized" []
 471                  [< print_term ~ids_to_inner_sorts synty >] ;
 472                  match expty with
 473                    None -> [<>]
 474                  | Some expty' -> X.xml_nempty "expected" []
 475                     [< print_term ~ids_to_inner_sorts expty' >]
 476                >]
 477            >]
 478          ) ids_to_inner_types [<>]
 479        )
 480    >]
 481 ;;