]> matita.cs.unibo.it Git - helm.git/commitdiff
Added check for duplicate (convertible) composite coercions,
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 5 Jan 2007 11:36:41 +0000 (11:36 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 5 Jan 2007 11:36:41 +0000 (11:36 +0000)
that are not added anymore.
Nicer api for meets used by unification.

helm/software/components/cic_unification/cicUnification.ml
helm/software/components/cic_unification/coercGraph.ml
helm/software/components/cic_unification/coercGraph.mli
helm/software/components/library/librarySync.ml

index a7a3a16741e50889b1a60a823eb41cd6d6f7452f..912ae1e8e0cbbee2d4deba85595418032c9ce04b 100644 (file)
@@ -628,51 +628,44 @@ let res =
                              metasenv (C.Appl l1) (C.Appl l2) ugraph
                          | _ -> raise exn)
                       else
-                       let meets = CoercGraph.meets car1 car2 in
+                       let meets = 
+                         CoercGraph.meets metasenv subst context car1 car2 
+                       in
                         (match meets with
                         | [] -> raise exn
-                        | _::_::_ ->
-prerr_endline ("1: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-let m1::m2::_ = meets in
-prerr_endline ("M1 = " ^ CoercDb.name_of_carr m1 ^ "\nM2 = " ^ CoercDb.name_of_carr m2);
-assert false
-                        | [m] -> 
+                        | (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 with
-                            | Cic.Meta (i1,l1)
-                              when not (CoercDb.eq_carr m car1) ->
-                               (match
-                                 CoercGraph.look_for_coercion' metasenv subst
-                                  context m car1
-                                with
-                                 | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_)
-                                   ->
-                                    last,
-                                    fo_unif_subst test_equality_only subst context
+                           match last_tl1,to1 with
+                            | Cic.Meta (i1,l1),Some (last,coerced) -> 
+                                last,
+                                  fo_unif_subst test_equality_only subst context
                                      metasenv coerced last_tl1 ugraph
-                                 | _ ->
-prerr_endline ("2: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-assert false)
-                            | _ -> last_tl1,(subst,metasenv,ugraph) in
+                            | _ -> last_tl1,(subst,metasenv,ugraph) 
+                          in
                           let last_tl2',(subst,metasenv,ugraph) =
-                           match last_tl2 with
-                              Cic.Meta (i2,l2) when not (CoercDb.eq_carr m car2) ->
-                               (match
-                                 CoercGraph.look_for_coercion' metasenv subst
-                                  context m car2
-                                with
-                                   (*CSC: bu here: I am considering only the first one*)
-                                 | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_)
-                                   ->
-                                    last,
-                                    fo_unif_subst test_equality_only subst context
+                           match last_tl2,to2 with
+                            | Cic.Meta (i2,l2),Some (last,coerced) -> 
+                                last,
+                                  fo_unif_subst test_equality_only subst context
                                      metasenv coerced last_tl2 ugraph
-                                 | _ ->
-prerr_endline ("3: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-assert false)
-                            | _ -> last_tl2,(subst,metasenv,ugraph)
+                            | _ -> last_tl2,(subst,metasenv,ugraph) 
                           in
-(*DEBUGGING ONLY:
+                        (*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 =
index 70e90af52f2c4fb0333441b872873c6e5fbfec0e..37ded8ee0675de18ca3600be2cba6ac57ec1e75d 100644 (file)
@@ -39,6 +39,30 @@ type coercion_search_result =
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
+let saturate_coercion ul metasenv subst context =
+  let cl = List.map CicUtil.term_of_uri ul in
+  let funclass_arityl = 
+    let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
+    List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
+  in
+  let freshmeta = CicMkImplicit.new_meta metasenv subst in
+   List.map2
+    (fun arity c -> 
+      let ty,_ =
+       CicTypeChecker.type_of_aux' ~subst metasenv context c
+        CicUniv.empty_ugraph in
+      let _,metasenv,args,lastmeta =
+       TermUtil.saturate_term freshmeta metasenv context ty arity in
+      let irl =
+       CicMkImplicit.identity_relocation_list_for_metavariable context
+      in
+       metasenv, Cic.Meta (lastmeta-1,irl),
+        match args with
+           [] -> c
+         | _ -> Cic.Appl (c::args)
+    ) funclass_arityl cl
+;;
+          
 (* searches a coercion fron src to tgt in the !coercions list *)
 let look_for_coercion' metasenv subst context src tgt =
   try 
@@ -64,31 +88,7 @@ let look_for_coercion' metasenv subst context src tgt =
     in
      (match uri with
          None -> NoCoercion
-       | Some ul ->
-          let cl = List.map CicUtil.term_of_uri ul in
-          let funclass_arityl = 
-            let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
-            List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
-          in
-          let freshmeta = CicMkImplicit.new_meta metasenv subst in
-          let newtl =
-           List.map2
-            (fun arity c -> 
-              let ty,_ =
-               CicTypeChecker.type_of_aux' ~subst metasenv context c
-                CicUniv.empty_ugraph in
-              let _,metasenv,args,lastmeta =
-               TermUtil.saturate_term freshmeta metasenv context ty arity in
-              let irl =
-               CicMkImplicit.identity_relocation_list_for_metavariable context
-              in
-               metasenv, Cic.Meta (lastmeta-1,irl),
-                match args with
-                   [] -> c
-                 | _ -> Cic.Appl (c::args)
-            ) funclass_arityl cl
-          in
-           SomeCoercion newtl)
+       | Some ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
   with
     | CoercDb.EqCarrNotImplemented s -> NotHandled s
     | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
@@ -150,51 +150,114 @@ let is_composite t =
   with Invalid_argument _ -> false
 ;;
 
-let uniq = HExtlib.list_uniq ~eq:(fun (a,_) (b,_) -> CoercDb.eq_carr a b);;
+let coerced_arg l =
+  match l with
+  | [] | [_] -> assert false
+  | c::_ when not (CoercDb.is_a_coercion' c) -> assert false
+  | c::tl -> 
+     let arity = 
+       match CoercDb.is_a_coercion_to_funclass c with None -> 0 | Some a -> a 
+    in
+    (* decide a decent structure for coercion carriers so that all this stuff is
+     * useless *)
+    let pi = 
+      (* this calculation is not complete, since we have strange carriers *)
+      let rec count_pi = function
+        | Cic.Prod(_,_,t) -> 1+ (count_pi t)
+        | _ -> 0
+      in
+      let uri = CicUtil.uri_of_term c in
+      match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+      | Cic.Constant (_, _, ty, _, _) -> count_pi ty
+      | _ -> assert false
+    in
+    try Some (List.nth tl (pi - arity)) with Invalid_argument _ -> None
+;;
+
+(************************* meet calculation stuff ********************)
+let eq_uri_opt u1 u2 = 
+  match u1,u2 with
+  | Some u1, Some u2 -> UriManager.eq u1 u2
+  | None,Some _ | Some _, None -> false
+  | None, None -> true
+;;
+
+let eq_carr_uri (c1,u1) (c2,u2) = CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2;;
+
+let eq_carr_uri_uri (c1,u1,u11) (c2,u2,u22) = 
+  CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2 && eq_uri_opt u11 u22
+;;
+
+let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;;
+
+let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;;
 
-let splat e l = List.map (fun x -> e, x) l;;
+let splat e l = List.map (fun x -> e, Some x) l;;
 
+(* : carr -> (carr * uri option) where the option is always Some *)
 let get_coercions_to carr = 
   let l = CoercDb.to_list () in
-  List.flatten 
-    (HExtlib.filter_map 
-      (fun (src,tgt,cl) -> 
-        if CoercDb.eq_carr tgt carr then Some (splat src cl) else None) 
-      l)
+  let splat_coercion_to carr (src,tgt,cl) =
+    if CoercDb.eq_carr tgt carr then Some (splat src cl) else None
+  in
+  let l = List.flatten (HExtlib.filter_map (splat_coercion_to carr) l) in
+  l
 ;;
 
+(* : carr -> (carr * uri option) where the option is always Some *)
 let get_coercions_from carr = 
   let l = CoercDb.to_list () in
-  List.flatten 
-    (HExtlib.filter_map 
-      (fun (src,tgt,cl) -> 
-        if CoercDb.eq_carr src carr then Some (splat tgt cl) else None) 
-      l)
+  let splat_coercion_from carr (src,tgt,cl) =
+    if CoercDb.eq_carr src carr then Some (splat tgt cl) else None
+  in
+  List.flatten (HExtlib.filter_map (splat_coercion_from carr) l)
 ;;
 
+(* intersect { (s1,u1) | u1:s1->t1 } { (s2,u2) | u2:s2->t2 } 
+ * gives the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } *)
 let intersect l1 l2 = 
-  let is_in_l1 (x,_) = List.exists (fun (src,_) -> CoercDb.eq_carr x src) l1 in
-  uniq (List.filter is_in_l1 l2)
+  let is_in_l1 (x,u2) = 
+    HExtlib.filter_map 
+      (fun (src,u1) -> 
+         if CoercDb.eq_carr x src then Some (src,u1,u2) else None)
+    l1
+  in
+  uniq2 (List.flatten (List.map is_in_l1 l2))
 ;;
 
-let grow s = 
-  uniq (List.flatten (List.map (fun (x,_) -> get_coercions_to x) s) @ s)
+(* grow tgt gives all the (src,u) such that u:tgt->src *)
+let grow tgt = 
+  uniq ((tgt,None)::(get_coercions_to tgt))
 ;;
 
-let lb c = 
+let lb (c,_,_) = 
   let l = get_coercions_from c in
-  function x -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
+  fun (x,_,_) -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
 ;;
 
+(* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements 
+ * (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *)
 let rec min acc = function
   | c::tl -> 
     if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
   | [] -> acc
 ;;
 
-let meets left right =
-  let u = UriManager.uri_of_string "cic:/foo.con" in
-  min [] (List.map fst (intersect (grow [left,u]) (grow [right,u])))
+let meets metasenv subst context left right =
+  let saturate metasenv uo =
+    match uo with 
+    | None -> metasenv, None
+    | Some u -> 
+        match saturate_coercion [u] metasenv subst context with
+        | [metasenv, sat, last] -> metasenv, Some (sat, last)
+        | _ -> assert false
+  in
+  List.map 
+    (fun (c,uo1,uo2) -> 
+      let metasenv, uo1 = saturate metasenv uo1 in
+      let metasenv, uo2 = saturate metasenv uo2 in
+      c,metasenv, uo1, uo2)
+    (min [] (intersect (grow left) (grow right)))
 ;;
 
 (* EOF *)
index 62e4844997e72f73bc02ae8e0c99fecaaee7f264..ae2bd9233943c3d1993be89f0c05d1fb6a775396 100644 (file)
@@ -52,7 +52,13 @@ val source_of: Cic.term -> Cic.term
 
 val generate_dot_file: unit -> string
 
+(* given the Appl contents returns the argument of the head coercion *)
+val coerced_arg: Cic.term list -> Cic.term 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 -> 
-    CoercDb.coerc_carr list
+    (CoercDb.coerc_carr * Cic.metasenv * 
+      (Cic.term * Cic.term) option * (Cic.term * Cic.term) option) list
   
index 4e64e6badc369c21d92e83d96c9719a4d72f1caa..a4908ce7c893141cb040a42e640fb78c7a46e4c3 100644 (file)
@@ -254,14 +254,27 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
         CoercDb.Fun arity
     | _ -> assert false    
   in
-  let already_in = 
+  let already_in_obj src_carr tgt_carr uri obj = 
      List.exists 
       (fun (s,t,ul) -> 
         List.exists 
          (fun u -> 
-           UriManager.eq u uri && 
+           let bo = 
+            match obj with 
+            | Cic.Constant (_, Some bo, _, _, _) -> bo
+            | _ -> assert false
+           in
            CoercDb.eq_carr s src_carr && 
-           CoercDb.eq_carr t tgt_carr) 
+           CoercDb.eq_carr t tgt_carr &&
+           if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
+           CicUniv.oblivion_ugraph)
+           then true else
+            (HLog.warn
+              ("Coercions " ^ 
+                UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri
+                uri^" are not convertible, but are between the same nodes.\n"^
+                "From now on nification can fail randomly.");
+             false))
          ul)
       (CoercDb.to_list ())
   in
@@ -272,52 +285,44 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
       CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri 
        baseuri
     in
+    let new_coercions = 
+      List.filter (fun (s,t,u,obj) -> not(already_in_obj s t u obj))
+      new_coercions 
+    in
     let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
-    if already_in then
-      (* this if starts here just to be sure the closure function works fine *)
-      begin 
-        assert (new_coercions = []); 
-        HLog.warn
-          (UriManager.string_of_uri uri ^ 
-            " is already declared as a coercion! skipping...");
-        [] 
-      end
-    else
-      begin
-        (* update the DB *)
-        List.iter 
-          (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) 
-          new_coercions;
-        CoercDb.add_coercion (src_carr, tgt_carr, uri);
-        (* add the composites obj and they eventual lemmas *)
-        let lemmas = 
-          if add_composites then
-            List.fold_left
-              (fun acc (_,tgt,uri,obj) -> 
-                add_single_obj uri obj refinement_toolkit;
-                let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
-                 (uri,arity)::acc) 
-              [] new_coercions
-          else
-            []
-        in
-        (* store that composite_uris are related to uri. the first component is
-         * the stuff in the DB while the second is stuff for remove_obj *)
-        (* 
-           prerr_endline ("adding: " ^ 
-             string_of_bool add_composites ^ UriManager.string_of_uri uri);
-           List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
-            composite_uris; 
-        *)
-        UriManager.UriHashtbl.add coercion_hashtbl uri 
-          (composite_uris,if add_composites then composite_uris else []);
-        (*
-        prerr_endline ("lemmas:");
-          List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
-          lemmas;
-        prerr_endline ("lemmas END");*)
-        lemmas
-      end
+    (* update the DB *)
+    List.iter 
+      (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) 
+      new_coercions;
+    CoercDb.add_coercion (src_carr, tgt_carr, uri);
+    (* add the composites obj and they eventual lemmas *)
+    let lemmas = 
+      if add_composites then
+        List.fold_left
+          (fun acc (_,tgt,uri,obj) -> 
+            add_single_obj uri obj refinement_toolkit;
+            let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
+             (uri,arity)::acc) 
+          [] new_coercions
+      else
+        []
+    in
+    (* store that composite_uris are related to uri. the first component is
+     * the stuff in the DB while the second is stuff for remove_obj *)
+    (* 
+       prerr_endline ("adding: " ^ 
+         string_of_bool add_composites ^ UriManager.string_of_uri uri);
+       List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+        composite_uris; 
+    *)
+    UriManager.UriHashtbl.add coercion_hashtbl uri 
+      (composite_uris,if add_composites then composite_uris else []);
+    (*
+    prerr_endline ("lemmas:");
+      List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+      lemmas;
+    prerr_endline ("lemmas END");*)
+    lemmas
 ;;
 
 let remove_coercion uri =