From 5aeba24517d4811e3dc08de5728a5ad8d47d41a7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 Oct 2009 14:36:13 +0000 Subject: [PATCH] new file for auto --- helm/software/components/ng_tactics/.depend | 7 ++-- .../components/ng_tactics/.depend.opt | 7 ++-- helm/software/components/ng_tactics/Makefile | 1 + helm/software/components/ng_tactics/nAuto.ml | 32 +++++++++++++++++++ helm/software/components/ng_tactics/nAuto.mli | 14 ++++++++ .../components/ng_tactics/nTactics.ml | 3 +- 6 files changed, 59 insertions(+), 5 deletions(-) create mode 100644 helm/software/components/ng_tactics/nAuto.ml create mode 100644 helm/software/components/ng_tactics/nAuto.mli 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 ;; -- 2.39.2