X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcic2Xml.ml;h=5d614db055d92d8cd570f7f93c1b79bb6766296d;hb=0aaed6f96b856d1181a3cd1f2ef3ea4a91990771;hp=564493cb83e9d9d2ae42908e3970b21fbb5107be;hpb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;p=helm.git diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml index 564493cb8..5d614db05 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.ml +++ b/helm/ocaml/cic_transformations/cic2Xml.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000, HELM Team. +(* Copyright (C) 2000-2004, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -20,7 +20,7 @@ * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. + * http://helm.cs.unibo.it/ *) (*CSC codice cut & paste da cicPp e xmlcommand *) @@ -30,7 +30,7 @@ exception NotImplemented;; let dtdname ~ask_dtd_to_the_getter dtd = if ask_dtd_to_the_getter then - Configuration.getter_url ^ "getdtd?uri=" ^ dtd + Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd else "http://mowgli.cs.unibo.it/dtd/" ^ dtd ;; @@ -49,16 +49,18 @@ let print_term ~ids_to_inner_sorts = C.ARel (id,idref,n,b) -> let sort = Hashtbl.find ids_to_inner_sorts id in X.xml_empty "REL" - ["value",(string_of_int n) ; "binder",b ; "id",id ; "idref",idref ; - "sort",sort] + [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ; + None,"idref",idref ; None,"sort",sort] | C.AVar (id,uri,exp_named_subst) -> let sort = Hashtbl.find ids_to_inner_sorts id in aux_subst uri - (X.xml_empty "VAR" ["uri",U.string_of_uri uri;"id",id;"sort",sort]) + (X.xml_empty "VAR" + [None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort]) exp_named_subst | C.AMeta (id,n,l) -> let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort] + X.xml_nempty "META" + [None,"no",(string_of_int n) ; None,"id",id ; None,"sort",sort] (List.fold_left (fun i t -> match t with @@ -70,11 +72,12 @@ let print_term ~ids_to_inner_sorts = | C.ASort (id,s) -> let string_of_sort = function - C.Prop -> "Prop" - | C.Set -> "Set" - | C.Type -> "Type" + C.Prop -> "Prop" + | C.Set -> "Set" + | C.Type _ -> "Type" (* TASSI *) + | C.CProp -> "CProp" in - X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id] + 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 = @@ -86,17 +89,17 @@ let print_term ~ids_to_inner_sorts = in let prods,t = eat_prods prods in let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "PROD" ["type",sort] + X.xml_nempty "PROD" [None,"type",sort] [< List.fold_left (fun i (id,binder,s) -> let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in let attrs = - ("id",id)::("type",sort):: + (None,"id",id)::(None,"type",sort):: match binder with C.Anonymous -> [] - | C.Name b -> ["binder",b] + | C.Name b -> [None,"binder",b] in [< i ; X.xml_nempty "decl" attrs (aux s) >] ) [< >] prods ; @@ -104,7 +107,7 @@ let print_term ~ids_to_inner_sorts = >] | C.ACast (id,v,t) -> let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "CAST" ["id",id ; "sort",sort] + X.xml_nempty "CAST" [None,"id",id ; None,"sort",sort] [< X.xml_nempty "term" [] (aux v) ; X.xml_nempty "type" [] (aux t) >] @@ -118,17 +121,17 @@ let print_term ~ids_to_inner_sorts = in let lambdas,t = eat_lambdas lambdas in let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "LAMBDA" ["sort",sort] + X.xml_nempty "LAMBDA" [None,"sort",sort] [< List.fold_left (fun i (id,binder,s) -> let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in let attrs = - ("id",id)::("type",sort):: + (None,"id",id)::(None,"type",sort):: match binder with C.Anonymous -> [] - | C.Name b -> ["binder",b] + | C.Name b -> [None,"binder",b] in [< i ; X.xml_nempty "decl" attrs (aux s) >] ) [< >] lambdas ; @@ -146,15 +149,15 @@ let print_term ~ids_to_inner_sorts = in let letins,t = eat_letins letins in let sort = Hashtbl.find ids_to_inner_sorts last_id in - X.xml_nempty "LETIN" ["sort",sort] + X.xml_nempty "LETIN" [None,"sort",sort] [< List.fold_left (fun i (id,binder,s) -> let sort = Hashtbl.find ids_to_inner_sorts id in let attrs = - ("id",id)::("sort",sort):: + (None,"id",id)::(None,"sort",sort):: match binder with C.Anonymous -> [] - | C.Name b -> ["binder",b] + | C.Name b -> [None,"binder",b] in [< i ; X.xml_nempty "def" attrs (aux s) >] ) [< >] letins ; @@ -162,36 +165,37 @@ let print_term ~ids_to_inner_sorts = >] | C.AAppl (id,li) -> let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "APPLY" ["id",id ; "sort",sort] + X.xml_nempty "APPLY" [None,"id",id ; None,"sort",sort] [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) >] | C.AConst (id,uri,exp_named_subst) -> let sort = Hashtbl.find ids_to_inner_sorts id in aux_subst uri (X.xml_empty "CONST" - ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort] + [None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort] ) exp_named_subst | C.AMutInd (id,uri,i,exp_named_subst) -> aux_subst uri (X.xml_empty "MUTIND" - ["uri", (U.string_of_uri uri) ; - "noType",(string_of_int i) ; - "id",id] + [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 = Hashtbl.find ids_to_inner_sorts id in aux_subst uri (X.xml_empty "MUTCONSTRUCT" - ["uri", (U.string_of_uri uri) ; - "noType",(string_of_int i) ; "noConstr",(string_of_int j) ; - "id",id ; "sort",sort] + [None,"uri", (U.string_of_uri uri) ; + None,"noType",(string_of_int i) ; + None,"noConstr",(string_of_int j) ; + None,"id",id ; None,"sort",sort] ) exp_named_subst | C.AMutCase (id,uri,typeno,ty,te,patterns) -> let sort = Hashtbl.find ids_to_inner_sorts id in X.xml_nempty "MUTCASE" - ["uriType",(U.string_of_uri uri) ; - "noType", (string_of_int typeno) ; - "id", id ; "sort",sort] + [None,"uriType",(U.string_of_uri uri) ; + None,"noType", (string_of_int typeno) ; + None,"id", id ; None,"sort",sort] [< X.xml_nempty "patternsType" [] [< (aux ty) >] ; X.xml_nempty "inductiveTerm" [] [< (aux te) >] ; List.fold_right @@ -201,11 +205,12 @@ let print_term ~ids_to_inner_sorts = | C.AFix (id, no, funs) -> let sort = Hashtbl.find ids_to_inner_sorts id in X.xml_nempty "FIX" - ["noFun", (string_of_int no) ; "id",id ; "sort",sort] + [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort] [< List.fold_right (fun (id,fi,ai,ti,bi) i -> [< X.xml_nempty "FixFunction" - ["id",id ; "name", fi ; "recIndex", (string_of_int ai)] + [None,"id",id ; None,"name", fi ; + None,"recIndex", (string_of_int ai)] [< X.xml_nempty "type" [] [< aux ti >] ; X.xml_nempty "body" [] [< aux bi >] >] ; @@ -216,10 +221,10 @@ let print_term ~ids_to_inner_sorts = | C.ACoFix (id,no,funs) -> let sort = Hashtbl.find ids_to_inner_sorts id in X.xml_nempty "COFIX" - ["noFun", (string_of_int no) ; "id",id ; "sort",sort] + [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort] [< List.fold_right (fun (id,fi,ti,bi) i -> - [< X.xml_nempty "CofixFunction" ["id",id ; "name", fi] + [< X.xml_nempty "CofixFunction" [None,"id",id ; None,"name", fi] [< X.xml_nempty "type" [] [< aux ti >] ; X.xml_nempty "body" [] [< aux bi >] >] ; @@ -234,7 +239,7 @@ let print_term ~ids_to_inner_sorts = target else Xml.xml_nempty "instantiate" - (match id with None -> [] | Some id -> ["id",id]) + (match id with None -> [] | Some id -> [None,"id",id]) [< target ; List.fold_left (fun i (uri,arg) -> @@ -253,47 +258,54 @@ let print_term ~ids_to_inner_sorts = in find_relUri buri_frags uri_frags in - [< i ; Xml.xml_nempty "arg" ["relUri", relUri] (aux arg) >] + [< i ; Xml.xml_nempty "arg" [None,"relUri", relUri] (aux arg) >] ) [<>] subst >] in aux ;; + (* TODO ZACK implement attributes pretty printing *) +let xml_of_attrs attributes = [< >] + let print_object uri ~ids_to_inner_sorts ~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) -> + 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 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" - ["of",UriManager.string_of_uri uri ; "id", id] - [< List.fold_left + [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" - ["id", cid ; "no",(string_of_int n)] + [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' -> ["id",hid;"name",n'] - | C.Anonymous -> ["id",hid]) + 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' -> ["id",hid;"name",n'] - | C.Anonymous -> ["id",hid]) + 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" ["id",hid] + | None -> X.xml_empty "Hidden" [None,"id",hid] ) ; i >] @@ -302,11 +314,12 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = (print_term ids_to_inner_sorts t) >] >]) - [<>] conjectures ; + [< >] conjectures ; X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >] in let xml_for_current_proof_type = - X.xml_nempty "ConstantType" ["name",n ; "params",params' ; "id", id] + X.xml_nempty "ConstantType" + [None,"name",n ; None,"params",params' ; None,"id", id] (print_term ids_to_inner_sorts ty) in let xmlbo = @@ -321,8 +334,9 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = >] in xmlty, Some xmlbo - | C.AConstant (id,idbody,n,bo,ty,params) -> + | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) -> let params' = param_attribute_of_params params in + let xml_attrs = xml_of_attrs obj_attrs in let xmlbo = match bo with None -> None @@ -333,8 +347,8 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_cdata ("\n") ; X.xml_nempty "ConstantBody" - ["for",UriManager.string_of_uri uri ; "params",params' ; - "id", id] + [None,"for",UriManager.string_of_uri uri ; + None,"params",params' ; None,"id", id] [< print_term ids_to_inner_sorts bo >] >] in @@ -342,13 +356,14 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = [< X.xml_cdata "\n" ; X.xml_cdata ("\n"); X.xml_nempty "ConstantType" - ["name",n ; "params",params' ; "id", id] - [< print_term ids_to_inner_sorts ty >] + [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) -> + | C.AVariable (id,n,bo,ty,params,obj_attrs) -> let params' = param_attribute_of_params params in + let xml_attrs = xml_of_attrs obj_attrs in let xmlbo = match bo with None -> [< >] @@ -359,28 +374,30 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = [< X.xml_cdata "\n" ; X.xml_cdata ("\n"); X.xml_nempty "Variable" - ["name",n ; "params",params' ; "id", id] - [< xmlbo ; + [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) -> + | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) -> let params' = param_attribute_of_params params in + let xml_attrs = xml_of_attrs obj_attrs in [< X.xml_cdata "\n" ; X.xml_cdata ("\n") ; X.xml_nempty "InductiveDefinition" - ["noParams",string_of_int nparams ; - "id",id ; - "params",params'] - [< (List.fold_left + [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" - ["id",id ; "name",typename ; - "inductive",(string_of_bool finite) + [None,"id",id ; None,"name",typename ; + None,"inductive",(string_of_bool finite) ] [< X.xml_nempty "arity" [] (print_term ids_to_inner_sorts arity) ; @@ -388,7 +405,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = (fun i (name,lc) -> [< i ; X.xml_nempty "Constructor" - ["name",name] + [None,"name",name] (print_term ids_to_inner_sorts lc) >]) [<>] cons ) @@ -410,11 +427,11 @@ let [< X.xml_cdata "\n" ; X.xml_cdata ("\n") ; - X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi] + 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" ["of",id] + X.xml_nempty "TYPE" [None,"of",id] [< X.xml_nempty "synthesized" [] [< print_term ids_to_inner_sorts synty >] ; match expty with