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