(* to apply the coercion it is sufficient to unify the last coercion
argument (that is a Meta) with the term to be coerced *)
| SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
+ | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
| NoCoercion
| NotMetaClosed
| NotHandled of string Lazy.t
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
let saturate_coercion ul metasenv subst context =
- let cl = List.map CicUtil.term_of_uri ul in
+ let cl =
+ List.map (fun u,saturations -> CicUtil.term_of_uri u,saturations) ul in
let funclass_arityl =
- let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
+ let _,tgtcarl = List.split (List.map (fun u,_ -> CoercDb.get_carr u) ul) in
List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
in
let freshmeta = CicMkImplicit.new_meta metasenv subst in
List.map2
- (fun arity c ->
+ (fun arity (c,saturations) ->
let ty,_ =
CicTypeChecker.type_of_aux' ~subst metasenv context c
CicUniv.empty_ugraph in
let _,metasenv,args,lastmeta =
- TermUtil.saturate_term freshmeta metasenv context ty arity in
+ TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context
in
- metasenv, Cic.Meta (lastmeta-1,irl),
+ metasenv, Cic.Meta (lastmeta - saturations - 1,irl),
match args with
[] -> c
| _ -> Cic.Appl (c::args)
(* searches a coercion fron src to tgt in the !coercions list *)
let look_for_coercion' metasenv subst context src tgt =
+ let pp_l s l =
+ match l with
+ | [] ->
+ debug_print
+ (lazy
+ (sprintf ":-( coercion non trovata[%s] da %s a %s" s
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)));
+ | _::_ ->
+ debug_print (lazy (
+ sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s
+ (List.length l)
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)));
+ in
try
let l =
CoercDb.find_coercion
- (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
- | _::_ ->
- debug_print (lazy (
- sprintf ":-) TROVATE %d coercion(s) da %s a %s"
- (List.length l)
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)));
- Some l
+ (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt)
in
- (match uri with
- None -> NoCoercion
- | Some ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
+ pp_l "precise" l;
+ (match l with
+ | [] ->
+ let l =
+ CoercDb.find_coercion
+ (fun (_,t) -> CoercDb.eq_carr t tgt)
+ in
+ pp_l "approx" l;
+ (match l with
+ | [] -> NoCoercion
+ | ul -> SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
+ | ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
with
| CoercDb.EqCarrNotImplemented s -> NotHandled s
| CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
Pp.node (CoercDb.name_of_carr carr)
~attrs:["href", UriManager.string_of_uri uri] fmt in
List.iter
- (fun (src, tgt, cl) ->
+ (fun (src, tgt, ul) ->
let src_name = CoercDb.name_of_carr src in
let tgt_name = CoercDb.name_of_carr tgt in
pp_description src;
pp_description tgt;
List.iter
- (fun c ->
+ (fun (u,saturations) ->
Pp.edge src_name tgt_name
- ~attrs:[ "label", UriManager.name_of_uri c;
- "href", UriManager.string_of_uri c ]
+ ~attrs:[ "label",
+ (UriManager.name_of_uri u ^
+ if saturations = 0 then
+ ""
+ else
+ "(" ^ string_of_int saturations ^ ")");
+ "href", UriManager.string_of_uri u ]
fmt)
- cl)
+ ul)
l;
Pp.trailer fmt;
Buffer.contents buf
(************************* meet calculation stuff ********************)
let eq_uri_opt u1 u2 =
match u1,u2 with
- | Some u1, Some u2 -> UriManager.eq u1 u2
+ | Some (u1,_), Some (u2,_) -> UriManager.eq u1 u2
| None,Some _ | Some _, None -> false
| None, None -> true
;;