helm/interface/cic2Xml.ml

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