(* searches a coercion fron src to tgt in the !coercions list *)
let look_for_coercion src tgt =
+ let arity_of con =
+ try
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
+ let rec count_pi = function
+ | Cic.Prod (_,_,t) -> 1 + count_pi t
+ | _ -> 0
+ in
+ count_pi ty
+ with Invalid_argument _ -> assert false (* all coercions have an uri *)
+ in
+ let rec mk_implicits = function
+ | 0 -> []
+ | n -> Cic.Implicit None :: mk_implicits (n-1)
+ in
try
let l =
CoercDb.find_coercion
- (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt)
+ (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in
+ let uri =
+ match l with
+ | [] ->
+ debug_print
+ (lazy
+ (sprintf ":-( coercion non trovata da %s a %s"
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)));
+ None
+ | [u] ->
+ debug_print (lazy (
+ sprintf ":-) TROVATA 1 coercion da %s a %s: %s"
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)
+ (UriManager.name_of_uri u)));
+ Some u
+ | u::_ ->
+ debug_print (lazy (
+ sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s"
+ (List.length l)
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)
+ (UriManager.name_of_uri u)));
+ Some u
in
- match l with
- | [] ->
- debug_print
- (lazy
- (sprintf ":-( coercion non trovata da %s a %s"
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)));
- NoCoercion
- | [u] ->
- debug_print (lazy (
- sprintf ":-) TROVATA 1 coercion da %s a %s: %s"
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)
- (UriManager.name_of_uri u)));
- SomeCoercion (CicUtil.term_of_uri u)
- | u::_ ->
- debug_print (lazy (
- sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s"
- (List.length l)
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)
- (UriManager.name_of_uri u)));
- SomeCoercion (CicUtil.term_of_uri u)
+ (match uri with
+ None -> NoCoercion
+ | Some u ->
+ let c = CicUtil.term_of_uri u in
+ let arity = arity_of c in
+ let args = mk_implicits (arity - 1) in
+ let newt =
+ match args with
+ [] -> c
+ | _ -> Cic.Appl (c::args)
+ in
+ SomeCoercion newt)
with
| CoercDb.EqCarrNotImplemented s -> NotHandled s
| CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed