X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=a2a98bd0d8213739796d81de2492cb1446b4242d;hb=8b55faddb06e3c4b0a13839210bb49170939b33e;hp=27150461fb0038ba4c5e7d81f8ff0562d0dc2de3;hpb=a93a94942ad58d8645af1fd94bef8fa31d9541a4;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 27150461f..a2a98bd0d 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -25,25 +25,25 @@ 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 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 +51,10 @@ 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) +in profiler_toa.HExtlib.profile foo () +;; let exists_a_meta l = List.exists (function Cic.Meta _ -> true | _ -> false) l @@ -77,10 +79,46 @@ 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 + = + try + match before_beta_expansion,after_beta_expansion_body with + Cic.Appl l, Cic.Appl l' -> + let rec all_but_last check_last = + function + [] -> assert false + | [Cic.Rel 1] -> [] + | [_] -> if check_last then raise WrongShape else [] + | he::tl -> he::(all_but_last check_last tl) + in + let all_but_last check_last l = + match all_but_last check_last l with + [] -> assert false + | [he] -> he + | l -> Cic.Appl l + in + let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in + let all_but_last = all_but_last false l in + (* here we should test alpha-equivalence; however we know by + construction that here alpha_equivalence is equivalent to = *) + if t = all_but_last then + all_but_last + else + after_beta_expansion + | _,_ -> after_beta_expansion + with + WrongShape -> after_beta_expansion 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 @@ -220,10 +258,12 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph = let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in let fresh_name = FreshNamesGenerator.mk_fresh_name ~subst - metasenv context (Cic.Name "Heta") ~typ:argty + metasenv context (Cic.Name "Hbeta") ~typ:argty in let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in - subst, metasenv, C.Lambda (fresh_name,argty,t'), ugraph2 + 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 = @@ -256,7 +296,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 @@ -300,7 +342,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." @@ -308,7 +350,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." @@ -343,8 +385,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!!!! @@ -360,7 +402,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 = @@ -394,7 +436,7 @@ 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")) + raise (UnificationFailure (lazy "3")) (* (sprintf "Can't unify %s with %s due to different constants" (CicMetaSubst.ppterm subst t1) @@ -405,7 +447,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 "4")) + raise (UnificationFailure (lazy "4")) (* (sprintf "Can't unify %s with %s due to different inductive principles" (CicMetaSubst.ppterm subst t1) @@ -417,7 +459,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) @@ -455,7 +497,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 @@ -532,7 +574,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"))) (* (sprintf "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) @@ -541,7 +583,7 @@ 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")) + raise (UnificationFailure (lazy "6")) (* (sprintf "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) @@ -575,9 +617,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) -> @@ -586,7 +628,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 @@ -595,12 +637,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) @@ -624,7 +666,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 *) @@ -637,33 +679,29 @@ 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 + (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) (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