X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=d1e010ca696558aefe36f8b2ec95f334634aea16;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=9a87bc51bba07e6493a4666ae494a0fdce006a45;hpb=fa40e1051d879aac77bd576d4a71d937a8d029a9;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 9a87bc51b..d1e010ca6 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -23,12 +23,15 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open Printf exception UnificationFailure of string Lazy.t;; exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; +let verbose = false;; let debug_print = fun _ -> () let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'" @@ -447,11 +450,11 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph else - raise (UnificationFailure (lazy "3")) - (* (sprintf + raise (UnificationFailure (lazy + (sprintf "Can't unify %s with %s due to different constants" (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2))) *) + (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 @@ -568,8 +571,58 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ fo_unif_l test_equality_only subst' metasenv' (l1,l2) ugraph1 in + (try fo_unif_l - test_equality_only subst metasenv (lr1, lr2) ugraph) + test_equality_only subst metasenv (lr1, lr2) ugraph + with + | UnificationFailure _ + | Uncertain _ as exn -> + (match l1, l2 with + | (((Cic.Const (uri1, ens1)) as c1) :: tl1), + (((Cic.Const (uri2, ens2)) as c2) :: tl2) when + CoercGraph.is_a_coercion c1 && + CoercGraph.is_a_coercion c2 -> + let body1, attrs1, ugraph = + match CicEnvironment.get_obj ugraph uri1 with + | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u + | _ -> assert false + in + let body2, attrs2, ugraph = + match CicEnvironment.get_obj ugraph uri2 with + | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u + | _ -> assert false + in + let is_composite1 = + List.exists ((=) (`Class `Coercion)) attrs1 in + let is_composite2 = + List.exists ((=) (`Class `Coercion)) attrs2 in + (match is_composite1, is_composite2 with + | false, false -> raise exn + | true, false -> + let body1 = CicSubstitution.subst_vars ens1 body1 in + let appl = Cic.Appl (body1::tl1) in + let redappl = CicReduction.head_beta_reduce appl in + fo_unif_subst + test_equality_only subst context metasenv + redappl t2 ugraph + | false, true -> + let body2 = CicSubstitution.subst_vars ens2 body2 in + let appl = Cic.Appl (body2::tl2) in + let redappl = CicReduction.head_beta_reduce appl in + fo_unif_subst + test_equality_only subst context metasenv + t1 redappl ugraph + | true, true -> + let body1 = CicSubstitution.subst_vars ens1 body1 in + let appl1 = Cic.Appl (body1::tl1) in + let redappl1 = CicReduction.head_beta_reduce appl1 in + let body2 = CicSubstitution.subst_vars ens2 body2 in + let appl2 = Cic.Appl (body2::tl2) in + let redappl2 = CicReduction.head_beta_reduce appl2 in + fo_unif_subst + test_equality_only subst context metasenv + redappl1 redappl2 ugraph) + | _ -> raise exn))) | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> let subst', metasenv',ugraph1 = fo_unif_subst test_equality_only subst context metasenv outt1 outt2 @@ -691,21 +744,50 @@ let fo_unif metasenv context t1 t2 ugraph = fo_unif_subst false [] context metasenv t1 t2 ugraph ;; let enrich_msg msg subst context metasenv t1 t2 ugraph = - lazy - (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" + lazy ( + if verbose then + sprintf "[Verbose] 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 let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in CicPp.ppterm ty_t1 - with _ -> "MALFORMED") + with + | UnificationFailure s + | Uncertain s + | AssertFailure s -> sprintf "MALFORMED(t1): \n%s\n" (Lazy.force s)) (CicMetaSubst.ppterm subst t2) (try let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in CicPp.ppterm ty_t2 - with _ -> "MALFORMED") + with + | UnificationFailure s + | Uncertain s + | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) + (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppmetasenv subst metasenv) + (CicMetaSubst.ppsubst subst) (Lazy.force msg) + else + sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s" + (CicMetaSubst.ppterm_in_context subst t1 context) + (try + let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in + CicMetaSubst.ppterm_in_context subst ty_t1 context + with + | UnificationFailure s + | Uncertain s + | AssertFailure s -> sprintf "MALFORMED(t1): \n%s\n" (Lazy.force s)) + (CicMetaSubst.ppterm_in_context subst t2 context) + (try + let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in + CicMetaSubst.ppterm_in_context subst ty_t2 context + with + | UnificationFailure s + | Uncertain s + | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) (CicMetaSubst.ppcontext subst context) (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst subst) (Lazy.force msg)) + (Lazy.force msg) + ) let fo_unif_subst subst context metasenv t1 t2 ugraph = try