From cb8646f6ae9bcbf19188f05a45059304ca8d5431 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 6 Nov 2008 14:05:33 +0000 Subject: [PATCH] better error messages. sorts are compared using whd --- .../components/ng_refiner/nCicRefiner.ml | 26 +++++++++++++++---- 1 file changed, 21 insertions(+), 5 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 2dce2a4a7..05862d9da 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -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 ;; @@ -327,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, _ = @@ -343,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 -- 2.39.2