From d0c7735ccdde99179105d56a8fafa22060aa6184 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 8 Apr 2010 16:38:53 +0000 Subject: [PATCH] New code (unbranched) to compute all keys by all possible ways of reducing the term. From: sacerdot --- helm/software/components/ng_tactics/nnAuto.ml | 130 ++++++++++++++++-- 1 file changed, 119 insertions(+), 11 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index b6bfbc6a3..323777d18 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -244,12 +244,12 @@ let solve f status eq_cache goal = with NCicRefiner.RefineFailure msg | NCicRefiner.Uncertain msg -> - print (lazy ("WARNING: refining in fast_eq_check failed\n" ^ + debug_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 -> - print (lazy ("WARNING: refining in fast_eq_check failed" ^ + debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^ Lazy.force msg ^ "\n in the environment\n" ^ NCicPp.ppmetasenv subst metasenv)); None @@ -584,9 +584,93 @@ let smart_apply_auto t eq_cache = type th_cache = (NCic.context * InvRelDiscriminationTree.t) list +(* cartesian: term set list -> term list set *) +let rec cartesian = + function + [] -> NDiscriminationTree.TermListSet.empty + | [l] -> + NDiscriminationTree.TermSet.fold + (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty + | he::tl -> + let rest = cartesian tl in + NDiscriminationTree.TermSet.fold + (fun x acc -> + NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc + ) he NDiscriminationTree.TermListSet.empty +;; + +(* all_keys_of_cic_type: term -> term set *) +let all_keys_of_cic_type metasenv subst context ty = + let saturate ty = + (* Here we are dropping the metasenv, but this should not raise any + exception (hopefully...) *) + let ty,_,hyps = + NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0 + in + ty,List.length hyps + in + let rec aux ty = + match ty with + NCic.Appl (he::tl) -> + let tl' = + List.map (fun ty -> + let wty = NCicReduction.whd ~delta:0 ~subst context ty in + if ty = wty then + NDiscriminationTree.TermSet.add ty (aux ty) + else + NDiscriminationTree.TermSet.union + (NDiscriminationTree.TermSet.add ty (aux ty)) + (NDiscriminationTree.TermSet.add wty (aux wty)) + ) tl + in + NDiscriminationTree.TermListSet.fold + (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc) + (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl')) + NDiscriminationTree.TermSet.empty + | _ -> NDiscriminationTree.TermSet.empty + in + let ty,ity = saturate ty in + let wty,iwty = saturate (NCicReduction.whd ~delta:0 ~subst context ty) in + if ty = wty then + [ity, NDiscriminationTree.TermSet.add ty (aux ty)] + else + [ity, NDiscriminationTree.TermSet.add ty (aux ty) ; + iwty, NDiscriminationTree.TermSet.add wty (aux wty) ] +;; + +let all_keys_of_type status t = + let _,_,metasenv,subst,_ = status#obj in + let context = ctx_of t in + let keys = + all_keys_of_cic_type metasenv subst context + (snd (term_of_cic_term status t context)) + in + status, + List.map + (fun (intros,keys) -> + intros, + NDiscriminationTree.TermSet.fold + (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc) + keys Ncic_termSet.empty + ) keys +;; + + let keys_of_type status orig_ty = + (* Here we are dropping the metasenv (in the status), but this should not + raise any exception (hopefully...) *) let _, ty, _ = saturate ~delta:max_int status orig_ty in - let keys = [ty] in + let keys = +(* + let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in + if orig_ty' <> orig_ty then + let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in + [ty;ty'] + else + [ty] +*) + [ty] in +(*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *) let keys = let _, ty = term_of_cic_term status ty (ctx_of ty) in match ty with @@ -600,6 +684,11 @@ let keys_of_type status orig_ty = status, keys ;; +let all_keys_of_term status t = + let status, orig_ty = typeof status (ctx_of t) t in + all_keys_of_type status orig_ty +;; + let keys_of_term status t = let status, orig_ty = typeof status (ctx_of t) t in keys_of_type status orig_ty @@ -928,11 +1017,28 @@ 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 cands = - NDiscriminationTree.DiscriminationTree.retrieve_unifiables - universe raw_gty - in + let keys = all_keys_of_cic_term metasenv subst context raw_gty in + (* we only keep those keys that do not require any intros for now *) + let no_intros_keys = snd (List.hd keys) in + let cands = + NDiscriminationTree.TermSet.fold + (fun ty acc -> + NDiscriminationTree.TermSet.union acc + (NDiscriminationTree.DiscriminationTree.retrieve_unifiables + universe ty) + ) no_intros_keys NDiscriminationTree.TermSet.empty in +(* old code: + let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables + universe raw_gty in +*) + let local_cands = + NDiscriminationTree.TermSet.fold + (fun ty acc -> + Ncic_termSet.union acc (search_in_th (mk_cic_term context ty) cache) + ) no_intros_keys Ncic_termSet.empty in +(* old code: let local_cands = search_in_th gty cache in +*) debug_print (lazy ("candidates for" ^ NTacStatus.ppterm status gty)); debug_print (lazy ("local cands = " ^ (string_of_int (List.length (Ncic_termSet.elements local_cands))))); let together global local = @@ -1135,11 +1241,13 @@ let rec intros ~depth status cache = | _ -> status, cache ;; -let reduce ~depth status g = +let reduce ~whd ~depth status g = let n,h,metasenv,subst,o = status#obj in let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in let ty = NCicUntrusted.apply_subst subst ctx ty in - let ty' = NCicReduction.whd ~subst ctx ty in + let ty' = + (if whd then NCicReduction.whd else NCicTacReduction.normalize) ~subst ctx ty + in if ty = ty' then [] else (debug_print ~depth @@ -1157,7 +1265,7 @@ let reduce ~depth status g = let do_something signature flags status g depth gty cache = (* whd *) - let l = reduce ~depth status g in + let l = (*reduce ~whd:true ~depth status g @*) reduce ~whd:true ~depth status g in (* if l <> [] then l,cache else *) (* backward aplications *) let l1 = @@ -1556,7 +1664,7 @@ let auto_tac ~params:(univ,flags) status = debug_print (lazy ("proved at depth " ^ string_of_int x)); List.iter (toref incr_uses statistics) trace; let trace = cleanup_trace s trace in - let _ = print (pptrace trace) in + let _ = debug_print (pptrace trace) in let stack = match s#stack with | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest -- 2.39.2