helm/interface/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 exception BinderNotSpecified;;
  32
  33 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
  34
  35 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
  36 let print_term curi =
  37  let rec aux =
  38   let module C = Cic in
  39   let module X = Xml in
  40   let module U = UriManager in
  41     function
  42        C.ARel (id,_,n,Some b) ->
  43         X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id]
  44      | C.ARel _ -> raise BinderNotSpecified
  45      | C.AVar (id,_,uri) ->
  46         let vdepth = U.depth_of_uri uri
  47         and cdepth = U.depth_of_uri curi in
  48          X.xml_empty "VAR"
  49           ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
  50             (U.name_of_uri uri) ;
  51            "id",id]
  52      | C.AMeta (id,_,n) ->
  53         X.xml_empty "META" ["no",(string_of_int n) ; "id",id]
  54      | C.ASort (id,_,s) ->
  55         let string_of_sort =
  56          function
  57             C.Prop -> "Prop"
  58           | C.Set  -> "Set"
  59           | C.Type -> "Type"
  60         in
  61          X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
  62      | C.AImplicit _ -> raise NotImplemented
  63      | C.AProd (id,_,C.Anonimous,s,t) ->
  64         X.xml_nempty "PROD" ["id",id]
  65          [< X.xml_nempty "source" [] (aux s) ;
  66             X.xml_nempty "target" [] (aux t)
  67          >]
  68      | C.AProd (xid,_,C.Name id,s,t) ->
  69        X.xml_nempty "PROD" ["id",xid]
  70         [< X.xml_nempty "source" [] (aux s) ;
  71            X.xml_nempty "target" ["binder",id] (aux t)
  72         >]
  73      | C.ACast (id,_,v,t) ->
  74         X.xml_nempty "CAST" ["id",id]
  75          [< X.xml_nempty "term" [] (aux v) ;
  76             X.xml_nempty "type" [] (aux t)
  77          >]
  78      | C.ALambda (id,_,C.Anonimous,s,t) ->
  79         X.xml_nempty "LAMBDA" ["id",id]
  80          [< X.xml_nempty "source" [] (aux s) ;
  81             X.xml_nempty "target" [] (aux t)
  82          >]
  83      | C.ALambda (xid,_,C.Name id,s,t) ->
  84        X.xml_nempty "LAMBDA" ["id",xid]
  85         [< X.xml_nempty "source" [] (aux s) ;
  86            X.xml_nempty "target" ["binder",id] (aux t)
  87         >]
  88      | C.ALetIn (xid,_,C.Anonimous,s,t) ->
  89        assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
  90      | C.ALetIn (xid,_,C.Name id,s,t) ->
  91        X.xml_nempty "LETIN" ["id",xid]
  92         [< X.xml_nempty "term" [] (aux s) ;
  93            X.xml_nempty "letintarget" ["binder",id] (aux t)
  94         >]
  95      | C.AAppl (id,_,li) ->
  96         X.xml_nempty "APPLY" ["id",id]
  97          [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
  98          >]
  99      | C.AConst (id,_,uri,_) ->
 100         X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id]
 101      | C.AAbst (id,_,uri) -> raise NotImplemented
 102      | C.AMutInd (id,_,uri,_,i) ->
 103         X.xml_empty "MUTIND"
 104          ["uri", (U.string_of_uri uri) ;
 105           "noType",(string_of_int i) ;
 106           "id",id]
 107      | C.AMutConstruct (id,_,uri,_,i,j) ->
 108         X.xml_empty "MUTCONSTRUCT"
 109          ["uri", (U.string_of_uri uri) ;
 110           "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
 111           "id",id]
 112      | C.AMutCase (id,_,uri,_,typeno,ty,te,patterns) ->
 113         X.xml_nempty "MUTCASE"
 114          ["uriType",(U.string_of_uri uri) ;
 115           "noType", (string_of_int typeno) ;
 116           "id", id]
 117          [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
 118             X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
 119             List.fold_right
 120              (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
 121              patterns [<>]
 122          >]
 123      | C.AFix (id, _, no, funs) ->
 124        X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id]
 125         [< List.fold_right
 126             (fun (fi,ai,ti,bi) i ->
 127               [< X.xml_nempty "FixFunction"
 128                   ["name", fi; "recIndex", (string_of_int ai)]
 129                   [< X.xml_nempty "type" [] [< aux ti >] ;
 130                      X.xml_nempty "body" [] [< aux bi >]
 131                   >] ;
 132                  i
 133               >]
 134             ) funs [<>]
 135         >]
 136      | C.ACoFix (id,_,no,funs) ->
 137        X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id]
 138         [< List.fold_right
 139             (fun (fi,ti,bi) i ->
 140               [< X.xml_nempty "CofixFunction" ["name", fi]
 141                   [< X.xml_nempty "type" [] [< aux ti >] ;
 142                      X.xml_nempty "body" [] [< aux bi >]
 143                   >] ;
 144                  i
 145               >]
 146             ) funs [<>]
 147         >]
 148  in
 149   aux
 150 ;;
 151
 152 let encode params =
 153  List.fold_right
 154   (fun (n,l) i ->
 155     match l with
 156        [] -> i
 157      | _ ->
 158        string_of_int n ^ ": " ^
 159        String.concat " " (List.map UriManager.name_of_uri l) ^
 160        i
 161   ) params ""
 162 ;;
 163
 164 let print_mutual_inductive_type curi (typename,inductive,arity,constructors) =
 165  let module C = Cic in
 166  let module X = Xml in
 167   [< X.xml_nempty "InductiveType"
 168       ["name",typename ;
 169        "inductive",(string_of_bool inductive)
 170       ]
 171       [< X.xml_nempty "arity" [] (print_term curi arity) ;
 172          (List.fold_right
 173           (fun (name,ty,_) i ->
 174             [< X.xml_nempty "Constructor" ["name",name]
 175                 (print_term curi ty) ;
 176                i
 177             >])
 178           constructors
 179           [<>]
 180          )
 181       >]
 182   >]
 183 ;;
 184
 185 let pp obj curi =
 186  let module C = Cic in
 187  let module X = Xml in
 188   match obj with
 189      C.ADefinition (xid, _, id, te, ty, params) ->
 190       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 191          X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
 192          X.xml_nempty "Definition"
 193           (["name", id ; "id",xid] @
 194            match params with
 195               C.Possible _ -> raise ImpossiblePossible
 196               (*CSC params are kept in inverted order in the internal *)
 197               (* representation (the order of application)            *)
 198             | C.Actual fv' -> ["params",(encode (List.rev fv'))])
 199           [< X.xml_nempty "body" [] (print_term curi te) ;
 200              X.xml_nempty "type"  [] (print_term curi ty) >]
 201       >]
 202    | C.AAxiom (xid, _, id, ty, params) ->
 203       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 204          X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
 205          X.xml_nempty "Axiom"
 206           (*CSC params are kept in inverted order in the internal *)
 207           (* representation (the order of application)            *)
 208           ["name",id ; "params",(encode (List.rev params)) ; "id",xid]
 209           [< X.xml_nempty "type" [] (print_term curi ty) >]
 210       >]
 211    | C.AVariable (xid, _, name, bo, ty) ->
 212       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 213          X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
 214          X.xml_nempty "Variable" ["name",name ; "id",xid]
 215           [< (match bo with
 216                  None -> [<>]
 217                | Some bo -> X.xml_nempty "body" [] (print_term curi bo)
 218              ) ;
 219              X.xml_nempty "type" [] (print_term curi ty)
 220           >]
 221       >]
 222    | C.ACurrentProof (xid, _, name, conjs, bo, ty) ->
 223       [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 224          X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n");
 225          X.xml_nempty "CurrentProof" ["name",name ; "id",xid]
 226           [< List.fold_right
 227               (fun (j,t) i ->
 228                 [< X.xml_nempty "Conjecture" ["no",(string_of_int j)]
 229                     [< print_term curi t >] ; i >])
 230               conjs [<>] ;
 231              X.xml_nempty "body" [] [< print_term curi bo >] ;
 232              X.xml_nempty "type" [] [< print_term curi ty >]
 233           >]
 234       >]
 235    | C.AInductiveDefinition (xid, _, tys, params, paramsno) ->
 236       let names =
 237        List.map
 238         (fun (typename,_,_,_) -> typename)
 239         tys
 240       in
 241        [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 242           X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
 243            dtdname ^ "\">\n\n") ;
 244           X.xml_nempty "InductiveDefinition"
 245            (*CSC params are kept in inverted order in the internal *)
 246            (* representation (the order of application)            *)
 247            ["noParams",string_of_int paramsno ;
 248             "params",(encode (List.rev params)) ;
 249             "id",xid]
 250           [< List.fold_right
 251               (fun x i -> [< print_mutual_inductive_type curi x ; i >])
 252               tys [< >]
 253            >]
 254        >]
 255 ;;