summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
8c678be)
It is called with "nauto demod".
let auto_tac ~params:(_,flags as params) =
if List.mem_assoc "paramodulation" flags then
auto_paramod_tac ~params
let auto_tac ~params:(_,flags as params) =
if List.mem_assoc "paramodulation" flags then
auto_paramod_tac ~params
+ else if List.mem_assoc "demod" flags then
+ NnAuto.demod_tac ~params
else if List.mem_assoc "paramod" flags then
NnAuto.paramod_tac ~params
else if List.mem_assoc "fast_paramod" flags then
else if List.mem_assoc "paramod" flags then
NnAuto.paramod_tac ~params
else if List.mem_assoc "fast_paramod" flags then
;;
(* =============================== paramod =========================== *)
;;
(* =============================== paramod =========================== *)
-let solve fast status eq_cache goal =
+let solve f status eq_cache goal =
+(*
let f =
if fast then NCicParamod.fast_eq_check
else NCicParamod.paramod in
let f =
if fast then NCicParamod.fast_eq_check
else NCicParamod.paramod in
let n,h,metasenv,subst,o = status#obj in
let gname, ctx, gty = List.assoc goal metasenv in
let gty = NCicUntrusted.apply_subst subst ctx gty in
let build_status (pt, _, metasenv, subst) =
try
let n,h,metasenv,subst,o = status#obj in
let gname, ctx, gty = List.assoc goal metasenv in
let gty = NCicUntrusted.apply_subst subst ctx gty in
let build_status (pt, _, metasenv, subst) =
try
- debug_print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
+ print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
let stamp = Unix.gettimeofday () in
let metasenv, subst, pt, pty =
(* NCicRefiner.typeof status
let stamp = Unix.gettimeofday () in
let metasenv, subst, pt, pty =
(* NCicRefiner.typeof status
;;
let fast_eq_check eq_cache status goal =
;;
let fast_eq_check eq_cache status goal =
- match solve true status eq_cache goal with
+ match solve NCicParamod.fast_eq_check status eq_cache goal with
| [] -> raise (Error (lazy "no proof found",None))
| s::_ -> s
;;
| [] -> raise (Error (lazy "no proof found",None))
| s::_ -> s
;;
;;
let paramod eq_cache status goal =
;;
let paramod eq_cache status goal =
- match solve false status eq_cache goal with
+ match solve NCicParamod.paramod status eq_cache goal with
| [] -> raise (Error (lazy "no proof found",None))
| s::_ -> s
;;
| [] -> raise (Error (lazy "no proof found",None))
| s::_ -> s
;;
NTactics.distribute_tac (paramod unit_eq) s
;;
NTactics.distribute_tac (paramod unit_eq) s
;;
+let demod eq_cache status goal =
+ match solve NCicParamod.demod status eq_cache goal with
+ | [] -> raise (Error (lazy "no progress",None))
+ | s::_ -> s
+;;
+
+let demod_tac ~params s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ NTactics.distribute_tac (demod unit_eq) s
+;;
+
(*
let fast_eq_check_tac_all ~params eq_cache status =
let g,_,_ = current_goal status in
(*
let fast_eq_check_tac_all ~params eq_cache status =
let g,_,_ = current_goal status in
params:(NTacStatus.tactic_term list * (string * string) list) ->
's NTacStatus.tactic
params:(NTacStatus.tactic_term list * (string * string) list) ->
's NTacStatus.tactic
+val demod_tac:
+ params:(NTacStatus.tactic_term list * (string * string) list) ->
+ 's NTacStatus.tactic
+
val smart_apply_tac:
NTacStatus.tactic_term -> 's NTacStatus.tactic
val smart_apply_tac:
NTacStatus.tactic_term -> 's NTacStatus.tactic