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