Fixed a few bugs

[helm.git] / helm / software / components / ng_tactics / nnAuto.ml

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 96cd29606493ce1eac22b671ad6c8a389cd8ee99..7c52a7f72ebf7f0122acc2d8f20f4500d2cc0605 100644 (file)
--- 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