X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=e521dd30144f7db95de3950996dd1c09cd8b54ac;hb=e62111335574a6ec78e5a4367a540e0529a00404;hp=805ea859f8beef8be33eb03d123b850f37a5c48e;hpb=a4615d355dba036f1faf4aa3306e005da5e839a0;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 805ea859f..e521dd301 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -50,7 +50,7 @@ let eta_reduce subst t = let _,_,t,_ = NCicUtils.lookup_subst i subst in let t = NCicSubstitution.subst_meta lc t in eat_lambdas ctx t - with Not_found -> ctx, t) + with NCicUtils.Subst_not_found _ -> ctx, t) | t -> ctx, t in let context_body = eat_lambdas [] t in @@ -241,9 +241,11 @@ let tipify exc metasenv subst context t ty = if is_type attrs then metasenv,subst,true else + let _,cc,ty = NCicUtils.lookup_meta n metasenv in + let metasenv,subst,ty = sortfy exc metasenv subst cc ty in let metasenv = NCicUntrusted.replace_in_metasenv n - (fun attrs,cc,ty -> NCicUntrusted.set_kind `IsType attrs, cc, ty) + (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty) metasenv in metasenv,subst,false @@ -253,9 +255,11 @@ let tipify exc metasenv subst context t ty = if is_type attrs then metasenv,subst,true else + let _,cc,_,ty = NCicUtils.lookup_subst n subst in + let metasenv,subst,ty = sortfy exc metasenv subst cc ty in let subst = NCicUntrusted.replace_in_subst n - (fun attrs,cc,bo,ty->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty) + (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty) subst in optimize_meta metasenv subst (NCicSubstitution.subst_meta lc bo)) @@ -354,8 +358,8 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap = | _ -> assert false) | `IsType | `IsTerm -> - (match ty,t with - NCic.Implicit (`Typeof _), _ -> + (match ty with + NCic.Implicit (`Typeof _) -> let (metasenv, subst), ty_t = try NCicMetaSubst.delift @@ -375,7 +379,7 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap = in delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv subst - | _, _ -> + | _ -> let lty = NCicSubstitution.subst_meta lc ty in pp (lazy ("On the types: " ^ ppterm ~metasenv ~subst ~context lty ^ "=<=" ^ @@ -546,6 +550,15 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst -> unify rdb test_eq_only metasenv subst context t2 t1 (not swap) + | C.Meta (n,_), C.Meta (m,lc') when + let _,cc1,_ = NCicUtils.lookup_meta n metasenv in + let _,cc2,_ = NCicUtils.lookup_meta m metasenv in + (n < m && cc1 = cc2) || + let len1 = List.length cc1 in + let len2 = List.length cc2 in + len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) -> + instantiate rdb test_eq_only metasenv subst context m lc' + (NCicReduction.head_beta_reduce ~subst t1) (not swap) | C.Meta (n,lc), t -> instantiate rdb test_eq_only metasenv subst context n lc (NCicReduction.head_beta_reduce ~subst t) swap @@ -559,12 +572,8 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = (NCicTypeChecker.typeof ~metasenv ~subst context meta) in let metasenv, subst = - try - unify rdb test_eq_only metasenv subst context - (C.Meta (i,l)) lambda_Mj swap - with UnificationFailure msg | Uncertain msg when not norm2-> - (* failure: let's try again argument vs argument *) - raise (KeepReducing msg) + unify rdb test_eq_only metasenv subst context + (C.Meta (i,l)) lambda_Mj swap in let metasenv, subst = unify rdb test_eq_only metasenv subst context t1 t2 swap @@ -599,14 +608,12 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = 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)) | KeepReducing _ | KeepReducingThis _ -> assert false in metasenv, subst | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1), - C.Match (ref2,outtype2,term2,pl2)) -> + C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 -> let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in let _,_,ty,_ = List.nth itl tyno in let rec remove_prods ~subst context ty = @@ -622,9 +629,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = | C.Sort C.Prop -> true | _ -> false in - if not (Ref.eq ref1 ref2) then + (* if not (Ref.eq ref1 ref2) then raise (Uncertain (mk_msg metasenv subst context t1 t2)) - else + else*) let metasenv, subst = unify rdb test_eq_only metasenv subst context outtype1 outtype2 swap in let metasenv, subst = @@ -647,6 +654,12 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = | _ -> raise (KeepReducing (mk_msg metasenv subst context t1 t2)) (*D*) in outside None; rc with exn -> outside (Some exn); raise exn in + let fo_unif test_eq_only metasenv subst (norm1,t1 as nt1) (norm2,t2 as nt2)= + try fo_unif test_eq_only metasenv subst nt1 nt2 + with + UnificationFailure _ | Uncertain _ when not norm1 || not norm2 -> + raise (KeepReducing (mk_msg metasenv subst context t1 t2)) + in let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) = (*D*) inside 'H'; try let rc = pp(lazy ("\nProblema:\n" ^