(* $Id: cicCoercion.ml 7077 2006-12-05 15:44:54Z fguidi $ *)
-let debug = false
+let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
(* given the new coercion uri from src to tgt returns the list
coercions
in
(HExtlib.flatten_map
- (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
+ (fun (_,t,ul) ->
+ if CoercDb.eq_carr ~exact:true src t then [] else
+ List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
(HExtlib.flatten_map
- (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
+ (fun (s,_,ul) ->
+ if CoercDb.eq_carr ~exact:true s tgt then [] else
+ List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
(HExtlib.flatten_map
(fun (s,_,u1l) ->
HExtlib.flatten_map
(fun (_,t,u2l) ->
HExtlib.flatten_map
(fun u1 ->
+ if CoercDb.eq_carr ~exact:true s t then [] else
List.map
(fun u2 -> (s,[u1;uri;u2],t))
u2l)
let spline_len = saturations_for_c1 + saturations_for_c2 in
let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in
debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c));
+ let old_insert_coercions = !CicRefine.insert_coercions in
let c, metasenv, univ =
try
+ CicRefine.insert_coercions := false;
let term, ty, metasenv, ugraph =
CicRefine.type_of_aux' metasenv context c univ
in
in
debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
+ CicRefine.insert_coercions := old_insert_coercions;
term, metasenv, ugraph
with
| CicRefine.RefineFailure s
| CicRefine.Uncertain s -> debug_print s;
+ CicRefine.insert_coercions := old_insert_coercions;
raise UnableToCompose
+ | exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
+ raise exn
in
c, metasenv, univ
;;