X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=a74172ca0e463b3e449f4fc970f877c677afc677;hb=4e7e01cd771c07b3605ba54d3853ac34a02cb86d;hp=13744017acc9d98125676b5bc8717a149be51af2;hpb=6733674a52c5a2c9e5bc3a39ad1614b5ee2b1d62;p=helm.git diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml index 13744017a..a74172ca0 100644 --- a/matita/components/ng_refiner/nCicUnification.ml +++ b/matita/components/ng_refiner/nCicUnification.ml @@ -382,8 +382,8 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap = | _ -> let lty = NCicSubstitution.subst_meta lc ty in pp (lazy ("On the types: " ^ - ppterm ~metasenv ~subst ~context lty ^ "=<=" ^ - ppterm ~metasenv ~subst ~context ty_t)); + ppterm ~metasenv ~subst ~context ty_t ^ "=<=" ^ + ppterm ~metasenv ~subst ~context lty)); let metasenv, subst = unify rdb false metasenv subst context ty_t lty false in @@ -559,6 +559,17 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = 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), C.Meta (m,lc') when + let _,_,tyn = NCicUtils.lookup_meta n metasenv in + let _,_,tym = NCicUtils.lookup_meta m metasenv in + let tyn = NCicSubstitution.subst_meta lc tyn in + let tym = NCicSubstitution.subst_meta lc tym in + match tyn,tym with + NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 -> + NCicEnvironment.universe_lt u1 u2 + | _,_ -> false -> + 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 @@ -566,24 +577,62 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = instantiate rdb test_eq_only metasenv subst context n lc (NCicReduction.head_beta_reduce ~subst t) (not swap) + (* higher order unification case *) | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ -> - let metasenv, lambda_Mj = - lambda_intros rdb metasenv subst context (List.length args) - (NCicTypeChecker.typeof ~metasenv ~subst context meta) - in - let metasenv, subst = - 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 - in - (try - let name, ctx, term, ty = NCicUtils.lookup_subst i subst in - let term = eta_reduce subst term in - let subst = List.filter (fun (j,_) -> j <> i) subst in - metasenv, ((i, (name, ctx, term, ty)) :: subst) - with Not_found -> assert false) + (* this easy_case handles "(? ?) =?= (f a)", same number of + * args, preferring the instantiation "f" over "\_.f a" for the + * metavariable in head position. Since the arguments of the meta + * are flexible, delift would ignore them generating a constant + * function even in the easy case above *) + let easy_case = + match t2 with + | NCic.Appl (f :: f_args) + when + List.exists (NCicMetaSubst.is_flexible context ~subst) args -> + let mlen = List.length args in + let flen = List.length f_args in + let min_len = min mlen flen in + let mhe,margs = HExtlib.split_nth (mlen - min_len) args in + let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in + (try + Some (List.fold_left2 + (fun (m, s) t1 t2 -> + unify rdb test_eq_only m s context t1 t2 swap + ) (metasenv,subst) + ((NCicUntrusted.mk_appl meta mhe)::margs) + ((NCicUntrusted.mk_appl f fhe)::fargs)) + with UnificationFailure _ | Uncertain _ | KeepReducing _ -> + None) + | _ -> None + in + (match easy_case with + | Some ms -> ms + | None -> + (* This case handles "(?_f ..ti..) =?= t2", abstracting every + * non flexible ti (delift skips local context items that are + * flexible) from t2 in two steps: + * 1) ?_f := \..xi.. .? + * 2) ?_f ..ti.. =?= t2 --unif_machines--> + ?_f[..ti..] =?= t2 --instantiate--> + delift [..ti..] t2 *) + let metasenv, lambda_Mj = + lambda_intros rdb metasenv subst context (List.length args) + (NCicTypeChecker.typeof ~metasenv ~subst context meta) + in + let metasenv, subst = + 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 + in + (try + let name, ctx, term, ty = NCicUtils.lookup_subst i subst in + let term = eta_reduce subst term in + let subst = List.filter (fun (j,_) -> j <> i) subst in + metasenv, ((i, (name, ctx, term, ty)) :: subst) + with Not_found -> assert false)) + | _, NCic.Appl (NCic.Meta (_,_) :: _) -> unify rdb test_eq_only metasenv subst context t2 t1 (not swap) @@ -789,10 +838,10 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = 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 + let relevance = match t1 with | C.Const r -> NCicEnvironment.get_relevance r - | _ -> [] *) in + | _ -> [] in let unif_from_stack (metasenv, subst) (t1, t2, b) = try let t1 = NCicReduction.from_stack ~delta:max_int t1 in @@ -805,7 +854,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = match l1,l2,r with | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo) | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo) - | l1, l2, _ -> + | l1, l2, _ -> NCicReduction.unwind (k1,e1,t1,List.rev l1), NCicReduction.unwind (k2,e2,t2,List.rev l2), todo @@ -814,10 +863,11 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = match t1, t2 with | NCic.Meta _, _ | _, NCic.Meta _ -> (NCicReduction.unwind (k1,e1,t1,s1)), - (NCicReduction.unwind (k2,e2,t2,s2)),[] + (NCicReduction.unwind (k2,e2,t2,s2)),[] | _ -> check_stack l1 l2 r [] in - let hh1,hh2,todo = check_stack (List.rev s1) (List.rev s2) relevance in + let hh1,hh2,todo = + check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in try fo_unif_heads_and_cont_or_unwind_and_hints test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) @@ -827,7 +877,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = | KeepReducing _ -> assert false | KeepReducingThis _ -> assert (not (norm1 && norm2)); - unif_machines metasenv subst (small_delta_step ~subst m1 m2) + 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