(*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
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
[< 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 [<>]