X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_transformations%2Fcic2Xml.ml;h=759f630b4b8abaa0100bac5ff1695ad789ec2e98;hb=423f3f23abfe6d5906818c26ab92d3703714057d;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..759f630b4 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 ;; @@ -41,24 +41,29 @@ let param_attribute_of_params params = (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *) let print_term ~ids_to_inner_sorts = + let find_sort id = + 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 = Hashtbl.find ids_to_inner_sorts id in + let sort = find_sort 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 + let sort = find_sort 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] + let sort = find_sort id in + 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 @@ -68,13 +73,10 @@ let print_term ~ids_to_inner_sorts = [< i ; X.xml_empty "substitution" [] >] ) [< >] l) | C.ASort (id,s) -> - let string_of_sort = - function - C.Prop -> "Prop" - | C.Set -> "Set" - | C.Type -> "Type" + let string_of_sort s = + Cic2acic.string_of_sort (Cic2acic.sort_of_sort s) 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 = @@ -85,26 +87,24 @@ let print_term ~ids_to_inner_sorts = | t -> [],t 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] + let sort = find_sort last_id in + 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 sort = find_sort (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 ; X.xml_nempty "target" [] (aux t) >] | C.ACast (id,v,t) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "CAST" ["id",id ; "sort",sort] + let sort = find_sort id in + X.xml_nempty "CAST" [None,"id",id ; None,"sort",sort] [< X.xml_nempty "term" [] (aux v) ; X.xml_nempty "type" [] (aux t) >] @@ -117,18 +117,16 @@ let print_term ~ids_to_inner_sorts = | t -> [],t 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] + let sort = find_sort last_id in + 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 sort = find_sort (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 ; @@ -145,53 +143,54 @@ let print_term ~ids_to_inner_sorts = | t -> [],t 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] + let sort = find_sort last_id in + 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 sort = find_sort 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 ; X.xml_nempty "target" [] (aux t) >] | C.AAppl (id,li) -> - let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "APPLY" ["id",id ; "sort",sort] + let sort = find_sort id in + 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 + let sort = find_sort 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 + let sort = find_sort 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 + let sort = find_sort 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 @@ -199,13 +198,14 @@ let print_term ~ids_to_inner_sorts = patterns [<>] >] | C.AFix (id, no, funs) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + let sort = find_sort 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 >] >] ; @@ -214,12 +214,12 @@ let print_term ~ids_to_inner_sorts = ) funs [<>] >] | C.ACoFix (id,no,funs) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + let sort = find_sort 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 +234,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 +253,71 @@ 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 ;; +let xml_of_attrs attributes = + let class_of = function + | `Coercion -> "coercion" + | `Elim Cic.Prop -> "elimProp" + | `Elim Cic.CProp -> "elimCProp" + | `Elim Cic.Set -> "elimSet" + | `Elim (Cic.Type _) -> "elimType" + | `Record -> "record" + | `Projection -> "projection" + in + let xml_attr_of = function + | `Generated -> None, "generated", "true" + | `Class c -> None, "class", class_of c + in + let xml_attrs = List.map xml_attr_of attributes in + Xml.xml_empty "attributes" xml_attrs + let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = + let find_sort id = + Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id) + in 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 +326,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 +346,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 +359,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 +368,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 +386,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 +417,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,16 +439,17 @@ 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 None -> [<>] - | Some expty' -> X.xml_nempty "expected" [] [< print_term ids_to_inner_sorts expty' >] + | Some expty' -> X.xml_nempty "expected" [] + [< print_term ids_to_inner_sorts expty' >] >] >] ) ids_to_inner_types [<>]