From: Claudio Sacerdoti Coen Date: Tue, 2 Mar 2004 17:30:06 +0000 (+0000) Subject: - Improved error messaging. X-Git-Tag: v0_0_4~53 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ccbdc83d7eaa5c06d89a8a863e310ddaf87d48c1;p=helm.git - Improved error messaging. - Invalid_argument was raised by List.fold_left2 ;-( I want checked excecptions! --- diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 83daf60a6..e7b0e3661 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -593,7 +593,7 @@ let delift n subst context metasenv l t = (* order (in the sense of alpha-conversion). See comment above *) (* related to the delift function. *) debug_print "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ; -debug_print "\nCicMetaSubst: UNCERTAIN" ; +print_string "\nCicMetaSubst: UNCERTAIN" ; raise (Uncertain (sprintf "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" (ppterm subst t) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 55781422c..d33230eb0 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -403,6 +403,7 @@ and type_of_aux' metasenv context t = in aux 1 canonical_context in + try List.fold_left2 (fun (subst,metasenv) t ct -> match (t,ct) with @@ -426,6 +427,14 @@ and type_of_aux' metasenv context t = (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))) ) (subst,metasenv) l lifted_canonical_context + with + Invalid_argument _ -> + raise + (NotRefinable + (sprintf + "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s" + (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) + (CicMetaSubst.ppcontext subst canonical_context))) and check_exp_named_subst metasubst metasenv context = let rec check_exp_named_subst_aux metasubst metasenv substs = @@ -533,14 +542,20 @@ and type_of_aux' metasenv context t = | (hete, hety)::tl -> (match hetype with Cic.Prod (n,s,t) -> +(* (try +*) let subst,metasenv = CicUnification.fo_unif_subst subst context metasenv s hety in eat_prods metasenv subst context (CicMetaSubst.subst subst hete t) tl - with - e -> raise (RefineFailure ("XXX " ^ Printexc.to_string e))) +(* + with + e -> + raise + (RefineFailure ("XXX " ^ Printexc.to_string e))) +*) | _ -> assert false ) in diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index fb1ca113f..37f8621c8 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -59,6 +59,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 = match (t1, t2) with (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> let ok,subst,metasenv = + try List.fold_left2 (fun (b,subst,metasenv) t1 t2 -> if b then true,subst,metasenv else @@ -80,13 +81,17 @@ let rec fo_unif_subst subst context metasenv t1 t2 = with Not_found -> false,subst,metasenv) ) (true,subst,metasenv) ln lm + with + Invalid_argument _ -> + raise (UnificationFailure (sprintf + "Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) in if ok then subst,metasenv else raise (UnificationFailure (sprintf "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted." - (CicPp.ppterm t1) (CicPp.ppterm t2))) + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm substt2))) | (C.Meta (n,l), C.Meta (m,_)) when n>m -> fo_unif_subst subst context metasenv t2 t1 | (C.Meta (n,l), t) @@ -132,7 +137,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; else raise (UnificationFailure (sprintf "Can't unify %s with %s due to different constants" - (CicPp.ppterm t1) (CicPp.ppterm t2))) + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) -> if UriManager.eq uri1 uri2 && i1 = i2 then fo_unif_subst_exp_named_subst subst context metasenv @@ -140,7 +145,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; else raise (UnificationFailure (sprintf "Can't unify %s with %s due to different inductive principles" - (CicPp.ppterm t1) (CicPp.ppterm t1))) + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) | C.MutConstruct (uri1,i1,j1,exp_named_subst1), C.MutConstruct (uri2,i2,j2,exp_named_subst2) -> if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then @@ -149,7 +154,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; else raise (UnificationFailure (sprintf "Can't unify %s with %s due to different inductive constructors" - (CicPp.ppterm t1) (CicPp.ppterm t1))) + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2 | (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te @@ -181,15 +186,20 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; fo_unif_l subst' metasenv' (l1,l2) in fo_unif_l subst metasenv (lr1, lr2) - | (C.MutCase (_,_,outt1,t1,pl1), C.MutCase (_,_,outt2,t2,pl2))-> + | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> let subst', metasenv' = fo_unif_subst subst context metasenv outt1 outt2 in let subst'',metasenv'' = - fo_unif_subst subst' context metasenv' t1 t2 in - List.fold_left2 - (function (subst,metasenv) -> - fo_unif_subst subst context metasenv - ) (subst'',metasenv'') pl1 pl2 + fo_unif_subst subst' context metasenv' t1' t2' in + (try + List.fold_left2 + (function (subst,metasenv) -> + fo_unif_subst subst context metasenv + ) (subst'',metasenv'') pl1 pl2 + with + Invalid_argument _ -> + raise (UnificationFailure (sprintf + "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))) | (C.Rel _, _) | (_, C.Rel _) | (C.Sort _ ,_) | (_, C.Sort _) | (C.Const _, _) | (_, C.Const _) @@ -202,29 +212,35 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; else raise (UnificationFailure (sprintf "Can't unify %s with %s because they are not convertible" - (CicPp.ppterm t1) (CicPp.ppterm t2))) + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) | (_,_) -> if R.are_convertible subst context t1 t2 then subst, metasenv else raise (UnificationFailure (sprintf "Can't unify %s with %s because they are not convertible" - (CicPp.ppterm t1) (CicPp.ppterm t2))) + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) and fo_unif_subst_exp_named_subst subst context metasenv exp_named_subst1 exp_named_subst2 = -try - List.fold_left2 - (fun (subst,metasenv) (uri1,t1) (uri2,t2) -> - assert (uri1=uri2) ; - fo_unif_subst subst context metasenv t1 t2 - ) (subst,metasenv) exp_named_subst1 exp_named_subst2 -with -e -> -let uri = UriManager.uri_of_string "cic:/dummy.var" in -debug_print ("@@@: " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst1)) ^ -" <==> " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst2))) ; raise e + try + List.fold_left2 + (fun (subst,metasenv) (uri1,t1) (uri2,t2) -> + assert (uri1=uri2) ; + fo_unif_subst subst context metasenv t1 t2 + ) (subst,metasenv) exp_named_subst1 exp_named_subst2 + with + Invalid_argument _ -> + let print_ens ens = + String.concat " ; " + (List.map + (fun (uri,t) -> + UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t) + ) ens) + in + raise (UnificationFailure (sprintf + "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2))) (* A substitution is a (int * Cic.term) list that associates a *) (* metavariable i with its body. *)