From: Andrea Asperti Date: Fri, 28 Oct 2011 10:58:22 +0000 (+0000) Subject: -applicative_case has been rewritten and simplified; X-Git-Tag: make_still_working~2150 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eed8389a5e472a79d242d4ce43a82f1cd2ac13c1;p=helm.git -applicative_case has been rewritten and simplified; the strategy should be clear, now. - if we have an unkown ?n goal we instantiate it with I:True:Prop. Due to the topological ordering of goals, ?n should not appear in any other open goal, so its instantiation can be arbitrary. - paramodulation is has only an implicit knowledge of the symmetry of equality, hence it is in trouble to prove (a=b) = (b=a). A try_sym tactic has been added to smart application to cover this case. --- diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml index b841f87e7..af30fcf93 100644 --- a/matitaB/components/ng_tactics/nnAuto.ml +++ b/matitaB/components/ng_tactics/nnAuto.ml @@ -582,12 +582,42 @@ let smart_apply t unit_eq status g = raise (Error (lazy "eq_coerc non yet defined",Some e)) | Error _ as e -> debug_print (lazy "error"); raise e +let compare_statuses ~past ~present = + let _,_,past,_,_ = past#obj in + let _,_,present,_,_ = present#obj in + List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present), + List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past) +;; + +(* paramodulation has only an implicit knoweledge of the symmetry of equality; + hence it is in trouble in proving (a = b) = (b = a) *) +let try_sym tac status g = + (* put the right uri *) + let sym_eq = Ast.Appl [Ast.Ident("sym_eq",`Ambiguous); Ast.Implicit `Vector] in + let _,_,metasenv,subst,_ = status#obj in + let _, context, gty = List.assoc g metasenv in + let is_eq = + NCicParamod.is_equation status metasenv subst context gty + in + if is_eq then + try tac status g + with Error _ -> + let new_status = instantiate_with_ast status g ("",0,sym_eq) in + let go, _ = compare_statuses ~past:status ~present:new_status in + assert (List.length go = 1); + let ng = List.hd go in + tac new_status ng + else tac status g +;; + let smart_apply_tac t s = let unit_eq = index_local_equations s#eq_cache s in - NTactics.distribute_tac (smart_apply t unit_eq) s + NTactics.distribute_tac (try_sym (smart_apply t unit_eq)) s + (* NTactics.distribute_tac (smart_apply t unit_eq) s *) let smart_apply_auto t eq_cache = - NTactics.distribute_tac (smart_apply t eq_cache) + NTactics.distribute_tac (try_sym (smart_apply t eq_cache)) + (* NTactics.distribute_tac (smart_apply t eq_cache) *) (****************** types **************) @@ -1128,79 +1158,49 @@ let applicative_case depth signature status flags gty cache = | _ -> false, NCicParamod.is_equation status metasenv subst context t in 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 - (* 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 + let test = is_a_fact_ast status subst metasenv context in + let candidates_facts,candidates_other = (* 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",`Ambiguous) ::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 - (lazy ("smart candidates: " ^ - string_of_int (List.length smart_candidates))); - (* - let sm = 0 in - let smart_candidates = [] in *) + since superposition should take care of them; refl is an + exception since it prompts for convertibility *) + let l1,l2 = List.partition test candidates in + (* put the right uri *) + 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 + in let sm = if is_eq then 0 else 2 in - (* wrong: we constraint maxdepth for equality goals to three *) - (* let maxdepth = if is_eq then min flags.maxdepth 6 else flags.maxdepth in *) + let sm1 = if flags.last then 2 else 0 in let maxd = (depth + 1 = flags.maxdepth) in - let only_one = flags.last && maxd in - debug_print ~depth (lazy ("only_one: " ^ (string_of_bool only_one))); - debug_print ~depth (lazy ("maxd: " ^ (string_of_bool maxd))); - let elems = + let try_candidates only_one sm acc candidates = List.fold_left (fun elems cand -> if (only_one && (elems <> [])) then elems - else - if (maxd && not(is_prod) & - not(is_a_fact_ast status subst metasenv context cand)) - then (debug_print ~depth (lazy "pruned: not a fact"); elems) else match try_candidate (~smart:sm) flags depth status cache.unit_eq context cand with | None -> elems | Some x -> x::elems) - [] candidates - in - let more_elems = - if only_one && elems <> [] then elems - else - List.fold_left - (fun elems cand -> - if (only_one && (elems <> [])) then elems - else - if (maxd && not(is_prod) && - not(is_a_fact_ast status subst metasenv context cand)) - then (debug_print ~depth (lazy "pruned: not a fact"); elems) - else - match try_candidate (~smart:2) (* was smart:1 *) - flags depth status cache.unit_eq context cand with - | None -> elems - | Some x -> x::elems) - [] smart_candidates - in - elems@more_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 ;; exception Found