From 989553966c7ba1a2cc23fd10fc2633dcb0f98648 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 24 Nov 2016 10:03:17 +0100 Subject: Fix incorrect long multiplication in the VM. If the result had its 30th bit set, then all the high part of the result on a 64-bit architecture would end up being set, thus breaking subsequent computations. This patch also fixes the incorrectly parenthesized definition of uint32_of_value, which by luck was never misused. --- kernel/byterun/coq_interp.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 792a311fcf..47df22807f 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -23,7 +23,7 @@ #include "coq_values.h" /* spiwack: I append here a few macros for value/number manipulation */ -#define uint32_of_value(val) (((uint32_t)val >> 1)) +#define uint32_of_value(val) ((uint32_t)(val) >> 1) #define value_of_uint32(i) ((value)(((uint32_t)(i) << 1) | 1)) #define UI64_of_uint32(lo) ((uint64_t)(lo)) #define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val))) @@ -1206,7 +1206,7 @@ value coq_interprete Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */ /*unsigned shift*/ Field(accu, 0) = (value)((p >> 31)|1) ; /*higher part*/ - Field(accu, 1) = (value)((int32_t)p|1); /*lower part*/ + Field(accu, 1) = (value)((uint32_t)p|1); /*lower part*/ } Next; } -- cgit v1.2.3 From 17559d528cf7ff92a089d1b966c500424ba45099 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 18 Nov 2016 13:24:39 +0100 Subject: Slightly more efficient [Univ.super] implem --- kernel/univ.ml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) (limited to 'kernel') diff --git a/kernel/univ.ml b/kernel/univ.ml index 9224ec48d7..c863fac0eb 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -471,12 +471,17 @@ struct let super (u,n as x) (v,n' as y) = let cmp = Level.compare u v in - if Int.equal cmp 0 then - if n < n' then Inl true - else Inl false - else if is_prop x then Inl true - else if is_prop y then Inl false - else Inr cmp + if Int.equal cmp 0 then Inl (n < n') + else + match x, y with + | (l,0), (l',0) -> + let open RawLevel in + (match Level.data l, Level.data l' with + | Prop, Prop -> Inl false + | Prop, _ -> Inl true + | _, Prop -> Inl false + | _, _ -> Inr cmp) + | _, _ -> Inr cmp let to_string (v, n) = if Int.equal n 0 then Level.to_string v -- cgit v1.2.3 From 25c82d55497db43bf2cd131f10d2ef366758bbe1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 18 Nov 2016 13:25:05 +0100 Subject: Fix UGraph.check_eq! Universes are kept in normal form w.r.t. equality but not the <= relation, so the previous check worked almost always but was actually too strict! In cases like (max(Set,u) = u) when u is declared >= Set it was failing to find an equality. Applying the KISS principle: u = v <-> u <= v /\ v <= u. Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of a colon in a typing judgment), this was not the case when an algebraic universe instantiated an evar that appeared in the term. We force their universe variable status to change in refresh_universes to avoid this. Fix ind sort inference: Use syntactic universe equality for inductive sort inference instead of check_leq (which now correctly takes constraints into account) and simplify code --- kernel/uGraph.ml | 21 +++++++-------------- 1 file changed, 7 insertions(+), 14 deletions(-) (limited to 'kernel') diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index e2712615be..4884d0deb1 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -638,19 +638,6 @@ let check_smaller g strict u v = type 'a check_function = universes -> 'a -> 'a -> bool -let check_equal_expr g x y = - x == y || (let (u, n) = x and (v, m) = y in - Int.equal n m && check_equal g u v) - -let check_eq_univs g l1 l2 = - let f x1 x2 = check_equal_expr g x1 x2 in - let exists x1 l = Universe.exists (fun x2 -> f x1 x2) l in - Universe.for_all (fun x1 -> exists x1 l2) l1 - && Universe.for_all (fun x2 -> exists x2 l1) l2 - -let check_eq g u v = - Universe.equal u v || check_eq_univs g u v - let check_smaller_expr g (u,n) (v,m) = let diff = n - m in match diff with @@ -669,7 +656,13 @@ let real_check_leq g u v = let check_leq g u v = Universe.equal u v || is_type0m_univ u || - check_eq_univs g u v || real_check_leq g u v + real_check_leq g u v + +let check_eq_univs g l1 l2 = + real_check_leq g l1 l2 && real_check_leq g l2 l1 + +let check_eq g u v = + Universe.equal u v || check_eq_univs g u v (* enforce_univ_eq g u v will force u=v if possible, will fail otherwise *) -- cgit v1.2.3 From d06211803146dec998b414d215d4d93190e2001f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 28 Nov 2016 18:36:10 +0100 Subject: Univs: fix bug #5180 In the kernel's generic conversion, backtrack on UniverseInconsistency for the unfolding heuristic (single backtracking point in reduction). This exception can be raised in the univ_compare structure to produce better error messages when the generic conversion function is called from higher level code in reductionops.ml, which itself is called during unification in evarconv.ml. Inside the kernel, the infer and check variants of conversion never raise UniverseInconsistency though, so this does not change the behavior of the kernel. --- kernel/reduction.ml | 2 +- kernel/reduction.mli | 8 +++++++- 2 files changed, 8 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 6c664f7918..1ae89347ad 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -316,7 +316,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (try let cuniv = conv_table_key infos fl1 fl2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - with NotConvertible -> + with NotConvertible | Univ.UniverseInconsistency _ -> (* else the oracle tells which constant is to be expanded *) let oracle = CClosure.oracle_of_infos infos in let (app1,app2) = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 9812c45f7b..8a2b2469d6 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -36,7 +36,7 @@ type 'a extended_conversion_function = type conv_pb = CONV | CUMUL type 'a universe_compare = - { (* Might raise NotConvertible *) + { (* Might raise NotConvertible or UnivInconsistency *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; @@ -56,9 +56,12 @@ constructors. *) val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare +(** These two never raise UnivInconsistency, inferred_universes + just gathers the constraints. *) val checked_universes : UGraph.t universe_compare val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare +(** These two functions can only raise NotConvertible *) val conv : constr extended_conversion_function val conv_leq : types extended_conversion_function @@ -70,6 +73,9 @@ val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> ?ts:Names.transparent_state -> types infer_conversion_function +(** Depending on the universe state functions, this might raise + [UniverseInconsistency] in addition to [NotConvertible] (for better error + messages). *) val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function -- cgit v1.2.3 From 0ea7bdc2e315da9a0a8338e5099dfcaad0bac9ef Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 2 Dec 2016 15:48:30 +0100 Subject: Fix #5242 - Dubious unsilenceable warning on invalid identifier We make this warning configurable and disabled by default. --- kernel/names.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'kernel') diff --git a/kernel/names.ml b/kernel/names.ml index 9267a64d61..1eb9a31751 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -34,9 +34,15 @@ struct let hash = String.hash + let warn_invalid_identifier = + CWarnings.create ~name:"invalid-identifier" ~category:"parsing" + ~default:CWarnings.Disabled + (fun s -> str s) + let check_soft ?(warn = true) x = let iter (fatal, x) = - if fatal then CErrors.error x else if warn then Feedback.msg_warning (str x) + if fatal then CErrors.error x else + if warn then warn_invalid_identifier x in Option.iter iter (Unicode.ident_refutation x) -- cgit v1.2.3 From b8c0f76e507dc0c5dbae3ea7a89d78f16b4a7acb Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 2 Dec 2016 18:00:18 +0100 Subject: Document changes --- kernel/univ.ml | 54 ++++++++++++++++++++++++++++++++++-------------------- 1 file changed, 34 insertions(+), 20 deletions(-) (limited to 'kernel') diff --git a/kernel/univ.ml b/kernel/univ.ml index c863fac0eb..09f884ecd0 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -468,20 +468,32 @@ struct else if Level.is_prop u then hcons (Level.set,n+k) else hcons (u,n+k) - + + type super_result = + SuperSame of bool + (* The level expressions are in cumulativity relation. boolean + indicates if left is smaller than right? *) + | SuperDiff of int + (* The level expressions are unrelated, the comparison result + is canonical *) + + (** [super u v] compares two level expressions, + returning [SuperSame] if they refer to the same level at potentially different + increments or [SuperDiff] if they are different. The booleans indicate if the + left expression is "smaller" than the right one in both cases. *) let super (u,n as x) (v,n' as y) = let cmp = Level.compare u v in - if Int.equal cmp 0 then Inl (n < n') + if Int.equal cmp 0 then SuperSame (n < n') else match x, y with | (l,0), (l',0) -> let open RawLevel in (match Level.data l, Level.data l' with - | Prop, Prop -> Inl false - | Prop, _ -> Inl true - | _, Prop -> Inl false - | _, _ -> Inr cmp) - | _, _ -> Inr cmp + | Prop, Prop -> SuperSame false + | Prop, _ -> SuperSame true + | _, Prop -> SuperSame false + | _, _ -> SuperDiff cmp) + | _, _ -> SuperDiff cmp let to_string (v, n) = if Int.equal n 0 then Level.to_string v @@ -603,24 +615,26 @@ struct | Nil, _ -> l2 | _, Nil -> l1 | Cons (h1, _, t1), Cons (h2, _, t2) -> - (match Expr.super h1 h2 with - | Inl true (* h1 < h2 *) -> merge_univs t1 l2 - | Inl false -> merge_univs l1 t2 - | Inr c -> - if c <= 0 (* h1 < h2 is name order *) - then cons h1 (merge_univs t1 l2) - else cons h2 (merge_univs l1 t2)) + let open Expr in + (match super h1 h2 with + | SuperSame true (* h1 < h2 *) -> merge_univs t1 l2 + | SuperSame false -> merge_univs l1 t2 + | SuperDiff c -> + if c <= 0 (* h1 < h2 is name order *) + then cons h1 (merge_univs t1 l2) + else cons h2 (merge_univs l1 t2)) let sort u = let rec aux a l = match l with | Cons (b, _, l') -> - (match Expr.super a b with - | Inl false -> aux a l' - | Inl true -> l - | Inr c -> - if c <= 0 then cons a l - else cons b (aux a l')) + let open Expr in + (match super a b with + | SuperSame false -> aux a l' + | SuperSame true -> l + | SuperDiff c -> + if c <= 0 then cons a l + else cons b (aux a l')) | Nil -> cons a l in fold (fun a acc -> aux a acc) u nil -- cgit v1.2.3 From 40cffd816b7adbf8f136f62f6f891fb5be9b96a6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 6 Dec 2016 16:56:42 +0100 Subject: Fix #5248 - test-suite fails in 8.6beta1 This was yet another bug in the VM long multiplication, that I unfortunately introduced in ebc509ed2. It was impacting only 32-bit architectures. In the future, I'll try to make sure that 1) we provide unit tests for integer arithmetic (my int63 branch ships with such tests) 2) our continuous testing infrastructure runs the test suite on a 32-bit architecture. I tried to set up such an instance, but failed. Waiting for support reply. --- kernel/byterun/coq_interp.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 47df22807f..5dec3b785c 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -23,9 +23,9 @@ #include "coq_values.h" /* spiwack: I append here a few macros for value/number manipulation */ -#define uint32_of_value(val) ((uint32_t)(val) >> 1) -#define value_of_uint32(i) ((value)(((uint32_t)(i) << 1) | 1)) -#define UI64_of_uint32(lo) ((uint64_t)(lo)) +#define uint32_of_value(val) (((uint32_t)(val)) >> 1) +#define value_of_uint32(i) ((value)((((uint32_t)(i)) << 1) | 1)) +#define UI64_of_uint32(lo) ((uint64_t)((uint32_t)(lo))) #define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val))) /* /spiwack */ -- cgit v1.2.3 From 90b61424761c5ba1ddbecf20c29d78b485584ae7 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Mon, 12 Dec 2016 14:18:48 +0100 Subject: Extend Fast_typeops to be a replacement for Typeops This brings the fix in cad44fc for #2996 to the copy of Fast_typeops.check_hyps_inclusion. Fast_typeops.constant_type checks the universe constraints instead of outputting them. Since everyone who used Typeops.constant_type just discarded the constraints they've been switched to constant_type_in which should be the same in Fast_typeops and Typeops. There are some small differences in the interfaces: - Typeops.type_of_projection <-> Fast_typeops.type_of_projection_constant to avoid collision with the internally used type_of_projection (which gives the type of [Proj(p,c)]). - check_hyps_inclusion takes [('a -> constr)] and ['a] instead of [constr] for reporting errors. --- kernel/fast_typeops.ml | 284 +++++++++++++++++++++++++++++++++++------------- kernel/fast_typeops.mli | 106 +++++++++++++++++- kernel/typeops.mli | 10 +- 3 files changed, 316 insertions(+), 84 deletions(-) (limited to 'kernel') diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index dce4e93076..7d9a2aac09 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -37,19 +37,14 @@ let check_constraints cst env = else error_unsatisfied_constraints env cst (* This should be a type (a priori without intention to be an assumption) *) -let type_judgment env c t = - match kind_of_term(whd_all env t) with - | Sort s -> {utj_val = c; utj_type = s } - | _ -> error_not_type env (make_judge c t) - let check_type env c t = match kind_of_term(whd_all env t) with | Sort s -> s | _ -> error_not_type env (make_judge c t) -(* This should be a type intended to be assumed. The error message is *) -(* not as useful as for [type_judgment]. *) -let assumption_of_judgment env t ty = +(* This should be a type intended to be assumed. The error message is + not as useful as for [type_judgment]. *) +let check_assumption env t ty = try let _ = check_type env t ty in t with TypeError _ -> error_assumption env (make_judge t ty) @@ -62,26 +57,24 @@ let assumption_of_judgment env t ty = (* Prop and Set *) -let judge_of_prop = mkSort type1_sort - -let judge_of_prop_contents _ = judge_of_prop +let type1 = mkSort type1_sort (* Type of Type(i). *) -let judge_of_type u = +let type_of_type u = let uu = Universe.super u in mkType uu (*s Type of a de Bruijn index. *) -let judge_of_relative env n = +let type_of_relative env n = try env |> lookup_rel n |> RelDecl.get_type |> lift n with Not_found -> error_unbound_rel env n (* Type of variables *) -let judge_of_variable env id = +let type_of_variable env id = try named_type id env with Not_found -> error_unbound_var env id @@ -89,17 +82,24 @@ let judge_of_variable env id = (* Management of context of variables. *) (* Checks if a context of variables can be instantiated by the - variables of the current env *) -(* TODO: check order? *) + variables of the current env. + Order does not have to be checked assuming that all names are distinct *) let check_hyps_inclusion env f c sign = Context.Named.fold_outside - (fun decl () -> - let id = NamedDecl.get_id decl in - let ty1 = NamedDecl.get_type decl in + (fun d1 () -> + let open Context.Named.Declaration in + let id = NamedDecl.get_id d1 in try - let ty2 = named_type id env in - if not (eq_constr ty2 ty1) then raise Exit - with Not_found | Exit -> + 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: *) () + | LocalDef _, LocalAssum _ -> raise NotConvertible + | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1); + with Not_found | NotConvertible | Option.Heterogeneous -> error_reference_variables env id (f c)) sign ~init:() @@ -111,7 +111,7 @@ let check_hyps_inclusion env f c sign = (* Type of constants *) -let type_of_constant_knowing_parameters_arity env t paramtyps = +let type_of_constant_type_knowing_parameters env t paramtyps = match t with | RegularArity t -> t | TemplateArity (sign,ar) -> @@ -119,19 +119,28 @@ let type_of_constant_knowing_parameters_arity env t paramtyps = let ctx,s = instantiate_universes env ctx ar paramtyps in mkArity (List.rev ctx,s) -let type_of_constant_knowing_parameters env cst paramtyps = - let ty, cu = constant_type env cst in - type_of_constant_knowing_parameters_arity env ty paramtyps, cu - -let judge_of_constant_knowing_parameters env (kn,u as cst) args = +let type_of_constant_knowing_parameters env (kn,u as cst) args = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in - let ty, cu = type_of_constant_knowing_parameters env cst args in + let ty, cu = constant_type env cst in + let ty = type_of_constant_type_knowing_parameters env ty args in let () = check_constraints cu env in ty -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] +let type_of_constant_knowing_parameters_in env (kn,u as cst) args = + let cb = lookup_constant kn env in + let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in + let ty = constant_type_in env cst in + type_of_constant_type_knowing_parameters env ty args + +let type_of_constant env cst = + type_of_constant_knowing_parameters env cst [||] + +let type_of_constant_in env cst = + type_of_constant_knowing_parameters_in env cst [||] + +let type_of_constant_type env t = + type_of_constant_type_knowing_parameters env t [||] (* Type of a lambda-abstraction. *) @@ -145,7 +154,7 @@ let judge_of_constant env cst = and no upper constraint exists on the sort $s$, we don't need to compute $s$ *) -let judge_of_abstraction env name var ty = +let type_of_abstraction env name var ty = mkProd (name, var, ty) (* Type of an application. *) @@ -153,7 +162,7 @@ let judge_of_abstraction env name var ty = let make_judgev c t = Array.map2 make_judge c t -let judge_of_apply env func funt argsv argstv = +let type_of_apply env func funt argsv argstv = let len = Array.length argsv in let rec apply_rec i typ = if Int.equal i len then typ @@ -207,7 +216,7 @@ let sort_of_product env domsort rangsort = where j.uj_type is convertible to a sort s2 *) -let judge_of_product env name s1 s2 = +let type_of_product env name s1 s2 = let s = sort_of_product env s1 s2 in mkSort s @@ -220,7 +229,7 @@ let judge_of_product env name s1 s2 = env |- c:typ2 *) -let judge_of_cast env c ct k expected_type = +let check_cast env c ct k expected_type = try match k with | VMcast -> @@ -249,33 +258,34 @@ let judge_of_cast env c ct k expected_type = the App case of execute; from this constraints, the expected dynamic constraints of the form u<=v are enforced *) -let judge_of_inductive_knowing_parameters env (ind,u as indu) args = +let type_of_inductive_knowing_parameters env (ind,u as indu) args = let (mib,mip) as spec = lookup_mind_specif env ind in check_hyps_inclusion env mkIndU indu mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters env (spec,u) args in - check_constraints cst env; - t + check_constraints cst env; + t -let judge_of_inductive env (ind,u as indu) = +let type_of_inductive env (ind,u as indu) = let (mib,mip) = lookup_mind_specif env ind in check_hyps_inclusion env mkIndU indu mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in - check_constraints cst env; - t + check_constraints cst env; + t (* Constructors. *) -let judge_of_constructor env (c,u as cu) = - let _ = +let type_of_constructor env (c,u as cu) = + let () = let ((kn,_),_) = c in let mib = lookup_mind kn env in - check_hyps_inclusion env mkConstructU cu mib.mind_hyps in + check_hyps_inclusion env mkConstructU cu mib.mind_hyps + in let specif = lookup_mind_specif env (inductive_of_constructor c) in let t,cst = constrained_type_of_constructor cu specif in let () = check_constraints cst env in - t + t (* Case. *) @@ -287,25 +297,25 @@ let check_branch_types env (ind,u) c ct lft explft = | Invalid_argument _ -> error_number_branches env (make_judge c ct) (Array.length explft) -let judge_of_case env ci p pt c ct lf lft = +let type_of_case env ci p pt c ct lf lft = let (pind, _ as indspec) = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - let _ = check_case_info env pind ci in + let () = check_case_info env pind ci in let (bty,rslty) = type_case_branches env indspec (make_judge p pt) c in let () = check_branch_types env pind c ct lft bty in - rslty + rslty -let judge_of_projection env p c ct = +let type_of_projection env p c ct = let pb = lookup_projection p env in let (ind,u), args = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(eq_mind pb.proj_ind (fst ind)); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in - substl (c :: List.rev args) ty + assert(eq_mind pb.proj_ind (fst ind)); + let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in + substl (c :: List.rev args) ty (* Fixpoints. *) @@ -313,7 +323,7 @@ let judge_of_projection env p c ct = (* Checks the type of a general (co)fixpoint, i.e. without checking *) (* the specific guard condition. *) -let type_fixpoint env lna lar vdef vdeft = +let check_fixpoint env lna lar vdef vdeft = let lt = Array.length vdeft in assert (Int.equal (Array.length lar) lt); try @@ -333,23 +343,23 @@ let rec execute env cstr = match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> - judge_of_prop_contents c + type1 | Sort (Type u) -> - judge_of_type u + type_of_type u | Rel n -> - judge_of_relative env n + type_of_relative env n | Var id -> - judge_of_variable env id + type_of_variable env id | Const c -> - judge_of_constant env c + type_of_constant env c | Proj (p, c) -> let ct = execute env c in - judge_of_projection env p c ct + type_of_projection env p c ct (* Lambda calculus operators *) | App (f,args) -> @@ -359,56 +369,56 @@ let rec execute env cstr = | Ind ind when Environ.template_polymorphic_pind ind env -> (* Template sort-polymorphism of inductive types *) let args = Array.map (fun t -> lazy t) argst in - judge_of_inductive_knowing_parameters env ind args + type_of_inductive_knowing_parameters env ind args | Const cst when Environ.template_polymorphic_pconstant cst env -> (* Template sort-polymorphism of constants *) let args = Array.map (fun t -> lazy t) argst in - judge_of_constant_knowing_parameters env cst args + type_of_constant_knowing_parameters env cst args | _ -> (* Full or no sort-polymorphism *) execute env f in - judge_of_apply env f ft args argst + type_of_apply env f ft args argst | Lambda (name,c1,c2) -> let _ = execute_is_type env c1 in let env1 = push_rel (LocalAssum (name,c1)) env in let c2t = execute env1 c2 in - judge_of_abstraction env name c1 c2t + type_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> let vars = execute_is_type env c1 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' + type_of_product env name vars vars' | LetIn (name,c1,c2,c3) -> 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 () = check_cast env c1 c1t DEFAULTcast c2 in let env1 = push_rel (LocalDef (name,c1,c2)) env in let c3t = execute env1 c3 in subst1 c1 c3t | Cast (c,k,t) -> let ct = execute env c in - let _ts = execute_type env t in - let _ = judge_of_cast env c ct k t in + let _ts = (check_type env t (execute env t)) in + let () = check_cast env c ct k t in t (* Inductive types *) | Ind ind -> - judge_of_inductive env ind + type_of_inductive env ind | Construct c -> - judge_of_constructor env c + type_of_constructor env c | Case (ci,p,c,lf) -> let ct = execute env c in let pt = execute env p in let lft = execute_array env lf in - judge_of_case env ci p pt c ct lf lft + type_of_case env ci p pt c ct lf lft | Fix ((vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in @@ -431,16 +441,12 @@ and execute_is_type env constr = let t = execute env constr in check_type env constr t -and execute_type env constr = - let t = execute env constr in - type_judgment env constr t - and execute_recdef env (names,lar,vdef) i = let lart = execute_array env lar in - let lara = Array.map2 (assumption_of_judgment env) lar lart in + let lara = Array.map2 (check_assumption env) lar lart in let env1 = push_rec_types (names,lara,vdef) env in let vdeft = execute_array env1 vdef in - let () = type_fixpoint env1 names lara vdef vdeft in + let () = check_fixpoint env1 names lara vdef vdeft in (lara.(i),(names,lara,vdef)) and execute_array env = Array.map (execute env) @@ -456,9 +462,133 @@ let infer = Profile.profile2 infer_key (fun b c -> infer b c) else (fun b c -> infer b c) +let assumption_of_judgment env {uj_val=c; uj_type=t} = + check_assumption env c t + +let type_judgment env {uj_val=c; uj_type=t} = + let s = check_type env c t in + {utj_val = c; utj_type = s } + let infer_type env constr = - execute_type env constr + let t = execute env constr in + let s = check_type env constr t in + {utj_val = constr; utj_type = s} let infer_v env cv = let jv = execute_array env cv in make_judgev cv jv + +(* Typing of several terms. *) + +let infer_local_decl env id = function + | Entries.LocalDefEntry c -> + let t = execute env c in + RelDecl.LocalDef (Name id, c, t) + | Entries.LocalAssumEntry c -> + let t = execute env c in + RelDecl.LocalAssum (Name id, check_assumption env c t) + +let infer_local_decls env decls = + let rec inferec env = function + | (id, d) :: l -> + let (env, l) = inferec env l in + let d = infer_local_decl env id d in + (push_rel d env, Context.Rel.add d l) + | [] -> (env, Context.Rel.empty) + in + inferec env decls + +let judge_of_prop = make_judge mkProp type1 +let judge_of_set = make_judge mkSet type1 +let judge_of_type u = make_judge (mkType u) (type_of_type u) + +let judge_of_prop_contents = function + | Null -> judge_of_prop + | Pos -> judge_of_set + +let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) + +let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) + +let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst) +let judge_of_constant_knowing_parameters env cst args = + make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args) + +let judge_of_projection env p cj = + make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type) + +let dest_judgev v = + Array.map j_val v, Array.map j_type v + +let judge_of_apply env funj argjv = + let args, argtys = dest_judgev argjv in + make_judge (mkApp (funj.uj_val, args)) (type_of_apply env funj.uj_val funj.uj_type args argtys) + +let judge_of_abstraction env x varj bodyj = + make_judge (mkLambda (x, varj.utj_val, bodyj.uj_val)) + (type_of_abstraction env x varj.utj_val bodyj.uj_type) + +let judge_of_product env x varj outj = + make_judge (mkProd (x, varj.utj_val, outj.utj_val)) + (mkSort (sort_of_product env varj.utj_type outj.utj_type)) + +let judge_of_letin env name defj typj j = + make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) + (subst1 defj.uj_val j.uj_type) + +let judge_of_cast env cj k tj = + let () = check_cast env cj.uj_val cj.uj_type k tj.utj_val in + let c = match k with | REVERTcast -> cj.uj_val | _ -> mkCast (cj.uj_val, k, tj.utj_val) in + make_judge c tj.utj_val + +let judge_of_inductive env indu = + make_judge (mkIndU indu) (type_of_inductive env indu) + +let judge_of_constructor env cu = + make_judge (mkConstructU cu) (type_of_constructor env cu) + +let judge_of_case env ci pj cj lfj = + let lf, lft = dest_judgev lfj in + make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) + (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) + +let type_of_projection_constant env (p,u) = + let cst = Projection.constant p in + let cb = lookup_constant cst env in + match cb.const_proj with + | Some pb -> + if cb.const_polymorphic then + Vars.subst_instance_constr u pb.proj_type + else pb.proj_type + | None -> raise (Invalid_argument "type_of_projection: not a projection") + +(* Instantiation of terms on real arguments. *) + +(* Make a type polymorphic if an arity *) + +let extract_level env p = + let _,c = dest_prod_assum env p in + match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None + +let extract_context_levels env l = + let fold l = function + | RelDecl.LocalAssum (_,p) -> extract_level env p :: l + | RelDecl.LocalDef _ -> l + in + List.fold_left fold [] 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) -> + let ind, l = decompose_app (whd_all 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 diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli index 41cff607e7..73c63db681 100644 --- a/kernel/fast_typeops.mli +++ b/kernel/fast_typeops.mli @@ -6,13 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Names +open Univ open Term open Environ +open Entries open Declarations (** {6 Typing functions (not yet tagged as safe) } - - They return unsafe judgments that are "in context" of a set of + + They return unsafe judgments that are "in context" of a set of (local) universe variables (the ones that appear in the term) and associated constraints. In case of polymorphic definitions, these variables and constraints will be generalized. @@ -22,3 +25,102 @@ open Declarations val infer : env -> constr -> unsafe_judgment val infer_v : env -> constr array -> unsafe_judgment array val infer_type : env -> types -> unsafe_type_judgment + +val infer_local_decls : + env -> (Id.t * local_entry) list -> (env * Context.Rel.t) + +(** {6 Basic operations of the typing machine. } *) + +(** If [j] is the judgement {% $ %}c:t{% $ %}, then [assumption_of_judgement env j] + returns the type {% $ %}c{% $ %}, checking that {% $ %}t{% $ %} is a sort. *) + +val assumption_of_judgment : env -> unsafe_judgment -> types +val type_judgment : env -> unsafe_judgment -> unsafe_type_judgment + +(** {6 Type of sorts. } *) +val judge_of_prop : unsafe_judgment +val judge_of_set : unsafe_judgment +val judge_of_prop_contents : contents -> unsafe_judgment +val judge_of_type : universe -> unsafe_judgment + +(** {6 Type of a bound variable. } *) +val judge_of_relative : env -> int -> unsafe_judgment + +(** {6 Type of variables } *) +val judge_of_variable : env -> variable -> unsafe_judgment + +(** {6 type of a constant } *) + +val judge_of_constant : env -> pconstant -> unsafe_judgment + +val judge_of_constant_knowing_parameters : + env -> pconstant -> types Lazy.t array -> unsafe_judgment + +(** {6 type of an applied projection } *) + +val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment + +(** {6 Type of application. } *) +val judge_of_apply : + env -> unsafe_judgment -> unsafe_judgment array + -> unsafe_judgment + +(** {6 Type of an abstraction. } *) +val judge_of_abstraction : + env -> Name.t -> unsafe_type_judgment -> unsafe_judgment + -> unsafe_judgment + +val sort_of_product : env -> sorts -> sorts -> sorts + +(** {6 Type of a product. } *) +val judge_of_product : + env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment + -> unsafe_judgment + +(** s Type of a let in. *) +val judge_of_letin : + env -> Name.t -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment + -> unsafe_judgment + +(** {6 Type of a cast. } *) +val judge_of_cast : + env -> unsafe_judgment -> cast_kind -> unsafe_type_judgment -> + unsafe_judgment + +(** {6 Inductive types. } *) + +val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment + +(* val judge_of_inductive_knowing_parameters : *) +(* env -> inductive -> unsafe_judgment array -> unsafe_judgment *) + +val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment + +(** {6 Type of Cases. } *) +val judge_of_case : env -> case_info + -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array + -> unsafe_judgment + +(* val type_of_constant : env -> pconstant -> types constrained *) + +val type_of_constant_type : env -> constant_type -> types + +val type_of_projection_constant : env -> Names.projection puniverses -> types + +val type_of_constant_in : env -> pconstant -> types + +val type_of_constant_type_knowing_parameters : + env -> constant_type -> types Lazy.t array -> types + +(* val type_of_constant_knowing_parameters : *) +(* env -> pconstant -> types Lazy.t array -> types constrained *) + +val type_of_constant_knowing_parameters_in : + env -> pconstant -> types Lazy.t array -> types + +(** Make a type polymorphic if an arity *) +val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> + constant_type + +(** Check that hyps are included in env and fails with error otherwise *) +val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 81fd1427d0..cfc82c1589 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -102,10 +102,10 @@ val judge_of_case : env -> case_info -> unsafe_judgment (** Typecheck general fixpoint (not checking guard conditions) *) -val type_fixpoint : env -> Name.t array -> types array - -> unsafe_judgment array -> unit +(* val type_fixpoint : env -> Name.t array -> types array *) +(* -> unsafe_judgment array -> unit *) -val type_of_constant : env -> pconstant -> types constrained +(* val type_of_constant : env -> pconstant -> types constrained *) val type_of_constant_type : env -> constant_type -> types @@ -116,8 +116,8 @@ val type_of_constant_in : env -> pconstant -> types val type_of_constant_type_knowing_parameters : env -> constant_type -> types Lazy.t array -> types -val type_of_constant_knowing_parameters : - env -> pconstant -> types Lazy.t array -> types constrained +(* val type_of_constant_knowing_parameters : *) +(* env -> pconstant -> types Lazy.t array -> types constrained *) val type_of_constant_knowing_parameters_in : env -> pconstant -> types Lazy.t array -> types -- cgit v1.2.3 From 421d846d80c19226ba0922ff3c3b0006c98c21b6 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Mon, 12 Dec 2016 14:49:01 +0100 Subject: Replace Typeops by Fast_typeops This is really [mv fast_typeops.ml{,i} typeops.ml{,i}] plus trivial changes in the other files, the real changes are in the parent commit. --- kernel/fast_typeops.ml | 594 ------------------------------------------------ kernel/fast_typeops.mli | 126 ---------- kernel/kernel.mllib | 1 - kernel/term_typing.ml | 1 - kernel/typeops.ml | 561 +++++++++++++++++++++++---------------------- kernel/typeops.mli | 10 +- 6 files changed, 295 insertions(+), 998 deletions(-) delete mode 100644 kernel/fast_typeops.ml delete mode 100644 kernel/fast_typeops.mli (limited to 'kernel') diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml deleted file mode 100644 index 7d9a2aac09..0000000000 --- a/kernel/fast_typeops.ml +++ /dev/null @@ -1,594 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - try conv_leq false env t1 t2 - with NotConvertible -> raise (NotConvertibleVect i)) - () - v1 - v2 - -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 intention to be an assumption) *) -let check_type env c t = - match kind_of_term(whd_all env t) with - | Sort s -> s - | _ -> error_not_type env (make_judge c t) - -(* This should be a type intended to be assumed. The error message is - not as useful as for [type_judgment]. *) -let check_assumption env t ty = - try let _ = check_type env t ty in t - with TypeError _ -> - error_assumption env (make_judge t ty) - -(************************************************) -(* Incremental typing rules: builds a typing judgment given the *) -(* judgments for the subterms. *) - -(*s Type of sorts *) - -(* Prop and Set *) - -let type1 = mkSort type1_sort - -(* Type of Type(i). *) - -let type_of_type u = - let uu = Universe.super u in - mkType uu - -(*s Type of a de Bruijn index. *) - -let type_of_relative env n = - try - env |> lookup_rel n |> RelDecl.get_type |> lift n - with Not_found -> - error_unbound_rel env n - -(* Type of variables *) -let type_of_variable env id = - try named_type id env - with Not_found -> - error_unbound_var env id - -(* Management of context of variables. *) - -(* Checks if a context of variables can be instantiated by the - variables of the current env. - Order does not have to be checked assuming that all names are distinct *) -let check_hyps_inclusion env f c sign = - Context.Named.fold_outside - (fun d1 () -> - let open Context.Named.Declaration in - let id = NamedDecl.get_id d1 in - try - 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: *) () - | LocalDef _, LocalAssum _ -> raise NotConvertible - | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1); - with Not_found | NotConvertible | Option.Heterogeneous -> - error_reference_variables env id (f c)) - sign - ~init:() - -(* Instantiation of terms on real arguments. *) - -(* Make a type polymorphic if an arity *) - -(* Type of constants *) - - -let type_of_constant_type_knowing_parameters env t paramtyps = - match t with - | RegularArity t -> t - | TemplateArity (sign,ar) -> - let ctx = List.rev sign in - let ctx,s = instantiate_universes env ctx ar paramtyps in - mkArity (List.rev ctx,s) - -let type_of_constant_knowing_parameters env (kn,u as cst) args = - let cb = lookup_constant kn env in - let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in - let ty, cu = constant_type env cst in - let ty = type_of_constant_type_knowing_parameters env ty args in - let () = check_constraints cu env in - ty - -let type_of_constant_knowing_parameters_in env (kn,u as cst) args = - let cb = lookup_constant kn env in - let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in - let ty = constant_type_in env cst in - type_of_constant_type_knowing_parameters env ty args - -let type_of_constant env cst = - type_of_constant_knowing_parameters env cst [||] - -let type_of_constant_in env cst = - type_of_constant_knowing_parameters_in env cst [||] - -let type_of_constant_type env t = - type_of_constant_type_knowing_parameters env t [||] - -(* Type of a lambda-abstraction. *) - -(* [judge_of_abstraction env name var j] implements the rule - - env, name:typ |- j.uj_val:j.uj_type env, |- (name:typ)j.uj_type : s - ----------------------------------------------------------------------- - env |- [name:typ]j.uj_val : (name:typ)j.uj_type - - Since all products are defined in the Calculus of Inductive Constructions - and no upper constraint exists on the sort $s$, we don't need to compute $s$ -*) - -let type_of_abstraction env name var ty = - mkProd (name, var, ty) - -(* Type of an application. *) - -let make_judgev c t = - Array.map2 make_judge c t - -let type_of_apply env func funt argsv argstv = - let len = Array.length argsv in - let rec apply_rec i typ = - if Int.equal i len then typ - else - (match kind_of_term (whd_all env typ) with - | Prod (_,c1,c2) -> - let arg = argsv.(i) and argt = argstv.(i) in - (try - let () = conv_leq false env argt c1 in - apply_rec (i+1) (subst1 arg c2) - with NotConvertible -> - error_cant_apply_bad_type env - (i+1,c1,argt) - (make_judge func funt) - (make_judgev argsv argstv)) - - | _ -> - error_cant_apply_not_functional env - (make_judge func funt) - (make_judgev argsv argstv)) - in apply_rec 0 funt - -(* Type of product *) - -let sort_of_product env domsort rangsort = - match (domsort, rangsort) with - (* Product rule (s,Prop,Prop) *) - | (_, Prop Null) -> rangsort - (* Product rule (Prop/Set,Set,Set) *) - | (Prop _, Prop Pos) -> rangsort - (* Product rule (Type,Set,?) *) - | (Type u1, Prop Pos) -> - if is_impredicative_set env then - (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) - rangsort - else - (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) - Type (Universe.sup Universe.type0 u1) - (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2) - (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Null, Type _) -> rangsort - (* Product rule (Type_i,Type_i,Type_i) *) - | (Type u1, Type u2) -> Type (Universe.sup u1 u2) - -(* [judge_of_product env name (typ1,s1) (typ2,s2)] implements the rule - - env |- typ1:s1 env, name:typ1 |- typ2 : s2 - ------------------------------------------------------------------------- - s' >= (s1,s2), env |- (name:typ)j.uj_val : s' - - where j.uj_type is convertible to a sort s2 -*) -let type_of_product env name s1 s2 = - let s = sort_of_product env s1 s2 in - mkSort s - -(* Type of a type cast *) - -(* [judge_of_cast env (c,typ1) (typ2,s)] implements the rule - - env |- c:typ1 env |- typ2:s env |- typ1 <= typ2 - --------------------------------------------------------------------- - env |- c:typ2 -*) - -let check_cast env c ct k expected_type = - try - match k with - | VMcast -> - vm_conv CUMUL env ct expected_type - | DEFAULTcast -> - default_conv ~l2r:false CUMUL env ct expected_type - | REVERTcast -> - default_conv ~l2r:true CUMUL env ct expected_type - | NATIVEcast -> - let sigma = Nativelambda.empty_evars in - Nativeconv.native_conv CUMUL sigma env ct expected_type - with NotConvertible -> - error_actual_type env (make_judge c ct) expected_type - -(* Inductive types. *) - -(* The type is parametric over the uniform parameters whose conclusion - is in Type; to enforce the internal constraints between the - parameters and the instances of Type occurring in the type of the - constructors, we use the level variables _statically_ assigned to - the conclusions of the parameters as mediators: e.g. if a parameter - has conclusion Type(alpha), static constraints of the form alpha<=v - exist between alpha and the Type's occurring in the constructor - types; when the parameters is finally instantiated by a term of - conclusion Type(u), then the constraints u<=alpha is computed in - the App case of execute; from this constraints, the expected - dynamic constraints of the form u<=v are enforced *) - -let type_of_inductive_knowing_parameters env (ind,u as indu) args = - let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters - env (spec,u) args - in - check_constraints cst env; - t - -let type_of_inductive env (ind,u as indu) = - let (mib,mip) = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in - check_constraints cst env; - t - -(* Constructors. *) - -let type_of_constructor env (c,u as cu) = - let () = - let ((kn,_),_) = c in - let mib = lookup_mind kn env in - check_hyps_inclusion env mkConstructU cu mib.mind_hyps - in - let specif = lookup_mind_specif env (inductive_of_constructor c) in - let t,cst = constrained_type_of_constructor cu specif in - let () = check_constraints cst env in - t - -(* Case. *) - -let check_branch_types env (ind,u) c ct lft explft = - try conv_leq_vecti env lft explft - with - NotConvertibleVect i -> - error_ill_formed_branch env c ((ind,i+1),u) lft.(i) explft.(i) - | Invalid_argument _ -> - error_number_branches env (make_judge c ct) (Array.length explft) - -let type_of_case env ci p pt c ct lf lft = - let (pind, _ as indspec) = - try find_rectype env ct - with Not_found -> error_case_not_inductive env (make_judge c ct) in - let () = check_case_info env pind ci in - let (bty,rslty) = - type_case_branches env indspec (make_judge p pt) c in - let () = check_branch_types env pind c ct lft bty in - rslty - -let type_of_projection env p c ct = - let pb = lookup_projection p env in - let (ind,u), args = - try find_rectype env ct - with Not_found -> error_case_not_inductive env (make_judge c ct) - in - assert(eq_mind pb.proj_ind (fst ind)); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in - substl (c :: List.rev args) ty - - -(* Fixpoints. *) - -(* Checks the type of a general (co)fixpoint, i.e. without checking *) -(* the specific guard condition. *) - -let check_fixpoint env lna lar vdef vdeft = - let lt = Array.length vdeft in - assert (Int.equal (Array.length lar) lt); - try - conv_leq_vecti env vdeft (Array.map (fun ty -> lift lt ty) lar) - with NotConvertibleVect i -> - error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar - -(************************************************************************) -(************************************************************************) - -(* The typing machine. *) - (* ATTENTION : faudra faire le typage du contexte des Const, - 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) -> - type1 - - | Sort (Type u) -> - type_of_type u - - | Rel n -> - type_of_relative env n - - | Var id -> - type_of_variable env id - - | Const c -> - type_of_constant env c - - | Proj (p, c) -> - let ct = execute env c in - type_of_projection env p c ct - - (* Lambda calculus operators *) - | App (f,args) -> - let argst = execute_array env args in - let ft = - match kind_of_term f with - | Ind ind when Environ.template_polymorphic_pind ind env -> - (* Template sort-polymorphism of inductive types *) - let args = Array.map (fun t -> lazy t) argst in - type_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_pconstant cst env -> - (* Template sort-polymorphism of constants *) - let args = Array.map (fun t -> lazy t) argst in - type_of_constant_knowing_parameters env cst args - | _ -> - (* Full or no sort-polymorphism *) - execute env f - in - - type_of_apply env f ft args argst - - | Lambda (name,c1,c2) -> - let _ = execute_is_type env c1 in - let env1 = push_rel (LocalAssum (name,c1)) env in - let c2t = execute env1 c2 in - type_of_abstraction env name c1 c2t - - | Prod (name,c1,c2) -> - let vars = execute_is_type env c1 in - let env1 = push_rel (LocalAssum (name,c1)) env in - let vars' = execute_is_type env1 c2 in - type_of_product env name vars vars' - - | LetIn (name,c1,c2,c3) -> - let c1t = execute env c1 in - let _c2s = execute_is_type env c2 in - let () = check_cast env c1 c1t DEFAULTcast c2 in - let env1 = push_rel (LocalDef (name,c1,c2)) env in - let c3t = execute env1 c3 in - subst1 c1 c3t - - | Cast (c,k,t) -> - let ct = execute env c in - let _ts = (check_type env t (execute env t)) in - let () = check_cast env c ct k t in - t - - (* Inductive types *) - | Ind ind -> - type_of_inductive env ind - - | Construct c -> - type_of_constructor env c - - | Case (ci,p,c,lf) -> - let ct = execute env c in - let pt = execute env p in - let lft = execute_array env lf in - type_of_case env ci p pt c ct lf lft - - | Fix ((vn,i as vni),recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in - let fix = (vni,recdef') in - check_fix env fix; fix_ty - - | CoFix (i,recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in - let cofix = (i,recdef') in - check_cofix env cofix; fix_ty - - (* Partial proofs: unsupported by the kernel *) - | Meta _ -> - anomaly (Pp.str "the kernel does not support metavariables") - - | Evar _ -> - anomaly (Pp.str "the kernel does not support existential variables") - -and execute_is_type env constr = - let t = execute env constr in - check_type env constr t - -and execute_recdef env (names,lar,vdef) i = - let lart = execute_array env lar in - let lara = Array.map2 (check_assumption env) lar lart in - let env1 = push_rec_types (names,lara,vdef) env in - let vdeft = execute_array env1 vdef in - let () = check_fixpoint env1 names lara vdef vdeft in - (lara.(i),(names,lara,vdef)) - -and execute_array env = Array.map (execute env) - -(* Derived functions *) -let infer env constr = - let t = execute env constr in - make_judge constr t - -let infer = - if Flags.profile then - let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile2 infer_key (fun b c -> infer b c) - else (fun b c -> infer b c) - -let assumption_of_judgment env {uj_val=c; uj_type=t} = - check_assumption env c t - -let type_judgment env {uj_val=c; uj_type=t} = - let s = check_type env c t in - {utj_val = c; utj_type = s } - -let infer_type env constr = - let t = execute env constr in - let s = check_type env constr t in - {utj_val = constr; utj_type = s} - -let infer_v env cv = - let jv = execute_array env cv in - make_judgev cv jv - -(* Typing of several terms. *) - -let infer_local_decl env id = function - | Entries.LocalDefEntry c -> - let t = execute env c in - RelDecl.LocalDef (Name id, c, t) - | Entries.LocalAssumEntry c -> - let t = execute env c in - RelDecl.LocalAssum (Name id, check_assumption env c t) - -let infer_local_decls env decls = - let rec inferec env = function - | (id, d) :: l -> - let (env, l) = inferec env l in - let d = infer_local_decl env id d in - (push_rel d env, Context.Rel.add d l) - | [] -> (env, Context.Rel.empty) - in - inferec env decls - -let judge_of_prop = make_judge mkProp type1 -let judge_of_set = make_judge mkSet type1 -let judge_of_type u = make_judge (mkType u) (type_of_type u) - -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set - -let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) - -let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) - -let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst) -let judge_of_constant_knowing_parameters env cst args = - make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args) - -let judge_of_projection env p cj = - make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type) - -let dest_judgev v = - Array.map j_val v, Array.map j_type v - -let judge_of_apply env funj argjv = - let args, argtys = dest_judgev argjv in - make_judge (mkApp (funj.uj_val, args)) (type_of_apply env funj.uj_val funj.uj_type args argtys) - -let judge_of_abstraction env x varj bodyj = - make_judge (mkLambda (x, varj.utj_val, bodyj.uj_val)) - (type_of_abstraction env x varj.utj_val bodyj.uj_type) - -let judge_of_product env x varj outj = - make_judge (mkProd (x, varj.utj_val, outj.utj_val)) - (mkSort (sort_of_product env varj.utj_type outj.utj_type)) - -let judge_of_letin env name defj typj j = - make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) - (subst1 defj.uj_val j.uj_type) - -let judge_of_cast env cj k tj = - let () = check_cast env cj.uj_val cj.uj_type k tj.utj_val in - let c = match k with | REVERTcast -> cj.uj_val | _ -> mkCast (cj.uj_val, k, tj.utj_val) in - make_judge c tj.utj_val - -let judge_of_inductive env indu = - make_judge (mkIndU indu) (type_of_inductive env indu) - -let judge_of_constructor env cu = - make_judge (mkConstructU cu) (type_of_constructor env cu) - -let judge_of_case env ci pj cj lfj = - let lf, lft = dest_judgev lfj in - make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) - (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) - -let type_of_projection_constant env (p,u) = - let cst = Projection.constant p in - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if cb.const_polymorphic then - Vars.subst_instance_constr u pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") - -(* Instantiation of terms on real arguments. *) - -(* Make a type polymorphic if an arity *) - -let extract_level env p = - let _,c = dest_prod_assum env p in - match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None - -let extract_context_levels env l = - let fold l = function - | RelDecl.LocalAssum (_,p) -> extract_level env p :: l - | RelDecl.LocalDef _ -> l - in - List.fold_left fold [] 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) -> - let ind, l = decompose_app (whd_all 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 diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli deleted file mode 100644 index 73c63db681..0000000000 --- a/kernel/fast_typeops.mli +++ /dev/null @@ -1,126 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr -> unsafe_judgment -val infer_v : env -> constr array -> unsafe_judgment array -val infer_type : env -> types -> unsafe_type_judgment - -val infer_local_decls : - env -> (Id.t * local_entry) list -> (env * Context.Rel.t) - -(** {6 Basic operations of the typing machine. } *) - -(** If [j] is the judgement {% $ %}c:t{% $ %}, then [assumption_of_judgement env j] - returns the type {% $ %}c{% $ %}, checking that {% $ %}t{% $ %} is a sort. *) - -val assumption_of_judgment : env -> unsafe_judgment -> types -val type_judgment : env -> unsafe_judgment -> unsafe_type_judgment - -(** {6 Type of sorts. } *) -val judge_of_prop : unsafe_judgment -val judge_of_set : unsafe_judgment -val judge_of_prop_contents : contents -> unsafe_judgment -val judge_of_type : universe -> unsafe_judgment - -(** {6 Type of a bound variable. } *) -val judge_of_relative : env -> int -> unsafe_judgment - -(** {6 Type of variables } *) -val judge_of_variable : env -> variable -> unsafe_judgment - -(** {6 type of a constant } *) - -val judge_of_constant : env -> pconstant -> unsafe_judgment - -val judge_of_constant_knowing_parameters : - env -> pconstant -> types Lazy.t array -> unsafe_judgment - -(** {6 type of an applied projection } *) - -val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment - -(** {6 Type of application. } *) -val judge_of_apply : - env -> unsafe_judgment -> unsafe_judgment array - -> unsafe_judgment - -(** {6 Type of an abstraction. } *) -val judge_of_abstraction : - env -> Name.t -> unsafe_type_judgment -> unsafe_judgment - -> unsafe_judgment - -val sort_of_product : env -> sorts -> sorts -> sorts - -(** {6 Type of a product. } *) -val judge_of_product : - env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment - -> unsafe_judgment - -(** s Type of a let in. *) -val judge_of_letin : - env -> Name.t -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment - -> unsafe_judgment - -(** {6 Type of a cast. } *) -val judge_of_cast : - env -> unsafe_judgment -> cast_kind -> unsafe_type_judgment -> - unsafe_judgment - -(** {6 Inductive types. } *) - -val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment - -(* val judge_of_inductive_knowing_parameters : *) -(* env -> inductive -> unsafe_judgment array -> unsafe_judgment *) - -val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment - -(** {6 Type of Cases. } *) -val judge_of_case : env -> case_info - -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array - -> unsafe_judgment - -(* val type_of_constant : env -> pconstant -> types constrained *) - -val type_of_constant_type : env -> constant_type -> types - -val type_of_projection_constant : env -> Names.projection puniverses -> types - -val type_of_constant_in : env -> pconstant -> types - -val type_of_constant_type_knowing_parameters : - env -> constant_type -> types Lazy.t array -> types - -(* val type_of_constant_knowing_parameters : *) -(* env -> pconstant -> types Lazy.t array -> types constrained *) - -val type_of_constant_knowing_parameters_in : - env -> pconstant -> types Lazy.t array -> types - -(** Make a type polymorphic if an arity *) -val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> - constant_type - -(** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 15f213ce9c..4c540a6d73 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -32,7 +32,6 @@ Type_errors Modops Inductive Typeops -Fast_typeops Indtypes Cooking Term_typing diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index d8774944e4..3a0d1a2a5e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -20,7 +20,6 @@ open Declarations open Environ open Entries open Typeops -open Fast_typeops module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 24018ab31a..7d9a2aac09 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -14,11 +14,9 @@ open Term open Vars open Declarations open Environ -open Entries open Reduction open Inductive open Type_errors -open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -38,61 +36,46 @@ 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) *) -let type_judgment env j = - match kind_of_term(whd_all env j.uj_type) with - | Sort s -> {utj_val = j.uj_val; utj_type = s } - | _ -> error_not_type env j +(* This should be a type (a priori without intention to be an assumption) *) +let check_type env c t = + match kind_of_term(whd_all env t) with + | Sort s -> s + | _ -> error_not_type env (make_judge c t) -(* This should be a type intended to be assumed. The error message is *) -(* not as useful as for [type_judgment]. *) -let assumption_of_judgment env j = - try (type_judgment env j).utj_val +(* This should be a type intended to be assumed. The error message is + not as useful as for [type_judgment]. *) +let check_assumption env t ty = + try let _ = check_type env t ty in t with TypeError _ -> - error_assumption env j + 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 *) (* Prop and Set *) -let judge_of_prop = - { uj_val = mkProp; - uj_type = mkSort type1_sort } - -let judge_of_set = - { uj_val = mkSet; - uj_type = mkSort type1_sort } - -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set +let type1 = mkSort type1_sort (* Type of Type(i). *) -let judge_of_type u = +let type_of_type u = let uu = Universe.super u in - { uj_val = mkType u; - uj_type = mkType uu } + mkType uu (*s Type of a de Bruijn index. *) -let judge_of_relative env n = +let type_of_relative env n = try - let typ = RelDecl.get_type (lookup_rel n env) in - { uj_val = mkRel n; - uj_type = lift n typ } + env |> lookup_rel n |> RelDecl.get_type |> lift n with Not_found -> error_unbound_rel env n (* Type of variables *) -let judge_of_variable env id = - try - let ty = named_type id env in - make_judge (mkVar id) ty +let type_of_variable env id = + try named_type id env with Not_found -> error_unbound_var env id @@ -101,7 +84,7 @@ let judge_of_variable env id = (* Checks if a context of variables can be instantiated by the 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 check_hyps_inclusion env f c sign = Context.Named.fold_outside (fun d1 () -> let open Context.Named.Declaration in @@ -117,7 +100,7 @@ let check_hyps_inclusion env c sign = | LocalDef _, LocalAssum _ -> raise NotConvertible | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1); with Not_found | NotConvertible | Option.Heterogeneous -> - error_reference_variables env id c) + error_reference_variables env id (f c)) sign ~init:() @@ -125,35 +108,9 @@ let check_hyps_inclusion env c sign = (* Make a type polymorphic if an arity *) -let extract_level env p = - let _,c = dest_prod_assum env p in - match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None - -let extract_context_levels env l = - let fold l = function - | LocalAssum (_,p) -> extract_level env p :: l - | LocalDef _ -> l - in - List.fold_left fold [] 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) -> - let ind, l = decompose_app (whd_all 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 - (* Type of constants *) + let type_of_constant_type_knowing_parameters env t paramtyps = match t with | RegularArity t -> t @@ -162,49 +119,28 @@ let type_of_constant_type_knowing_parameters env t paramtyps = let ctx,s = instantiate_universes env ctx ar paramtyps in mkArity (List.rev ctx,s) -let type_of_constant_knowing_parameters env cst paramtyps = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in +let type_of_constant_knowing_parameters env (kn,u as cst) args = + let cb = lookup_constant kn env in + let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty, cu = constant_type env cst in - type_of_constant_type_knowing_parameters env ty paramtyps, cu + let ty = type_of_constant_type_knowing_parameters env ty args in + let () = check_constraints cu env in + ty -let type_of_constant_knowing_parameters_in env cst paramtyps = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in +let type_of_constant_knowing_parameters_in env (kn,u as cst) args = + let cb = lookup_constant kn env in + let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty = constant_type_in env cst in - type_of_constant_type_knowing_parameters env ty paramtyps - -let type_of_constant_type env t = - type_of_constant_type_knowing_parameters env t [||] + type_of_constant_type_knowing_parameters env ty args let type_of_constant env cst = type_of_constant_knowing_parameters env cst [||] let type_of_constant_in env cst = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in - let ar = constant_type_in env cst in - type_of_constant_type_knowing_parameters env ar [||] - -let judge_of_constant_knowing_parameters env (kn,u as cst) args = - let c = mkConstU cst in - let ty, cu = type_of_constant_knowing_parameters env cst args in - let () = check_constraints cu env in - make_judge c ty - -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] - -let type_of_projection env (p,u) = - let cst = Projection.constant p in - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if cb.const_polymorphic then - Vars.subst_instance_constr u pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") + type_of_constant_knowing_parameters_in env cst [||] +let type_of_constant_type env t = + type_of_constant_type_knowing_parameters env t [||] (* Type of a lambda-abstraction. *) @@ -218,40 +154,36 @@ let type_of_projection env (p,u) = and no upper constraint exists on the sort $s$, we don't need to compute $s$ *) -let judge_of_abstraction env name var j = - { uj_val = mkLambda (name, var.utj_val, j.uj_val); - uj_type = mkProd (name, var.utj_val, j.uj_type) } - -(* Type of let-in. *) - -let judge_of_letin env name defj typj j = - { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ; - uj_type = subst1 defj.uj_val j.uj_type } +let type_of_abstraction env name var ty = + mkProd (name, var, ty) (* Type of an application. *) -let judge_of_apply env funj argjv = - let rec apply_rec n typ = function - | [] -> - { uj_val = mkApp (j_val funj, Array.map j_val argjv); - uj_type = typ } - | hj::restjl -> - (match kind_of_term (whd_all env typ) with - | Prod (_,c1,c2) -> - (try - let () = conv_leq false env hj.uj_type c1 in - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - with NotConvertible -> - error_cant_apply_bad_type env - (n,c1, hj.uj_type) - funj argjv) - - | _ -> - error_cant_apply_not_functional env funj argjv) - in - apply_rec 1 - funj.uj_type - (Array.to_list argjv) +let make_judgev c t = + Array.map2 make_judge c t + +let type_of_apply env func funt argsv argstv = + let len = Array.length argsv in + let rec apply_rec i typ = + if Int.equal i len then typ + else + (match kind_of_term (whd_all env typ) with + | Prod (_,c1,c2) -> + let arg = argsv.(i) and argt = argstv.(i) in + (try + let () = conv_leq false env argt c1 in + apply_rec (i+1) (subst1 arg c2) + with NotConvertible -> + error_cant_apply_bad_type env + (i+1,c1,argt) + (make_judge func funt) + (make_judgev argsv argstv)) + + | _ -> + error_cant_apply_not_functional env + (make_judge func funt) + (make_judgev argsv argstv)) + in apply_rec 0 funt (* Type of product *) @@ -284,10 +216,9 @@ let sort_of_product env domsort rangsort = where j.uj_type is convertible to a sort s2 *) -let judge_of_product env name t1 t2 = - let s = sort_of_product env t1.utj_type t2.utj_type in - { uj_val = mkProd (name, t1.utj_val, t2.utj_val); - uj_type = mkSort s } +let type_of_product env name s1 s2 = + let s = sort_of_product env s1 s2 in + mkSort s (* Type of a type cast *) @@ -298,29 +229,20 @@ let judge_of_product env name t1 t2 = env |- c:typ2 *) -let judge_of_cast env cj k tj = - let expected_type = tj.utj_val in +let check_cast env c ct k expected_type = try - let c, cst = - match k with - | VMcast -> - mkCast (cj.uj_val, k, 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 - | REVERTcast -> - cj.uj_val, - default_conv ~l2r:true CUMUL env cj.uj_type expected_type - | NATIVEcast -> - let sigma = Nativelambda.empty_evars in - mkCast (cj.uj_val, k, expected_type), - Nativeconv.native_conv CUMUL sigma env cj.uj_type expected_type - in - { uj_val = c; - uj_type = expected_type } + match k with + | VMcast -> + vm_conv CUMUL env ct expected_type + | DEFAULTcast -> + default_conv ~l2r:false CUMUL env ct expected_type + | REVERTcast -> + default_conv ~l2r:true CUMUL env ct expected_type + | NATIVEcast -> + let sigma = Nativelambda.empty_evars in + Nativeconv.native_conv CUMUL sigma env ct expected_type with NotConvertible -> - error_actual_type env cj expected_type + error_actual_type env (make_judge c ct) expected_type (* Inductive types. *) @@ -336,83 +258,78 @@ let judge_of_cast env cj k tj = the App case of execute; from this constraints, the expected dynamic constraints of the form u<=v are enforced *) -let judge_of_inductive_knowing_parameters env (ind,u as indu) args = - let c = mkIndU indu in +let type_of_inductive_knowing_parameters env (ind,u as indu) args = let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env c mib.mind_hyps; + check_hyps_inclusion env mkIndU indu mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters env (spec,u) args in - check_constraints cst env; - make_judge c t + check_constraints cst env; + t -let judge_of_inductive env (ind,u as indu) = - let c = mkIndU indu in - let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env c mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive env (spec,u) in - check_constraints cst env; - (make_judge c t) +let type_of_inductive env (ind,u as indu) = + let (mib,mip) = lookup_mind_specif env ind in + check_hyps_inclusion env mkIndU indu mib.mind_hyps; + let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in + check_constraints cst env; + t (* Constructors. *) -let judge_of_constructor env (c,u as cu) = - let constr = mkConstructU cu in - let _ = +let type_of_constructor env (c,u as cu) = + let () = let ((kn,_),_) = c in let mib = lookup_mind kn env in - check_hyps_inclusion env constr mib.mind_hyps in + check_hyps_inclusion env mkConstructU cu mib.mind_hyps + in let specif = lookup_mind_specif env (inductive_of_constructor c) in let t,cst = constrained_type_of_constructor cu specif in let () = check_constraints cst env in - (make_judge constr t) + t (* Case. *) -let check_branch_types env (ind,u) cj (lfj,explft) = - try conv_leq_vecti env (Array.map j_type lfj) explft +let check_branch_types env (ind,u) c ct lft explft = + try conv_leq_vecti env lft explft with NotConvertibleVect i -> - error_ill_formed_branch env cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i) + error_ill_formed_branch env c ((ind,i+1),u) lft.(i) explft.(i) | Invalid_argument _ -> - error_number_branches env cj (Array.length explft) + error_number_branches env (make_judge c ct) (Array.length explft) -let judge_of_case env ci pj cj lfj = +let type_of_case env ci p pt c ct lf lft = let (pind, _ as indspec) = - try find_rectype env cj.uj_type - with Not_found -> error_case_not_inductive env cj in + try find_rectype env ct + with Not_found -> error_case_not_inductive env (make_judge c ct) in let () = check_case_info env pind ci in let (bty,rslty) = - type_case_branches env indspec pj cj.uj_val in - let () = check_branch_types env pind cj (lfj,bty) in - ({ uj_val = mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, - Array.map j_val lfj); - uj_type = rslty }) + type_case_branches env indspec (make_judge p pt) c in + let () = check_branch_types env pind c ct lft bty in + rslty -let judge_of_projection env p cj = +let type_of_projection env p c ct = let pb = lookup_projection p env in let (ind,u), args = - try find_rectype env cj.uj_type - with Not_found -> error_case_not_inductive env cj + try find_rectype env ct + with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(eq_mind pb.proj_ind (fst ind)); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in - let ty = substl (cj.uj_val :: List.rev args) ty in - {uj_val = mkProj (p,cj.uj_val); - uj_type = ty} + assert(eq_mind pb.proj_ind (fst ind)); + let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in + substl (c :: List.rev args) ty + (* Fixpoints. *) (* Checks the type of a general (co)fixpoint, i.e. without checking *) (* the specific guard condition. *) -let type_fixpoint env lna lar vdefj = - let lt = Array.length vdefj in +let check_fixpoint env lna lar vdef vdeft = + let lt = Array.length vdeft in assert (Int.equal (Array.length lar) lt); try - conv_leq_vecti env (Array.map j_type vdefj) (Array.map (fun ty -> lift lt ty) lar) + conv_leq_vecti env vdeft (Array.map (fun ty -> lift lt ty) lar) with NotConvertibleVect i -> - error_ill_typed_rec_body env i lna vdefj lar + error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar (************************************************************************) (************************************************************************) @@ -422,95 +339,96 @@ 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) -> - judge_of_prop_contents c + type1 | Sort (Type u) -> - judge_of_type u + type_of_type u | Rel n -> - judge_of_relative env n + type_of_relative env n | Var id -> - judge_of_variable env id + type_of_variable env id | Const c -> - judge_of_constant env c + type_of_constant env c | Proj (p, c) -> - let cj = execute env c in - judge_of_projection env p cj + let ct = execute env c in + type_of_projection env p c ct (* Lambda calculus operators *) | App (f,args) -> - let jl = execute_array env args in - let j = + let argst = execute_array env args in + let ft = match kind_of_term f with - | Ind ind when Environ.template_polymorphic_pind ind env -> - (* Sort-polymorphism of inductive types *) - let args = Array.map (fun j -> lazy j.uj_type) jl in - judge_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_pconstant cst env -> - (* Sort-polymorphism of constant *) - let args = Array.map (fun j -> lazy j.uj_type) jl in - judge_of_constant_knowing_parameters env cst args - | _ -> - (* No sort-polymorphism *) - execute env f + | Ind ind when Environ.template_polymorphic_pind ind env -> + (* Template sort-polymorphism of inductive types *) + let args = Array.map (fun t -> lazy t) argst in + type_of_inductive_knowing_parameters env ind args + | Const cst when Environ.template_polymorphic_pconstant cst env -> + (* Template sort-polymorphism of constants *) + let args = Array.map (fun t -> lazy t) argst in + type_of_constant_knowing_parameters env cst args + | _ -> + (* Full or no sort-polymorphism *) + execute env f in - judge_of_apply env j jl + + type_of_apply env f ft args argst | Lambda (name,c1,c2) -> - let varj = execute_type env c1 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' + let _ = execute_is_type env c1 in + let env1 = push_rel (LocalAssum (name,c1)) env in + let c2t = execute env1 c2 in + type_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> - let varj = execute_type env c1 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' + let vars = execute_is_type env c1 in + let env1 = push_rel (LocalAssum (name,c1)) env in + let vars' = execute_is_type env1 c2 in + type_of_product env name vars vars' | LetIn (name,c1,c2,c3) -> - 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 (LocalDef (name,j1.uj_val,j2.utj_val)) env in - let j' = execute env1 c3 in - judge_of_letin env name j1 j2 j' + let c1t = execute env c1 in + let _c2s = execute_is_type env c2 in + let () = check_cast env c1 c1t DEFAULTcast c2 in + let env1 = push_rel (LocalDef (name,c1,c2)) env in + let c3t = execute env1 c3 in + subst1 c1 c3t | Cast (c,k,t) -> - let cj = execute env c in - let tj = execute_type env t in - judge_of_cast env cj k tj + let ct = execute env c in + let _ts = (check_type env t (execute env t)) in + let () = check_cast env c ct k t in + t (* Inductive types *) | Ind ind -> - judge_of_inductive env ind + type_of_inductive env ind | Construct c -> - judge_of_constructor env c + type_of_constructor env c | Case (ci,p,c,lf) -> - let cj = execute env c in - let pj = execute env p in - let lfj = execute_array env lf in - judge_of_case env ci pj cj lfj + let ct = execute env c in + let pt = execute env p in + let lft = execute_array env lf in + type_of_case env ci p pt c ct lf lft | Fix ((vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let fix = (vni,recdef') in - check_fix env fix; - make_judge (mkFix fix) fix_ty + check_fix env fix; fix_ty | CoFix (i,recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let cofix = (i,recdef') in - check_cofix env cofix; - (make_judge (mkCoFix cofix) fix_ty) + check_cofix env cofix; fix_ty (* Partial proofs: unsupported by the kernel *) | Meta _ -> @@ -519,53 +437,158 @@ let rec execute env cstr = | Evar _ -> anomaly (Pp.str "the kernel does not support existential variables") -and execute_type env constr = - let j = execute env constr in - type_judgment env j +and execute_is_type env constr = + let t = execute env constr in + check_type env constr t and execute_recdef env (names,lar,vdef) i = - let larj = execute_array env lar in - let lara = Array.map (assumption_of_judgment env) larj in + let lart = execute_array env lar in + let lara = Array.map2 (check_assumption env) lar lart in let env1 = push_rec_types (names,lara,vdef) env in - let vdefj = execute_array env1 vdef in - let vdefv = Array.map j_val vdefj in - let () = type_fixpoint env1 names lara vdefj in - (lara.(i),(names,lara,vdefv)) + let vdeft = execute_array env1 vdef in + let () = check_fixpoint env1 names lara vdef vdeft in + (lara.(i),(names,lara,vdef)) and execute_array env = Array.map (execute env) (* Derived functions *) let infer env constr = - let j = execute env constr in - assert (eq_constr j.uj_val constr); - j + let t = execute env constr in + make_judge constr t + +let infer = + if Flags.profile then + let infer_key = Profile.declare_profile "Fast_infer" in + Profile.profile2 infer_key (fun b c -> infer b c) + else (fun b c -> infer b c) + +let assumption_of_judgment env {uj_val=c; uj_type=t} = + check_assumption env c t -(* let infer_key = Profile.declare_profile "infer" *) -(* let infer = Profile.profile2 infer_key infer *) +let type_judgment env {uj_val=c; uj_type=t} = + let s = check_type env c t in + {utj_val = c; utj_type = s } let infer_type env constr = - let j = execute_type env constr in - j + let t = execute env constr in + let s = check_type env constr t in + {utj_val = constr; utj_type = s} let infer_v env cv = let jv = execute_array env cv in - jv + make_judgev cv jv (* Typing of several terms. *) let infer_local_decl env id = function - | LocalDefEntry c -> - let j = infer env c in - LocalDef (Name id, j.uj_val, j.uj_type) - | LocalAssumEntry c -> - let j = infer env c in - LocalAssum (Name id, assumption_of_judgment env j) + | Entries.LocalDefEntry c -> + let t = execute env c in + RelDecl.LocalDef (Name id, c, t) + | Entries.LocalAssumEntry c -> + let t = execute env c in + RelDecl.LocalAssum (Name id, check_assumption env c t) let infer_local_decls env decls = let rec inferec env = function | (id, d) :: l -> let (env, l) = inferec env l in let d = infer_local_decl env id d in - (push_rel d env, Context.Rel.add d l) - | [] -> (env, Context.Rel.empty) in + (push_rel d env, Context.Rel.add d l) + | [] -> (env, Context.Rel.empty) + in inferec env decls + +let judge_of_prop = make_judge mkProp type1 +let judge_of_set = make_judge mkSet type1 +let judge_of_type u = make_judge (mkType u) (type_of_type u) + +let judge_of_prop_contents = function + | Null -> judge_of_prop + | Pos -> judge_of_set + +let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) + +let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) + +let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst) +let judge_of_constant_knowing_parameters env cst args = + make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args) + +let judge_of_projection env p cj = + make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type) + +let dest_judgev v = + Array.map j_val v, Array.map j_type v + +let judge_of_apply env funj argjv = + let args, argtys = dest_judgev argjv in + make_judge (mkApp (funj.uj_val, args)) (type_of_apply env funj.uj_val funj.uj_type args argtys) + +let judge_of_abstraction env x varj bodyj = + make_judge (mkLambda (x, varj.utj_val, bodyj.uj_val)) + (type_of_abstraction env x varj.utj_val bodyj.uj_type) + +let judge_of_product env x varj outj = + make_judge (mkProd (x, varj.utj_val, outj.utj_val)) + (mkSort (sort_of_product env varj.utj_type outj.utj_type)) + +let judge_of_letin env name defj typj j = + make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) + (subst1 defj.uj_val j.uj_type) + +let judge_of_cast env cj k tj = + let () = check_cast env cj.uj_val cj.uj_type k tj.utj_val in + let c = match k with | REVERTcast -> cj.uj_val | _ -> mkCast (cj.uj_val, k, tj.utj_val) in + make_judge c tj.utj_val + +let judge_of_inductive env indu = + make_judge (mkIndU indu) (type_of_inductive env indu) + +let judge_of_constructor env cu = + make_judge (mkConstructU cu) (type_of_constructor env cu) + +let judge_of_case env ci pj cj lfj = + let lf, lft = dest_judgev lfj in + make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) + (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) + +let type_of_projection_constant env (p,u) = + let cst = Projection.constant p in + let cb = lookup_constant cst env in + match cb.const_proj with + | Some pb -> + if cb.const_polymorphic then + Vars.subst_instance_constr u pb.proj_type + else pb.proj_type + | None -> raise (Invalid_argument "type_of_projection: not a projection") + +(* Instantiation of terms on real arguments. *) + +(* Make a type polymorphic if an arity *) + +let extract_level env p = + let _,c = dest_prod_assum env p in + match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None + +let extract_context_levels env l = + let fold l = function + | RelDecl.LocalAssum (_,p) -> extract_level env p :: l + | RelDecl.LocalDef _ -> l + in + List.fold_left fold [] 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) -> + let ind, l = decompose_app (whd_all 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 diff --git a/kernel/typeops.mli b/kernel/typeops.mli index cfc82c1589..73c63db681 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -15,7 +15,7 @@ open Declarations (** {6 Typing functions (not yet tagged as safe) } - They return unsafe judgments that are "in context" of a set of + They return unsafe judgments that are "in context" of a set of (local) universe variables (the ones that appear in the term) and associated constraints. In case of polymorphic definitions, these variables and constraints will be generalized. @@ -101,15 +101,11 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -(** Typecheck general fixpoint (not checking guard conditions) *) -(* val type_fixpoint : env -> Name.t array -> types array *) -(* -> unsafe_judgment array -> unit *) - (* val type_of_constant : env -> pconstant -> types constrained *) val type_of_constant_type : env -> constant_type -> types -val type_of_projection : env -> Names.projection puniverses -> types +val type_of_projection_constant : env -> Names.projection puniverses -> types val type_of_constant_in : env -> pconstant -> types @@ -127,4 +123,4 @@ val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> constant_type (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> constr -> Context.Named.t -> unit +val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit -- cgit v1.2.3 From f5575393258492837d3764d07f8290b576f61160 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 22 Dec 2016 21:32:35 +0100 Subject: Fixing injection in the presence of let-in in constructors. This also fixes decide equality, discriminate, ... (see e.g. #5279). --- kernel/vars.ml | 9 +++++++++ kernel/vars.mli | 4 ++++ 2 files changed, 13 insertions(+) (limited to 'kernel') diff --git a/kernel/vars.ml b/kernel/vars.ml index b27e27fdac..4affb5f9fb 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -181,6 +181,15 @@ let subst_of_rel_context_instance sign l = let adjust_subst_to_rel_context sign l = List.rev (subst_of_rel_context_instance sign l) +let adjust_rel_to_rel_context sign n = + let rec aux sign = + let open RelDecl in + match sign with + | LocalAssum _ :: sign' -> let (n',p) = aux sign' in (n'+1,p) + | LocalDef (_,c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n' (0,n) + in snd (aux sign) + (* (thin_val sigma) removes identity substitutions from sigma *) let rec thin_val = function diff --git a/kernel/vars.mli b/kernel/vars.mli index 574d50eccb..f7535e6d8f 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -73,6 +73,10 @@ val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl (** For compatibility: returns the substitution reversed *) val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list +(** Take an index in an instance of a context and returns its index wrt to + the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *) +val adjust_rel_to_rel_context : Context.Rel.t -> int -> int + (** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an] for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates accordingly indexes in [an],...,[a1] and [c]. In terms of typing, if -- cgit v1.2.3 From 021f94d7dfef5630e48e79c9238db3a24b2aa221 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 23 Dec 2016 09:28:47 +0100 Subject: Handle application of a primitive projection to a not yet evaluated cofixpoint (bug #5286). --- kernel/byterun/coq_interp.c | 63 ++++++++++++++++++++++++++++++++++----------- 1 file changed, 48 insertions(+), 15 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 5dec3b785c..af89712d5e 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -891,25 +891,58 @@ value coq_interprete Instruct(PROJ){ + do_proj: print_instr("PROJ"); if (Is_accu (accu)) { - value block; - /* Skip over the index of projected field */ - pc++; - /* Create atom */ - Alloc_small(block, 2, ATOM_PROJ_TAG); - Field(block, 0) = Field(coq_global_data, *pc); - Field(block, 1) = accu; - accu = block; - /* Create accumulator */ - Alloc_small(block, 2, Accu_tag); - Code_val(block) = accumulate; - Field(block, 1) = accu; - accu = block; + *--sp = accu; // Save matched block on stack + accu = Field(accu, 1); // Save atom to accu register + switch (Tag_val(accu)) { + case ATOM_COFIX_TAG: // We are forcing a cofix + { + mlsize_t i, nargs; + sp -= 2; + // Push the current instruction as the return address + sp[0] = (value)(pc - 1); + sp[1] = coq_env; + coq_env = Field(accu, 0); // Pointer to suspension + accu = sp[2]; // Save accumulator to accu register + sp[2] = Val_long(coq_extra_args); // Push number of args for return + nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom) + // Push arguments to stack + CHECK_STACK(nargs + 1); + sp -= nargs; + for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 2); + *--sp = accu; // Last argument is the pointer to the suspension + coq_extra_args = nargs; + pc = Code_val(coq_env); // Trigger evaluation + goto check_stack; + } + case ATOM_COFIXEVALUATED_TAG: + { + accu = Field(accu, 1); + ++sp; + goto do_proj; + } + default: + { + value block; + /* Skip over the index of projected field */ + ++pc; + /* Create atom */ + Alloc_small(accu, 2, ATOM_PROJ_TAG); + Field(accu, 0) = Field(coq_global_data, *pc++); + Field(accu, 1) = *sp++; + /* Create accumulator */ + Alloc_small(block, 2, Accu_tag); + Code_val(block) = accumulate; + Field(block, 1) = accu; + accu = block; + } + } } else { - accu = Field(accu, *pc++); + accu = Field(accu, *pc); + pc += 2; } - pc++; Next; } -- cgit v1.2.3 From 63ca4aac83ced14b9b8065ef43e29f7c2dfd331c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 23 Dec 2016 09:28:47 +0100 Subject: Handle application of a primitive projection to a not yet evaluated cofixpoint (bug #5286). --- kernel/byterun/coq_interp.c | 63 ++++++++++++++++++++++++++++++++++----------- 1 file changed, 48 insertions(+), 15 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 35abd011bb..a67c27e87f 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -898,25 +898,58 @@ value coq_interprete Instruct(PROJ){ + do_proj: print_instr("PROJ"); if (Is_accu (accu)) { - value block; - /* Skip over the index of projected field */ - pc++; - /* Create atom */ - Alloc_small(block, 2, ATOM_PROJ_TAG); - Field(block, 0) = Field(coq_global_data, *pc); - Field(block, 1) = accu; - accu = block; - /* Create accumulator */ - Alloc_small(block, 2, Accu_tag); - Code_val(block) = accumulate; - Field(block, 1) = accu; - accu = block; + *--sp = accu; // Save matched block on stack + accu = Field(accu, 1); // Save atom to accu register + switch (Tag_val(accu)) { + case ATOM_COFIX_TAG: // We are forcing a cofix + { + mlsize_t i, nargs; + sp -= 2; + // Push the current instruction as the return address + sp[0] = (value)(pc - 1); + sp[1] = coq_env; + coq_env = Field(accu, 0); // Pointer to suspension + accu = sp[2]; // Save accumulator to accu register + sp[2] = Val_long(coq_extra_args); // Push number of args for return + nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom) + // Push arguments to stack + CHECK_STACK(nargs + 1); + sp -= nargs; + for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 2); + *--sp = accu; // Last argument is the pointer to the suspension + coq_extra_args = nargs; + pc = Code_val(coq_env); // Trigger evaluation + goto check_stack; + } + case ATOM_COFIXEVALUATED_TAG: + { + accu = Field(accu, 1); + ++sp; + goto do_proj; + } + default: + { + value block; + /* Skip over the index of projected field */ + ++pc; + /* Create atom */ + Alloc_small(accu, 2, ATOM_PROJ_TAG); + Field(accu, 0) = Field(coq_global_data, *pc++); + Field(accu, 1) = *sp++; + /* Create accumulator */ + Alloc_small(block, 2, Accu_tag); + Code_val(block) = accumulate; + Field(block, 1) = accu; + accu = block; + } + } } else { - accu = Field(accu, *pc++); + accu = Field(accu, *pc); + pc += 2; } - pc++; Next; } -- cgit v1.2.3 From 8d783c10d9505cbc1beb1c8e3451ea5dd567f260 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 Jan 2017 11:23:48 +0100 Subject: Mapping named_context_val preserves sharing when possible. This was deactivated by 27c9346 and made an optimization moot in eauto. This optimization was physically checking for equality, but as lists where rebuilt by the mapping, this was never true. Some contribs were thus quite slower, including persistent-union-find which was twice slower. This 2-line patch fixes it by trying to preserve sharing as much as possible. Note that we should still do something about eauto, because it does redo useless work a lot whenever the environment only changes a bit, while we could cache this computation. --- kernel/pre_env.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'kernel') diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 7be8606ef4..f211583e06 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -156,7 +156,8 @@ let map_named_val f ctxt = (accu, d') in let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in - { env_named_ctx = ctx; env_named_map = map } + if map == ctxt.env_named_map then ctxt + else { env_named_ctx = ctx; env_named_map = map } let push_named d env = (* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); -- cgit v1.2.3 From a9b76df171ceea443885bb4be919ea586a82beee Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 20 Jan 2017 10:55:17 +0100 Subject: Do not add redundant side effects in tactic code. This was observable in long proofs, because side effects kept being duplicated, leading to an additional cost linear in the size of the proof. This commit touches kernel files, but the corresponding API is only used in tactic-facing code so that the side_effects type remains opaque. Thus it does not affect the kernel safety. --- kernel/safe_typing.ml | 4 ++-- kernel/term_typing.mli | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 09f7bd75cd..95d9c75d30 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -213,8 +213,8 @@ type private_constant_role = Term_typing.side_effect_role = | Schema of inductive * string let empty_private_constants = [] -let add_private x xs = x :: xs -let concat_private xs ys = xs @ ys +let add_private x xs = if List.mem_f Term_typing.equal_eff x xs then xs else x :: xs +let concat_private xs ys = List.fold_right add_private xs ys let mk_pure_proof = Term_typing.mk_pure_proof let inline_private_constants_in_constr = Term_typing.inline_side_effects let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index fcd95576c0..89b5fc40e3 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -30,6 +30,7 @@ val inline_entry_side_effects : yet type checked proof. *) val uniq_seff : side_effects -> side_effects +val equal_eff : side_effect -> side_effect -> bool val translate_constant : structure_body -> env -> constant -> side_effects constant_entry -> -- cgit v1.2.3 From 86116b181bb866c7f63a37796e1388f731ce7204 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Jan 2017 11:38:19 +0100 Subject: [native comp] Improve error message on linking error. The native compiler doesn't support `Require` inside `Module` sections in some cases, we improve the error message. See: https://coq.inria.fr/bugs/show_bug.cgi?id=4335 This patch improves the error message and gives the user some feedback. --- kernel/safe_typing.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'kernel') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8b28cd87bd..7e28b1c567 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -795,7 +795,10 @@ type compiled_library = { type native_library = Nativecode.global list let get_library_native_symbols senv dir = - DPMap.find dir senv.native_symbols + try DPMap.find dir senv.native_symbols + with Not_found -> Errors.errorlabstrm "get_library_native_symbols" + Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++ + (str "This use case is not supported, but disabling the native compiler may help.")) (** FIXME: MS: remove?*) let current_modpath senv = senv.modpath -- cgit v1.2.3 From 90b6969c467f097a4d7da0140e1351ef98d6401d Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Sat, 28 Jan 2017 14:11:50 +0100 Subject: Remove useless comments --- kernel/typeops.mli | 8 -------- 1 file changed, 8 deletions(-) (limited to 'kernel') diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 73c63db681..007acae604 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -91,9 +91,6 @@ val judge_of_cast : val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment -(* val judge_of_inductive_knowing_parameters : *) -(* env -> inductive -> unsafe_judgment array -> unsafe_judgment *) - val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) @@ -101,8 +98,6 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -(* val type_of_constant : env -> pconstant -> types constrained *) - val type_of_constant_type : env -> constant_type -> types val type_of_projection_constant : env -> Names.projection puniverses -> types @@ -112,9 +107,6 @@ val type_of_constant_in : env -> pconstant -> types val type_of_constant_type_knowing_parameters : env -> constant_type -> types Lazy.t array -> types -(* val type_of_constant_knowing_parameters : *) -(* env -> pconstant -> types Lazy.t array -> types constrained *) - val type_of_constant_knowing_parameters_in : env -> pconstant -> types Lazy.t array -> types -- cgit v1.2.3