Better (and more localized) error message for sort_of_prod.

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

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 0a6510b445ad1957681f60db8faf51b7ba18072d..be4014507355ab62e4d319fa115074b9aee1b552 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -395,8 +395,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                    subst', metasenv',ugraph1)
         | C.Sort (C.Type tno) -> 
             let tno' = CicUniv.fresh() in 
-            let ugraph1 = CicUniv.add_gt tno' tno ugraph in
-              t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+             (try
+               let ugraph1 = CicUniv.add_gt tno' tno ugraph in
+                 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
         | C.Sort _ -> 
             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
         | C.Implicit infos ->
@@ -502,8 +505,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               t' sort2 subst'' context_for_t metasenv'' ugraph2
             in
               let sop,subst''',metasenv''',ugraph3 =
-                sort_of_prod subst'' metasenv'' 
-                  context (name,s') (sort1,sort2) ugraph2
+                sort_of_prod localization_tbl subst'' metasenv'' 
+                  context (name,s') t' (sort1,sort2) ugraph2
               in
                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
         | C.Lambda (n,s,t) ->
@@ -1133,7 +1136,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
 
 
-  and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
+  and sort_of_prod localization_tbl subst metasenv context (name,s) t (t1, t2)
+   ugraph
+  =
     let module C = Cic in
     let context_for_t2 = (Some (name,C.Decl s))::context in
     let t1'' = CicReduction.whd ~subst context t1 in
@@ -1145,9 +1150,12 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
               C.Sort s2,subst,metasenv,ugraph
         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
             let t' = CicUniv.fresh() in 
-            let ugraph1 = CicUniv.add_ge t' t1 ugraph in
-            let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
-              C.Sort (C.Type t'),subst,metasenv,ugraph2
+             (try
+              let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+              let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+                C.Sort (C.Type t'),subst,metasenv,ugraph2
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
         | (C.Sort _,C.Sort (C.Type t1)) -> 
             C.Sort (C.Type t1),subst,metasenv,ugraph
         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
@@ -1166,15 +1174,23 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
              with _ -> assert false (* unification against a metavariable *)
             in
               t2'',subst,metasenv,ugraph1
+        | (C.Sort _,_)
+        | (C.Meta _,_) -> 
+            enrich localization_tbl s
+             (RefineFailure 
+               (lazy 
+                 (sprintf
+                   "%s is supposed to be a type, but its type is %s"
+               (CicMetaSubst.ppterm_in_context subst t context)
+               (CicMetaSubst.ppterm_in_context subst t2 context))))
         | _,_ -> 
-            raise 
-              (RefineFailure 
-                (lazy 
-                  (sprintf
-                    ("Two sorts were expected, found %s " ^^ 
-                     "(that reduces to %s) and %s (that reduces to %s)")
-                (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
-                (CicPp.ppterm t2''))))
+            enrich localization_tbl t
+             (RefineFailure 
+               (lazy 
+                 (sprintf
+                   "%s is supposed to be a type, but its type is %s"
+               (CicMetaSubst.ppterm_in_context subst s context)
+               (CicMetaSubst.ppterm_in_context subst t1 context))))
 
   and avoid_double_coercion context subst metasenv ugraph t ty = 
    if not !pack_coercions then
@@ -1809,6 +1825,31 @@ let pack_coercion metasenv ctx t =
   merge_coercions ctx t
 ;;
 
+let pack_coercion_metasenv conjectures =
+  let module C = Cic in
+  List.map 
+    (fun (i, ctx, ty) -> 
+       let ctx = 
+         List.fold_right 
+           (fun item ctx ->
+              let item' =
+                match item with
+                    Some (name, C.Decl t) -> 
+                      Some (name, C.Decl (pack_coercion conjectures ctx t))
+                  | Some (name, C.Def (t,None)) -> 
+                      Some (name,C.Def (pack_coercion conjectures ctx t,None))
+                  | Some (name, C.Def (t,Some ty)) -> 
+                      Some (name, C.Def (pack_coercion conjectures ctx t, 
+                                        Some (pack_coercion conjectures ctx ty)))
+                  | None -> None
+              in
+                item'::ctx
+           ) ctx []
+       in
+         ((i,ctx,pack_coercion conjectures ctx ty))
+    ) conjectures
+;;
+
 let pack_coercion_obj obj =
   let module C = Cic in
   match obj with
@@ -1829,29 +1870,7 @@ let pack_coercion_obj obj =
       let ty = pack_coercion [] [] ty in
         C.Variable (name, body, ty, params, attrs)
   | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
-      let conjectures = 
-        List.map 
-          (fun (i, ctx, ty) -> 
-            let ctx = 
-              List.fold_right 
-                (fun item ctx ->
-                  let item' =
-                   match item with
-                      Some (name, C.Decl t) -> 
-                        Some (name, C.Decl (pack_coercion conjectures ctx t))
-                    | Some (name, C.Def (t,None)) -> 
-                        Some (name,C.Def (pack_coercion conjectures ctx t,None))
-                    | Some (name, C.Def (t,Some ty)) -> 
-                        Some (name, C.Def (pack_coercion conjectures ctx t, 
-                                       Some (pack_coercion conjectures ctx ty)))
-                    | None -> None
-                  in
-                   item'::ctx
-                ) ctx []
-            in
-             ((i,ctx,pack_coercion conjectures ctx ty))
-          ) conjectures
-      in
+      let conjectures = pack_coercion_metasenv conjectures in
       let body = pack_coercion conjectures [] body in
       let ty = pack_coercion conjectures [] ty in
       C.CurrentProof (name, conjectures, body, ty, params, attrs)