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