-(* 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 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 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 "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 = Hashtbl.find ids_to_inner_sorts 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 = Hashtbl.find ids_to_inner_sorts 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
[< i ; X.xml_empty "substitution" [] >]
) [< >] l)
| C.ASort (id,s) ->
- let string_of_sort =
- function
- C.Prop -> "Prop"
- | C.Set -> "Set"
- | C.Type -> "Type"
- | 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
- 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 =
- Hashtbl.find ids_to_inner_sorts (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 = Hashtbl.find ids_to_inner_sorts 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 = Hashtbl.find ids_to_inner_sorts 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 =
- Hashtbl.find ids_to_inner_sorts (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 = Hashtbl.find ids_to_inner_sorts 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 = Hashtbl.find ids_to_inner_sorts 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 = Hashtbl.find ids_to_inner_sorts 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 = Hashtbl.find ids_to_inner_sorts 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 = Hashtbl.find ids_to_inner_sorts 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 = Hashtbl.find ids_to_inner_sorts 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 = Hashtbl.find ids_to_inner_sorts 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 = Hashtbl.find ids_to_inner_sorts 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]
aux
;;
-let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
+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 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"
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) >]
+ [< >] conjectures ;
+ 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" ;
>]
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_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]
- [< 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 -> [< >]
| 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_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
X.xml_nempty "Variable"
[None,"name",n ; None,"params",params' ; None,"id", id]
- [< xmlbo ;
- X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
+ [< 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"
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' >]
+ | Some expty' -> X.xml_nempty "expected" []
+ [< print_term ~ids_to_inner_sorts expty' >]
>]
>]
) ids_to_inner_types [<>]
projects / helm.git / blobdiff