X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=27150461fb0038ba4c5e7d81f8ff0562d0dc2de3;hb=28ac70d3f475442cda4ef30e0e9c0e6d012b2527;hp=dc7cd2721b91d02ea0bb8dd31aacf536312654de;hpb=3a12950125e7a4a792546aacea40505f3cecae89;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index dc7cd2721..27150461f 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 _ -> () @@ -43,9 +50,9 @@ let type_of_aux' metasenv subst context term ugraph = (CicMetaSubst.ppterm subst term) (CicMetaSubst.ppterm [] term) (CicMetaSubst.ppcontext subst context) - (CicMetaSubst.ppmetasenv metasenv subst) + (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 @@ -284,7 +291,7 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph = with Uncertain _ | UnificationFailure _ -> -debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)); +debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j))); let metasenv, subst = CicMetaSubst.restrict subst [(n,j)] metasenv in @@ -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,11 +343,10 @@ 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"; + debug_print (lazy "siamo allo huge hack"); (* TODO huge hack!!!! * we keep on unifying/refining in the hope that * the problem will be eventually solved. @@ -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 @@ -651,13 +665,5 @@ let fo_unif_subst subst context metasenv t1 t2 ugraph = CicPp.ppterm ty_t2 with _ -> "MALFORMED") (CicMetaSubst.ppcontext subst context) - (CicMetaSubst.ppmetasenv metasenv subst) + (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)) -;; -