From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 5 Oct 2009 14:36:13 +0000 (+0000)
Subject: new file for auto
X-Git-Tag: make_still_working~3381
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5aeba24517d4811e3dc08de5728a5ad8d47d41a7;p=helm.git

new file for auto
---

diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend
index 7a49c201b..b398d8132 100644
--- 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 7a49c201b..b398d8132 100644
--- 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 e99dd2422..b3d2bf069 100644
--- 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
index 000000000..d50db9053
--- /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
index 000000000..c1d24e70b
--- /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 760d84e8d..5da8f677c 100644
--- 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
 ;;