From: Enrico Tassi Date: Thu, 30 Sep 2010 12:23:09 +0000 (+0000) Subject: patches for hints & unification: X-Git-Tag: make_still_working~2814 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=53b957fd45c47b20d698503c9bb67e2ef3ab98e1;p=helm.git patches for hints & unification: 1) =========== It is an old and know issue. The check_stack calls fo_unif_w_hints only on a prefix of applications, leaving some arguments on the stack. This prevents hints to be found. Example Hint: And A B === fun_of_morph And_morphism A B If the problem And A B =?= fun_of_morph ? A B is found immediately (before entering the KAM) the it is solved, but if it shows up inside the KAM, A and B are left on the stack and a fo_unif_w_hints has to solve And =?= fun_of_morph ? While one could declare hints multiple times, varying the number of actual arguments, I believe that the right solution is to make the KAM code pass more information to fo_unif_w_hints, like the remaining arguments. Nevertheless, the new fo_unif_w_hints is hard to factor with the old one (that is used elsewere) so I wrote a new one called fo_unif_heads_and_cont_or_unwind_and_hints. It first tries fo_unif on the heads, and if successfull call a continuation (that will unify all stack arguments pairwise) or unwinds the machine and looks for hints on the complete terms, not just a prefix. 2) =========== The fo_unif function does some clever higher order unification in the case (? x1 ... xn) =?= (t y1 ... ym) but in the very similar case K (? x1 ... xn) _ =?= (t y1 ... ym) it does not. K has to be reduced away, and afterwards the KAM configuration has ? and t as heads, xs and ys on the stack. Assume m-n=l, the unification problems generated by the check_stack function are ? =?= t y1 .. yl xi =?= yl+i for i in 1 .. n That is clearly suboptimal, since xn and ym could differ, but a clever instantiation of the flexible head could drop or move around xm. Moreover one expects the two unification problems to be solved in the same way by the system, but it does not, and in my case the second one actually fails. The KAM code should just be a speedup over a naive unfolding of constants, beta-iota-zeta reduction and fo_unif, but in this (unfortunate) case it is weaker. 3) ============ The delift function does a lot of work even if the metavariable is being instantiated with a closed term. This is very often the case when the term is suggested by hints. Hints may suggest constants in partially unfolded form (see paper submitted to Type09), that can thus be very big. This simple patch speeds up delift in this case. --- diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml index d3250c2fe..b1cf9aed0 100644 --- a/helm/software/components/disambiguation/multiPassDisambiguator.ml +++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml @@ -51,6 +51,8 @@ let passes () = (* *) (* for demo to reduce the number of interpretations *) (true, `Library, true); ] + else if !debug then + [ (true, `Multi, true); ] else [ (true, `Mono, false); (true, `Multi, false); diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index 9c96469e5..82f7cef80 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -317,7 +317,7 @@ let count_occurrences ~subst n t = let occurrences = ref 0 in let rec aux k _ = function | C.Rel m when m = n+k -> incr occurrences - | C.Rel m -> () + | C.Rel _m -> () | C.Implicit _ -> () | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) () | C.Meta (mno,(s,l)) -> @@ -334,3 +334,17 @@ let count_occurrences ~subst n t = aux 0 () t; !occurrences ;; + +exception Found_variable + +let looks_closed t = + let rec aux k _ = function + | C.Rel m when k < m -> raise Found_variable + | C.Rel _m -> () + | C.Implicit _ -> () + | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) () + | C.Meta _ -> raise Found_variable + | t -> NCicUtils.fold (fun _ k -> k + 1) k aux () t + in + try aux 0 () t; true with Found_variable -> false +;; diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli index 702f8fc19..7ff7f9335 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.mli +++ b/helm/software/components/ng_kernel/nCicUntrusted.mli @@ -43,3 +43,5 @@ val apply_subst_metasenv : NCic.substitution -> NCic.metasenv -> NCic.metasenv val count_occurrences : subst:NCic.substitution -> int -> NCic.term -> int +(* quick, but with false negatives (since no ~subst), check for closed terms *) +val looks_closed : NCic.term -> bool diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 549f06f85..8bc281953 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -349,6 +349,9 @@ let delift ~unify metasenv subst context n l t = lb in let rec aux (context,k,in_scope) (metasenv, subst as ms) t = + (* XXX if t is closed, we should just terminate. Speeds up hints! *) + if NCicUntrusted.looks_closed t then ms, t + else match unify_list in_scope metasenv subst context k t with | Some x -> x | None -> diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index deb743d90..13744017a 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/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 -> ()); @@ -730,6 +730,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))) @@ -767,7 +793,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = match t1 with | C.Const r -> NCicEnvironment.get_relevance r | _ -> [] *) in - let unif_from_stack t1 t2 b metasenv subst = + 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 @@ -784,14 +810,19 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = 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) 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 _ ->