auto and auto_paramod are in nAuto

[helm.git] / helm / software / components / ng_tactics / nAuto.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 *)