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 5eb75b5da73b3aa9db52ab99178410904854072c..54e7fc5f25bd9cfdadd9f01582a25d941ccd4755 100644 (file)
--- 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 2fa2c4b0c5ca4ba216534de62d26cbebb9e02bcd..e54b3a847dde2d9489cf142baaa09f7b8b79cb11 100644 (file)
--- 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 abc94688c5a6b27897ca1c63b2fc8a1946e45efd..6c6ef2b50f2089230f39eabd50db0bccbaee0736 100644 (file)
--- 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 0248b72a100729cf6f224b13c80b0044dd0939d2..e179fe3f0695f3a6c541e177b82972fa16fc449b 100644 (file)
--- 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
+  |*)