helm/gTopLevel/cic2Xml.ml

   1
   2 (* Copyright (C) 2000, HELM Team.
   3  *
   4  * This file is part of HELM, an Hypertextual, Electronic
   5  * Library of Mathematics, developed at the Computer Science
   6  * Department, University of Bologna, Italy.
   7  *
   8  * HELM is free software; you can redistribute it and/or
   9  * modify it under the terms of the GNU General Public License
  10  * as published by the Free Software Foundation; either version 2
  11  * of the License, or (at your option) any later version.
  12  *
  13  * HELM is distributed in the hope that it will be useful,
  14  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  15  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  16  * GNU General Public License for more details.
  17  *
  18  * You should have received a copy of the GNU General Public License
  19  * along with HELM; if not, write to the Free Software
  20  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  21  * MA  02111-1307, USA.
  22  *
  23  * For details, see the HELM World-Wide-Web page,
  24  * http://cs.unibo.it/helm/.
  25  *)
  26
  27 (*CSC codice cut & paste da cicPp e xmlcommand *)
  28
  29 exception ImpossiblePossible;;
  30 exception NotImplemented;;
  31 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
  32
  33 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
  34 let print_term curi ids_to_inner_sorts =
  35  let rec aux =
  36   let module C = Cic in
  37   let module X = Xml in
  38   let module U = UriManager in
  39     function
  40        C.ARel (id,n,b) ->
  41         let sort = Hashtbl.find ids_to_inner_sorts id in
  42          X.xml_empty "REL"
  43           ["value",(string_of_int n) ; "binder",b ; "id",id ; "sort",sort]
  44      | C.AVar (id,uri) ->
  45         let vdepth = U.depth_of_uri uri
  46         and cdepth = U.depth_of_uri curi
  47         and sort = Hashtbl.find ids_to_inner_sorts id in
  48          X.xml_empty "VAR"
  49           ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
  50             (U.name_of_uri uri) ;
  51            "id",id ; "sort",sort]
  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 (id,C.Anonimous,s,t) ->
  73         let ty = Hashtbl.find ids_to_inner_sorts id in
  74          X.xml_nempty "PROD" ["id",id ; "type",ty]
  75           [< X.xml_nempty "source" [] (aux s) ;
  76              X.xml_nempty "target" [] (aux t)
  77           >]
  78      | C.AProd (xid,C.Name id,s,t) ->
  79         let ty = Hashtbl.find ids_to_inner_sorts xid in
  80          X.xml_nempty "PROD" ["id",xid ; "type",ty]
  81           [< X.xml_nempty "source" [] (aux s) ;
  82              X.xml_nempty "target" ["binder",id] (aux t)
  83           >]
  84      | C.ACast (id,v,t) ->
  85         let sort = Hashtbl.find ids_to_inner_sorts id in
  86          X.xml_nempty "CAST" ["id",id ; "sort",sort]
  87           [< X.xml_nempty "term" [] (aux v) ;
  88              X.xml_nempty "type" [] (aux t)
  89           >]
  90      | C.ALambda (id,C.Anonimous,s,t) ->
  91         let sort = Hashtbl.find ids_to_inner_sorts id in
  92          X.xml_nempty "LAMBDA" ["id",id ; "sort",sort]
  93           [< X.xml_nempty "source" [] (aux s) ;
  94              X.xml_nempty "target" [] (aux t)
  95           >]
  96      | C.ALambda (xid,C.Name id,s,t) ->
  97         let sort = Hashtbl.find ids_to_inner_sorts xid in
  98          X.xml_nempty "LAMBDA" ["id",xid ; "sort",sort]
  99           [< X.xml_nempty "source" [] (aux s) ;
 100              X.xml_nempty "target" ["binder",id] (aux t)
 101           >]
 102      | C.ALetIn (xid,C.Anonimous,s,t) ->
 103        assert false
 104      | C.ALetIn (xid,C.Name id,s,t) ->
 105         let sort = Hashtbl.find ids_to_inner_sorts xid in
 106          X.xml_nempty "LETIN" ["id",xid ; "sort",sort]
 107           [< X.xml_nempty "term" [] (aux s) ;
 108              X.xml_nempty "letintarget" ["binder",id] (aux t)
 109           >]
 110      | C.AAppl (id,li) ->
 111         let sort = Hashtbl.find ids_to_inner_sorts id in
 112          X.xml_nempty "APPLY" ["id",id ; "sort",sort]
 113           [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
 114           >]
 115      | C.AConst (id,uri,_) ->
 116         let sort = Hashtbl.find ids_to_inner_sorts id in
 117          X.xml_empty "CONST"
 118           ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
 119      | C.AAbst (id,uri) -> raise NotImplemented
 120      | C.AMutInd (id,uri,_,i) ->
 121         X.xml_empty "MUTIND"
 122          ["uri", (U.string_of_uri uri) ;
 123           "noType",(string_of_int i) ;
 124           "id",id]
 125      | C.AMutConstruct (id,uri,_,i,j) ->
 126         let sort = Hashtbl.find ids_to_inner_sorts id in
 127          X.xml_empty "MUTCONSTRUCT"
 128           ["uri", (U.string_of_uri uri) ;
 129            "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
 130            "id",id ; "sort",sort]
 131      | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
 132         let sort = Hashtbl.find ids_to_inner_sorts id in
 133          X.xml_nempty "MUTCASE"
 134           ["uriType",(U.string_of_uri uri) ;
 135            "noType", (string_of_int typeno) ;
 136            "id", id ; "sort",sort]
 137           [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
 138              X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
 139              List.fold_right
 140               (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
 141               patterns [<>]
 142           >]
 143      | C.AFix (id, no, funs) ->
 144         let sort = Hashtbl.find ids_to_inner_sorts id in
 145          X.xml_nempty "FIX"
 146           ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
 147           [< List.fold_right
 148               (fun (fi,ai,ti,bi) i ->
 149                 [< X.xml_nempty "FixFunction"
 150                     ["name", fi; "recIndex", (string_of_int ai)]
 151                     [< X.xml_nempty "type" [] [< aux ti >] ;
 152                        X.xml_nempty "body" [] [< aux bi >]
 153                     >] ;
 154                    i
 155                 >]
 156               ) funs [<>]
 157           >]
 158      | C.ACoFix (id,no,funs) ->
 159         let sort = Hashtbl.find ids_to_inner_sorts id in
 160          X.xml_nempty "COFIX"
 161           ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
 162           [< List.fold_right
 163               (fun (fi,ti,bi) i ->
 164                 [< X.xml_nempty "CofixFunction" ["name", fi]
 165                     [< X.xml_nempty "type" [] [< aux ti >] ;
 166                        X.xml_nempty "body" [] [< aux bi >]
 167                     >] ;
 168                    i
 169                 >]
 170               ) funs [<>]
 171           >]
 172  in
 173   aux
 174 ;;
 175
 176 exception NotImplemented;;
 177
 178 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
 179 let print_object curi ids_to_inner_sorts =
 180  let rec aux =
 181   let module C = Cic in
 182   let module X = Xml in
 183   let module U = UriManager in
 184     function
 185        C.ACurrentProof (id,n,conjectures,bo,ty) ->
 186         X.xml_nempty "CurrentProof" ["name",n ; "id", id]
 187          [< List.fold_left
 188              (fun i (cid,n,canonical_context,t) ->
 189                [< i ;
 190                   X.xml_nempty "Conjecture"
 191                    ["id", cid ; "no",(string_of_int n)]
 192                    [< List.fold_left
 193                        (fun i (hid,t) ->
 194                          [< (match t with
 195                                Some (n,C.ADecl t) ->
 196                                 X.xml_nempty "Decl"
 197                                  (match n with
 198                                      C.Name n' -> ["id",hid;"name",n']
 199                                    | C.Anonimous -> ["id",hid])
 200                                  (print_term curi ids_to_inner_sorts t)
 201                              | Some (n,C.ADef t) ->
 202                                 X.xml_nempty "Def"
 203                                  (match n with
 204                                      C.Name n' -> ["id",hid;"name",n']
 205                                    | C.Anonimous -> ["id",hid])
 206                                  (print_term curi ids_to_inner_sorts t)
 207                              | None -> X.xml_empty "Hidden" ["id",hid]
 208                             ) ;
 209                             i
 210                          >]
 211                        ) [< >] canonical_context ;
 212                       X.xml_nempty "Goal" []
 213                        (print_term curi ids_to_inner_sorts t)
 214                    >]
 215                >])
 216              [<>] conjectures ;
 217             X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
 218             X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty)  >]
 219      | C.ADefinition (id,n,bo,ty,C.Actual params) ->
 220         let params' =
 221          List.fold_right
 222           (fun (_,x) i ->
 223             List.fold_right
 224              (fun x i ->
 225                U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i'
 226              ) x "" ^ match i with "" -> "" | i' -> " " ^ i'
 227           ) params ""
 228         in
 229          X.xml_nempty "Definition" ["name",n ; "params",params' ; "id", id]
 230           [< X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
 231              X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty)  >]
 232      | C.ADefinition _ -> assert false
 233      | _ -> raise NotImplemented
 234  in
 235   aux
 236 ;;
 237
 238 let print_inner_types curi ids_to_inner_sorts ids_to_inner_types =
 239  let module X = Xml in
 240   X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
 241    (Hashtbl.fold
 242      (fun id ty x ->
 243        [< x ;
 244           X.xml_nempty "TYPE" ["of",id]
 245            (print_term curi ids_to_inner_sorts ty)
 246        >]
 247      ) ids_to_inner_types [<>]
 248    )
 249 ;;