X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=9db77c5d526200246379772cd0a9a1d8cf78c67a;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;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..9db77c5d5 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -25,27 +25,48 @@ open Printf -exception UnificationFailure of string;; -exception Uncertain of string;; -exception AssertFailure of string;; +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." (CicMetaSubst.ppterm subst term) (CicMetaSubst.ppterm [] term) (CicMetaSubst.ppcontext subst context) - (CicMetaSubst.ppmetasenv metasenv subst) - (CicMetaSubst.ppsubst subst) msg) in - raise (AssertFailure msg);; + (CicMetaSubst.ppmetasenv subst metasenv) + (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 @@ -70,10 +91,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 @@ -213,10 +270,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 = @@ -249,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 @@ -284,7 +345,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 +354,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin with Exit -> raise - (UnificationFailure "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." @@ -301,7 +362,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin (CicMetaSubst.ppterm subst t2))) *) | Invalid_argument _ -> raise - (UnificationFailure "2")) + (UnificationFailure (lazy "2"))) (* (sprintf "Error trying to unify %s with %s: the lengths of the two local contexts do not match." @@ -336,11 +397,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 _ as e -> raise e + | Uncertain msg -> raise (UnificationFailure 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. @@ -388,18 +448,18 @@ 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") - (* (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 "4") + raise (UnificationFailure (lazy "4")) (* (sprintf "Can't unify %s with %s due to different inductive principles" (CicMetaSubst.ppterm subst t1) @@ -411,7 +471,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 (lazy "5")) (* (sprintf "Can't unify %s with %s due to different inductive constructors" (CicMetaSubst.ppterm subst t1) @@ -449,7 +509,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 (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 @@ -526,7 +586,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 (lazy "6.1"))) (* (sprintf "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) @@ -535,11 +595,11 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin if t1 = t2 then subst, metasenv,ugraph else - raise (UnificationFailure "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 @@ -569,18 +629,18 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin if b then subst, metasenv, ugraph1 else - raise (* (UnificationFailure "7") *) - (UnificationFailure (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))) + (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 (lazy "8"))) | (t1, C.Prod _) -> let t1' = R.whd ~subst context t1 in (match t1' with @@ -589,22 +649,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 - "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)))) + (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 (lazy "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 +678,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 (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 *) (* metavariable i with its body. *) @@ -637,27 +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 = - let enrich_msg msg = (* "bella roba" *) - 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 metasenv subst) - (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)) + | 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)) ;; -