From 50183ce7200d6059b4146c0cc4933aa524178c02 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 12 Oct 2015 15:39:20 +0200 Subject: Univs: be more restrictive for template polymorphic constants: only direct aliases are ok, and indices should not be made polymorphic. Fixes NFix. --- kernel/typeops.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index fe82d85d5d..8895bae5da 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -134,10 +134,16 @@ let extract_context_levels env l = let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = let params, ccl = dest_prod_assum env t in match kind_of_term ccl with - | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) -> - let param_ccls = extract_context_levels env params in - let s = { template_param_levels = param_ccls; template_level = u} in - TemplateArity (params,s) + | Sort (Type u) -> + let ind, l = decompose_app (whd_betadeltaiota env c) in + if isInd ind && List.is_empty l then + let mis = lookup_mind_specif env (fst (destInd ind)) in + let nparams = Inductive.inductive_params mis in + let paramsl = CList.lastn nparams params in + let param_ccls = extract_context_levels env paramsl in + let s = { template_param_levels = param_ccls; template_level = u} in + TemplateArity (params,s) + else RegularArity t | _ -> RegularArity t -- cgit v1.2.3 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/typeops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 8895bae5da..70f6fd803c 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -310,7 +310,7 @@ let judge_of_cast env cj k tj = | NATIVEcast -> let sigma = Nativelambda.empty_evars in mkCast (cj.uj_val, k, expected_type), - native_conv CUMUL sigma env cj.uj_type expected_type + Nativeconv.native_conv CUMUL sigma env cj.uj_type expected_type in { uj_val = c; uj_type = expected_type } -- cgit v1.2.3 From 44817bf722eacb0379bebc7e435bfafa503d574f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 15 Oct 2015 14:21:45 +0200 Subject: Fix #4346 2/2: VM casts were not inferring universe constraints. --- kernel/typeops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 70f6fd803c..09299f31d7 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -300,7 +300,7 @@ let judge_of_cast env cj k tj = match k with | VMcast -> mkCast (cj.uj_val, k, expected_type), - vm_conv CUMUL env cj.uj_type expected_type + Reduction.vm_conv CUMUL env cj.uj_type expected_type | DEFAULTcast -> mkCast (cj.uj_val, k, expected_type), default_conv ~l2r:false CUMUL env cj.uj_type expected_type -- cgit v1.2.3 From c8b57f62f5ad12f8926f57fcdbc5bb2ee3c63eff Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 13 Oct 2015 11:40:22 +0200 Subject: Miscellaneous typos, spacing, US spelling in comments or variable names. --- kernel/typeops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 09299f31d7..4f32fdce83 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -477,7 +477,7 @@ let rec execute env cstr = let j' = execute env1 c3 in judge_of_letin env name j1 j2 j' - | Cast (c,k, t) -> + | Cast (c,k,t) -> let cj = execute env c in let tj = execute_type env t in judge_of_cast env cj k tj -- 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/typeops.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 4f32fdce83..35f53b7e7c 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -12,7 +12,6 @@ open Names open Univ open Term open Vars -open Context open Declarations open Environ open Entries @@ -99,7 +98,7 @@ let judge_of_variable env id = variables of the current env. Order does not have to be checked assuming that all names are distinct *) let check_hyps_inclusion env c sign = - Context.fold_named_context + Context.Named.fold_outside (fun (id,b1,ty1) () -> try let (_,b2,ty2) = lookup_named id env in @@ -561,6 +560,6 @@ let infer_local_decls env decls = | (id, d) :: l -> let (env, l) = inferec env l in let d = infer_local_decl env id d in - (push_rel d env, add_rel_decl d l) - | [] -> (env, empty_rel_context) in + (push_rel d env, Context.Rel.add d l) + | [] -> (env, Context.Rel.empty) in inferec env decls -- 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/typeops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 4f32fdce83..f7f5e5074e 100644 --- a/kernel/typeops.ml +++ b/kernel/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/typeops.ml | 39 ++++++++++++++++++++++----------------- 1 file changed, 22 insertions(+), 17 deletions(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index f31cba0a8a..eeb12a2b49 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -77,8 +77,9 @@ let judge_of_type u = (*s Type of a de Bruijn index. *) let judge_of_relative env n = + let open Context.Rel.Declaration in try - let (_,_,typ) = lookup_rel n env in + let typ = get_type (lookup_rel n env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> @@ -98,18 +99,20 @@ let judge_of_variable env id = variables of the current env. Order does not have to be checked assuming that all names are distinct *) let check_hyps_inclusion env c sign = + let open Context.Named.Declaration in Context.Named.fold_outside - (fun (id,b1,ty1) () -> + (fun d1 () -> + let id = get_id d1 in try - let (_,b2,ty2) = lookup_named id env in - conv env ty2 ty1; - (match b2,b1 with - | None, None -> () - | None, Some _ -> + let d2 = lookup_named id env in + conv env (get_type d2) (get_type d1); + (match d2,d1 with + | LocalAssum _, LocalAssum _ -> () + | LocalAssum _, LocalDef _ -> (* This is wrong, because we don't know if the body is needed or not for typechecking: *) () - | Some _, None -> raise NotConvertible - | Some b2, Some b1 -> conv env b2 b1); + | LocalDef _, LocalAssum _ -> raise NotConvertible + | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1); with Not_found | NotConvertible | Option.Heterogeneous -> error_reference_variables env id c) sign @@ -124,9 +127,10 @@ let extract_level env p = match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None let extract_context_levels env l = - let fold l (_, b, p) = match b with - | None -> extract_level env p :: l - | _ -> l + let open Context.Rel.Declaration in + let fold l = function + | LocalAssum (_,p) -> extract_level env p :: l + | LocalDef _ -> l in List.fold_left fold [] l @@ -416,6 +420,7 @@ let type_fixpoint env lna lar vdefj = 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) -> @@ -458,13 +463,13 @@ let rec execute env cstr = | Lambda (name,c1,c2) -> let varj = execute_type env c1 in - let env1 = push_rel (name,None,varj.utj_val) env in + let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in let j' = execute env1 c2 in judge_of_abstraction env name varj j' | Prod (name,c1,c2) -> let varj = execute_type env c1 in - let env1 = push_rel (name,None,varj.utj_val) env in + let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in let varj' = execute_type env1 c2 in judge_of_product env name varj varj' @@ -472,7 +477,7 @@ let rec execute env cstr = let j1 = execute env c1 in let j2 = execute_type env c2 in let _ = judge_of_cast env j1 DEFAULTcast j2 in - let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in + let env1 = push_rel (LocalDef (name,j1.uj_val,j2.utj_val)) env in let j' = execute env1 c3 in judge_of_letin env name j1 j2 j' @@ -550,10 +555,10 @@ let infer_v env cv = let infer_local_decl env id = function | LocalDef c -> let j = infer env c in - (Name id, Some j.uj_val, j.uj_type) + Context.Rel.Declaration.LocalDef (Name id, j.uj_val, j.uj_type) | LocalAssum c -> let j = infer env c in - (Name id, None, assumption_of_judgment env j) + Context.Rel.Declaration.LocalAssum (Name id, assumption_of_judgment env j) let infer_local_decls env decls = let rec inferec env = function -- cgit v1.2.3 From 1dddd062f35736285eb2940382df2b53224578a7 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 16 Feb 2016 07:38:45 +0100 Subject: Renaming variants of Entries.local_entry The original datatype: Entries.local_entry = LocalDef of constr | LocalAssum of constr was changed to: Entries.local_entry = LocalDefEntry of constr | LocalAssumEntry of constr There are two advantages: 1. the new names are consistent with other variant names in the same module which also have this "*Entry" suffix 2. the new names do not collide with variants defined in the Context.{Rel,Named}.Declaration modules so both, "Entries" as well as "Context.{Rel,Named}.Declaration" can be open at the same time. The disadvantage is that those new variants are longer. But since those variants are rarely used, it it is not a big deal. --- kernel/typeops.ml | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index eeb12a2b49..0ea68e2bcc 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -18,6 +18,7 @@ open Entries open Reduction open Inductive open Type_errors +open Context.Rel.Declaration let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y @@ -77,7 +78,6 @@ let judge_of_type u = (*s Type of a de Bruijn index. *) let judge_of_relative env n = - let open Context.Rel.Declaration in try let typ = get_type (lookup_rel n env) in { uj_val = mkRel n; @@ -99,9 +99,9 @@ let judge_of_variable env id = variables of the current env. Order does not have to be checked assuming that all names are distinct *) let check_hyps_inclusion env c sign = - let open Context.Named.Declaration in Context.Named.fold_outside (fun d1 () -> + let open Context.Named.Declaration in let id = get_id d1 in try let d2 = lookup_named id env in @@ -127,7 +127,6 @@ let extract_level env p = match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None let extract_context_levels env l = - let open Context.Rel.Declaration in let fold l = function | LocalAssum (_,p) -> extract_level env p :: l | LocalDef _ -> l @@ -420,7 +419,6 @@ let type_fixpoint env lna lar vdefj = 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) -> @@ -553,12 +551,12 @@ let infer_v env cv = (* Typing of several terms. *) let infer_local_decl env id = function - | LocalDef c -> + | LocalDefEntry c -> let j = infer env c in - Context.Rel.Declaration.LocalDef (Name id, j.uj_val, j.uj_type) - | LocalAssum c -> + LocalDef (Name id, j.uj_val, j.uj_type) + | LocalAssumEntry c -> let j = infer env c in - Context.Rel.Declaration.LocalAssum (Name id, assumption_of_judgment env j) + LocalAssum (Name id, assumption_of_judgment env j) let infer_local_decls env decls = let rec inferec env = function -- cgit v1.2.3