| Not_found -> ""
;;
-let int name params =
+let int name default params =
try int_of_string (List.assoc name params) with
- | Not_found -> default_depth
+ | Not_found -> default
| Failure _ ->
raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
;;
-let auto_tac ~params ~(dbd:HMysql.dbd) =
+(*
+let callback_for_paramodulation dbd width depth t l =
+ let _,y,x,xx = t in
+ let universe = MetadataQuery.universe_of_goals ~dbd t l in
+ let todo = List.map (fun g -> (g, depth)) l in
+ prerr_endline ("AUTO: " ^ CicPp.ppterm x ^ " : " ^ CicPp.ppterm xx);
+ prerr_endline ("MENV: " ^ CicMetaSubst.ppmetasenv [] y);
+ match auto_new dbd width [] universe [(fun x -> x), (t, todo, None)] with
+ | (_,(proof,[],_))::_ -> proof
+ | _ -> raise (Failure "xxx")
+;;
+*)
+
+let callback_for_paramodulation dbd flags proof commonctx ?universe cache l =
+ let _,metasenv,_,_ = proof in
+ let oldmetasenv = metasenv in
+ let universe =
+ match universe with
+ | Some u -> u
+ | None ->
+ let universe =
+ AutoTypes.universe_of_goals dbd proof l AutoTypes.empty_universe
+ in
+ AutoTypes.universe_of_context commonctx metasenv universe
+ in
+ match
+ Auto.auto_all_solutions universe cache commonctx metasenv l flags
+ with
+ | [],cache -> [],cache,universe
+ | solutions,cache ->
+ let solutions =
+ HExtlib.filter_map
+ (fun (subst,metasenv) ->
+ let opened =
+ ProofEngineHelpers.compare_metasenvs
+ ~oldmetasenv ~newmetasenv:metasenv
+ in
+ if opened = [] then
+ Some subst
+ else
+ None)
+ solutions
+ in
+ solutions,cache,universe
+;;
+
+let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
(* argument parsing *)
- let depth = int "depth" params in
- let width = int "width" params in
+ let depth = int "depth" AutoTypes.default_flags.AutoTypes.maxdepth params in
+ let width = int "width" AutoTypes.default_flags.AutoTypes.maxwidth params in
let timeout = string "timeout" params in
let paramodulation = bool "paramodulation" params in
let full = bool "full" params in
let timeout =
try Some (float_of_string timeout) with Failure _ -> None
in
- (* the real tactic *)
- let auto_tac dbd (proof, goal) =
- let normal_auto () =
- let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in
- Hashtbl.clear inspected_goals;
- 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(lazy "Auto failed");
- raise (ProofEngineTypes.Fail (lazy "No Applicable theorem"))
- | (_,(proof,[],_))::_ ->
- let t2 = Unix.gettimeofday () in
- debug_print (lazy "AUTO_TAC HA FINITO");
- let _,_,p,_ = proof in
- debug_print (lazy (CicPp.ppterm p));
- debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)));
- (proof,[])
- | _ -> assert false
- in
- let paramodulation_ok =
- let _, metasenv, _, _ = proof in
- let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
- paramodulation && (full || (Equality.term_is_equality meta_goal))
- in
- if paramodulation_ok then (
- debug_print (lazy "USO PARAMODULATION...");
-(* try *)
- try
- let rc = Saturation.saturate caso_strano dbd ~depth ~width ~full
- ?timeout (proof, goal) in
- prerr_endline (Saturation.get_stats ());
- rc
- with exn ->
- prerr_endline (Saturation.get_stats ());
- raise exn
-
-(* with ProofEngineTypes.Fail _ -> *)
-(* normal_auto () *)
- ) else
- normal_auto ()
- in
match superposition with
| true ->
- ProofEngineTypes.mk_tactic
- (Saturation.superposition_tac ~target ~table ~subterms_only ~demod_table)
- | _ -> ProofEngineTypes.mk_tactic (auto_tac dbd)
+ (* this is the ugly hack to debug paramod *)
+ Saturation.superposition_tac
+ ~target ~table ~subterms_only ~demod_table (proof,goal)
+ | false ->
+ (* this is the real auto *)
+ let _, metasenv, _, _ = proof in
+ let _, context, goalty = CicUtil.lookup_meta goal metasenv in
+ let use_paramodulation =
+ paramodulation && Equality.term_is_equality goalty
+ in
+ if use_paramodulation then
+ try
+ let rc =
+ Saturation.saturate
+ ~auto:(callback_for_paramodulation dbd)
+ caso_strano dbd ~depth ~width ~full
+ ?timeout (proof, goal)
+ in
+ prerr_endline (Saturation.get_stats ());rc
+ with exn ->
+ prerr_endline (Saturation.get_stats ());raise exn
+ else
+ let universe =
+ AutoTypes.universe_of_goals dbd proof [goal] AutoTypes.empty_universe
+ in
+ let universe = (* we should get back a menv too XXX *)
+ AutoTypes.universe_of_context context metasenv universe
+ in
+ let oldmetasenv = metasenv in
+ match
+ Auto.auto universe AutoTypes.cache_empty context metasenv [goal]
+ {AutoTypes.default_flags with
+ AutoTypes.maxdepth = depth;
+ AutoTypes.maxwidth = width;
+(* AutoTypes.timeout = 0; *)
+ }
+ with
+ | None,cache ->
+ raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
+ | Some (subst,metasenv),cache ->
+ let proof,metasenv =
+ ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+ proof goal (CicMetaSubst.apply_subst subst) metasenv
+ in
+ let opened =
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+ ~newmetasenv:metasenv
+ in
+ proof,opened
;;
-(********************** applyS *******************)
+let auto_tac ~params ~dbd =
+ ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd)
+;;
+
+(* {{{ **************** applyS *******************)
let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term' ty termty goal_arity =
let (consthead,newmetasenv,arguments,_) =
| CicTypeChecker.TypeCheckerFailure msg ->
raise (ProofEngineTypes.Fail msg))
+(* }}} ********************************)
+
let pp_proofterm = Equality.pp_proofterm;;
projects / helm.git / blobdiff