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 ImpossiblePossible;;
  29 exception NotImplemented;;
  30
  31 let dtdname ~ask_dtd_to_the_getter dtd =
  32  if ask_dtd_to_the_getter then
  33   Helm_registry.get "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 find_sort id =
  45    Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)
  46  in
  47  let rec aux =
  48   let module C = Cic in
  49   let module X = Xml in
  50   let module U = UriManager in
  51     function
  52        C.ARel (id,idref,n,b) ->
  53         let sort = find_sort id in
  54          X.xml_empty "REL"
  55           [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ;
  56            None,"idref",idref ; None,"sort",sort]
  57      | C.AVar (id,uri,exp_named_subst) ->
  58         let sort = find_sort id in
  59          aux_subst uri
  60           (X.xml_empty "VAR"
  61             [None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort])
  62           exp_named_subst
  63      | C.AMeta (id,n,l) ->
  64         let sort = find_sort id in
  65          X.xml_nempty "META"
  66           [None,"no",(string_of_int n) ; None,"id",id ; None,"sort",sort]
  67           (List.fold_left
  68             (fun i t ->
  69               match t with
  70                  Some t' ->
  71                   [< i ; X.xml_nempty "substitution" [] (aux t') >]
  72                | None ->
  73                   [< i ; X.xml_empty "substitution" [] >]
  74             ) [< >] l)
  75      | C.ASort (id,s) ->
  76         let string_of_sort s =
  77           Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)
  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 = find_sort last_id in
  91            X.xml_nempty "PROD" [None,"type",sort]
  92             [< List.fold_left
  93                 (fun i (id,binder,s) ->
  94                   let sort = find_sort (Cic2acic.source_id_of_id id) in
  95                    let attrs =
  96                     (None,"id",id)::(None,"type",sort)::
  97                     match binder with
  98                        C.Anonymous -> []
  99                      | C.Name b -> [None,"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 = find_sort id in
 107          X.xml_nempty "CAST" [None,"id",id ; None,"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 = find_sort last_id in
 121            X.xml_nempty "LAMBDA" [None,"sort",sort]
 122             [< List.fold_left
 123                 (fun i (id,binder,s) ->
 124                   let sort = find_sort (Cic2acic.source_id_of_id id) in
 125                    let attrs =
 126                     (None,"id",id)::(None,"type",sort)::
 127                     match binder with
 128                        C.Anonymous -> []
 129                      | C.Name b -> [None,"binder",b]
 130                    in
 131                     [< i ; X.xml_nempty "decl" attrs (aux s) >]
 132                 ) [< >] lambdas ;
 133                X.xml_nempty "target" [] (aux t)
 134             >]
 135      | C.ALetIn (xid,C.Anonymous,s,t) ->
 136        assert false
 137      | C.ALetIn (last_id,C.Name _,_,_) as letins ->
 138         let rec eat_letins =
 139          function
 140             C.ALetIn (id,n,s,t) ->
 141              let letins,t' = eat_letins t in
 142               (id,n,s)::letins,t'
 143           | t -> [],t
 144         in
 145          let letins,t = eat_letins letins in
 146           let sort = find_sort last_id in
 147            X.xml_nempty "LETIN" [None,"sort",sort]
 148             [< List.fold_left
 149                 (fun i (id,binder,s) ->
 150                   let sort = find_sort id in
 151                    let attrs =
 152                     (None,"id",id)::(None,"sort",sort)::
 153                     match binder with
 154                        C.Anonymous -> []
 155                      | C.Name b -> [None,"binder",b]
 156                    in
 157                     [< i ; X.xml_nempty "def" attrs (aux s) >]
 158                 ) [< >] letins ;
 159                X.xml_nempty "target" [] (aux t)
 160             >]
 161      | C.AAppl (id,li) ->
 162         let sort = find_sort id in
 163          X.xml_nempty "APPLY" [None,"id",id ; None,"sort",sort]
 164           [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
 165           >]
 166      | C.AConst (id,uri,exp_named_subst) ->
 167         let sort = find_sort id in
 168          aux_subst uri
 169           (X.xml_empty "CONST"
 170             [None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort]
 171           ) exp_named_subst
 172      | C.AMutInd (id,uri,i,exp_named_subst) ->
 173         aux_subst uri
 174          (X.xml_empty "MUTIND"
 175            [None, "uri", (U.string_of_uri uri) ;
 176             None, "noType", (string_of_int i) ;
 177             None, "id", id]
 178          ) exp_named_subst
 179      | C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
 180         let sort = find_sort id in
 181          aux_subst uri
 182           (X.xml_empty "MUTCONSTRUCT"
 183             [None,"uri", (U.string_of_uri uri) ;
 184              None,"noType",(string_of_int i) ;
 185              None,"noConstr",(string_of_int j) ;
 186              None,"id",id ; None,"sort",sort]
 187           ) exp_named_subst
 188      | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
 189         let sort = find_sort id in
 190          X.xml_nempty "MUTCASE"
 191           [None,"uriType",(U.string_of_uri uri) ;
 192            None,"noType", (string_of_int typeno) ;
 193            None,"id", id ; None,"sort",sort]
 194           [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
 195              X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
 196              List.fold_right
 197               (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
 198               patterns [<>]
 199           >]
 200      | C.AFix (id, no, funs) ->
 201         let sort = find_sort id in
 202          X.xml_nempty "FIX"
 203           [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
 204           [< List.fold_right
 205               (fun (id,fi,ai,ti,bi) i ->
 206                 [< X.xml_nempty "FixFunction"
 207                     [None,"id",id ; None,"name", fi ;
 208                      None,"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 = find_sort id in
 218          X.xml_nempty "COFIX"
 219           [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
 220           [< List.fold_right
 221               (fun (id,fi,ti,bi) i ->
 222                 [< X.xml_nempty "CofixFunction" [None,"id",id ; None,"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 -> [None,"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" [None,"relUri", relUri] (aux arg) >]
 257          ) [<>] subst
 258      >]
 259   in
 260    aux
 261 ;;
 262
 263 let xml_of_attrs attributes =
 264   let class_of = function
 265     | `Coercion -> "coercion"
 266     | `Elim Cic.Prop -> "elimProp"
 267     | `Elim Cic.CProp -> "elimCProp"
 268     | `Elim Cic.Set -> "elimSet"
 269     | `Elim (Cic.Type _) -> "elimType"
 270     | `Record -> "record"
 271     | `Projection -> "projection"
 272   in
 273   let xml_attr_of = function
 274     | `Generated -> None, "generated", "true"
 275     | `Class c -> None, "class", class_of c
 276   in
 277   let xml_attrs = List.map xml_attr_of attributes in
 278   Xml.xml_empty "attributes" xml_attrs
 279
 280 let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
 281  let find_sort id =
 282    Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)
 283  in
 284  let module C = Cic in
 285  let module X = Xml in
 286  let module U = UriManager in
 287   let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in
 288    match obj with
 289        C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) ->
 290         let params' = param_attribute_of_params params in
 291         let xml_attrs = xml_of_attrs obj_attrs in
 292         let xml_for_current_proof_body =
 293 (*CSC: Should the CurrentProof also have the list of variables it depends on? *)
 294 (*CSC: I think so. Not implemented yet.                                       *)
 295          X.xml_nempty "CurrentProof"
 296           [None,"of",UriManager.string_of_uri uri ; None,"id", id]
 297           [< xml_attrs;
 298             List.fold_left
 299               (fun i (cid,n,canonical_context,t) ->
 300                 [< i ;
 301                    X.xml_nempty "Conjecture"
 302                     [None,"id",cid ; None,"no",(string_of_int n)]
 303                     [< List.fold_left
 304                         (fun i (hid,t) ->
 305                           [< (match t with
 306                                  Some (n,C.ADecl t) ->
 307                                   X.xml_nempty "Decl"
 308                                    (match n with
 309                                        C.Name n' ->
 310                                         [None,"id",hid;None,"name",n']
 311                                      | C.Anonymous -> [None,"id",hid])
 312                                    (print_term ids_to_inner_sorts t)
 313                                | Some (n,C.ADef t) ->
 314                                   X.xml_nempty "Def"
 315                                    (match n with
 316                                        C.Name n' ->
 317                                         [None,"id",hid;None,"name",n']
 318                                      | C.Anonymous -> [None,"id",hid])
 319                                    (print_term ids_to_inner_sorts t)
 320                               | None -> X.xml_empty "Hidden" [None,"id",hid]
 321                              ) ;
 322                              i
 323                           >]
 324                         ) [< >] canonical_context ;
 325                        X.xml_nempty "Goal" []
 326                         (print_term ids_to_inner_sorts t)
 327                     >]
 328                 >])
 329               [< >] conjectures ;
 330              X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
 331         in
 332         let xml_for_current_proof_type =
 333          X.xml_nempty "ConstantType"
 334           [None,"name",n ; None,"params",params' ; None,"id", id]
 335           (print_term ids_to_inner_sorts ty)
 336         in
 337         let xmlbo =
 338          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 339             X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^ dtdname ^ "\">\n");
 340             xml_for_current_proof_body
 341          >] in
 342         let xmlty =
 343          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 344             X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
 345             xml_for_current_proof_type
 346          >]
 347         in
 348          xmlty, Some xmlbo
 349      | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) ->
 350         let params' = param_attribute_of_params params in
 351         let xml_attrs = xml_of_attrs obj_attrs in
 352         let xmlbo =
 353          match bo with
 354             None -> None
 355           | Some bo ->
 356              Some
 357               [< X.xml_cdata
 358                   "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 359                  X.xml_cdata
 360                   ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
 361                  X.xml_nempty "ConstantBody"
 362                   [None,"for",UriManager.string_of_uri uri ;
 363                    None,"params",params' ; None,"id", id]
 364                   [< print_term ids_to_inner_sorts bo >]
 365               >]
 366         in
 367         let xmlty =
 368          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 369             X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
 370              X.xml_nempty "ConstantType"
 371               [None,"name",n ; None,"params",params' ; None,"id", id]
 372               [< xml_attrs; print_term ids_to_inner_sorts ty >]
 373          >]
 374         in
 375          xmlty, xmlbo
 376      | C.AVariable (id,n,bo,ty,params,obj_attrs) ->
 377         let params' = param_attribute_of_params params in
 378         let xml_attrs = xml_of_attrs obj_attrs in
 379         let xmlbo =
 380          match bo with
 381             None -> [< >]
 382           | Some bo ->
 383              X.xml_nempty "body" [] [< print_term ids_to_inner_sorts bo >]
 384         in
 385         let aobj =
 386          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 387             X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
 388              X.xml_nempty "Variable"
 389               [None,"name",n ; None,"params",params' ; None,"id", id]
 390               [< xml_attrs; xmlbo;
 391                  X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
 392               >]
 393          >]
 394         in
 395          aobj, None
 396      | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) ->
 397         let params' = param_attribute_of_params params in
 398         let xml_attrs = xml_of_attrs obj_attrs in
 399          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 400             X.xml_cdata
 401              ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
 402             X.xml_nempty "InductiveDefinition"
 403              [None,"noParams",string_of_int nparams ;
 404               None,"id",id ;
 405               None,"params",params']
 406              [< xml_attrs;
 407                 (List.fold_left
 408                   (fun i (id,typename,finite,arity,cons) ->
 409                     [< i ;
 410                        X.xml_nempty "InductiveType"
 411                         [None,"id",id ; None,"name",typename ;
 412                          None,"inductive",(string_of_bool finite)
 413                         ]
 414                         [< X.xml_nempty "arity" []
 415                             (print_term ids_to_inner_sorts arity) ;
 416                            (List.fold_left
 417                             (fun i (name,lc) ->
 418                               [< i ;
 419                                  X.xml_nempty "Constructor"
 420                                   [None,"name",name]
 421                                   (print_term ids_to_inner_sorts lc)
 422                               >]) [<>] cons
 423                            )
 424                         >]
 425                     >]
 426                   ) [< >] tys
 427                 )
 428              >]
 429          >], None
 430 ;;
 431
 432 let
 433  print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types
 434   ~ask_dtd_to_the_getter
 435 =
 436  let module C2A = Cic2acic in
 437  let module X = Xml in
 438   let dtdname = dtdname ~ask_dtd_to_the_getter "cictypes.dtd" in
 439    [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 440       X.xml_cdata
 441        ("<!DOCTYPE InnerTypes SYSTEM \"" ^ dtdname ^ "\">\n") ;
 442       X.xml_nempty "InnerTypes" [None,"of",UriManager.string_of_uri curi]
 443        (Hashtbl.fold
 444          (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
 445            [< x ;
 446               X.xml_nempty "TYPE" [None,"of",id]
 447                [< X.xml_nempty "synthesized" []
 448                  [< print_term ids_to_inner_sorts synty >] ;
 449                  match expty with
 450                    None -> [<>]
 451                  | Some expty' -> X.xml_nempty "expected" []
 452                     [< print_term ids_to_inner_sorts expty' >]
 453                >]
 454            >]
 455          ) ids_to_inner_types [<>]
 456        )
 457    >]
 458 ;;