]> matita.cs.unibo.it Git - helm.git/commitdiff
compose tactic restore and added nocomposites keyword
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 16 Nov 2007 14:24:24 +0000 (14:24 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 16 Nov 2007 14:24:24 +0000 (14:24 +0000)
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/library/coercDb.ml
helm/software/components/library/librarySync.ml
helm/software/components/tactics/closeCoercionGraph.ml
helm/software/components/tactics/compose.ml

index cf9106ea374d44527481c5e12297be63ee52f9f2..fd3c444b9d26e009e55b23453949e60bd1df5ebe 100644 (file)
@@ -265,9 +265,9 @@ let pp_default what uris =
     (String.concat " " (List.map UriManager.string_of_uri uris))
 
 let pp_coercion uri do_composites arity saturations=
-   Printf.sprintf "coercion %s %d %d (* %s *)"
+   Printf.sprintf "coercion %s %d %d %s"
     (UriManager.string_of_uri uri) arity saturations
-    (if do_composites then "compounds" else "no compounds")
+    (if do_composites then "" else "nocomposites")
     
 let pp_command ~term_pp ~obj_pp = function
   | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
index a0fd3335806f1468e3c637621b4cc4f9faef0c64..50a373e49bf8b8389d0aad6836d2459c17f59a30 100644 (file)
@@ -637,11 +637,13 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
-    | IDENT "coercion" ; suri = URI ; arity = OPT int ; saturations = OPT int ->
+    | IDENT "coercion" ; suri = URI ; arity = OPT int ; 
+      saturations = OPT int; composites = OPT (IDENT "nocomposites") ->
         let arity = match arity with None -> 0 | Some x -> x in
         let saturations = match saturations with None -> 0 | Some x -> x in
+        let composites = match composites with None -> true | Some _ -> false in
         GrafiteAst.Coercion
-         (loc, UriManager.uri_of_string suri, true, arity, saturations)
+         (loc, UriManager.uri_of_string suri, composites, arity, saturations)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
index 14ddf7c8631b5054aca10a8accc0268e9c12b05f..0ca40eb1c2860cef5da6d5def71040cfb7422234 100644 (file)
@@ -73,16 +73,12 @@ let eq_carr ?(exact=false) src tgt =
   match src, tgt with
   | Uri src, Uri tgt -> 
       let coarse_eq = UriManager.eq src tgt in
-      let src_noxpointer = UriManager.strip_xpointer src in
-      if exact && coarse_eq && UriManager.uri_is_ind src_noxpointer then
-        match 
-          fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph src_noxpointer)
-        with
-        | Cic.InductiveDefinition (_,[],m,_) when m = 0 -> true
-        | Cic.Constant _ -> true
-        | _ -> false
-      else
-        coarse_eq
+      let t = CicUtil.term_of_uri src in
+      let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in
+      (match ty, exact with
+      | Cic.Prod _, true -> false
+      | Cic.Prod _, false -> coarse_eq
+      | _ -> coarse_eq) 
   | Sort (Cic.Type _), Sort (Cic.Type _) -> true
   | Sort src, Sort tgt when src = tgt -> true
   | Term t1, Term t2 ->
index c6682bd9100df786a88c71425230f8a219de07ed..c36d84c90dd88de02938fdef9507906a55659edb 100644 (file)
@@ -318,7 +318,9 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
       (CoercDb.to_list ())
   in
   if not add_composites then
-    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[])
+    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+    UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]);
+    [])
   else
     let new_coercions = 
       CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
@@ -337,14 +339,11 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
     CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
     (* add the composites obj and they eventual lemmas *)
     let lemmas = 
-      if add_composites then
         List.fold_left
           (fun acc (_,tgt,uri,saturations,obj,arity) -> 
             add_single_obj uri obj refinement_toolkit;
              (uri,arity,saturations)::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 *)
@@ -354,8 +353,8 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
        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 []);
+    UriManager.UriHashtbl.add 
+      coercion_hashtbl uri (composite_uris,composite_uris);
     (*
     prerr_endline ("lemmas:");
       List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
@@ -373,7 +372,8 @@ let remove_coercion uri =
     List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
       composites_in_db;*)
     UriManager.UriHashtbl.remove coercion_hashtbl uri;
-    CoercDb.remove_coercion (fun (_,_,u,_) -> UriManager.eq uri u);
+    CoercDb.remove_coercion 
+      (fun (_,_,u,_) -> UriManager.eq uri u);
     (* remove from the DB *) 
     List.iter 
       (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
@@ -381,7 +381,7 @@ let remove_coercion uri =
     (* remove composites from the lib *)
     List.iter remove_single_obj composites_in_lib
   with
-    Not_found -> () (* mhh..... *)
+    Not_found -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *)
     
 
 let generate_projections refinement_toolkit uri fields =
index 95b9fd6e04f04a100746d316a95059fe264eae15..7ed3c36e6b86d24d4a46b753a750e11597d919c0 100644 (file)
@@ -39,21 +39,33 @@ let get_closure_coercions src tgt uri coercions =
   in
   let uri = enrich uri tgt in
   let eq_carr ?exact s t = 
