X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FcloseCoercionGraph.ml;h=2c67c95ee2a333154b80bce2ac3cc3760b783548;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=0041685ef212d62d68e2c1bd453ad840cb263360;hpb=910c252965fe17d6b5af92e4658e7d02bac82d58;p=helm.git

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index 0041685ef..2c67c95ee 100644
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -89,8 +89,6 @@ let get_closure_coercions src tgt uri coercions =
   | _ -> [] (* do not close in case source or target is not an indty ?? *)
 ;;
 
-let obj_attrs n = [`Class (`Coercion n); `Generated]
-
 exception UnableToCompose
 
 (* generate_composite (c2 (c1 s)) in the universe graph univ
@@ -281,9 +279,11 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
   let c = mk_lambda_spine c (namer (names_c1 @ names_c2)) spine_len in
   debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c));
   let old_insert_coercions = !CicRefine.insert_coercions in
+  let old_pack_coercions = !CicRefine.pack_coercions in
   let c, metasenv, univ, saturationsres, cpos =
     try
       CicRefine.insert_coercions := false;
+      CicRefine.pack_coercions := false;
       let term, ty, metasenv, ugraph = 
         CicRefine.type_of_aux' metasenv context c univ
       in
@@ -334,32 +334,92 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
       debug_print (lazy ("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
       debug_print (lazy ("####################"));
       CicRefine.insert_coercions := old_insert_coercions;
+      CicRefine.pack_coercions := old_pack_coercions;
       term, metasenv, ugraph, saturationsres, cpos
     with
     | CicRefine.RefineFailure s 
     | CicRefine.Uncertain s -> debug_print s; 
         CicRefine.insert_coercions := old_insert_coercions;
+        CicRefine.pack_coercions := old_pack_coercions;
         raise UnableToCompose
     | exn ->
         CicRefine.insert_coercions := old_insert_coercions;
+        CicRefine.pack_coercions := old_pack_coercions;
         raise exn
   in
-  c, metasenv, univ, saturationsres, arity2, cpos
+  let c_ty, univ = 
+    CicTypeChecker.type_of_aux' ~subst:[] [] [] c univ
+  in
+  let real_composed = ref true in
+  let c = 
+    let rec is_id = function
+      | Cic.Lambda(_,_,t) -> is_id t
+      | Cic.Rel 1 -> true
+      | _ -> false
+    in
+    let is_id = function
+      | Cic.Const (u,_) -> 
+          (match CicEnvironment.get_obj CicUniv.empty_ugraph u with
+          | Cic.Constant (_,Some bo,_,_,_), _ ->  is_id bo
+          | _ -> false)
+      | _ -> false
+    in
+    let unvariant u =
+     match CicEnvironment.get_obj CicUniv.empty_ugraph u with
+     | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _
+       when List.exists ((=) (`Flavour `Variant)) attrs ->
+         u'
+     | _ -> u
+    in
+    let is_variant u =
+     match CicEnvironment.get_obj CicUniv.empty_ugraph u with
+     | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _
+       when List.exists ((=) (`Flavour `Variant)) attrs -> true
+     | _ -> false
+    in
+    let rec aux = function
+      | Cic.Lambda(n,s,t) -> Cic.Lambda(n,s,aux t)
+      | Cic.Appl (c::_) as t -> 
+          let t = 
+            if is_id c then
+              (real_composed := false ;
+               CicReduction.head_beta_reduce ~delta:true t)
+            else t
+          in 
+          (match t with
+          | Cic.Appl l -> Cic.Appl (List.map aux l)
+          | Cic.Const (u,[]) when is_variant u -> Cic.Const (unvariant u,[])
+          | t -> t)
+       | Cic.Const (u,[]) when is_variant u -> Cic.Const (unvariant u,[])
+       | t -> t
+    in
+    let simple_eta_c t = 
+      let incr = 
+        List.map (function Cic.Rel n -> Cic.Rel (n+1) | _ -> assert false)
+      in
+      let rec aux acc ctx = function
+        | Cic.Lambda (n,s,tgt) -> 
+            aux (incr acc @ [Cic.Rel 1]) (Some (n,Cic.Decl s) ::ctx) tgt
+        | Cic.Appl (t::tl) when tl = acc && 
+            CicTypeChecker.does_not_occur ctx 0 (List.length acc) t -> true, t
+        | t -> false, t
+      in
+      let b, newt = aux [] [] t in
+      if b then newt else t
+    in
+     simple_eta_c (aux c)
+  in
+  debug_print (lazy ("COMPOSED COMPRESSED: " ^ string_of_bool !real_composed ^" : " ^ CicPp.ppterm c));
+  c, c_ty, metasenv, univ, saturationsres, arity2, cpos, !real_composed
 ;;
 
-let build_obj c univ arity =
-  let c_ty,univ = 
-    try 
-      CicTypeChecker.type_of_aux' [] [] c univ
-    with CicTypeChecker.TypeCheckerFailure s ->
-      debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s" 
-        (CicPp.ppterm c) (Lazy.force s)));
-      raise UnableToCompose
-  in
+let build_obj c c_ty univ arity is_var =
   let cleaned_ty =
     FreshNamesGenerator.clean_dummy_dependent_types c_ty 
   in
-  let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs arity) in 
+  let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],
+    [`Generated] @ if not is_var then [`Flavour `Variant] else [] )  in 
+
     obj,univ
 ;;
 
