From f1fc99e982ca6c9c939504c4dcf773edf582792a Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 18 Mar 2010 11:23:53 +0000
Subject: [PATCH] New demodulation tactics (mostly for debugging purposes). It
 is called with "nauto demod".

---
 helm/software/components/ng_tactics/nAuto.ml  |  2 ++
 helm/software/components/ng_tactics/nnAuto.ml | 21 +++++++++++++++----
 .../software/components/ng_tactics/nnAuto.mli |  4 ++++
 3 files changed, 23 insertions(+), 4 deletions(-)

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 53c87673b..65252eaf9 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -1709,6 +1709,8 @@ let auto_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 
diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 460bf2d53..f314d3eb3 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -161,16 +161,18 @@ let height_of_goals status =
 ;;
 
 (* =============================== 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 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
@@ -205,7 +207,7 @@ let solve fast status eq_cache 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
 ;;
@@ -254,7 +256,7 @@ let fast_eq_check_tac ~params s =
 ;;
 
 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
 ;;
@@ -264,6 +266,17 @@ let paramod_tac ~params 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
diff --git a/helm/software/components/ng_tactics/nnAuto.mli b/helm/software/components/ng_tactics/nnAuto.mli
index 7d59d395d..13a519d70 100644
--- a/helm/software/components/ng_tactics/nnAuto.mli
+++ b/helm/software/components/ng_tactics/nnAuto.mli
@@ -20,6 +20,10 @@ val paramod_tac:
   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
 
-- 
2.39.2