+    debug_print (lazy(CoercDb.name_of_carr s^" VS "^CoercDb.name_of_carr t));
     try
-      CoercDb.eq_carr ?exact s t
+            let rc = CoercDb.eq_carr ?exact s t in
+            debug_print(lazy(string_of_bool rc));
+            rc
     with
-    | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
+    | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> 
+        debug_print (lazy("false"));            
+        false
   in
   match src,tgt with
   | CoercDb.Uri _, CoercDb.Uri _ ->
+                  debug_print (lazy ("Uri, Uri4"));
       let c_from_tgt = 
         List.filter 
-          (fun (f,t,_) -> eq_carr f tgt (*&& not (eq_carr t src)*)) 
+          (fun (f,t,_) -> 
+                  
+                  debug_print (lazy ("Uri, Uri3"));
+                  eq_carr f tgt (*&& not (eq_carr t src)*)) 
           coercions 
       in
       let c_to_src = 
         List.filter 
-          (fun (f,t,_) -> eq_carr t src (*&& not (eq_carr f tgt)*)) 
+          (fun (f,t,_) -> 
+                  
+                  debug_print (lazy ("Uri, Uri2"));
+                  eq_carr t src (*&& not (eq_carr f tgt)*)) 
           coercions 
       in
         (HExtlib.flatten_map 
@@ -70,6 +82,7 @@ let get_closure_coercions src tgt uri coercions =
               (fun (_,t,u2l) ->
                 HExtlib.flatten_map
                   (fun u1 ->
+                  debug_print (lazy ("Uri, Uri1"));
                     if  eq_carr ~exact:true s t
                      || eq_carr ~exact:true s tgt
                      || eq_carr ~exact:true src t
@@ -122,8 +135,8 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
       names
   in
   let compose c1 nc1 c2 nc2 =
-   Cic.Appl (CicSubstitution.lift 1 c2 :: mk_implicits (nc2 - sat2 - 1) @
-     Cic.Appl (CicSubstitution.lift 1 c1 :: mk_implicits nc1 ) ::
+   Cic.Appl ((*CicSubstitution.lift 1*) c2 :: mk_implicits (nc2 - sat2 - 1) @
+     Cic.Appl ((*CicSubstitution.lift 1*) c1 :: mk_implicits nc1 ) ::
      mk_implicits sat2)
   in
   let rec create_subst_from_metas_to_rels n = function 
@@ -205,8 +218,14 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
     let meta_to_be_coerced =
      try
       match List.nth l_c1 (c1_pis - sat1 - 1) with
-       | Cic.Meta (i,_) -> i
-       | _ -> assert false
+       | Cic.Meta (i,_) -> Some i
+       | t -> 
+          debug_print 
+            (lazy("meta_to_be_coerced: " ^ CicPp.ppterm t));
+          debug_print 
+            (lazy("c1_pis: " ^ string_of_int c1_pis ^ 
+             " sat1:" ^ string_of_int sat1));
+          None
      with
       Failure _ -> assert false
     in
@@ -230,15 +249,20 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
       | (i,_,_)::_ when i = n -> acc
       | _::tl -> position_of n (acc + 1) tl
     in
-    debug_print
-     (lazy ("META_TO_BE_COERCED: " ^ string_of_int meta_to_be_coerced));
-    let position_of_meta_to_be_coerced =
-     position_of meta_to_be_coerced 0 sorted in
-     debug_print (lazy ("POSITION_OF_META_TO_BE_COERCED: " ^
-      string_of_int position_of_meta_to_be_coerced));
-     debug_print (lazy ("SATURATIONS: " ^
-      string_of_int (List.length sorted - position_of_meta_to_be_coerced - 1)));
-     sorted, List.length sorted - position_of_meta_to_be_coerced - 1
+    let saturations_res = 
+      match meta_to_be_coerced with
+      | None -> 0
+      | Some meta_to_be_coerced -> 
+          debug_print
+            (lazy ("META_TO_BE_COERCED: " ^ string_of_int meta_to_be_coerced));
+          let position_of_meta_to_be_coerced =
+            position_of meta_to_be_coerced 0 sorted in
+          debug_print (lazy ("POSITION_OF_META_TO_BE_COERCED: " ^
+            string_of_int position_of_meta_to_be_coerced));
+          List.length sorted - position_of_meta_to_be_coerced - 1
+    in
+    debug_print (lazy ("SATURATIONS: " ^ string_of_int saturations_res));
+    sorted, saturations_res
   in
   let namer l n = 
     let l = List.map (function Cic.Name s -> s | _ -> "A") l in
@@ -270,6 +294,8 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
         CicRefine.type_of_aux' metasenv context c univ
       in
       debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term));
+      debug_print(lazy("COMPOSED REFINED (pretty): "^
+        CicMetaSubst.ppterm_in_context [] ~metasenv term context));
 (*       let metasenv = order_metasenv metasenv in *)
 (*       debug_print(lazy("ORDERED MENV: "^CicMetaSubst.ppmetasenv [] metasenv)); *)
       let body_metasenv, lambdas_metasenv = 
@@ -353,7 +379,7 @@ let filter_duplicates l coercions =
           try 
             List.for_all2 (fun (u1,_,_) (u2,_) -> UriManager.eq u1 u2) l1 l2
           with
-          | Invalid_argument "List.for_all2" -> false)
+          | Invalid_argument "List.for_all2" -> debug_print (lazy("XXX")); false)
         coercions))
   l
 
