X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcic2Xml.ml;h=3be3ba7f115ea5cc7b8cd72e624f6a30c7cdbf07;hb=50377dde5b5b1a8e5c7b2fb48b47defde9508b50;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..3be3ba7f1 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.ml +++ b/helm/ocaml/cic_transformations/cic2Xml.ml @@ -41,24 +41,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 +73,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 +87,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 +103,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 +117,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 +143,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 +159,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 +177,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 +186,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 +198,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 +214,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 @@ -269,6 +264,9 @@ let print_term ~ids_to_inner_sorts = let xml_of_attrs attributes = [< >] 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 +434,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 [<>]