From 5f2a4177ea8f13e2f854cf64e36e1b24e9f001bd Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 19 Apr 2010 09:47:02 +0000 Subject: [PATCH] Elimination of recursive inductive types leads to looping. ELimnation of singleton types gives problems with negation. From: asperti --- helm/software/components/ng_tactics/nnAuto.ml | 71 ++++++++++++++----- 1 file changed, 52 insertions(+), 19 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 93078df25..39eb0baac 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -58,6 +58,14 @@ let toref f tbl t = | Ast.NCic _ (* local candidate *) | _ -> () +let is_relevant tbl item = + try + let v = RefHash.find tbl item in + if !(v.nominations) < 60 then true (* not enough info *) + else if !(v.uses) = 0 then false + else true + with Not_found -> true + let print_stat tbl = let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in let relevance v = float !(v.uses) /. float !(v.nominations) in @@ -65,10 +73,12 @@ let print_stat tbl = Pervasives.compare (relevance v1) (relevance v2) in let l = List.sort vcompare l in let vstring (a,v)= - CicNotationPp.pp_term (Ast.NRef a) ^ ": rel = " ^ + CicNotationPp.pp_term (Ast.NCic (NCic.Const a)) ^ ": rel = " ^ (string_of_float (relevance v)) ^ - "; uses = " ^ (string_of_int !(v.uses)) in - lazy (String.concat "\n" (List.map vstring l)) + "; uses = " ^ (string_of_int !(v.uses)) ^ + "; nom = " ^ (string_of_int !(v.nominations)) in + lazy ("\n\nSTATISTICS:\n" ^ + String.concat "\n" (List.map vstring l)) (* ======================= utility functions ========================= *) module IntSet = Set.Make(struct type t = int let compare = compare end) @@ -259,7 +269,7 @@ let solve f status eq_cache goal = (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty)) ;; -let fast_eq_check eq_cache status goal = +let fast_eq_check eq_cache status (goal:int) = match solve NCicParamod.fast_eq_check status eq_cache goal with | [] -> raise (Error (lazy "no proof found",None)) | s::_ -> s @@ -274,17 +284,15 @@ let auto_eq_check eq_cache status = let s = dist_fast_eq_check eq_cache status in [s] with - | Error _ -> [] + | Error _ -> debug_print (lazy ("no paramod proof found"));[] ;; -(* warning: ctx is supposed to be already instantiated w.r.t subst *) let index_local_equations eq_cache status = debug_print (lazy "indexing equations"); let open_goals = head_goals status#stack in let open_goal = List.hd open_goals in let ngty = get_goalty status open_goal in - let ctx = ctx_of ngty in - let ctx = apply_subst_context ~fix_projections:true status ctx in + let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in let c = ref 0 in List.fold_left (fun eq_cache _ -> @@ -294,7 +302,6 @@ let index_local_equations eq_cache status = let ty = NCicTypeChecker.typeof [] [] ctx t in if is_a_fact status (mk_cic_term ctx ty) then (debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty))); - debug_print(lazy("riprovo " ^ (ppterm status (mk_cic_term ctx ty)))); NCicParamod.forward_infer_step eq_cache t ty) else (debug_print (lazy ("not a fact: " ^ (NCicPp.ppterm ctx [] [] ty))); @@ -985,8 +992,11 @@ let get_candidates ?(smart=true) depth flags status cache signature gty = | None -> let mapf s = let to_ast = function - | NCic.Const r -> Ast.NRef r | _ -> assert false in - List.map to_ast (NDiscriminationTree.TermSet.elements s) in + | NCic.Const r when true (*is_relevant statistics r*) -> Some (Ast.NRef r) + | NCic.Const _ -> None + | _ -> assert false in + HExtlib.filter_map + to_ast (NDiscriminationTree.TermSet.elements s) in let g,l = get_cands (NDiscriminationTree.DiscriminationTree.retrieve_unifiables @@ -1101,10 +1111,32 @@ let applicative_case depth signature status flags gty cache = | NCic.Prod _ -> true, false | _ -> false, NCicParamod.is_equation metasenv subst context t in - debug_print(lazy (string_of_bool is_eq)); + debug_print~depth (lazy (string_of_bool is_eq)); + (* old let candidates, smart_candidates = get_candidates ~smart:(not is_eq) depth - flags status tcache signature gty in + flags status tcache signature gty in + (* if the goal is an equation we avoid to apply unit equalities, + since superposition should take care of them; refl is an + exception since it prompts for convertibility *) + let candidates = + let test x = not (is_a_fact_ast status subst metasenv context x) in + if is_eq then + Ast.Ident("refl",None) ::List.filter test candidates + else candidates in *) + (* new *) + let candidates, smart_candidates = + get_candidates ~smart:true depth + flags status tcache signature gty in + (* if the goal is an equation we avoid to apply unit equalities, + since superposition should take care of them; refl is an + exception since it prompts for convertibility *) + let candidates,smart_candidates = + let test x = not (is_a_fact_ast status subst metasenv context x) in + if is_eq then + Ast.Ident("refl",None) ::List.filter test candidates, + List.filter test smart_candidates + else candidates,smart_candidates in debug_print ~depth (lazy ("candidates: " ^ string_of_int (List.length candidates))); debug_print ~depth @@ -1210,13 +1242,13 @@ let is_prod status = let _, raw_gty = term_of_cic_term status gty ctx in match raw_gty with | NCic.Prod (name,src,_) -> - let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in + let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in (match snd (term_of_cic_term status src ctx) with | NCic.Const(NReference.Ref (_,NReference.Ind _) as r) | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) -> let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys r in (match itys with - | [_,_,_,[_;_]] + (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *) | [_,_,_,[_]] | [_,_,_,[]] -> `Inductive (guess_name name ctx) | _ -> `Some (guess_name name ctx)) @@ -1237,13 +1269,14 @@ let intro ~depth status facts name = let rec intros_facts ~depth status facts = if List.length (head_goals status#stack) <> 1 then status, facts else match is_prod status with + | `Inductive name | `Some(name) -> let status,facts = intro ~depth status facts name - in intros_facts ~depth status facts - | `Inductive name -> + in intros_facts ~depth status facts +(* | `Inductive name -> let status = NTactics.case1_tac name status in - intros_facts ~depth status facts + intros_facts ~depth status facts *) | _ -> status, facts ;; @@ -1704,7 +1737,7 @@ let auto_tac ~params:(univ,flags) status = oldstatus#set_status s in let s = up_to depth depth in - debug_print (print_stat statistics); + print (print_stat statistics); debug_print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); debug_print(lazy -- 2.39.2