X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FprimitiveTactics.ml;h=47acc7c583a30cc789d96439852dfc5361b70aa2;hb=6ad533c972e6c9e9db53f38f972e7c0792160f2e;hp=64db996667879cd10efb1adf0ad83b7032fd2a94;hpb=f63581865541fbda2a55c931563dc58a30d31615;p=helm.git diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 64db99666..47acc7c58 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -52,9 +52,13 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name = match ty with C.Cast (te,_) -> collect_context context howmany do_whd te | C.Prod (n,s,t) -> - let n' = mk_fresh_name metasenv context n ~typ:s in + let n' = mk_fresh_name metasenv context n ~typ:s in let (context',ty,bo) = - let ctx = (Some (n',(C.Decl s)))::context in + let entry = match n' with + | C.Name _ -> Some (n',(C.Decl s)) + | C.Anonymous -> None + in + let ctx = entry :: context in collect_context ctx (howmany - 1) do_whd t in (context',ty,C.Lambda(n',s,bo)) @@ -257,7 +261,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) = let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in - let (_,metasenv,_,_, _) = proof in + let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = @@ -321,7 +325,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) = let subst_in = (* if we just apply the subtitution, the type is irrelevant: we may use Implicit, since it will be dropped *) - CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst) + ((metano,(context,bo',Cic.Implicit None))::subst) in let (newproof, newmetasenv''') = ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in @@ -365,13 +369,11 @@ let apply_tac ~term = PET.mk_tactic (apply_tac ~term) let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ()= - let intros_tac - ?(mk_fresh_name_callback = (FreshNamesGenerator.mk_fresh_name ~subst:[])) () - (proof, goal) + let intros_tac (proof, goal) = let module C = Cic in let module R = CicReduction in - let (_,metasenv,_,_, _) = proof in + let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in let (context',ty',bo') = @@ -383,7 +385,7 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_ in (newproof, [newmeta]) in - PET.mk_tactic (intros_tac ~mk_fresh_name_callback ()) + PET.mk_tactic intros_tac let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term = let cut_tac @@ -391,7 +393,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst: term (proof, goal) = let module C = Cic in - let curi,metasenv,pbo,pty, attrs = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in let newmeta2 = newmeta1 + 1 in @@ -407,11 +409,16 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst: CicMkImplicit.identity_relocation_list_for_metavariable context in let newmeta1ty = CicSubstitution.lift 1 ty in +(* This is the pre-letin implementation let bo' = C.Appl [C.Lambda (fresh_name,term,C.Meta (newmeta1,irl1)) ; C.Meta (newmeta2,irl2)] in +*) + let bo' = + Cic.LetIn (fresh_name, C.Meta (newmeta2,irl2), C.Meta (newmeta1,irl1)) + in let (newproof, _) = ProofEngineHelpers.subst_meta_in_proof proof metano bo' [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty]; @@ -426,7 +433,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: term (proof, goal) = let module C = Cic in - let curi,metasenv,pbo,pty, attrs = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in (* occur check *) let occur i t = let m = CicUtil.metas_of_term t in @@ -462,7 +469,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: let exact_tac ~term = let exact_tac ~term (proof, goal) = (* Assumption: the term bo must be closed in the current context *) - let (_,metasenv,_,_, _) = proof in + let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let module T = CicTypeChecker in let module R = CicReduction in @@ -492,10 +499,65 @@ module S = CicSubstitution module T = Tacticals module RT = ReductionTactics +let rec args_init n f = + if n <= 0 then [] else f n :: args_init (pred n) f + +let mk_predicate_for_elim + ~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no = + let instantiated_eliminator = + let f n = if n = 1 then arg else C.Implicit None in + C.Appl (using :: args_init args_no f) + in + let _actual_arg, iety, _metasenv', _ugraph = + CicRefine.type_of_aux' metasenv context instantiated_eliminator ugraph + in + let _actual_meta, actual_args = match iety with + | C.Meta (i, _) -> i, [] + | C.Appl (C.Meta (i, _) :: args) -> i, args + | _ -> assert false + in +(* let _, upto = PEH.split_with_whd (List.nth splits pred_pos) in *) + let rec mk_pred metasenv context' pred arg' cpattern' = function + | [] -> metasenv, pred, arg' + | arg :: tail -> +(* FG: we find the predicate for the eliminator as in the rewrite tactic ****) + let argty, _ugraph = TC.type_of_aux' metasenv context arg ugraph in + let argty = CicReduction.whd context argty in + let fresh_name = + FreshNamesGenerator.mk_fresh_name + ~subst:[] metasenv context' C.Anonymous ~typ:argty + in + let hyp = Some (fresh_name, C.Decl argty) in + let lazy_term c m u = + let distance = List.length c - List.length context in + S.lift distance arg, m, u + in + let pattern = Some lazy_term, [], Some cpattern' in + let subst, metasenv, _ugraph, _conjecture, selected_terms = + ProofEngineHelpers.select + ~metasenv ~ugraph ~conjecture:(0, context, pred) ~pattern + in + let metasenv = MS.apply_subst_metasenv subst metasenv in + let map (_context_of_t, t) l = t :: l in + let what = List.fold_right map selected_terms [] in + let arg' = MS.apply_subst subst arg' in + let argty = MS.apply_subst subst argty in + let pred = PER.replace_with_rel_1_from ~equality:(==) ~what 1 pred in + let pred = MS.apply_subst subst pred in + let pred = C.Lambda (fresh_name, argty, pred) in + let cpattern' = C.Lambda (C.Anonymous, C.Implicit None, cpattern') in + mk_pred metasenv (hyp :: context') pred arg' cpattern' tail + in + let metasenv, pred, arg = + mk_pred metasenv context goal arg cpattern (List.rev actual_args) + in + HLog.debug ("PREDICATE: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args)); + metasenv, pred, arg, actual_args + let beta_after_elim_tac upto predicate = let beta_after_elim_tac status = let proof, goal = status in - let _, metasenv, _, _, _ = proof in + let _, metasenv, _subst, _, _, _ = proof in let _, _, ty = CicUtil.lookup_meta goal metasenv in let mk_pattern ~equality ~upto ~predicate ty = (* code adapted from ProceduralConversion.generalize *) @@ -557,12 +619,12 @@ let beta_after_elim_tac upto predicate = let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = let elim_tac (proof, goal) = - let cpatt = match pattern with - | None, [], Some cpatt -> cpatt - | _ -> raise (PET.Fail (lazy "not implemented")) + let cpattern = match pattern with + | None, [], Some cpattern -> cpattern + | _ -> raise (PET.Fail (lazy "not implemented")) in let ugraph = CicUniv.empty_ugraph in - let curi, metasenv, proofbo, proofty, attrs = proof in + let curi, metasenv, _subst, proofbo, proofty, attrs = proof in let conjecture = CicUtil.lookup_meta goal metasenv in let metano, context, ty = conjecture in let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in @@ -608,67 +670,20 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = TC.type_of_aux' metasenv' context eliminator_ref ugraph in (* FG: ADDED PART ***********************************************************) (* FG: we can not assume eliminator is the default eliminator ***************) - let rec args_init n f = - if n <= 0 then [] else f n :: args_init (pred n) f - in let splits, args_no = PEH.split_with_whd (context, ety) in let pred_pos = match List.hd splits with | _, C.Rel i when i > 1 && i <= args_no -> i | _, C.Appl (C.Rel i :: _) when i > 1 && i <= args_no -> i | _ -> raise NotAnEliminator in - let upto, metasenv', pred, term = match pattern with + let metasenv', pred, term, actual_args = match pattern with | None, [], Some (C.Implicit (Some `Hole)) -> - 0, metasenv', C.Implicit None, term + metasenv', C.Implicit None, term, [] | _ -> - let instantiated_eliminator = - let f n = if n = 1 then term else C.Implicit None in - C.Appl (eliminator_ref :: args_init args_no f) - in - let _actual_term, iety, _metasenv'', _ugraph = - CicRefine.type_of_aux' metasenv' context instantiated_eliminator ugraph - in - let _actual_meta, actual_args = match iety with - | C.Meta (i, _) -> i, [] - | C.Appl (C.Meta (i, _) :: args) -> i, args - | _ -> assert false - in - (* let _, upto = PEH.split_with_whd (List.nth splits pred_pos) in *) - let upto = List.length actual_args in - let rec mk_pred metasenv context' pred term' = function - | [] -> metasenv, pred, term' - | term :: tail -> -(* FG: we find the predicate for the eliminator as in the rewrite tactic ****) - let termty, _ugraph = TC.type_of_aux' metasenv context' term ugraph in - let termty = CicReduction.whd context' termty in - let fresh_name = - FreshNamesGenerator.mk_fresh_name - ~subst:[] metasenv context' C.Anonymous ~typ:termty - in - let hyp = Some (fresh_name, C.Decl termty) in - let lazy_term c m u = - let distance = List.length c - List.length context in - S.lift distance term, m, u - in - let pattern = Some lazy_term, [], Some cpatt in - let subst, metasenv, _ugraph, _conjecture, selected_terms = - ProofEngineHelpers.select - ~metasenv ~ugraph ~conjecture:(metano, context, pred) ~pattern - in - let metasenv = MS.apply_subst_metasenv subst metasenv in - let map (_context_of_t, t) l = t :: l in - let what = List.fold_right map selected_terms [] in - let term' = MS.apply_subst subst term' in - let termty = MS.apply_subst subst termty in - let pred = PER.replace_with_rel_1_from ~equality:(==) ~what 1 pred in - let pred = MS.apply_subst subst pred in - let pred = C.Lambda (fresh_name, termty, pred) in - mk_pred metasenv (hyp :: context') pred term' tail - in - let metasenv', pred, term = mk_pred metasenv' context ty term actual_args in - HLog.debug ("PRED: " ^ CicPp.ppterm ~metasenv:metasenv' pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv:metasenv') actual_args)); - upto, metasenv', pred, term - in + mk_predicate_for_elim + ~args_no ~context ~ugraph ~cpattern + ~metasenv:metasenv' ~arg:term ~using:eliminator_ref ~goal:ty + in (* FG: END OF ADDED PART ****************************************************) let term_to_refine = let f n = @@ -684,18 +699,19 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv:metasenv'' in - let proof' = curi,metasenv'',proofbo,proofty, attrs in + let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in let proof'', new_goals' = PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal) in (* The apply_tactic can have closed some of the new_goals *) let patched_new_goals = - let (_,metasenv''',_,_, _) = proof'' in + let (_,metasenv''',_subst,_,_, _) = proof'' in List.filter (function i -> List.exists (function (j,_,_) -> j=i) metasenv''') new_goals @ new_goals' in let res = proof'', patched_new_goals in + let upto = List.length actual_args in if upto = 0 then res else let continuation = beta_after_elim_tac upto pred in let dummy_status = proof,goal in @@ -706,13 +722,13 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = PET.mk_tactic elim_tac ;; -let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term = +let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term = let cases_tac ~term (proof, goal) = let module TC = CicTypeChecker in let module U = UriManager in let module R = CicReduction in let module C = Cic in - let (curi,metasenv,proofbo,proofty, attrs) = proof in + let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in let termty = CicReduction.whd context termty in @@ -823,13 +839,13 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv:metasenv'' in - let proof' = curi,metasenv'',proofbo,proofty, attrs in + let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in let proof'', new_goals' = PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal) in (* The apply_tactic can have closed some of the new_goals *) let patched_new_goals = - let (_,metasenv''',_,_,_) = proof'' in + let (_,metasenv''',_subst,_,_,_) = proof'' in List.filter (function i -> List.exists (function (j,_,_) -> j=i) metasenv''') new_goals @ new_goals' @@ -864,7 +880,7 @@ let letout_tac = let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in let term = C.Sort C.Set in let letout_tac (proof, goal) = - let curi, metasenv, pbo, pty, attrs = proof in + let curi, metasenv, _subst, pbo, pty, attrs = proof in let metano, context, ty = CicUtil.lookup_meta goal metasenv in let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in