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