X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=d3c86d2816c2c9bd050bbe1b336d033d95e4c8dd;hb=1ee5193677b8e2a80d4f068ee79ecac335de1196;hp=9c456cd87f70c6659396b5038ec5e6cf0a2434fc;hpb=b68325537e9e42c5da370c9f053fa99dba8a55cd;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 9c456cd87..d3c86d281 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -17,16 +17,210 @@ 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 ^ " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2)) ;; -let unify metasenv subst context t1 t2 = - (* are_convertible?? *) - let rec aux test_eq_only metasenv subst context t1 t2 = - let fo_unif test_eq_only t1 t2 = +let mk_appl hd tl = + match hd with + | NCic.Appl l -> NCic.Appl (l@tl) + | _ -> NCic.Appl (hd :: tl) +;; + +let flexible l = + List.exists + (function + | NCic.Meta _ + | NCic.Appl (NCic.Meta _::_) -> true + | _ -> false) l +;; + +exception WrongShape;; + +let eta_reduce = + let delift_if_not_occur body orig = + try + NCicSubstitution.psubst ~avoid_beta_redexes:true + (fun () -> raise WrongShape) [()] body + with WrongShape -> orig + in + function + | NCic.Lambda(_, _, NCic.Appl [hd; NCic.Rel 1]) as orig -> + delift_if_not_occur hd 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 + NCic.Appl (hd::args) + in + delift_if_not_occur body orig + | t -> t +;; + +module C = NCic;; +module Ref = NReference;; + +let indent = ref "";; +let inside c = indent := !indent ^ String.make 1 c;; +let outside () = indent := String.sub !indent 0 (String.length !indent -1);; + +let pp s = + prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) +;; + +(* let pp _ = ();; *) + +let fix_sorts metasenv subst context meta t = + let rec aux () = function + | NCic.Sort (NCic.Type u) as orig -> + (match NCicEnvironment.sup u with + | None -> raise (fail_exc metasenv subst context meta t) + | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)) + | NCic.Meta _ as orig -> orig + | t -> NCicUtils.map (fun _ _ -> ()) () aux t + in + aux () t +;; + +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 = + 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), NCic.Rel (1 + n) + with Uncertain _ | UnificationFailure _ -> + match t' with + | 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 + iterate on the local context. For this reason, we renounce + to iterate and just lift *) + | NCic.Meta (i,(shift,lc)) -> + (metasenv,subst), NCic.Meta (i,(shift+1,lc)) + | 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 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,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 = + aux (0, context, test_eq_only) (metasenv, subst) t 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 _ -> + metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg) + +and beta_expand_many test_equality_only swap metasenv subst context t args = +(* (*D*) inside 'B'; try let rc = *) + pp (lazy (String.concat ", " + (List.map (NCicPp.ppterm ~metasenv ~subst ~context) + args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t)); + let _, subst, metasenv, hd = + List.fold_right + (fun arg (num,subst,metasenv,t) -> + 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) + in + pp (lazy ("Head syntesized by b-exp: " ^ + NCicPp.ppterm ~metasenv ~subst ~context hd)); + metasenv, subst, hd +(* (*D*) in outside (); rc with exn -> outside (); raise exn *) + +and instantiate test_eq_only metasenv subst context n lc t swap = + (*D*) inside 'I'; try let rc = + 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 fix_sorts t = + if swap then fix_sorts metasenv subst context (NCic.Meta (n,lc)) t + else + NCic.Sort (NCic.Type ( + match NCicEnvironment.sup NCicEnvironment.type0 with Some x ->x| _ -> + assert false)) + in + let name, ctx, ty = NCicUtils.lookup_meta n metasenv in + let metasenv, subst, t = + match ty with + | NCic.Implicit (`Typeof _) -> metasenv, subst, fix_sorts t + | _ -> + pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)); + let t, ty_t = + try t, NCicTypeChecker.typeof ~subst ~metasenv context t + with NCicTypeChecker.TypeCheckerFailure _ -> + let ft = fix_sorts t in + if ft == t then assert false else + try + pp (lazy ("typeof: " ^ + NCicPp.ppterm ~metasenv ~subst ~context ft)); + ft, NCicTypeChecker.typeof ~subst ~metasenv context ft + with NCicTypeChecker.TypeCheckerFailure msg -> + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context ft); + prerr_endline (Lazy.force msg); + assert false + in + let lty = NCicSubstitution.subst_meta lc ty in + pp (lazy("On the types: " ^ + NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " + ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); + let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in + metasenv, subst, t + in + let (metasenv, subst), t = + try NCicMetaSubst.delift metasenv subst context n lc t + with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg) + | NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg) + in + (* Unifying the types may have already instantiated n. *) + try + let _, _,oldt,_ = NCicUtils.lookup_subst n subst in + let oldt = NCicSubstitution.subst_meta lc oldt in + let t = NCicSubstitution.subst_meta lc t in + (* conjecture: always fail --> occur check *) + unify test_eq_only metasenv subst context oldt t + 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 + pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm + ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t))); + let metasenv = + List.filter (fun (m,_) -> not (n = m)) metasenv + in + metasenv, subst + (*D*) in outside(); rc with exn -> outside (); raise exn + +and unify test_eq_only metasenv subst context t1 t2 = + (*D*) inside 'U'; try let rc = + let fo_unif test_eq_only metasenv subst t1 t2 = + (*D*) inside 'F'; try let rc = + pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ + NCicPp.ppterm ~metasenv ~subst ~context t2)); if t1 === t2 then metasenv, subst else @@ -43,88 +237,135 @@ let 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, C.Irl _)), C.Meta (n2,(s2, C.Irl _))) - when n1 = n2 && s1 = s2 -> true - | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 && - let l1 = NCicUtils.expand_local_context l1 in - let l2 = NCicUtils.expand_local_context l2 in - (try List.for_all2 - (fun t1 t2 -> aux test_eq_only context - (NCicSubstitution.lift s1 t1) - (NCicSubstitution.lift s2 t2)) - l1 l2 - with Invalid_argument _ -> assert false) -> true - - | C.Meta (n1,l1), _ -> - (try - let _,_,term,_ = NCicUtils.lookup_subst n1 subst in - let term = NCicSubstitution.subst_meta l1 term in - aux test_eq_only context term t2 - with NCicUtils.Subst_not_found _ -> false) - | _, C.Meta (n2,l2) -> + | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 -> (try - let _,_,term,_ = NCicUtils.lookup_subst n2 subst in - let term = NCicSubstitution.subst_meta l2 term in - aux test_eq_only context t1 term - with NCicUtils.Subst_not_found _ -> false) - + let l1 = NCicUtils.expand_local_context l1 in + let l2 = NCicUtils.expand_local_context l2 in + let metasenv, subst, to_restrict, _ = + List.fold_right2 + (fun t1 t2 (metasenv, subst, to_restrict, i) -> + try + 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) + in + let metasenv, subst, _ = + NCicMetaSubst.restrict metasenv subst n1 to_restrict + in + metasenv, subst + with + | Invalid_argument _ -> assert false + | NCicMetaSubst.MetaSubstFailure msg -> + try + let _,_,term,_ = NCicUtils.lookup_subst n1 subst in + let term1 = NCicSubstitution.subst_meta lc1 term in + let term2 = NCicSubstitution.subst_meta lc2 term in + unify test_eq_only metasenv subst context term1 term2 + with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg)) + + | C.Meta (n,lc), t -> + (try + let _,_,term,_ = NCicUtils.lookup_subst n subst in + let term = NCicSubstitution.subst_meta lc term in + 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) + + | t, C.Meta (n,lc) -> + (try + let _,_,term,_ = NCicUtils.lookup_subst n subst in + let term = NCicSubstitution.subst_meta lc term in + 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) + + | 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 + 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 + 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 + List.fold_left2 + (fun (metasenv, subst) 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)) + + | 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 metasenv, subst, beta_expanded = + beta_expand_many + test_eq_only false + metasenv subst context t2 args + in + 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 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) -> @@ -134,8 +375,10 @@ let unify metasenv subst context t1 t2 = let is_prop = match remove_prods ~subst [] ty with | C.Sort C.Prop -> true + | _ -> 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) -> @@ -146,79 +389,104 @@ let 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) + (*D*) in outside(); rc with exn -> outside (); raise exn in - let unif_machines ... - + 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 + | _ -> 0 + in + let put_in_whd m1 m2 = + NCicReduction.reduce_machine ~delta:max_int ~subst context m1, + NCicReduction.reduce_machine ~delta:max_int ~subst context m2 + in + let small_delta_step + ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2) + = + assert (not (norm1 && norm2)); + if norm1 then + x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2 + else if norm2 then + NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2 + else + 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 in - try fo_unif - with Uncertain msg as exn -> - try unif_machines + let rec unif_machines metasenv subst = + function + | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) -> + (*D*) inside 'M'; try let rc = +(* + pp (lazy((if are_normal then "*" else " ") ^ " " ^ + NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^ + " === " ^ + NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2))); +*) + let relevance = [] (* TO BE UNDERSTOOD + match t1 with + | C.Const r -> NCicEnvironment.get_relevance r + | _ -> [] *) 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 (put_in_whd 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 + try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst) + with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) -> + unif_machines metasenv subst (small_delta_step m1 m2) + (*D*) in outside(); rc with exn -> outside (); raise exn + in + try fo_unif test_eq_only metasenv subst t1 t2 + with UnificationFailure msg | Uncertain msg as exn -> + try + unif_machines metasenv subst + (put_in_whd (0,[],t1,[]) (0,[],t2,[])) with | UnificationFailure _ -> raise (UnificationFailure msg) | Uncertain _ -> raise exn - in - aux false metasenv subst context t1 t2 - -let are_convertible ?(subst=[]) get_relevance = - let rec aux test_eq_only metasenv subst context t1 t2 = - in - if alpha_eq test_eq_only t1 t2 then - true - else - let height_of = function - | C.Const (Ref.Ref (_,Ref.Def h)) - | C.Const (Ref.Ref (_,Ref.Fix (_,_,h))) - | C.Appl(C.Const(Ref.Ref(_,Ref.Def h))::_) - | C.Appl(C.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h - | _ -> 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 - let rec convert_machines ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) = - (alpha_eq test_eq_only - (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[])) && - let relevance = - match t1 with - C.Const r -> NCicEnvironment.get_relevance r - | _ -> [] in - try - HExtlib.list_forall_default3 - (fun t1 t2 b -> - not b || - let t1 = RS.from_stack t1 in - let t2 = RS.from_stack t2 in - convert_machines (small_delta_step t1 t2)) s1 s2 true relevance - with Invalid_argument _ -> false) || - (delta > 0 && - let delta = delta - 1 in - let red = R.reduce ~delta ~subst context in - convert_machines (red m1,red m2,delta)) - in - convert_machines (small_delta_step (0,[],t1,[]) (0,[],t2,[])) - in - aux false + (*D*) in outside(); rc with exn -> outside (); raise exn ;; +let unify = + indent := ""; + unify false;; + (*