(* $Id$ *)
+let object_declaration_hook = ref (fun _ _ -> ());;
+let set_object_declaration_hook f =
+ object_declaration_hook := f
+
exception AlreadyDefined of UriManager.uri
let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
HExtlib.mkdir dir
in
(* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
- let annobj, innertypes =
+ let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
if Helm_registry.get_bool "matita.system" then
- let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
+ let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
Cic2acic.acic_object_of_cic_object obj
in
let innertypesxml =
Cic2Xml.print_inner_types
uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false
in
- annobj, Some innertypesxml
+ annobj, Some innertypesxml, Some ids_to_inner_sorts, false
else
let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
- annobj, None
+ annobj, None, None, true
in
(* prepare XML *)
let xml, bodyxml =
Cic2Xml.print_object
- uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj
+ uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false
+ ~generate_attributes annobj
in
let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
xmlunivgraphpath, univgraphuri =
try
(*3*)
let new_stuff = save_object_to_disk uri obj ugraph univlist in
+ (* EXPERIMENTAL: pretty print the object in natural language *)
+ (try !object_declaration_hook uri obj
+ with exc ->
+ prerr_endline "Error: object_declaration_hook failed");
try
HLog.message
(Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
baseuri
in
let new_coercions =
- List.filter (fun (s,t,u,saturations,obj) -> not(already_in_obj s t u obj))
+ List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj))
new_coercions
in
- let composite_uris = List.map (fun (_,_,uri,_,_) -> uri) new_coercions in
+ let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in
(* update the DB *)
List.iter
- (fun (src,tgt,uri,saturations,_) ->
+ (fun (src,tgt,uri,saturations,_,_) ->
CoercDb.add_coercion (src,tgt,uri,saturations))
new_coercions;
CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
let lemmas =
if add_composites then
List.fold_left
- (fun acc (_,tgt,uri,saturations,obj) ->
+ (fun acc (_,tgt,uri,saturations,obj,arity) ->
add_single_obj uri obj refinement_toolkit;
- let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
(uri,arity,saturations)::acc)
[] new_coercions
else