+ enrich localization_tbl t
+ (RefineFailure
+ (lazy
+ (sprintf
+ "%s is supposed to be a type, but its type is %s"
+ (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
+ (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
+
+ and avoid_double_coercion context subst metasenv ugraph t ty =
+ if not !pack_coercions then
+ t,ty,subst,metasenv,ugraph
+ else
+ let b, c1, c2, head, c1_c2_implicit = 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 metasenv subst context source_carr tgt_carr
+ with
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (function (metasenv,last,c) ->
+ match c with
+ | c when not (CoercGraph.is_composite c) ->
+ debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
+ None
+ | c ->
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv last head ugraph in
+ debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
+ (try
+ debug_print
+ (lazy
+ ("packing: " ^
+ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
+ let newt,_,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context c ugraph in
+ debug_print (lazy "tipa...");
+ let subst, metasenv, ugraph =
+ (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
+ fo_unif_subst subst context metasenv newt t ugraph
+ in
+ debug_print (lazy "unifica...");
+ Some (newt, ty, subst, metasenv, ugraph)
+ with
+ | RefineFailure s | Uncertain s when not !pack_coercions->
+ debug_print s; debug_print (lazy "stop\n");None
+ | RefineFailure s | Uncertain s ->
+ debug_print s;debug_print (lazy "goon\n");
+ try
+ let old_pack_coercions = !pack_coercions in
+ pack_coercions := false; (* to avoid diverging *)
+ let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context c1_c2_implicit ugraph
+ in
+ pack_coercions := old_pack_coercions;
+ let b, _, _, _, _ =
+ is_a_double_coercion refined_c1_c2_implicit
+ in
+ if b then
+ None
+ else
+ let head' =
+ match refined_c1_c2_implicit with
+ | Cic.Appl l -> HExtlib.list_last l
+ | _ -> assert false
+ in
+ let subst, metasenv, ugraph =
+ try fo_unif_subst subst context metasenv
+ head head' ugraph
+ with RefineFailure s| Uncertain s->
+ debug_print s;assert false
+ in
+ let subst, metasenv, ugraph =
+ fo_unif_subst subst context metasenv
+ refined_c1_c2_implicit t ugraph
+ in
+ Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
+ with
+ | RefineFailure s | Uncertain s ->
+ pack_coercions := true;debug_print s;None
+ | exn -> pack_coercions := true; raise exn))
+ candidates
+ in
+ (match selected with
+ | Some x -> x
+ | None ->
+ debug_print
+ (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
+ t, ty, subst, metasenv, ugraph)
+ | _ -> t, ty, subst, metasenv, ugraph)
+ else
+ t, ty, subst, metasenv, ugraph
+
+ and typeof_list subst metasenv context ugraph l =
+ let tlbody_and_type,subst,metasenv,ugraph =
+ List.fold_right
+ (fun x (res,subst,metasenv,ugraph) ->
+ let x',ty,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context x ugraph
+ in
+ (x', ty)::res,subst',metasenv',ugraph1
+ ) l ([],subst,metasenv,ugraph)
+ in
+ tlbody_and_type,subst,metasenv,ugraph