X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=5500abcbf189ee44073a288ac59049410b4cd083;hb=48a389fa5b4c7d80f97c8c6c7a1f47e840977f39;hp=deb743d90b8fd20a63f292d79ffe350adeefe317;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml index deb743d90..5500abcbf 100644 --- a/matita/components/ng_refiner/nCicUnification.ml +++ b/matita/components/ng_refiner/nCicUnification.ml @@ -97,7 +97,7 @@ let outside exc_opt = let time2 = Unix.gettimeofday () in let time1 = match !times with time1::tl -> times := tl; time1 | [] -> assert false in - prerr_endline ("}}} " ^ string_of_float (time2 -. time1)); + prerr_endline ("}}} " ^ !indent ^ " " ^ string_of_float (time2 -. time1)); (match exc_opt with | Some e -> prerr_endline ("exception raised: " ^ Printexc.to_string e) | None -> ()); @@ -566,24 +566,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) @@ -730,6 +768,32 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = | Uncertain _ as exn -> raise exn | _ -> assert false in + let fo_unif_heads_and_cont_or_unwind_and_hints + test_eq_only metasenv subst m1 m2 cont hm1 hm2 + = + let ms, continuation = + (* calling the continuation inside the outermost try is an option + and makes unification stronger, but looks not frequent to me + that heads unify but not the arguments and that an hints can fix + that *) + try fo_unif test_eq_only metasenv subst m1 m2, cont + with + | UnificationFailure _ + | KeepReducing _ | Uncertain _ as exn -> + let (t1,norm1),(t2,norm2) = hm1, hm2 in + match + try_hints metasenv subst + (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2) + with + | Some x -> x, fun x -> x + | None -> + match exn with + | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2)) + | UnificationFailure _ | Uncertain _ as exn -> raise exn + | _ -> assert false + in + continuation ms + in let height_of = function | NCic.Const (Ref.Ref (_,Ref.Def h)) | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) @@ -763,11 +827,11 @@ 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 - let unif_from_stack t1 t2 b metasenv subst = + | _ -> [] in + let unif_from_stack (metasenv, subst) (t1, t2, b) = try let t1 = NCicReduction.from_stack ~delta:max_int t1 in let t2 = NCicReduction.from_stack ~delta:max_int t2 in @@ -779,19 +843,25 @@ 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 in - let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in + let check_stack l1 l2 r = + match t1, t2 with + | NCic.Meta _, _ | _, NCic.Meta _ -> + (NCicReduction.unwind (k1,e1,t1,s1)), + (NCicReduction.unwind (k2,e2,t2,s2)),[] + | _ -> check_stack l1 l2 r [] + in + let hh1,hh2,todo = + check_stack (List.rev s1) (List.rev s2) (List.rev relevance) in try - let metasenv,subst = - fo_unif_w_hints 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 + fo_unif_heads_and_cont_or_unwind_and_hints + test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) + (fun ms -> List.fold_left unif_from_stack ms todo) + m1 m2 with | KeepReducing _ -> assert false | KeepReducingThis _ ->