X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Fcic_acic%2Fcic2Xml.ml;fp=components%2Fcic_acic%2Fcic2Xml.ml;h=0708a839f49439ddb424e5201f2ce75272b44198;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/cic_acic/cic2Xml.ml b/components/cic_acic/cic2Xml.ml new file mode 100644 index 000000000..0708a839f --- /dev/null +++ b/components/cic_acic/cic2Xml.ml @@ -0,0 +1,493 @@ +(* Copyright (C) 2000-2004, 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://helm.cs.unibo.it/ + *) + +(* $Id$ *) + +(*CSC codice cut & paste da cicPp e xmlcommand *) + +exception NotImplemented;; + +let dtdname ~ask_dtd_to_the_getter dtd = + if ask_dtd_to_the_getter then + Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd + else + "http://mowgli.cs.unibo.it/dtd/" ^ dtd +;; + +let param_attribute_of_params params = + String.concat " " (List.map UriManager.string_of_uri params) +;; + +(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) +let print_term ?ids_to_inner_sorts = + let find_sort name id = + match ids_to_inner_sorts with + None -> [] + | Some ids_to_inner_sorts -> + [None,name,Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)] + in + let rec aux = + let module C = Cic in + let module X = Xml in + let module U = UriManager in + function + C.ARel (id,idref,n,b) -> + let sort = find_sort "sort" id in + X.xml_empty "REL" + (sort @ + [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ; + None,"idref",idref]) + | C.AVar (id,uri,exp_named_subst) -> + let sort = find_sort "sort" id in + aux_subst uri + (X.xml_empty "VAR" + (sort @ [None,"uri",U.string_of_uri uri;None,"id",id])) + exp_named_subst + | C.AMeta (id,n,l) -> + let sort = find_sort "sort" id in + X.xml_nempty "META" + (sort @ [None,"no",(string_of_int n) ; None,"id",id]) + (List.fold_left + (fun i t -> + match t with + Some t' -> + [< i ; X.xml_nempty "substitution" [] (aux t') >] + | None -> + [< i ; X.xml_empty "substitution" [] >] + ) [< >] l) + | C.ASort (id,s) -> + let string_of_sort s = + Cic2acic.string_of_sort (Cic2acic.sort_of_sort s) + in + X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id] + | C.AImplicit _ -> raise NotImplemented + | C.AProd (last_id,_,_,_) as prods -> + let rec eat_prods = + function + C.AProd (id,n,s,t) -> + let prods,t' = eat_prods t in + (id,n,s)::prods,t' + | t -> [],t + in + let prods,t = eat_prods prods in + let sort = find_sort "type" last_id in + X.xml_nempty "PROD" sort + [< List.fold_left + (fun i (id,binder,s) -> + let sort = find_sort "type" (Cic2acic.source_id_of_id id) in + let attrs = + sort @ ((None,"id",id):: + match binder with + C.Anonymous -> [] + | C.Name b -> [None,"binder",b]) + in + [< i ; X.xml_nempty "decl" attrs (aux s) >] + ) [< >] prods ; + X.xml_nempty "target" [] (aux t) + >] + | C.ACast (id,v,t) -> + let sort = find_sort "sort" id in + X.xml_nempty "CAST" (sort @ [None,"id",id]) + [< X.xml_nempty "term" [] (aux v) ; + X.xml_nempty "type" [] (aux t) + >] + | C.ALambda (last_id,_,_,_) as lambdas -> + let rec eat_lambdas = + function + C.ALambda (id,n,s,t) -> + let lambdas,t' = eat_lambdas t in + (id,n,s)::lambdas,t' + | t -> [],t + in + let lambdas,t = eat_lambdas lambdas in + let sort = find_sort "sort" last_id in + X.xml_nempty "LAMBDA" sort + [< List.fold_left + (fun i (id,binder,s) -> + let sort = find_sort "type" (Cic2acic.source_id_of_id id) in + let attrs = + sort @ ((None,"id",id):: + match binder with + C.Anonymous -> [] + | C.Name b -> [None,"binder",b]) + in + [< i ; X.xml_nempty "decl" attrs (aux s) >] + ) [< >] lambdas ; + X.xml_nempty "target" [] (aux t) + >] + | C.ALetIn (xid,C.Anonymous,s,ty,t) -> + assert false + | C.ALetIn (last_id,C.Name _,_,_,_) as letins -> + let rec eat_letins = + function + C.ALetIn (id,n,s,ty,t) -> + let letins,t' = eat_letins t in + (id,n,s,ty)::letins,t' + | t -> [],t + in + let letins,t = eat_letins letins in + let sort = find_sort "sort" last_id in + X.xml_nempty "LETIN" sort + [< List.fold_left + (fun i (id,binder,s,ty) -> + let sort = find_sort "sort" id in + let attrs = + sort @ ((None,"id",id):: + match binder with + C.Anonymous -> [] + | C.Name b -> [None,"binder",b]) + in + [< i ; X.xml_nempty "def" attrs [< aux s ; aux ty >] >] + ) [< >] letins ; + X.xml_nempty "target" [] (aux t) + >] + | C.AAppl (id,li) -> + let sort = find_sort "sort" id in + X.xml_nempty "APPLY" (sort @ [None,"id",id]) + [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) + >] + | C.AConst (id,uri,exp_named_subst) -> + let sort = find_sort "sort" id in + aux_subst uri + (X.xml_empty "CONST" + (sort @ [None,"uri",(U.string_of_uri uri) ; None,"id",id]) + ) exp_named_subst + | C.AMutInd (id,uri,i,exp_named_subst) -> + aux_subst uri + (X.xml_empty "MUTIND" + [None, "uri", (U.string_of_uri uri) ; + None, "noType", (string_of_int i) ; + None, "id", id] + ) exp_named_subst + | C.AMutConstruct (id,uri,i,j,exp_named_subst) -> + let sort = find_sort "sort" id in + aux_subst uri + (X.xml_empty "MUTCONSTRUCT" + (sort @ + [None,"uri", (U.string_of_uri uri) ; + None,"noType",(string_of_int i) ; + None,"noConstr",(string_of_int j) ; + None,"id",id]) + ) exp_named_subst + | C.AMutCase (id,uri,typeno,ty,te,patterns) -> + let sort = find_sort "sort" id in + X.xml_nempty "MUTCASE" + (sort @ + [None,"uriType",(U.string_of_uri uri) ; + None,"noType", (string_of_int typeno) ; + None,"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) -> + let sort = find_sort "sort" id in + X.xml_nempty "FIX" + (sort @ [None,"noFun", (string_of_int no) ; None,"id",id]) + [< List.fold_right + (fun (id,fi,ai,ti,bi) i -> + [< X.xml_nempty "FixFunction" + [None,"id",id ; None,"name", fi ; + None,"recIndex", (string_of_int ai)] + [< X.xml_nempty "type" [] [< aux ti >] ; + X.xml_nempty "body" [] [< aux bi >] + >] ; + i + >] + ) funs [<>] + >] + | C.ACoFix (id,no,funs) -> + let sort = find_sort "sort" id in + X.xml_nempty "COFIX" + (sort @ [None,"noFun", (string_of_int no) ; None,"id",id]) + [< List.fold_right + (fun (id,fi,ti,bi) i -> + [< X.xml_nempty "CofixFunction" [None,"id",id ; None,"name", fi] + [< X.xml_nempty "type" [] [< aux ti >] ; + X.xml_nempty "body" [] [< aux bi >] + >] ; + i + >] + ) funs [<>] + >] + and aux_subst buri target subst = +(*CSC: I have now no way to assign an ID to the explicit named substitution *) + let id = None in + if subst = [] then + target + else + Xml.xml_nempty "instantiate" + (match id with None -> [] | Some id -> [None,"id",id]) + [< target ; + List.fold_left + (fun i (uri,arg) -> + let relUri = + let buri_frags = + Str.split (Str.regexp "/") (UriManager.string_of_uri buri) in + let uri_frags = + Str.split (Str.regexp "/") (UriManager.string_of_uri uri) in + let rec find_relUri buri_frags uri_frags = + match buri_frags,uri_frags with + [_], _ -> String.concat "/" uri_frags + | he1::tl1, he2::tl2 -> + assert (he1 = he2) ; + find_relUri tl1 tl2 + | _,_ -> assert false (* uri is not relative to buri *) + in + find_relUri buri_frags uri_frags + in + [< i ; Xml.xml_nempty "arg" [None,"relUri", relUri] (aux arg) >] + ) [<>] subst + >] + in + aux +;; + +let xml_of_attrs generate_attributes attributes = + let class_of = function + | `Coercion n -> + Xml.xml_empty "class" [None,"value","coercion";None,"arity",string_of_int n] + | `Elim s -> + Xml.xml_nempty "class" [None,"value","elim"] + [< Xml.xml_empty + "SORT" [None,"value", + (Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)) ; + None,"id","elimination_sort"] >] + | `Record field_names -> + Xml.xml_nempty "class" [None,"value","record"] + (List.fold_right + (fun (name,coercion,arity) res -> + [< Xml.xml_empty "field" + [None,"name", + if coercion then + name ^ " coercion " ^ string_of_int arity + else + name]; + res >] + ) field_names [<>]) + | `Projection -> Xml.xml_empty "class" [None,"value","projection"] + | `InversionPrinciple -> Xml.xml_empty "class" [None,"value","inversion"] + in + let flavour_of = function + | `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"] + | `MutualDefinition -> + Xml.xml_empty "flavour" [None, "value", "mutual_definition"] + | `Fact -> Xml.xml_empty "flavour" [None, "value", "fact"] + | `Lemma -> Xml.xml_empty "flavour" [None, "value", "lemma"] + | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"] + | `Theorem -> Xml.xml_empty "flavour" [None, "value", "theorem"] + | `Variant -> Xml.xml_empty "flavour" [None, "value", "variant"] + | `Axiom -> Xml.xml_empty "flavour" [None, "value", "axiom"] + in + let xml_attr_of = function + | `Generated -> Xml.xml_empty "generated" [] + | `Class c -> class_of c + | `Flavour f -> flavour_of f + in + let xml_attrs = + List.fold_right + (fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>] + in + if generate_attributes then Xml.xml_nempty "attributes" [] xml_attrs else [<>] + +let print_object uri + ?ids_to_inner_sorts ?(generate_attributes=true) ~ask_dtd_to_the_getter obj = + let module C = Cic in + let module X = Xml in + let module U = UriManager in + let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in + match obj with + C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) -> + let params' = param_attribute_of_params params in + let xml_attrs = xml_of_attrs generate_attributes obj_attrs in + let xml_for_current_proof_body = +(*CSC: Should the CurrentProof also have the list of variables it depends on? *) +(*CSC: I think so. Not implemented yet. *) + X.xml_nempty "CurrentProof" + [None,"of",UriManager.string_of_uri uri ; None,"id", id] + [< xml_attrs; + List.fold_left + (fun i (cid,n,canonical_context,t) -> + [< i ; + X.xml_nempty "Conjecture" + [None,"id",cid ; None,"no",(string_of_int n)] + [< List.fold_left + (fun i (hid,t) -> + [< (match t with + Some (n,C.ADecl t) -> + X.xml_nempty "Decl" + (match n with + C.Name n' -> + [None,"id",hid;None,"name",n'] + | C.Anonymous -> [None,"id",hid]) + (print_term ?ids_to_inner_sorts t) + | Some (n,C.ADef (t,_)) -> + X.xml_nempty "Def" + (match n with + C.Name n' -> + [None,"id",hid;None,"name",n'] + | C.Anonymous -> [None,"id",hid]) + (print_term ?ids_to_inner_sorts t) + | None -> X.xml_empty "Hidden" [None,"id",hid] + ) ; + i + >] + ) [< >] canonical_context ; + X.xml_nempty "Goal" [] + (print_term ?ids_to_inner_sorts t) + >] + >]) + [< >] conjectures ; + X.xml_nempty "body" [] (print_term ?ids_to_inner_sorts bo) >] + in + let xml_for_current_proof_type = + X.xml_nempty "ConstantType" + [None,"name",n ; None,"params",params' ; None,"id", id] + (print_term ?ids_to_inner_sorts ty) + in + let xmlbo = + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n"); + xml_for_current_proof_body + >] in + let xmlty = + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n"); + xml_for_current_proof_type + >] + in + xmlty, Some xmlbo + | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) -> + let params' = param_attribute_of_params params in + let xml_attrs = xml_of_attrs generate_attributes obj_attrs in + let xmlbo = + match bo with + None -> None + | Some bo -> + Some + [< X.xml_cdata + "\n" ; + X.xml_cdata + ("\n") ; + X.xml_nempty "ConstantBody" + [None,"for",UriManager.string_of_uri uri ; + None,"params",params' ; None,"id", id] + [< print_term ?ids_to_inner_sorts bo >] + >] + in + let xmlty = + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n"); + X.xml_nempty "ConstantType" + [None,"name",n ; None,"params",params' ; None,"id", id] + [< xml_attrs; print_term ?ids_to_inner_sorts ty >] + >] + in + xmlty, xmlbo + | C.AVariable (id,n,bo,ty,params,obj_attrs) -> + let params' = param_attribute_of_params params in + let xml_attrs = xml_of_attrs generate_attributes obj_attrs in + let xmlbo = + match bo with + None -> [< >] + | Some bo -> + X.xml_nempty "body" [] [< print_term ?ids_to_inner_sorts bo >] + in + let aobj = + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n"); + X.xml_nempty "Variable" + [None,"name",n ; None,"params",params' ; None,"id", id] + [< xml_attrs; xmlbo; + X.xml_nempty "type" [] (print_term ?ids_to_inner_sorts ty) + >] + >] + in + aobj, None + | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) -> + let params' = param_attribute_of_params params in + let xml_attrs = xml_of_attrs generate_attributes obj_attrs in + [< X.xml_cdata "\n" ; + X.xml_cdata + ("\n") ; + X.xml_nempty "InductiveDefinition" + [None,"noParams",string_of_int nparams ; + None,"id",id ; + None,"params",params'] + [< xml_attrs; + (List.fold_left + (fun i (id,typename,finite,arity,cons) -> + [< i ; + X.xml_nempty "InductiveType" + [None,"id",id ; None,"name",typename ; + None,"inductive",(string_of_bool finite) + ] + [< X.xml_nempty "arity" [] + (print_term ?ids_to_inner_sorts arity) ; + (List.fold_left + (fun i (name,lc) -> + [< i ; + X.xml_nempty "Constructor" + [None,"name",name] + (print_term ?ids_to_inner_sorts lc) + >]) [<>] cons + ) + >] + >] + ) [< >] tys + ) + >] + >], None +;; + +let + print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types + ~ask_dtd_to_the_getter += + let module C2A = Cic2acic in + let module X = Xml in + let dtdname = dtdname ~ask_dtd_to_the_getter "cictypes.dtd" in + [< X.xml_cdata "\n" ; + X.xml_cdata + ("\n") ; + X.xml_nempty "InnerTypes" [None,"of",UriManager.string_of_uri curi] + (Hashtbl.fold + (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x -> + [< x ; + X.xml_nempty "TYPE" [None,"of",id] + [< X.xml_nempty "synthesized" [] + [< print_term ~ids_to_inner_sorts synty >] ; + match expty with + None -> [<>] + | Some expty' -> X.xml_nempty "expected" [] + [< print_term ~ids_to_inner_sorts expty' >] + >] + >] + ) ids_to_inner_types [<>] + ) + >] +;;