let module S = CicSubstitution in
let t1 = deref subst t1 in
let t2 = deref subst t2 in
- let b,ugraph =
+ let (&&&) a b = (a && b) || ((not a) && (not b)) in
+(* let bef = Sys.time () in *)
+ let b,ugraph =
+ if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
+ false,ugraph
+ else
let foo () =
R.are_convertible ~subst ~metasenv context t1 t2 ugraph
in profiler_are_convertible.HExtlib.profile foo ()
in
+(* let aft = Sys.time () in
+if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^ CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
if b then
subst, metasenv, ugraph
else
subst context metasenv te t2 ugraph
| (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
subst context metasenv t1 te ugraph
- | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
- let subst',metasenv',ugraph1 =
- fo_unif_subst true subst context metasenv s1 s2 ugraph
- in
- fo_unif_subst test_equality_only
- subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
| (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
let subst',metasenv',ugraph1 =
fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
| UnificationFailure s
| Uncertain s as exn ->
(match l1, l2 with
- | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
- (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
- CoercDb.is_a_coercion' c1 &&
- CoercDb.is_a_coercion' c2 &&
+ | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
+ (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
+ CoercDb.is_a_coercion cc1 <> None &&
+ CoercDb.is_a_coercion cc2 <> None &&
not (UriManager.eq uri1 uri2) ->
-(*DEBUGGING ONLY:
+(*DEBUGGING ONLY:
prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
let res =
-*)
- let rec look_for_first_coercion c tl =
- match
- CicMetaSubst.apply_subst subst (HExtlib.list_last tl)
- with
- Cic.Appl ((Cic.Const (uri1,ens1) as c')::tl')
- when CoercDb.is_a_coercion' c' ->
- look_for_first_coercion c' tl'
- | last_tl -> c,last_tl
+ *)
+ let inner_coerced t =
+ let t = CicMetaSubst.apply_subst subst t in
+ let rec aux c x t =
+ match t with
+ | Cic.Appl l ->
+ (match CoercGraph.coerced_arg l with
+ | None -> c, x
+ | Some (t,_) -> aux (List.hd l) t t)
+ | _ -> c, x
+ in
+ aux (Cic.Implicit None) (Cic.Implicit None) t
in
- let c1,last_tl1 = look_for_first_coercion c1 tl1 in
- let c2,last_tl2 = look_for_first_coercion c2 tl2 in
- let car1 =
- CoercDb.coerc_carr_of_term (CoercGraph.source_of c1) in
- let car2 =
- CoercDb.coerc_carr_of_term (CoercGraph.source_of c2) in
+ let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
+ let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
+ let car1, car2 =
+ match
+ CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
+ with
+ | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
+ | _ -> assert false
+ in
+ let head1_c, head2_c =
+ match
+ CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
+ with
+ | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
+ | _ -> assert false
+ in
+ 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
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 _ ->
+ 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 (C.Appl l1) (C.Appl l2) ugraph
- | _ -> raise exn)
+ 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 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 meets =
CoercGraph.meets metasenv subst context car1 car2
in
- (match meets with
+ (match meets with
| [] -> raise exn
| (carr,metasenv,to1,to2)::xxx ->
(match xxx with
- [] -> ()
+ | [] -> ()
| (m2,_,c2,c2')::_ ->
let m1,_,c1,c1' = carr,metasenv,to1,to2 in
let unopt =
in
HLog.warn
("There are two minimal joins of "^
- CoercDb.name_of_carr car1^" and "^
- CoercDb.name_of_carr car2^": " ^
- CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^
- unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^
+ CoercDb.string_of_carr car1^" and "^
+ CoercDb.string_of_carr car2^": " ^
+ CoercDb.string_of_carr m1 ^ " via "^unopt c1^" + "^
+ unopt c1'^" and "^CoercDb.string_of_carr m2^" via "^
unopt c2^" + "^unopt c2'));
let last_tl1',(subst,metasenv,ugraph) =
match last_tl1,to1 with
prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
res
*)
+
(*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
subst context metasenv t1' t2 ugraph
| _ -> raise (UnificationFailure (lazy "8")))
*)
-(* The following idea could be exploited again; right now we have no
- longer any example requiring it
- | (C.Prod _, t2) ->
- let t2' = R.whd ~subst context t2 in
- (match t2' with
- C.Prod _ ->
- fo_unif_subst test_equality_only
- subst context metasenv t1 t2' ugraph
- | _ -> raise (UnificationFailure (lazy "8")))
- | (t1, C.Prod _) ->
- let t1' = R.whd ~subst context t1 in
- (match t1' with
- C.Prod _ ->
- fo_unif_subst test_equality_only
- subst context metasenv t1' t2 ugraph
- | _ -> (* raise (UnificationFailure "9")) *)
- raise
- (UnificationFailure (lazy (sprintf
- "Can't unify %s with %s because they are not convertible"
- (CicMetaSubst.ppterm ~metasenv subst t1)
- (CicMetaSubst.ppterm ~metasenv subst t2)))))
-*)
+ | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
+ let subst',metasenv',ugraph1 =
+ fo_unif_subst true subst context metasenv s1 s2 ugraph
+ in
+ fo_unif_subst test_equality_only
+ subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
+ | (C.Prod _, _) ->
+ (match CicReduction.whd ~subst context t2 with
+ | C.Prod _ as t2 ->
+ fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
+ | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
+ | (_, C.Prod _) ->
+ (match CicReduction.whd ~subst context t1 with
+ | C.Prod _ as t1 ->
+ fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
+ | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
| (_,_) ->
(* delta-beta reduction should almost never be a problem for
unification since:
projects / helm.git / blobdiff