module MI = CicMkImplicit
module TC = CicTypeChecker
module PET = ProofEngineTypes
+module PEH = ProofEngineHelpers
module U = CicUniv
module S = CicSubstitution
module PT = PrimitiveTactics
+module T = Tacticals
+module FNG = FreshNamesGenerator
-(*
-let module R = CicReduction
-*)
-
-let fail_msg0 = "not a declaration of the current context"
let fail_msg1 = "no applicable simplification"
let error msg = raise (PET.Fail msg)
-let rec declaration name = function
- | [] -> error fail_msg0
- | Some (hyp, Cic.Decl ty) :: _ when hyp = name -> ty
- | _ :: tail -> declaration name tail
-
(* lapply *******************************************************************)
-let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
- ?(substs = []) what =
- let rec strip_dependent_prods metasenv context ss = function
- | Cic.Prod (name, t1, t2) as t ->
- if TC.does_not_occur context 0 1 t2 then metasenv, ss, t else
- let metasenv, index = MI.mk_implicit metasenv [] context in
- let rs = MI.identity_relocation_list_for_metavariable context in
- let e, s = Some (name, Cic.Decl t1), Some (Cic.Meta (index, rs)) in
- strip_dependent_prods metasenv (e :: context) (s :: ss) t2
- | t -> metasenv, ss, t
+let strip_dependent_prods metasenv context t =
+ let irl = MI.identity_relocation_list_for_metavariable context in
+ let mk_meta metasenv t =
+ let index = MI.new_meta metasenv [] in
+ let metasenv = [index, context, t] @ metasenv in
+ metasenv, Cic.Meta (index, irl)
in
- let update_metasenv metasenv ((xuri, _, u,t), goal) =
- ((xuri, metasenv, u,t), goal)
+ let rec aux metasenv metas = function
+ | Cic.Prod (Cic.Name _ as name, t1, t2) ->
+ let metasenv, meta = mk_meta metasenv t1 in
+ aux metasenv (meta :: metas) (S.subst meta t2)
+ | Cic.Prod (Cic.Anonymous, t1, _) ->
+ let metasenv, meta = mk_meta metasenv t1 in
+ metasenv, metas, Some meta
+ | t -> metasenv, metas, None
in
- let lapply_tac status =
- let (proof, goal) = status in
- let _,metasenv,_,_ = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
+ aux metasenv [] t
+
+let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+ (* ?(substs = []) *) ?to_what what =
+ let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term 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 metasenv, substs, stripped_lemma = strip_dependent_prods metasenv context [] lemma in
- let status = update_metasenv metasenv status in
- let holed_lemma = S.subst_meta substs stripped_lemma in
- PET.apply_tactic (PT.cut_tac ~mk_fresh_name_callback holed_lemma) status
+ let lemma = FNG.clean_dummy_dependent_types lemma in
+ match strip_dependent_prods metasenv context lemma with
+ | metasenv, metas, Some meta ->
+ let pippo = Cic.Appl (what :: List.rev (meta :: metas)) in
+ Printf.eprintf "lapply: %s\n" (CicPp.ppterm pippo); flush stderr;
+ let outer_tac = letin_tac pippo in
+ let status = (xuri, metasenv, u, t), goal in
+ PET.apply_tactic outer_tac status
+ | metasenv, metas, None ->
+ failwith "lapply_tac: not implemented"
in
PET.mk_tactic lapply_tac
+
+(*
+
+
+
+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
+*)
(* fwd **********************************************************************)
-let fwd_simpl_tac ~hyp ~dbd =
+let fwd_simpl_tac ~what ~dbd =
let fwd_simpl_tac status =
let (proof, goal) = status in
- let _,metasenv,_,_ = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let major = declaration hyp context in
- match MetadataQuery.fwd_simpl ~dbd major with
+ let _, metasenv, _, _ = proof in
+ let _, context, ty = CicUtil.lookup_meta goal metasenv in
+ let major, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
+ match MetadataQuery.fwd_simpl ~dbd major with
| [] -> error fail_msg1
| uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, [])
in
projects / helm.git / blobdiff