From fcde872381886367925435e32ae3ae2e6f9190de Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 8 Oct 2009 10:01:46 +0000 Subject: [PATCH] removed misleading context --- helm/software/components/ng_tactics/nAuto.ml | 69 +++++++++++--------- 1 file changed, 37 insertions(+), 32 deletions(-) diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index fbb43cbb0..37ac72eb9 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -936,7 +936,7 @@ type cache_examination_result = type sort = T | P type goal = int * int * sort (* goal, depth, sort *) type fail = goal * cic_term -type candidate = int * NCic.term (* unique candidate number, candidate *) +type candidate = int * Ast.term (* unique candidate number, candidate *) type op = (* goal has to be proved *) @@ -969,9 +969,9 @@ let close_failures _ c = c;; let prunable _ _ _ = false;; let cache_examine cache gty = `Notfound;; let put_in_subst s _ _ _ = s;; -let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ _ = c, o, f, false ;; +let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; let cache_add_underinspection c _ _ = c;; -let equational_case _ _ _ _ _ _ _ = [];; +let equational_case _ _ _ _ _ _ = [];; let sort_new_elems l = l;; let only _ _ _ = true;; @@ -979,37 +979,42 @@ let candidate_no = ref 0;; let try_candidate status t g = try - debug_print (lazy (" try " ^ - NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t - )); - let ast_for_t = - match t with - | NCic.Rel i -> assert false - | NCic.Const ref -> Ast.NRef ref - | _ -> assert false - in + debug_print (lazy (" try " ^ CicNotationPp.pp_term t)); let status = NTactics.focus_tac [g] status in - let status = NTactics.apply_tac ("",0,ast_for_t) status in + let status = NTactics.apply_tac ("",0,t) status in let open_goals = head_goals status#stack in + debug_print + (lazy (" success: "^String.concat " "(List.map string_of_int open_goals))); incr candidate_no; Some ((!candidate_no,t),status,open_goals) - with Error (msg,exn) -> debug_print msg; None + with Error (msg,exn) -> debug_print (lazy " failed"); None ;; +let rec mk_irl n = function + | [] -> [] + | _ :: tl -> NCic.Rel n :: mk_irl (n+1) tl +;; -let get_candidates status context gty = +let get_candidates status signature gty = let universe = status#auto_cache in - let _, gty = term_of_cic_term status gty (ctx_of gty) in + let context = ctx_of gty in + let _, gty = term_of_cic_term status gty context in let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe gty in - (* XXX we have to trie for the context *) - NDiscriminationTree.TermSet.elements cands + let cands = + List.filter (only signature context) + (NDiscriminationTree.TermSet.elements cands) + in + (* XXX we have to use the trie for the context *) + HExtlib.filter_map (fun name,_ -> + if name <> "_" then Some (Ast.Ident (name,None)) else None) context + @ + List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands ;; -let applicative_case signature status flags g gty cache context = - let candidates = get_candidates status context gty in - let candidates = List.filter (only signature context) candidates in +let applicative_case signature status flags g gty cache = + let candidates = get_candidates status signature gty in debug_print (lazy ("candidates: " ^ string_of_int (List.length candidates))); let elems = List.fold_left @@ -1023,17 +1028,17 @@ let applicative_case signature status flags g gty cache context = ;; let equational_and_applicative_case - signature flags status g depth gty cache context + signature flags status g depth gty cache = let elems = if false (*is_equational_case gty flags*) then let elems = equational_case - signature status flags g gty cache context + signature status flags g gty cache in let more_elems = applicative_case - signature status flags g gty cache context + signature status flags g gty cache in elems@more_elems else @@ -1044,7 +1049,7 @@ let equational_and_applicative_case gty m context signature universe cache flags | None -> *) applicative_case - signature status flags g gty cache context + signature status flags g gty cache in elems in @@ -1080,7 +1085,7 @@ let remove_s_from_fl (id,_,_) (fl : fail list) = aux fl ;; -let auto_main context flags signature elems cache = +let auto_main flags signature elems cache = let rec aux (elems, cache : 'a auto_status) = (* processa le hint dell'utente *) (* let cache, elems = filter_prune_hint cache elems in *) @@ -1108,7 +1113,7 @@ let auto_main context flags signature elems cache = | (s, size, don, (S(g, key, c) as op)::todo, fl)::orlist -> let cache, orlist, fl, sibling_pruned = add_to_cache_and_del_from_orlist_if_green_cut - g s cache key todo orlist fl context size + g s cache key todo orlist fl size in let fl = remove_s_from_fl g fl in let don = if sibling_pruned then don else op::don in @@ -1161,7 +1166,7 @@ let auto_main context flags signature elems cache = (* elems are possible computations for proving gty *) let elems = equational_and_applicative_case - signature flags s gno depth gty cache context + signature flags s gno depth gty cache in if elems = [] then (* this goal has failed *) @@ -1203,18 +1208,18 @@ let auto_main context flags signature elems cache = let auto_tac ~params status = let cache = Cache.empty in let goals = head_goals status#stack in - let depth = 3 in (* XXX fix sort *) + let depth = 3 in + (* XXX fix sort *) let goals = List.map (fun i -> D(i,depth,P)) goals in let elems = [status,0,[],goals,[]] in - let context = [] (* XXX big problem *) in let signature = () in let flags = { - maxwidth = 3; + maxwidth = 3 + List.length goals; maxsize = 10; timeout = Unix.gettimeofday() +. 3000.; do_types = false; } in - match auto_main context flags signature elems cache with + match auto_main flags signature elems cache with | Gaveup -> raise (Error (lazy "auto gave up", None)) | Proved (s, (_orlist, _cache)) -> let stack = -- 2.39.2