-let avoid_double_coercion context subst metasenv ugraph t ty =
- 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 tail = function
- | 0 -> [tail]
- | n -> Cic.Implicit None :: mk_implicits tail (n-1)
- in
- let b, c1, c2, head = is_a_double_coercion t in
- if b then
- let source_carr = CoercGraph.source_of c2 in
- let tgt_carr = CicMetaSubst.apply_subst subst ty in
- (match CoercGraph.look_for_coercion source_carr tgt_carr
- with
- | CoercGraph.SomeCoercion c ->
- let arity = arity_of c in
- let args = mk_implicits head (arity - 1) in
- let c_bo = CicUtil.term_of_uri (CicUtil.uri_of_term c) in
- let newt = Cic.Appl (c_bo::args) in
- let subst, metasenv, ugraph =
- CicUnification.fo_unif_subst subst context metasenv newt t ugraph
- in
- debug_print
- (lazy
- ("packing: " ^
- CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args))));
- Cic.Appl (c::args), ty, subst, metasenv, ugraph
- | _ -> assert false) (* the composite coercion must exist *)
- else
- t, ty, subst, metasenv, ugraph
-