summaryrefslogtreecommitdiff
path: root/plugins/decl_mode/decl_proof_instr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/decl_mode/decl_proof_instr.ml')
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml99
1 files changed, 65 insertions, 34 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index ba9fb728..d30fcf60 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Pp
open Evd
@@ -29,9 +29,27 @@ open Termops
open Namegen
open Goptions
open Misctypes
+open Sigma.Notations
+open Context.Named.Declaration
(* Strictness option *)
+let clear ids { it = goal; sigma } =
+ let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
+ let env = Goal.V82.env sigma goal in
+ let sign = Goal.V82.hyps sigma goal in
+ let cl = Goal.V82.concl sigma goal in
+ let evdref = ref (Evd.clear_metas sigma) in
+ let (hyps, concl) =
+ try Evarutil.clear_hyps_in_evi env evdref sign cl ids
+ with Evarutil.ClearDependencyError (id, _) ->
+ errorlabstrm "" (str "Cannot clear " ++ pr_id id)
+ in
+ let sigma = !evdref in
+ let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
+ let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
+ { it = [gl]; sigma }
+
let get_its_info gls = get_info gls.sigma gls.it
let get_strictness,set_strictness =
@@ -42,7 +60,7 @@ let _ =
declare_bool_option
{ optsync = true;
optdepr = false;
- optname = "strict mode";
+ optname = "strict proofs";
optkey = ["Strict";"Proofs"];
optread = get_strictness;
optwrite = set_strictness }
@@ -66,12 +84,12 @@ let tcl_erase_info gls =
tcl_change_info_gen info_gen gls
let special_whd gl=
- let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in
- (fun t -> Closure.whd_val infos (Closure.inject t))
+ let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
+ (fun t -> CClosure.whd_val infos (CClosure.inject t))
let special_nf gl=
- let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in
- (fun t -> Closure.norm_val infos (Closure.inject t))
+ let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
+ (fun t -> CClosure.norm_val infos (CClosure.inject t))
let is_good_inductive env ind =
let mib,oib = Inductive.lookup_mind_specif env ind in
@@ -86,7 +104,7 @@ Please \"suppose\" something or \"end\" it now."
| _ -> ()
let mk_evd metalist gls =
- let evd0= create_goal_evar_defs (sig_sig gls) in
+ let evd0= clear_metas (sig_sig gls) in
let add_one (meta,typ) evd =
meta_declare meta typ evd in
List.fold_right add_one metalist evd0
@@ -151,7 +169,7 @@ let do_daimon () =
daimon_instr env p
end
in
- if not status then Pp.feedback Feedback.AddedAxiom else ()
+ if not status then Feedback.feedback Feedback.AddedAxiom else ()
(* post-instruction focus management *)
@@ -228,7 +246,8 @@ let close_previous_case pts =
(* automation *)
let filter_hyps f gls =
- let filter_aux (id,_,_) =
+ let filter_aux id =
+ let id = get_id id in
if f id then
tclIDTAC
else
@@ -258,12 +277,16 @@ let prepare_goal items gls =
filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls
let my_automation_tac = ref
- (Proofview.tclZERO (Errors.make_anomaly (Pp.str"No automation registered")))
+ (Proofview.tclZERO (CErrors.make_anomaly (Pp.str"No automation registered")))
let register_automation_tac tac = my_automation_tac:= tac
let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac)
+let warn_insufficient_justification =
+ CWarnings.create ~name:"declmode-insufficient-justification" ~category:"declmode"
+ (fun () -> strbrk "Insufficient justification.")
+
let justification tac gls=
tclORELSE
(tclSOLVE [tclTHEN tac (Proofview.V82.of_tactic assumption)])
@@ -272,7 +295,7 @@ let justification tac gls=
error "Insufficient justification."
else
begin
- msg_warning (str "Insufficient justification.");
+ warn_insufficient_justification ();
daimon_tac gls
end) gls
@@ -330,11 +353,12 @@ let enstack_subsubgoals env se stack gls=
let rc,_ = Reduction.dest_prod env apptype in
let rec meta_aux last lenv = function
[] -> (last,lenv,[])
- | (nam,_,typ)::q ->
+ | decl::q ->
let nlast=succ last in
let (llast,holes,metas) =
meta_aux nlast (mkMeta nlast :: lenv) q in
- (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in
+ let open Context.Rel.Declaration in
+ (llast,holes,(nlast,special_nf gls (substl lenv (get_type decl)))::metas) in
let (nlast,holes,nmetas) =
meta_aux se.se_last_meta [] (List.rev rc) in
let refiner = applist (appterm,List.rev holes) in
@@ -391,7 +415,7 @@ let find_subsubgoal c ctyp skip submetas gls =
se.se_meta submetas se.se_meta_list}
else
dfs (pred n)
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
begin
enstack_subsubgoals env se stack gls;
dfs n
@@ -403,15 +427,15 @@ let concl_refiner metas body gls =
let concl = pf_concl gls in
let evd = sig_sig gls in
let env = pf_env gls in
- let sort = family_of_sort (Typing.sort_of env (ref evd) concl) in
+ let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in
let rec aux env avoid subst = function
[] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
| (n,typ)::rest ->
let _A = subst_meta subst typ in
let x = id_of_name_using_hdchar env _A Anonymous in
let _x = fresh_id avoid x gls in
- let nenv = Environ.push_named (_x,None,_A) env in
- let asort = family_of_sort (Typing.sort_of nenv (ref evd) _A) in
+ let nenv = Environ.push_named (LocalAssum (_x,_A)) env in
+ let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) _A) in
let nsubst = (n,mkVar _x)::subst in
if List.is_empty rest then
asort,_A,mkNamedLambda _x _A (subst_meta nsubst body)
@@ -465,7 +489,7 @@ let thus_tac c ctyp submetas gls =
Proofview.V82.of_tactic (exact_check proof) gls
else
let refiner = concl_refiner list proof gls in
- Tactics.refine refiner gls
+ Tacmach.refine refiner gls
(* general forward step *)
@@ -492,7 +516,7 @@ let just_tac _then cut info gls0 =
None ->
Proofview.V82.of_tactic automation_tac gls
| Some tac ->
- Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in
+ Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in
justification (tclTHEN items_tac method_tac) gls0
let instr_cut mkstat _thus _then cut gls0 =
@@ -542,7 +566,7 @@ let instr_rew _thus rew_side cut gls0 =
None ->
Proofview.V82.of_tactic automation_tac gls
| Some tac ->
- Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in
+ Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in
let just_tac gls =
justification (tclTHEN items_tac method_tac) gls in
let (c_id,_) = match cut.cut_stat.st_label with
@@ -605,7 +629,7 @@ let assume_tac hyps gls =
tclTHEN
(push_intro_tac
(fun id ->
- Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label))
+ Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label))
hyps tclIDTAC gls
let assume_hyps_or_theses hyps gls =
@@ -615,7 +639,7 @@ let assume_hyps_or_theses hyps gls =
tclTHEN
(push_intro_tac
(fun id ->
- Proofview.V82.of_tactic (convert_hyp (id,None,c))) nam)
+ Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,c)))) nam)
| Hprop {st_label=nam;st_it=Thesis (tk)} ->
tclTHEN
(push_intro_tac
@@ -627,7 +651,7 @@ let assume_st hyps gls =
(fun st ->
tclTHEN
(push_intro_tac
- (fun id -> Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label))
+ (fun id -> Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label))
hyps tclIDTAC gls
let assume_st_letin hyps gls =
@@ -636,7 +660,7 @@ let assume_st_letin hyps gls =
tclTHEN
(push_intro_tac
(fun id ->
- Proofview.V82.of_tactic (convert_hyp (id,Some (fst st.st_it),snd st.st_it))) st.st_label))
+ Proofview.V82.of_tactic (convert_hyp (LocalDef (id, fst st.st_it, snd st.st_it)))) st.st_label))
hyps tclIDTAC gls
(* suffices *)
@@ -730,7 +754,7 @@ let rec consider_match may_intro introduced available expected gls =
error "Not enough sub-hypotheses to match statements."
(* should tell which ones *)
| id::rest_ids,(Hvar st | Hprop st)::rest ->
- tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it)))
+ tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it))))
begin
match st.st_label with
Anonymous ->
@@ -798,8 +822,8 @@ let define_tac id args body gls =
let cast_tac id_or_thesis typ gls =
match id_or_thesis with
This id ->
- let (_,body,_) = pf_get_hyp gls id in
- Proofview.V82.of_tactic (convert_hyp (id,body,typ)) gls
+ let body = pf_get_hyp gls id |> get_value in
+ Proofview.V82.of_tactic (convert_hyp (of_tuple (id,body,typ))) gls
| Thesis (For _ ) ->
error "\"thesis for ...\" is not applicable here."
| Thesis Plain ->
@@ -1199,6 +1223,9 @@ let hrec_for fix_id per_info gls obj_id =
let hd2 = applist (mkVar fix_id,args@[obj]) in
compose_lam rc (Reductionops.whd_beta gls.sigma hd2)
+let warn_missing_case =
+ CWarnings.create ~name:"declmode-missing-case" ~category:"declmode"
+ (fun () -> strbrk "missing case")
let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
match tree, objs with
@@ -1269,12 +1296,12 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
(fun id ->
hrec_for (out_name fix_name) per_info gls1 id)
recs in
- generalize hrecs gls1
+ Proofview.V82.of_tactic (generalize hrecs) gls1
end;
match bro with
None ->
- msg_warning (str "missing case");
- tacnext (mkMeta 1)
+ warn_missing_case ();
+ tacnext (mkMeta 1)
| Some (sub_ids,tree) ->
let br_args =
List.filter
@@ -1305,7 +1332,11 @@ let understand_my_constr env sigma c concl =
Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc)
let my_refine c gls =
- let oc sigma = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
+ let oc = { run = begin fun sigma ->
+ let sigma = Sigma.to_evar_map sigma in
+ let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
+ Sigma.Unsafe.of_pair (c, sigma)
+ end } in
Proofview.V82.of_tactic (Tactics.New.refine oc) gls
(* end focus/claim *)
@@ -1341,7 +1372,7 @@ let end_tac et2 gls =
(default_justification (List.map mkVar clauses))
| ET_Induction,EK_nodep ->
tclTHENLIST
- [generalize (pi.per_args@[pi.per_casee]);
+ [Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee]));
Proofview.V82.of_tactic (simple_induct (AnonHyp (succ (List.length pi.per_args))));
default_justification (List.map mkVar clauses)]
| ET_Case_analysis,EK_dep tree ->
@@ -1353,7 +1384,7 @@ let end_tac et2 gls =
(initial_instance_stack clauses) [pi.per_casee] 0 tree
| ET_Induction,EK_dep tree ->
let nargs = (List.length pi.per_args) in
- tclTHEN (generalize (pi.per_args@[pi.per_casee]))
+ tclTHEN (Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee])))
begin
fun gls0 ->
let fix_id =
@@ -1361,7 +1392,7 @@ let end_tac et2 gls =
let c_id =
pf_get_new_id (Id.of_string "_main_arg") gls0 in
tclTHENLIST
- [fix (Some fix_id) (succ nargs);
+ [Proofview.V82.of_tactic (fix (Some fix_id) (succ nargs));
tclDO nargs (Proofview.V82.of_tactic introf);
Proofview.V82.of_tactic (intro_mustbe_force c_id);
execute_cases (Name fix_id) pi
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 21:10:25 +0000