X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicUnification.ml;h=fca316fa3a6a238eae3c1c4d52206ec0d7226da4;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=5fe0f35a5b549e74414e16d2c26abce830c50523;hpb=1b9751de891efa2761cdc6cb9d019df6aaaa8514;p=helm.git diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml index 5fe0f35a5..fca316fa3 100644 --- a/helm/software/components/cic_unification/cicUnification.ml +++ b/helm/software/components/cic_unification/cicUnification.ml @@ -302,21 +302,25 @@ and beta_expand_many test_equality_only metasenv subst context t args ugraph = 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 @@ -620,12 +624,15 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (*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 @@ -663,7 +670,7 @@ prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl 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 @@ -671,19 +678,33 @@ prerr_endline 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 @@ -712,23 +733,25 @@ res) 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) -> @@ -745,7 +768,18 @@ res) 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 @@ -948,7 +982,7 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph = | Uncertain s | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) (CicMetaSubst.ppcontext ~metasenv subst context) - (CicMetaSubst.ppmetasenv subst metasenv) + ("OMITTED" (*CicMetaSubst.ppmetasenv subst metasenv*)) (Lazy.force msg) )