From c63c1b75e1afd0307c932e43375963aea1ec6c0b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Dec 2008 13:58:09 +0000 Subject: [PATCH] hints attached --- .../components/ng_refiner/nCicUnification.ml | 425 +++++++++--------- 1 file changed, 207 insertions(+), 218 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index abbafc458..c6f4f6d91 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -247,223 +247,208 @@ and instantiate hdb test_eq_only metasenv subst context n lc t swap = and unify hdb test_eq_only metasenv subst context t1 t2 = (*D*) inside 'U'; try let rc = - let rec fo_unif test_eq_only metasenv subst t1 t2 = - let try_hints metasenv subst context t1 t2 (* exc*) = - let candidates = NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2 - in - let rec cand_iter = function - | [] -> None (* raise exc *) - | (metasenv,c1,c2)::tl -> - try - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t1); - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context c1); - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t2); - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context c2); - let metasenv,subst = fo_unif test_eq_only metasenv subst t1 c1 in - let metasenv,subst = fo_unif test_eq_only metasenv subst c2 t2 in - Some (fo_unif test_eq_only metasenv subst t1 t2) - with - UnificationFailure _ | Uncertain _ -> cand_iter tl - in - cand_iter candidates - in - + 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 - match (try_hints metasenv subst context t1 t2) with - | Some x -> x - | None -> - match (t1,t2) with - | (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) - | (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) - | (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) - - | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) - | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> - let metasenv, subst = unify hdb true metasenv subst context s1 s2 in - unify hdb 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=unify hdb test_eq_only metasenv subst context ty1 ty2 in - let metasenv,subst=unify hdb test_eq_only metasenv subst context s1 s2 in - let context = (name1, C.Def (s1,ty1))::context in - unify hdb 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 - 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 hdb 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 - if to_restrict <> [] then - let metasenv, subst, _ = - NCicMetaSubst.restrict metasenv subst n1 to_restrict - in - metasenv, subst - else metasenv, subst - with - | Invalid_argument _ -> assert false - | NCicMetaSubst.MetaSubstFailure msg -> + match (t1,t2) with + | (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) + | (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) + | (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) + + | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) + | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> + let metasenv, subst = unify hdb true metasenv subst context s1 s2 in + unify hdb 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=unify hdb test_eq_only metasenv subst context ty1 ty2 in + let metasenv,subst=unify hdb test_eq_only metasenv subst context s1 s2 in + let context = (name1, C.Def (s1,ty1))::context in + unify hdb 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 + 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 _,_,term,_ = NCicUtils.lookup_subst n1 subst in - let term1 = NCicSubstitution.subst_meta lc1 term in - let term2 = NCicSubstitution.subst_meta lc2 term in - unify hdb 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 hdb test_eq_only metasenv subst context term t - with NCicUtils.Subst_not_found _-> - instantiate hdb 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 hdb test_eq_only metasenv subst context t term - with NCicUtils.Subst_not_found _-> - instantiate hdb 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 hdb 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 hdb 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 hdb 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 hdb - test_eq_only false - metasenv subst context t2 args - in - unify hdb 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 hdb - test_eq_only true - metasenv subst context t1 args - in - unify hdb 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 -> - 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 metasenv, subst = + unify hdb 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 + if to_restrict <> [] then 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 hdb 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,_,_ = NCicEnvironment.get_checked_indtys ref1 in - let _,_,ty,_ = List.nth itl tyno in - let rec remove_prods ~subst context ty = - let ty = NCicReduction.whd ~subst context ty in - match ty with - | C.Sort _ -> ty - | C.Prod (name,so,ta) -> - remove_prods ~subst ((name,(C.Decl so))::context) ta - | _ -> assert false + NCicMetaSubst.restrict metasenv subst n1 to_restrict in - 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 = NCicReduction.whd ~subst context ty in - match ty with - | C.Sort _ -> ty - | C.Prod (name,so,ta) -> - remove_prods ~subst ((name,(C.Decl so))::context) ta - | _ -> assert false + metasenv, subst + else 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 hdb 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 hdb test_eq_only metasenv subst context term t + with NCicUtils.Subst_not_found _-> + instantiate hdb 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 hdb test_eq_only metasenv subst context t term + with NCicUtils.Subst_not_found _-> + instantiate hdb 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 hdb 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 hdb 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 hdb 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 hdb + test_eq_only false + metasenv subst context t2 args + in + unify hdb 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 hdb + test_eq_only true + metasenv subst context t1 args + in + unify hdb 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 -> + 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 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 hdb 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,_,_ = NCicEnvironment.get_checked_indtys ref1 in + let _,_,ty,_ = List.nth itl tyno in + let rec remove_prods ~subst context ty = + let ty = NCicReduction.whd ~subst context ty in + match ty with + | C.Sort _ -> ty + | C.Prod (name,so,ta) -> + remove_prods ~subst ((name,(C.Decl so))::context) ta + | _ -> assert false + in + let is_prop = + match remove_prods ~subst [] ty with + | C.Sort C.Prop -> true + | _ -> false + in + if not (Ref.eq ref1 ref2) then + raise (uncert_exc metasenv subst context t1 t2) + else + let metasenv, subst = + unify hdb test_eq_only metasenv subst context outtype1 outtype2 in + let metasenv, subst = + try unify hdb test_eq_only metasenv subst context term1 term2 + with UnificationFailure _ | Uncertain _ when is_prop -> + metasenv, subst in - if not (Ref.eq ref1 ref2) then - raise (uncert_exc metasenv subst context t1 t2) - else - let metasenv, subst = - unify hdb test_eq_only metasenv subst context outtype1 outtype2 in - let metasenv, subst = - try unify hdb test_eq_only metasenv subst context term1 term2 - with UnificationFailure _ | Uncertain _ when is_prop -> - metasenv, subst - in - (try - List.fold_left2 - (fun (metasenv,subst) -> - unify hdb test_eq_only metasenv subst context) - (metasenv, subst) pl1 pl2 - with Invalid_argument _ -> - raise (uncert_exc metasenv subst context t1 t2)) - | (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) + (try + List.fold_left2 + (fun (metasenv,subst) -> + unify hdb test_eq_only metasenv subst context) + (metasenv, subst) pl1 pl2 + with Invalid_argument _ -> + raise (uncert_exc metasenv subst context t1 t2)) + | (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) (*D*) in outside(); rc with exn -> outside (); raise exn in + let try_hints metasenv subst t1 t2 (* exc*) = + let candidates = + NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2 + in + let rec cand_iter = function + | [] -> None (* raise exc *) + | (metasenv,c1,c2)::tl -> + try + let metasenv,subst = fo_unif test_eq_only metasenv subst t1 c1 in + let metasenv,subst = fo_unif test_eq_only metasenv subst c2 t2 in + Some (metasenv, subst) + with + UnificationFailure _ | Uncertain _ -> cand_iter tl + in + cand_iter candidates + in let height_of = function | NCic.Const (Ref.Ref (_,Ref.Def h)) | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) @@ -475,7 +460,7 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = NCicReduction.reduce_machine ~delta:max_int ~subst context m1, NCicReduction.reduce_machine ~delta:max_int ~subst context m2 in - let small_delta_step + let small_delta_step ~subst ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2) = assert (not (norm1 && norm2)); @@ -494,12 +479,13 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = 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) ^ + pp (lazy("UM: " ^ + NCicPp.ppterm ~metasenv ~subst ~context + (NCicReduction.unwind (k1,e1,t1,s1)) ^ " === " ^ - NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2))); -*) + NCicPp.ppterm ~metasenv ~subst ~context + (NCicReduction.unwind (k2,e2,t2,s2)))); +pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2)); let relevance = [] (* TO BE UNDERSTOOD match t1 with | C.Const r -> NCicEnvironment.get_relevance r @@ -529,17 +515,20 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = unif_from_stack x1 x2 r metasenv subst ) (metasenv,subst) todo with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) -> - unif_machines metasenv subst (small_delta_step m1 m2) + unif_machines metasenv subst (small_delta_step ~subst 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 + match try_hints metasenv subst t1 t2 with + | Some x -> x + | None -> + try + unif_machines metasenv subst + (put_in_whd (0,[],t1,[]) (0,[],t2,[])) + with + | UnificationFailure _ -> raise (UnificationFailure msg) + | Uncertain _ -> raise exn (*D*) in outside(); rc with exn -> outside (); raise exn ;; -- 2.39.2