X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcic2Xml.ml;h=3ca6a3a5040990370f722c0e8c30755b1a1eba3d;hb=cd602bc57c4ceba6188b4cac0dbf5dad8f5df7b6;hp=ea7d1958df50af969c4530683ff1e26ec71554aa;hpb=ebfab836e9e047756b7a53c3f46f69ec4532685a;p=helm.git diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml index ea7d1958d..3ca6a3a50 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" - | 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,20 +259,61 @@ let print_term ~ids_to_inner_sorts = aux ;; +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 flavour_of = function + | `Definition -> Xml.xml_empty "flavour" [None, "value", "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"] + 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 + 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 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" [None,"of",UriManager.string_of_uri uri ; None,"id", id] - [< List.fold_left + [< xml_attrs; + List.fold_left (fun i (cid,n,canonical_context,t) -> [< i ; X.xml_nempty "Conjecture" @@ -309,7 +344,7 @@ 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 = @@ -329,8 +364,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 @@ -351,12 +387,13 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_cdata ("\n"); X.xml_nempty "ConstantType" [None,"name",n ; None,"params",params' ; None,"id", id] - [< print_term ids_to_inner_sorts ty >] + [< 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 -> [< >] @@ -368,14 +405,15 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_cdata ("\n"); X.xml_nempty "Variable" [None,"name",n ; None,"params",params' ; None,"id", id] - [< xmlbo ; + [< 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") ; @@ -383,7 +421,8 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = [None,"noParams",string_of_int nparams ; None,"id",id ; None,"params",params'] - [< (List.fold_left + [< xml_attrs; + (List.fold_left (fun i (id,typename,finite,arity,cons) -> [< i ; X.xml_nempty "InductiveType" @@ -427,7 +466,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 [<>]