diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof.ml | 28 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 1 | ||||
| -rw-r--r-- | proofs/proofview.ml | 117 | ||||
| -rw-r--r-- | proofs/proofview.mli | 41 | ||||
| -rw-r--r-- | proofs/refine.ml | 122 | ||||
| -rw-r--r-- | proofs/refine.mli | 37 |
6 files changed, 184 insertions, 162 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index b604fde4e..86af420dc 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -334,22 +334,24 @@ let compact p = (*** Tactics ***) let run_tactic env tac pr = + let open Proofview.Notations in let sp = pr.proofview in - let (_,tacticced_proofview,(status,to_shelve,give_up),info_trace) = - Proofview.apply env tac sp + let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in + let tac = + tac >>= fun () -> + Proofview.tclEVARMAP >>= fun sigma -> + (* Already solved goals are not to be counted as shelved. Nor are + they to be marked as unresolvable. *) + let retrieved = undef sigma (List.rev (Evd.future_goals sigma)) in + let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in + Proofview.Unsafe.tclEVARS sigma >>= fun () -> + Proofview.tclUNIT retrieved in - let sigma = Proofview.return tacticced_proofview in - (* Already solved goals are not to be counted as shelved. Nor are - they to be marked as unresolvable. *) - let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in - let retrieved = undef (List.rev (Evd.future_goals sigma)) in - let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in - let proofview = - List.fold_left - Proofview.Unsafe.mark_as_goal - tacticced_proofview - retrieved + let (retrieved,proofview,(status,to_shelve,give_up),info_trace) = + Proofview.apply env tac sp in + let sigma = Proofview.return proofview in + let shelf = (undef sigma pr.shelf)@retrieved@(undef sigma to_shelve) in let given_up = pr.given_up@give_up in let proofview = Proofview.Unsafe.reset_future_goals proofview in { pr with proofview ; shelf ; given_up },(status,info_trace) diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 08556d62e..236d47932 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -5,6 +5,7 @@ Proof_using Proof_errors Logic Proofview +Refine Proof Proof_global Redexpr diff --git a/proofs/proofview.ml b/proofs/proofview.ml index f42a60d9d..20be02e76 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -901,7 +901,7 @@ module Unsafe = struct let reset_future_goals p = { p with solution = Evd.reset_future_goals p.solution } - let mark_as_goal_evm evd content = + let mark_as_goal evd content = let info = Evd.find evd content in let info = { info with Evd.evar_source = match info.Evd.evar_source with @@ -911,8 +911,7 @@ module Unsafe = struct let info = Typeclasses.mark_unresolvable info in Evd.add evd content info - let mark_as_goal p gl = - { p with solution = mark_as_goal_evm p.solution gl } + let advance = advance end @@ -1075,118 +1074,6 @@ end -(** {6 The refine tactic} *) - -module Refine = -struct - - let extract_prefix env info = - let ctx1 = List.rev (Environ.named_context env) in - let ctx2 = List.rev (Evd.evar_context info) in - let rec share l1 l2 accu = match l1, l2 with - | d1 :: l1, d2 :: l2 -> - if d1 == d2 then share l1 l2 (d1 :: accu) - else (accu, d2 :: l2) - | _ -> (accu, l2) - in - share ctx1 ctx2 [] - - let typecheck_evar ev env sigma = - let info = Evd.find sigma ev in - (** Typecheck the hypotheses. *) - let type_hyp (sigma, env) decl = - let t = get_type decl in - let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref t in - let () = match decl with - | LocalAssum _ -> () - | LocalDef (_,body,_) -> Typing.e_check env evdref body t - in - (!evdref, Environ.push_named decl env) - in - let (common, changed) = extract_prefix env info in - let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in - let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in - (** Typecheck the conclusion *) - let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in - !evdref - - let typecheck_proof c concl env sigma = - let evdref = ref sigma in - let () = Typing.e_check env evdref c concl in - !evdref - - let (pr_constrv,pr_constr) = - Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") () - - let refine ?(unsafe = true) f = Goal.enter { Goal.enter = begin fun gl -> - let sigma = Goal.sigma gl in - let sigma = Sigma.to_evar_map sigma in - let env = Goal.env gl in - let concl = Goal.concl gl in - (** Save the [future_goals] state to restore them after the - refinement. *) - let prev_future_goals = Evd.future_goals sigma in - let prev_principal_goal = Evd.principal_future_goal sigma in - (** Create the refinement term *) - let (c, sigma) = Sigma.run (Evd.reset_future_goals sigma) f in - let evs = Evd.future_goals sigma in - let evkmain = Evd.principal_future_goal sigma in - (** Check that the introduced evars are well-typed *) - let fold accu ev = typecheck_evar ev env accu in - let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in - (** Check that the refined term is typesafe *) - let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in - (** Check that the goal itself does not appear in the refined term *) - let _ = - if not (Evarutil.occur_evar_upto sigma gl.Goal.self c) then () - else Pretype_errors.error_occur_check env sigma gl.Goal.self c - in - (** Proceed to the refinement *) - let sigma = match evkmain with - | None -> Evd.define gl.Goal.self c sigma - | Some evk -> - let id = Evd.evar_ident gl.Goal.self sigma in - let sigma = Evd.define gl.Goal.self c sigma in - match id with - | None -> sigma - | Some id -> Evd.rename evk id sigma - in - (** Restore the [future goals] state. *) - let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in - (** Select the goals *) - let comb = undefined sigma (CList.rev evs) in - let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in - let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> - Pv.modify (fun ps -> { ps with solution = sigma; comb; }) - end } - - (** Useful definitions *) - - let with_type env evd c t = - let my_type = Retyping.get_type_of env evd c in - let j = Environ.make_judge c my_type in - let (evd,j') = - Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t - in - evd , j'.Environ.uj_val - - let refine_casted ?unsafe f = Goal.enter { Goal.enter = begin fun gl -> - let concl = Goal.concl gl in - let env = Goal.env gl in - let f = { run = fun h -> - let Sigma (c, h, p) = f.run h in - let sigma, c = with_type env (Sigma.to_evar_map h) c concl in - Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) - } in - refine ?unsafe f - end } -end - - - (** {6 Trace} *) module Trace = struct diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 20f67f258..6bc2e9a0e 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -406,7 +406,13 @@ module Unsafe : sig (** Give an evar the status of a goal (changes its source location and makes it unresolvable for type classes. *) - val mark_as_goal : proofview -> Evar.t -> proofview + val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map + + (** [advance sigma g] returns [Some g'] if [g'] is undefined and is + the current avatar of [g] (for instance [g] was changed by [clear] + into [g']). It returns [None] if [g] has been (partially) + solved. *) + val advance : Evd.evar_map -> Evar.t -> Evar.t option end (** This module gives access to the innards of the monad. Its use is @@ -491,39 +497,6 @@ module Goal : sig end -(** {6 The refine tactic} *) - -module Refine : sig - - (** Printer used to print the constr which refine refines. *) - val pr_constr : - (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t - - (** {7 Refinement primitives} *) - - val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic - (** In [refine ?unsafe t], [t] is a term with holes under some - [evar_map] context. The term [t] is used as a partial solution - for the current goal (refine is a goal-dependent tactic), the - new holes created by [t] become the new subgoals. Exceptions - raised during the interpretation of [t] are caught and result in - tactic failures. If [unsafe] is [false] (default is [true]) [t] is - type-checked beforehand. *) - - (** {7 Helper functions} *) - - val with_type : Environ.env -> Evd.evar_map -> - Term.constr -> Term.types -> Evd.evar_map * Term.constr - (** [with_type env sigma c t] ensures that [c] is of type [t] - inserting a coercion if needed. *) - - val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic - (** Like {!refine} except the refined term is coerced to the conclusion of the - current goal. *) - -end - - (** {6 Trace} *) module Trace : sig diff --git a/proofs/refine.ml b/proofs/refine.ml new file mode 100644 index 000000000..db0b26f7e --- /dev/null +++ b/proofs/refine.ml @@ -0,0 +1,122 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Util +open Proofview_monad +open Sigma.Notations +open Proofview.Notations +open Context.Named.Declaration + +let extract_prefix env info = + let ctx1 = List.rev (Environ.named_context env) in + let ctx2 = List.rev (Evd.evar_context info) in + let rec share l1 l2 accu = match l1, l2 with + | d1 :: l1, d2 :: l2 -> + if d1 == d2 then share l1 l2 (d1 :: accu) + else (accu, d2 :: l2) + | _ -> (accu, l2) + in + share ctx1 ctx2 [] + +let typecheck_evar ev env sigma = + let info = Evd.find sigma ev in + (** Typecheck the hypotheses. *) + let type_hyp (sigma, env) decl = + let t = get_type decl in + let evdref = ref sigma in + let _ = Typing.e_sort_of env evdref t in + let () = match decl with + | LocalAssum _ -> () + | LocalDef (_,body,_) -> Typing.e_check env evdref body t + in + (!evdref, Environ.push_named decl env) + in + let (common, changed) = extract_prefix env info in + let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in + let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in + (** Typecheck the conclusion *) + let evdref = ref sigma in + let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in + !evdref + +let typecheck_proof c concl env sigma = + let evdref = ref sigma in + let () = Typing.e_check env evdref c concl in + !evdref + +let (pr_constrv,pr_constr) = + Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") () + +let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl -> + let gl = Proofview.Goal.assume gl in + let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + (** Save the [future_goals] state to restore them after the + refinement. *) + let prev_future_goals = Evd.future_goals sigma in + let prev_principal_goal = Evd.principal_future_goal sigma in + (** Create the refinement term *) + let (c, sigma) = Sigma.run (Evd.reset_future_goals sigma) f in + let evs = Evd.future_goals sigma in + let evkmain = Evd.principal_future_goal sigma in + (** Check that the introduced evars are well-typed *) + let fold accu ev = typecheck_evar ev env accu in + let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in + (** Check that the refined term is typesafe *) + let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in + (** Check that the goal itself does not appear in the refined term *) + let self = Proofview.Goal.goal gl in + let _ = + if not (Evarutil.occur_evar_upto sigma self c) then () + else Pretype_errors.error_occur_check env sigma self c + in + (** Proceed to the refinement *) + let sigma = match evkmain with + | None -> Evd.define self c sigma + | Some evk -> + let id = Evd.evar_ident self sigma in + let sigma = Evd.define self c sigma in + match id with + | None -> sigma + | Some id -> Evd.rename evk id sigma + in + (** Restore the [future goals] state. *) + let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in + (** Select the goals *) + let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in + let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in + let trace () = Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)) in + Proofview.Trace.name_tactic trace (Proofview.tclUNIT ()) >>= fun () -> + Proofview.Unsafe.tclEVARS sigma >>= fun () -> + Proofview.Unsafe.tclSETGOALS comb +end } + +(** Useful definitions *) + +let with_type env evd c t = + let my_type = Retyping.get_type_of env evd c in + let j = Environ.make_judge c my_type in + let (evd,j') = + Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t + in + evd , j'.Environ.uj_val + +let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> + let gl = Proofview.Goal.assume gl in + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let f = { run = fun h -> + let Sigma (c, h, p) = f.run h in + let sigma, c = with_type env (Sigma.to_evar_map h) c concl in + Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) + } in + refine ?unsafe f +end } diff --git a/proofs/refine.mli b/proofs/refine.mli new file mode 100644 index 000000000..17c7e28ca --- /dev/null +++ b/proofs/refine.mli @@ -0,0 +1,37 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Proofview + +(** {6 The refine tactic} *) + +(** Printer used to print the constr which refine refines. *) +val pr_constr : + (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t + +(** {7 Refinement primitives} *) + +val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic +(** In [refine ?unsafe t], [t] is a term with holes under some + [evar_map] context. The term [t] is used as a partial solution + for the current goal (refine is a goal-dependent tactic), the + new holes created by [t] become the new subgoals. Exceptions + raised during the interpretation of [t] are caught and result in + tactic failures. If [unsafe] is [false] (default is [true]) [t] is + type-checked beforehand. *) + +(** {7 Helper functions} *) + +val with_type : Environ.env -> Evd.evar_map -> + Term.constr -> Term.types -> Evd.evar_map * Term.constr +(** [with_type env sigma c t] ensures that [c] is of type [t] + inserting a coercion if needed. *) + +val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic +(** Like {!refine} except the refined term is coerced to the conclusion of the + current goal. *) |