From 8e905c34eb47a3f5fa67afa7997576d57588a50f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Oct 2009 13:35:37 +0000 Subject: [PATCH] auto works on the regular tactics status --- helm/software/components/ng_tactics/nAuto.ml | 218 +++++++++++++----- helm/software/components/ng_tactics/nAuto.mli | 3 - 2 files changed, 162 insertions(+), 59 deletions(-) diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index 642682a89..422a1be41 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -13,7 +13,7 @@ open Printf -let debug = false +let debug = true let debug_print s = if debug then prerr_endline (Lazy.force s) else () open Continuationals.Stack @@ -934,31 +934,29 @@ type cache_examination_result = ] type sort = T | P -type goal = int * int * sort -type fail = goal * NCic.term -type candidate = NCic.term -type menv = NCic.metasenv -type subst = NCic.substitution +type goal = int * int * sort (* goal, depth, sort *) +type fail = goal * NTacStatus.cic_term +type candidate = int * NCic.term (* unique candidate number, candidate *) type op = (* goal has to be proved *) | D of goal (* goal has to be cached as a success obtained using candidate as the first * step *) - | S of goal * Cache.input * candidate (* int was minsize *) -type elem = + | S of goal * NTacStatus.cic_term * candidate (* int was minsize *) +type 'a elem = (* menv, subst, size, operations done (only S), operations to do, * failures to cache if any op fails *) - menv * subst * int * op list * op list * fail list + (#NTacStatus.tac_status as 'a) * int * op list * op list * fail list -type auto_status = +type 'a auto_status = (* list of computations that may lead to the solution: all op list will * end with the same (S(g,_)) *) - elem list * Cache.t + 'a elem list * Cache.t -type auto_result = +type 'a auto_result = | Gaveup - | Proved of menv * subst * auto_status (* the alternative proofs *) + | Proved of (#NTacStatus.tac_status as 'a) * 'a auto_status (* alt. proofs *) type flags = { do_types : bool; (* solve goals in Type *) @@ -967,15 +965,105 @@ type flags = { timeout : float; } -let close_failures _ = assert false;; -let equational_and_applicative_case _ = assert false;; -let prunable _ = assert false;; -let cache_examine _ = assert false;; -let put_in_subst _ = assert false;; -let calculate_goal_ty _ = assert false;; -let add_to_cache_and_del_from_orlist_if_green_cut _ = assert false;; -let cache_add_underinspection _ = assert false;; +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 cache_add_underinspection c _ _ = c;; +let equational_case _ _ _ _ _ _ _ = [];; +let sort_new_elems l = l;; +let only _ _ _ = true;; + +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 -> CicNotationPt.NRef ref + | _ -> assert false + in + let status = NTactics.focus_tac [g] status in + let status = NTactics.apply_tac ("",0,ast_for_t) status in + let open_goals = Continuationals.Stack.head_goals status#stack in + incr candidate_no; + Some ((!candidate_no,t),status,open_goals) + with NTacStatus.Error (msg,exn) -> debug_print msg; None +;; + + +let get_candidates status context gty = + let universe = status#auto_cache in + let _, gty = NTacStatus.term_of_cic_term status gty (NTacStatus.ctx_of gty) in + let cands = + NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe gty + in + (* XXX we have to trie for the context *) + let cands = NDiscriminationTree.TermSet.elements cands in + List.iter (fun x -> + debug_print (lazy (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x))) + cands; + 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 + debug_print (lazy ("candidates: " ^ string_of_int (List.length candidates))); + let elems = + List.fold_left + (fun elems cand -> + match try_candidate status cand g with + | None -> elems + | Some x -> x::elems) + [] candidates + in + elems +;; + +let equational_and_applicative_case + signature flags status g depth gty cache context += + let elems = + if false (*is_equational_case gty flags*) then + let elems = + equational_case + signature status flags g gty cache context + in + let more_elems = + applicative_case + signature status flags g gty cache context + in + elems@more_elems + else + let elems = + (*match LibraryObjects.eq_URI () with + | Some _ -> + smart_applicative_case dbd tables depth s fake_proof goalno + gty m context signature universe cache flags + | None -> *) + applicative_case + signature status flags g gty cache context + in + elems + in + let elems = + (* XXX calculate the sort *) + List.map (fun c,s,gl -> c,s,List.map (fun i -> i,depth-1,P) gl) elems + in + let elems = sort_new_elems elems in + elems +;; +let calculate_goal_ty (goalno,_,_) status = + try Some (NTacStatus.get_goalty status goalno) + with NTacStatus.Error _ -> None +;; let d_goals l = let rec aux acc = function | (D g)::tl -> aux (acc@[g]) tl @@ -996,8 +1084,8 @@ let remove_s_from_fl (id,_,_) (fl : fail list) = aux fl ;; -let auto_main status context flags signature elems cache = - let rec aux (elems, cache : auto_status) = +let auto_main context 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 *) match elems with @@ -1015,44 +1103,41 @@ let auto_main status context flags signature elems cache = (* complete failure *) debug_print (lazy "gave up"); Gaveup - | (m, s, _, _, [],_)::orlist -> - (* complete success *) + | (s, _, _, [],_)::orlist -> debug_print (lazy "success"); - Proved (m, s, (orlist, cache)) - | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist + Proved (s, (orlist, cache)) + | (s, size, don, (D (_,_,T))::todo, fl)::orlist when not flags.do_types -> - (* skip since not Prop, don't even check if closed by side-effect *) debug_print (lazy "skip goal in Type"); - aux ((m, s, size, don, todo, fl)::orlist, cache) - | (m, s, size, don, (S(g, key, c) as op)::todo, fl)::orlist -> - (* partial success, cache g and go on *) + aux ((s, size, don, todo, fl)::orlist, 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 m cache key todo orlist fl context size + g s cache key todo orlist fl context size in let fl = remove_s_from_fl g fl in let don = if sibling_pruned then don else op::don in - aux ((m, s, size, don, todo, fl)::orlist, cache) - | (m, s, size, don, todo, fl)::orlist + let s = NTactics.unfocus_tac s in + aux ((s, size, don, todo, fl)::orlist, cache) + | (s, size, don, todo, fl)::orlist when List.length(prop_only (d_goals todo)) > flags.maxwidth -> debug_print (lazy ("FAIL: WIDTH")); aux (orlist, cache) - | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize -> + | (s, size, don, todo, fl)::orlist when size > flags.maxsize -> debug_print (lazy ("FAIL: SIZE: "^string_of_int size ^ " > " ^ string_of_int flags.maxsize )); aux (orlist, cache) | _ when Unix.gettimeofday () > flags.timeout -> debug_print (lazy ("FAIL: TIMEOUT")); Gaveup - | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status -> + | (s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist -> debug_print (lazy "attack goal"); - match calculate_goal_ty g s m with + match calculate_goal_ty g s with | None -> debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno)); - aux ((m,s,size,don,todo, fl)::orlist, cache) - | Some (canonical_ctx, gty) -> - debug_print (lazy ("EXAMINE: "^ - NCicPp.ppterm ~metasenv:m ~subst:s ~context gty)); + aux ((s,size,don,todo, fl)::orlist, cache) + | Some gty -> + debug_print (lazy ("EXAMINE: "^ NTacStatus.ppterm s gty)); match cache_examine cache gty with | `Failed_in d when d >= depth -> debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno)); @@ -1064,12 +1149,12 @@ let auto_main status context flags signature elems cache = aux (orlist,cache) | `Succeded t -> debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno)); - let s, m = put_in_subst s m g canonical_ctx t gty in - aux ((m, s, size, don,todo, fl)::orlist, cache) + let s = put_in_subst s g t gty in + aux ((s, size, don,todo, fl)::orlist, cache) | `Notfound | `Failed_in _ when depth > 0 -> ( (* more depth or is the first time we see the goal *) - if prunable m s gty todo then + if prunable s gty todo then (debug_print (lazy( "FAIL: LOOP: one father is equal")); let cache = close_failures fl cache in aux (orlist,cache)) @@ -1077,11 +1162,11 @@ let auto_main status context flags signature elems cache = let cache = cache_add_underinspection cache gty depth in debug_print (lazy ("INSPECTING: " ^ string_of_int gno ^ "("^ string_of_int size ^ "): "^ - NCicPp.ppterm ~metasenv:m ~subst:s ~context gty)); + NTacStatus.ppterm s gty)); (* elems are possible computations for proving gty *) let elems = equational_and_applicative_case - signature status flags m s g gty cache context + signature flags s gno depth gty cache context in if elems = [] then (* this goal has failed *) @@ -1095,19 +1180,19 @@ let auto_main status context flags signature elems cache = let inj_gl gl = List.map (fun g -> D g) gl in let rec map = function | [] -> assert false - | (cand,m,s,gl)::[] -> + | (cand,s,gl)::[] -> let todo = inj_gl gl @ (S(g,gty,cand))::todo in (* we are the last in OR, we fail on g and * also on all failures implied by g *) - (m,s, size + size_gl gl, don, todo, (g,gty)::fl) + (s, size + size_gl gl, don, todo, (g,gty)::fl) :: orlist - | (cand,m,s,gl)::tl -> + | (cand,s,gl)::tl -> let todo = inj_gl gl @ (S(g,gty,cand))::todo in - (m,s, size + size_gl gl, don, todo, []) :: map tl + (s, size + size_gl gl, don, todo, []) :: map tl in map elems in @@ -1117,18 +1202,39 @@ let auto_main status context flags signature elems cache = let cache = close_failures fl cache in aux (orlist, cache) in - (aux (elems, cache) : auto_result) + (aux (elems, cache) : 'a auto_result) ;; let auto_tac ~params status = prerr_endline "I teoremi noti sono"; NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun _ t -> - List.iter (fun t -> - prerr_endline - (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t)) - (NDiscriminationTree.TermSet.elements t)); - status + List.iter + (fun t -> + prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t)) + (NDiscriminationTree.TermSet.elements t)); + let cache = Cache.empty in + let goals = Continuationals.Stack.head_goals status#stack in + 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; + maxsize = 10; + timeout = Unix.gettimeofday() +. 3000.; + do_types = false; + } in + match auto_main context flags signature elems cache with + | Gaveup -> raise (NTacStatus.Error (lazy "auto gave up", None)) + | Proved (s, (_orlist, _cache)) -> + let stack = + match s#stack with + | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest + | _ -> assert false + in + s#set_stack stack ;; diff --git a/helm/software/components/ng_tactics/nAuto.mli b/helm/software/components/ng_tactics/nAuto.mli index f8f5ae4e2..7121bb946 100644 --- a/helm/software/components/ng_tactics/nAuto.mli +++ b/helm/software/components/ng_tactics/nAuto.mli @@ -15,6 +15,3 @@ val auto_tac: params:(NTacStatus.tactic_term list * (string * string) list) -> 's NTacStatus.tactic -val auto_paramod_tac: - params:(NTacStatus.tactic_term list * (string * string) list) -> - 's NTacStatus.tactic -- 2.39.2