| _, t -> metasenv, metas, conts
in
aux metasenv [] [] to_what (how_many, term)
-
-let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+
+let get_clearables context terms =
+ let aux = function
+ | Cic.Rel i
+ | Cic.Appl (Cic.Rel i :: _) -> PEH.get_name context i
+ | _ -> None
+ in
+ PEH.list_rev_map_filter aux terms
+
+let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
(* ?(substs = []) *) ?how_many ?(to_what = []) what =
let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term in
let lapply_tac (proof, goal) =
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
let lemma = FNG.clean_dummy_dependent_types lemma in
- let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in
+ let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in
let conclusion =
match metas with [] -> what | _ -> Cic.Appl (what :: List.rev metas)
in
- let tac = T.then_ ~start:(letin_tac conclusion)
- ~continuation:(clearbody ~index:1)
+ let tac =
+ T.then_ ~start:(letin_tac conclusion)
+ ~continuation:(clearbody ~index:1)
in
let proof = (xuri, metasenv, u, t) in
let aux (proof, goals) (tac, goal) =
List.fold_left aux (proof, []) ((tac, goal) :: conts)
in
PET.mk_tactic lapply_tac
-
+
+let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+ (* ?(substs = []) *) ?(linear = false) ?how_many ?(to_what = []) what =
+ let lapply_tac status =
+ let proof, goal = status in
+ let _, metasenv, _, _ = proof in
+ let _, context, _ = CicUtil.lookup_meta goal metasenv in
+ let lapply = lapply_tac_aux ~mk_fresh_name_callback ?how_many ~to_what what in
+ let tac =
+ if linear then
+ let hyps = get_clearables context (what :: to_what) in
+ T.then_ ~start:lapply
+ ~continuation:(PESR.clear ~hyps) (* T.try_tactic ~tactic: *)
+ else
+ lapply
+ in
+ PET.apply_tactic tac status
+ in
+ PET.mk_tactic lapply_tac
+
(* fwd **********************************************************************)
let fwd_simpl_tac
| uri :: _ ->
Printf.eprintf "fwd: %s\n" (UriManager.string_of_uri uri); flush stderr;
let start = lapply_tac (Cic.Rel index) (Cic.Const (uri, [])) in
- let tac = T.then_ ~start ~continuation:(PESR.clear hyp) in
+ let tac = T.then_ ~start ~continuation:(PESR.clear ~hyps:[hyp]) in
PET.apply_tactic tac status
in
PET.mk_tactic fwd_simpl_tac