X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_annotations%2FcicAnnotation2Xml.ml;fp=helm%2Focaml%2Fcic_annotations%2FcicAnnotation2Xml.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=23c3a9b68446a3812f8682a7c2a0e96c78051ac4;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml deleted file mode 100644 index 23c3a9b68..000000000 --- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml +++ /dev/null @@ -1,165 +0,0 @@ -(* 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 NotImplemented;; - -let dtdname = "http://www.cs.unibo.it/helm/dtd/annotations.dtd";; - -let get_ann ids_to_annotations = - CicXPath.get_annotation ids_to_annotations -;; - -let print_ann i2a id = - let module X = Xml in - let ann = get_ann i2a id in - match ann with - None -> [<>] - | Some ann -> (X.xml_nempty "Annotation" [None,"of", id] (X.xml_cdata ann)) -;; - -(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) -(* It takes in input a hash table mapping ids to annotations, an annotated -term, and gives back a Xml.token Stream.t representing the .ann file *) -let print_term i2a = - let rec aux = - let module C = Cic in - let module X = Xml in - let module U = UriManager in - function - C.ARel (id,_,_,_) -> print_ann i2a id - | C.AMeta (id,_,_) -> print_ann i2a id - | C.ASort (id,_) -> print_ann i2a id - | C.AImplicit _ -> raise NotImplemented - | C.AProd (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >] - | C.ACast (id,v,t) -> [< print_ann i2a id ; aux v ; aux t >] - | C.ALambda (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >] - | C.ALetIn (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >] - | C.AAppl (id,li) -> - [< print_ann i2a id ; - List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>] - >] - | C.AVar (id,_,exp_named_subst) - | C.AConst (id,_,exp_named_subst) - | C.AMutInd (id,_,_,exp_named_subst) - | C.AMutConstruct (id,_,_,_,exp_named_subst) -> - [< print_ann i2a id ; - List.fold_right - (fun (_,x) i -> [< aux x ; i >]) - exp_named_subst [<>] - >] - | C.AMutCase (id,_,_,ty,te,patterns) -> - [< print_ann i2a id ; - aux ty ; - aux te ; - List.fold_right - (fun x i -> [< aux x ; i>]) - patterns [<>] - >] - | C.AFix (id,_,funs) -> - [< print_ann i2a id ; - List.fold_right - (fun (_,_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>] - >] - | C.ACoFix (id,no,funs) -> - [< print_ann i2a id ; - List.fold_right - (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>] - >] - in - aux -;; - -let print_mutual_inductive_type i2a (_,_,_,arity,constructors) = - [< print_term i2a arity ; - List.fold_right - (fun (name,ty) i -> [< print_term i2a ty ; i >]) constructors [<>] - >] -;; - -let pp_annotation obj i2a curi = - let module C = Cic in - let module X = Xml in - [< X.xml_cdata "\n" ; - X.xml_cdata ("\n\n") ; - X.xml_nempty "Annotations" - [None, "of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)] - begin - match obj with - C.AConstant (xid, xidobj, _, te, ty, _) -> - [< print_ann i2a xid ; - (match xidobj,te with - Some xidobj, Some te -> - [< print_ann i2a xidobj ; - print_term i2a te - >] - | None, None -> [<>] - | _,_ -> assert false - ) ; - print_term i2a ty - >] - | C.AVariable (xid, _, bo, ty,_) -> - [< print_ann i2a xid ; - (match bo with - None -> [<>] - | Some bo -> print_term i2a bo - ) ; - print_term i2a ty - >] - | C.ACurrentProof (xid, xidobj, _, conjs, bo, ty,_) -> - [< print_ann i2a xid ; - print_ann i2a xidobj ; - List.fold_right - (fun (cid, _, context, t) i -> - [< print_ann i2a cid ; - List.fold_right - (fun (hid,context_entry) i -> - [ print_term i2a at - | Some (_,C.ADef at) -> print_term i2a at - | None -> [< >] - ) ; i - >] - ) context [< >]; - print_term i2a t ; i - >] - ) conjs [<>] ; - print_term i2a bo ; - print_term i2a ty - >] - | C.AInductiveDefinition (xid, tys, params, paramsno) -> - [< print_ann i2a xid ; - List.fold_right - (fun x i -> [< print_mutual_inductive_type i2a x ; i >]) - tys [< >] - >] - end - >] -;; - - -