diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 14:37:55 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 14:37:55 +0200 |
commit | 751246d893470b95d3d96ef87fe6dc86950d8d63 (patch) | |
tree | a4512b9db59c10ed761d124f63f18a30ce1f51aa /tactics/tactics.ml | |
parent | 7e29b535397c98a46999ecdd827fa5f4cebc8798 (diff) | |
parent | 4f392bc8114309f388791c1ddc7cc95cc021aa5e (diff) |
Merge PR #830: Moving assert (the "Cut" rule) to new proof engine
Diffstat (limited to 'tactics/tactics.ml')
-rw-r--r-- | tactics/tactics.ml | 135 |
1 files changed, 92 insertions, 43 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 062040df6..67bc55d3f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -436,19 +436,85 @@ let find_name mayrepl decl naming gl = match naming with id (**************************************************************) +(* Computing position of hypotheses for replacing *) +(**************************************************************) + +let get_next_hyp_position id = + let rec aux = function + | [] -> error_no_such_hypothesis id + | decl :: right -> + if Id.equal (NamedDecl.get_id decl) id then + match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveFirst + else + aux right + in + aux + +let get_previous_hyp_position id = + let rec aux dest = function + | [] -> error_no_such_hypothesis id + | decl :: right -> + let hyp = NamedDecl.get_id decl in + if Id.equal hyp id then dest else aux (MoveAfter hyp) right + in + aux MoveLast + +(**************************************************************) (* Cut rule *) (**************************************************************) +let clear_hyps2 env sigma ids sign t cl = + try + let evdref = ref (Evd.clear_metas sigma) in + let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in + (hyps, t, cl, !evdref) + with Evarutil.ClearDependencyError (id,err) -> + error_replacing_dependency env sigma id err + +let internal_cut_gen ?(check=true) dir replace id t = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let concl = Proofview.Goal.concl gl in + let store = Proofview.Goal.extra gl in + let sign = named_context_val env in + let sign',t,concl,sigma = + if replace then + let nexthyp = get_next_hyp_position id (named_context_of_val sign) in + let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in + let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in + sign',t,concl,sigma + else + (if check && mem_named_context_val id sign then + user_err (str "Variable " ++ pr_id id ++ str " is already declared."); + push_named_context_val (LocalAssum (id,t)) sign,t,concl,sigma) in + let nf_t = nf_betaiota sigma t in + Proofview.tclTHEN + (Proofview.Unsafe.tclEVARS sigma) + (Refine.refine ~typecheck:false begin fun sigma -> + let (sigma,ev,ev') = + if dir then + let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in + let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in + (sigma,ev,ev') + else + let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in + let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in + (sigma,ev,ev') in + let term = mkLetIn (Name id, ev, t, EConstr.Vars.subst_var id ev') in + (sigma, term) + end) + end + +let internal_cut ?(check=true) = internal_cut_gen ~check true +let internal_cut_rev ?(check=true) = internal_cut_gen ~check false + let assert_before_then_gen b naming t tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> let id = find_name b (LocalAssum (Anonymous,t)) naming gl in Tacticals.New.tclTHENLAST - (Proofview.V82.tactic - (fun gl -> - try Tacmach.internal_cut b id t gl - with Evarutil.ClearDependencyError (id,err) -> - error_replacing_dependency (pf_env gl) (project gl) id err)) + (internal_cut b id t) (tac id) end @@ -463,11 +529,7 @@ let assert_after_then_gen b naming t tac = Proofview.Goal.enter begin fun gl -> let id = find_name b (LocalAssum (Anonymous,t)) naming gl in Tacticals.New.tclTHENFIRST - (Proofview.V82.tactic - (fun gl -> - try Tacmach.internal_cut_rev b id t gl - with Evarutil.ClearDependencyError (id,err) -> - error_replacing_dependency (pf_env gl) (project gl) id err)) + (internal_cut_rev b id t) (tac id) end @@ -999,29 +1061,10 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = in aux n [] -let get_next_hyp_position id gl = - let rec aux = function - | [] -> raise (RefinerError (NoSuchHyp id)) - | decl :: right -> - if Id.equal (NamedDecl.get_id decl) id then - match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveLast - else - aux right - in - aux (Proofview.Goal.hyps (Proofview.Goal.assume gl)) - -let get_previous_hyp_position id gl = - let rec aux dest = function - | [] -> raise (RefinerError (NoSuchHyp id)) - | decl :: right -> - let hyp = NamedDecl.get_id decl in - if Id.equal hyp id then dest else aux (MoveAfter hyp) right - in - aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) - let intro_replacing id = Proofview.Goal.enter begin fun gl -> - let next_hyp = get_next_hyp_position id gl in + let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let next_hyp = get_next_hyp_position id hyps in Tacticals.New.tclTHENLIST [ clear_for_replacing [id]; introduction id; @@ -1040,7 +1083,8 @@ let intro_replacing id = let intros_possibly_replacing ids = let suboptimal = true in Proofview.Goal.enter begin fun gl -> - let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in + let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in Tacticals.New.tclTHEN (Tacticals.New.tclMAP (fun id -> Tacticals.New.tclTRY (clear_for_replacing [id])) @@ -1053,7 +1097,8 @@ let intros_possibly_replacing ids = (* This version assumes that replacement is actually possible *) let intros_replacing ids = Proofview.Goal.enter begin fun gl -> - let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in + let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let posl = List.map (fun id -> (id, get_next_hyp_position id hyps)) ids in Tacticals.New.tclTHEN (clear_for_replacing ids) (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl) @@ -2578,7 +2623,8 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars Proofview.Goal.enter begin fun gl -> let destopt = if with_evars then MoveLast (* evars would depend on the whole context *) - else get_previous_hyp_position id gl in + else + get_previous_hyp_position id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) in let naming,ipat_tac = prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in let lemmas_target, last_lemma_target = @@ -3809,11 +3855,12 @@ let compare_upto_variables sigma x y = in compare x y -let specialize_eqs id gl = +let specialize_eqs id = let open Context.Rel.Declaration in - let env = Tacmach.pf_env gl in - let ty = Tacmach.pf_get_hyp_typ gl id in - let evars = ref (project gl) in + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let ty = Tacmach.New.pf_get_hyp_typ id gl in + let evars = ref (Proofview.Goal.sigma gl) in let unif env evars c1 c2 = compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2 in @@ -3856,16 +3903,18 @@ let specialize_eqs id gl = and acc' = Tacred.whd_simpl env !evars acc' in let ty' = Evarutil.nf_evar !evars ty' in if worked then - tclTHENFIRST (Tacmach.internal_cut true id ty') - (Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl - else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl - + Tacticals.New.tclTHENFIRST + (internal_cut true id ty') + (exact_no_check ((* refresh_universes_strict *) acc')) + else + Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) + end let specialize_eqs id = Proofview.Goal.enter begin fun gl -> let msg = str "Specialization not allowed on dependent hypotheses" in Proofview.tclOR (clear [id]) (fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () -> - Proofview.V82.tactic (specialize_eqs id) + specialize_eqs id end let occur_rel sigma n c = |