(* $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 =
- if Helm_registry.get_bool "matita.system" then
- let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
+ let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
+ if Helm_registry.get_bool "matita.system" &&
+ not (Helm_registry.get_bool "matita.noinnertypes")
+ then
+ 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))
in
let src_carr, tgt_carr =
let get_classes arity saturations l =
- let rec aux target = function
- 0,0,tgt::src::_ when target = None -> src,Some (`Class tgt)
- | 0,0,src::_ when target <> None -> src,target
- | 0,saturations,tgt::tl when target = None ->
- aux (Some (`Class tgt)) (0,saturations,tl)
- | 0,saturations,_::tl ->
- aux target (0,saturations - 1,tl)
- | arity,saturations,_::tl ->
- aux (Some `Funclass) (arity - 1, saturations, tl)
- | _,_,_ -> assert false
+ (* this is the ackerman's function revisited *)
+ let rec aux = function
+ 0,0,None,tgt::src::_ -> src,Some (`Class tgt)
+ | 0,0,target,src::_ -> src,target
+ | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl)
+ | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl)
+ | arity,saturations,None,_::tl ->
+ aux (arity, saturations, Some `Funclass, tl)
+ | arity,saturations,target,_::tl ->
+ aux (arity - 1, saturations, target, tl)
+ | _ -> assert false
in
- aux None (arity,saturations,List.rev l)
+ aux (arity,saturations,None,List.rev l)
in
let types = spine2list coer_ty in
let src,tgt = get_classes arity saturations types in
(CoercDb.to_list ())
in
if not add_composites then
- (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[])
+ (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+ UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]);
+ [])
else
let new_coercions =
CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
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);
(* add the composites obj and they eventual lemmas *)
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
- []
in
(* store that composite_uris are related to uri. the first component is
* the stuff in the DB while the second is stuff for remove_obj *)
List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
composite_uris;
*)
- UriManager.UriHashtbl.add coercion_hashtbl uri
- (composite_uris,if add_composites then composite_uris else []);
+ UriManager.UriHashtbl.add
+ coercion_hashtbl uri (composite_uris,composite_uris);
(*
prerr_endline ("lemmas:");
List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
composites_in_db;*)
UriManager.UriHashtbl.remove coercion_hashtbl uri;
- CoercDb.remove_coercion (fun (_,_,u,_) -> UriManager.eq uri u);
+ CoercDb.remove_coercion
+ (fun (_,_,u,_) -> UriManager.eq uri u);
(* remove from the DB *)
List.iter
(fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
(* remove composites from the lib *)
List.iter remove_single_obj composites_in_lib
with
- Not_found -> () (* mhh..... *)
+ Not_found -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *)
let generate_projections refinement_toolkit uri fields =
projects / helm.git / blobdiff