let default_depth = 5
let default_width = 3
-(*
-let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
+let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
()
=
let auto_tac dbd (proof,goal) =
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 "No Applicable theorem")
+ raise (ProofEngineTypes.Fail (lazy "No Applicable theorem"))
| (_,(proof,[],_))::_ ->
let t2 = Unix.gettimeofday () in
debug_print (lazy "AUTO_TAC HA FINITO");
(proof,[])
| _ -> assert false
in
- ProofEngineTypes.mk_tactic (auto_tac dbd)
+ auto_tac dbd
;;
-*)
-(*
-let paramodulation_tactic = ref
- (fun dbd ?full ?depth ?width status ->
- raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));;
-
-let term_is_equality = ref
- (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);;
-*)
-
-let bool name params =
- try let _ = List.assoc name params in true with
- | Not_found -> false
+let bool params name default =
+ try
+ let s = List.assoc name params in
+ if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
+ else if s = "0" || s = "false" || s = "no" || s= "off" then false
+ else
+ let msg = "Unrecognized value for parameter "^name^"\n" in
+ let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
+ raise (ProofEngineTypes.Fail (lazy msg))
+ with Not_found -> default
;;
-let string name params =
+let string params name default =
try List.assoc name params with
- | Not_found -> ""
+ | Not_found -> default
;;
-let int name default params =
+let int params name default =
try int_of_string (List.assoc name params) with
| Not_found -> default
| Failure _ ->
raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
;;
-(*
-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" 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 superposition = bool "superposition" params in
- let target = string "target" params in
- let table = string "table" params in
- let subterms_only = bool "subterms_only" params in
- let caso_strano = bool "caso_strano" params in
- let demod_table = string "demod_table" params in
- let timeout =
- try Some (float_of_string timeout) with Failure _ -> None
- in
+ let int = int params
+ and string = string params
+ and bool = bool params in
+ let newauto = bool "new" false in
+ let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
+ let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
+ let timeout = int "timeout" 0 in
+ let use_paramod = bool "use_paramod" true in
+ let use_only_paramod = bool "paramodulation" false in
+ (* hacks to debug paramod *)
+ let superposition = bool "superposition" false in
+ let target = string "target" "" in
+ let table = string "table" "" in
+ let subterms_only = bool "subterms_only" false in
+ let demod_table = string "demod_table" "" in
+ let newauto = if use_only_paramod then true else newauto in
match superposition with
| true ->
(* this is the ugly hack to debug paramod *)
Saturation.superposition_tac
~target ~table ~subterms_only ~demod_table (proof,goal)
| false ->
+ if not newauto then
+ auto_tac_old ~depth ~width ~dbd () (proof,goal)
+ else
(* 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
+ let cache =
+ let cache =
+ AutoCache.cache_add_context context metasenv AutoCache.cache_empty
+ in
+ if use_only_paramod then (* only paramod *)
+ cache
+ else
+ AutoCache.cache_add_library dbd proof [goal] cache
+ in
+ let oldmetasenv = metasenv in
+ let flags = {
+ AutoTypes.maxdepth =
+ if use_only_paramod then 2 else depth;
+ AutoTypes.maxwidth = width;
+ AutoTypes.timeout =
+ if timeout = 0 then float_of_int timeout
+ else Unix.gettimeofday() +. (float_of_int timeout);
+ AutoTypes.use_paramod = use_paramod;
+ AutoTypes.use_only_paramod = use_only_paramod;
+ AutoTypes.dont_cache_failures = false
+ }
in
- if use_paramodulation then
- try
- let rc =
- Saturation.saturate
- ~auto:(callback_for_paramodulation dbd)
- caso_strano dbd ~depth ~width ~full
- ?timeout (proof, goal)
+ match Auto.auto dbd cache context metasenv [goal] flags 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
- 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
+ let opened =
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+ ~newmetasenv:metasenv
+ in
+ proof,opened
;;
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,_) =
- ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
- let term'' = match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) in
- let proof',metasenv =
- let (puri,metasenv,pbo,pty) = proof in
- (puri,newmetasenv,pbo,pty),metasenv
- in
- let proof'',goals =
- match LibraryObjects.eq_URI () with
- | Some uri ->
- ProofEngineTypes.apply_tactic
- (Tacticals.then_
- ~start:(PrimitiveTactics.letin_tac term''(*Tacticals.id_tac*))
- ~continuation:
- (PrimitiveTactics.cut_tac
- (CicSubstitution.lift 1
- (Cic.Appl
- [Cic.MutInd (uri,0,[]);
- Cic.Sort Cic.Prop;
- consthead;
- ty])))) (proof',goal)
- | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
- in
- match goals with
- [g1;g2] ->
- let proof'',goals =
- ProofEngineTypes.apply_tactic
- (auto_tac ~params:["caso_strano","on";"paramodulation","on"] ~dbd) (proof'',g2)
- in
- let proof'',goals =
- ProofEngineTypes.apply_tactic
- (Tacticals.then_
- ~start:(EqualityTactics.rewrite_tac ~direction:`RightToLeft
- ~pattern:(ProofEngineTypes.conclusion_pattern None) (Cic.Rel 1))
- ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2))
- ) (proof'',g1)
- in
- proof'',
- (*CSC: Brrrr.... *)
- ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
- ~newmetasenv:(let _,m,_,_ = proof'' in m)
- | _ -> assert false
-
-let rec count_prods context ty =
- match CicReduction.whd context ty with
- Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
- | _ -> 0
-
-let applyS_tac ~dbd ~term (proof, goal) =
- let module T = CicTypeChecker in
- let module R = CicReduction in
- let module C = Cic in
- let (_,metasenv,_,_) = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
- let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
- match term with
- C.Var (uri,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.Var (uri,exp_named_subst')
- | C.Const (uri,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.Const (uri,exp_named_subst')
- | C.MutInd (uri,tyno,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.MutInd (uri,tyno,exp_named_subst')
- | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.MutConstruct (uri,tyno,consno,exp_named_subst')
- | _ -> [],newmeta,[],term
- in
- let metasenv' = metasenv@newmetasenvfragment in
- let termty,_ =
- CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
- in
- let termty =
- CicSubstitution.subst_vars exp_named_subst_diff termty in
- let goal_arity = count_prods context ty in
- let res =
- new_metasenv_and_unify_and_t dbd proof goal
- newmeta' metasenv' context term' ty termty goal_arity
- in
- res
-
-let applyS_tac ~dbd ~term =
- ProofEngineTypes.mk_tactic
- (fun status ->
- try applyS_tac ~dbd ~term status
- with
- | CicUnification.UnificationFailure msg
- | CicTypeChecker.TypeCheckerFailure msg ->
- raise (ProofEngineTypes.Fail msg))
-
-(* }}} ********************************)
-
let pp_proofterm = Equality.pp_proofterm;;
projects / helm.git / blobdiff