Composition of coercions with arity > 0 is now implemented correctly.

[helm.git] / components / tactics / closeCoercionGraph.ml

diff --git a/components/tactics/closeCoercionGraph.ml b/components/tactics/closeCoercionGraph.ml
index 68e4e7cb2c2b2c176e274e76b6257ea7e09cf2a0..d558c0ef030e6a1af2ff864b243dc1af410637ea 100644 (file)
--- a/components/tactics/closeCoercionGraph.ml
+++ b/components/tactics/closeCoercionGraph.ml
@@ -33,6 +33,11 @@ let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
  * (source, list of coercions to follow, target)
  *)
 let get_closure_coercions src tgt uri coercions =
+  let enrich (uri,sat) tgt =
+   let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
+    uri,sat,arity
+  in
+  let uri = enrich uri tgt in
   let eq_carr ?exact s t = 
     try
       CoercDb.eq_carr ?exact s t
@@ -54,13 +59,13 @@ let get_closure_coercions src tgt uri coercions =
         (HExtlib.flatten_map 
           (fun (_,t,ul) -> 
              if eq_carr ~exact:true src t then [] else
-             List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
+             List.map (fun u -> src,[uri; enrich u t],t) ul) c_from_tgt) @
         (HExtlib.flatten_map 
-          (fun (s,_,ul) -> 
+          (fun (s,t,ul) -> 
              if eq_carr ~exact:true s tgt then [] else
-             List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
+             List.map (fun u -> s,[enrich u t; uri],tgt) ul) c_to_src) @
         (HExtlib.flatten_map 
-          (fun (s,_,u1l) ->
+          (fun (s,t1,u1l) ->
             HExtlib.flatten_map 
               (fun (_,t,u2l) ->
                 HExtlib.flatten_map
@@ -70,7 +75,7 @@ let get_closure_coercions src tgt uri coercions =
                      || eq_carr ~exact:true src t
                     then [] else
                     List.map 
-                      (fun u2 -> (s,[u1;uri;u2],t)) 
+                      (fun u2 -> (s,[enrich u1 t1;uri;enrich u2 t],t)) 
                       u2l)
                   u1l) 
               c_from_tgt) 
@@ -83,8 +88,14 @@ let obj_attrs n = [`Class (`Coercion n); `Generated]
 exception UnableToCompose
 
 (* generate_composite (c2 (c1 s)) in the universe graph univ
- * both living in the same context and metasenv *)
-let generate_composite' (c1,sat1) (c2,sat2) context metasenv univ arity =
+   both living in the same context and metasenv
+
+    c2 ?p2 (c1 ?p1 ?x ?s1) ?s2
+
+    where:
+     ?pn + 1 + ?sn = count_pi n - arity n
+*)
+let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
   let original_metasenv = metasenv in 
   let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in
   let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in
@@ -210,8 +221,8 @@ let generate_composite' (c1,sat1) (c2,sat2) context metasenv univ arity =
   debug_print (lazy ("\nCOMPOSING"));
   debug_print (lazy (" c1= "^CicPp.ppterm c1 ^"  :  "^ CicPp.ppterm c1_ty));
   debug_print (lazy (" c2= "^CicPp.ppterm c2 ^"  :  "^ CicPp.ppterm c2_ty));
-  let c1_pis, names_c1 = count_pis c1_ty 0 in 
-  let c2_pis, names_c2 = count_pis c2_ty arity in
+  let c1_pis, names_c1 = count_pis c1_ty arity1 in 
+  let c2_pis, names_c2 = count_pis c2_ty arity2 in
   let c = compose c1 c1_pis c2 c2_pis in
   let spine_len = c1_pis + c2_pis in
   let c = mk_lambda_spine c (namer (names_c1 @ names_c2)) spine_len in
@@ -278,7 +289,7 @@ let generate_composite' (c1,sat1) (c2,sat2) context metasenv univ arity =
         CicRefine.insert_coercions := old_insert_coercions;
         raise exn
   in
-  c, metasenv, univ, saturationsres
+  c, metasenv, univ, saturationsres, arity2
 ;;
 
 let build_obj c univ arity =
@@ -305,7 +316,7 @@ let filter_duplicates l coercions =
           CoercDb.eq_carr s src && 
           CoercDb.eq_carr t tgt &&
           try 
-            List.for_all2 (fun (u1,_) (u2,_) -> UriManager.eq u1 u2) l1 l2
+            List.for_all2 (fun (u1,_,_) (u2,_) -> UriManager.eq u1 u2) l1 l2
           with
           | Invalid_argument "List.for_all2" -> false)
         coercions))
@@ -366,44 +377,45 @@ let close_coercion_graph src tgt uri saturations baseuri =
           try 
             (match l with
             | [] -> assert false 
-            | (he,saturations1) :: tl ->
-                let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
+            | (he,saturations1,arity1) :: tl ->
                 let first_step = 
                   Cic.Constant ("", 
-                    Some (CoercDb.term_of_carr (CoercDb.Uri he)),
-                    Cic.Sort Cic.Prop, [], obj_attrs arity), saturations1
+                   Some (CoercDb.term_of_carr (CoercDb.Uri he)),
+                    Cic.Sort Cic.Prop, [], obj_attrs arity1),
+                  saturations1,
+                  arity1
                 in
                 let o,_ = 
-                  List.fold_left (fun (o,univ) (coer,saturations) ->
+                  List.fold_left (fun (o,univ) (coer,saturations2,arity2) ->
                     match o with 
-                    | Cic.Constant (_,Some u,_,[],_),saturations1 ->
-                        let t, menv, univ, saturationsres = 
-                          generate_composite' (u,saturations1) 
+                    | Cic.Constant (_,Some u,_,[],_),saturations1,arity1 ->
+                        let t, menv, univ, saturationsres, arityres = 
+                          generate_composite' (u,saturations1,arity1) 
                             (CoercDb.term_of_carr (CoercDb.Uri coer),
-                             saturations) [] [] univ arity
+                             saturations2, arity2) [] [] univ
                         in
                         if (menv = []) then
                           HLog.warn "MENV non empty after composing coercions";
-                        let o,univ = build_obj t univ arity in
-                         (o,saturationsres),univ
+                        let o,univ = build_obj t univ arityres in
+                         (o,saturationsres,arityres),univ
                     | _ -> assert false 
                   ) (first_step, CicUniv.empty_ugraph) tl
                 in
                 let name_src = CoercDb.name_of_carr src in
                 let name_tgt = CoercDb.name_of_carr tgt in
-                let by = List.map (fun u,_ -> UriManager.name_of_uri u) l in
+                let by = List.map (fun u,_,_ -> UriManager.name_of_uri u) l in
                 let name = mangle name_tgt name_src by in
                 let c_uri = 
                   number_if_already_defined baseuri name 
-                    (List.map (fun (_,_,u,_,_) -> u) acc) 
+                    (List.map (fun (_,_,u,_,_,_) -> u) acc) 
                 in
-                let named_obj,saturations = 
+                let named_obj,saturations,arity = 
                   match o with
-                  | Cic.Constant (_,bo,ty,vl,attrs),saturations ->
-                      Cic.Constant (name,bo,ty,vl,attrs),saturations
+                  | Cic.Constant (_,bo,ty,vl,attrs),saturations,arity ->
+                      Cic.Constant (name,bo,ty,vl,attrs),saturations,arity
                   | _ -> assert false 
                 in
-                  (src,tgt,c_uri,saturations,named_obj))::acc
+                  (src,tgt,c_uri,saturations,named_obj,arity))::acc
           with UnableToCompose -> acc
       ) [] todo_list
     in
@@ -415,9 +427,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 arity =
- let a,b,c,_ =
-  generate_composite' (c1,0) (c2,0) context metasenv univ arity
+let generate_composite c1 c2 context metasenv univ sat2 =
+ let a,b,c,_,_ =
+  generate_composite' (c1,0,0) (c2,sat2,0) context metasenv univ
  in
   a,b,c
 ;;