From 30f0cf11c54154787e259c01bb99595c4a92ab1c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 12 Oct 2009 17:38:50 +0000 Subject: [PATCH] 1) Bug fixed: the case Meta(i) vs Meta(i) was handled in a particular way, but the case Meta(i) vs (Appl (Meta(j),...)) that reduces to Meta(i) was not. As a result, a tempeted self assegniment yielded strange errors. Fixed by more aggressively unwinding the subst during fo_unif. 2) Major re-organization of the code to gain some speed in Oliboni's stuff. The idea is that of introducing a new internal exception KeepReducing used to signal that, after a fo_unif, it still makes sense to fall back to machines. Only if it does not it makes sense to distinguish between Failures and Uncertain and the latter test can now be implemented more lazily w.r.t. the old version that used to call metas_of_term on the unwinded machines (that are potentially HUGE). With this modification, all Oliboni's tests terminate, even if they are still very slow compared to the height=0 strategy. Moreover, the tests show that unification on closed terms can still be 4x slower than conversion, which is partially unexpected. --- .../components/ng_refiner/nCicUnification.ml | 184 ++++++++++-------- 1 file changed, 101 insertions(+), 83 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 5353363d5..d95415d99 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -14,20 +14,14 @@ exception UnificationFailure of string Lazy.t;; exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; +exception KeepReducing of string Lazy.t;; let (===) x y = Pervasives.compare x y = 0 ;; -let uncert_exc metasenv subst context t1 t2 = - Uncertain (lazy ( +let mk_msg metasenv subst context t1 t2 = + (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 mk_appl ~upto hd tl = NCicReduction.head_beta_reduce ~upto @@ -210,7 +204,9 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = assert(has_tag ((=)`IsSort) tags); metasenv, subst, t | _ -> - let exc_to_be = fail_exc metasenv subst context (NCic.Meta (n,lc)) t in + let exc_to_be = + UnificationFailure (mk_msg metasenv subst context (NCic.Meta (n,lc)) t) + in let t, ty_t = try t, NCicTypeChecker.typeof ~subst ~metasenv context t with @@ -356,11 +352,14 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = and unify rdb test_eq_only metasenv subst context t1 t2 = (*D*) inside 'U'; try let rc = - let fo_unif test_eq_only metasenv subst t1 t2 = + let fo_unif test_eq_only metasenv subst (norm1,t1) (norm2,t2) = (*D*) inside 'F'; try let rc = pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ NCicPp.ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv ~subst metasenv)); + pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst:[] ~context t1 ^ " ==??== " ^ + NCicPp.ppterm ~metasenv ~subst:[] ~context t2 ^ ppmetasenv + ~subst metasenv)); if t1 === t2 then metasenv, subst else @@ -371,13 +370,13 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = assert false | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> if NCicEnvironment.universe_leq a b then metasenv, subst - else raise (fail_exc metasenv subst context t1 t2) + else raise (UnificationFailure (mk_msg metasenv subst context t1 t2)) | (C.Sort (C.Type a), C.Sort (C.Type b)) -> if NCicEnvironment.universe_eq a b then metasenv, subst - else raise (fail_exc metasenv subst context t1 t2) + else raise (UnificationFailure (mk_msg metasenv subst context t1 t2)) | (C.Sort C.Prop,C.Sort (C.Type _)) -> if (not test_eq_only) then metasenv, subst - else raise (fail_exc metasenv subst context t1 t2) + else raise (UnificationFailure (mk_msg metasenv subst context t1 t2)) | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> @@ -421,6 +420,16 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = let term2 = NCicSubstitution.subst_meta lc2 term in unify rdb test_eq_only metasenv subst context term1 term2 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg)) + + | 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 rdb test_eq_only metasenv subst context t1 t2) + (metasenv,subst) l1 l2 + with Invalid_argument _ -> + raise (UnificationFailure (mk_msg metasenv subst context t1 t2))) | _, NCic.Meta (n, _) when is_locked n subst -> (let (metasenv, subst), i = @@ -462,23 +471,15 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = metasenv, ((i, (name, ctx, term, ty)) :: subst) with Not_found -> assert false)) - | C.Meta (n,lc), t -> - (try - let _,_,term,_ = NCicUtils.lookup_subst n subst in - let term = NCicSubstitution.subst_meta lc term in - unify rdb test_eq_only metasenv subst context term t - with NCicUtils.Subst_not_found _-> - instantiate rdb test_eq_only metasenv subst context n lc - (NCicReduction.head_beta_reduce ~subst t) false) + | C.Meta (n,lc), t when List.mem_assoc n subst -> + let _,_,term,_ = NCicUtils.lookup_subst n subst in + let term = NCicSubstitution.subst_meta lc term in + unify rdb test_eq_only metasenv subst context term t - | t, C.Meta (n,lc) -> - (try - let _,_,term,_ = NCicUtils.lookup_subst n subst in - let term = NCicSubstitution.subst_meta lc term in - unify rdb test_eq_only metasenv subst context t term - with NCicUtils.Subst_not_found _-> - instantiate rdb test_eq_only metasenv subst context n lc - (NCicReduction.head_beta_reduce ~subst t) true) + | t, C.Meta (n,lc) when List.mem_assoc n subst -> + let _,_,term,_ = NCicUtils.lookup_subst n subst in + let term = NCicSubstitution.subst_meta lc term in + unify rdb test_eq_only metasenv subst context t term | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst -> let _,_,term,_ = NCicUtils.lookup_subst i subst in @@ -492,23 +493,25 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = unify rdb test_eq_only metasenv subst context t1 (mk_appl ~upto:(List.length args) 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 rdb test_eq_only metasenv subst context t1 t2) - (metasenv,subst) l1 l2 - with Invalid_argument _ -> - raise (fail_exc metasenv subst context t1 t2)) + | C.Meta (n,lc), t -> + instantiate rdb test_eq_only metasenv subst context n lc + (NCicReduction.head_beta_reduce ~subst t) false + + | t, C.Meta (n,lc) -> + instantiate rdb test_eq_only metasenv subst context n lc + (NCicReduction.head_beta_reduce ~subst t) true | NCic.Appl (NCic.Meta (i,l)::args), _ -> let metasenv, subst, lambda_Mj = lambda_intros rdb metasenv subst context t1 args in let metasenv, subst = + try unify rdb test_eq_only metasenv subst context (C.Meta (i,l)) lambda_Mj + with UnificationFailure msg | Uncertain msg -> + (* failure: let's try again argument vs argument *) + raise (KeepReducing msg) in let metasenv, subst = unify rdb test_eq_only metasenv subst context t1 t2 @@ -525,8 +528,12 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = lambda_intros rdb metasenv subst context t2 args in let metasenv, subst = + try unify rdb test_eq_only metasenv subst context lambda_Mj (C.Meta (i,l)) + with UnificationFailure msg | Uncertain msg -> + (* failure: let's try again argument vs argument *) + raise (KeepReducing msg) in let metasenv, subst = unify rdb test_eq_only metasenv subst context t1 t2 @@ -564,8 +571,11 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = in metasenv, subst, relevance) (metasenv, subst, relevance) tl1 tl2 - with Invalid_argument _ -> - raise (uncert_exc metasenv subst context t1 t2) + with + Invalid_argument _ -> + raise (Uncertain (mk_msg metasenv subst context t1 t2)) + | UnificationFailure _ | Uncertain _ when not (norm1 && norm2) -> + raise (KeepReducing (mk_msg metasenv subst context t1 t2)) in metasenv, subst @@ -587,7 +597,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = | _ -> false in if not (Ref.eq ref1 ref2) then - raise (uncert_exc metasenv subst context t1 t2) + raise (Uncertain (mk_msg metasenv subst context t1 t2)) else let metasenv, subst = unify rdb test_eq_only metasenv subst context outtype1 outtype2 in @@ -603,13 +613,15 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = (metasenv, subst) pl1 pl2 with Invalid_argument _ -> assert false) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false - | _ when NCicUntrusted.metas_of_term subst context t1 = [] && - NCicUntrusted.metas_of_term subst context t2 = [] -> - raise (fail_exc metasenv subst context t1 t2) - | _ -> raise (uncert_exc metasenv subst context t1 t2) + | _ when norm1 && norm2 -> + if (could_reduce t1 || could_reduce t2) then + raise (Uncertain (mk_msg metasenv subst context t1 t2)) + else + raise (UnificationFailure (mk_msg metasenv subst context t1 t2)) + | _ -> raise (KeepReducing (mk_msg metasenv subst context t1 t2)) (*D*) in outside true; rc with exn -> outside false; raise exn in - let try_hints metasenv subst t1 t2 (* exc*) = + let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) = (*D*) inside 'H'; try let rc = pp(lazy ("\nProblema:\n" ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^ @@ -632,9 +644,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = try (*D*) inside 'K'; try let rc = let metasenv,subst = - fo_unif test_eq_only metasenv subst t1 c1 in + fo_unif test_eq_only metasenv subst mt1 (false,c1) in let metasenv,subst = - fo_unif test_eq_only metasenv subst c2 t2 in + fo_unif test_eq_only metasenv subst (false,c2) mt2 in let metasenv,subst = List.fold_left (fun (metasenv, subst) (x,y) -> @@ -645,8 +657,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = Some (metasenv, subst) (*D*) in outside true; rc with exn -> outside false; raise exn with - UnificationFailure _ | Uncertain _ -> - cand_iter tl + KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl in cand_iter candidates (*D*) in outside true; rc with exn -> outside false; raise exn @@ -667,9 +678,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = = assert (not (norm1 && norm2)); if norm1 then - x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2 + x1,NCicReduction.reduce_machine ~delta:0 ~subst context m2 else if norm2 then - NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2 + NCicReduction.reduce_machine ~delta:0 ~subst context m1,x2 else let h1 = height_of t1 in let h2 = height_of t2 in @@ -711,43 +722,48 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2)); in let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in try - let metasenv,subst = fo_unif test_eq_only metasenv subst hh1 hh2 in + let metasenv,subst = + fo_unif test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) in List.fold_left (fun (metasenv,subst) (x1,x2,r) -> unif_from_stack x1 x2 r metasenv subst ) (metasenv,subst) todo - with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) -> + with + | KeepReducing _ -> + assert (not (norm1 && norm2)); unif_machines metasenv subst (small_delta_step ~subst m1 m2) + | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2)) + -> unif_machines metasenv subst (small_delta_step ~subst m1 m2) + | UnificationFailure msg + when could_reduce (NCicReduction.unwind (fst m1)) + || could_reduce (NCicReduction.unwind (fst m2)) + -> raise (Uncertain msg) (*D*) in outside true; rc with exn -> outside false; raise exn in - try fo_unif test_eq_only metasenv subst t1 t2 + try fo_unif test_eq_only metasenv subst (false,t1) (false,t2) with - | UnificationFailure msg as exn -> - (try - unif_machines metasenv subst - (put_in_whd (0,[],t1,[]) (0,[],t2,[])) - with - | UnificationFailure _ -> raise (UnificationFailure msg) - | Uncertain _ -> raise exn) - | Uncertain msg as exn -> -(* - prerr_endline "PROBLEMA"; - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t1); - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t2); -*) - let (t1,_ as t1m),(t2,_ as t2m) = put_in_whd (0,[],t1,[]) (0,[],t2,[]) in - match - try_hints metasenv subst - (NCicReduction.unwind t1) (NCicReduction.unwind t2) - with - | Some x -> x - | None -> - try - unif_machines metasenv subst (t1m, t2m) - with - | UnificationFailure _ -> raise (UnificationFailure msg) - | Uncertain _ -> raise exn - (*D*) in outside true; rc with exn -> outside false; raise exn + | UnificationFailure _ as exn -> raise exn + | KeepReducing _ | Uncertain _ as exn -> + let (t1,norm1 as tm1),(t2,norm2 as tm2) = + put_in_whd (0,[],t1,[]) (0,[],t2,[]) + in + (match + try_hints metasenv subst + (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2) + with + | Some x -> x + | None -> + match exn with + | KeepReducing msg -> + (try + unif_machines metasenv subst (tm1,tm2) + with + | UnificationFailure _ -> raise (UnificationFailure msg) + | Uncertain _ -> raise (Uncertain msg) + | KeepReducing _ -> assert false) + | Uncertain _ -> raise exn + | _ -> assert false) + (*D*) in outside true; rc with KeepReducing _ -> assert false | exn -> outside false; raise exn and delift_type_wrt_terms rdb metasenv subst context t args = let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in @@ -762,7 +778,9 @@ and delift_type_wrt_terms rdb metasenv subst context t args = in indent := ind; res) metasenv subst context 0 (0,NCic.Ctx lc) t - with NCicMetaSubst.MetaSubstFailure _ -> (metasenv, subst), t + with + NCicMetaSubst.MetaSubstFailure _ + | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t in metasenv, subst, t ;; -- 2.39.2