From 3116aeff0cdc51e6801f3e8ae4a6c0533e1a75ac Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 8 Oct 2015 18:06:55 +0200 Subject: Fix #4346 1/2: native casts were not inferring universe constraints. --- kernel/fast_typeops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/fast_typeops.ml') diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index d22abff10c..063c9cf126 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -227,7 +227,7 @@ let judge_of_cast env c ct k expected_type = default_conv ~l2r:true CUMUL env ct expected_type | NATIVEcast -> let sigma = Nativelambda.empty_evars in - native_conv CUMUL sigma env ct expected_type + Nativeconv.native_conv CUMUL sigma env ct expected_type with NotConvertible -> error_actual_type env (make_judge c ct) expected_type -- cgit v1.2.3 From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 7 Dec 2015 10:52:14 +0100 Subject: Fix some typos. --- kernel/fast_typeops.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/fast_typeops.ml') diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index 063c9cf126..b625478f25 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -33,7 +33,7 @@ let check_constraints cst env = if Environ.check_constraints cst env then () else error_unsatisfied_constraints env cst -(* This should be a type (a priori without intension to be an assumption) *) +(* This should be a type (a priori without intention to be an assumption) *) let type_judgment env c t = match kind_of_term(whd_betadeltaiota env t) with | Sort s -> {utj_val = c; utj_type = s } @@ -52,8 +52,8 @@ let assumption_of_judgment env t ty = error_assumption env (make_judge t ty) (************************************************) -(* Incremental typing rules: builds a typing judgement given the *) -(* judgements for the subterms. *) +(* Incremental typing rules: builds a typing judgment given the *) +(* judgments for the subterms. *) (*s Type of sorts *) -- cgit v1.2.3 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/fast_typeops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/fast_typeops.ml') diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index b625478f25..85c74534ef 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -90,7 +90,7 @@ let judge_of_variable env id = variables of the current env *) (* TODO: check order? *) let check_hyps_inclusion env f c sign = - Context.fold_named_context + Context.Named.fold_outside (fun (id,_,ty1) () -> try let ty2 = named_type id env in -- 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/fast_typeops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/fast_typeops.ml') diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index b625478f25..2a6a55adfe 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.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/fast_typeops.ml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) (limited to 'kernel/fast_typeops.ml') diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index ebc1853d93..df95c93dc5 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -73,8 +73,9 @@ let judge_of_type u = let judge_of_relative env n = try - let (_,_,typ) = lookup_rel n env in - lift n typ + let open Context.Rel.Declaration in + let typ = get_type (lookup_rel n env) in + lift n typ with Not_found -> error_unbound_rel env n @@ -91,7 +92,10 @@ let judge_of_variable env id = (* TODO: check order? *) let check_hyps_inclusion env f c sign = Context.Named.fold_outside - (fun (id,_,ty1) () -> + (fun decl () -> + let open Context.Named.Declaration in + let id = get_id decl in + let ty1 = get_type decl in try let ty2 = named_type id env in if not (eq_constr ty2 ty1) then raise Exit @@ -325,6 +329,7 @@ let type_fixpoint env lna lar vdef vdeft = Ind et Constructsi un jour cela devient des constructions arbitraires et non plus des variables *) let rec execute env cstr = + let open Context.Rel.Declaration in match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> @@ -368,13 +373,13 @@ let rec execute env cstr = | Lambda (name,c1,c2) -> let _ = execute_is_type env c1 in - let env1 = push_rel (name,None,c1) env in + let env1 = push_rel (LocalAssum (name,c1)) env in let c2t = execute env1 c2 in judge_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> let vars = execute_is_type env c1 in - let env1 = push_rel (name,None,c1) env in + let env1 = push_rel (LocalAssum (name,c1)) env in let vars' = execute_is_type env1 c2 in judge_of_product env name vars vars' @@ -382,7 +387,7 @@ let rec execute env cstr = let c1t = execute env c1 in let _c2s = execute_is_type env c2 in let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in - let env1 = push_rel (name,Some c1,c2) env in + let env1 = push_rel (LocalDef (name,c1,c2)) env in let c3t = execute env1 c3 in subst1 c1 c3t -- 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/fast_typeops.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'kernel/fast_typeops.ml') diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index df95c93dc5..7f4ba8ecbe 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -74,8 +74,7 @@ let judge_of_type u = let judge_of_relative env n = try let open Context.Rel.Declaration in - let typ = get_type (lookup_rel n env) in - lift n typ + env |> lookup_rel n |> get_type |> lift n with Not_found -> error_unbound_rel env n -- cgit v1.2.3