;;
(*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
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
| 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)
>]
| 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 ;
| 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
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
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"
) 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]
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
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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
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 =
X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\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
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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
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
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
)
>]
[< 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 [<>]
projects / helm.git / blobdiff