aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-06-25 16:24:30 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-06-25 21:30:09 +0200
commit9e1372f77218ca6f0baf4ed7c590c91ad84b6313 (patch)
treef75c23cb31a84f6010e15a7ec612640d6cac5e0d /tactics
parent7446e3e1555c0f41373b71b92a3f01f060e8e0e0 (diff)
Moving "assert" (internally "Cut") to the new proof engine.
It allows in particular to have "Info" on tactic "assert" and derivatives not to give an "<unknown>".
Diffstat (limited to 'tactics')
-rw-r--r--tactics/tactics.ml87
1 files changed, 68 insertions, 19 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 689cc48aa..061eca10b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -439,16 +439,66 @@ let find_name mayrepl decl naming gl = match naming with
(* 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 rec get_hyp_after h = function
+ | [] -> error_no_such_hypothesis h
+ | d :: right ->
+ if Id.equal (NamedDecl.get_id d) h then
+ match right with d' ::_ -> MoveBefore (NamedDecl.get_id d') | [] -> MoveFirst
+ else
+ get_hyp_after h right
+
+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_hyp_after 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 +513,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
@@ -3805,11 +3851,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
@@ -3852,16 +3899,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 =