Bug fixed in insertion of parametric coercions.

To fix the bug, the CoercGraph.look_for_coercion now returns a term saturated
with Cic.Implicits. As usual, remember to refine the term before further usage.

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index b9c5b0c6a642e50210edf3a579e1824da510d8c2..844260480134d42fd61acc3efbae44b755ccd2ef 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -118,54 +118,6 @@ let is_a_double_coercion t =
       | _ -> dummyres)
   | _ -> dummyres
   
-let avoid_double_coercion context subst metasenv ugraph t ty = 
-  let arity_of con =
-    try
-      let ty,_=CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
-      let rec count_pi = function
-        | Cic.Prod (_,_,t) -> 1 + count_pi t
-        | _ -> 0
-      in
-      count_pi ty
-    with Invalid_argument _ -> assert false (* all coercions have an uri *)
-  in
-  let rec mk_implicits tail = function
-    | 0 -> [tail] 
-    | n -> Cic.Implicit None :: mk_implicits tail (n-1)
-  in
-  let b, c1, c2, head = is_a_double_coercion t in
-  if b then
-    let source_carr = CoercGraph.source_of c2 in
-    let tgt_carr = CicMetaSubst.apply_subst subst ty in
-    (match CoercGraph.look_for_coercion source_carr tgt_carr 
-    with
-    | CoercGraph.SomeCoercion c -> 
-        let arity = arity_of c in
-        let args = mk_implicits head (arity - 1) in
-        let c_bo = CicUtil.term_of_uri (CicUtil.uri_of_term c) in
-        let newt = Cic.Appl (c_bo::args) in
-        (try
-          let subst, metasenv, ugraph = 
-           fo_unif_subst subst context metasenv newt t ugraph
-          in
-          debug_print 
-            (lazy 
-              ("packing: " ^ 
-                CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args))));
-          Cic.Appl (c::args), ty, subst, metasenv, ugraph
-         with
-            RefineFailure _ ->
-             prerr_endline ("#### Coercion not packed (Refine_failure): " ^
-              CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args)));
-             assert false
-          | Uncertain _ ->
-             prerr_endline ("#### Coercion not packed (Uncercatin case): " ^
-              CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args)));
-             assert false)
-    | _ -> assert false) (* the composite coercion must exist *)
-  else
-    t, ty, subst, metasenv, ugraph  
-
 let rec type_of_constant uri ugraph =
  let module C = Cic in
  let module R = CicReduction in
@@ -395,8 +347,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     t, cast, subst, metasenv, ugraph
                 | term -> 
                     let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
-                    let search = CoercGraph.look_for_coercion in
-                    let boh = search coercion_src coercion_tgt in
+                    let boh =
+                     CoercGraph.look_for_coercion coercion_src coercion_tgt
+                    in
                     (match boh with
                     | CoercGraph.NoCoercion
                     | CoercGraph.NotHandled _ ->
@@ -416,10 +369,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                           CicMetaSubst.ppterm_in_context 
                            subst coercion_src context ^ " that is not a sort")))
                     | CoercGraph.SomeCoercion c -> 
+                       let newt,_,subst,metasenv,ugraph = 
+                         type_of_aux subst metasenv context (Cic.Appl[c;t])
+                          ugraph in
                        let newt, tty, subst, metasenv, ugraph = 
-                         avoid_double_coercion context
-                          subst metasenv ugraph
-                            (Cic.Appl[c;t]) coercion_tgt
+                         avoid_double_coercion context subst metasenv ugraph
+                          newt coercion_tgt
                        in
                         newt, tty, subst, metasenv, ugraph)
             in
@@ -456,14 +411,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                   | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
                   | coercion_src ->
                      let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
-                     let search = CoercGraph.look_for_coercion in
-                     let boh = search coercion_src coercion_tgt in
+                     let boh =
+                      CoercGraph.look_for_coercion coercion_src coercion_tgt
+                     in
                       match boh with
                       | CoercGraph.SomeCoercion c -> 
