X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=7c52a7f72ebf7f0122acc2d8f20f4500d2cc0605;hb=320c0f89a7e31e996b6eff2b4165eb74e8141cec;hp=96cd29606493ce1eac22b671ad6c8a389cd8ee99;hpb=6c3b2a89bd14bb8a96e56565b725dd635effc2e5;p=helm.git

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 96cd29606..7c52a7f72 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -161,10 +161,12 @@ let height_of_goals status =
 ;;
 
 (* =============================== paramod =========================== *)
-let solve fast status eq_cache goal =
+let solve f 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
@@ -205,7 +207,7 @@ let solve fast status eq_cache goal =
 ;;
 
 let fast_eq_check eq_cache status goal =
-  match solve true status eq_cache goal with
+  match solve NCicParamod.fast_eq_check status eq_cache goal with
   | [] -> raise (Error (lazy "no proof found",None))
   | s::_ -> s
 ;;
@@ -254,7 +256,7 @@ let fast_eq_check_tac ~params s =
 ;;
 
 let paramod eq_cache status goal =
-  match solve false status eq_cache goal with
+  match solve NCicParamod.paramod status eq_cache goal with
   | [] -> raise (Error (lazy "no proof found",None))
   | s::_ -> s
 ;;
@@ -264,6 +266,17 @@ let paramod_tac ~params s =
   NTactics.distribute_tac (paramod unit_eq) s
 ;;
 
+let demod eq_cache status goal =
+  match solve NCicParamod.demod status eq_cache goal with
+  | [] -> raise (Error (lazy "no progress",None))
+  | s::_ -> s
+;;
+
+let demod_tac ~params s = 
+  let unit_eq = index_local_equations s#eq_cache s in   
+  NTactics.distribute_tac (demod unit_eq) s
+;;
+
 (*
 let fast_eq_check_tac_all  ~params eq_cache status = 
   let g,_,_ = current_goal status in
@@ -468,6 +481,7 @@ let smart_apply t unit_eq status g =
   (* let ggty = mk_cic_term context gty in *)
   let status, t = disambiguate status ctx t None in
   let status,t = term_of_cic_term status t ctx in
+  let _,_,metasenv,subst,_ = status#obj in
   let ty = NCicTypeChecker.typeof subst metasenv ctx t in
   let ty,metasenv,args = 
     match gty with
@@ -478,9 +492,13 @@ let smart_apply t unit_eq status g =
 	  NCicMetaSubst.saturate metasenv subst ctx ty 0 in
   let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
   let status = status#set_obj (n,h,metasenv,subst,o) in
-  let pterm = if args=[] then t else NCic.Appl(t::args) in
-  debug_print(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm)));
-  debug_print(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty)));
+  let pterm = if args=[] then t else 
+    match t with
+      | NCic.Appl l -> NCic.Appl(l@args) 
+      | _ -> NCic.Appl(t::args) 
+  in
+  noprint(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm)));
+  noprint(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty)));
   let eq_coerc =       
     let uri = 
       NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in
@@ -495,7 +513,7 @@ let smart_apply t unit_eq status g =
       let _,_,metasenv,subst,_ = status#obj in
       let _,ctx,jty = List.assoc j metasenv in
       let jty = NCicUntrusted.apply_subst subst ctx jty in
-        debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
+        print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
         fast_eq_check unit_eq status j
     with
       | Error _ as e -> debug_print (lazy "error"); raise e
@@ -1148,7 +1166,14 @@ let rec auto_clusters ?(top=false)
     if depth = 0 then raise (Proved status)
     else 
       let status = NTactics.merge_tac status in
-	auto_clusters flags signature (cache:cache) (depth-1) status
+	let cache =
+	let l,tree = cache.under_inspection in
+	  match l with 
+	    | [] -> cache (* possible because of intros that cleans the cache *)
+	    | a::tl -> let tree = rm_from_th a tree a in
+	       {cache with under_inspection = tl,tree} 
+	in 
+	 auto_clusters flags signature cache (depth-1) status
   else if List.length goals < 2 then
     auto_main flags signature cache depth status
   else
@@ -1221,7 +1246,7 @@ auto_main flags signature (cache:cache) depth status: unit =
 	let cache =
 	  let l,tree = cache.under_inspection in
 	    match l with 
-	      | [] -> assert false
+	      | [] -> cache (* possible because of intros that cleans the cache *)
 	      | a::tl -> let tree = rm_from_th a tree a in
 		  {cache with under_inspection = tl,tree} 
 	in 
@@ -1230,6 +1255,13 @@ auto_main flags signature (cache:cache) depth status: unit =
 	if depth > 0 && move_to_side depth status
 	then 
 	  let status = NTactics.merge_tac status in
+	  let cache =
+	    let l,tree = cache.under_inspection in
+	      match l with 
+	        | [] -> cache (* possible because of intros that cleans the cache*)
+	        | a::tl -> let tree = rm_from_th a tree a in
+		    {cache with under_inspection = tl,tree} 
+	  in 
 	    auto_clusters flags signature cache (depth-1) status 
 	else
         let ng = List.length goals in