From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 18 Jan 2010 10:04:51 +0000 (+0000)
Subject: New paramod tac.
X-Git-Tag: make_still_working~3112
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8e15fc948d1c5dafb982701790fb085f34a7dd10;p=helm.git

New paramod tac.
---

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index e2ddda033..6044f3a34 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -56,7 +56,8 @@ let menv_closure status gl =
 (* we call a "fact" an object whose hypothesis occur in the goal 
    or in types of goal-variables *)
 let is_a_fact status ty =   
-  let status, ty, _ = saturate ~delta:max_int status ty in
+  let status, ty, _ = saturate ~delta:0 status ty in
+  debug_print (lazy (ppterm status ty));
   let g_metas = metas_of_term status ty in
   let clos = menv_closure status g_metas in
   let _,_,metasenv,_,_ = status#obj in
@@ -84,34 +85,10 @@ let current_goal 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 (ctx_of gty) t None 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 (Error (lazy "no proof found",None))
-  | (pt, _, metasenv, subst)::_ -> 
-      let status = status#set_obj (n,h,metasenv,subst,o) in
-      instantiate status goal (mk_cic_term (ctx_of gty) pt)
-;;
-
-let auto_paramod_tac ~params status = 
-  NTactics.distribute_tac (auto_paramod ~params) status
-;;
-
-let fast_eq_check_all status eq_cache goal =
+let solve fast status eq_cache goal =
+  let f = 
+    if fast then NCicParamod.fast_eq_check
+    else NCicParamod.paramod in
   let n,h,metasenv,subst,o = status#obj in
   let gname, ctx, gty = List.assoc goal metasenv in
   let gty = NCicUntrusted.apply_subst subst ctx gty in
@@ -120,8 +97,8 @@ let fast_eq_check_all status eq_cache goal =
       print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
       let stamp = Unix.gettimeofday () in 
       let metasenv, subst, pt, pty =
-	NCicRefiner.typeof 
-       	  (status#set_coerc_db NCicCoercion.empty_db) 
+	NCicRefiner.typeof status
+       	 (* (status#set_coerc_db NCicCoercion.empty_db) *)
 	  metasenv subst ctx pt None in
 	print (lazy ("synt: "^(NCicPp.ppterm ctx subst metasenv pty)));
 	let metasenv, subst =
@@ -140,15 +117,22 @@ let fast_eq_check_all status eq_cache goal =
 	  let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
 	  let subst = (goal,(gname,ctx,pt,pty)) :: subst in
 	    Some (status#set_obj (n,h,metasenv,subst,o))
-    with _ -> prerr_endline "WARNING: refining in fast_eq_check failed"; None 
+    with 
+	NCicRefiner.RefineFailure msg 
+      | NCicRefiner.Uncertain msg ->
+	  debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
+			snd (Lazy.force msg))); None
+      | NCicRefiner.AssertFailure msg -> 
+	  debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
+			Lazy.force msg)); None
+      | _ -> None
     in
     HExtlib.filter_map build_status
-      (NCicParamod.fast_eq_check status metasenv subst ctx 
-	 eq_cache (NCic.Rel ~-1,gty))
+      (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
 ;;
 
 let fast_eq_check eq_cache status goal =
-  match fast_eq_check_all status eq_cache goal with
+  match solve true status eq_cache goal with
   | [] -> raise (Error (lazy "no proof found",None))
   | s::_ -> s
 ;;
@@ -191,6 +175,17 @@ let fast_eq_check_tac ~params s =
   dist_fast_eq_check unit_eq s
 ;;
 
+let paramod eq_cache status goal =
+  match solve false status eq_cache goal with
+  | [] -> raise (Error (lazy "no proof found",None))
+  | s::_ -> s
+;;
+
+let paramod_tac ~params s = 
+  let unit_eq = index_local_equations s#eq_cache s in   
+  NTactics.distribute_tac (paramod unit_eq) s
+;;
+
 (*
 let fast_eq_check_tac_all  ~params eq_cache status = 
   let g,_,_ = current_goal status in
@@ -203,6 +198,17 @@ let fast_eq_check_tac_all  ~params eq_cache status =
 ;;
 *)
 
+(*
+let demod status eq_cache goal =
+  let n,h,metasenv,subst,o = status#obj in
+  let gname, ctx, gty = List.assoc goal metasenv in
+  let gty = NCicUntrusted.apply_subst subst ctx gty in
+
+let demod_tac ~params s = 
+  let unit_eq = index_local_equations s#eq_cache s in   
+  dist_fast_eq_check unit_eq s
+*)
+
 (*************** subsumption ****************)
 
 let close_wrt_context =
@@ -1470,19 +1476,27 @@ let get_candidates ?(smart=true) status cache signature gty =
 ;;
 
 let applicative_case depth signature status flags gty (cache:cache) =
-  app_counter:= !app_counter+1;
+  app_counter:= !app_counter+1; 
+  let _,_,metasenv,subst,_ = status#obj in
+  let context = ctx_of gty in
   let tcache = cache.facts in
+  let is_eq =   
+    let status, t = term_of_cic_term status gty context  in 
+    NCicParamod.is_equation metasenv subst context t 
+  in
+  debug_print(lazy (string_of_bool is_eq)); 
   let candidates, smart_candidates = 
-    get_candidates status tcache signature gty in
-  print ~depth
+    get_candidates ~smart:(not is_eq) status tcache signature gty in
+  debug_print ~depth
     (lazy ("candidates: " ^ string_of_int (List.length candidates)));
-  print ~depth
+  debug_print ~depth
     (lazy ("smart candidates: " ^ 
 	     string_of_int (List.length smart_candidates)));
+  let sm = if is_eq then 0 else 2 in
   let elems = 
     List.fold_left 
       (fun elems cand ->
-        match try_candidate (~smart:2) 
+        match try_candidate (~smart:sm) 
 	  flags depth status cache.unit_eq cand with
         | None -> elems
         | Some x -> x::elems)
@@ -1613,17 +1627,19 @@ let do_something signature flags status g depth gty cache =
   (* whd *)
   let l = reduce ~depth status g in
   (* backward aplications *)
-  let l1 = applicative_case depth signature status flags gty cache in
-  (* fast paramodulation *) 
-  let l2 = 
+  let l1 = 
     List.map 
       (fun s ->
 	 incr candidate_no;
 	 ((!candidate_no,Ast.Ident("__paramod",None)),s))
-      (auto_eq_check cache.unit_eq status)
+      (auto_eq_check cache.unit_eq status) in
+  let l2 = 
+    if (l1 <> []) then []
+    else applicative_case depth signature status flags gty cache 
+  (* fast paramodulation *) 
   in
-  (* states in l2 have have an set of subgoals: no point to sort them *)
-    l2 @ (sort_new_elems (l@l1)), cache
+  (* states in l1 have have an empty set of subgoals: no point to sort them *)
+    l1 @ (sort_new_elems (l@l2)), cache
 ;;
 
 let pp_goal = function