+                        let newt,_,subst',metasenv',ugraph1 = 
+                         type_of_aux subst' metasenv' context (Cic.Appl[c;s'])
+                          ugraph1 in
                         let newt, tty, subst', metasenv', ugraph1 = 
-                          avoid_double_coercion context
-                           subst' metasenv' ugraph1 
-                             (Cic.Appl[c;s']) coercion_tgt 
+                          avoid_double_coercion context subst' metasenv'
+                           ugraph1 newt coercion_tgt 
                         in
                          newt, tty, subst', metasenv', ugraph1
                       | CoercGraph.NoCoercion
@@ -1111,6 +1069,43 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
                 (CicPp.ppterm t2''))))
 
+  and avoid_double_coercion context subst metasenv ugraph t ty = 
+    let b, c1, c2, head = is_a_double_coercion t in
+    if b then
+      let source_carr = CoercGraph.source_of c2 in
+      let tgt_carr = CicMetaSubst.apply_subst subst ty in
+      (match CoercGraph.look_for_coercion source_carr tgt_carr 
+      with
+      | CoercGraph.SomeCoercion c -> 
+         let newt =
+          match c with
+             Cic.Appl l -> Cic.Appl (l @ [head])
+           | _ -> Cic.Appl [c;head]
+         in
+          (try
+            let newt,_,subst,metasenv,ugraph = 
+              type_of_aux subst metasenv context newt ugraph in
+            let subst, metasenv, ugraph = 
+             fo_unif_subst subst context metasenv newt t ugraph
+            in
+            debug_print 
+              (lazy 
+                ("packing: " ^ 
+                  CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
+            newt, ty, subst, metasenv, ugraph
+           with
+              RefineFailure _ ->
+               prerr_endline ("#### Coercion not packed (Refine_failure): " ^
+                CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
+               assert false
+            | Uncertain _ ->
+               prerr_endline ("#### Coercion not packed (Uncercatin case): " ^
+                CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
+               assert false)
+      | _ -> assert false) (* the composite coercion must exist *)
+    else
+      t, ty, subst, metasenv, ugraph  
+
   and eat_prods 
     allow_coercions subst metasenv context he hetype tlbody_and_type ugraph 
   =
@@ -1216,20 +1211,20 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                                 CicMetaSubst.ppterm_in_context subst s context
                                  (* "\nReason: " ^ Lazy.force e*))))
                        | CoercGraph.SomeCoercion c -> 
+                          try
+                           let newt,newhety,subst,metasenv,ugraph = 
+                            type_of_aux subst metasenv context
+                             (Cic.Appl[c;hete]) ugraph in
                            let newt, _, subst, metasenv, ugraph = 
-                             avoid_double_coercion context
-                              subst metasenv ugraph 
-                                (Cic.Appl[c;hete]) tgt_carr in
-                           try
-                            let newty,newhety,subst,metasenv,ugraph = 
-                              type_of_aux subst metasenv context newt ugraph in
+                            avoid_double_coercion context subst metasenv
+                             ugraph newt tgt_carr in
                             let subst,metasenv,ugraph1 = 
                              fo_unif_subst subst context metasenv 
                                 newhety s ugraph
                             in
                              newt, subst, metasenv, ugraph
-                           with _ ->
-                            enrich localization_tbl hete
+                          with _ ->
+                           enrich localization_tbl hete
                              ~f:(fun _ ->
                                (lazy ("The term " ^
                                  CicMetaSubst.ppterm_in_context subst hete

diff --git a/components/library/coercGraph.ml b/components/library/coercGraph.ml
index 62a89b0a71ea36ed8b5ad3b48912a1c7af8616a9..06d7a12d3ea3a5e250ae595dc747d906e75b0857 100644 (file)
--- a/components/library/coercGraph.ml
+++ b/components/library/coercGraph.ml
@@ -38,34 +38,61 @@ let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (* searches a coercion fron src to tgt in the !coercions list *)
 let look_for_coercion src tgt =
+  let arity_of con =
+    try
+      let ty,_ = CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
+      let rec count_pi = function
+        | Cic.Prod (_,_,t) -> 1 + count_pi t
+        | _ -> 0
+      in
+      count_pi ty
+    with Invalid_argument _ -> assert false (* all coercions have an uri *)
+  in
+  let rec mk_implicits = function
+    | 0 -> [] 
+    | n -> Cic.Implicit None :: mk_implicits (n-1)
+  in
   try 
     let l = 
       CoercDb.find_coercion 
-        (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) 
+        (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in
+    let uri =
+     match l with
+     | [] -> 
+         debug_print 
+           (lazy 
+             (sprintf ":-( coercion non trovata da %s a %s" 
+               (CoercDb.name_of_carr src) 
+               (CoercDb.name_of_carr tgt)));
+         None
+     | [u] -> 
+         debug_print (lazy (
+           sprintf ":-) TROVATA 1 coercion da %s a %s: %s" 
+             (CoercDb.name_of_carr src) 
+             (CoercDb.name_of_carr tgt)
+             (UriManager.name_of_uri u)));
+         Some u
+     | u::_ -> 
+         debug_print (lazy (
+           sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" 
+             (List.length l)
+             (CoercDb.name_of_carr src) 
+             (CoercDb.name_of_carr tgt)
+             (UriManager.name_of_uri u)));
+         Some u
     in
-    match l with
-    | [] -> 
-        debug_print 
-          (lazy 
-            (sprintf ":-( coercion non trovata da %s a %s" 
-              (CoercDb.name_of_carr src) 
-              (CoercDb.name_of_carr tgt)));
-        NoCoercion
-    | [u] -> 
-        debug_print (lazy (
-          sprintf ":-) TROVATA 1 coercion da %s a %s: %s" 
-            (CoercDb.name_of_carr src) 
-            (CoercDb.name_of_carr tgt)
-            (UriManager.name_of_uri u)));
-        SomeCoercion (CicUtil.term_of_uri u)
-    | u::_ -> 
-        debug_print (lazy (
-          sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" 
-            (List.length l)
-            (CoercDb.name_of_carr src) 
-            (CoercDb.name_of_carr tgt)
-            (UriManager.name_of_uri u)));
-        SomeCoercion (CicUtil.term_of_uri u)
+     (match uri with
+         None -> NoCoercion
+       | Some u ->
+          let c = CicUtil.term_of_uri u in
+          let arity = arity_of c in
+          let args = mk_implicits (arity - 1) in
+          let newt =
+           match args with
+              [] -> c
+            | _ -> Cic.Appl (c::args)
+          in
+           SomeCoercion newt)
   with
     | CoercDb.EqCarrNotImplemented s -> NotHandled s
     | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed