(* 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.AMutInd (id,uri,_,i) -> | 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 ;; let encode params = List.fold_right (fun (n,l) i -> match l with [] -> i | _ -> string_of_int n ^ ": " ^ String.concat " " (List.map UriManager.name_of_uri l) ^ i ) params "" ;; let print_mutual_inductive_type curi (typename,inductive,arity,constructors) = let module C = Cic in let module X = Xml in [< X.xml_nempty "InductiveType" ["name",typename ; "inductive",(string_of_bool inductive) ] [< X.xml_nempty "arity" [] (print_term curi arity) ; (List.fold_right (fun (name,ty,_) i -> [< X.xml_nempty "Constructor" ["name",name] (print_term curi ty) ; i >]) constructors [<>] ) >] >] ;; let pp obj curi = let module C = Cic in let module X = Xml in match obj with C.ADefinition (xid, id, te, ty, params) -> [< X.xml_cdata "\n" ; X.xml_cdata ("\n\n") ; X.xml_nempty "Definition" (["name", id ; "id",xid] @ match params with C.Possible _ -> raise ImpossiblePossible (*CSC params are kept in inverted order in the internal *) (* representation (the order of application) *) | C.Actual fv' -> ["params",(encode (List.rev fv'))]) [< X.xml_nempty "body" [] (print_term curi te) ; X.xml_nempty "type" [] (print_term curi ty) >] >] | C.AAxiom (xid, id, ty, params) -> [< X.xml_cdata "\n" ; X.xml_cdata ("\n\n") ; X.xml_nempty "Axiom" (*CSC params are kept in inverted order in the internal *) (* representation (the order of application) *) ["name",id ; "params",(encode (List.rev params)) ; "id",xid] [< X.xml_nempty "type" [] (print_term curi ty) >] >] | C.AVariable (xid, name, bo, ty) -> [< X.xml_cdata "\n" ; X.xml_cdata ("\n\n") ; X.xml_nempty "Variable" ["name",name ; "id",xid] [< (match bo with None -> [<>] | Some bo -> X.xml_nempty "body" [] (print_term curi bo) ) ; X.xml_nempty "type" [] (print_term curi ty) >] >] | C.ACurrentProof (xid, name, conjs, bo, ty) -> [< X.xml_cdata "\n" ; X.xml_cdata ("\n\n"); X.xml_nempty "CurrentProof" ["name",name ; "id",xid] [< List.fold_right (fun (j,t) i -> [< X.xml_nempty "Conjecture" ["no",(string_of_int j)] [< print_term curi t >] ; i >]) conjs [<>] ; X.xml_nempty "body" [] [< print_term curi bo >] ; X.xml_nempty "type" [] [< print_term curi ty >] >] >] | C.AInductiveDefinition (xid, tys, params, paramsno) -> let names = List.map (fun (typename,_,_,_) -> typename) tys in [< X.xml_cdata "\n" ; X.xml_cdata ("\n\n") ; X.xml_nempty "InductiveDefinition" (*CSC params are kept in inverted order in the internal *) (* representation (the order of application) *) ["noParams",string_of_int paramsno ; "params",(encode (List.rev params)) ; "id",xid] [< List.fold_right (fun x i -> [< print_mutual_inductive_type curi x ; i >]) tys [< >] >] >] ;;