Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
| _ -> 0
-let apply_tac_verbose_with_subst ~term (proof, goal) =
+let apply_with_subst ~term ~subst (proof, goal) =
(* Assumption: The term "term" must be closed in the current context *)
let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic in
let (_,metasenv,_,_) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let newmeta = new_meta_of_proof ~proof in
+ let newmeta = CicMkImplicit.new_meta metasenv subst in
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
match term with
C.Var (uri,exp_named_subst) ->
(* ALB *)
-let apply_tac_verbose_with_subst ~term status =
+let apply_with_subst ~term ?(subst=[]) status =
try
(* apply_tac_verbose ~term status *)
- apply_tac_verbose_with_subst ~term status
+ apply_with_subst ~term ~subst status
(* TODO cacciare anche altre eccezioni? *)
with
| CicUnification.UnificationFailure msg
(* ALB *)
let apply_tac_verbose ~term status =
- let subst, status = apply_tac_verbose_with_subst ~term status in
+ let subst, status = apply_with_subst ~term status in
(CicMetaSubst.apply_subst subst), status
let apply_tac ~term status = snd (apply_tac_verbose ~term status)
=
let module C = Cic in
let curi,metasenv,pbo,pty = proof in
+ (* occur check *)
+ let occur i t =
+ let m = CicUtil.metas_of_term t in
+ List.exists (fun (j,_) -> i=j) m
+ in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let _,_ = (* TASSI: FIXME *)
+ if occur metano term then
+ raise
+ (ProofEngineTypes.Fail (lazy
+ "You can't letin a term containing the current goal"));
+ let _,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let newmeta = new_meta_of_proof ~proof in
let fresh_name =
let (curi,metasenv,proofbo,proofty) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let termty = CicReduction.whd context termty in
let (termty,metasenv',arguments,fresh_meta) =
ProofEngineHelpers.saturate_term
(ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
[ReductionTactics.simpl_tac
~pattern:(ProofEngineTypes.conclusion_pattern None)])
;;
+
+(* FG: insetrts a "hole" in the context (derived from letin_tac) *)
+
+module C = Cic
+
+let letout_tac =
+ let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
+ let term = C.Sort C.Set in
+ let letout_tac (proof, goal) =
+ let curi, metasenv, pbo, pty = proof in
+ let metano, context, ty = CicUtil.lookup_meta goal metasenv in
+ let newmeta = new_meta_of_proof ~proof in
+ let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
+ let context_for_newmeta = None :: context in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in
+ let newmetaty = CicSubstitution.lift 1 ty in
+ let bo' = C.LetIn (fresh_name, term, C.Meta (newmeta,irl)) in
+ let newproof, _ = subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in
+ newproof, [newmeta]
+ in
+ mk_tactic letout_tac