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
let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
in
- let to_remove =
- uri ::
- (if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else []) @
- derived_uris_of_uri uri
- in
+ let uris_to_remove =
+ if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri]
+ in
+ let files_to_remove = uri :: derived_uris_of_uri uri in
+ List.iter
+ (fun uri ->
+ (try
+ let file = Http_getter.resolve' ~writable:true uri in
+ HExtlib.safe_remove file;
+ HExtlib.rmdir_descend (Filename.dirname file)
+ with Http_getter_types.Key_not_found _ -> ());
+ ) files_to_remove ;
List.iter
- (fun uri ->
- (try
- let file = Http_getter.resolve' ~writable:true uri in
- HExtlib.safe_remove file;
- HExtlib.rmdir_descend (Filename.dirname file)
- with Http_getter_types.Key_not_found _ -> ());
- ignore (LibraryDb.remove_uri uri);
- (*CoercGraph.remove_coercion uri;*)
- CicEnvironment.remove_obj uri)
- to_remove
+ (fun uri ->
+ ignore (LibraryDb.remove_uri uri);
+ (*CoercGraph.remove_coercion uri;*)
+ ) uris_to_remove ;
+ CicEnvironment.remove_obj uri
(*** GENERATION OF AUXILIARY LEMMAS ***)
UriManager.UriHashtbl.clear coercion_hashtbl;
CoercDb.remove_coercion (fun (_,_,u1) -> true)
-let add_coercion ~add_composites refinement_toolkit uri =
+let add_coercion ~add_composites refinement_toolkit uri arity 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 extract_last_two_p ty =
+ let spline2list ty =
let rec aux = function
- | Cic.Prod( _, _, ((Cic.Prod _) as t)) ->
- aux t
- | Cic.Prod( _, src, tgt) -> src, tgt
- | _ -> assert false
+ | Cic.Prod( _, src, tgt) -> src::aux tgt
+ | t -> [t]
in
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
+ in
+ aux n (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
+ in
let already_in =
List.exists
- (fun (_,_,ul) -> List.exists (fun u -> UriManager.eq u uri) ul)
+ (fun (s,t,ul) ->
+ List.exists
+ (fun u ->
+ UriManager.eq u uri &&
+ CoercDb.eq_carr s src_carr &&
+ CoercDb.eq_carr t tgt_carr)
+ ul)
(CoercDb.to_list ())
in
- let ty_src, ty_tgt = extract_last_two_p coer_ty in
- let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
- let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
if not add_composites then
(CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
else
let new_coercions =
CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri
+ baseuri
in
let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
if already_in then
let lemmas =
if add_composites then
List.fold_left
- (fun acc (_,_,uri,obj) ->
+ (fun acc (_,tgt,uri,obj) ->
add_single_obj uri obj refinement_toolkit;
- uri::acc)
+ let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
+ (uri,arity)::acc)
[] new_coercions
else
[]
let generate_projections refinement_toolkit uri fields =
let uris = ref [] in
- let projections = CicRecord.projections_of uri (List.map fst fields) in
+ let projections =
+ CicRecord.projections_of uri
+ (List.map (fun (x,_,_) -> x) fields)
+ in
try
List.iter2
- (fun (uri, name, bo) (_name, coercion) ->
+ (fun (uri, name, bo) (_name, coercion, arity) ->
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);*)
- let x = add_coercion ~add_composites:true refinement_toolkit 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)
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 fst x
end
else
[]
projects / helm.git / blobdiff