Computation of the trace.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 7c52a7f72ebf7f0122acc2d8f20f4500d2cc0605..57f99b52b405c48f1f26c8de6483046778ef1292 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -195,11 +195,15 @@ let solve f 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
@@ -513,7 +517,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
-        print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
+        debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
         fast_eq_check unit_eq status j
     with
       | Error _ as e -> debug_print (lazy "error"); raise e
@@ -648,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
@@ -658,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;; *)
@@ -668,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
 (*
@@ -1163,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 =
@@ -1201,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 
@@ -1215,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
         
@@ -1240,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 =
@@ -1302,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)
 ;;
@@ -1315,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
@@ -1365,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