housekeeping:

[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 2dce2a4a70f0dad2de5ce0738c7f13b339043f41..479f95802059ce9db3a81034a4aac5e61681010f 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -40,7 +40,7 @@ let wrap_exc msg = function
 let exp_implicit metasenv context expty =
  let foo x = match expty with Some t -> `WithType t | None -> x in
  function      
-  | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Type)
+  | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
   | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
   | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
   | _ -> assert false
@@ -60,7 +60,7 @@ let force_to_sort metasenv subst context t =
        else metasenv, subst, i
      in
      metasenv, subst, C.Meta (newmeta,(0,C.Irl 0))
-  | C.Sort _ -> metasenv, subst, t 
+  | C.Sort _ as t -> metasenv, subst, t 
   | _ -> assert false
 ;;
 
@@ -307,7 +307,9 @@ let rec typeof
       metasenv, subst, 
       C.Match (r, outtype, term, List.rev pl_rev),
       NCicReduction.head_beta_reduce (C.Appl (outtype::arguments@[term]))
-    | C.Match _ -> assert false
+    | C.Match _ as orig -> 
+        prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context orig);
+        assert false
     in
     pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
          NCicPp.ppterm ~metasenv ~subst ~context infty ));
@@ -327,7 +329,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, _ = 
@@ -343,13 +346,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