From c695e5adb3cb5492d412d933b1dd7901dc6676af Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 25 Jan 2018 17:46:00 +0100 Subject: [checker] Better error message for bad recursive trees --- checker/indtypes.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'checker') diff --git a/checker/indtypes.ml b/checker/indtypes.ml index bb0db8cfe..4de597766 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -502,10 +502,19 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc indlc in mk_paths (Mrec ind) irecargs +let prrecarg = function + | Norec -> str "Norec" + | Mrec (mind,i) -> + str "Mrec[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]" + | Imbr (mind,i) -> + str "Imbr[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]" + let check_subtree t1 t2 = let cmp_labels l1 l2 = l1 == Norec || eq_recarg l1 l2 in if not (Rtree.equiv eq_recarg cmp_labels t1 t2) - then failwith "bad recursive trees" + then user_err Pp.(str "Bad recursive tree: found " ++ fnl () + ++ Rtree.pp_tree prrecarg t1 ++ fnl () ++ str " when expected " ++ fnl () + ++ Rtree.pp_tree prrecarg t2) (* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*) let check_positivity env_ar mind params nrecp inds = -- cgit v1.2.3