From 9182039cdc2a7573f36014f9b266e27ac123a1ad Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 24 Sep 2008 16:59:37 +0000 Subject: [PATCH] ... --- .../components/ng_refiner/nCicMetaSubst.mli | 7 +- .../components/ng_refiner/nCicUnification.ml | 165 +++++++++++------- 2 files changed, 109 insertions(+), 63 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index 8f03ccb11..91752fbf7 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -46,4 +46,9 @@ val delift : NCic.metasenv -> NCic.substitution -> NCic.context -> int -> NCic.local_context -> NCic.term -> (NCic.metasenv * NCic.substitution) * NCic.term - + +val restrict: + NCic.metasenv -> + NCic.substitution -> + int -> int list -> NCic.metasenv * NCic.substitution * int + diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 9c456cd87..6a4781794 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -24,9 +24,8 @@ let fail_exc metasenv subst context t1 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 fo_unif test_eq_only metasenv subst t1 t2 = if t1 === t2 then metasenv, subst else @@ -51,29 +50,52 @@ let unify metasenv subst context t1 t2 = let context = (name1, C.Def (s1,ty1))::context in aux 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,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 -> + (try + 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 + aux test_eq_only metasenv subst context + (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2), + 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 + aux test_eq_only metasenv subst context term1 term2 + with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg)) + + | C.Meta (n1,l1), _ + | _, C.Meta (n2,l2) -> + + + - | 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) -> + aux test_eq_only metasenv subst context term t2 + with NCicUtils.Subst_not_found _ -> + + ) (try let _,_,term,_ = NCicUtils.lookup_subst n2 subst in let term = NCicSubstitution.subst_meta l2 term in - aux test_eq_only context t1 term + aux test_eq_only metasenv subst context t1 term with NCicUtils.Subst_not_found _ -> false) | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2)) @@ -134,6 +156,8 @@ 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 match ty with @@ -161,29 +185,59 @@ let unify metasenv subst context t1 t2 = | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | _ -> raise (uncert_exc metasenv subst context t1 t2) in - let unif_machines ... - - in - try fo_unif - with Uncertain msg as exn -> - try unif_machines - 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 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 = + 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)))) + 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) + in 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 + | 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) = @@ -194,29 +248,16 @@ let are_convertible ?(subst=[]) get_relevance = 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,[])) + try fo_unif test_eq_only metasenv subst t1 t2 + with UnificationFailure msg |Uncertain msg as exn -> + try + unif_machines metasenv subst + (small_delta_step (0,[],t1,[]) (0,[],t2,[])) + with + | UnificationFailure _ -> raise (UnificationFailure msg) + | Uncertain _ -> raise exn in - aux false + aux false metasenv subst context t1 t2 ;; -- 2.39.2