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 9fa8dbb000a30e17e20b5f221b142b5cf77db098..871ec01b8dde9a5c3e019488999049af1ebcf4f7 100644 (file)
--- 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 b398d8132daa50a95d29cb1123bd8fa585e01998..615a158e92abe4180fbde0a74ad4bdfc2b0f6efe 100644 (file)
--- 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 b398d8132daa50a95d29cb1123bd8fa585e01998..615a158e92abe4180fbde0a74ad4bdfc2b0f6efe 100644 (file)
--- 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 b3d2bf06918fd9ebd5631f38df7157dcd8852d57..1db1ad6e76f975b9f4bc5340f86a39d4a77e1f05 100644 (file)
--- 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 d50db90533e0b5e14c266ab483d6e1aa5de2c4ef..60587e1e34ec3277dee4a6c0c42cbd8424f6707d 100644 (file)
--- 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 c1d24e70be8bd86bdd5a139ab469dd9d2a393394..f8f5ae4e212a40c234f0534fe9923bd8367615f0 100644 (file)
--- 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 5da8f677cffd07791f7c9ab14789d175e4de56a7..1cedd2d3d3107325c363cbc29d6ee17ad3fc8c89 100644 (file)
--- 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 8211adb37ca6c26e91e76716811f826de7ca0e0f..b8659c3574fe63dfb34a170f052e2649408bc70f 100644 (file)
--- 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