-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2000-2004, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
* MA 02111-1307, USA.
*
* For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
+ * http://helm.cs.unibo.it/
*)
(*CSC codice cut & paste da cicPp e xmlcommand *)
-exception ImpossiblePossible;;
exception NotImplemented;;
let dtdname ~ask_dtd_to_the_getter dtd =
if ask_dtd_to_the_getter then
- Configuration.getter_url ^ "getdtd?uri=" ^ dtd
+ Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd
else
"http://mowgli.cs.unibo.it/dtd/" ^ 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"
+ 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
;;
+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 xml_attr_of = function
+ | `Generated -> Xml.xml_empty "generated" []
+ | `Class c -> class_of c
+ 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"
(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 =
>]
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
X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\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 -> [< >]
X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata
("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
[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"
[< 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 [<>]
projects / helm.git / blobdiff