@@ -404,6 +430,7 @@ let close_coercion_graph src tgt uri saturations baseuri =
   (* check if the coercion already exists *)
   let coercions = CoercDb.to_list () in
   let todo_list = get_closure_coercions src tgt (uri,saturations) coercions in
+  debug_print (lazy("composed " ^ string_of_int (List.length todo_list)));
   let todo_list = filter_duplicates todo_list coercions in
   try
     let new_coercions = 
@@ -462,9 +489,9 @@ CicCoercion.set_close_coercion_graph close_coercion_graph;;
 
 (* generate_composite (c2 (c1 s)) in the universe graph univ
  * both living in the same context and metasenv *)
-let generate_composite c1 c2 context metasenv univ sat2 =
+let generate_composite c1 c2 context metasenv univ sat1 sat2 =
  let a,b,c,_,_ =
-  generate_composite' (c1,0,0) (c2,sat2,0) context metasenv univ
+  generate_composite' (c1,sat1,0) (c2,sat2,0) context metasenv univ
  in
   a,b,c
 ;;
index 317030404d12acd322676fd91e56cf05b3fe79c5..6bc3dd0fa2160dac8117a9d64f52f94f4a1870b2 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
+let debug = false;;
+let debug_print = 
+  if not debug then (fun _ -> ()) else (fun s -> prerr_endline (Lazy.force s))
+;;
+
 let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 ;;
 
 let compose_core t2 t1 (proof, goal) =
@@ -34,11 +39,27 @@ let compose_core t2 t1 (proof, goal) =
   let ty2,_ = 
     CicTypeChecker.type_of_aux' metasenv context t2 CicUniv.oblivion_ugraph 
   in
-  let saturated_ty2, menv_for_saturated_ty2 = 
+  let saturated_ty2, menv_for_saturated_ty2, args_t2 = 
     let maxm = CicMkImplicit.new_meta metasenv [] in
-    let ty2, menv, _, _ = TermUtil.saturate_term maxm metasenv context ty2 0 in
-    ty2, menv
+    let ty2, menv, args, _ = 
+      TermUtil.saturate_term ~delta:false maxm metasenv context ty2 0 in
+    ty2, menv, args
+  in
+  let saturations_t2 = 
+    let rec aux n = function 
+      | Cic.Meta (i,_)::tl -> 
+          let _,c,ty = CicUtil.lookup_meta i menv_for_saturated_ty2 in
+          if fst (CicReduction.are_convertible c ty (Cic.Sort Cic.Prop)
+            CicUniv.oblivion_ugraph) 
+          then n else aux (n+1) tl
+      | _::tl -> aux (n+1) tl
+      | [] -> n+1
+    in
+      List.length args_t2 - aux 0 args_t2 +1
   in
+  debug_print (lazy("saturated_ty2: "^CicMetaSubst.ppterm_in_context
+    [] ~metasenv:menv_for_saturated_ty2 saturated_ty2 context ^
+    " saturations_t2:" ^ string_of_int saturations_t2));
   (* unifies t with saturated_ty2 and gives back a fresh meta of type t *)
   let unif menv t = 
     let m, menv2 =
@@ -64,22 +85,23 @@ let compose_core t2 t1 (proof, goal) =
         let b, newmenv, sb = unif menv s in
         if b then
           (saturations - cur - 1) :: 
-            (positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t))
+            (positions newmenv (cur + 1) saturations 
+             (CicSubstitution.subst sb t))
         else
           positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t)
     | _ -> []
   in
-  (* position is a list of arities, that is if t1 : a -> b -> c and saturations is
-   * 0 then the computed term will be (t1 ? t2) of type a -> c
-   * if saturations is 1 then (t1 t2 ?) of type b -> c *)
+  (* position is a list of arities, that is if t1 : a -> b -> c and saturations
+   * is 0 then the computed term will be (t1 ? t2) of type a -> c if saturations
+   * is 1 then (t1 t2 ?) of type b -> c *)
   let rec generate positions menv acc =
     match positions with
     | [] -> acc, menv
-    | saturations::tl ->
+    | saturations_t1::tl ->
       try
         let t, menv1, _ =
           CloseCoercionGraph.generate_composite t2 t1 context menv
-            CicUniv.oblivion_ugraph saturations
+            CicUniv.oblivion_ugraph saturations_t2 saturations_t1
         in
         assert (List.length menv1 = List.length menv);
         generate tl menv (t::acc)