@@ -395,18 +455,10 @@ let number_if_already_defined buri name l =
         ("Unable to give an altenative name to " ^ buri ^ "/" ^ name ^ ".con"))
   in
   let rec aux n =
-    let suffix = if n > 0 then string_of_int n else "" in
+    let suffix = if n > 0 then ("__" ^ string_of_int n) else "" in
     let suri = buri ^ "/" ^ name ^ suffix ^ ".con" in
     let uri = UriManager.uri_of_string suri in
-    let retry () = 
-      if n < 100 then 
-        begin
-          HLog.warn ("Uri " ^ suri ^ " already exists.");
-          aux (n+1)
-        end
-      else
-        err ()
-    in
+    let retry () = if n < max_int then aux (n+1) else err () in
     if List.exists (UriManager.eq uri) l then retry ()
     else
       try
@@ -438,7 +490,7 @@ let close_coercion_graph src tgt uri saturations baseuri =
             | (he,saturations1,arity1) :: tl ->
                 let first_step = 
                   Cic.Constant ("", Some (CicUtil.term_of_uri he),
-                    Cic.Sort Cic.Prop, [], obj_attrs arity1),
+                  Cic.Sort Cic.Prop, [], [`Generated]),
                   saturations1,
                   arity1,0
                 in
@@ -446,14 +498,16 @@ let close_coercion_graph src tgt uri saturations baseuri =
                   List.fold_left (fun (o,univ) (coer,saturations2,arity2) ->
                     match o with 
                     | Cic.Constant (_,Some u,_,[],_),saturations1,arity1,_ ->
-                        let t, menv, univ, saturationsres, arityres, cposres = 
+                        let t, t_ty, menv, univ, saturationsres, 
+                          arityres, cposres, is_var 
+                        = 
                           generate_composite' (u,saturations1,arity1) 
                             (CicUtil.term_of_uri coer,
                              saturations2, arity2) [] [] univ
                         in
-                        if (menv = []) then
+                        if (menv <> []) then
                           HLog.warn "MENV non empty after composing coercions";
-                        let o,univ = build_obj t univ arityres in
+                        let o,univ = build_obj t t_ty univ arityres is_var in
                          (o,saturationsres,arityres,cposres),univ
                     | _ -> assert false 
                   ) (first_step, CicUniv.oblivion_ugraph) tl
@@ -485,7 +539,7 @@ 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 sat1 sat2 =
- let a,b,c,_,_,_ =
+ let a,_,b,c,_,_,_,_ =
   generate_composite' (c1,sat1,0) (c2,sat2,0) context metasenv univ
  in
   a,b,c