- (match is_composite1, is_composite2 with
- | false, false -> raise exn
- | true, false ->
- let body1 = CicSubstitution.subst_vars ens1 body1 in
- let appl = Cic.Appl (body1::tl1) in
- let redappl = CicReduction.head_beta_reduce appl in
- fo_unif_subst
- test_equality_only subst context metasenv
- redappl t2 ugraph
- | false, true ->
- let body2 = CicSubstitution.subst_vars ens2 body2 in
- let appl = Cic.Appl (body2::tl2) in
- let redappl = CicReduction.head_beta_reduce appl in
- fo_unif_subst
- test_equality_only subst context metasenv
- t1 redappl ugraph
- | true, true ->
- let body1 = CicSubstitution.subst_vars ens1 body1 in
- let appl1 = Cic.Appl (body1::tl1) in
- let redappl1 = CicReduction.head_beta_reduce appl1 in
- let body2 = CicSubstitution.subst_vars ens2 body2 in
- let appl2 = Cic.Appl (body2::tl2) in
- let redappl2 = CicReduction.head_beta_reduce appl2 in
- fo_unif_subst
- test_equality_only subst context metasenv
- redappl1 redappl2 ugraph)
- (*CSC: This is necessary because of the "elim H" tactic
+ if CoercDb.eq_carr car1 car2 then
+ match last_tl1,last_tl2 with
+ | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
+ | _, C.Meta _
+ | C.Meta _, _ ->
+ let subst,metasenv,ugraph =
+ fo_unif_subst test_equality_only subst context
+ metasenv last_tl1 last_tl2 ugraph
+ in
+ fo_unif_subst test_equality_only subst context
+ metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
+ | _ when CoercDb.eq_carr head1_c head2_c ->
+ let l1, l2 =
+ (* composite VS composition + metas avoiding
+ * coercions not only in coerced position *)
+ if c1 = cc1 then
+ unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
+ else if c2 = cc2 then
+ Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
+ else raise exn
+ in
+ fo_unif_subst test_equality_only subst context
+ metasenv l1 l2 ugraph
+ | _ -> raise exn
+ else
+ let conclude subst metasenv ugraph last_tl1' last_tl2' =
+ let subst',metasenv,ugraph =
+(*DEBUGGING ONLY:
+prerr_endline
+ ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
+ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
+*)
+ fo_unif_subst test_equality_only subst context
+ metasenv last_tl1' last_tl2' ugraph
+ in
+ if subst = subst' then raise exn
+ else
+(*DEBUGGING ONLY:
+let subst,metasenv,ugraph as res =
+*)
+ fo_unif_subst test_equality_only subst' context
+ metasenv (C.Appl l1) (C.Appl l2) ugraph
+(*DEBUGGING ONLY:
+in
+(prerr_endline
+ (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
+ " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
+res)
+*)
+ in
+ let grow1 =
+ match last_tl1 with Cic.Meta _ -> true | _ -> false in
+ let grow2 =
+ match last_tl2 with Cic.Meta _ -> true | _ -> false in
+ if not (grow1 || grow2) then
+ (* no flexible terminals -> no pullback, but
+ * we still unify them, in some cases it helps *)
+ conclude subst metasenv ugraph last_tl1 last_tl2
+ else
+ let meets =
+ CoercGraph.meets
+ metasenv subst context (grow1,car1) (grow2,car2)
+ in
+ (match meets with
+ | [] -> raise exn
+ | (carr,metasenv,to1,to2)::xxx ->
+ warn_if_not_unique xxx to1 to2 carr car1 car2;
+ let last_tl1',(subst,metasenv,ugraph) =
+ match grow1,to1 with
+ | true,Some (last,coerced) ->
+ last,
+ fo_unif_subst test_equality_only subst context
+ metasenv coerced last_tl1 ugraph
+ | _ -> last_tl1,(subst,metasenv,ugraph)
+ in
+ let last_tl2',(subst,metasenv,ugraph) =
+ match grow2,to2 with
+ | true,Some (last,coerced) ->
+ last,
+ fo_unif_subst test_equality_only subst context
+ metasenv coerced last_tl2 ugraph
+ | _ -> last_tl2,(subst,metasenv,ugraph)
+ in
+ conclude subst metasenv ugraph last_tl1' last_tl2')
+ (* }}} pullback *)
+ (* {{{ CSC: This is necessary because of the "elim H" tactic