From: Enrico Tassi Date: Tue, 30 Sep 2008 16:24:35 +0000 (+0000) Subject: unification completed X-Git-Tag: make_still_working~4719 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a677e0d09755766c61ce9b30a98bec10cb8902b3;p=helm.git unification completed --- diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index cc4d99e05..316b39dab 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -365,4 +365,13 @@ let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l = let head_beta_reduce ?delta ?upto t = head_beta_reduce ?delta ?upto t [];; +type stack_item = RS.stack_term +type environment_item = RS.env_term + +type machine = int * environment_item list * NCic.term * stack_item list + +let reduce_machine = R.reduce +let from_stack = RS.from_stack +let unwind = R.unwind + (* vim:set foldmethod=marker: *) diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli index ebbba2543..56b8ee06c 100644 --- a/helm/software/components/ng_kernel/nCicReduction.mli +++ b/helm/software/components/ng_kernel/nCicReduction.mli @@ -27,3 +27,14 @@ val are_convertible : delta reduction; if provided, ~upto is the maximum number of beta redexes reduced *) val head_beta_reduce: ?delta:int -> ?upto:int -> NCic.term -> NCic.term + +type stack_item +type environment_item + +type machine = int * environment_item list * NCic.term * stack_item list + +val reduce_machine : + delta:int -> ?subst:NCic.substitution -> NCic.context -> machine -> machine +val from_stack : stack_item -> machine +val unwind : machine -> NCic.term + diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 5267796ef..abc9eae6a 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -155,7 +155,7 @@ exception NotInTheList;; let position n (shift, lc) = match lc with | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList - | NCic.Irl len -> n - shift + | NCic.Irl _ -> n - shift | NCic.Ctx tl -> let rec aux k = function | [] -> raise NotInTheList @@ -190,7 +190,7 @@ let mk_restricted_irl shift len restrictions = exception Occur;; let rec force_does_not_occur metasenv subst restrictions t = - let rec aux k (metasenv, subst as ms) = function + let rec aux k ms = function | NCic.Rel r when List.mem (r - k) restrictions -> raise Occur | NCic.Meta (n, l) as orig -> (* we ignore the subst since restrict will take care of already @@ -276,7 +276,7 @@ and restrict metasenv subst i restrictions = let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in metasenv, subst_entry_j :: List.map - (fun (n,x) as orig -> if i = n then subst_entry_i else orig) subst, + (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst, j with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf ("Cannot restrict the context of the metavariable ?%d over "^^ @@ -298,7 +298,7 @@ and restrict metasenv subst i restrictions = let reloc_irl = mk_restricted_irl 0 (List.length ctx) restrictions in let subst_entry = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in List.map - (fun (n,x) as orig -> if i = n then metasenv_entry else orig) + (fun (n,_) as orig -> if i = n then metasenv_entry else orig) metasenv, subst_entry :: subst, j with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf @@ -355,11 +355,10 @@ let delift metasenv subst context n l t = in (metasenv, subst), NCic.Meta(newmeta, mk_restricted_irl shift1 len1 restrictions) - | NCic.Irl len, NCic.Irl len1 when shift = 0 -> ms, orig - | NCic.Irl len, NCic.Irl len1 -> + | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig + | NCic.Irl _, NCic.Irl _ -> ms, NCic.Meta (i, (shift1 - shift, lc1)) | _ -> - let to_be_restricted = ref [] in let lc1 = NCicUtils.expand_local_context lc1 in let rec deliftl tbr j ms = function | [] -> ms, tbr, [] diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 147bb555f..16178bd3b 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -17,6 +17,12 @@ exception AssertFailure of string Lazy.t;; let (===) x y = Pervasives.compare x y = 0 ;; +let uncert_exc metasenv subst context t1 t2 = + Uncertain (lazy ( + "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ + " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2)) +;; + let fail_exc metasenv subst context t1 t2 = UnificationFailure (lazy ( "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ @@ -47,29 +53,34 @@ let eta_reduce = with WrongShape -> orig in function - | NCic.Lambda(name, src, NCic.Appl [hd; NCic.Rel 1]) as orig -> + | NCic.Lambda(_, _, NCic.Appl [hd; NCic.Rel 1]) as orig -> delift_if_not_occur hd orig - | NCic.Lambda(name, src, NCic.Appl (hd :: l)) as orig + | NCic.Lambda(_, _, NCic.Appl (hd :: l)) as orig when HExtlib.list_last l = NCic.Rel 1 -> let body = - let args, _ = Hextlib.split_nth (List.length l - 1) l in + let args, _ = HExtlib.split_nth (List.length l - 1) l in NCic.Appl (hd::args) in delift_if_not_occur body orig | t -> t ;; - + +module C = NCic;; +module Ref = NReference;; + let rec beta_expand num test_eq_only swap metasenv subst context t arg = let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' = try let metasenv, subst = - unify test_eq_only metasenv subst context - (NCicSubstitution.lift n arg) t' + if swap then + unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg) + else + unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t' in - (metasenv, subst), C.Rel (1 + n) + (metasenv, subst), NCic.Rel (1 + n) with Uncertain _ | UnificationFailure _ -> match t' with - | NCic.Rel m orig -> + | NCic.Rel m as orig -> (metasenv, subst), if m <= n then orig else NCic.Rel (m+1) (* andrea: in general, beta_expand can create badly typed terms. This happens quite seldom in practice, UNLESS we @@ -80,31 +91,31 @@ let rec beta_expand num test_eq_only swap metasenv subst context t arg = | NCic.Prod (name, src, tgt) as orig -> let (metasenv, subst), src1 = aux (n,context,true) acc src in let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in - let (metasenv,subst), tgt1 = aux k (metasenv, subst) tgt in - if src == src1 && tgt == tgt1 then orig else - NCic.Prod (name, src1, tgt1) + let ms, tgt1 = aux k (metasenv, subst) tgt in + if src == src1 && tgt == tgt1 then ms, orig else + ms, NCic.Prod (name, src1, tgt1) | t -> NCicUntrusted.map_term_fold_a - (fun e (n,ctx) -> n+1,e::ctx) k aux acc t + (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t in let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in let fresh_name = "Hbeta" ^ string_of_int num in - let (metasenv,subst,_), t1 = + let (metasenv,subst), t1 = aux (0, context, test_eq_only) (metasenv, subst) t in - let t2 = eta_reduce (C.Lambda (fresh_name,argty,t1)) in + let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in try ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2); metasenv, subst, t2 with NCicTypeChecker.TypeCheckerFailure _ -> - NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg) + metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg) -and beta_expand_many test_equality_only metasenv subst context t args ugraph = +and beta_expand_many test_equality_only swap metasenv subst context t args = let _, subst, metasenv, hd = List.fold_right (fun arg (num,subst,metasenv,t) -> - let subst, metasenv, t = - beta_expand num test_equality_only metasenv subst context t arg + let metasenv, subst, t = + beta_expand num test_equality_only swap metasenv subst context t arg in num+1,subst,metasenv,t) args (1,subst,metasenv,t) @@ -112,8 +123,9 @@ and beta_expand_many test_equality_only metasenv subst context t args ugraph = metasenv, subst, hd and instantiate test_eq_only metasenv subst context n lc t swap = - let unif m s c t1 t2 = - if swap then unify m s c t2 t1 else unify m s c t1 t2 + let unify test_eq_only m s c t1 t2 = + if swap then unify test_eq_only m s c t2 t1 + else unify test_eq_only m s c t1 t2 in let ty_t = try NCicTypeChecker.typeof ~subst ~metasenv context t @@ -121,27 +133,26 @@ and instantiate test_eq_only metasenv subst context n lc t swap = in let name, ctx, ty = NCicUtils.lookup_meta n metasenv in let ty = NCicSubstitution.subst_meta lc ty in - let metasenv, subst = unify metasenv susbt context ty ty_t in + let metasenv, subst = unify test_eq_only metasenv subst context ty ty_t in let (metasenv, subst), t = NCicMetaSubst.delift metasenv subst context n lc t in (* Unifying the types may have already instantiated n. *) try - let _, _,oldt,_ = CicUtil.lookup_subst n subst in + let _, _,oldt,_ = NCicUtils.lookup_subst n subst in let oldt = NCicSubstitution.subst_meta lc oldt in (* conjecture: always fail --> occur check *) unify test_eq_only metasenv subst context oldt t - with CicUtil.Subst_not_found _ -> + with NCicUtils.Subst_not_found _ -> (* by cumulativity when unify(?,Type_i) * we could ? := Type_j with j <= i... *) let subst = (n, (name, ctx, t, ty)) :: subst in let metasenv = List.filter (fun (m,_) -> not (n = m)) metasenv in - subst, metasenv + metasenv, subst -and unify metasenv subst context t1 t2 = - let rec aux test_eq_only metasenv subst context t1 t2 = +and unify test_eq_only metasenv subst context t1 t2 = let fo_unif test_eq_only metasenv subst t1 t2 = if t1 === t2 then metasenv, subst @@ -159,13 +170,13 @@ and unify metasenv subst context t1 t2 = | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> - let metasenv, subst = aux true metasenv subst context s1 s2 in - aux test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 + let metasenv, subst = unify true metasenv subst context s1 s2 in + unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) -> - let metasenv,subst=aux test_eq_only metasenv subst context ty1 ty2 in - let metasenv,subst=aux test_eq_only metasenv subst context s1 s2 in + let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in + let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in let context = (name1, C.Def (s1,ty1))::context in - aux test_eq_only metasenv subst context t1 t2 + unify test_eq_only metasenv subst context t1 t2 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 -> (try @@ -175,9 +186,11 @@ and unify metasenv subst context t1 t2 = List.fold_right2 (fun t1 t2 (metasenv, subst, to_restrict, i) -> try - aux test_eq_only metasenv subst context - (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2), - to_restrict, i-1 + let metasenv, subst = + unify test_eq_only metasenv subst context + (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2) + in + metasenv, subst, to_restrict, i-1 with UnificationFailure _ | Uncertain _ -> metasenv, subst, i::to_restrict, i-1) l1 l2 (metasenv, subst, [], List.length l1) @@ -193,113 +206,99 @@ and unify metasenv subst context t1 t2 = let _,_,term,_ = NCicUtils.lookup_subst n1 subst in let term1 = NCicSubstitution.subst_meta lc1 term in let term2 = NCicSubstitution.subst_meta lc2 term in - aux test_eq_only metasenv subst context term1 term2 + unify test_eq_only metasenv subst context term1 term2 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg)) | C.Meta (n,lc), t -> - try + (try let _,_,term,_ = NCicUtils.lookup_subst n subst in let term = NCicSubstitution.subst_meta lc term in - aux test_eq_only metasenv subst context term t + unify test_eq_only metasenv subst context term t with NCicUtils.Subst_not_found _-> - instantiate test_eq_only metasenv subst context n lc t false + instantiate test_eq_only metasenv subst context n lc t false) | t, C.Meta (n,lc) -> - try + (try let _,_,term,_ = NCicUtils.lookup_subst n subst in let term = NCicSubstitution.subst_meta lc term in - aux test_eq_only metasenv subst context t term + unify test_eq_only metasenv subst context t term with NCicUtils.Subst_not_found _-> - instantiate test_eq_only metasenv subst context n lc t true + instantiate test_eq_only metasenv subst context n lc t true) | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst -> let _,_,term,_ = NCicUtils.lookup_subst i subst in let term = NCicSubstitution.subst_meta l term in - aux test_eq_only metasenv subst context (mk_appl term args) t2 + unify test_eq_only metasenv subst context (mk_appl term args) t2 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst -> let _,_,term,_ = NCicUtils.lookup_subst i subst in let term = NCicSubstitution.subst_meta l term in - aux test_eq_only metasenv subst context t1 (mk_appl term args) + unify test_eq_only metasenv subst context t1 (mk_appl term args) | NCic.Appl (NCic.Meta (i,_)::_ as l1), NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j -> - try + (try List.fold_left2 (fun (metasenv, subst) t1 t2 -> - aux test_eq_only metasenv subst context t1 t2) + unify test_eq_only metasenv subst context t1 t2) (metasenv,subst) l1 l2 with Invalid_argument _ -> - raise (fail_exc metasenv subst context t1 t2) + raise (fail_exc metasenv subst context t1 t2)) | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) -> (* we verify that none of the args is a Meta, since beta expanding w.r.t a metavariable makes no sense *) - let subst, metasenv, beta_expanded = - beta_expand_many (* passare swap *) - test_equality_only metasenv subst context t2 args ugraph + let metasenv, subst, beta_expanded = + beta_expand_many + test_eq_only false + metasenv subst context t2 args in - aux test_eq_only metasenv subst context + unify test_eq_only metasenv subst context (C.Meta (i,l)) beta_expanded + | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) -> - let subst,metasenv,beta_expanded = - 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 metasenv, subst, beta_expanded = + beta_expand_many + test_eq_only true + metasenv subst context t1 args + in + unify test_eq_only metasenv subst context + beta_expanded (C.Meta (i,l)) + + (* processing this case here we avoid a useless small delta step *) | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2)) - when (Ref.eq r1 r2 && - List.length (E.get_relevance r1) >= List.length tl1) -> - let relevance = E.get_relevance r1 in - let relevance = match r1 with + when Ref.eq r1 r2 -> + let relevance = NCicEnvironment.get_relevance r1 in + let relevance = match r1 with | Ref.Ref (_,Ref.Con (_,_,lno)) -> let _,relevance = HExtlib.split_nth lno relevance in HExtlib.mk_list false lno @ relevance | _ -> relevance - in - let fail = ref ~-1 in - let res = (try - HExtlib.list_forall_default3 - (fun t1 t2 b -> fail := !fail+1; not b || aux test_eq_only context t1 t2) - tl1 tl2 true relevance - with Invalid_argument _ -> false) - in res - (* if res then true - else - let relevance = get_relevance_p ~subst context _hd1 tl1 in - let _,relevance = HExtlib.split_nth !fail relevance in - let b,relevance = (match relevance with - | [] -> assert false - | b::tl -> b,tl) in - let _,tl1 = HExtlib.split_nth (!fail+1) tl1 in - let _,tl2 = HExtlib.split_nth (!fail+1) tl2 in - if (not b) then - (dance (); - try - HExtlib.list_forall_default3 - (fun t1 t2 b -> not b || aux test_eq_only context t1 t2) - tl1 tl2 true relevance - with Invalid_argument _ -> false) - else false *) - | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) -> - aux test_eq_only context hd1 hd2 && - let relevance = get_relevance ~subst context hd1 tl1 in - (try - HExtlib.list_forall_default3 - (fun t1 t2 b -> not b || aux test_eq_only context t1 t2) - tl1 tl2 true relevance - with Invalid_argument _ -> false) + in + let metasenv, subst, _ = + try + List.fold_left2 + (fun (metasenv, subst, relevance) t1 t2 -> + let b, relevance = + match relevance with b::tl -> b,tl | _ -> true, [] in + let metasenv, subst = + try unify test_eq_only metasenv subst context t1 t2 + with UnificationFailure _ | Uncertain _ when not b -> + metasenv, subst + in + metasenv, subst, relevance) + (metasenv, subst, relevance) tl1 tl2 + with Invalid_argument _ -> + raise (uncert_exc metasenv subst context t1 t2) + in + metasenv, subst | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1), C.Match (ref2,outtype2,term2,pl2)) -> - let _,_,itl,_,_ = E.get_checked_indtys ref1 in + let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in let _,_,ty,_ = List.nth itl tyno in let rec remove_prods ~subst context ty = - let ty = whd ~subst context ty in + let ty = NCicReduction.whd ~subst context ty in match ty with | C.Sort _ -> ty | C.Prod (name,so,ta) -> @@ -312,7 +311,7 @@ and unify metasenv subst context t1 t2 = | _ -> false in let rec remove_prods ~subst context ty = - let ty = whd ~subst context ty in + let ty = NCicReduction.whd ~subst context ty in match ty with | C.Sort _ -> ty | C.Prod (name,so,ta) -> @@ -323,96 +322,85 @@ and unify metasenv subst context t1 t2 = raise (uncert_exc metasenv subst context t1 t2) else let metasenv, subst = - aux test_eq_only metasenv subst context outtype1 outtype2 in + unify test_eq_only metasenv subst context outtype1 outtype2 in let metasenv, subst = - try aux test_eq_only metasenv subst context term1 term2 + try unify test_eq_only metasenv subst context term1 term2 with UnificationFailure _ | Uncertain _ when is_prop -> metasenv, subst in - try + (try List.fold_left2 - (fun (metasenv,subst) -> aux test_eq_only metasenv subst context) + (fun (metasenv,subst) -> + unify test_eq_only metasenv subst context) (metasenv, subst) pl1 pl2 with Invalid_argument _ -> - raise (uncert_exc metasenv subst context t1 t2) + raise (uncert_exc metasenv subst context t1 t2)) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | _ -> raise (uncert_exc metasenv subst context t1 t2) in + let height_of = function + | NCic.Const (Ref.Ref (_,Ref.Def h)) + | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) + | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_) + | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h + | NCic.Meta _ -> max_int + | _ -> 0 + in + let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = + let h1 = height_of t1 in + let h2 = height_of t2 in + let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in + NCicReduction.reduce_machine ~delta ~subst context m1, + NCicReduction.reduce_machine ~delta ~subst context m2, + delta + in let rec unif_machines metasenv subst = function - | ((k1,e1,NCic.Meta _ as t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) - | ((k1,e1,t1,s1 as m1),(k2,e2,NCic.Meta _ as t2,s2 as m2),delta) -> - try - fo_unif test_eq_only metasenv subst (R.unwind m1) (R.unwind m2) - with UnificationFailure _ | Uncertain _ when delta > 0 -> - let delta = delta - 1 in - let red = R.reduce ~delta ~subst context in - unif_machines metasenv subst (red m1,red m2,delta) | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) -> try - let metasenv, subst = - fo_unif test_eq_only metasenv subst - (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[])) - in - let relevance = + let relevance = [] (* TO BE UNDERSTOOD match t1 with | C.Const r -> NCicEnvironment.get_relevance r - | _ -> [] in - try - let rec check_stack f l1 l2 r a = - match l1,l2,r with - | x1::tl1, x2::tl2, r::tr -> - check_stack f tl1 tl2 tr (f x1 x2 r a) - | x1::tl1, x2::tl2, [] -> - check_stack f tl1 tl2 tr (f x1 x2 true a) - | [], [], _ -> a - | _ -> raise (Invalid_argument "check_stack") - in - check_stack - (fun t1 t2 b (metasenv,subst) -> - try - let t1 = RS.from_stack t1 in - let t2 = RS.from_stack t2 in - unif_machines metasenv subst (small_delta_step t1 t2) - with UnificationFailure _ | Uncertain _ when not b -> - metasenv, subst) - s1 s2 relevance (metasenv,subst) - with Invalid_argument _ -> - raise (UnificationFailure (lazy ( "Can't unify " ^ NCicPp.ppterm - ~metasenv ~subst ~context (R.unwind m1) ^ " with " ^ NCicPp.ppterm - ~metasenv ~subst ~context (R.unwind m2)))) + | _ -> [] *) in + let unif_from_stack t1 t2 b metasenv subst = + try + let t1 = NCicReduction.from_stack t1 in + let t2 = NCicReduction.from_stack t2 in + unif_machines metasenv subst (small_delta_step t1 t2) + with UnificationFailure _ | Uncertain _ when not b -> + metasenv, subst + in + let rec check_stack l1 l2 r (metasenv, subst) = + match l1,l2,r with + | x1::tl1, x2::tl2, r::tr -> + check_stack tl1 tl2 tr + (unif_from_stack x1 x2 r metasenv subst) + | x1::tl1, x2::tl2, [] -> + check_stack tl1 tl2 [] + (unif_from_stack x1 x2 true metasenv subst) + | l1, l2, _ -> + fo_unif test_eq_only metasenv subst + (NCicReduction.unwind (k1,e1,t1,List.rev l1)) + (NCicReduction.unwind (k2,e2,t2,List.rev l2)) + in + check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst) with UnificationFailure _ | Uncertain _ when delta > 0 -> let delta = delta - 1 in - let red = R.reduce ~delta ~subst context in + let red = NCicReduction.reduce_machine ~delta ~subst context in unif_machines metasenv subst (red m1,red m2,delta) in - let height_of = function - | NCic.Const (Ref.Ref (_,Ref.Def h)) - | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) - | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_) - | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h - | NCic.Meta _ -> max_int - | _ -> 0 - in - let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = - let h1 = height_of t1 in - let h2 = height_of t2 in - let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in - R.reduce ~delta ~subst context m1, - R.reduce ~delta ~subst context m2, - delta - in try fo_unif test_eq_only metasenv subst t1 t2 - with UnificationFailure msg |Uncertain msg as exn -> + with UnificationFailure msg |Uncertain msg as exn + when not (flexible [t1;t2]) -> try unif_machines metasenv subst (small_delta_step (0,[],t1,[]) (0,[],t2,[])) with | UnificationFailure _ -> raise (UnificationFailure msg) | Uncertain _ -> raise exn - in - aux false metasenv subst context t1 t2 ;; +let unify = unify false;; + (*