From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 5 Oct 2009 14:53:10 +0000 (+0000)
Subject: auto and auto_paramod are in nAuto
X-Git-Tag: make_still_working~3380
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=39fb4421e9bea7f21f46c2fa1145c248c08d16b6;p=helm.git

auto and auto_paramod are in nAuto
---

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 9fa8dbb00..871ec01b8 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -692,7 +692,7 @@ let eval_ng_tac tac =
           (text,prefix_len,concl))
        ) seqs)
   | GrafiteAst.NAuto (_loc, (l,a)) ->
-      NTactics.auto_tac
+      NAuto.auto_tac
 	~params:(List.map (fun x -> "",0,x) l,a)
   | GrafiteAst.NBranch _ -> NTactics.branch_tac 
   | GrafiteAst.NCases (_loc, what, where) ->
diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend
index b398d8132..615a158e9 100644
--- a/helm/software/components/ng_tactics/.depend
+++ b/helm/software/components/ng_tactics/.depend
@@ -12,7 +12,7 @@ nCicElim.cmo: nCicElim.cmi
 nCicElim.cmx: nCicElim.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 
+nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi 
+nTactics.cmx: nTacStatus.cmx nCicElim.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 b398d8132..615a158e9 100644
--- a/helm/software/components/ng_tactics/.depend.opt
+++ b/helm/software/components/ng_tactics/.depend.opt
@@ -12,7 +12,7 @@ nCicElim.cmo: nCicElim.cmi
 nCicElim.cmx: nCicElim.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 
+nTactics.cmo: nTacStatus.cmi nCicElim.cmi nTactics.cmi 
+nTactics.cmx: nTacStatus.cmx nCicElim.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 b3d2bf069..1db1ad6e7 100644
--- a/helm/software/components/ng_tactics/Makefile
+++ b/helm/software/components/ng_tactics/Makefile
@@ -4,8 +4,8 @@ INTERFACE_FILES = \
 	nCicTacReduction.mli \
 	nTacStatus.mli \
 	nCicElim.mli \
-	nAuto.mli \
 	nTactics.mli \
+	nAuto.mli \
 	nInversion.mli
 
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index d50db9053..60587e1e3 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -20,7 +20,36 @@ open Continuationals.Stack
 open NTacStatus
 module Ast = CicNotationPt
 
-let auto_tac status =
+(* =================================== paramod =========================== *)
+let auto_paramod ~params:(l,_) status goal =
+  let gty = get_goalty status goal in
+  let n,h,metasenv,subst,o = status#obj in
+  let status,t = term_of_cic_term status gty (ctx_of gty) in
+  let status, l = 
+    List.fold_left
+      (fun (status, l) t ->
+        let status, t = disambiguate status t None (ctx_of gty) in
+        let status, ty = typeof status (ctx_of t) t in
+        let status, t =  term_of_cic_term status t (ctx_of gty) in
+        let status, ty = term_of_cic_term status ty (ctx_of ty) in
+        (status, (t,ty) :: l))
+      (status,[]) l
+  in
+  match
+    NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
+  with
+  | [] -> raise (NTacStatus.Error (lazy "no proof found",None))
+  | (pt, metasenv, subst)::_ -> 
+      let status = status#set_obj (n,h,metasenv,subst,o) in
+      instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
+;;
+
+let auto_paramod_tac ~params status = 
+  NTactics.distribute_tac (auto_paramod ~params) status
+;;
+
+(* =================================== auto =========================== *)
+let auto_tac ~params status =
   prerr_endline "I teoremi noti sono";
   NDiscriminationTree.DiscriminationTree.iter status#auto_cache
     (fun _ t -> 
@@ -30,3 +59,13 @@ let auto_tac status =
        (NDiscriminationTree.TermSet.elements t));
   status
 ;;
+
+(* ========================= dispatching of auto/auto_paramod ============ *)
+let auto_tac ~params:(_,flags as params) =
+  if List.mem_assoc "paramodulation" flags then 
+    auto_paramod_tac ~params  
+  else 
+    auto_tac ~params
+;;
+
+(* EOF *)
diff --git a/helm/software/components/ng_tactics/nAuto.mli b/helm/software/components/ng_tactics/nAuto.mli
index c1d24e70b..f8f5ae4e2 100644
--- a/helm/software/components/ng_tactics/nAuto.mli
+++ b/helm/software/components/ng_tactics/nAuto.mli
@@ -11,4 +11,10 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-val auto_tac : 's NTacStatus.tactic
+val auto_tac:
+  params:(NTacStatus.tactic_term list * (string * string) list) -> 
+   's NTacStatus.tactic
+
+val auto_paramod_tac:
+  params:(NTacStatus.tactic_term list * (string * string) list) -> 
+   's NTacStatus.tactic
diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 5da8f677c..1cedd2d3d 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -655,31 +655,3 @@ let assert_tac seqs status =
      ) status
 ;;
 
-let auto ~params:(l,_) status goal =
-  let gty = get_goalty status goal in
-  let n,h,metasenv,subst,o = status#obj in
-  let status,t = term_of_cic_term status gty (ctx_of gty) in
-  let status, l = 
-    List.fold_left
-      (fun (status, l) t ->
-        let status, t = disambiguate status t None (ctx_of gty) in
-        let status, ty = typeof status (ctx_of t) t in
-        let status, t =  term_of_cic_term status t (ctx_of gty) in
-        let status, ty = term_of_cic_term status ty (ctx_of ty) in
-        (status, (t,ty) :: l))
-      (status,[]) l
-  in
-  match
-    NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
-  with
-  | [] -> raise (NTacStatus.Error (lazy "no proof found",None))
-  | (pt, metasenv, subst)::_ -> 
-      let status = status#set_obj (n,h,metasenv,subst,o) in
-      instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
-;;
-
-let auto_tac ~params status =
-  (* distribute_tac (auto ~params) status *)
-  NAuto.auto_tac status
-;;
-
diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 8211adb37..b8659c357 100644
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -59,9 +59,5 @@ val assert_tac:
  ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
   's NTacStatus.tactic
 
-val auto_tac:
-  params:(NTacStatus.tactic_term list * (string * string) list) -> 
-   's NTacStatus.tactic
-
 val constructor_tac : 
         ?num:int -> args:NTacStatus.tactic_term list -> 's NTacStatus.tactic