X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=57f99b52b405c48f1f26c8de6483046778ef1292;hb=95adf6dc8e29a71adc34e71eafe3f427990126e0;hp=1d4738d952029f98835a93fbefefe7af21516313;hpb=3dadfa509ace9184e5cf33a46d44c48c6fbed31b;p=helm.git

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 1d4738d95..57f99b52b 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
@@ -193,11 +195,15 @@ let solve fast status eq_cache goal =
     with 
         NCicRefiner.RefineFailure msg 
       | NCicRefiner.Uncertain msg ->
-          debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
-                        snd (Lazy.force msg))); None
+          print (lazy ("WARNING: refining in fast_eq_check failed\n" ^
+                        snd (Lazy.force msg) ^	
+			"\n in the environment\n" ^ 
+			NCicPp.ppmetasenv subst metasenv)); None
       | NCicRefiner.AssertFailure msg -> 
-          debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
-                        Lazy.force msg)); None
+          print (lazy ("WARNING: refining in fast_eq_check failed" ^
+                        Lazy.force msg ^
+			"\n in the environment\n" ^ 
+			NCicPp.ppmetasenv subst metasenv)); None
       | _ -> None
     in
     HExtlib.filter_map build_status
@@ -205,7 +211,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 +260,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 +270,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 +485,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 +496,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
@@ -630,9 +652,26 @@ type flags = {
 type cache =
     {facts : th_cache; (* positive results *)
      under_inspection : cic_term list * th_cache; (* to prune looping *)
-     unit_eq : NCicParamod.state
+     unit_eq : NCicParamod.state;
+     trace: Ast.term list
     }
 
+let add_to_trace cache t =
+  match t with
+    | Ast.NRef _ -> {cache with trace = t::cache.trace}
+    | Ast.NCic _  (* local candidate *)
+    | _  -> (*not an application *) cache 
+
+(* not used
+let remove_from_trace cache t =
+  match t with
+    | Ast.NRef _ -> 
+	(match cache.trace with 
+	   |  _::tl -> {cache with trace = tl}
+           | _ -> assert false)
+    | Ast.NCic _  (* local candidate *)
+    |  _  -> (*not an application *) cache *)
+
 type sort = T | P
 type goal = int * sort (* goal, depth, sort *)
 type fail = goal * cic_term
@@ -640,7 +679,7 @@ type candidate = int * Ast.term (* unique candidate number, candidate *)
 
 exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
                                 atoms of the input goals *)
-exception Proved of NTacStatus.tac_status
+exception Proved of NTacStatus.tac_status * Ast.term list
 
 (* let close_failures _ c = c;; *)
 (* let prunable _ _ _ = false;; *)
@@ -650,11 +689,13 @@ exception Proved of NTacStatus.tac_status
 (* let cache_add_underinspection c _ _ = c;; *)
 
 let init_cache ?(facts=[]) ?(under_inspection=[],[]) 
-    ?(unit_eq=NCicParamod.empty_state) _ = 
+    ?(unit_eq=NCicParamod.empty_state) 
+    ?(trace=[]) 
+    _ = 
     {facts = facts;
      under_inspection = under_inspection;
-     unit_eq = unit_eq
-    }
+     unit_eq = unit_eq;
+     trace = trace}
 
 let only signature _context candidate = true
 (*
@@ -1145,7 +1186,7 @@ let rec auto_clusters ?(top=false)
   let status = clean_up_tac status in
   let goals = head_goals status#stack in
   if goals = [] then 
-    if depth = 0 then raise (Proved status)
+    if depth = 0 then raise (Proved (status, cache.trace))
     else 
       let status = NTactics.merge_tac status in
 	let cache =
@@ -1183,9 +1224,10 @@ let rec auto_clusters ?(top=false)
               (fun l -> 
                  ("cluster:" ^ String.concat "," (List.map string_of_int l)))
            classes)));
-      let status,b = 
+      let status,trace,b = 
         List.fold_left
-          (fun (status,b) gl ->
+          (fun (status,trace,b) gl ->
+	     let cache = {cache with trace = trace} in
              let flags = 
                {flags with last = (List.length gl = 1)} in 
              let lold = List.length status#stack in 
@@ -1197,19 +1239,19 @@ let rec auto_clusters ?(top=false)
                               String.concat "," (List.map string_of_int gl)));
                auto_main flags signature cache depth fstatus; assert false
              with 
-               | Proved(status) -> 
+               | Proved(status,trace) -> 
 		   let status = NTactics.merge_tac status in
 		   let lnew = List.length status#stack in 
 		     assert (lold = lnew);
-		   (status,true)
-               | Gaveup _ when top -> (status,b)
+		   (status,trace,true)
+               | Gaveup _ when top -> (status,trace,b)
           )
-          (status,false) classes
+          (status,cache.trace,false) classes
       in
       let rec final_merge n s =
 	if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
       in let status = final_merge depth status 
-      in if b then raise (Proved status) else raise (Gaveup IntSet.empty)
+      in if b then raise (Proved(status,trace)) else raise (Gaveup IntSet.empty)
 
 and
         
@@ -1222,7 +1264,7 @@ auto_main flags signature (cache:cache) depth status: unit =
   let status = sort_tac (clean_up_tac status) in
   let goals = head_goals status#stack in
   match goals with
-    | [] when depth = 0 -> raise (Proved status)
+    | [] when depth = 0 -> raise (Proved (status,cache.trace))
     | []  -> 
 	let status = NTactics.merge_tac status in
 	let cache =
@@ -1284,10 +1326,12 @@ auto_main flags signature (cache:cache) depth status: unit =
              let depth,cache =
 	       if t=Ast.Ident("__whd",None) then depth, cache 
 	       else depth+1,loop_cache in 
+	     let cache = add_to_trace cache t in
 	     try
 	       auto_clusters flags signature (cache:cache) depth status
 	     with Gaveup _ ->
-	       debug_print ~depth (lazy "Failed");())
+	       debug_print ~depth (lazy "Failed");
+	       ())
 	  alternatives;
 	raise (debug_print(lazy "no more candidates"); Gaveup IntSet.empty)
 ;;
@@ -1297,6 +1341,23 @@ let int name l def =
   with Failure _ | Not_found -> def
 ;;
 
+module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
+
+let cleanup_trace s trace =
+  (* removing duplicates *)
+  let trace_set = 
+    List.fold_left 
+      (fun acc t -> AstSet.add t acc)
+      AstSet.empty trace in
+  let trace = AstSet.elements trace_set
+    (* filtering facts *)
+  in List.filter 
+       (fun t -> 
+	  match t with
+	    | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
+	    | _ -> false) trace
+;;
+
 let auto_tac ~params:(_univ,flags) status =
   let oldstatus = status in
   let status = (status:> NTacStatus.tac_status) in
@@ -1347,8 +1408,12 @@ let auto_tac ~params:(_univ,flags) status =
 *)
         with
           | Gaveup _ -> up_to (x+1) y
-          | Proved s -> 
+          | Proved (s,trace) -> 
               debug_print (lazy ("proved at depth " ^ string_of_int x));
+              let trace = cleanup_trace s trace in
+	      let _ = print (lazy 
+			("Proof Trace: " ^ (String.concat ";" 
+			       (List.map CicNotationPp.pp_term trace)))) in
               let stack = 
                 match s#stack with
                   | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest