fixed coercions. composite can't occur if to funclass

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 798c38540d5118cc4f3f8ab190152d1dcfdebdd4..bd8e992d0bfdef7d8b3eddc39a0a4b4c1a25ed90 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -34,8 +34,8 @@ exception AssertFailure of string Lazy.t;;
 let insert_coercions = ref true
 let pack_coercions = ref true
 
-let debug_print = fun _ -> ()
-(* let debug_print x = prerr_endline (Lazy.force x);; *)
+(* let debug_print = fun _ -> () *)
+ let debug_print x = prerr_endline (Lazy.force x);; 
 
 let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
 
@@ -144,12 +144,17 @@ let is_a_double_coercion t =
       | _ -> dummyres)
   | _ -> dummyres
 
-let more_args_than_expected subst he context hetype' tlbody_and_type =
-  lazy ("The term " ^
-    CicMetaSubst.ppterm_in_context subst he context ^ 
-    " (that has type " ^ CicMetaSubst.ppterm_in_context subst hetype' context ^
-    ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
-    " arguments that are more than expected")
+let more_args_than_expected
+  localization_tbl subst he context hetype' tlbody_and_type exn
+=
+  let msg = 
+    lazy ("The term " ^
+      CicMetaSubst.ppterm_in_context subst he context ^ 
+      " (that has type "^CicMetaSubst.ppterm_in_context subst hetype' context ^
+      ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
+      " arguments that are more than expected")
+  in
+  enrich localization_tbl he ~f:(fun _-> msg) exn
 ;; 
 
 let mk_prod_of_metas metasenv context' subst args = 
@@ -1248,7 +1253,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               debug_print
                 (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
               t, ty, subst, metasenv, ugraph)
-      | _ -> assert false) (* the composite coercion must exist *)
+      | _ -> t, ty, subst, metasenv, ugraph)
     else
       t, ty, subst, metasenv, ugraph  
 
@@ -1286,8 +1291,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
         let metasenv = pristinemenv in
         debug_print (lazy 
           ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^
-           " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' ^ 
-           " cause: " ^ Lazy.force s));
+           " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' 
+           (* ^ " cause: " ^ Lazy.force s *)));
         let how_many_args_are_needed = 
           let rec aux n = function
             | Cic.Prod(_,_,t) -> aux (n+1) t
@@ -1353,22 +1358,21 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                             metasenv context subst t tty remainder ugraph
                         in
                         Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
-                      with exn -> None
-                with exn -> None)
+                      with Uncertain _ | RefineFailure _ -> None
+                with Uncertain _ | RefineFailure _ -> None)
               candidates
            with
            | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
                subst,metasenv,ugraph,hetype',he,args_bo_and_ty
            | None -> 
-               enrich localization_tbl he
-                ~f:(fun _-> more_args_than_expected subst he context hetype
-                             args_bo_and_ty) exn
+               more_args_than_expected localization_tbl 
+                 subst he context hetype args_bo_and_ty exn
       (* }}} end coercion to funclass stuff *)           
       (* }}} end fix_arity *)           
     in
     (* aux function to process the type of the head and the args in parallel *)
     let rec eat_prods_and_args 
-      pristinemenv metasenv subst context he hetype ugraph newargs 
+      pristinemenv metasenv subst context pristinehe he hetype ugraph newargs 
     =
       (* {{{ body *)
       function
@@ -1463,7 +1467,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                            "\nReason: " ^ Printexc.to_string exn))) exn
                   (* }}} end coercion stuff *)
                 in
-                  eat_prods_and_args pristinemenv metasenv subst context he
+                  eat_prods_and_args pristinemenv metasenv subst context pristinehe he
                     (CicSubstitution.subst (fst arg) t) 
                     ugraph1 (newargs@[arg]) tl
             | _ -> 
@@ -1474,14 +1478,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                        (newargs@[hete,hety]@tl) ugraph
                   in
                   eat_prods_and_args metasenv
-                    metasenv subst context he hetype' ugraph [] args_bo_and_ty
-                with RefineFailure s | Uncertain s ->
+                    metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty
+                with RefineFailure _ | Uncertain _ as exn ->
                   (* unable to fix arity *)
-                  let msg = 
-                   more_args_than_expected 
-                     subst he context hetype args_bo_and_ty
-                  in
-                  raise (RefineFailure msg)
+                   more_args_than_expected localization_tbl 
+                     subst he context hetype args_bo_and_ty exn
       (* }}} *)
     in
     (* first we check if we are in the simple case of a meta closed term *)
@@ -1495,7 +1496,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
     in
     let coerced_args,subst,metasenv,he,t,ugraph =
       eat_prods_and_args 
-        metasenv metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
+        metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
     in
     he,(List.map fst coerced_args),t,subst,metasenv,ugraph
   in

diff --git a/helm/software/matita/tests/coercions.ma b/helm/software/matita/tests/coercions.ma
index dc4e030bd45d5d0e925948546d0027a2964f110b..1d841d16ebc2f3cad7299d9ec30cf9198ffa81c8 100644 (file)
--- a/helm/software/matita/tests/coercions.ma
+++ b/helm/software/matita/tests/coercions.ma
@@ -105,7 +105,8 @@ definition church: nat \to nat \to nat \def times.
 coercion cic:/matita/tests/coercions/church.con 1.
 
 definition mapmult:  \forall n:nat.\forall l:listn nat n. nat \to nat \to nat \def
-  \lambda n:nat.\lambda l:listn nat n.\lambda m,o:nat.l m o.
+  \lambda n:nat.\lambda l:listn nat n.\lambda m,o:nat.
+  l (m m) o (o o o).