From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- kernel/cooking.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/cooking.ml') diff --git a/kernel/cooking.ml b/kernel/cooking.ml index be71bd7b41..1302e71c95 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -173,7 +173,7 @@ let expmod_constr_subst cache modlist subst c = let cook_constr { Opaqueproof.modlist ; abstract } c = let cache = RefTable.create 13 in let expmod = expmod_constr_subst cache modlist (pi2 abstract) in - let hyps = Context.map_named_context expmod (pi1 abstract) in + let hyps = Context.Named.map expmod (pi1 abstract) in abstract_constant_body (expmod c) hyps let lift_univs cb subst = @@ -195,13 +195,13 @@ let cook_constant env { from = cb; info } = let abstract, usubst, abs_ctx = abstract in let usubst, univs = lift_univs cb usubst in let expmod = expmod_constr_subst cache modlist usubst in - let hyps = Context.map_named_context expmod abstract in + let hyps = Context.Named.map expmod abstract in let body = on_body modlist (hyps, usubst, abs_ctx) (fun c -> abstract_constant_body (expmod c) hyps) cb.const_body in let const_hyps = - Context.fold_named_context (fun (h,_,_) hyps -> + Context.Named.fold_outside (fun (h,_,_) hyps -> List.filter (fun (id,_,_) -> not (Id.equal id h)) hyps) hyps ~init:cb.const_hyps in let typ = match cb.const_type with -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/cooking.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/cooking.ml') diff --git a/kernel/cooking.ml b/kernel/cooking.ml index be71bd7b41..f0e9255824 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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/cooking.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'kernel/cooking.ml') diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 3ab6983d8a..d2106f8609 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -201,8 +201,11 @@ let cook_constant env { from = cb; info } = cb.const_body in let const_hyps = - Context.Named.fold_outside (fun (h,_,_) hyps -> - List.filter (fun (id,_,_) -> not (Id.equal id h)) hyps) + Context.Named.fold_outside (fun decl hyps -> + let open Context.Named.Declaration in + let h = get_id decl in + List.filter (fun decl -> let id = get_id decl in + not (Id.equal id h)) hyps) hyps ~init:cb.const_hyps in let typ = match cb.const_type with | RegularArity t -> -- 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/cooking.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'kernel/cooking.ml') diff --git a/kernel/cooking.ml b/kernel/cooking.ml index d2106f8609..86d786b09a 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -203,9 +203,8 @@ let cook_constant env { from = cb; info } = let const_hyps = Context.Named.fold_outside (fun decl hyps -> let open Context.Named.Declaration in - let h = get_id decl in - List.filter (fun decl -> let id = get_id decl in - not (Id.equal id h)) hyps) + List.filter (fun decl' -> not (Id.equal (get_id decl) (get_id decl'))) + hyps) hyps ~init:cb.const_hyps in let typ = match cb.const_type with | RegularArity t -> -- cgit v1.2.3 From 920f1548e9245ddfc8b923c5039a5e09dc0c87d4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 31 Jul 2015 18:53:21 +0200 Subject: Adding eq/compare/hash for syntactic view at constant/inductive/constructor kernel_name pairs rather than viewing them from only the user or canonical part. Hopefully more uniformity in Constr.hasheq (using systematically == on subterms). A semantic change: Cooking now indexing again on full pairs of kernel names rather than only on the canonical names, so as to preserve user name. Also, in pair of kernel names, ensuring the compact representation is used as soon as both names are the same. --- kernel/cooking.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'kernel/cooking.ml') diff --git a/kernel/cooking.ml b/kernel/cooking.ml index f0e9255824..9476e8a839 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -44,15 +44,15 @@ module RefHash = struct type t = my_global_reference let equal gr1 gr2 = match gr1, gr2 with - | ConstRef c1, ConstRef c2 -> Constant.CanOrd.equal c1 c2 - | IndRef i1, IndRef i2 -> eq_ind i1 i2 - | ConstructRef c1, ConstructRef c2 -> eq_constructor c1 c2 + | ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2 + | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2 + | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2 | _ -> false open Hashset.Combine let hash = function - | ConstRef c -> combinesmall 1 (Constant.hash c) - | IndRef i -> combinesmall 2 (ind_hash i) - | ConstructRef c -> combinesmall 3 (constructor_hash c) + | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c) + | IndRef i -> combinesmall 2 (ind_syntactic_hash i) + | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c) end module RefTable = Hashtbl.Make(RefHash) -- cgit v1.2.3