new file for auto

diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend
index 7a49c201b82ace4e34fbc67990d96894c7d68b94..b398d8132daa50a95d29cb1123bd8fa585e01998 100644 (file)
--- a/helm/software/components/ng_tactics/.depend
+++ b/helm/software/components/ng_tactics/.depend
@@ -1,6 +1,7 @@
 nCicTacReduction.cmi: 
 nTacStatus.cmi: 
 nCicElim.cmi: 
+nAuto.cmi: nTacStatus.cmi 
 nTactics.cmi: nTacStatus.cmi 
 nInversion.cmi: nTacStatus.cmi 
 nCicTacReduction.cmo: nCicTacReduction.cmi 
@@ -9,7 +10,9 @@ nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi
 nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi 
 nCicElim.cmo: nCicElim.cmi 
 nCicElim.cmx: nCicElim.cmi 
-nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi 
-nTactics.cmx: nTacStatus.cmx nCicElim.cmx nTactics.cmi 
+nAuto.cmo: nTacStatus.cmi nAuto.cmi 
+nAuto.cmx: nTacStatus.cmx nAuto.cmi 
+nTactics.cmo: nTacStatus.cmi nCicElim.cmi nAuto.cmi nTactics.cmi 
+nTactics.cmx: nTacStatus.cmx nCicElim.cmx nAuto.cmx nTactics.cmi 
 nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi 
 nInversion.cmx: nTactics.cmx nCicElim.cmx nInversion.cmi 

diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt
index 7a49c201b82ace4e34fbc67990d96894c7d68b94..b398d8132daa50a95d29cb1123bd8fa585e01998 100644 (file)
--- a/helm/software/components/ng_tactics/.depend.opt
+++ b/helm/software/components/ng_tactics/.depend.opt
@@ -1,6 +1,7 @@
 nCicTacReduction.cmi: 
 nTacStatus.cmi: 
 nCicElim.cmi: 
+nAuto.cmi: nTacStatus.cmi 
 nTactics.cmi: nTacStatus.cmi 
 nInversion.cmi: nTacStatus.cmi 
 nCicTacReduction.cmo: nCicTacReduction.cmi 
@@ -9,7 +10,9 @@ nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi
 nTacStatus.cmx: nCicTacReduction.cmx nTacStatus.cmi 
 nCicElim.cmo: nCicElim.cmi 
 nCicElim.cmx: nCicElim.cmi 
-nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi 
-nTactics.cmx: nTacStatus.cmx nCicElim.cmx nTactics.cmi 
+nAuto.cmo: nTacStatus.cmi nAuto.cmi 
+nAuto.cmx: nTacStatus.cmx nAuto.cmi 
+nTactics.cmo: nTacStatus.cmi nCicElim.cmi nAuto.cmi nTactics.cmi 
+nTactics.cmx: nTacStatus.cmx nCicElim.cmx nAuto.cmx nTactics.cmi 
 nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi 
 nInversion.cmx: nTactics.cmx nCicElim.cmx nInversion.cmi 

diff --git a/helm/software/components/ng_tactics/Makefile b/helm/software/components/ng_tactics/Makefile
index e99dd242222029ecaf0b79a2a6ac21be040627a4..b3d2bf06918fd9ebd5631f38df7157dcd8852d57 100644 (file)
--- a/helm/software/components/ng_tactics/Makefile
+++ b/helm/software/components/ng_tactics/Makefile
@@ -4,6 +4,7 @@ INTERFACE_FILES = \
        nCicTacReduction.mli \
        nTacStatus.mli \
        nCicElim.mli \
+       nAuto.mli \
        nTactics.mli \
        nInversion.mli
 

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
new file mode 100644 (file)
index 0000000..d50db90
--- /dev/null
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -0,0 +1,32 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+open Printf
+
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+
+open Continuationals.Stack
+open NTacStatus
+module Ast = CicNotationPt
+
+let auto_tac status =
+  prerr_endline "I teoremi noti sono";
+  NDiscriminationTree.DiscriminationTree.iter status#auto_cache
+    (fun _ t -> 
+      List.iter (fun t ->
+       prerr_endline
+        (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t))
+       (NDiscriminationTree.TermSet.elements t));
+  status
+;;

diff --git a/helm/software/components/ng_tactics/nAuto.mli b/helm/software/components/ng_tactics/nAuto.mli
new file mode 100644 (file)
index 0000000..c1d24e7
--- /dev/null
+++ b/helm/software/components/ng_tactics/nAuto.mli
@@ -0,0 +1,14 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+val auto_tac : 's NTacStatus.tactic

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 760d84e8d90bdf22157a405b30ee4d4afe0c5b51..5da8f677cffd07791f7c9ab14789d175e4de56a7 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -679,6 +679,7 @@ let auto ~params:(l,_) status goal =
 ;;
 
 let auto_tac ~params status =
-  distribute_tac (auto ~params) status
+  (* distribute_tac (auto ~params) status *)
+  NAuto.auto_tac status
 ;;