X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FautoTactic.ml;h=b232d9894c444fb1ea2b431ff3811908e033930f;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=d46aa6949c9f074526ca0ab312f96e6f8f90db22;hpb=cb790b3f03194d3155841431d17cfea1245fea9d;p=helm.git diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index d46aa6949..b232d9894 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -23,14 +23,17 @@ * http://cs.unibo.it/helm/. *) - let debug_print = (* ignore *) prerr_endline + let debug = false + let debug_print s = if debug then prerr_endline (Lazy.force s) (* let debug_print = fun _ -> () *) +(* Profiling code let new_experimental_hint = let profile = CicUtil.profile "new_experimental_hint" in fun ~dbd ~facts ?signature ~universe status -> - profile (MetadataQuery.new_experimental_hint ~dbd ~facts ?signature ~universe) status + profile.profile (MetadataQuery.new_experimental_hint ~dbd ~facts ?signature ~universe) status +*) let new_experimental_hint = MetadataQuery.new_experimental_hint (* In this versions of auto_tac we maintain an hash table of all inspected goals. We assume that the context is invariant for application. @@ -143,8 +146,8 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals match exitus with Yes (bo,_) -> (* - debug_print "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; - debug_print (CicPp.ppterm ty); + debug_print (lazy "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); + debug_print (lazy (CicPp.ppterm ty)); *) let subst_in = (* if we just apply the subtitution, the type @@ -157,13 +160,13 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals proof goal subst_in metasenv in [(subst_in,(proof,[],sign))] | No d when (d >= depth) -> - (* debug_print "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *) + (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *) [] (* the empty list means no choices, i.e. failure *) | No _ | NotYetInspected -> - debug_print ("CURRENT GOAL = " ^ CicPp.ppterm ty); - debug_print ("CURRENT PROOF = " ^ CicPp.ppterm p); - debug_print ("CURRENT HYP = " ^ CicPp.ppcontext ey); + debug_print (lazy ("CURRENT GOAL = " ^ CicPp.ppterm ty)); + debug_print (lazy ("CURRENT PROOF = " ^ CicPp.ppterm p)); + debug_print (lazy ("CURRENT HYP = " ^ CicPp.ppcontext ey)); let sign, new_sign = if is_meta_closed then None, Some (MetadataConstraints.signature_of ty) @@ -214,8 +217,8 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals in if not (cty = ty) then begin - debug_print ("ty = "^CicPp.ppterm ty); - debug_print ("cty = "^CicPp.ppterm cty); + debug_print (lazy ("ty = "^CicPp.ppterm ty)); + debug_print (lazy ("cty = "^CicPp.ppterm cty)); assert false end Hashtbl.add inspected_goals @@ -276,23 +279,23 @@ let default_depth = 5 let default_width = 3 (* -let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) +let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) () = let auto_tac dbd (proof,goal) = let universe = MetadataQuery.signature_of_goal ~dbd (proof,goal) in Hashtbl.clear inspected_goals; - debug_print "Entro in Auto"; + debug_print (lazy "Entro in Auto"); let id t = t in let t1 = Unix.gettimeofday () in match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with - [] -> debug_print("Auto failed"); + [] -> debug_print (lazy "Auto failed"); raise (ProofEngineTypes.Fail "No Applicable theorem") | (_,(proof,[],_))::_ -> let t2 = Unix.gettimeofday () in - debug_print "AUTO_TAC HA FINITO"; + debug_print (lazy "AUTO_TAC HA FINITO"); let _,_,p,_ = proof in - debug_print (CicPp.ppterm p); + debug_print (lazy (CicPp.ppterm p)); Printf.printf "tempo: %.9f\n" (t2 -. t1); (proof,[]) | _ -> assert false @@ -302,44 +305,53 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) *) let paramodulation_tactic = ref - (fun dbd status -> raise (ProofEngineTypes.Fail "Not Ready yet..."));; + (fun dbd ?full ?depth ?width status -> + raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));; let term_is_equality = ref - (fun term -> debug_print "term_is_equality E` DUMMY!!!!"; false);; + (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);; -let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) () = +let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation + ?full ~(dbd:HMysql.dbd) () = let auto_tac dbd (proof, goal) = - let paramodulation_ok = - let _, metasenv, _, _ = proof in - let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in - !term_is_equality meta_goal - in - if paramodulation_ok then ( - debug_print "USO PARAMODULATION..."; - try - !paramodulation_tactic dbd (proof, goal) - with e -> - raise (ProofEngineTypes.Fail "paramodulation failure") - ) else + let normal_auto () = let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in Hashtbl.clear inspected_goals; - debug_print "Entro in Auto"; + debug_print (lazy "Entro in Auto"); let id t = t in let t1 = Unix.gettimeofday () in match auto_new dbd width [] universe [id, (proof, [(goal, depth)], None)] with - [] -> debug_print("Auto failed"); - raise (ProofEngineTypes.Fail "No Applicable theorem") + [] -> debug_print(lazy "Auto failed"); + raise (ProofEngineTypes.Fail (lazy "No Applicable theorem")) | (_,(proof,[],_))::_ -> let t2 = Unix.gettimeofday () in - debug_print "AUTO_TAC HA FINITO"; + debug_print (lazy "AUTO_TAC HA FINITO"); let _,_,p,_ = proof in - debug_print (CicPp.ppterm p); - debug_print (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)); + debug_print (lazy (CicPp.ppterm p)); + debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1))); (proof,[]) | _ -> assert false + in + let full = match full with None -> false | Some _ -> true in + let paramodulation_ok = + match paramodulation with + | None -> false + | Some _ -> + let _, metasenv, _, _ = proof in + let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in + full || (!term_is_equality meta_goal) + in + if paramodulation_ok then ( + debug_print (lazy "USO PARAMODULATION..."); +(* try *) + !paramodulation_tactic dbd ~depth ~width ~full (proof, goal) +(* with ProofEngineTypes.Fail _ -> *) +(* normal_auto () *) + ) else + normal_auto () in ProofEngineTypes.mk_tactic (auto_tac dbd) ;;