From cf72398627cd1189f42c3fbb9e29fa4b32e723c8 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 24 Mar 2010 13:04:27 +0000 Subject: [PATCH] Computation of the trace. From: asperti --- helm/software/components/ng_tactics/nnAuto.ml | 89 ++++++++++++++----- 1 file changed, 68 insertions(+), 21 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 7c52a7f72..57f99b52b 100644 --- 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 -- 2.39.2