X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=d3a297d43e88b517cec0e9caf4eef32e322896d9;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=09265ef2e4c265007218bb81382aba337deb0ff0;hpb=ca7c474381445e17d15ced6bf42da16946335598;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 09265ef2e..d3a297d43 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -42,6 +42,12 @@ in profiler.HExtlib.profile foo ()
       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
 ;;
+
+let enrich f =
+ function
+    RefineFailure msg -> raise (RefineFailure (f msg))
+  | Uncertain msg -> raise (Uncertain (f msg))
+  | _ -> assert false
                        
 let rec split l n =
  match (l,n) with
@@ -392,12 +398,13 @@ and type_of_aux' metasenv context t ugraph =
                   let search = CoercGraph.look_for_coercion in
                   let boh = search coercion_src coercion_tgt in
                   (match boh with
-                  | CoercGraph.NoCoercion ->
-                      raise (RefineFailure (lazy "no coercion"))
+                  | CoercGraph.NoCoercion
                   | CoercGraph.NotHandled _ -> 
-                      raise (RefineFailure (lazy "not a sort in PI"))
+                     raise
+                      (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
                   | CoercGraph.NotMetaClosed -> 
-                      raise (Uncertain (lazy "Coercions on metas 1"))
+                     raise
+                      (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
                   | CoercGraph.SomeCoercion c -> 
                       Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
             in
@@ -426,22 +433,28 @@ and type_of_aux' metasenv context t ugraph =
         | C.Lambda (n,s,t) ->
 
             let s',sort1,subst',metasenv',ugraph1 = 
-              type_of_aux subst metasenv context s ugraph
-            in
-            (match CicReduction.whd ~subst:subst' context sort1 with
+              type_of_aux subst metasenv context s ugraph in
+            let s',sort1 =
+             match CicReduction.whd ~subst:subst' context sort1 with
                  C.Meta _
-               | C.Sort _ -> ()
-               | _ ->
-                   raise (RefineFailure (lazy (sprintf
-                                           "Not well-typed lambda-abstraction: the source %s should be a type;
-           instead it is a term of type %s" (CicPp.ppterm s)
-                                           (CicPp.ppterm sort1))))
-            ) ;
+               | C.Sort _ -> s',sort1
+               | 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
+                   match boh with
+                    | CoercGraph.SomeCoercion c -> 
+                       Cic.Appl [c;s'], coercion_tgt
+                  | CoercGraph.NoCoercion
+                  | CoercGraph.NotHandled _
+                  | CoercGraph.NotMetaClosed -> 
+                     raise (RefineFailure (lazy (sprintf
+                      "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1))))
+            in
             let context_for_t = ((Some (n,(C.Decl s')))::context) in 
             let metasenv',t = exp_impl metasenv' subst' context_for_t t in
             let t',type2,subst'',metasenv'',ugraph2 =
-              type_of_aux subst' metasenv' 
-                context_for_t t ugraph1
+              type_of_aux subst' metasenv' context_for_t t ugraph1
             in
               C.Lambda (n,s',t'),C.Prod (n,s',type2),
                 subst'',metasenv'',ugraph2
@@ -477,8 +490,16 @@ and type_of_aux' metasenv context t ugraph =
                 ) tl ([],subst',metasenv',ugraph1)
             in
             let tl',applty,subst''',metasenv''',ugraph3 =
+             try
               eat_prods true subst'' metasenv'' context 
                 hetype tlbody_and_type ugraph2
+             with
+              exn ->
+               enrich
+                (fun msg ->
+                  lazy ("The application " ^
+                   CicMetaSubst.ppterm_in_context subst'' t context ^
+                  " is not well typed:\n" ^ Lazy.force msg)) exn
             in
               C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
         | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
@@ -1094,7 +1115,17 @@ and type_of_aux' metasenv context t ugraph =
                        in
                        match coer with
                        | CoercGraph.NoCoercion 
-                       | CoercGraph.NotHandled _ -> raise exn
+                       | CoercGraph.NotHandled _ ->
+                          let msg e =
+                           lazy ("The term " ^
+                            CicMetaSubst.ppterm_in_context subst hete
+                             context ^ " has type " ^
+                            CicMetaSubst.ppterm_in_context subst hety
+                             context ^ " but is here used with type " ^
+                            CicMetaSubst.ppterm_in_context subst s context
+                             (* "\nReason: " ^ Lazy.force e*))
+                          in
+                           enrich msg exn
                        | CoercGraph.NotMetaClosed -> 
                            raise (Uncertain (lazy "Coercions on meta"))
                        | CoercGraph.SomeCoercion c -> 
@@ -1102,7 +1133,7 @@ and type_of_aux' metasenv context t ugraph =
                    in
                    let coerced_args,metasenv',subst',t',ugraph2 =
                      eat_prods metasenv subst context
-                      (CicSubstitution.subst arg t) ugraph1 tl
+                       (CicSubstitution.subst arg t) ugraph1 tl
                    in
                      arg::coerced_args,metasenv',subst',t',ugraph2
                | _ -> assert false