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=517c013d42b2ac4ffcb6fe7973725561d0fa01da;hpb=20c47f607c279c480743954fc0ba305fcb3ed645;p=helm.git diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml index 517c013d4..fca316fa3 100644 --- a/helm/software/components/cic_unification/cicUnification.ml +++ b/helm/software/components/cic_unification/cicUnification.ml @@ -302,6 +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 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 @@ -329,7 +348,9 @@ let foo () = 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 @@ -594,96 +615,173 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ | UnificationFailure s | Uncertain s as exn -> (match l1, l2 with - | (((Cic.Const (uri1, ens1)) as c1) :: tl1), - (((Cic.Const (uri2, ens2)) as c2) :: tl2) when - CoercDb.is_a_coercion' c1 && - CoercDb.is_a_coercion' c2 && + (* {{{ 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: 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 rec look_for_first_coercion c tl = - match - CicMetaSubst.apply_subst subst (HExtlib.list_last tl) - with - Cic.Appl ((Cic.Const (uri1,ens1) as c')::tl') - when CoercDb.is_a_coercion' c' -> - look_for_first_coercion c' tl' - | last_tl -> c,last_tl + 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 + in + aux (Cic.Implicit None) (Cic.Implicit None) t in - let c1,last_tl1 = look_for_first_coercion c1 tl1 in - let c2,last_tl2 = look_for_first_coercion c2 tl2 in - let car1 = - CoercDb.coerc_carr_of_term (CoercGraph.source_of c1) in - let car2 = - CoercDb.coerc_carr_of_term (CoercGraph.source_of c2) in + let c1,last_tl1 = inner_coerced (Cic.Appl l1) in + let c2,last_tl2 = inner_coerced (Cic.Appl l2) in + let car1, car2 = + match + CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2 + with + | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2 + | _ -> assert false + in + let head1_c, head2_c = + match + CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2 + with + | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2 + | _ -> assert false + in + let unfold uri ens args = + let o, _ = + CicEnvironment.get_obj CicUniv.oblivion_ugraph uri + in + assert (ens = []); + match o with + | Cic.Constant (_,Some bo,_,_,_) -> + CicReduction.head_beta_reduce ~delta:false + (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 - | C.Meta _, _ - | _, C.Meta _ -> + match last_tl1,last_tl2 with + | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn + | _, C.Meta _ + | C.Meta _, _ -> let subst,metasenv,ugraph = fo_unif_subst test_equality_only subst context metasenv last_tl1 last_tl2 ugraph in fo_unif_subst test_equality_only subst context - metasenv (C.Appl l1) (C.Appl l2) ugraph - | _ -> raise exn) + metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph + | _ when CoercDb.eq_carr head1_c head2_c -> + (* 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 + 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 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.name_of_carr car1^" and "^ - CoercDb.name_of_carr car2^": " ^ - CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^ - unopt c1'^" and " ^ CoercDb.name_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 - (*DEBUGGING ONLY: -prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context); -*) - let subst,metasenv,ugraph = - 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 - 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 @@ -706,7 +804,9 @@ res 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 = @@ -882,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) )