X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FprimitiveTactics.ml;h=aeb0c0751286285b637a1cff94aae6854ee3cae4;hb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;hp=64db996667879cd10efb1adf0ad83b7032fd2a94;hpb=88536b5cc7f2fb3d53f5f33cf946989a7e1436be;p=helm.git diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 64db99666..aeb0c0751 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -52,9 +52,13 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name = match ty with C.Cast (te,_) -> collect_context context howmany do_whd te | C.Prod (n,s,t) -> - let n' = mk_fresh_name metasenv context n ~typ:s in + let n' = mk_fresh_name metasenv context n ~typ:s in let (context',ty,bo) = - let ctx = (Some (n',(C.Decl s)))::context in + let entry = match n' with + | C.Name _ -> Some (n',(C.Decl s)) + | C.Anonymous -> None + in + let ctx = entry :: context in collect_context ctx (howmany - 1) do_whd t in (context',ty,C.Lambda(n',s,bo)) @@ -257,7 +261,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) = let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in - let (_,metasenv,_,_, _) = proof in + let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = @@ -321,7 +325,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) = let subst_in = (* if we just apply the subtitution, the type is irrelevant: we may use Implicit, since it will be dropped *) - CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst) + ((metano,(context,bo',Cic.Implicit None))::subst) in let (newproof, newmetasenv''') = ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in @@ -365,13 +369,11 @@ let apply_tac ~term = PET.mk_tactic (apply_tac ~term) let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ()= - let intros_tac - ?(mk_fresh_name_callback = (FreshNamesGenerator.mk_fresh_name ~subst:[])) () - (proof, goal) + let intros_tac (proof, goal) = let module C = Cic in let module R = CicReduction in - let (_,metasenv,_,_, _) = proof in + let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in let (context',ty',bo') = @@ -383,7 +385,7 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_ in (newproof, [newmeta]) in - PET.mk_tactic (intros_tac ~mk_fresh_name_callback ()) + PET.mk_tactic intros_tac let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term = let cut_tac @@ -391,7 +393,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst: term (proof, goal) = let module C = Cic in - let curi,metasenv,pbo,pty, attrs = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in let newmeta2 = newmeta1 + 1 in @@ -426,7 +428,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: term (proof, goal) = let module C = Cic in - let curi,metasenv,pbo,pty, attrs = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in (* occur check *) let occur i t = let m = CicUtil.metas_of_term t in @@ -462,7 +464,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: let exact_tac ~term = let exact_tac ~term (proof, goal) = (* Assumption: the term bo must be closed in the current context *) - let (_,metasenv,_,_, _) = proof in + let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let module T = CicTypeChecker in let module R = CicReduction in @@ -495,7 +497,7 @@ module RT = ReductionTactics let beta_after_elim_tac upto predicate = let beta_after_elim_tac status = let proof, goal = status in - let _, metasenv, _, _, _ = proof in + let _, metasenv, _subst, _, _, _ = proof in let _, _, ty = CicUtil.lookup_meta goal metasenv in let mk_pattern ~equality ~upto ~predicate ty = (* code adapted from ProceduralConversion.generalize *) @@ -562,7 +564,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = | _ -> raise (PET.Fail (lazy "not implemented")) in let ugraph = CicUniv.empty_ugraph in - let curi, metasenv, proofbo, proofty, attrs = proof in + let curi, metasenv, _subst, proofbo, proofty, attrs = proof in let conjecture = CicUtil.lookup_meta goal metasenv in let metano, context, ty = conjecture in let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in @@ -684,13 +686,13 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv:metasenv'' in - let proof' = curi,metasenv'',proofbo,proofty, attrs in + let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in let proof'', new_goals' = PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal) in (* The apply_tactic can have closed some of the new_goals *) let patched_new_goals = - let (_,metasenv''',_,_, _) = proof'' in + let (_,metasenv''',_subst,_,_, _) = proof'' in List.filter (function i -> List.exists (function (j,_,_) -> j=i) metasenv''') new_goals @ new_goals' @@ -706,13 +708,13 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = PET.mk_tactic elim_tac ;; -let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term = +let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term = let cases_tac ~term (proof, goal) = let module TC = CicTypeChecker in let module U = UriManager in let module R = CicReduction in let module C = Cic in - let (curi,metasenv,proofbo,proofty, attrs) = proof in + let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in let termty = CicReduction.whd context termty in @@ -823,13 +825,13 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv:metasenv'' in - let proof' = curi,metasenv'',proofbo,proofty, attrs in + let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in let proof'', new_goals' = PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal) in (* The apply_tactic can have closed some of the new_goals *) let patched_new_goals = - let (_,metasenv''',_,_,_) = proof'' in + let (_,metasenv''',_subst,_,_,_) = proof'' in List.filter (function i -> List.exists (function (j,_,_) -> j=i) metasenv''') new_goals @ new_goals' @@ -864,7 +866,7 @@ 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, attrs = proof in + let curi, metasenv, _subst, pbo, pty, attrs = proof in let metano, context, ty = CicUtil.lookup_meta goal metasenv in let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in