COERCIONS: tentative addition of an equivalence relation over coercion source

[helm.git] / components / cic_unification / cicRefine.ml

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 120fed3ebde9a4c3f2b8142e9ab651136fcb1f41..856c9a58622480d6f938cbeb0e8a25c1ce913473 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -78,8 +78,10 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn =
   match exn with
      RefineFailure msg -> RefineFailure (f msg)
    | Uncertain msg -> Uncertain (f msg)
+   | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
    | Sys.Break -> raise exn
-   | _ -> assert false in
+   | _ -> prerr_endline (Printexc.to_string exn); assert false 
+ in
  let loc =
   try
    Cic.CicHash.find localization_tbl t
@@ -422,7 +424,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                exn ->
                 enrich localization_tbl te'
                  ~f:(fun _ ->
-                   lazy ("The term " ^
+                   lazy ("(3)The term " ^
                     CicMetaSubst.ppterm_in_context metasenv'' subst'' te'
                      context ^ " has type " ^
                     CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty
@@ -452,10 +454,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     in
                     (match boh with
                     | CoercGraph.NoCoercion
+                    | CoercGraph.SomeCoercionToTgt _
                     | CoercGraph.NotHandled _ ->
                        enrich localization_tbl t
                         (RefineFailure 
-                          (lazy ("The term " ^ 
+                          (lazy ("(4)The term " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ 
                           " is not a type since it has type " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv
@@ -463,7 +466,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     | CoercGraph.NotMetaClosed -> 
                        enrich localization_tbl t
                         (Uncertain 
-                          (lazy ("The term " ^ 
+                          (lazy ("(5)The term " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ 
                           " is not a type since it has type " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv
@@ -479,7 +482,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                         | None -> 
                             enrich localization_tbl t
                               (RefineFailure 
-                                (lazy ("The term " ^ 
+                                (lazy ("(6)The term " ^ 
                                 CicMetaSubst.ppterm_in_context ~metasenv
                                   subst t context ^ 
                                   " is not a type since it has type " ^ 
@@ -524,10 +527,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                      in
                       match boh with
                       | CoercGraph.NoCoercion
+                      | CoercGraph.SomeCoercionToTgt _
                       |  CoercGraph.NotHandled _ ->
                         enrich localization_tbl s'
                          (RefineFailure 
-                          (lazy ("The term " ^ 
+                          (lazy ("(7)The term " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ 
                           " is not a type since it has type " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv
@@ -535,7 +539,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                       | CoercGraph.NotMetaClosed -> 
                         enrich localization_tbl s'
                          (Uncertain 
-                          (lazy ("The term " ^ 
+                          (lazy ("(8)The term " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ 
                           " is not a type since it has type " ^ 
                           CicMetaSubst.ppterm_in_context ~metasenv 
@@ -551,7 +555,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                         | None -> 
                            enrich localization_tbl s'
                             (RefineFailure 
-                             (lazy ("The term " ^ 
+                             (lazy ("(9)The term " ^ 
                               CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ 
                               " is not a type since it has type " ^ 
                               CicMetaSubst.ppterm_in_context ~metasenv
@@ -681,9 +685,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                expected_type' actual_type ugraph2
             with
              exn ->
+               prerr_endline (CicMetaSubst.ppmetasenv subst metasenv);
+               prerr_endline (CicMetaSubst.ppsubst subst ~metasenv);
               enrich localization_tbl term' exn
                ~f:(function _ ->
-                 lazy ("The term " ^
+                 lazy ("(10)The term " ^
                   CicMetaSubst.ppterm_in_context ~metasenv subst term'
                    context ^ " has type " ^
                   CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
@@ -728,7 +734,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     exn ->
                      enrich localization_tbl constructor'
                       ~f:(fun _ ->
-                        lazy ("The term " ^
+                        lazy ("(11)The term " ^
                          CicMetaSubst.ppterm_in_context metasenv subst p'
                           context ^ " has type " ^
                          CicMetaSubst.ppterm_in_context metasenv subst actual_type
@@ -916,7 +922,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                       exn ->
                        enrich localization_tbl p exn
                         ~f:(function _ ->
-                          lazy ("The term " ^
+                          lazy ("(12)The term " ^
                            CicMetaSubst.ppterm_in_context ~metasenv subst p
                             context ^ " has type " ^
                            CicMetaSubst.ppterm_in_context ~metasenv subst instance'
@@ -957,7 +963,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                      exn ->
                       enrich localization_tbl bo exn
                        ~f:(function _ ->
-                         lazy ("The term " ^
+                         lazy ("(13)The term " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
                            context' ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
@@ -1010,7 +1016,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                      exn ->
                       enrich localization_tbl bo exn
                        ~f:(function _ ->
-                         lazy ("The term " ^
+                         lazy ("(14)The term " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst bo
                            context' ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
@@ -1359,6 +1365,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
         | CoercGraph.NoCoercion 
         | CoercGraph.NotMetaClosed 
         | CoercGraph.NotHandled _ -> raise exn
+        | CoercGraph.SomeCoercionToTgt candidates
         | CoercGraph.SomeCoercion candidates ->
             match  
             HExtlib.list_findopt 
@@ -1443,10 +1450,11 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                     in
                     (match coer with
                     | CoercGraph.NoCoercion 
+                    | CoercGraph.SomeCoercionToTgt _
                     | CoercGraph.NotHandled _ ->
                         enrich localization_tbl hete exn
                          ~f:(fun _ ->
-                           (lazy ("The term " ^
+                           (lazy ("(15)The term " ^
                              CicMetaSubst.ppterm_in_context ~metasenv subst hete
                               context ^ " has type " ^
                              CicMetaSubst.ppterm_in_context ~metasenv subst hety
@@ -1456,7 +1464,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                     | CoercGraph.NotMetaClosed -> 
                         enrich localization_tbl hete exn
                          ~f:(fun _ ->
-                           (lazy ("The term " ^
+                           (lazy ("(16)The term " ^
                              CicMetaSubst.ppterm_in_context ~metasenv subst hete
                               context ^ " has type " ^
                              CicMetaSubst.ppterm_in_context ~metasenv subst hety
@@ -1492,7 +1500,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                         | None ->  
                            enrich localization_tbl hete
                             ~f:(fun _ ->
-                             (lazy ("The term " ^
+                             (lazy ("(1)The term " ^
                               CicMetaSubst.ppterm_in_context ~metasenv subst hete
                                context ^ " has type " ^
                               CicMetaSubst.ppterm_in_context ~metasenv subst hety
@@ -1502,7 +1510,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                   | exn ->
                      enrich localization_tbl hete
                       ~f:(fun _ ->
-                        (lazy ("The term " ^
+                        (lazy ("(2)The term " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst hete
                            context ^ " has type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst hety
@@ -1728,6 +1736,7 @@ let typecheck metasenv uri obj ~localization_tbl =
      let con_context =
       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
      (* second phase: we fix only the constructors *)
+     let saved_menv = metasenv in
      let metasenv,ugraph,tys =
       List.fold_right
        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
@@ -1740,7 +1749,7 @@ let typecheck metasenv uri obj ~localization_tbl =
              let ty',_,metasenv,ugraph =
               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
              let ty' = undebrujin uri typesno tys ty' in
-              metasenv,ugraph,(name,ty')::res
+              metasenv@saved_menv,ugraph,(name,ty')::res
            ) cl (metasenv,ugraph,[])
          in
           metasenv,ugraph,(name,b,ty,cl')::res