X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcic2Xml.ml;h=5bd9fd1c9878acafebb44c093c154b1d06773c77;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=3be3ba7f115ea5cc7b8cd72e624f6a30c7cdbf07;hpb=ff981d975589f8d21a364e7cfe875647f7483cd9;p=helm.git diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml index 3be3ba7f1..5bd9fd1c9 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 = @@ -40,9 +39,12 @@ 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) +let print_term ?ids_to_inner_sorts = + let find_sort name id = + match ids_to_inner_sorts with + None -> [] + | Some ids_to_inner_sorts -> + [None,name,Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)] in let rec aux = let module C = Cic in @@ -50,20 +52,21 @@ let print_term ~ids_to_inner_sorts = let module U = UriManager in function C.ARel (id,idref,n,b) -> - let sort = find_sort id in + let sort = find_sort "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] + (sort @ + [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ; + None,"idref",idref]) | C.AVar (id,uri,exp_named_subst) -> - let sort = find_sort id in + let sort = find_sort "sort" id in aux_subst uri (X.xml_empty "VAR" - [None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort]) + (sort @ [None,"uri",U.string_of_uri uri;None,"id",id])) exp_named_subst | C.AMeta (id,n,l) -> - let sort = find_sort id in + let sort = find_sort "sort" id in X.xml_nempty "META" - [None,"no",(string_of_int n) ; None,"id",id ; None,"sort",sort] + (sort @ [None,"no",(string_of_int n) ; None,"id",id]) (List.fold_left (fun i t -> match t with @@ -87,24 +90,24 @@ let print_term ~ids_to_inner_sorts = | t -> [],t in let prods,t = eat_prods prods in - let sort = find_sort last_id in - X.xml_nempty "PROD" [None,"type",sort] + let sort = find_sort "type" last_id in + X.xml_nempty "PROD" sort [< List.fold_left (fun i (id,binder,s) -> - let sort = find_sort (Cic2acic.source_id_of_id id) in + let sort = find_sort "type" (Cic2acic.source_id_of_id id) in let attrs = - (None,"id",id)::(None,"type",sort):: - match binder with - C.Anonymous -> [] - | C.Name b -> [None,"binder",b] + sort @ ((None,"id",id):: + match binder with + C.Anonymous -> [] + | 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 = find_sort id in - X.xml_nempty "CAST" [None,"id",id ; None,"sort",sort] + let sort = find_sort "sort" id in + X.xml_nempty "CAST" (sort @ [None,"id",id]) [< X.xml_nempty "term" [] (aux v) ; X.xml_nempty "type" [] (aux t) >] @@ -117,16 +120,16 @@ let print_term ~ids_to_inner_sorts = | t -> [],t in let lambdas,t = eat_lambdas lambdas in - let sort = find_sort last_id in - X.xml_nempty "LAMBDA" [None,"sort",sort] + let sort = find_sort "sort" last_id in + X.xml_nempty "LAMBDA" sort [< List.fold_left (fun i (id,binder,s) -> - let sort = find_sort (Cic2acic.source_id_of_id id) in + let sort = find_sort "type" (Cic2acic.source_id_of_id id) in let attrs = - (None,"id",id)::(None,"type",sort):: - match binder with - C.Anonymous -> [] - | C.Name b -> [None,"binder",b] + sort @ ((None,"id",id):: + match binder with + C.Anonymous -> [] + | C.Name b -> [None,"binder",b]) in [< i ; X.xml_nempty "decl" attrs (aux s) >] ) [< >] lambdas ; @@ -143,31 +146,31 @@ let print_term ~ids_to_inner_sorts = | t -> [],t in let letins,t = eat_letins letins in - let sort = find_sort last_id in - X.xml_nempty "LETIN" [None,"sort",sort] + let sort = find_sort "sort" last_id in + X.xml_nempty "LETIN" sort [< List.fold_left (fun i (id,binder,s) -> - let sort = find_sort id in + let sort = find_sort "sort" id in let attrs = - (None,"id",id)::(None,"sort",sort):: - match binder with - C.Anonymous -> [] - | C.Name b -> [None,"binder",b] + sort @ ((None,"id",id):: + match binder with + C.Anonymous -> [] + | 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 = find_sort id in - X.xml_nempty "APPLY" [None,"id",id ; None,"sort",sort] + let sort = find_sort "sort" id in + X.xml_nempty "APPLY" (sort @ [None,"id",id]) [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]) >] | C.AConst (id,uri,exp_named_subst) -> - let sort = find_sort id in + let sort = find_sort "sort" id in aux_subst uri (X.xml_empty "CONST" - [None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort] + (sort @ [None,"uri",(U.string_of_uri uri) ; None,"id",id]) ) exp_named_subst | C.AMutInd (id,uri,i,exp_named_subst) -> aux_subst uri @@ -177,20 +180,22 @@ let print_term ~ids_to_inner_sorts = None, "id", id] ) exp_named_subst | C.AMutConstruct (id,uri,i,j,exp_named_subst) -> - let sort = find_sort id in + let sort = find_sort "sort" id in aux_subst uri (X.xml_empty "MUTCONSTRUCT" - [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] + (sort @ + [None,"uri", (U.string_of_uri uri) ; + None,"noType",(string_of_int i) ; + None,"noConstr",(string_of_int j) ; + None,"id",id]) ) exp_named_subst | C.AMutCase (id,uri,typeno,ty,te,patterns) -> - let sort = find_sort id in + let sort = find_sort "sort" id in X.xml_nempty "MUTCASE" - [None,"uriType",(U.string_of_uri uri) ; - None,"noType", (string_of_int typeno) ; - None,"id", id ; None,"sort",sort] + (sort @ + [None,"uriType",(U.string_of_uri uri) ; + None,"noType", (string_of_int typeno) ; + None,"id", id]) [< X.xml_nempty "patternsType" [] [< (aux ty) >] ; X.xml_nempty "inductiveTerm" [] [< (aux te) >] ; List.fold_right @@ -198,9 +203,9 @@ let print_term ~ids_to_inner_sorts = patterns [<>] >] | C.AFix (id, no, funs) -> - let sort = find_sort id in + let sort = find_sort "sort" id in X.xml_nempty "FIX" - [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort] + (sort @ [None,"noFun", (string_of_int no) ; None,"id",id]) [< List.fold_right (fun (id,fi,ai,ti,bi) i -> [< X.xml_nempty "FixFunction" @@ -214,9 +219,9 @@ let print_term ~ids_to_inner_sorts = ) funs [<>] >] | C.ACoFix (id,no,funs) -> - let sort = find_sort id in + let sort = find_sort "sort" id in X.xml_nempty "COFIX" - [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort] + (sort @ [None,"noFun", (string_of_int no) ; None,"id",id]) [< List.fold_right (fun (id,fi,ti,bi) i -> [< X.xml_nempty "CofixFunction" [None,"id",id ; None,"name", fi] @@ -260,13 +265,43 @@ 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 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 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 @@ -295,30 +330,30 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = C.Name n' -> [None,"id",hid;None,"name",n'] | C.Anonymous -> [None,"id",hid]) - (print_term ids_to_inner_sorts t) + (print_term ?ids_to_inner_sorts t) | Some (n,C.ADef t) -> X.xml_nempty "Def" (match n with C.Name n' -> [None,"id",hid;None,"name",n'] | C.Anonymous -> [None,"id",hid]) - (print_term ids_to_inner_sorts t) + (print_term ?ids_to_inner_sorts t) | None -> X.xml_empty "Hidden" [None,"id",hid] ) ; i >] ) [< >] canonical_context ; X.xml_nempty "Goal" [] - (print_term ids_to_inner_sorts t) + (print_term ?ids_to_inner_sorts t) >] >]) [< >] conjectures ; - X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >] + X.xml_nempty "body" [] (print_term ?ids_to_inner_sorts bo) >] in let xml_for_current_proof_type = X.xml_nempty "ConstantType" [None,"name",n ; None,"params",params' ; None,"id", id] - (print_term ids_to_inner_sorts ty) + (print_term ?ids_to_inner_sorts ty) in let xmlbo = [< X.xml_cdata "\n" ; @@ -347,7 +382,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_nempty "ConstantBody" [None,"for",UriManager.string_of_uri uri ; None,"params",params' ; None,"id", id] - [< print_term ids_to_inner_sorts bo >] + [< print_term ?ids_to_inner_sorts bo >] >] in let xmlty = @@ -355,7 +390,7 @@ 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] - [< xml_attrs; print_term ids_to_inner_sorts ty >] + [< xml_attrs; print_term ?ids_to_inner_sorts ty >] >] in xmlty, xmlbo @@ -366,7 +401,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = match bo with None -> [< >] | Some bo -> - X.xml_nempty "body" [] [< print_term ids_to_inner_sorts bo >] + X.xml_nempty "body" [] [< print_term ?ids_to_inner_sorts bo >] in let aobj = [< X.xml_cdata "\n" ; @@ -374,7 +409,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_nempty "Variable" [None,"name",n ; None,"params",params' ; None,"id", id] [< xml_attrs; xmlbo; - X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty) + X.xml_nempty "type" [] (print_term ?ids_to_inner_sorts ty) >] >] in @@ -398,13 +433,13 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = None,"inductive",(string_of_bool finite) ] [< X.xml_nempty "arity" [] - (print_term ids_to_inner_sorts arity) ; + (print_term ?ids_to_inner_sorts arity) ; (List.fold_left (fun i (name,lc) -> [< i ; X.xml_nempty "Constructor" [None,"name",name] - (print_term ids_to_inner_sorts lc) + (print_term ?ids_to_inner_sorts lc) >]) [<>] cons ) >] @@ -431,11 +466,11 @@ let [< x ; X.xml_nempty "TYPE" [None,"of",id] [< X.xml_nempty "synthesized" [] - [< print_term ids_to_inner_sorts synty >] ; + [< print_term ~ids_to_inner_sorts synty >] ; match expty with None -> [<>] | Some expty' -> X.xml_nempty "expected" [] - [< print_term ids_to_inner_sorts expty' >] + [< print_term ~ids_to_inner_sorts expty' >] >] >] ) ids_to_inner_types [<>]