From 365bd84918e8e2fe0c6f3714b94e81b443a8f244 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 7 Nov 2011 09:02:42 +0000 Subject: [PATCH] New management of justifications. Justifications do not contain neither facts nor local hypothesis, hence they must be computed by auto. --- matitaB/components/ng_tactics/nnAuto.ml | 241 +++++++++++++++--------- 1 file changed, 157 insertions(+), 84 deletions(-) diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml index fc8c83938..201f522d0 100644 --- a/matitaB/components/ng_tactics/nnAuto.ml +++ b/matitaB/components/ng_tactics/nnAuto.ml @@ -1028,6 +1028,154 @@ let get_cands retrieve_for diff empty gty weak_gty = cands, diff more_cands cands ;; +let get_candidates ?(smart=true) depth flags status cache signature gty = + let universe = status#auto_cache in + let _,_,metasenv,subst,_ = status#obj in + let context = ctx_of gty in + let _, raw_gty = term_of_cic_term status gty context in + let is_prod, is_eq = + let status, t = term_of_cic_term status gty context in + let t = NCicReduction.whd status subst context t in + match t with + | NCic.Prod _ -> true, false + | _ -> false, NCicParamod.is_equation status metasenv subst context t + in + debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty)); + let is_eq = + NCicParamod.is_equation status metasenv subst context raw_gty + in + let raw_weak_gty, weak_gty = + if smart then + match raw_gty with + | NCic.Appl _ + | NCic.Const _ + | NCic.Rel _ -> + let raw_weak = + perforate_small status subst metasenv context raw_gty in + let weak = mk_cic_term context raw_weak in + debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak)); + Some raw_weak, Some (weak) + | _ -> None,None + else None,None + in + (* we now compute global candidates *) + let global_cands, smart_global_cands = + let mapf s = + let to_ast = function + | 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 universe) + NDiscriminationTree.TermSet.diff + NDiscriminationTree.TermSet.empty + raw_gty raw_weak_gty in + mapf g, mapf l in + (* we now compute local candidates *) + let local_cands,smart_local_cands = + let mapf s = + let to_ast t = + let _status, t = term_of_cic_term status t context + in Ast.NCic t in + List.map to_ast (Ncic_termSet.elements s) in + let g,l = + get_cands + (fun ty -> search_in_th ty cache) + Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in + mapf g, mapf l in + (* we now splits candidates in facts or not facts *) + let test = is_a_fact_ast status subst metasenv context in + let by,given_candidates = + match flags.candidates with + | Some l -> true, l + | None -> false, [] in + (* we compute candidates to be applied in normal mode, splitted in + facts and not facts *) + let candidates_facts,candidates_other = + (* warning : the order between global_cands and local_cand is + relevant. In this way we process first local cands *) + let l1,l2 = List.partition test (global_cands@local_cands) 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 l1 = if is_eq then [Ast.Ident("refl",`Ambiguous)] else l1 in + let l2 = + (* if smart given candidates are applied in smart mode *) + if by && smart then [] + else if by then given_candidates + else l2 + in l1,l2 + in + (* we now compute candidates to be applied in smart mode, splitted in + facts and not facts *) + let smart_candidates_facts, smart_candidates_other = + if is_prod || not(smart) then [],[] + else + let l1,l2 = List.partition test (smart_local_cands@smart_global_cands) in + let l1 = if is_eq then [] else l1 in + let l2 = if by then given_candidates else l2 + in + l1,l2 + in + candidates_facts, + smart_candidates_facts, + sort_candidates status context (candidates_other), + sort_candidates status context (smart_candidates_other) +;; + +let applicative_case depth signature status flags gty cache = + app_counter:= !app_counter+1; + let _,_,metasenv,subst,_ = status#obj in + let context = ctx_of gty in + let tcache = cache.facts in + let is_prod, is_eq = + let status, t = term_of_cic_term status gty context in + let t = NCicReduction.whd status subst context t in + match t with + | NCic.Prod _ -> true, false + | _ -> false, NCicParamod.is_equation status metasenv subst context t + in + debug_print ~depth (lazy (string_of_bool is_eq)); + (* new *) + let candidates_facts, smart_candidates_facts, + candidates_other, smart_candidates_other = + get_candidates ~smart:true depth + flags status tcache signature gty + in + let sm = if is_eq || is_prod then 0 else 2 in + let sm1 = if flags.last then 2 else 0 in + let maxd = (depth + 1 = flags.maxdepth) in + let try_candidates only_one sm acc candidates = + List.fold_left + (fun elems cand -> + if (only_one && (elems <> [])) then elems + else + match try_candidate (~smart:sm) + flags depth status cache.unit_eq context cand with + | None -> elems + | Some x -> x::elems) + acc candidates + in + (* if the goal is the last one we stop at the first fact *) + let elems = try_candidates flags.last sm [] candidates_facts in + (* now we add smart_facts *) + let elems = try_candidates flags.last sm elems smart_candidates_facts in + (* if we are at maxdepth and the goal is not a product we are done + similarly, if the goal is the last one and we already found a + solution *) + if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems + else + let elems = try_candidates false 2 elems candidates_other in + debug_print ~depth (lazy ("not facts: try smart application")); + try_candidates false 2 elems smart_candidates_other +;; + + +(* let get_candidates ?(smart=true) depth flags status cache signature gty = let maxd = ((depth + 1) = flags.maxdepth) in let universe = status#auto_cache in @@ -1082,87 +1230,8 @@ let get_candidates ?(smart=true) depth flags status cache signature gty = mapf g, mapf l in sort_candidates status context (global_cands@local_cands), sort_candidates status context (smart_global_cands@smart_local_cands) -;; - -(* old version -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 - in Ast.NCic t in - 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 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 = - List.map c_ast - (List.filter (only signature context) - (NDiscriminationTree.TermSet.elements global)) @ - List.map t_ast (Ncic_termSet.elements local) in - let candidates = together cands local_cands in - let candidates = sort_candidates status context candidates in - let smart_candidates = - if smart then - match raw_gty with - | NCic.Appl _ - | NCic.Const _ - | NCic.Rel _ -> - let weak_gty = perforate_small status subst metasenv context raw_gty in - (* - NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0))) - (List.length tl)) in *) - let more_cands = - NDiscriminationTree.DiscriminationTree.retrieve_unifiables - universe weak_gty - in - let smart_cands = - NDiscriminationTree.TermSet.diff more_cands cands in - let cic_weak_gty = mk_cic_term context weak_gty in - let more_local_cands = search_in_th cic_weak_gty cache in - let smart_local_cands = - Ncic_termSet.diff more_local_cands local_cands in - together smart_cands smart_local_cands - (* together more_cands more_local_cands *) - | _ -> [] - else [] - in - let smart_candidates = sort_candidates status context smart_candidates in - (* if smart then smart_candidates, [] - else candidates, [] *) - candidates, smart_candidates ;; -let get_candidates ?(smart=true) flags status cache signature gty = - match flags.candidates with - | None -> get_candidates ~smart status cache signature gty - | Some l -> l,[] -;; *) - let applicative_case depth signature status flags gty cache = app_counter:= !app_counter+1; let _,_,metasenv,subst,_ = status#obj in @@ -1190,8 +1259,11 @@ let applicative_case depth signature status flags gty cache = if is_eq then [Ast.Ident("refl",`Ambiguous)],l2 else l1,l2 in let smart_candidates_facts, smart_candidates_other = - let l1,l2 = List.partition test smart_candidates in - if is_eq then [],l2 else l1,l2 + match flags.candidates with + | Some l -> [],l + | None -> + let l1,l2 = List.partition test smart_candidates in + if is_eq then [],l2 else l1,l2 in let sm = if is_eq then 0 else 2 in let sm1 = if flags.last then 2 else 0 in @@ -1219,10 +1291,11 @@ let applicative_case depth signature status flags gty cache = let elems = try_candidates false 2 elems candidates_other in debug_print ~depth (lazy ("not facts: try smart application")); try_candidates false 2 elems smart_candidates_other -;; +;; *) exception Found -;; +;; + (* gty is supposed to be meta-closed *) @@ -1789,7 +1862,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = let _,res = term_of_cic_term status res (ctx_of res) in Ast.NCic res in Some (List.map to_Ast l) - in + in let depth = int "depth" flags 3 in let size = int "size" flags 10 in let width = int "width" flags 4 (* (3+List.length goals)*) in -- 2.39.2