- let is_composite1 =
- List.exists ((=) (`Class `Coercion)) attrs1 in
- let is_composite2 =
- List.exists ((=) (`Class `Coercion)) attrs2 in
- (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)
+ let unfold uri ens args =
+ let o, _ =
+ CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
+ in
+ assert (ens = []);
+ match o with
+ | Cic.Constant (_,Some bo,_,_,_) ->
+ CicReduction.head_beta_reduce ~delta:false
+ (Cic.Appl (bo::args))
+ | _ -> assert false
+ in
+ let conclude subst metasenv ugraph last_tl1' last_tl2' =
+ let subst',metasenv,ugraph =
+(*DEBUGGING ONLY:
+prerr_endline
+ ("conclude: " ^ 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,ugrph as res =
+*)
+ fo_unif_subst test_equality_only subst' context
+ metasenv (C.Appl l1) (C.Appl l2) ugraph
+(*DEBUGGING ONLY:
+in
+(prerr_endline
+ ("OK: "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
+ " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
+res)
+*)
+ in
+(*DEBUGGING ONLY:
+prerr_endline (Printf.sprintf
+"Pullback problem\nterm1: %s\nterm2: %s\ncar1: %s\ncar2: %s\nlast_tl1: %s
+last_tl2: %s\nhead1_c: %s\nhead2_c: %s\n"
+(CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context)
+(CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context)
+(CoercDb.string_of_carr car1)
+(CoercDb.string_of_carr car2)
+(CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1 context)
+(CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2 context)
+(CoercDb.string_of_carr head1_c)
+(CoercDb.string_of_carr head2_c)
+);
+*)
+ 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 ->
+ (* composite VS composition + metas avoiding
+ * coercions not only in coerced position *)
+ if c1 <> cc1 && c2 <> cc2 then
+ conclude subst metasenv ugraph
+ last_tl1 last_tl2
+ else
+ let l1, l2 =
+ if c1 = cc1 then
+ unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
+ else
+ Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
+ in
+ fo_unif_subst test_equality_only subst context
+ metasenv l1 l2 ugraph
+ | _ -> raise exn
+ else
+ 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
+ let _,last_tl1 =
+ inner_coerced ~skip_non_c:true (Cic.Appl l1) in
+ let _,last_tl2 =
+ inner_coerced ~skip_non_c:true (Cic.Appl l2) in
+ conclude subst metasenv ugraph last_tl1 last_tl2
+ else
+ let meets =
+ CoercGraph.meets
+ metasenv subst context (grow1,car1) (grow2,car2)
+ in
+ (match
+ HExtlib.list_findopt
+ (fun (carr,metasenv,to1,to2) meet_no ->
+ try
+ 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
+ if meet_no > 0 then
+ HLog.warn ("Using pullback number " ^ string_of_int
+ meet_no);
+ Some
+ (conclude subst metasenv ugraph last_tl1' last_tl2')
+ with
+ | UnificationFailure _
+ | Uncertain _ -> None)
+ meets
+ with
+ | Some x -> x
+ | None -> raise exn)
+ (* }}} pullback *)
+ (* {{{ CSC: This is necessary because of the "elim H" tactic
+ where the type of H is only reducible to an
+ inductive type. This could be extended from inductive
+ types to any rigid term. However, the code is
+ duplicated in two places: inside applications and
+ outside them. Probably it would be better to
+ work with lambda-bar terms instead. *)
+ | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
+ | (_, Cic.MutInd _::_) ->
+ let t1' = R.whd ~subst context t1 in
+ (match t1' with
+ C.Appl (C.MutInd _::_) ->
+ fo_unif_subst test_equality_only
+ subst context metasenv t1' t2 ugraph
+ | _ -> raise (UnificationFailure (lazy "88")))
+ | (Cic.MutInd _::_,_) ->
+ let t2' = R.whd ~subst context t2 in
+ (match t2' with
+ C.Appl (C.MutInd _::_) ->
+ fo_unif_subst test_equality_only
+ subst context metasenv t1 t2' ugraph
+ | _ -> raise
+ (UnificationFailure
+ (lazy ("not a mutind :"^
+ CicMetaSubst.ppterm ~metasenv subst t2 ))))
+ (* }}} elim H *)