in
subst,metasenv,hd,ugraph
-and warn_if_not_unique xxx to1 to2 carr car1 car2 =
+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
| [] -> ()
- | (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')
+ ("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
(*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 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
let subst',metasenv,ugraph =
(*DEBUGGING ONLY:
prerr_endline
- ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
+ ("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
in
if subst = subst' then raise exn
else
-(*DEBUGGING ONLY:
+(*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:
+(*DEBUGGING ONLY:
in
(prerr_endline
- (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
+ ("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
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
- (* 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 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
+ 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;
+ (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) ->
metasenv coerced last_tl2 ugraph
| _ -> last_tl2,(subst,metasenv,ugraph)
in
- conclude subst metasenv ugraph last_tl1' last_tl2')
+ 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
| 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