From: Enrico Tassi Date: Fri, 5 Sep 2008 08:44:21 +0000 (+0000) Subject: unification+pullback fix. It used to saturate a coercion (generating new metas) X-Git-Tag: make_still_working~4808 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0ad07ee93a134773c16986552dc88e4e50a437ce;p=helm.git unification+pullback fix. It used to saturate a coercion (generating new metas) but not do any unification steps on them nor using them to build a new term, thus they were left in the metasenv with no chance to be closed by subsequent calls to unification. The meets function has been specialized takin in input a boolean for every direction (left/right) to state if the graph can grow in this direction and it returns saturated coercions and augmented metasenv only for the requested directions. Still unclear to me what does it mean to search a non triangular pullback with a boolean set to false.... --- diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml index 5eb75b5da..54e7fc5f2 100644 --- a/helm/software/components/cic_unification/cicUnification.ml +++ b/helm/software/components/cic_unification/cicUnification.ml @@ -302,6 +302,21 @@ 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 = + 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') (* NUOVA UNIFICAZIONE *) (* A substitution is a (int * Cic.term) list that associates a @@ -329,7 +344,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,15 +611,15 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ | 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 t = CicMetaSubst.apply_subst subst t in let rec aux c x t = @@ -655,73 +672,79 @@ let res = 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 + (* 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 | _ -> raise exn else - let meets = - CoercGraph.meets metasenv subst context car1 car2 + 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 - (match meets with + 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 meets = + CoercGraph.meets + metasenv subst context (grow1,car1) (grow2,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, + warn_if_not_unique xxx to1 to2 carr car1 car2; + 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 + conclude subst metasenv ugraph last_tl1' last_tl2') + (* }}} 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 @@ -744,7 +767,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 = diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml index 2fa2c4b0c..e54b3a847 100644 --- a/helm/software/components/cic_unification/coercGraph.ml +++ b/helm/software/components/cic_unification/coercGraph.ml @@ -259,7 +259,7 @@ let rec min acc = function | [] -> acc ;; -let meets metasenv subst context left right = +let meets metasenv subst context (grow_left,left) (grow_right,right) = let saturate metasenv uo = match uo with | None -> metasenv, None @@ -270,8 +270,10 @@ let meets metasenv subst context left right = in List.map (fun (c,uo1,uo2) -> - let metasenv, uo1 = saturate metasenv uo1 in - let metasenv, uo2 = saturate metasenv uo2 in + let metasenv, uo1 = + if grow_left then saturate metasenv uo1 else metasenv, None in + let metasenv, uo2 = + if grow_right then saturate metasenv uo2 else metasenv, None in c,metasenv, uo1, uo2) (min [] (intersect (grow left) (grow right))) ;; diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli index abc94688c..6c6ef2b50 100644 --- a/helm/software/components/cic_unification/coercGraph.mli +++ b/helm/software/components/cic_unification/coercGraph.mli @@ -54,7 +54,7 @@ val coerced_arg: Cic.term list -> (Cic.term * int) option (* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *) val meets : Cic.metasenv -> Cic.substitution -> Cic.context -> - CoercDb.coerc_carr -> CoercDb.coerc_carr -> + bool * CoercDb.coerc_carr -> bool * CoercDb.coerc_carr -> (CoercDb.coerc_carr * Cic.metasenv * (Cic.term * Cic.term) option * (Cic.term * Cic.term) option) list diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma index 0248b72a1..e179fe3f0 100644 --- a/helm/software/matita/library/formal_topology/concrete_spaces.ma +++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma @@ -76,14 +76,8 @@ qed. interpretation "fintersectsS" 'fintersects U V = (fun1 ___ (fintersectsS _) U V). -definition relS: ∀o: basic_pair. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP. - intros (o); constructor 1; - [ apply (λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y); - (* BUG HERE: WORKAROUND *) apply (concr o); - | intros; split; intros; cases H2; exists [1,3: apply w] - [ apply (. (#‡H1)‡(H‡#)); assumption - | apply (. (#‡H1 \sup -1)‡(H \sup -1‡#)); assumption]] -qed. +definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp ≝ + λo:basic_pair.λx:concr o.λS: Ω \sup (form o).∃y: form o.y ∈ S ∧ x ⊩ y. interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun1 ___ (relS _) x y). interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun1 ___ (relS _)). @@ -106,6 +100,7 @@ record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝ extS ?? (rel CS1) (form CS1) }. +(* definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid. intros; constructor 1; @@ -150,4 +145,4 @@ definition CSPA: category. | ] - |*) \ No newline at end of file + |*)