X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcic2Xml.ml;h=056240ef13899e24b08a8adf1b9aac306f94eb64;hb=23641e7c4b061a2dbc5862d763e8c3602793a94c;hp=5d614db055d92d8cd570f7f93c1b79bb6766296d;hpb=6a6d9950d0c3a7974bc0f0d8a85369b733138647;p=helm.git diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml index 5d614db05..056240ef1 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.ml +++ b/helm/ocaml/cic_transformations/cic2Xml.ml @@ -25,7 +25,6 @@ (*CSC codice cut & paste da cicPp e xmlcommand *) -exception ImpossiblePossible;; exception NotImplemented;; let dtdname ~ask_dtd_to_the_getter dtd = @@ -41,24 +40,27 @@ 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" [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" [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 + 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 @@ -70,12 +72,8 @@ 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" (* TASSI *) - | C.CProp -> "CProp" + 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 @@ -88,13 +86,11 @@ 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 + 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 = (None,"id",id)::(None,"type",sort):: match binder with @@ -106,7 +102,7 @@ let print_term ~ids_to_inner_sorts = X.xml_nempty "target" [] (aux t) >] | C.ACast (id,v,t) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + 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) @@ -120,13 +116,11 @@ 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 + 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 = (None,"id",id)::(None,"type",sort):: match binder with @@ -148,11 +142,11 @@ 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 + 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 = (None,"id",id)::(None,"sort",sort):: match binder with @@ -164,12 +158,12 @@ let print_term ~ids_to_inner_sorts = X.xml_nempty "target" [] (aux t) >] | C.AAppl (id,li) -> - let sort = Hashtbl.find ids_to_inner_sorts id in + 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" [None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort] @@ -182,7 +176,7 @@ let print_term ~ids_to_inner_sorts = 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" [None,"uri", (U.string_of_uri uri) ; @@ -191,7 +185,7 @@ let print_term ~ids_to_inner_sorts = 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" [None,"uriType",(U.string_of_uri uri) ; None,"noType", (string_of_int typeno) ; @@ -203,7 +197,7 @@ 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" [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort] [< List.fold_right @@ -219,7 +213,7 @@ 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" [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort] [< List.fold_right @@ -265,10 +259,37 @@ let print_term ~ids_to_inner_sorts = aux ;; - (* TODO ZACK implement attributes pretty printing *) -let xml_of_attrs attributes = [< >] +let xml_of_attrs attributes = + let class_of = function + | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"] + | `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 res -> + [< Xml.xml_empty "field" [None,"name",name]; res >] + ) field_names [<>]) + | `Projection -> Xml.xml_empty "class" [None,"value","projection"] + in + let xml_attr_of = function + | `Generated -> Xml.xml_empty "generated" [] + | `Class c -> class_of c + in + let xml_attrs = + List.fold_right + (fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>] + in + Xml.xml_nempty "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 @@ -436,7 +457,8 @@ let [< 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 [<>]