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 =
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 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
+ let x =
+ add_coercion ~add_composites:true refinement_toolkit uri arity
in
(*prerr_endline ("are: ");
List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;