From e82e30cc9885f2acdf03801c637aaacfd8c81d71 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 Sep 2005 13:51:29 +0000 Subject: [PATCH] This commit (partially) removes a big source of inefficiency (at least for the select function and the rewrite tactic): CicUnification.UnificationFailure exceptions were enriched producing (in a very expensive way) a nice error message. However, the expensive error message is useful only when it must be shown to the user. Very often this is not the case. Thus I am now postponing the production of the error message, changing the type of the exception. NOTE: this kind of improvement can be applied everywhere in the code! At least it should be applied to functions that can normally fail (e.g. unification, refinement, convertibility, type checking, etc.) --- helm/ocaml/cic_disambiguation/disambiguate.ml | 4 +- helm/ocaml/cic_unification/cicRefine.ml | 71 ++++++++------- helm/ocaml/cic_unification/cicRefine.mli | 5 +- helm/ocaml/cic_unification/cicUnification.ml | 90 ++++++++++--------- helm/ocaml/cic_unification/cicUnification.mli | 9 +- helm/ocaml/paramodulation/inference.ml | 8 +- 6 files changed, 105 insertions(+), 82 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index b9aa8f844..11d195205 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -75,7 +75,7 @@ let refine_term metasenv context uri term ugraph = Uncertain,ugraph | CicRefine.RefineFailure msg -> debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppterm term) msg); + (CicPp.ppterm term) (CicRefine.explain_error msg)); Ko,ugraph let refine_obj metasenv context uri obj ugraph = @@ -91,7 +91,7 @@ let refine_obj metasenv context uri obj ugraph = Uncertain,ugraph | CicRefine.RefineFailure msg -> debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppobj obj) msg); + (CicPp.ppobj obj) (CicRefine.explain_error msg)); Ko,ugraph let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index e4b935089..a5221c229 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -25,7 +25,16 @@ open Printf -exception RefineFailure of string;; +type failure_msg = + Reason of string + | UnificationFailure of CicUnification.failure_msg + +let explain_error = + function + Reason msg -> msg + | UnificationFailure msg -> CicUnification.explain_error msg + +exception RefineFailure of failure_msg;; exception Uncertain of string;; exception AssertFailure of string;; @@ -35,7 +44,7 @@ let fo_unif_subst subst context metasenv t1 t2 ugraph = try CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph with - (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) + (CicUnification.UnificationFailure msg) -> raise (RefineFailure (UnificationFailure msg)) | (CicUnification.Uncertain msg) -> raise (Uncertain msg) ;; @@ -61,7 +70,7 @@ let rec type_of_constant uri ugraph = | C.CurrentProof (_,_,_,ty,_,_) -> ty,u | _ -> raise - (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri)) + (RefineFailure (Reason ("Unknown constant definition " ^ U.string_of_uri uri))) and type_of_variable uri ugraph = let module C = Cic in @@ -78,7 +87,7 @@ and type_of_variable uri ugraph = | _ -> raise (RefineFailure - ("Unknown variable definition " ^ UriManager.string_of_uri uri)) + (Reason ("Unknown variable definition " ^ UriManager.string_of_uri uri))) and type_of_mutual_inductive_defs uri i ugraph = let module C = Cic in @@ -97,7 +106,7 @@ and type_of_mutual_inductive_defs uri i ugraph = | _ -> raise (RefineFailure - ("Unknown mutual inductive definition " ^ U.string_of_uri uri)) + (Reason ("Unknown mutual inductive definition " ^ U.string_of_uri uri))) and type_of_mutual_inductive_constr uri i j ugraph = let module C = Cic in @@ -117,7 +126,7 @@ and type_of_mutual_inductive_constr uri i j ugraph = | _ -> raise (RefineFailure - ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) + (Reason ("Unkown mutual inductive definition " ^ U.string_of_uri uri))) (* type_of_aux' is just another name (with a different scope) for type_of_aux *) @@ -180,9 +189,9 @@ and type_of_aux' metasenv context t ugraph = (S.lift n bo) ugraph in t,ty,subst,metasenv,ugraph - | None -> raise (RefineFailure "Rel to hidden hypothesis") + | None -> raise (RefineFailure (Reason "Rel to hidden hypothesis")) with - _ -> raise (RefineFailure "Not a close term") + _ -> raise (RefineFailure (Reason "Not a close term")) ) | C.Var (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = @@ -237,7 +246,7 @@ and type_of_aux' metasenv context t ugraph = in C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 with - _ -> raise (RefineFailure "Cast")) + _ -> raise (RefineFailure (Reason "Cast"))) | C.Prod (name,s,t) -> let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph @@ -259,10 +268,10 @@ and type_of_aux' metasenv context t ugraph = C.Meta _ | C.Sort _ -> () | _ -> - raise (RefineFailure (sprintf + raise (RefineFailure (Reason (sprintf "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) - (CicPp.ppterm sort1))) + (CicPp.ppterm sort1)))) ) ; let t',type2,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' @@ -303,7 +312,7 @@ and type_of_aux' metasenv context t ugraph = hetype tlbody_and_type ugraph2 in C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3 - | C.Appl _ -> raise (RefineFailure "Appl: no arguments") + | C.Appl _ -> raise (RefineFailure (Reason "Appl: no arguments")) | C.Const (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = check_exp_named_subst subst metasenv context @@ -347,8 +356,8 @@ and type_of_aux' metasenv context t ugraph = | _ -> raise (RefineFailure - ("Unkown mutual inductive definition " ^ - U.string_of_uri uri)) + (Reason ("Unkown mutual inductive definition " ^ + U.string_of_uri uri))) in let rec count_prod t = match CicReduction.whd ~subst context t with @@ -706,7 +715,7 @@ and type_of_aux' metasenv context t ugraph = let subst',metasenv',ugraph' = (try fo_unif_subst subst context metasenv t ct ugraph - with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) + with e -> raise (RefineFailure (Reason (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))) in l @ [Some t],subst',metasenv',ugraph' | Some t,Some (_,C.Decl ct) -> @@ -717,23 +726,23 @@ and type_of_aux' metasenv context t ugraph = (try fo_unif_subst subst' context metasenv' inferredty ct ugraph1 - with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) + with e -> raise (RefineFailure (Reason (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))) in l @ [Some t'], subst'',metasenv'',ugraph2 | None, Some _ -> - raise (RefineFailure (sprintf + raise (RefineFailure (Reason (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) - (CicMetaSubst.ppcontext subst canonical_context))) + (CicMetaSubst.ppcontext subst canonical_context)))) ) ([],subst,metasenv,ugraph) l lifted_canonical_context with Invalid_argument _ -> raise (RefineFailure - (sprintf + (Reason (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))) + (CicMetaSubst.ppcontext subst canonical_context)))) and check_exp_named_subst metasubst metasenv context tl ugraph = let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph = @@ -747,13 +756,13 @@ and type_of_aux' metasenv context t ugraph = (match CicEnvironment.get_cooked_obj ~trust:false uri with Cic.Variable (_,Some bo,_,_) -> raise - (RefineFailure - "A variable with a body can not be explicit substituted") + (RefineFailure (Reason + "A variable with a body can not be explicit substituted")) | Cic.Variable (_,None,_,_) -> () | _ -> raise - (RefineFailure - ("Unkown variable definition " ^ UriManager.string_of_uri uri)) + (RefineFailure (Reason + ("Unkown variable definition " ^ UriManager.string_of_uri uri))) ) ; *) let t',typeoft,metasubst',metasenv',ugraph2 = @@ -764,11 +773,11 @@ and type_of_aux' metasenv context t ugraph = fo_unif_subst metasubst' context metasenv' typeoft typeofvar ugraph2 with _ -> - raise (RefineFailure + raise (RefineFailure (Reason ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^ " not unifiable with " ^ - CicMetaSubst.ppterm metasubst' typeofvar)) + CicMetaSubst.ppterm metasubst' typeofvar))) in (* FIXME: no mere tail recursive! *) let exp_name_subst, metasubst''', metasenv''', ugraph4 = @@ -812,10 +821,10 @@ and type_of_aux' metasenv context t ugraph = in t2'',subst,metasenv,ugraph1 | (_,_) -> - raise (RefineFailure (sprintf + raise (RefineFailure (Reason (sprintf "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)" (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) - (CicPp.ppterm t2''))) + (CicPp.ppterm t2'')))) and eat_prods subst metasenv context hetype tlbody_and_type ugraph = let rec mk_prod metasenv context = @@ -961,7 +970,7 @@ let type_of_aux' metasenv context term ugraph = try type_of_aux' metasenv context term ugraph with - CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg) + CicUniv.UniverseInconsistency msg -> raise (RefineFailure (Reason msg)) (*CSC: this is a very very rough approximation; to be finished *) let are_all_occurrences_positive uri = @@ -971,7 +980,7 @@ let are_all_occurrences_positive uri = Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> () | Cic.MutInd (uri',_,_) when uri = uri' -> () | Cic.Prod (_,_,t) -> aux t - | _ -> raise (RefineFailure "not well formed constructor type") + | _ -> raise (RefineFailure (Reason "not well formed constructor type")) in aux @@ -1000,7 +1009,7 @@ let typecheck metasenv uri obj = (* instead of raising Uncertain, let's hope that the meta will become a sort *) | Cic.Meta _ -> () - | _ -> raise (RefineFailure "The term provided is not a type") + | _ -> raise (RefineFailure (Reason "The term provided is not a type")) end; let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in let bo' = CicMetaSubst.apply_subst subst bo' in diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli index 2e132c043..24a6c276f 100644 --- a/helm/ocaml/cic_unification/cicRefine.mli +++ b/helm/ocaml/cic_unification/cicRefine.mli @@ -23,10 +23,13 @@ * http://cs.unibo.it/helm/. *) -exception RefineFailure of string;; +type failure_msg +exception RefineFailure of failure_msg;; exception Uncertain of string;; exception AssertFailure of string;; +val explain_error: failure_msg -> string + (* type_of_aux' metasenv context term graph *) (* refines [term] and returns the refined form of [term], *) (* its type, the new metasenv and universe graph. *) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 8ae284483..fe5ae7650 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -25,9 +25,16 @@ open Printf -exception UnificationFailure of string;; +type failure_msg = + Reason of string + | Enriched of string * Cic.substitution * Cic.context * Cic.metasenv * + Cic.term * Cic.term * CicUniv.universe_graph + +let failure_msg_of_string msg = Reason msg + +exception UnificationFailure of failure_msg;; exception Uncertain of string;; -exception AssertFailure of string;; +exception AssertFailure of failure_msg;; let debug_print = fun _ -> () @@ -45,7 +52,7 @@ let type_of_aux' metasenv subst context term ugraph = (CicMetaSubst.ppcontext subst context) (CicMetaSubst.ppmetasenv subst metasenv) (CicMetaSubst.ppsubst subst) msg) in - raise (AssertFailure msg);; + raise (AssertFailure (Reason msg));; let exists_a_meta l = List.exists (function Cic.Meta _ -> true | _ -> false) l @@ -293,7 +300,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin with Exit -> raise - (UnificationFailure "1") + (UnificationFailure (Reason "1")) (* (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." @@ -301,7 +308,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin (CicMetaSubst.ppterm subst t2))) *) | Invalid_argument _ -> raise - (UnificationFailure "2")) + (UnificationFailure (Reason "2"))) (* (sprintf "Error trying to unify %s with %s: the lengths of the two local contexts do not match." @@ -336,9 +343,8 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin test_equality_only subst context metasenv tyt (S.subst_meta l meta_type) ugraph1 with - UnificationFailure msg - | Uncertain msg -> - (* debug_print msg; *)raise (UnificationFailure msg) + UnificationFailure msg ->raise (UnificationFailure msg) + | Uncertain msg -> raise (UnificationFailure (Reason msg)) | AssertFailure _ -> debug_print "siamo allo huge hack"; (* TODO huge hack!!!! @@ -354,7 +360,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin CicMetaSubst.delift n subst context metasenv l t with (CicMetaSubst.MetaSubstFailure msg)-> - raise (UnificationFailure msg) + raise (UnificationFailure (Reason msg)) | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) in let t'',ugraph2 = @@ -388,7 +394,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph else - raise (UnificationFailure "3") + raise (UnificationFailure (Reason "3")) (* (sprintf "Can't unify %s with %s due to different constants" (CicMetaSubst.ppterm subst t1) @@ -399,7 +405,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph else - raise (UnificationFailure "4") + raise (UnificationFailure (Reason "4")) (* (sprintf "Can't unify %s with %s due to different inductive principles" (CicMetaSubst.ppterm subst t1) @@ -411,7 +417,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph else - raise (UnificationFailure "5") + raise (UnificationFailure (Reason "5")) (* (sprintf "Can't unify %s with %s due to different inductive constructors" (CicMetaSubst.ppterm subst t1) @@ -449,7 +455,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin test_equality_only subst context metasenv t1 t2 ugraph) (subst,metasenv,ugraph) l1 l2 with (Invalid_argument msg) -> - raise (UnificationFailure msg)) + raise (UnificationFailure (Reason msg))) | C.Meta (i,l)::args, _ when not(exists_a_meta args) -> (* we verify that none of the args is a Meta, since beta expanding with respoect to a metavariable @@ -526,7 +532,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin ) (subst'',metasenv'',ugraph2) pl1 pl2 with Invalid_argument _ -> - raise (UnificationFailure "6")) + raise (UnificationFailure (Reason "6"))) (* (sprintf "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) @@ -535,7 +541,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin if t1 = t2 then subst, metasenv,ugraph else - raise (UnificationFailure "6") + raise (UnificationFailure (Reason "6")) (* (sprintf "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) @@ -570,17 +576,17 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin subst, metasenv, ugraph1 else raise (* (UnificationFailure "7") *) - (UnificationFailure (sprintf + (UnificationFailure (Reason (sprintf "7: Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2))) + (CicMetaSubst.ppterm subst t2)))) | (C.Prod _, t2) -> let t2' = R.whd ~subst context t2 in (match t2' with C.Prod _ -> fo_unif_subst test_equality_only subst context metasenv t1 t2' ugraph - | _ -> raise (UnificationFailure "8")) + | _ -> raise (UnificationFailure (Reason "8"))) | (t1, C.Prod _) -> let t1' = R.whd ~subst context t1 in (match t1' with @@ -589,22 +595,16 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin subst context metasenv t1' t2 ugraph | _ -> (* raise (UnificationFailure "9")) *) raise - (UnificationFailure (sprintf + (UnificationFailure (Reason (sprintf "9: Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) + (CicMetaSubst.ppterm subst t2))))) | (_,_) -> - let b,ugraph1 = - R.are_convertible ~subst ~metasenv context t1 t2 ugraph - in - if b then - subst, metasenv, ugraph1 - else - raise (UnificationFailure "10") - (* (sprintf - "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2))) *) + raise (UnificationFailure (Reason "10")) + (* (sprintf + "Can't unify %s with %s because they are not convertible" + (CicMetaSubst.ppterm subst t1) + (CicMetaSubst.ppterm subst t2))) *) and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph @@ -624,8 +624,8 @@ and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv 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))) + raise (UnificationFailure (Reason (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. *) @@ -638,7 +638,21 @@ let fo_unif metasenv context t1 t2 ugraph = fo_unif_subst false [] context metasenv t1 t2 ugraph ;; let fo_unif_subst subst context metasenv t1 t2 ugraph = - let enrich_msg msg = (* "bella roba" *) + try + fo_unif_subst false subst context metasenv t1 t2 ugraph + with + | AssertFailure (Enriched _ as msg) -> assert false + | AssertFailure (Reason msg) -> + raise (AssertFailure (Enriched (msg,subst,context,metasenv,t1,t2,ugraph))) + | UnificationFailure (Enriched _ as msg) -> assert false + | UnificationFailure (Reason msg) -> + raise (UnificationFailure (Enriched (msg,subst,context,metasenv,t1,t2,ugraph))) +;; + +let explain_error = + function + Reason msg -> msg + | Enriched (msg,subst,context,metasenv,t1,t2,ugraph) -> sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s" (CicMetaSubst.ppterm subst t1) (try @@ -653,11 +667,3 @@ let fo_unif_subst subst context metasenv t1 t2 ugraph = (CicMetaSubst.ppcontext subst context) (CicMetaSubst.ppmetasenv subst metasenv) (CicMetaSubst.ppsubst subst) msg - in - try - fo_unif_subst false subst context metasenv t1 t2 ugraph - with - | AssertFailure msg -> raise (AssertFailure (enrich_msg msg)) - | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg)) -;; - diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli index 2c8e12f60..5887f004d 100644 --- a/helm/ocaml/cic_unification/cicUnification.mli +++ b/helm/ocaml/cic_unification/cicUnification.mli @@ -23,9 +23,14 @@ * http://cs.unibo.it/helm/. *) -exception UnificationFailure of string;; +type failure_msg + +exception UnificationFailure of failure_msg;; exception Uncertain of string;; -exception AssertFailure of string;; +exception AssertFailure of failure_msg;; + +val failure_msg_of_string: string -> failure_msg +val explain_error: failure_msg -> string (* fo_unif metasenv context t1 t2 *) (* unifies [t1] and [t2] in a context [context]. *) diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 969d412ce..5ccd87412 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -480,7 +480,7 @@ let unification_simple metasenv context t1 t2 ugraph = | C.Meta (i, _), C.Meta (j, _) when i > j -> unif subst menv t s | C.Meta _, t when occurs_check subst s t -> - raise (U.UnificationFailure "Inference.unification.unif") + raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif")) | C.Meta (i, l), t -> ( try let _, _, ty = CicUtil.lookup_meta i menv in @@ -500,16 +500,16 @@ let unification_simple metasenv context t1 t2 ugraph = ) | _, C.Meta _ -> unif subst menv t s | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> - raise (U.UnificationFailure "Inference.unification.unif") + raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif")) | C.Appl (hds::tls), C.Appl (hdt::tlt) -> ( try List.fold_left2 (fun (subst', menv) s t -> unif subst' menv s t) (subst, menv) tls tlt with Invalid_argument _ -> - raise (U.UnificationFailure "Inference.unification.unif") + raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif")) ) - | _, _ -> raise (U.UnificationFailure "Inference.unification.unif") + | _, _ -> raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif")) in let subst, menv = unif [] metasenv t1 t2 in let menv = -- 2.39.2