-(*
-
-
-
-let skip_metas p =
- let rec aux conts p =
- if p <= 0 then conts else aux (T.id_tac :: conts) (pred p)
- in
- aux [] p
-
-let get_conclusion context t =
- let rec aux p context = function
- | Cic.Prod (name, t1, t2) ->
- aux (succ p) (Some (name, Cic.Decl t1) :: context) t2
- | Cic.LetIn (name, u1, t2) ->
- aux (succ p) (Some (name, Cic.Def (u1, None)) :: context) t2
- | Cic.Cast (t2, t1) -> aux p context t2
- | t -> p, context, t
- in aux 0 context t
-
-let get_conclusion_dependences context t =
- let p, context, conclusion = get_conclusion context t in
- let rec aux l q =
- if q <= 0 then l else
- let b = TC.does_not_occur context (pred q) q conclusion in
- aux (b :: l) (pred q)
- in
- aux [] p
-
-let solve_independents ?with_what deps =
- let rec aux p conts = function
- | [] -> p, conts
- | true :: tl ->
- let cont = PT.apply_tac ~term:(Cic.Rel (succ p)) in
- aux (succ p) (cont :: conts) tl
- | false :: tl -> aux (succ p) conts tl
- in
- let p, conts = aux 0 [] deps in
- match with_what with
- | None -> conts
- | Some t -> PT.apply_tac ~term:(S.lift p t) :: conts
-
-let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
- (* ?(substs = []) *) ?to_what what =
- let cut_tac term = PT.cut_tac ~mk_fresh_name_callback term in
- let intros_tac () = PT.intros_tac ~mk_fresh_name_callback () in
- let solve_conclusion_tac ?with_what p deps =
- T.then_ ~start:(intros_tac ())
- ~continuation:(
- T.thens ~start:(PT.apply_tac what)
- ~continuations:( [ T.id_tac; T.id_tac; T.id_tac ]
-(* skip_metas p @ solve_independents ?with_what deps *)
- )
- )
- in
- let lapply_tac (proof, goal) =
- let xuri, metasenv, u, t = proof in
- 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
- match strip_dependent_prods metasenv context lemma with
- | metasenv, p, Some premise, conclusion ->
- let deps = get_conclusion_dependences context conclusion in
- let inner_tac = match to_what with
- | None ->
- T.thens ~start:(cut_tac premise)
- ~continuations:[
- solve_conclusion_tac ~with_what:(Cic.Rel 1) p deps;
- T.id_tac
- ]
- | Some with_what ->
- solve_conclusion_tac ~with_what p deps
- in
- let outer_tac =
- T.thens ~start:(cut_tac conclusion)
- ~continuations:[T.id_tac; T.id_tac (* inner_tac *)]
- in
-*)