X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=d8a078997a04ca3e9a1d8de75db88d4da96b90e2;hb=07151480b04db0ef4e77d09a5b7559ae5ab25ab4;hp=5e2eaba0046fca7544454395852a995acc258ca6;hpb=5530db2f72548a8c579ae5f9868cbd38290eb065;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 5e2eaba00..d8a078997 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,36 +50,13 @@ 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 -let rec beta_reduce = - function - (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> - let he'' = CicSubstitution.subst he' t in - if tl' = [] then - he'' - else - beta_reduce (Cic.Appl(he''::tl')) - | t -> t -(* -let rec deref subst = - let snd (_,a,_) = a in - function - Cic.Meta(n,l) as t -> - (try - deref subst - (CicSubstitution.subst_meta - l (snd (CicUtil.lookup_subst n subst))) - with - CicUtil.Subst_not_found _ -> t) - | t -> t -;; *) - let rec deref subst t = let snd (_,a,_) = a in match t with @@ -86,13 +70,44 @@ let rec deref subst t = | Cic.Appl(Cic.Meta(n,l)::args) -> (match deref subst (Cic.Meta(n,l)) with | Cic.Lambda _ as t -> - deref subst (beta_reduce (Cic.Appl(t::args))) + deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args))) | r -> Cic.Appl(r::args)) | Cic.Appl(((Cic.Lambda _) as t)::args) -> - deref subst (beta_reduce (Cic.Appl(t::args))) + deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args))) | t -> t ;; +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 @@ -236,10 +251,11 @@ 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 and beta_expand_many test_equality_only metasenv subst context t args ugraph = @@ -307,7 +323,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 @@ -316,7 +332,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." @@ -324,7 +340,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." @@ -359,11 +375,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. @@ -377,7 +392,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 = @@ -411,7 +426,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) @@ -422,7 +437,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) @@ -434,7 +449,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) @@ -472,7 +487,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 @@ -481,7 +496,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin (try let (_,t,_) = CicUtil.lookup_subst i subst in let lifted = S.subst_meta l t in - let reduced = beta_reduce (Cic.Appl (lifted::args)) in + let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in fo_unif_subst test_equality_only subst context metasenv reduced t2 ugraph @@ -496,7 +511,7 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin (* (try let (_,t,_) = CicUtil.lookup_subst i subst in let lifted = S.subst_meta l t in - let reduced = beta_reduce (Cic.Appl (lifted::args)) in + let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in fo_unif_subst test_equality_only subst context metasenv t1 reduced ugraph @@ -549,7 +564,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) @@ -558,11 +573,25 @@ 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) (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 + test_equality_only metasenv subst context t2 args ugraph + in + fo_unif_subst test_equality_only subst context metasenv + (C.Meta (i,l)) beta_expanded ugraph1 + | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) -> + let subst,metasenv,beta_expanded,ugraph1 = + beta_expand_many + test_equality_only metasenv subst context t1 args ugraph + in + fo_unif_subst test_equality_only subst context metasenv + beta_expanded (C.Meta (i,l)) ugraph1 | (C.Sort _ ,_) | (_, C.Sort _) | (C.Const _, _) | (_, C.Const _) | (C.MutInd _, _) | (_, C.MutInd _) @@ -579,31 +608,17 @@ debug_print ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (strin subst, metasenv, ugraph1 else raise (* (UnificationFailure "7") *) - (UnificationFailure (sprintf - "Can't unify %s with %s because they are not convertible" + (UnificationFailure (Reason (sprintf + "7: Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) - (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 - test_equality_only metasenv subst context t2 args ugraph - in - fo_unif_subst test_equality_only subst context metasenv - (C.Meta (i,l)) beta_expanded ugraph1 - | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) -> - let subst,metasenv,beta_expanded,ugraph1 = - beta_expand_many - test_equality_only metasenv subst context t1 args ugraph - in - fo_unif_subst test_equality_only subst context metasenv - beta_expanded (C.Meta (i,l)) ugraph1 + (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 @@ -612,22 +627,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 - "Can't unify %s with %s because they are not convertible" + (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 @@ -647,8 +656,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. *) @@ -661,7 +670,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 @@ -674,13 +697,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)) -;; -