(*CSC codice cut & paste da cicPp e xmlcommand *)
-exception ImpossiblePossible;;
exception NotImplemented;;
let dtdname ~ask_dtd_to_the_getter dtd =
(*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
[< 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
| 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
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)
| 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
| 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
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]
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) ;
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) ;
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
) 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
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 module C = Cic in
let module X = Xml in
let module U = UriManager in
[< 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 [<>]