X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=9db77c5d526200246379772cd0a9a1d8cf78c67a;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=25db7d9154b5a6e785a6d90cc4e20159bf631533;hpb=2468d0398195d41200bfd07db68fa675dc90b875;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 25db7d915..9db77c5d5 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -25,76 +25,112 @@ 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 debug_print = prerr_endline +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 = - (sprintf - "Kernel Type checking error: + 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 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 metasenv subst) - (CicMetaSubst.ppsubst subst) msg) in - raise (AssertFailure msg);; + (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 -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 Cic.Meta(n,l) -> - (try - deref subst - (CicSubstitution.subst_meta - l (snd (CicUtil.lookup_subst n subst))) - with - CicUtil.Subst_not_found _ -> t) + (try + deref subst + (CicSubstitution.subst_meta + l (snd (CicUtil.lookup_subst n subst))) + with + CicUtil.Subst_not_found _ -> 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))) - | r -> Cic.Appl(r::args)) + (match deref subst (Cic.Meta(n,l)) with + | Cic.Lambda _ as t -> + deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args))) + | r -> Cic.Appl(r::args)) + | Cic.Appl(((Cic.Lambda _) as t)::args) -> + deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args))) | 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 @@ -116,16 +152,16 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph = in subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1 | C.Meta (i,l) -> - (* andrea: in general, beta_expand can create badly typed + (* andrea: in general, beta_expand can create badly typed terms. This happens quite seldom in practice, UNLESS we iterate on the local context. For this reason, we renounce to iterate and just lift *) let l = - List.map - (function - Some t -> Some (CicSubstitution.lift 1 t) - | None -> None) l in - subst, metasenv, C.Meta (i,l), ugraph + List.map + (function + Some t -> Some (CicSubstitution.lift 1 t) + | None -> None) l in + subst, metasenv, C.Meta (i,l), ugraph | C.Sort _ | C.Implicit _ as t -> subst,metasenv,t,ugraph | C.Cast (te,ty) -> @@ -140,7 +176,7 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph = aux metasenv subst n context s ugraph in let subst,metasenv,t',ugraph2 = aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t - ugraph1 + ugraph1 in (* TASSI: sure this is in serial? *) subst,metasenv,(C.Prod (nn, s', t')),ugraph2 @@ -211,7 +247,7 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph = in C.Fix (i, substitutedfl) *) - subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph + subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph | C.CoFix (i,fl) -> (*CSC: not implemented let tylen = List.length fl in @@ -223,7 +259,7 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph = C.CoFix (i, substitutedfl) *) - subst,metasenv,(CicSubstitution.lift 1 t'), ugraph + subst,metasenv,(CicSubstitution.lift 1 t'), ugraph and aux_exp_named_subst metasenv subst n context ens ugraph = List.fold_right @@ -234,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 = @@ -245,9 +283,9 @@ and beta_expand_many test_equality_only metasenv subst context t args ugraph = List.fold_right (fun arg (subst,metasenv,t,ugraph) -> let subst,metasenv,t,ugraph1 = - beta_expand test_equality_only - metasenv subst context t arg ugraph - in + beta_expand test_equality_only + metasenv subst context t arg ugraph + in subst,metasenv,t,ugraph1 ) args (subst,metasenv,t,ugraph) in @@ -270,173 +308,174 @@ 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 else match (t1, t2) with | (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> - let _,subst,metasenv,ugraph1 = - (try + let _,subst,metasenv,ugraph1 = + (try List.fold_left2 - (fun (j,subst,metasenv,ugraph) t1 t2 -> - match t1,t2 with - None,_ - | _,None -> j+1,subst,metasenv,ugraph - | Some t1', Some t2' -> - (* First possibility: restriction *) - (* Second possibility: unification *) - (* Third possibility: convertibility *) - let b, ugraph1 = - R.are_convertible - ~subst ~metasenv context t1' t2' ugraph - in - if b then - j+1,subst,metasenv, ugraph1 - else - (try - let subst,metasenv,ugraph2 = - fo_unif_subst - test_equality_only - subst context metasenv t1' t2' ugraph - in - j+1,subst,metasenv,ugraph2 - with - Uncertain _ - | UnificationFailure _ -> -prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)); - let metasenv, subst = - CicMetaSubst.restrict - subst [(n,j)] metasenv in - j+1,subst,metasenv,ugraph1) - ) (1,subst,metasenv,ugraph) ln lm - with - Exit -> - raise - (UnificationFailure "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." - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2))) *) - | Invalid_argument _ -> - raise - (UnificationFailure "2")) - (* - (sprintf - "Error trying to unify %s with %s: the lengths of the two local contexts do not match." - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) *) - in subst,metasenv,ugraph1 + (fun (j,subst,metasenv,ugraph) t1 t2 -> + match t1,t2 with + None,_ + | _,None -> j+1,subst,metasenv,ugraph + | Some t1', Some t2' -> + (* First possibility: restriction *) + (* Second possibility: unification *) + (* Third possibility: convertibility *) + let b, ugraph1 = + R.are_convertible + ~subst ~metasenv context t1' t2' ugraph + in + if b then + j+1,subst,metasenv, ugraph1 + else + (try + let subst,metasenv,ugraph2 = + fo_unif_subst + test_equality_only + subst context metasenv t1' t2' ugraph + in + j+1,subst,metasenv,ugraph2 + with + Uncertain _ + | UnificationFailure _ -> +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 + j+1,subst,metasenv,ugraph1) + ) (1,subst,metasenv,ugraph) ln lm + with + Exit -> + raise + (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." + (CicMetaSubst.ppterm subst t1) + (CicMetaSubst.ppterm subst t2))) *) + | Invalid_argument _ -> + raise + (UnificationFailure (lazy "2"))) + (* + (sprintf + "Error trying to unify %s with %s: the lengths of the two local contexts do not match." + (CicMetaSubst.ppterm subst t1) + (CicMetaSubst.ppterm subst t2)))) *) + in subst,metasenv,ugraph1 | (C.Meta (n,_), C.Meta (m,_)) when n>m -> - fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph + fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph | (C.Meta (n,l), t) | (t, C.Meta (n,l)) -> - let swap = + let swap = match t1,t2 with C.Meta (n,_), C.Meta (m,_) when n < m -> false | _, C.Meta _ -> false | _,_ -> true - in - let lower = fun x y -> if swap then y else x in - let upper = fun x y -> if swap then x else y in - let fo_unif_subst_ordered + in + let lower = fun x y -> if swap then y else x in + let upper = fun x y -> if swap then x else y in + let fo_unif_subst_ordered test_equality_only subst context metasenv m1 m2 ugraph = fo_unif_subst test_equality_only subst context metasenv (lower m1 m2) (upper m1 m2) ugraph - in + in begin let subst,metasenv,ugraph1 = let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in (try let tyt,ugraph1 = - type_of_aux' metasenv subst context t ugraph - in - fo_unif_subst - test_equality_only - subst context metasenv tyt (S.subst_meta l meta_type) ugraph1 + type_of_aux' metasenv subst context t ugraph + in + fo_unif_subst + test_equality_only + subst context metasenv tyt (S.subst_meta l meta_type) ugraph1 with - UnificationFailure msg - | Uncertain msg -> - prerr_endline msg;raise (UnificationFailure msg) + UnificationFailure _ as e -> raise e + | Uncertain msg -> raise (UnificationFailure msg) | AssertFailure _ -> - prerr_endline "siamo allo huge hack"; - (* TODO huge hack!!!! - * we keep on unifying/refining in the hope that - * the problem will be eventually solved. - * In the meantime we're breaking a big invariant: - * the terms that we are unifying are no longer well - * typed in the current context (in the worst case - * we could even diverge) *) - (subst, metasenv,ugraph)) in - let t',metasenv,subst = - try - CicMetaSubst.delift n subst context metasenv l t - with - (CicMetaSubst.MetaSubstFailure msg)-> - raise (UnificationFailure msg) - | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) - in - let t'',ugraph2 = - match t' with - C.Sort (C.Type u) when not test_equality_only -> - let u' = CicUniv.fresh () in - let s = C.Sort (C.Type u') in - let ugraph2 = - CicUniv.add_ge (upper u u') (lower u u') ugraph1 - in - s,ugraph2 - | _ -> t',ugraph1 - in - (* Unifying the types may have already instantiated n. Let's check *) - try - let (_, oldt,_) = CicUtil.lookup_subst n subst in - let lifted_oldt = S.subst_meta l oldt in - fo_unif_subst_ordered - test_equality_only subst context metasenv t lifted_oldt ugraph2 - with - CicUtil.Subst_not_found _ -> - let (_, context, ty) = CicUtil.lookup_meta n metasenv in - let subst = (n, (context, t'',ty)) :: subst in - let metasenv = - List.filter (fun (m,_,_) -> not (n = m)) metasenv in - subst, metasenv, ugraph2 - end + 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. + * In the meantime we're breaking a big invariant: + * the terms that we are unifying are no longer well + * typed in the current context (in the worst case + * we could even diverge) *) + (subst, metasenv,ugraph)) in + let t',metasenv,subst = + try + CicMetaSubst.delift n subst context metasenv l t + with + (CicMetaSubst.MetaSubstFailure msg)-> + raise (UnificationFailure msg) + | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) + in + let t'',ugraph2 = + match t' with + C.Sort (C.Type u) when not test_equality_only -> + let u' = CicUniv.fresh () in + let s = C.Sort (C.Type u') in + let ugraph2 = + CicUniv.add_ge (upper u u') (lower u u') ugraph1 + in + s,ugraph2 + | _ -> t',ugraph1 + in + (* Unifying the types may have already instantiated n. Let's check *) + try + let (_, oldt,_) = CicUtil.lookup_subst n subst in + let lifted_oldt = S.subst_meta l oldt in + fo_unif_subst_ordered + test_equality_only subst context metasenv t lifted_oldt ugraph2 + with + CicUtil.Subst_not_found _ -> + let (_, context, ty) = CicUtil.lookup_meta n metasenv in + let subst = (n, (context, t'',ty)) :: subst in + let metasenv = + List.filter (fun (m,_,_) -> not (n = m)) metasenv in + subst, metasenv, ugraph2 + end | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2)) | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) -> if UriManager.eq uri1 uri2 then 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 + 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) - (CicMetaSubst.ppterm subst t2))) *) + (CicMetaSubst.ppterm subst t2))) *) | C.MutConstruct (uri1,i1,j1,exp_named_subst1), C.MutConstruct (uri2,i2,j2,exp_named_subst2) -> if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then - fo_unif_subst_exp_named_subst - test_equality_only - subst context metasenv exp_named_subst1 exp_named_subst2 ugraph + fo_unif_subst_exp_named_subst + test_equality_only + subst context metasenv exp_named_subst1 exp_named_subst2 ugraph else - raise (UnificationFailure "5") - (* (sprintf + raise (UnificationFailure (lazy "5")) + (* (sprintf "Can't unify %s with %s due to different inductive constructors" (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2))) *) + (CicMetaSubst.ppterm subst t2))) *) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only subst context metasenv te t2 ugraph @@ -446,91 +485,92 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str let subst',metasenv',ugraph1 = fo_unif_subst true subst context metasenv s1 s2 ugraph in - fo_unif_subst test_equality_only + fo_unif_subst test_equality_only subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> let subst',metasenv',ugraph1 = fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph in - fo_unif_subst test_equality_only - subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 + fo_unif_subst test_equality_only + subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 | (C.LetIn (_,s1,t1), t2) | (t2, C.LetIn (_,s1,t1)) -> fo_unif_subst test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph | (C.Appl l1, C.Appl l2) -> (* andrea: this case should be probably rewritten in the - spirit of deref *) + spirit of deref *) (match l1,l2 with | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j -> - (try - List.fold_left2 - (fun (subst,metasenv,ugraph) t1 t2 -> - fo_unif_subst - test_equality_only subst context metasenv t1 t2 ugraph) - (subst,metasenv,ugraph) l1 l2 - with (Invalid_argument msg) -> - raise (UnificationFailure msg)) + (try + List.fold_left2 + (fun (subst,metasenv,ugraph) t1 t2 -> + fo_unif_subst + test_equality_only subst context metasenv t1 t2 ugraph) + (subst,metasenv,ugraph) l1 l2 + with (Invalid_argument 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, + (* we verify that none of the args is a Meta, since beta expanding with respoect to a metavariable makes no sense *) (* (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 - fo_unif_subst - test_equality_only - subst context metasenv reduced t2 ugraph - with CicUtil.Subst_not_found _ -> *) - let subst,metasenv,beta_expanded,ugraph1 = - beta_expand_many - test_equality_only metasenv subst context t2 args ugraph - in + let (_,t,_) = CicUtil.lookup_subst i subst in + let lifted = S.subst_meta l t in + let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in + fo_unif_subst + test_equality_only + subst context metasenv reduced t2 ugraph + with CicUtil.Subst_not_found _ -> *) + 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 + (C.Meta (i,l)) beta_expanded ugraph1 | _, C.Meta (i,l)::args when not(exists_a_meta args) -> (* (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 - fo_unif_subst - test_equality_only - subst context metasenv t1 reduced ugraph - with CicUtil.Subst_not_found _ -> *) - 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 - (C.Meta (i,l)) beta_expanded ugraph1 + let (_,t,_) = CicUtil.lookup_subst i subst in + let lifted = S.subst_meta l t in + let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in + fo_unif_subst + test_equality_only + subst context metasenv t1 reduced ugraph + with CicUtil.Subst_not_found _ -> *) + 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 + (C.Meta (i,l)) beta_expanded ugraph1 | _,_ -> - let lr1 = List.rev l1 in + let lr1 = List.rev l1 in let lr2 = List.rev l2 in let rec - fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph = + fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph = match (l1,l2) with [],_ | _,[] -> assert false | ([h1],[h2]) -> fo_unif_subst - test_equality_only subst context metasenv h1 h2 ugraph + test_equality_only subst context metasenv h1 h2 ugraph | ([h],l) | (l,[h]) -> fo_unif_subst test_equality_only subst context metasenv - h (C.Appl (List.rev l)) ugraph + h (C.Appl (List.rev l)) ugraph | ((h1::l1),(h2::l2)) -> let subst', metasenv',ugraph1 = - fo_unif_subst - test_equality_only - subst context metasenv h1 h2 ugraph + fo_unif_subst + test_equality_only + subst context metasenv h1 h2 ugraph in - fo_unif_l - test_equality_only subst' metasenv' (l1,l2) ugraph1 + fo_unif_l + test_equality_only subst' metasenv' (l1,l2) ugraph1 in - fo_unif_l - test_equality_only subst metasenv (lr1, lr2) ugraph) + fo_unif_l + test_equality_only subst metasenv (lr1, lr2) ugraph) | (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 @@ -542,24 +582,38 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str List.fold_left2 (fun (subst,metasenv,ugraph) t1 t2 -> fo_unif_subst - test_equality_only subst context metasenv t1 t2 ugraph + test_equality_only subst context metasenv t1 t2 ugraph ) (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) - (CicMetaSubst.ppterm subst t2)))) *) + (CicMetaSubst.ppterm subst t1) + (CicMetaSubst.ppterm subst t2)))) *) | (C.Rel _, _) | (_, C.Rel _) -> 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 + 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 _) @@ -569,62 +623,42 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str if t1 = t2 then subst, metasenv, ugraph else - let b,ugraph1 = - R.are_convertible ~subst ~metasenv context t1 t2 ugraph - in - if b then - subst, metasenv, ugraph1 - else - raise (* (UnificationFailure "7") *) - (UnificationFailure (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 + let b,ugraph1 = + R.are_convertible ~subst ~metasenv context t1 t2 ugraph + in + if b then + subst, metasenv, ugraph1 + else + 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) -> 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")) + C.Prod _ -> + fo_unif_subst test_equality_only + subst context metasenv t1 t2' ugraph + | _ -> raise (UnificationFailure (lazy "8"))) | (t1, C.Prod _) -> let t1' = R.whd ~subst context t1 in (match t1' with - C.Prod _ -> - fo_unif_subst test_equality_only - subst context metasenv t1' t2 ugraph - | _ -> (* raise (UnificationFailure "9")) *) - raise - (UnificationFailure (sprintf - "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) + C.Prod _ -> + fo_unif_subst test_equality_only + subst context metasenv t1' t2 ugraph + | _ -> (* raise (UnificationFailure "9")) *) + raise + (UnificationFailure (lazy (sprintf + "Can't unify %s with %s because they are not convertible" + (CicMetaSubst.ppterm subst t1) + (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 @@ -644,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. *) @@ -657,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)) ;; -