From 403e3c6f8e9288926e1bca283ff0bf54233354a2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 15 Jan 2009 15:32:52 +0000
Subject: [PATCH] - name mangling changed, added __ to separate additional
 number - composing a coercion with an identity does not affect the body, and
 a variant is generated

---
 .../components/tactics/closeCoercionGraph.ml  | 89 +++++++++++++++----
 1 file changed, 74 insertions(+), 15 deletions(-)

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index ebf4cbc2a..2c67c95ee 100644
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -347,22 +347,79 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
         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,[],[`Generated]) in 
+  let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],
+    [`Generated] @ if not is_var then [`Flavour `Variant] else [] )  in 
+
     obj,univ
 ;;
 
@@ -398,7 +455,7 @@ 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 < max_int then aux (n+1) else err () in
@@ -441,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
                           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
@@ -480,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
-- 
2.39.2