better error messages. sorts are compared using whd

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index eb7b136c28f3ba948c9048a5f247241614181499..05862d9dab7f63ed4616119766f456f2660a3b97 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -48,17 +48,19 @@ let exp_implicit metasenv context expty =
 
 let force_to_sort metasenv subst context t =
   match NCicReduction.whd ~subst context t with
-  | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) as t -> 
+  | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as t -> 
      metasenv, subst, t
-  | C.Meta (i,(_,lc)) as t ->
+  | C.Meta (i,(_,(C.Irl 0 | C.Ctx []))) -> 
+     metasenv, subst, C.Meta(i,(0,C.Irl 0))
+  | C.Meta (i,(_,lc)) ->
      let len = match lc with C.Irl len->len | C.Ctx l->List.length l in
-     let metasenv, subst, _ = 
+     let metasenv, subst, newmeta = 
        if len > 0 then
          NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1)) 
-       else metasenv, subst, 0
+       else metasenv, subst, i
      in
-     metasenv, subst, t
-  | C.Sort _ -> metasenv, subst, t 
+     metasenv, subst, C.Meta (newmeta,(0,C.Irl 0))
+  | C.Sort _ as t -> metasenv, subst, t 
   | _ -> assert false
 ;;
 
@@ -73,9 +75,9 @@ let sort_of_prod
    | C.Sort (C.Type u1), C.Sort (C.Type u2) ->
         metasenv, subst, C.Sort (C.Type (u1@u2)) 
    | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, t2
-   | C.Meta _, C.Sort _
-   | C.Meta _, C.Meta _
-   | C.Sort _, C.Meta  _ -> metasenv, subst, t2
+   | C.Meta _, C.Sort _ 
+   | C.Meta _, C.Meta (_,(_,_))
+   | C.Sort _, C.Meta (_,(_,_)) -> metasenv, subst, t2 
    | x, (C.Sort _ | C.Meta _) | _, x -> 
       let y, context, orig = 
         if x == t1 then s, context, orig_s 
@@ -96,10 +98,9 @@ let check_allowed_sort_elimination localise r orig =
    let rec aux metasenv subst context ind arity1 arity2 =
      (*D*)inside 'S'; try let rc = 
      let arity1 = NCicReduction.whd ~subst context arity1 in
-     pp (lazy(NCicPp.ppterm ~subst ~metasenv ~context arity1 ^ " ... " ^
-        NCicPp.ppterm ~subst ~metasenv ~context arity2 ^ "\nNEV:"^
-NCicPp.ppmetasenv ~subst metasenv
-));
+     pp (lazy(NCicPp.ppterm ~subst ~metasenv ~context arity1 ^ "   elimsto   " ^
+        NCicPp.ppterm ~subst ~metasenv ~context arity2 ^ "\nMENV:\n"^
+        NCicPp.ppmetasenv ~subst metasenv));
      match arity1 with
      | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) ->
         let metasenv, meta, _ = 
@@ -166,6 +167,7 @@ let rec typeof
     fun t as orig -> 
     (*D*)inside 'R'; try let rc = 
     pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t));
+    pp (lazy (NCicPp.ppmetasenv ~subst metasenv));
     let metasenv, subst, t, infty = 
     match t with
     | C.Rel n ->
@@ -307,6 +309,8 @@ let rec typeof
       NCicReduction.head_beta_reduce (C.Appl (outtype::arguments@[term]))
     | C.Match _ -> assert false
     in
+    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
+         NCicPp.ppterm ~metasenv ~subst ~context infty ));
       force_ty metasenv subst context orig t infty expty
     (*D*)in outside(); rc with exc -> outside (); raise exc
   in
@@ -323,7 +327,8 @@ and eat_prods localise metasenv subst context orig_he he ty_he args =
             typeof ~localise metasenv subst context arg (Some s) in
           let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in
           aux metasenv subst (arg :: args_so_far) t tl
-      | t ->
+      | C.Meta _
+      | C.Appl (C.Meta _ :: _) as t ->
           let metasenv, subst, arg, ty_arg = 
             typeof ~localise metasenv subst context arg None in
           let metasenv, meta, _ = 
@@ -339,13 +344,28 @@ and eat_prods localise metasenv subst context orig_he he ty_he args =
           let metasenv, subst = 
              try NCicUnification.unify metasenv subst context t flex_prod 
              with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
-              ("The term %s is here applied to %d arguments but expects " ^^
-              "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
-              (List.length args) (List.length args_so_far))) exc)
+              ("The term %s has an inferred type %s, but is applied to the" ^^
+               " argument %s of type %s")
+              (NCicPp.ppterm ~metasenv ~subst ~context he)
+              (NCicPp.ppterm ~metasenv ~subst ~context t)
+              (NCicPp.ppterm ~metasenv ~subst ~context arg)
+              (NCicPp.ppterm ~metasenv ~subst ~context ty_arg))) exc)
               (* XXX coerce to funclass *)
           in
           let meta = NCicSubstitution.subst ~avoid_beta_redexes:true arg meta in
           aux metasenv subst (arg :: args_so_far) meta tl
+      | C.Match (_,_,C.Meta _,_) 
+      | C.Match (_,_,C.Appl (C.Meta _ :: _),_) 
+      | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) ->
+          raise (Uncertain (lazy (localise orig_he, Printf.sprintf
+            ("The term %s is here applied to %d arguments but expects " ^^
+            "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
+            (List.length args) (List.length args_so_far))))
+      | _ ->
+          raise (RefineFailure (lazy (localise orig_he, Printf.sprintf
+            ("The term %s is here applied to %d arguments but expects " ^^
+            "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
+            (List.length args) (List.length args_so_far))))
   in
    aux metasenv subst [] ty_he args
   (*D*)in outside(); rc with exc -> outside (); raise exc