(* Copyright (C) 2000, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

(*CSC codice cut & paste da cicPp e xmlcommand *)

exception ImpossiblePossible;;
exception NotImplemented;;
let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;

(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
let print_term curi =
 let rec aux =
  let module C = Cic in
  let module X = Xml in
  let module U = UriManager in
    function
       C.ARel (id,n,b) ->
        X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id]
     | C.AVar (id,uri) ->
        let vdepth = U.depth_of_uri uri
        and cdepth = U.depth_of_uri curi in
         X.xml_empty "VAR"
          ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
            (U.name_of_uri uri) ;
           "id",id]
     | C.AMeta (id,n) ->
        X.xml_empty "META" ["no",(string_of_int n) ; "id",id]
     | C.ASort (id,s) ->
        let string_of_sort =
         function
            C.Prop -> "Prop"
          | C.Set  -> "Set"
          | C.Type -> "Type"
        in
         X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
     | C.AImplicit _ -> raise NotImplemented
     | C.AProd (id,C.Anonimous,s,t) ->
        X.xml_nempty "PROD" ["id",id]
         [< X.xml_nempty "source" [] (aux s) ;
            X.xml_nempty "target" [] (aux t)
         >]
     | C.AProd (xid,C.Name id,s,t) ->
       X.xml_nempty "PROD" ["id",xid]
        [< X.xml_nempty "source" [] (aux s) ;
           X.xml_nempty "target" ["binder",id] (aux t)
        >]
     | C.ACast (id,v,t) ->
        X.xml_nempty "CAST" ["id",id]
         [< X.xml_nempty "term" [] (aux v) ;
            X.xml_nempty "type" [] (aux t)
         >]
     | C.ALambda (id,C.Anonimous,s,t) ->
        X.xml_nempty "LAMBDA" ["id",id]
         [< X.xml_nempty "source" [] (aux s) ;
            X.xml_nempty "target" [] (aux t)
         >]
     | C.ALambda (xid,C.Name id,s,t) ->
       X.xml_nempty "LAMBDA" ["id",xid]
        [< X.xml_nempty "source" [] (aux s) ;
           X.xml_nempty "target" ["binder",id] (aux t)
        >]
     | C.ALetIn (xid,C.Anonimous,s,t) ->
       assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
     | C.ALetIn (xid,C.Name id,s,t) ->
       X.xml_nempty "LETIN" ["id",xid]
        [< X.xml_nempty "term" [] (aux s) ;
           X.xml_nempty "letintarget" ["binder",id] (aux t)
        >]
     | C.AAppl (id,li) ->
        X.xml_nempty "APPLY" ["id",id]
         [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
         >]
     | C.AConst (id,uri,_) ->
        X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id]
     | C.AAbst (id,uri) -> raise NotImplemented
     | C.AMutInd (id,uri,_,i) ->
        X.xml_empty "MUTIND"
         ["uri", (U.string_of_uri uri) ;
          "noType",(string_of_int i) ;
          "id",id]
     | C.AMutConstruct (id,uri,_,i,j) ->
        X.xml_empty "MUTCONSTRUCT"
         ["uri", (U.string_of_uri uri) ;
          "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
          "id",id]
     | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
        X.xml_nempty "MUTCASE"
         ["uriType",(U.string_of_uri uri) ;
          "noType", (string_of_int typeno) ;
          "id", id]
         [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
            X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
            List.fold_right
             (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
             patterns [<>]
         >]
     | C.AFix (id, no, funs) ->
       X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id]
        [< List.fold_right
            (fun (fi,ai,ti,bi) i ->
              [< X.xml_nempty "FixFunction"
                  ["name", fi; "recIndex", (string_of_int ai)]
                  [< X.xml_nempty "type" [] [< aux ti >] ;
                     X.xml_nempty "body" [] [< aux bi >]
                  >] ;
                 i
              >]
            ) funs [<>]
        >]
     | C.ACoFix (id,no,funs) ->
       X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id]
        [< List.fold_right
            (fun (fi,ti,bi) i ->
              [< X.xml_nempty "CofixFunction" ["name", fi]
                  [< X.xml_nempty "type" [] [< aux ti >] ;
                     X.xml_nempty "body" [] [< aux bi >]
                  >] ;
                 i
              >]
            ) funs [<>]
        >]
 in
  aux
;;