From 4c1ae9c678da6c94c69d3cb6d8cb296c32d324e6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 Apr 2010 19:55:18 +0000 Subject: [PATCH] auto destructs while introducing in the context From: tassi --- helm/software/components/ng_tactics/nnAuto.ml | 60 ++++++++++++++----- 1 file changed, 45 insertions(+), 15 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 323777d18..93078df25 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -166,7 +166,7 @@ let fast_height_of_term t = | NCic.Rel _ | NCic.Sort _ -> () | NCic.Implicit _ -> assert false - | NCic.Const nref as t -> + | NCic.Const nref -> (* prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t ^ ":" ^ string_of_int (height_of_ref nref)); @@ -284,6 +284,7 @@ let index_local_equations eq_cache status = 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 c = ref 0 in List.fold_left (fun eq_cache _ -> @@ -293,6 +294,7 @@ 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))); @@ -519,7 +521,7 @@ let saturate_to_ref metasenv subst ctx nref ty = | NCic.Const(NReference.Ref (_,NReference.Def _) as nre) when nre<>nref -> let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in - aux metasenv ty (args@moreargs) + aux metasenv bo (args@moreargs) | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl) when nre<>nref -> let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in @@ -641,6 +643,7 @@ let all_keys_of_cic_type metasenv subst context ty = let all_keys_of_type status t = let _,_,metasenv,subst,_ = status#obj in let context = ctx_of t in + let status, t = apply_subst status context t in let keys = all_keys_of_cic_type metasenv subst context (snd (term_of_cic_term status t context)) @@ -660,6 +663,7 @@ 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 _, ty = apply_subst status (ctx_of ty) ty in let keys = (* let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in @@ -772,7 +776,7 @@ let search_in_th gty th = | [] -> (* Ncic_termSet.elements *) acc | (_::tl) as k -> try - let idx = List.assq k th in + let idx = List.assoc(*q*) k th in let acc = Ncic_termSet.union acc (InvRelDiscriminationTree.retrieve_unifiables idx gty) in @@ -897,7 +901,7 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t = else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status else (* smart = 2: both *) try NTactics.apply_tac ("",0,t) status - with Error _ as exc -> + with Error _ -> smart_apply_auto ("",0,t) eq_cache status in (* @@ -1202,10 +1206,22 @@ let rec guess_name name ctx = let is_prod status = let _, ctx, gty = current_goal status in + let status, gty = apply_subst status ctx gty in let _, raw_gty = term_of_cic_term status gty ctx in match raw_gty with - | NCic.Prod (name,_,_) -> Some (guess_name name ctx) - | _ -> None + | NCic.Prod (name,src,_) -> + 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 + | [_,_,_,[_;_]] + | [_,_,_,[_]] + | [_,_,_,[]] -> `Inductive (guess_name name ctx) + | _ -> `Some (guess_name name ctx)) + | _ -> `Some (guess_name name ctx)) + | _ -> `None let intro ~depth status facts name = let status = NTactics.intro_tac name status in @@ -1219,26 +1235,36 @@ 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 - | Some(name) -> + | `Some(name) -> let status,facts = intro ~depth status facts name in intros_facts ~depth status facts + | `Inductive name -> + let status = NTactics.case1_tac name status in + intros_facts ~depth status facts | _ -> status, facts ;; -let rec intros ~depth status cache = +let intros ~depth status cache = match is_prod status with - | Some _ -> + | `Inductive _ + | `Some _ -> let trace = cache.trace in let status,facts = intros_facts ~depth status cache.facts in + if head_goals status#stack = [] then + let status = NTactics.merge_tac status in + [(0,Ast.Ident("__intros",None)),status], cache + else (* we reindex the equation from scratch *) - let unit_eq = - index_local_equations status#eq_cache status in - status, init_cache ~facts ~unit_eq () ~trace - | _ -> status, cache + let unit_eq = index_local_equations status#eq_cache status in + let status = NTactics.merge_tac status in + [(0,Ast.Ident("__intros",None)),status], + init_cache ~facts ~unit_eq () ~trace + | _ -> [],cache ;; let reduce ~whd ~depth status g = @@ -1264,6 +1290,9 @@ let reduce ~whd ~depth status g = ;; let do_something signature flags status g depth gty cache = + let l0, cache = intros ~depth status cache in + if l0 <> [] then l0, cache + else (* whd *) let l = (*reduce ~whd:true ~depth status g @*) reduce ~whd:true ~depth status g in (* if l <> [] then l,cache else *) @@ -1537,7 +1566,6 @@ auto_main flags signature cache depth status: unit = 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 let ctx,ty = close status g in let closegty = mk_cic_term ctx ty in @@ -1565,7 +1593,9 @@ auto_main flags signature cache depth status: unit = debug_print (~depth:depth) (lazy ("Case: " ^ CicNotationPp.pp_term t)); let depth,cache = - if t=Ast.Ident("__whd",None) then depth, cache + if t=Ast.Ident("__whd",None) || + t=Ast.Ident("__intros",None) + then depth, cache else depth+1,loop_cache in let cache = add_to_trace ~depth cache t in try -- 2.39.2