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