module U = CicUniv
module S = CicSubstitution
module PT = PrimitiveTactics
+module T = Tacticals
let fail_msg1 = "no applicable simplification"
(* lapply *******************************************************************)
let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
- (* ?(substs = []) *) what =
- let count_dependent_prods context t =
- let rec aux context p = function
- | Cic.Prod (name, t1, t2) ->
- if TC.does_not_occur context 0 1 t2 then p else
- let e = Some (name, Cic.Decl t1) in
- aux (e :: context) (succ p) t2
- | t -> p
+ (* ?(substs = []) *) ?to_what what =
+ let cut_tac term = PT.cut_tac ~mk_fresh_name_callback term in
+ let apply_tac term = PT.apply_tac term in
+ let strip_dependent_prods metasenv context t =
+ let irl = MI.identity_relocation_list_for_metavariable context in
+ let rec aux metasenv p xcontext = function
+ | Cic.Prod (name, t1, t2) when not (TC.does_not_occur xcontext 0 1 t2) ->
+ let index = MI.new_meta metasenv [] in
+ let metasenv = [index, context, t1] @ metasenv in
+ let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, irl) in
+ aux metasenv (succ p) (e :: xcontext) (S.subst s t2)
+ | Cic.Prod (name, t1, t2) -> metasenv, p, Some t1, t2
+ | t -> metasenv, p, None, t
in
- aux context 0 t
+ aux metasenv 0 context t
in
- let rec pad_context p context add_context =
- if List.length add_context >= p then add_context @ context
- else pad_context p context (None :: add_context)
- in
- let strip_dependent_prods metasenv context p t =
- let rec aux metasenv add_context q = function
- | Cic.Prod (name, t1, t2) when q > 0 ->
- let context_for_meta = pad_context p context add_context in
- let metasenv, index = MI.mk_implicit metasenv [] context_for_meta in
- let rs = MI.identity_relocation_list_for_metavariable context_for_meta in
- let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, rs) in
- aux metasenv (e :: add_context) (pred q) (S.subst s t2)
- | t -> metasenv, add_context, t
- in
- aux metasenv [] p t
- in
- let mk_body bo = function
- | Some (name, Cic.Decl t1) -> Cic.Lambda (name, t1, bo)
- | _ -> failwith "mk_body"
+ let rec mk_continuations p l =
+ if p <= 0 then l else mk_continuations (pred p) (T.id_tac :: l)
in
let lapply_tac (proof, goal) =
let xuri, metasenv, u, t = proof in
-(* preliminaries *)
- let metano, context, ty = CicUtil.lookup_meta goal metasenv in
+ let _, context, _ = CicUtil.lookup_meta goal metasenv in
let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
- let p = count_dependent_prods context lemma in
-(* stripping *)
- let metasenv, add_context, holed_lemma = strip_dependent_prods metasenv context p lemma in
- let proof = xuri, metasenv, u, t in
- let newmeta = MI.new_meta metasenv [] in
- let context = add_context @ context in
- let irl = MI.identity_relocation_list_for_metavariable context in
- let bo = List.fold_left mk_body (Cic.Meta (newmeta, irl)) add_context in
- let ty = S.lift p ty in
- let (xuri, metasenv, u, t), _ =
- PEH.subst_meta_in_proof proof metano bo [newmeta, context, ty]
- in
- prerr_endline (CicPp.ppterm holed_lemma);
-(* cut *)
- let status = (xuri, metasenv, u, t), newmeta in
- PET.apply_tactic (PT.cut_tac ~mk_fresh_name_callback holed_lemma) status
+ match strip_dependent_prods metasenv context lemma with
+ | metasenv, p, Some premise, conclusion ->
+ let premise_tac =
+ match to_what with
+ | None -> T.id_tac
+ | Some term -> PT.apply_tac term
+ in
+ let status = (xuri, metasenv, u, t), goal in
+ let tac = T.thens ~start:(cut_tac premise)
+ ~continuations:[
+ T.thens ~start:(cut_tac conclusion)
+ ~continuations:[ T.id_tac;
+ T.thens ~start:(PT.apply_tac what)
+ ~continuations:(mk_continuations p [PT.apply_tac ~term:(Cic.Rel 1)])
+ ]; premise_tac ]
+ in
+ PET.apply_tactic tac status
+ | metasenv, p, None, conclusion ->
+ failwith "lapply_tac: not implemented"
in
PET.mk_tactic lapply_tac
-
+
(* fwd **********************************************************************)
let fwd_simpl_tac ~what ~dbd =