X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=9db77c5d526200246379772cd0a9a1d8cf78c67a;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=d8a078997a04ca3e9a1d8de75db88d4da96b90e2;hpb=62de5609df6dd2138e0e998e4b5956ced8924a0a;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index d8a078997..9db77c5d5 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -25,25 +25,26 @@ open Printf -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 failure_msg;; +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'" +let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand" +let profiler_deref = HExtlib.profile "fo_unif_subst.deref'" +let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible" + let type_of_aux' metasenv subst context term ugraph = +let foo () = try CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph with CicTypeChecker.TypeCheckerFailure msg -> let msg = + lazy (sprintf "Kernel Type checking error: %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." @@ -51,8 +52,21 @@ let type_of_aux' metasenv subst context term ugraph = (CicMetaSubst.ppterm [] term) (CicMetaSubst.ppcontext subst context) (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst subst) msg) in - raise (AssertFailure (Reason msg));; + (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in + raise (AssertFailure msg) + | CicTypeChecker.AssertFailure msg -> + let msg = lazy + (sprintf + "Kernel Type checking assertion failure: +%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." + (CicMetaSubst.ppterm subst term) + (CicMetaSubst.ppterm [] term) + (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppmetasenv subst metasenv) + (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in + raise (AssertFailure msg) +in profiler_toa.HExtlib.profile foo () +;; let exists_a_meta l = List.exists (function Cic.Meta _ -> true | _ -> false) l @@ -77,6 +91,10 @@ let rec deref subst t = | t -> t ;; +let deref subst t = + let foo () = deref subst t + in profiler_deref.HExtlib.profile foo () + exception WrongShape;; let eta_reduce after_beta_expansion after_beta_expansion_body before_beta_expansion @@ -112,6 +130,7 @@ let eta_reduce after_beta_expansion after_beta_expansion_body let rec beta_expand test_equality_only metasenv subst context t arg ugraph = let module S = CicSubstitution in let module C = Cic in +let foo () = let rec aux metasenv subst n context t' ugraph = try @@ -256,6 +275,7 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph = let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in subst, metasenv, t'', ugraph2 +in profiler_beta_expand.HExtlib.profile foo () and beta_expand_many test_equality_only metasenv subst context t args ugraph = @@ -288,7 +308,9 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph = let t1 = deref subst t1 in let t2 = deref subst t2 in let b,ugraph = +let foo () = R.are_convertible ~subst ~metasenv context t1 t2 ugraph +in profiler_are_convertible.HExtlib.profile foo () in if b then subst, metasenv, ugraph @@ -332,7 +354,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ with Exit -> raise - (UnificationFailure (Reason "1")) + (UnificationFailure (lazy "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." @@ -340,7 +362,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (CicMetaSubst.ppterm subst t2))) *) | Invalid_argument _ -> raise - (UnificationFailure (Reason "2"))) + (UnificationFailure (lazy "2"))) (* (sprintf "Error trying to unify %s with %s: the lengths of the two local contexts do not match." @@ -375,8 +397,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ test_equality_only subst context metasenv tyt (S.subst_meta l meta_type) ugraph1 with - UnificationFailure msg ->raise (UnificationFailure msg) - | Uncertain msg -> raise (UnificationFailure (Reason msg)) + UnificationFailure _ as e -> raise e + | Uncertain msg -> raise (UnificationFailure msg) | AssertFailure _ -> debug_print (lazy "siamo allo huge hack"); (* TODO huge hack!!!! @@ -392,7 +414,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ CicMetaSubst.delift n subst context metasenv l t with (CicMetaSubst.MetaSubstFailure msg)-> - raise (UnificationFailure (Reason msg)) + raise (UnificationFailure msg) | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) in let t'',ugraph2 = @@ -426,18 +448,18 @@ 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 (Reason "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 test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph else - raise (UnificationFailure (Reason "4")) + raise (UnificationFailure (lazy "4")) (* (sprintf "Can't unify %s with %s due to different inductive principles" (CicMetaSubst.ppterm subst t1) @@ -449,7 +471,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph else - raise (UnificationFailure (Reason "5")) + raise (UnificationFailure (lazy "5")) (* (sprintf "Can't unify %s with %s due to different inductive constructors" (CicMetaSubst.ppterm subst t1) @@ -487,7 +509,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ test_equality_only subst context metasenv t1 t2 ugraph) (subst,metasenv,ugraph) l1 l2 with (Invalid_argument msg) -> - raise (UnificationFailure (Reason msg))) + raise (UnificationFailure (lazy 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 @@ -564,7 +586,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ ) (subst'',metasenv'',ugraph2) pl1 pl2 with Invalid_argument _ -> - raise (UnificationFailure (Reason "6"))) + raise (UnificationFailure (lazy "6.1"))) (* (sprintf "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) @@ -573,11 +595,11 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ if t1 = t2 then subst, metasenv,ugraph else - raise (UnificationFailure (Reason "6")) - (* (sprintf + raise (UnificationFailure (lazy + (sprintf "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2))) *) + (CicMetaSubst.ppterm subst t2)))) | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) -> let subst,metasenv,beta_expanded,ugraph1 = beta_expand_many @@ -607,9 +629,9 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ if b then subst, metasenv, ugraph1 else - raise (* (UnificationFailure "7") *) - (UnificationFailure (Reason (sprintf - "7: Can't unify %s with %s because they are not convertible" + raise + (UnificationFailure (lazy (sprintf + "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))) | (C.Prod _, t2) -> @@ -618,7 +640,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ C.Prod _ -> fo_unif_subst test_equality_only subst context metasenv t1 t2' ugraph - | _ -> raise (UnificationFailure (Reason "8"))) + | _ -> raise (UnificationFailure (lazy "8"))) | (t1, C.Prod _) -> let t1' = R.whd ~subst context t1 in (match t1' with @@ -627,12 +649,12 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ subst context metasenv t1' t2 ugraph | _ -> (* raise (UnificationFailure "9")) *) raise - (UnificationFailure (Reason (sprintf - "9: Can't unify %s with %s because they are not convertible" + (UnificationFailure (lazy (sprintf + "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))) | (_,_) -> - raise (UnificationFailure (Reason "10")) + raise (UnificationFailure (lazy "10")) (* (sprintf "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) @@ -656,7 +678,7 @@ 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 (Reason (sprintf + raise (UnificationFailure (lazy (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 *) @@ -669,33 +691,58 @@ and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv 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 ( + 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 + | 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 + | 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) + (Lazy.force msg) + ) + let fo_unif_subst subst context metasenv t1 t2 ugraph = 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))) + | AssertFailure msg -> + raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph)) + | UnificationFailure msg -> + raise (UnificationFailure (enrich_msg 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 - let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in - CicPp.ppterm ty_t1 - with _ -> "MALFORMED") - (CicMetaSubst.ppterm subst t2) - (try - let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in - CicPp.ppterm ty_t2 - with _ -> "MALFORMED") - (CicMetaSubst.ppcontext subst context) - (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst subst) msg