in
subst,metasenv,hd,ugraph
+and warn_if_not_unique xxx to1 to2 carr car1 car2 =
+ match xxx with
+ | [] -> ()
+ | (m2,_,c2,c2')::_ ->
+ let m1,c1,c1' = carr,to1,to2 in
+ let unopt =
+ function Some (_,t) -> CicPp.ppterm t
+ | None -> "id"
+ in
+ HLog.warn
+ ("There are two minimal joins of "^ 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')
(* NUOVA UNIFICAZIONE *)
(* A substitution is a (int * Cic.term) list that associates a
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 (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
| UnificationFailure s
| Uncertain s as exn ->
(match l1, l2 with
+ (* {{{ pullback *)
| (((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 inner_coerced t =
+*)
+ let inner_coerced ?(skip_non_c=false) 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 when skip_non_c ->
+ aux c (HExtlib.list_last l)
+ (HExtlib.list_last l)
| None -> c, x
| Some (t,_) -> aux (List.hd l) t t)
| _ -> c, x
(Cic.Appl (bo::args))
| _ -> assert false
in
+ 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,ugrph 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
if CoercDb.eq_carr car1 car2 then
match last_tl1,last_tl2 with
| C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
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 *)
+ (* 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 if c2 = cc2 then
+ else
Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
- else raise exn
- in
- fo_unif_subst test_equality_only subst context
- metasenv l1 l2 ugraph
+ 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
+ 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 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 =
- function Some (_,t) -> CicPp.ppterm t
- | None -> "id"
- in
- HLog.warn
- ("There are two minimal joins of "^
- 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
- | Cic.Meta (i1,l1),Some (last,coerced) ->
- last,
+ 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 last_tl2,to2 with
- | Cic.Meta (i2,l2),Some (last,coerced) ->
- last,
+ 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
- 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
+ metasenv coerced last_tl2 ugraph
+ | _ -> last_tl2,(subst,metasenv,ugraph)
in
- if subst = subst' then raise exn else
- fo_unif_subst test_equality_only subst' context
- metasenv (C.Appl l1) (C.Appl l2) ugraph)
-(*DEBUGGING ONLY:
-in
-let subst,metasenv,ugraph = res in
-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
+ conclude subst metasenv ugraph last_tl1' last_tl2')
+ (* }}} 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
subst context metasenv t1 t2' ugraph
| _ -> raise
(UnificationFailure
- (lazy ("not a mutind :"^CicMetaSubst.ppterm ~metasenv subst t2 ))))
+ (lazy ("not a mutind :"^
+ CicMetaSubst.ppterm ~metasenv subst t2 ))))
+ (* }}} elim H *)
| _ -> raise exn)))
| (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
let subst', metasenv',ugraph1 =
projects / helm.git / blobdiff