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) ->
  53         let sort = Hashtbl.find ids_to_inner_sorts id in
  54          X.xml_empty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort]
  55      | C.ASort (id,s) ->
  56         let string_of_sort =
  57          function
  58             C.Prop -> "Prop"
  59           | C.Set  -> "Set"
  60           | C.Type -> "Type"
  61         in
  62          X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
  63      | C.AImplicit _ -> raise NotImplemented
  64      | C.AProd (id,C.Anonimous,s,t) ->
  65         let ty = Hashtbl.find ids_to_inner_sorts id in
  66          X.xml_nempty "PROD" ["id",id ; "type",ty]
  67           [< X.xml_nempty "source" [] (aux s) ;
  68              X.xml_nempty "target" [] (aux t)
  69           >]
  70      | C.AProd (xid,C.Name id,s,t) ->
  71         let ty = Hashtbl.find ids_to_inner_sorts xid in
  72          X.xml_nempty "PROD" ["id",xid ; "type",ty]
  73           [< X.xml_nempty "source" [] (aux s) ;
  74              X.xml_nempty "target" ["binder",id] (aux t)
  75           >]
  76      | C.ACast (id,v,t) ->
  77         let sort = Hashtbl.find ids_to_inner_sorts id in
  78          X.xml_nempty "CAST" ["id",id ; "sort",sort]
  79           [< X.xml_nempty "term" [] (aux v) ;
  80              X.xml_nempty "type" [] (aux t)
  81           >]
  82      | C.ALambda (id,C.Anonimous,s,t) ->
  83         let sort = Hashtbl.find ids_to_inner_sorts id in
  84          X.xml_nempty "LAMBDA" ["id",id ; "sort",sort]
  85           [< X.xml_nempty "source" [] (aux s) ;
  86              X.xml_nempty "target" [] (aux t)
  87           >]
  88      | C.ALambda (xid,C.Name id,s,t) ->
  89         let sort = Hashtbl.find ids_to_inner_sorts xid in
  90          X.xml_nempty "LAMBDA" ["id",xid ; "sort",sort]
  91           [< X.xml_nempty "source" [] (aux s) ;
  92              X.xml_nempty "target" ["binder",id] (aux t)
  93           >]
  94      | C.ALetIn (xid,C.Anonimous,s,t) ->
  95        assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
  96      | C.ALetIn (xid,C.Name id,s,t) ->
  97         let sort = Hashtbl.find ids_to_inner_sorts xid in
  98          X.xml_nempty "LETIN" ["id",xid ; "sort",sort]
  99           [< X.xml_nempty "term" [] (aux s) ;
 100              X.xml_nempty "letintarget" ["binder",id] (aux t)
 101           >]
 102      | C.AAppl (id,li) ->
 103         let sort = Hashtbl.find ids_to_inner_sorts id in
 104          X.xml_nempty "APPLY" ["id",id ; "sort",sort]
 105           [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
 106           >]
 107      | C.AConst (id,uri,_) ->
 108         let sort = Hashtbl.find ids_to_inner_sorts id in
 109          X.xml_empty "CONST"
 110           ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
 111      | C.AAbst (id,uri) -> raise NotImplemented
 112      | C.AMutInd (id,uri,_,i) ->
 113         X.xml_empty "MUTIND"
 114          ["uri", (U.string_of_uri uri) ;
 115           "noType",(string_of_int i) ;
 116           "id",id]
 117      | C.AMutConstruct (id,uri,_,i,j) ->
 118         let sort = Hashtbl.find ids_to_inner_sorts id in
 119          X.xml_empty "MUTCONSTRUCT"
 120           ["uri", (U.string_of_uri uri) ;
 121            "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
 122            "id",id ; "sort",sort]
 123      | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
 124         let sort = Hashtbl.find ids_to_inner_sorts id in
 125          X.xml_nempty "MUTCASE"
 126           ["uriType",(U.string_of_uri uri) ;
 127            "noType", (string_of_int typeno) ;
 128            "id", id ; "sort",sort]
 129           [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
 130              X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
 131              List.fold_right
 132               (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
 133               patterns [<>]
 134           >]
 135      | C.AFix (id, no, funs) ->
 136         let sort = Hashtbl.find ids_to_inner_sorts id in
 137          X.xml_nempty "FIX"
 138           ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
 139           [< List.fold_right
 140               (fun (fi,ai,ti,bi) i ->
 141                 [< X.xml_nempty "FixFunction"
 142                     ["name", fi; "recIndex", (string_of_int ai)]
 143                     [< X.xml_nempty "type" [] [< aux ti >] ;
 144                        X.xml_nempty "body" [] [< aux bi >]
 145                     >] ;
 146                    i
 147                 >]
 148               ) funs [<>]
 149           >]
 150      | C.ACoFix (id,no,funs) ->
 151         let sort = Hashtbl.find ids_to_inner_sorts id in
 152          X.xml_nempty "COFIX"
 153           ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
 154           [< List.fold_right
 155               (fun (fi,ti,bi) i ->
 156                 [< X.xml_nempty "CofixFunction" ["name", fi]
 157                     [< X.xml_nempty "type" [] [< aux ti >] ;
 158                        X.xml_nempty "body" [] [< aux bi >]
 159                     >] ;
 160                    i
 161                 >]
 162               ) funs [<>]
 163           >]
 164  in
 165   aux
 166 ;;
 167
 168 exception NotImplemented;;
 169
 170 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
 171 let print_object curi ids_to_inner_sorts =
 172  let rec aux =
 173   let module C = Cic in
 174   let module X = Xml in
 175   let module U = UriManager in
 176     function
 177        C.ACurrentProof (id,n,conjectures,bo,ty) ->
 178         X.xml_nempty "CurrentProof" ["name",n ; "id", id]
 179          [< List.fold_left
 180              (fun i (n,t) ->
 181                [< i ;
 182                   X.xml_nempty "Conjecture" ["no",(string_of_int n)]
 183                    (print_term curi ids_to_inner_sorts t)
 184                >])
 185              [<>] conjectures ;
 186             X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
 187             X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty)  >]
 188      | C.ADefinition (id,n,bo,ty,C.Actual params) ->
 189         let params' =
 190          List.fold_right
 191           (fun (_,x) i ->
 192             List.fold_right
 193              (fun x i ->
 194                U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i'
 195              ) x "" ^ match i with "" -> "" | i' -> " " ^ i'
 196           ) params ""
 197         in
 198          X.xml_nempty "Definition" ["name",n ; "params",params' ; "id", id]
 199           [< X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
 200              X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty)  >]
 201      | C.ADefinition _ -> assert false
 202      | _ -> raise NotImplemented
 203  in
 204   aux
 205 ;;
 206
 207 let print_inner_types curi ids_to_inner_sorts ids_to_inner_types =
 208  let module X = Xml in
 209   X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
 210    (Hashtbl.fold
 211      (fun id ty x ->
 212        [< x ;
 213           X.xml_nempty "TYPE" ["of",id]
 214            (print_term curi ids_to_inner_sorts ty)
 215        >]
 216      ) ids_to_inner_types [<>]
 217    )
 218 ;;