aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_global.ml
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-01-29 10:13:12 +0100
committerGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-02-09 15:58:17 +0100
commit34ef02fac1110673ae74c41c185c228ff7876de2 (patch)
treea688eb9e2c23fc5353391f0c8b4ba1d7ba327844 /proofs/proof_global.ml
parente9675e068f9e0e92bab05c030fb4722b146123b8 (diff)
CLEANUP: Context.{Rel,Named}.Declaration.t
Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published.
Diffstat (limited to 'proofs/proof_global.ml')
-rw-r--r--proofs/proof_global.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index fc33e9a65..403a36141 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -267,18 +267,19 @@ let _ = Goptions.declare_bool_option
Goptions.optwrite = (fun b -> proof_using_auto_clear := b) }
let set_used_variables l =
+ let open Context.Named.Declaration in
let env = Global.env () in
let ids = List.fold_right Id.Set.add l Id.Set.empty in
let ctx = Environ.keep_hyps env ids in
let ctx_set =
- List.fold_right Id.Set.add (List.map pi1 ctx) Id.Set.empty in
+ List.fold_right Id.Set.add (List.map get_id ctx) Id.Set.empty in
let vars_of = Environ.global_vars_set in
let aux env entry (ctx, all_safe, to_clear as orig) =
match entry with
- | (x,None,_) ->
+ | LocalAssum (x,_) ->
if Id.Set.mem x all_safe then orig
else (ctx, all_safe, (Loc.ghost,x)::to_clear)
- | (x,Some bo, ty) as decl ->
+ | LocalDef (x,bo, ty) as decl ->
if Id.Set.mem x all_safe then orig else
let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
if Id.Set.subset vars all_safe