From 34ef02fac1110673ae74c41c185c228ff7876de2 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 29 Jan 2016 10:13:12 +0100 Subject: 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. --- kernel/closure.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'kernel/closure.ml') diff --git a/kernel/closure.ml b/kernel/closure.ml index 9bc67b5adb..dc98cc65d0 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -247,8 +247,8 @@ let info_env info = info.i_cache.i_env let rec assoc_defined id = function | [] -> raise Not_found -| (_, None, _) :: ctxt -> assoc_defined id ctxt -| (id', Some c, _) :: ctxt -> +| Context.Named.Declaration.LocalAssum _ :: ctxt -> assoc_defined id ctxt +| Context.Named.Declaration.LocalDef (id', c, _) :: ctxt -> if Id.equal id id' then c else assoc_defined id ctxt let ref_value_cache ({i_cache = cache} as infos) ref = @@ -285,9 +285,9 @@ let defined_rels flags env = let ctx = rel_context env in let len = List.length ctx in let ans = Array.make len None in - let iter i (_, b, _) = match b with - | None -> () - | Some _ -> Array.unsafe_set ans i b + let iter i = function + | Context.Rel.Declaration.LocalAssum _ -> () + | Context.Rel.Declaration.LocalDef (_,b,_) -> Array.unsafe_set ans i (Some b) in let () = List.iteri iter ctx in ans -- cgit v1.2.3 From 4f041384cb27f0d24fa14b272884b4b7f69cacbe Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 15 Feb 2016 11:55:43 +0100 Subject: CLEANUP: Simplifying the changes done in "kernel/*" ... ... ... ... ... ... ... ... ... ... ... ... ... ... --- kernel/closure.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'kernel/closure.ml') diff --git a/kernel/closure.ml b/kernel/closure.ml index dc98cc65d0..4476fe5241 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -245,10 +245,12 @@ and 'a infos = { let info_flags info = info.i_flags let info_env info = info.i_cache.i_env +open Context.Named.Declaration + let rec assoc_defined id = function | [] -> raise Not_found -| Context.Named.Declaration.LocalAssum _ :: ctxt -> assoc_defined id ctxt -| Context.Named.Declaration.LocalDef (id', c, _) :: ctxt -> +| LocalAssum _ :: ctxt -> assoc_defined id ctxt +| LocalDef (id', c, _) :: ctxt -> if Id.equal id id' then c else assoc_defined id ctxt let ref_value_cache ({i_cache = cache} as infos) ref = @@ -285,9 +287,10 @@ let defined_rels flags env = let ctx = rel_context env in let len = List.length ctx in let ans = Array.make len None in + let open Context.Rel.Declaration in let iter i = function - | Context.Rel.Declaration.LocalAssum _ -> () - | Context.Rel.Declaration.LocalDef (_,b,_) -> Array.unsafe_set ans i (Some b) + | LocalAssum _ -> () + | LocalDef (_,b,_) -> Array.unsafe_set ans i (Some b) in let () = List.iteri iter ctx in ans -- cgit v1.2.3