in
subst,metasenv,hd,ugraph
+and warn_if_not_unique xxx car1 car2 =
+ let unopt =
+ function
+ | Some (_,Cic.Appl(Cic.Const(u,_)::_)) -> UriManager.string_of_uri u
+ | Some (_,t) -> CicPp.ppterm t
+ | None -> "id"
+ in
+ match xxx with
+ | [] -> ()
+ | _ ->
+ HLog.warn
+ ("There are "^string_of_int (List.length xxx + 1)^
+ " minimal joins of "^ CoercDb.string_of_carr car1^" and "^
+ CoercDb.string_of_carr car2^": " ^
+ String.concat " and "
+ (List.map
+ (fun (m2,_,c2,c2') ->
+ " via "^CoercDb.string_of_carr m2^" via "^unopt c2^" + "^unopt c2')
+ xxx))
(* 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
+ ("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
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
- | [] -> 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,
+ 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 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
+ 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
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 =
| Uncertain s
| AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
(CicMetaSubst.ppcontext ~metasenv subst context)
- (CicMetaSubst.ppmetasenv subst metasenv)
+ ("OMITTED" (*CicMetaSubst.ppmetasenv subst metasenv*))
(Lazy.force msg)
)
projects / helm.git / blobdiff