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

diff --git a/helm/software/components/library/cicCoercion.ml b/helm/software/components/library/cicCoercion.ml
index 85dc9f65b83d8951022dc510a770b392e78043f7..638c0ce64a81d037749048c9a698362bde6b0916 100644 (file)
--- a/helm/software/components/library/cicCoercion.ml
+++ b/helm/software/components/library/cicCoercion.ml
@@ -29,7 +29,7 @@ let close_coercion_graph_ref = ref
  (fun _ _ _ _ _ -> [] : 
    CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
    string (* baseuri *) ->
-     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) list)
+     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj * int) list)
 ;;
 
 let set_close_coercion_graph f = close_coercion_graph_ref := f;;

diff --git a/helm/software/components/library/cicCoercion.mli b/helm/software/components/library/cicCoercion.mli
index d862297261eecf8a37801db95d2a707e178cc0e8..97463b1d6e32a66e60945ab05e00a6779b9e2b36 100644 (file)
--- a/helm/software/components/library/cicCoercion.mli
+++ b/helm/software/components/library/cicCoercion.mli
@@ -28,11 +28,13 @@
 val set_close_coercion_graph : 
   (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
   string (* baseuri *) ->
-    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) list)
+    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri *
+      int (* saturations *) * Cic.obj * int (* arity *)) list)
   -> unit
 
 val close_coercion_graph:
   CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
   string (* baseuri *) ->
-    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) list
+    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri *
+      int (* saturations *) * Cic.obj * int (* arity *) ) list
 

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 5897d62ba8c81256b3213af333c9a1d0cbf03baa..5189547d33135903df0731105a50fa99041b2f91 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -314,13 +314,13 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
        baseuri
     in
     let new_coercions = 
-      List.filter (fun (s,t,u,saturations,obj) -> not(already_in_obj s t u obj))
+      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
+    let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in
     (* update the DB *)
     List.iter 
-      (fun (src,tgt,uri,saturations,_) ->
+      (fun (src,tgt,uri,saturations,_,_) ->
         CoercDb.add_coercion (src,tgt,uri,saturations)) 
       new_coercions;
     CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
@@ -328,9 +328,8 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
     let lemmas = 
       if add_composites then
         List.fold_left
-          (fun acc (_,tgt,uri,saturations,obj) -> 
+          (fun acc (_,tgt,uri,saturations,obj,arity) -> 
             add_single_obj uri obj refinement_toolkit;
-            let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
              (uri,arity,saturations)::acc) 
           [] new_coercions
       else

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index 68e4e7cb2c2b2c176e274e76b6257ea7e09cf2a0..d558c0ef030e6a1af2ff864b243dc1af410637ea 100644 (file)
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/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
 ;;

diff --git a/helm/software/components/tactics/closeCoercionGraph.mli b/helm/software/components/tactics/closeCoercionGraph.mli
index baf926ff156e37d1d685a7a38c54e6127eeaed03..7157e5c2de683aff7670b5c798d3b750c79a5118 100644 (file)
--- a/helm/software/components/tactics/closeCoercionGraph.mli
+++ b/helm/software/components/tactics/closeCoercionGraph.mli
@@ -28,12 +28,12 @@
 val close_coercion_graph:
   CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
   string (* baseuri *) ->
-    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj)
-      list
+    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri *
+      int (* saturations *) * Cic.obj * int (* arity *)) list
 
 exception UnableToCompose
 
 val generate_composite:
-  Cic.term -> Cic.term -> Cic.context -> 
-  Cic.metasenv -> CicUniv.universe_graph -> int (* arity *) -> 
+  Cic.term -> Cic.term (* t2 *) -> Cic.context -> 
+  Cic.metasenv -> CicUniv.universe_graph -> int (* saturations of t2 *) ->
     Cic.term * Cic.metasenv * CicUniv.universe_graph

diff --git a/helm/software/components/tactics/compose.ml b/helm/software/components/tactics/compose.ml
index cd355dc2785049d44dd78630401ea1884a052087..317030404d12acd322676fd91e56cf05b3fe79c5 100644 (file)
--- a/helm/software/components/tactics/compose.ml
+++ b/helm/software/components/tactics/compose.ml
@@ -59,27 +59,27 @@ let compose_core t2 t1 (proof, goal) =
     | CicUnification.Uncertain _ -> false, menv2, m
   in
   (* check which "positions" in the input arrow unifies with saturated_ty2 *)
-  let rec positions menv cur arity = function 
+  let rec positions menv cur saturations = function 
     | Cic.Prod (n,s,t) -> 
         let b, newmenv, sb = unif menv s in
         if b then
-          (arity - cur - 1) :: 
-            (positions newmenv (cur + 1) arity (CicSubstitution.subst sb t))
+          (saturations - cur - 1) :: 
+            (positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t))
         else
-          positions newmenv (cur + 1) arity (CicSubstitution.subst sb t)
+          positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t)
     | _ -> []
   in
-  (* position is a list of arities, that is if t1 : a -> b -> c and arity is
+  (* 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 arity is 1 then (t1 t2 ?) of type b -> c *)
+   * if saturations is 1 then (t1 t2 ?) of type b -> c *)
   let rec generate positions menv acc =
     match positions with
     | [] -> acc, menv
-    | arity::tl ->
+    | saturations::tl ->
       try
         let t, menv1, _ =
           CloseCoercionGraph.generate_composite t2 t1 context menv
-            CicUniv.oblivion_ugraph arity
+            CicUniv.oblivion_ugraph saturations
         in
         assert (List.length menv1 = List.length menv);
         generate tl menv (t::acc)