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=54e7fc5f25bd9cfdadd9f01582a25d941ccd4755;hpb=0ad07ee93a134773c16986552dc88e4e50a437ce;p=helm.git diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml index 54e7fc5f2..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 @@ -659,6 +666,45 @@ prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl (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 @@ -671,61 +717,41 @@ prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl 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 *) - if c1 = cc1 then - unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2) - else if c2 = cc2 then - Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2 - else raise exn - in - fo_unif_subst test_equality_only subst context - metasenv l1 l2 ugraph + 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 + 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 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,ugraph 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 - 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) -> @@ -742,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 @@ -945,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) )