From b879541d6103c346cfe14db79ff54249830a20fa Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 4 Mar 2010 08:06:43 +0000 Subject: [PATCH] 1. For smart application, we only perforate small terms (terms with sort Type0). E.g. Not(P(a)) is perforated to Not(P(?)) and not to Not(?) as before. 2. At maxdepth, we restrict the analysis to facts only in case the goal is not reducible to a Pi. Example: if Not A = A -> False, Not A is not a fact, and the previous politics would prune its application. --- helm/software/components/ng_tactics/nnAuto.ml | 1135 +++-------------- 1 file changed, 172 insertions(+), 963 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 8f3ba4921..bee8b69cc 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -94,6 +94,70 @@ let current_goal status = let ctx = ctx_of gty in open_goal, ctx, gty +let height_of_ref (NReference.Ref (uri, x)) = + match x with + | NReference.Decl + | NReference.Ind _ + | NReference.Con _ + | NReference.CoFix _ -> + let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in + height + | NReference.Def h -> h + | NReference.Fix (_,_,h) -> h +;; + +(*************************** height functions ********************************) +let fast_height_of_term t = + let h = ref 0 in + let rec aux = + function + NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l + | NCic.Meta _ -> () + | NCic.Rel _ + | NCic.Sort _ -> () + | NCic.Implicit _ -> assert false + | NCic.Const nref as t -> +(* + prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] + ~context:[] t ^ ":" ^ string_of_int (height_of_ref nref)); +*) + h := max !h (height_of_ref nref) + | NCic.Prod (_,t1,t2) + | NCic.Lambda (_,t1,t2) -> aux t1; aux t2 + | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t + | NCic.Appl l -> List.iter aux l + | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl + in + aux t; !h +;; + +let height_of_goal g status = + let ty = get_goalty status g in + let context = ctx_of ty in + let _, ty = term_of_cic_term status ty (ctx_of ty) in + let h = ref (fast_height_of_term ty) in + List.iter + (function + | _, NCic.Decl ty -> h := max !h (fast_height_of_term ty) + | _, NCic.Def (bo,ty) -> + h := max !h (fast_height_of_term ty); + h := max !h (fast_height_of_term bo); + ) + context; + !h +;; + +let height_of_goals status = + let open_goals = head_goals status#stack in + assert (List.length open_goals > 0); + let h = ref 1 in + List.iter + (fun open_goal -> + h := max !h (height_of_goal open_goal status)) + open_goals; + debug_print (lazy ("altezza sequente: " ^ string_of_int !h)); + !h +;; (* =============================== paramod =========================== *) let solve fast status eq_cache goal = @@ -108,20 +172,16 @@ let solve fast status eq_cache goal = debug_print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt))); let stamp = Unix.gettimeofday () in let metasenv, subst, pt, pty = - NCicRefiner.typeof status - (* (status#set_coerc_db NCicCoercion.empty_db) *) + (* NCicRefiner.typeof status + (* (status#set_coerc_db NCicCoercion.empty_db) *) metasenv subst ctx pt None in - debug_print (lazy ("refined: "^(NCicPp.ppterm ctx subst metasenv pt))); - debug_print (lazy ("synt: "^(NCicPp.ppterm ctx subst metasenv pty))); - let metasenv, subst = - NCicUnification.unify status metasenv subst ctx gty pty - (* the previous code is much less expensive than directly refining - pt with expected type pty - in - prerr_endline ("exp: "^(NCicPp.ppterm ctx subst metasenv gty)); - NCicRefiner.typeof - (status#set_coerc_db NCicCoercion.empty_db) - metasenv subst ctx pt (Some gty) *) + print (lazy ("refined: "^(NCicPp.ppterm ctx subst metasenv pt))); + debug_print (lazy ("synt: "^(NCicPp.ppterm ctx subst metasenv pty))); + let metasenv, subst = + NCicUnification.unify status metasenv subst ctx gty pty *) + NCicRefiner.typeof + (status#set_coerc_db NCicCoercion.empty_db) + metasenv subst ctx pt (Some gty) in debug_print (lazy (Printf.sprintf "Refined in %fs" (Unix.gettimeofday() -. stamp))); @@ -381,874 +441,25 @@ let close status g = ctx,ty ;; - - -(* =================================== auto =========================== *) -(****************** AUTO ******************** - -let calculate_timeout flags = - if flags.timeout = 0. then - (debug_print (lazy "AUTO WITH NO TIMEOUT"); - {flags with timeout = infinity}) - else - flags -;; -let is_equational_case goalty flags = - let ensure_equational t = - if is_an_equational_goal t then true - else false - in - (flags.use_paramod && is_an_equational_goal goalty) || - (flags.use_only_paramod && ensure_equational goalty) -;; - -type menv = Cic.metasenv -type subst = Cic.substitution -type goal = ProofEngineTypes.goal * int * AutoTypes.sort -let candidate_no = ref 0;; -type candidate = int * Cic.term Lazy.t -type cache = AutoCache.cache - -type fail = - (* the goal (mainly for depth) and key of the goal *) - goal * AutoCache.cache_key -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 * AutoCache.cache_key * candidate * int -type 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 -type status = - (* list of computations that may lead to the solution: all op list will - * end with the same (S(g,_)) *) - elem list -type auto_result = - (* menv, subst, alternatives, tables, cache *) - | Proved of menv * subst * elem list * AutomationCache.tables * cache - | Gaveup of AutomationCache.tables * cache - - -(* the status exported to the external observer *) -type auto_status = - (* context, (goal,candidate) list, and_list, history *) - Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list * - (int * Cic.term * int) list * Cic.term Lazy.t list - -let d_prefix l = - let rec aux acc = function - | (D g)::tl -> aux (acc@[g]) tl - | _ -> acc - in - aux [] l -;; - -let calculate_goal_ty (goalno,_,_) s m = - try - let _,cc,goalty = CicUtil.lookup_meta goalno m in - (* XXX applicare la subst al contesto? *) - Some (cc, CicMetaSubst.apply_subst s goalty) - with CicUtil.Meta_not_found i when i = goalno -> None -;; - -let calculate_closed_goal_ty (goalno,_,_) s = - try - let cc,_,goalty = List.assoc goalno s in - (* XXX applicare la subst al contesto? *) - Some (cc, CicMetaSubst.apply_subst s goalty) - with Not_found -> - None -;; - -let pp_status ctx status = - if debug then - let names = Utils.names_of_context ctx in - let pp x = - let x = - ProofEngineReduction.replace - ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false) - ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x - in - CicPp.pp x names - in - let string_of_do m s (gi,_,_ as g) d = - match calculate_goal_ty g s m with - | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d - | None -> Printf.sprintf "D(%d, _, %d)" gi d - in - let string_of_s m su k (ci,ct) gi = - Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci - in - let string_of_ol m su l = - String.concat " | " - (List.map - (function - | D (g,d,s) -> string_of_do m su (g,d,s) d - | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi) - l) - in - let string_of_fl m s fl = - String.concat " | " - (List.map (fun ((i,_,_),ty) -> - Printf.sprintf "(%d, %s)" i (pp ty)) fl) - in - let rec aux = function - | [] -> () - | (m,s,_,_,ol,fl)::tl -> - Printf.eprintf "< [%s] ;;; [%s]>\n" - (string_of_ol m s ol) (string_of_fl m s fl); - aux tl - in - Printf.eprintf "-------------------------- status -------------------\n"; - aux status; - Printf.eprintf "-----------------------------------------------------\n"; -;; - -let auto_status = ref [] ;; -let auto_context = ref [];; -let in_pause = ref false;; -let pause b = in_pause := b;; -let cond = Condition.create ();; -let mutex = Mutex.create ();; -let hint = ref None;; -let prune_hint = ref [];; - -let step _ = Condition.signal cond;; -let give_hint n = hint := Some n;; -let give_prune_hint hint = - prune_hint := hint :: !prune_hint -;; - -let check_pause _ = - if !in_pause then - begin - Mutex.lock mutex; - Condition.wait cond mutex; - Mutex.unlock mutex - end -;; - -let get_auto_status _ = - let status = !auto_status in - let and_list,elems,last = - match status with - | [] -> [],[],[] - | (m,s,_,don,gl,fail)::tl -> - let and_list = - HExtlib.filter_map - (fun (id,d,_ as g) -> - match calculate_goal_ty g s m with - | Some (_,x) -> Some (id,x,d) | None -> None) - (d_goals gl) - in - let rows = - (* these are the S goalsin the or list *) - let orlist = - List.map - (fun (m,s,_,don,gl,fail) -> - HExtlib.filter_map - (function S (g,k,c,_) -> Some (g,k,c) | _ -> None) - (List.rev don @ gl)) - status - in - (* this function eats id from a list l::[id,x] returning x, l *) - let eat_tail_if_eq id l = - let rec aux (s, l) = function - | [] -> s, l - | ((id1,_,_),k1,c)::tl when id = id1 -> - (match s with - | None -> aux (Some c,l) tl - | Some _ -> assert false) - | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl - in - let c, l = aux (None, []) l in - c, List.rev l - in - let eat_in_parallel id l = - let rec aux (b,eaten, new_l as acc) l = - match l with - | [] -> acc - | l::tl -> - match eat_tail_if_eq id l with - | None, l -> aux (b@[false], eaten, new_l@[l]) tl - | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl - in - aux ([],[],[]) l - in - let rec eat_all rows l = - match l with - | [] -> rows - | elem::or_list -> - match List.rev elem with - | ((to_eat,depth,_),k,_)::next_lunch -> - let b, eaten, l = eat_in_parallel to_eat l in - let eaten = HExtlib.list_uniq eaten in - let eaten = List.rev eaten in - let b = true (* List.hd (List.rev b) *) in - let rows = rows @ [to_eat,k,b,depth,eaten] in - eat_all rows l - | [] -> eat_all rows or_list - in - eat_all [] (List.rev orlist) - in - let history = - HExtlib.filter_map - (function (S (_,_,(_,c),_)) -> Some c | _ -> None) - gl - in -(* let rows = List.filter (fun (_,l) -> l <> []) rows in *) - and_list, rows, history - in - !auto_context, elems, and_list, last -;; - -(* Works if there is no dependency over proofs *) -let is_a_green_cut goalty = - CicUtil.is_meta_closed goalty -;; -let rec first_s = function - | (D _)::tl -> first_s tl - | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl) - | [] -> None -;; -let list_union l1 l2 = - (* TODO ottimizzare compare *) - HExtlib.list_uniq (List.sort compare (l1 @ l1)) -;; -let rec eq_todo l1 l2 = - match l1,l2 with - | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2 - | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2 - when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 -> - if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false - | [],[] -> true - | _ -> false -;; -let eat_head todo id fl orlist = - let rec aux acc = function - | [] -> [], acc - | (m, s, _, _, todo1, fl1)::tl as orlist -> - let rec aux1 todo1 = - match first_s todo1 with - | None -> orlist, acc - | Some (((gno,_,_),_,_,_), todo11) -> - (* TODO confronto tra todo da ottimizzare *) - if gno = id && eq_todo todo11 todo then - aux (list_union fl1 acc) tl - else - aux1 todo11 - in - aux1 todo1 - in - aux fl orlist -;; -let close_proof p ty menv context = - let metas = - List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty) - in - let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in - naif_closure p menv context -;; -(* XXX capire bene quando aggiungere alla cache *) -let add_to_cache_and_del_from_orlist_if_green_cut - g s m cache key todo orlist fl ctx size minsize -= - let cache = cache_remove_underinspection cache key in - (* prima per fare la irl usavamo il contesto vero e proprio e non quello - * canonico! XXX *) - match calculate_closed_goal_ty g s with - | None -> assert false - | Some (canonical_ctx , gty) -> - let goalno,depth,sort = g in - let irl = mk_irl canonical_ctx in - let goal = Cic.Meta(goalno, irl) in - let proof = CicMetaSubst.apply_subst s goal in - let green_proof, closed_proof = - let b = is_a_green_cut proof in - if not b then - b, (* close_proof proof gty m ctx *) proof - else - b, proof - in - debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key)); - if is_a_green_cut key then - (* if the initia goal was closed, we cut alternatives *) - let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in - let orlist, fl = eat_head todo goalno fl orlist in - let cache = - if size < minsize then - (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache) - else - (* if the proof is closed we cache it *) - if green_proof then cache_add_success cache key proof - else (* cache_add_success cache key closed_proof *) - (debug_print (lazy ("NO CACHE: (no gree proof)"));cache) - in - cache, orlist, fl, true - else - let cache = - debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty)); - if size < minsize then - (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else - (* if the substituted goal and the proof are closed we cache it *) - if is_a_green_cut gty then - if green_proof then cache_add_success cache gty proof - else (* cache_add_success cache gty closed_proof *) - (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache) - else (* - try - let ty, _ = - CicTypeChecker.type_of_aux' ~subst:s - m ctx closed_proof CicUniv.oblivion_ugraph - in - if is_a_green_cut ty then - cache_add_success cache ty closed_proof - else cache - with - | CicTypeChecker.TypeCheckerFailure _ ->*) - (debug_print (lazy ("NO CACHE: (no green gty )"));cache) - in - cache, orlist, fl, false -;; -let close_failures (fl : fail list) (cache : cache) = - List.fold_left - (fun cache ((gno,depth,_),gty) -> - if CicUtil.is_meta_closed gty then - ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno)); - cache_add_failure cache gty depth) - else - cache) - cache fl -;; -let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty = - let entry = goalno, (canonical_ctx, t,ty) in - assert_subst_are_disjoint subst [entry]; - let subst = entry :: subst in - - let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in - - subst, metasenv -;; - -let mk_fake_proof metasenv subst (goalno,_,_) goalty context = - None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, [] -;; - -let equational_case - tables cache depth fake_proof goalno goalty subst context - flags -= - let active,passive,bag = tables in - let ppterm = ppterm context in - let status = (fake_proof,goalno) in - if flags.use_only_paramod then - begin - debug_print (lazy ("PARAMODULATION SU: " ^ - string_of_int goalno ^ " " ^ ppterm goalty )); - let goal_steps, saturation_steps, timeout = - max_int,max_int,flags.timeout - in - match - Saturation.given_clause bag status active passive - goal_steps saturation_steps timeout - with - | None, active, passive, bag -> - [], (active,passive,bag), cache, flags - | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active, - passive,bag -> - assert_subst_are_disjoint subst subst'; - let subst = subst@subst' in - let open_goals = - order_new_goals metasenv subst open_goals ppterm - in - let open_goals = - List.map (fun (x,sort) -> x,depth-1,sort) open_goals - in - incr candidate_no; - [(!candidate_no,proof),metasenv,subst,open_goals], - (active,passive,bag), cache, flags - end - else - begin - debug_print (lazy ("NARROWING DEL GOAL: " ^ - string_of_int goalno ^ " " ^ ppterm goalty )); - let goal_steps, saturation_steps, timeout = - 1,0,flags.timeout - in - match - Saturation.solve_narrowing bag status active passive goal_steps - with - | None, active, passive, bag -> - [], (active,passive,bag), cache, flags - | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active, - passive,bag -> - assert_subst_are_disjoint subst subst'; - let subst = subst@subst' in - let open_goals = - order_new_goals metasenv subst open_goals ppterm - in - let open_goals = - List.map (fun (x,sort) -> x,depth-1,sort) open_goals - in - incr candidate_no; - [(!candidate_no,proof),metasenv,subst,open_goals], - (active,passive,bag), cache, flags - end -(* - begin - let params = ([],["use_context","false"]) in - let automation_cache = { - AutomationCache.tables = tables ; - AutomationCache.univ = Universe.empty; } - in - try - let ((_,metasenv,subst,_,_,_),open_goals) = - - solve_rewrite ~params ~automation_cache - (fake_proof, goalno) - in - let proof = lazy (Cic.Meta (-1,[])) in - [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags - with ProofEngineTypes.Fail _ -> [], tables, cache, flags -(* - let res = Saturation.all_subsumed bag status active passive in - let res' = - List.map - (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) -> - assert_subst_are_disjoint subst subst'; - let subst = subst@subst' in - let open_goals = - order_new_goals metasenv subst open_goals ppterm - in - let open_goals = - List.map (fun (x,sort) -> x,depth-1,sort) open_goals - in - incr candidate_no; - (!candidate_no,proof),metasenv,subst,open_goals) - res - in - res', (active,passive,bag), cache, flags -*) - end -*) -;; - -let sort_new_elems = - List.sort (fun (_,_,_,l1) (_,_,_,l2) -> - let p1 = List.length (prop_only l1) in - let p2 = List.length (prop_only l2) in - if p1 = p2 then List.length l1 - List.length l2 else p1-p2) -;; - - -let try_candidate dbd - goalty tables subst fake_proof goalno depth context cand -= - let ppterm = ppterm context in - try - let actives, passives, bag = tables in - let (_,metasenv,subst,_,_,_), open_goals = - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:cand) - (fake_proof,goalno) - in - let tables = actives, passives, - Equality.push_maxmeta bag - (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst)) - in - debug_print (lazy (" OK: " ^ ppterm cand)); - let metasenv = CicRefine.pack_coercion_metasenv metasenv in - let open_goals = order_new_goals metasenv subst open_goals ppterm in - let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in - incr candidate_no; - Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables - with - | ProofEngineTypes.Fail s -> None,tables - | CicUnification.Uncertain s -> None,tables -;; - -let applicative_case dbd - tables depth subst fake_proof goalno goalty metasenv context - signature universe cache flags -= - (* let goalty_aux = - match goalty with - | Cic.Appl (hd::tl) -> - Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl)) - | _ -> goalty - in *) - let goalty_aux = goalty in - let candidates = - get_candidates flags.skip_trie_filtering universe cache goalty_aux - in - (* if the goal is an equality we skip the congruence theorems - let candidates = - if is_equational_case goalty flags - then List.filter not_default_eq_term candidates - else candidates - in *) - let candidates = List.filter (only signature context metasenv) candidates - in - let tables, elems = - List.fold_left - (fun (tables,elems) cand -> - match - try_candidate dbd goalty - tables subst fake_proof goalno depth context cand - with - | None, tables -> tables, elems - | Some x, tables -> tables, x::elems) - (tables,[]) candidates - in - let elems = sort_new_elems elems in - elems, tables, cache -;; - -let try_smart_candidate dbd - goalty tables subst fake_proof goalno depth context cand -= - let ppterm = ppterm context in - try - let params = ([],[]) in - let automation_cache = { - AutomationCache.tables = tables ; - AutomationCache.univ = Universe.empty; } - in - debug_print (lazy ("candidato per " ^ string_of_int goalno - ^ ": " ^ CicPp.ppterm cand)); -(* - let (_,metasenv,subst,_,_,_) = fake_proof in - prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv); - prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst); -*) - let ((_,metasenv,subst,_,_,_),open_goals) = - apply_smart ~dbd ~term:cand ~params ~automation_cache - (fake_proof, goalno) - in - let metasenv = CicRefine.pack_coercion_metasenv metasenv in - let open_goals = order_new_goals metasenv subst open_goals ppterm in - let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in - incr candidate_no; - Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables - with - | ProofEngineTypes.Fail s -> None,tables - | CicUnification.Uncertain s -> None,tables -;; - -let smart_applicative_case dbd - tables depth subst fake_proof goalno goalty metasenv context signature - universe cache flags -= - let goalty_aux = - match goalty with - | Cic.Appl (hd::tl) -> - Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl)) - | _ -> goalty - in - let smart_candidates = - get_candidates flags.skip_trie_filtering universe cache goalty_aux - in - let candidates = - get_candidates flags.skip_trie_filtering universe cache goalty - in - let smart_candidates = - List.filter - (fun x -> not(List.mem x candidates)) smart_candidates - in - let debug_msg = - (lazy ("smart_candidates" ^ " = " ^ - (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in - debug_print debug_msg; - let candidates = List.filter (only signature context metasenv) candidates in - let smart_candidates = - List.filter (only signature context metasenv) smart_candidates - in -(* - let penalty cand depth = - if only signature context metasenv cand then depth else ((prerr_endline ( - "penalizzo " ^ CicPp.ppterm cand));depth -1) - in -*) - let tables, elems = - List.fold_left - (fun (tables,elems) cand -> - match - try_candidate dbd goalty - tables subst fake_proof goalno depth context cand - with - | None, tables -> - (* if normal application fails we try to be smart *) - (match try_smart_candidate dbd goalty - tables subst fake_proof goalno depth context cand - with - | None, tables -> tables, elems - | Some x, tables -> tables, x::elems) - | Some x, tables -> tables, x::elems) - (tables,[]) candidates - in - let tables, smart_elems = - List.fold_left - (fun (tables,elems) cand -> - match - try_smart_candidate dbd goalty - tables subst fake_proof goalno depth context cand - with - | None, tables -> tables, elems - | Some x, tables -> tables, x::elems) - (tables,[]) smart_candidates - in - let elems = sort_new_elems (elems @ smart_elems) in - elems, tables, cache -;; - -let equational_and_applicative_case dbd - signature universe flags m s g gty tables cache context -= - let goalno, depth, sort = g in - let fake_proof = mk_fake_proof m s g gty context in - if is_equational_case gty flags then - let elems,tables,cache, flags = - equational_case tables cache - depth fake_proof goalno gty s context flags - in - let more_elems, tables, cache = - if flags.use_only_paramod then - [],tables, cache - else - applicative_case dbd - tables depth s fake_proof goalno - gty m context signature universe cache flags - in - elems@more_elems, tables, cache, flags - else - let elems, tables, cache = - 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 dbd tables depth s fake_proof goalno - gty m context signature universe cache flags - in - elems, tables, cache, flags -;; -let rec condition_for_hint i = function - | [] -> false - | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *) - | _::tl -> condition_for_hint i tl -;; -let prunable_for_size flags s m todo = - let rec aux b = function - | (S _)::tl -> aux b tl - | (D (_,_,T))::tl -> aux b tl - | (D g)::tl -> - (match calculate_goal_ty g s m with - | None -> aux b tl - | Some (canonical_ctx, gty) -> - let gsize, _ = - Utils.weight_of_term - ~consider_metas:false ~count_metas_occurrences:true gty in - let newb = b || gsize > flags.maxgoalsizefactor in - aux newb tl) - | [] -> b - in - aux false todo - -(* -let prunable ty todo = - let rec aux b = function - | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl - | (D (_,_,T))::tl -> aux b tl - | D _::_ -> false - | [] -> b - in - aux false todo -;; -*) - -let prunable menv subst ty todo = - let rec aux = function - | (S(_,k,_,_))::tl -> - (match Equality.meta_convertibility_subst k ty menv with - | None -> aux tl - | Some variant -> - no_progress variant tl (* || aux tl*)) - | (D (_,_,T))::tl -> aux tl - | _ -> false - and no_progress variant = function - | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true - | D ((n,_,P) as g)::tl -> - (match calculate_goal_ty g subst menv with - | None -> no_progress variant tl - | Some (_, gty) -> - (match calculate_goal_ty g variant menv with - | None -> assert false - | Some (_, gty') -> - if gty = gty' then no_progress variant tl -(* -(prerr_endline (string_of_int n); - prerr_endline (CicPp.ppterm gty); - prerr_endline (CicPp.ppterm gty'); - prerr_endline "---------- subst"; - prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst); - prerr_endline "---------- variant"; - prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant); - prerr_endline "---------- menv"; - prerr_endline (CicMetaSubst.ppmetasenv [] menv); - no_progress variant tl) *) - else false)) - | _::tl -> no_progress variant tl - in - aux todo - -;; -let condition_for_prune_hint prune (m, s, size, don, todo, fl) = - let s = - HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo - in - List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s -;; -let filter_prune_hint c l = - let prune = !prune_hint in - prune_hint := []; (* possible race... *) - if prune = [] then c,l - else - cache_reset_underinspection c, - List.filter (condition_for_prune_hint prune) l -;; - - - -let - auto_all_solutions dbd tables universe cache context metasenv gl flags -= - let signature = - List.fold_left - (fun set g -> - MetadataConstraints.UriManagerSet.union set - (MetadataQuery.signature_of metasenv g) - ) - MetadataConstraints.UriManagerSet.empty gl - in - let goals = order_new_goals metasenv [] gl CicPp.ppterm in - let goals = - List.map - (fun (x,s) -> D (x,flags.maxdepth,s)) goals - in - let elems = [metasenv,[],1,[],goals,[]] in - let rec aux tables solutions cache elems flags = - match auto_main dbd tables context flags signature universe cache elems with - | Gaveup (tables,cache) -> - solutions,cache, tables - | Proved (metasenv,subst,others,tables,cache) -> - if Unix.gettimeofday () > flags.timeout then - ((subst,metasenv)::solutions), cache, tables - else - aux tables ((subst,metasenv)::solutions) cache others flags - in - let rc = aux tables [] cache elems flags in - match rc with - | [],cache,tables -> [],cache,tables - | solutions, cache,tables -> - let solutions = - HExtlib.filter_map - (fun (subst,newmetasenv) -> - let opened = - ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv - in - if opened = [] then Some subst else None) - solutions - in - solutions,cache,tables -;; - -(******************* AUTO ***************) - - -let auto dbd flags metasenv tables universe cache context metasenv gl = - let initial_time = Unix.gettimeofday() in - let signature = - List.fold_left - (fun set g -> - MetadataConstraints.UriManagerSet.union set - (MetadataQuery.signature_of metasenv g) - ) - MetadataConstraints.UriManagerSet.empty gl - in - let goals = order_new_goals metasenv [] gl CicPp.ppterm in - let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in - let elems = [metasenv,[],1,[],goals,[]] in - match auto_main dbd tables context flags signature universe cache elems with - | Proved (metasenv,subst,_, tables,cache) -> - debug_print(lazy - ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); - Some (subst,metasenv), cache - | Gaveup (tables,cache) -> - debug_print(lazy - ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); - None,cache -;; - -let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) = - let flags = flags_of_params params () in - let use_library = flags.use_library in - let universe, tables, cache = - init_cache_and_tables - ~dbd ~use_library ~use_context:(not flags.skip_context) - automation_cache univ (proof, goal) - in - let _,metasenv,subst,_,_, _ = proof in - let _,context,goalty = CicUtil.lookup_meta goal metasenv in - let signature = MetadataQuery.signature_of metasenv goal in - let signature = - List.fold_left - (fun set t -> - let ty, _ = - CicTypeChecker.type_of_aux' metasenv context t - CicUniv.oblivion_ugraph - in - MetadataConstraints.UriManagerSet.union set - (MetadataConstraints.constants_of ty) - ) - signature univ - in - let tables,cache = - if flags.close_more then - close_more - tables context (proof, goal) - (auto_all_solutions dbd) signature universe cache - else tables,cache in - let initial_time = Unix.gettimeofday() in - let (_,oldmetasenv,_,_,_, _) = proof in - hint := None; - let elem = - metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[] - in - match auto_main dbd tables context flags signature universe cache [elem] with - | Proved (metasenv,subst,_, tables,cache) -> - debug_print (lazy - ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time))); - let proof,metasenv = - ProofEngineHelpers.subst_meta_and_metasenv_in_proof - proof goal subst metasenv - in - let opened = - ProofEngineHelpers.compare_metasenvs ~oldmetasenv - ~newmetasenv:metasenv - in - proof,opened - | Gaveup (tables,cache) -> - debug_print - (lazy ("TIME:"^ - string_of_float(Unix.gettimeofday()-.initial_time))); - raise (ProofEngineTypes.Fail (lazy "Auto gave up")) -;; -*) - (****************** smart application ********************) +let saturate_to_ref metasenv subst ctx nref ty = + let height = height_of_ref nref in + let rec aux metasenv ty args = + let ty,metasenv,moreargs = + NCicMetaSubst.saturate ~delta:height metasenv subst ctx ty 0 in + match ty with + | NCic.Const(NReference.Ref (_,NReference.Def _) as nre) + when nre<>nref -> + let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in + aux metasenv ty (args@moreargs) + | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl) + when nre<>nref -> + let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in + aux metasenv (NCic.Appl(bo::tl)) (args@moreargs) + | _ -> ty,metasenv,(args@moreargs) + in + aux metasenv ty [] let smart_apply t unit_eq status g = let n,h,metasenv,subst,o = status#obj in @@ -1257,10 +468,18 @@ let smart_apply t unit_eq status g = let status, t = disambiguate status ctx t None in let status,t = term_of_cic_term status t ctx in let ty = NCicTypeChecker.typeof subst metasenv ctx t in - let ty,metasenv,args = NCicMetaSubst.saturate metasenv subst ctx ty 0 in + let ty,metasenv,args = + match gty with + | NCic.Const(nref) + | NCic.Appl(NCic.Const(nref)::_) -> + saturate_to_ref metasenv subst ctx nref ty + | _ -> + 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 eq_coerc = let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in @@ -1422,65 +641,6 @@ exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive atoms of the input goals *) exception Proved of NTacStatus.tac_status -let height_of_ref (NReference.Ref (uri, x)) = - match x with - | NReference.Decl - | NReference.Ind _ - | NReference.Con _ - | NReference.CoFix _ -> - let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in - height - | NReference.Def h -> h - | NReference.Fix (_,_,h) -> h -;; - -let fast_height_of_term t = - let h = ref 0 in - let rec aux = - function - NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l - | NCic.Meta _ -> () - | NCic.Rel _ - | NCic.Sort _ -> () - | NCic.Implicit _ -> assert false - | NCic.Const nref as t -> -(* - prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] - ~context:[] t ^ ":" ^ string_of_int (height_of_ref nref)); -*) - h := max !h (height_of_ref nref) - | NCic.Prod (_,t1,t2) - | NCic.Lambda (_,t1,t2) -> aux t1; aux t2 - | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t - | NCic.Appl l -> List.iter aux l - | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl - in - aux t; !h -;; - -let height_of_goals status = - let open_goals = head_goals status#stack in - assert (List.length open_goals > 0); - let h = ref 1 in - List.iter - (fun open_goal -> - let ty = get_goalty status open_goal in - let context = ctx_of ty in - let _, ty = term_of_cic_term status ty (ctx_of ty) in - h := max !h (fast_height_of_term ty); - List.iter - (function - | _, NCic.Decl ty -> h := max !h (fast_height_of_term ty) - | _, NCic.Def (bo,ty) -> - h := max !h (fast_height_of_term ty); - h := max !h (fast_height_of_term bo); - ) - context) - open_goals; - debug_print (lazy ("altezza sequente: " ^ string_of_int !h)); - !h -;; - (* let close_failures _ c = c;; *) (* let prunable _ _ _ = false;; *) (* let cache_examine cache gty = `Notfound;; *) @@ -1521,7 +681,7 @@ let sort_new_elems l = let try_candidate ?(smart=0) flags depth status eq_cache t = try - debug_print ~depth (lazy ("------------ try " ^ CicNotationPp.pp_term t)); + debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t)); let status = if smart= 0 then NTactics.apply_tac ("",0,t) status else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status @@ -1539,8 +699,33 @@ let try_candidate ?(smart=0) flags depth status eq_cache t = with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None ;; +let sort_of metasenv ctx t = + let ty = NCicTypeChecker.typeof [] metasenv ctx t in + NCicTypeChecker.typeof [] metasenv ctx ty +;; + +let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ") +;; + +let perforate_small metasenv context t = + let rec aux = function + | NCic.Appl (hd::tl) -> + let map t = + let s = sort_of metasenv context t in + match s with + | NCic.Sort(NCic.Type [`Type,u]) + when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0)) + | _ -> aux t + in + NCic.Appl (hd::List.map map tl) + | t -> t + in + aux t +;; + let get_candidates ?(smart=true) status cache signature gty = let universe = status#auto_cache in + let _,_,metasenv,subst,_ = status#obj in let context = ctx_of gty in let t_ast t = let _status, t = term_of_cic_term status t context @@ -1548,6 +733,7 @@ let get_candidates ?(smart=true) status cache signature gty = let c_ast = function | NCic.Const r -> Ast.NRef r | _ -> assert false in let _, raw_gty = term_of_cic_term status gty context in +(* let raw_gty = NCicUntrusted.apply_subst subst context raw_gty in *) let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe raw_gty in let local_cands = search_in_th gty cache in @@ -1562,10 +748,11 @@ let get_candidates ?(smart=true) status cache signature gty = let smart_candidates = if smart then match raw_gty with - | NCic.Appl (hd::tl) -> - let weak_gty = + | NCic.Appl _ -> + let weak_gty = perforate_small metasenv context raw_gty in + (* NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0))) - (List.length tl)) in + (List.length tl)) in *) let more_cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe weak_gty in @@ -1587,9 +774,12 @@ let applicative_case depth signature status flags gty (cache:cache) = let _,_,metasenv,subst,_ = status#obj in let context = ctx_of gty in let tcache = cache.facts in - let is_eq = + let is_prod, is_eq = let status, t = term_of_cic_term status gty context in - NCicParamod.is_equation metasenv subst context t + let t = NCicReduction.whd subst context t in + match t with + | NCic.Prod _ -> true, false + | _ -> false, NCicParamod.is_equation metasenv subst context t in debug_print(lazy (string_of_bool is_eq)); let candidates, smart_candidates = @@ -1612,7 +802,8 @@ let applicative_case depth signature status flags gty (cache:cache) = (fun elems cand -> if (only_one && (elems <> [])) then elems else - if (maxd && not(is_a_fact_ast status subst metasenv context cand)) + if (maxd && not(is_prod) & + not(is_a_fact_ast status subst metasenv context cand)) then (debug_print (lazy "pruned: not a fact"); elems) else match try_candidate (~smart:sm) @@ -1628,7 +819,8 @@ let applicative_case depth signature status flags gty (cache:cache) = (fun elems cand -> if (only_one && (elems <> [])) then elems else - if (maxd && not(is_a_fact_ast status subst metasenv context cand)) + if (maxd && not(is_prod) && + not(is_a_fact_ast status subst metasenv context cand)) then (debug_print (lazy "pruned: not a fact"); elems) else match try_candidate (~smart:1) @@ -1754,6 +946,7 @@ let reduce ~depth status g = let do_something signature flags status g depth gty cache = (* whd *) let l = reduce ~depth status g in + (* if l <> [] then l,cache else *) (* backward aplications *) let l1 = List.map @@ -1763,14 +956,14 @@ let do_something signature flags status g depth gty cache = (auto_eq_check cache.unit_eq status) in let l2 = - (* if (l1 <> []) then [] else *) + if ((l1 <> []) && flags.last) then [] else applicative_case depth signature status flags gty cache (* fast paramodulation *) in (* states in l1 have have an empty set of subgoals: no point to sort them *) debug_print ~depth (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2))))); - l1 @ (sort_new_elems (l@l2)), cache + l1 @ (sort_new_elems (l @ l2)), cache ;; let pp_goal = function @@ -1865,9 +1058,8 @@ let deep_focus_tac level focus status = | (g, t, k, tag) :: s -> let f,o,gs = slice (level-1) s in let f1,o1 = List.partition in_focus g - in - (* we need to mark it as a BranchTag, otherwise cannot merge later *) - (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs + in + (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs in let gstatus = let f,o,s = slice level status#stack in f@o@s @@ -1902,13 +1094,25 @@ let rec auto_clusters ?(top=false) else let status = NTactics.merge_tac status in auto_clusters flags signature (cache:cache) (depth-1) status - else if List.length goals < 2 then - auto_main flags signature cache depth status + else if List.length goals < 2 then + auto_main flags signature cache depth status else let all_goals = open_goals (depth+1) status in debug_print ~depth (lazy ("goals = " ^ String.concat "," (List.map string_of_int all_goals))); let classes = HExtlib.clusters (deps status) all_goals in + List.iter + (fun gl -> + if List.length gl > flags.maxwidth then + (debug_print (lazy "FAIL GLOBAL WIDTH"); + raise (Gaveup IntSet.empty)) + else ()) classes; + if List.length classes = 1 then + let flags = + {flags with last = (List.length all_goals = 1)} in + (* no need to cluster *) + auto_main flags signature cache depth status + else let classes = if top then List.rev classes else classes in debug_print ~depth (lazy @@ -1920,6 +1124,8 @@ let rec auto_clusters ?(top=false) let status,b = List.fold_left (fun (status,b) gl -> + let flags = + {flags with last = (List.length gl = 1)} in let lold = List.length status#stack in debug_print ~depth (lazy ("stack length = " ^ (string_of_int lold))); @@ -1966,11 +1172,12 @@ auto_main flags signature (cache:cache) depth status: unit = in auto_clusters flags signature (cache:cache) (depth-1) status | orig::_ -> - let ng = List.length goals in + let ng = List.length goals in + (* moved inside auto_clusters *) if ng > flags.maxwidth then - (debug_print (lazy "FAIL WIDTH"); raise (Gaveup IntSet.empty)) - else if depth = flags.maxdepth then raise (Gaveup IntSet.empty) - else + (debug_print (lazy "FAIL LOCAL WIDTH"); raise (Gaveup IntSet.empty)) + else if depth = flags.maxdepth then raise (Gaveup IntSet.empty) + else let status = NTactics.branch_tac ~force:true status in let status, cache = intros ~depth status cache in let g,gctx, gty = current_goal status in @@ -1981,11 +1188,13 @@ auto_main flags signature (cache:cache) depth status: unit = if is_subsumed depth status closegty (snd cache.under_inspection) then (debug_print ~depth (lazy "SUBSUMED"); raise (Gaveup IntSet.add g IntSet.empty)) - else - let do_flags = - {flags with last = flags.last && ng=1} in + else + let new_sig = height_of_goal g status in + if new_sig < signature then + (debug_print (lazy ("news = " ^ (string_of_int new_sig))); + debug_print (lazy ("olds = " ^ (string_of_int signature)))); let alternatives, cache = - do_something signature do_flags status g depth gty cache in + do_something signature flags status g depth gty cache in let loop_cache = let l,tree = cache.under_inspection in let l,tree = closegty::l, add_to_th closegty tree closegty in @@ -1993,7 +1202,7 @@ auto_main flags signature (cache:cache) depth status: unit = List.iter (fun ((_,t),status) -> debug_print ~depth - (lazy("(re)considering goal " ^ + (lazy ("(re)considering goal " ^ (string_of_int g) ^" : "^ppterm status gty)); debug_print (~depth:depth) (lazy ("Case: " ^ CicNotationPp.pp_term t)); -- 2.39.2