helm/gTopLevel/cic2Xml.ml

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