From c32e87198e3434dc89009b954223e825da34c1ac Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 21 Dec 2009 10:52:10 +0000 Subject: [PATCH] Refining with no expected type + unification seems to be faster. --- helm/software/components/ng_tactics/nnAuto.ml | 22 +++++++++++++------ 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 07d08345c..e00bb2ade 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -116,19 +116,27 @@ let fast_eq_check_all status eq_cache goal = let gname, ctx, gty = List.assoc goal metasenv in let gty = NCicUntrusted.apply_subst subst ctx gty in let build_status (pt, _, metasenv, subst) = - (* let stamp = Unix.gettimeofday () in *) - let metasenv, subst, pt, pty = + let stamp = Unix.gettimeofday () in + let metasenv, subst, pt, pty = NCicRefiner.typeof (status#set_coerc_db NCicCoercion.empty_db) - metasenv subst ctx pt (Some gty) - in -(* print (lazy (Printf.sprintf "Refined in %fs" - (Unix.gettimeofday() -. stamp))); *) + metasenv subst ctx pt None in + let metasenv, subst = + NCicUnification.unify status metasenv subst ctx gty pty +(* the previous code is much less expensive than directly refining + pt with expected type pty + in + NCicRefiner.typeof + (status#set_coerc_db NCicCoercion.empty_db) + metasenv subst ctx pt (Some gty) *) + in + print (lazy (Printf.sprintf "Refined in %fs" + (Unix.gettimeofday() -. stamp))); let status = status#set_obj (n,h,metasenv,subst,o) in let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in let subst = (goal,(gname,ctx,pt,pty)) :: subst in status#set_obj (n,h,metasenv,subst,o) - in + in List.map build_status (NCicParamod.fast_eq_check status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty)) -- 2.39.2