X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FprimitiveTactics.ml;h=e17d6cb7b68f16c5f4bac08b75fe91d3bdda4506;hb=797f61edb93f41eb2c5e281bc9457f6bff633063;hp=aeb0c0751286285b637a1cff94aae6854ee3cae4;hpb=ac741958783108ff31552e533c853e85c2ebb1c5;p=helm.git diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index aeb0c0751..e17d6cb7b 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -494,6 +494,58 @@ 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' = 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 + mk_pred metasenv (hyp :: context') pred arg' tail + in + let metasenv, pred, arg = mk_pred metasenv context goal arg actual_args in + HLog.debug ("PRED: " ^ 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 @@ -559,9 +611,9 @@ 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, _subst, proofbo, proofty, attrs = proof in @@ -610,67 +662,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 = @@ -698,6 +703,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = 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