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 =
  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         X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id]
  42      | C.AVar (id,uri) ->
  43         let vdepth = U.depth_of_uri uri
  44         and cdepth = U.depth_of_uri curi in
  45          X.xml_empty "VAR"
  46           ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
  47             (U.name_of_uri uri) ;
  48            "id",id]
  49      | C.AMeta (id,n) ->
  50         X.xml_empty "META" ["no",(string_of_int n) ; "id",id]
  51      | C.ASort (id,s) ->
  52         let string_of_sort =
  53          function
  54             C.Prop -> "Prop"
  55           | C.Set  -> "Set"
  56           | C.Type -> "Type"
  57         in
  58          X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
  59      | C.AImplicit _ -> raise NotImplemented
  60      | C.AProd (id,C.Anonimous,s,t) ->
  61         X.xml_nempty "PROD" ["id",id]
  62          [< X.xml_nempty "source" [] (aux s) ;
  63             X.xml_nempty "target" [] (aux t)
  64          >]
  65      | C.AProd (xid,C.Name id,s,t) ->
  66        X.xml_nempty "PROD" ["id",xid]
  67         [< X.xml_nempty "source" [] (aux s) ;
  68            X.xml_nempty "target" ["binder",id] (aux t)
  69         >]
  70      | C.ACast (id,v,t) ->
  71         X.xml_nempty "CAST" ["id",id]
  72          [< X.xml_nempty "term" [] (aux v) ;
  73             X.xml_nempty "type" [] (aux t)
  74          >]
  75      | C.ALambda (id,C.Anonimous,s,t) ->
  76         X.xml_nempty "LAMBDA" ["id",id]
  77          [< X.xml_nempty "source" [] (aux s) ;
  78             X.xml_nempty "target" [] (aux t)
  79          >]
  80      | C.ALambda (xid,C.Name id,s,t) ->
  81        X.xml_nempty "LAMBDA" ["id",xid]
  82         [< X.xml_nempty "source" [] (aux s) ;
  83            X.xml_nempty "target" ["binder",id] (aux t)
  84         >]
  85      | C.ALetIn (xid,C.Anonimous,s,t) ->
  86        assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
  87      | C.ALetIn (xid,C.Name id,s,t) ->
  88        X.xml_nempty "LETIN" ["id",xid]
  89         [< X.xml_nempty "term" [] (aux s) ;
  90            X.xml_nempty "letintarget" ["binder",id] (aux t)
  91         >]
  92      | C.AAppl (id,li) ->
  93         X.xml_nempty "APPLY" ["id",id]
  94          [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
  95          >]
  96      | C.AConst (id,uri,_) ->
  97         X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id]
  98      | C.AAbst (id,uri) -> raise NotImplemented
  99      | C.AMutInd (id,uri,_,i) ->
 100         X.xml_empty "MUTIND"
 101          ["uri", (U.string_of_uri uri) ;
 102           "noType",(string_of_int i) ;
 103           "id",id]
 104      | C.AMutConstruct (id,uri,_,i,j) ->
 105         X.xml_empty "MUTCONSTRUCT"
 106          ["uri", (U.string_of_uri uri) ;
 107           "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
 108           "id",id]
 109      | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
 110         X.xml_nempty "MUTCASE"
 111          ["uriType",(U.string_of_uri uri) ;
 112           "noType", (string_of_int typeno) ;
 113           "id", id]
 114          [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
 115             X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
 116             List.fold_right
 117              (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
 118              patterns [<>]
 119          >]
 120      | C.AFix (id, no, funs) ->
 121        X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id]
 122         [< List.fold_right
 123             (fun (fi,ai,ti,bi) i ->
 124               [< X.xml_nempty "FixFunction"
 125                   ["name", fi; "recIndex", (string_of_int ai)]
 126                   [< X.xml_nempty "type" [] [< aux ti >] ;
 127                      X.xml_nempty "body" [] [< aux bi >]
 128                   >] ;
 129                  i
 130               >]
 131             ) funs [<>]
 132         >]
 133      | C.ACoFix (id,no,funs) ->
 134        X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id]
 135         [< List.fold_right
 136             (fun (fi,ti,bi) i ->
 137               [< X.xml_nempty "CofixFunction" ["name", fi]
 138                   [< X.xml_nempty "type" [] [< aux ti >] ;
 139                      X.xml_nempty "body" [] [< aux bi >]
 140                   >] ;
 141                  i
 142               >]
 143             ) funs [<>]
 144         >]
 145  in
 146   aux
 147 ;;