(* $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
innertypesuri,bodyuri,univgraphuri
let paths_and_uris_of_obj uri =
- let resolved = Http_getter.filename' ~writable:true uri in
+ let resolved = Http_getter.filename' ~local:true ~writable:true uri in
let basepath = Filename.dirname resolved in
let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in
HExtlib.mkdir dir
in
(* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
- let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
+ 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, Some ids_to_inner_sorts, false
+ else
+ let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
+ 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
- in
+ uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false
+ ~generate_attributes annobj
+ in
let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
xmlunivgraphpath, univgraphuri =
paths_and_uris_of_obj uri
(* we return a list of uri,path we registered/created *)
(uri,xmlpath) ::
(univgraphuri,xmlunivgraphpath) ::
+ (* now the optional inner types, both write and register *)
+ (match innertypes with
+ | None -> []
+ | Some innertypesxml ->
+ write ensure_path_exists innertypespath;
+ write (Xml.pp ~gzip:true innertypesxml) (Some innertypespath);
+ [innertypesuri, innertypespath]
+ ) @
(* now the optional body, both write and register *)
(match bodyxml,bodyuri with
None,_ -> []
let module RT = RefinementTool in
let obj =
if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
- not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
+ not (CoercDb.is_a_coercion' (Cic.Const (uri, [])))
then
refinement_toolkit.RT.pack_coercion_obj obj
else
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))
raise exc
with exc ->
CicEnvironment.remove_obj uri; (* -1 *)
- raise exc
+ raise exc
end
let remove_single_obj uri =
List.iter
(fun uri ->
(try
- let file = Http_getter.resolve' ~writable:true uri in
+ let file = Http_getter.resolve' ~local:true ~writable:true uri in
HExtlib.safe_remove file;
HExtlib.rmdir_descend (Filename.dirname file)
with Http_getter_types.Key_not_found _ -> ());
let remove_all_coercions () =
UriManager.UriHashtbl.clear coercion_hashtbl;
- CoercDb.remove_coercion (fun (_,_,u1) -> true)
+ CoercDb.remove_coercion (fun (_,_,_,_) -> true)
-let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
+let add_coercion ~add_composites refinement_toolkit uri arity saturations
+ baseuri
+=
let coer_ty,_ =
let coer = CicUtil.term_of_uri uri in
CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph
* should we saturate it with metas in case we insert it?
*
*)
- let spline2list ty =
+ let spine2list ty =
let rec aux = function
| Cic.Prod( _, src, tgt) -> src::aux tgt
| t -> [t]
aux ty
in
let src_carr, tgt_carr =
- let list_remove_from_tail n l =
- let rec aux n = function
- | hd::tl when n > 0 -> aux (n-1) tl
- | l when n = 0 -> l
- | _ -> assert false
+ let get_classes arity saturations l =
+ (* 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 n (List.rev l)
+ aux (arity,saturations,None,List.rev l)
in
- let types = spline2list coer_ty in
- match arity, list_remove_from_tail arity types with
- | 0,tgt::src::_ ->
- (* if ~delta is true, it is impossible to define an identity coercion *)
- CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
- CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
- | n,_::src::_ ->
- CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
- CoercDb.Fun arity
- | _ -> assert false
+ let types = spine2list coer_ty in
+ let src,tgt = get_classes arity saturations types in
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+ match tgt with
+ None -> assert false
+ | Some `Funclass -> CoercDb.Fun arity
+ | Some (`Class tgt) ->
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
in
- let already_in =
+ let already_in_obj src_carr tgt_carr uri obj =
List.exists
(fun (s,t,ul) ->
List.exists
- (fun u ->
- UriManager.eq u uri &&
+ (fun u,_ ->
+ let bo =
+ match obj with
+ | Cic.Constant (_, Some bo, _, _, _) -> bo
+ | _ -> assert false
+ in
CoercDb.eq_carr s src_carr &&
- CoercDb.eq_carr t tgt_carr)
+ CoercDb.eq_carr t tgt_carr &&
+ if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
+ CicUniv.oblivion_ugraph)
+ then true else
+ (HLog.warn
+ ("Coercions " ^
+ UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri
+ uri^" are not convertible, but are between the same nodes.\n"^
+ "From now on unification can fail randomly.");
+ false))
ul)
(CoercDb.to_list ())
in
if not add_composites then
- (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
+ (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[])
else
let new_coercions =
- CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri
+ CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
baseuri
in
- let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
- if already_in then
- (* this if starts here just to be sure the closure function works fine *)
- begin
- assert (new_coercions = []);
- HLog.warn
- (UriManager.string_of_uri uri ^
- " is already declared as a coercion! skipping...");
- []
- end
- else
- begin
- (* update the DB *)
- List.iter
- (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri))
- new_coercions;
- CoercDb.add_coercion (src_carr, tgt_carr, uri);
- (* add the composites obj and they eventual lemmas *)
- let lemmas =
- if add_composites then
- List.fold_left
- (fun acc (_,_,uri,obj) ->
- add_single_obj uri obj refinement_toolkit;
- uri::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 *)
- (*
- prerr_endline ("adding: " ^
- string_of_bool add_composites ^ UriManager.string_of_uri uri);
- 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 []);
- (*
- prerr_endline ("lemmas:");
- List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
- lemmas;
- prerr_endline ("lemmas END");*)
- lemmas
- end
+ let new_coercions =
+ 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
+ (* update the DB *)
+ List.iter
+ (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,arity) ->
+ add_single_obj uri obj refinement_toolkit;
+ (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 *)
+ (*
+ prerr_endline ("adding: " ^
+ string_of_bool add_composites ^ UriManager.string_of_uri uri);
+ 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 []);
+ (*
+ prerr_endline ("lemmas:");
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+ lemmas;
+ prerr_endline ("lemmas END");*)
+ lemmas
;;
let remove_coercion uri =
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))
+ (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
composites_in_db;
(* remove composites from the lib *)
List.iter remove_single_obj composites_in_lib
try
List.iter2
(fun (uri, name, bo) (_name, coercion, arity) ->
+ let saturations = 0 in
try
let ty, ugraph =
CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
if coercion then
begin
(*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
+ (*CSC: I think there is a bug here. The composite coercions
+ are not remembered in the .moo file. Thus they are re-generated
+ every time. Right? *)
let x =
add_coercion ~add_composites:true refinement_toolkit uri arity
- (UriManager.buri_of_uri uri)
+ saturations (UriManager.buri_of_uri uri)
in
(*prerr_endline ("are: ");
List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
prerr_endline "---";
*)
- x
+ (*CSC: I throw the arity away. See comment above *)
+ List.map (fun u,_,_ -> u) x
end
else
[]
add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri)
(!build_inversion_principle uri obj)
+let
+ generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid
+=
+ function
+ Cic.Fix (_,funs) ->
+ snd (
+ List.fold_right
+ (fun (name,idx,ty,bo) (n,uris) ->
+ if name = name_to_avoid then
+ (n+1,uris)
+ else
+ let uri =
+ UriManager.uri_of_string
+ (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+ let bo = Cic.Fix (n,funs) in
+ let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+ add_single_obj uri obj refinement_toolkit;
+ (n+1,uri::uris)
+ ) funs (1,[]))
+ | Cic.CoFix (_,funs) ->
+ snd (
+ List.fold_right
+ (fun (name,ty,bo) (n,uris) ->
+ if name = name_to_avoid then
+ (n+1,uris)
+ else
+ let uri =
+ UriManager.uri_of_string
+ (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+ let bo = Cic.CoFix (n,funs) in
+ let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+ add_single_obj uri obj refinement_toolkit;
+ (n+1,uri::uris)
+ ) funs (1,[]))
+ | _ -> assert false
+
let add_obj refinement_toolkit uri obj =
add_single_obj uri obj refinement_toolkit;
let uris = ref [] in
+ let not_debug = not (Helm_registry.get_bool "matita.debug") in
try
begin
match obj with
+ | Cic.Constant (name,Some bo,_,_,attrs) when
+ List.mem (`Flavour `MutualDefinition) attrs ->
+ uris :=
+ !uris @
+ generate_sibling_mutual_definitions refinement_toolkit uri attrs
+ name bo
| Cic.Constant _ -> ()
| Cic.InductiveDefinition (_,_,_,attrs) ->
uris := !uris @
end;
UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
!uris
- with exn ->
- List.iter remove_single_obj !uris;
- raise exn
+ with
+ | exn when not_debug ->
+ List.iter remove_single_obj !uris;
+ raise exn
let remove_obj uri =
let uris =
projects / helm.git / blobdiff