diff options
| -rw-r--r-- | kernel/cPrimitives.mli | 1 | ||||
| -rw-r--r-- | kernel/primred.ml | 77 | ||||
| -rw-r--r-- | kernel/primred.mli | 7 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 16 | ||||
| -rw-r--r-- | test-suite/arithmetic/primitive.v | 12 | ||||
| -rw-r--r-- | test-suite/success/primitive.v | 69 | ||||
| -rw-r--r-- | vernac/comPrimitive.ml | 8 | ||||
| -rw-r--r-- | vernac/himsg.ml | 25 |
8 files changed, 162 insertions, 53 deletions
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 5e5fad9f04..41b3bff465 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -128,6 +128,7 @@ val prim_ind_to_string : 'a prim_ind -> string (** Can raise [Not_found] *) val op_or_type_of_string : string -> op_or_type + val op_or_type_to_string : op_or_type -> string val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type diff --git a/kernel/primred.ml b/kernel/primred.ml index 10a8da8813..90eeeb9be7 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -5,62 +5,71 @@ open Retroknowledge open Environ open CErrors -let add_retroknowledge env action = +type _ action_kind = + | IncompatTypes : _ prim_type -> Constant.t action_kind + | IncompatInd : _ prim_ind -> inductive action_kind + +type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn + +let check_same_types typ c1 c2 = + if not (Constant.equal c1 c2) + then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2)) + +let check_same_inds ind i1 i2 = + if not (eq_ind i1 i2) + then raise (IncompatibleDeclarations (IncompatInd ind, i1, i2)) + +let add_retroknowledge retro action = match action with - | Register_type(PT_int63,c) -> - let retro = env.retroknowledge in - let retro = - match retro.retro_int63 with - | None -> { retro with retro_int63 = Some c } - | Some c' -> assert (Constant.equal c c'); retro in - set_retroknowledge env retro - | Register_type(PT_float64,c) -> - let retro = env.retroknowledge in - let retro = - match retro.retro_float64 with - | None -> { retro with retro_float64 = Some c } - | Some c' -> assert (Constant.equal c c'); retro in - set_retroknowledge env retro - | Register_type(PT_array,c) -> - let retro = env.retroknowledge in - let retro = - match retro.retro_array with - | None -> { retro with retro_array = Some c } - | Some c' -> assert (Constant.equal c c'); retro in - set_retroknowledge env retro + | Register_type(typ,c) -> + begin match typ with + | PT_int63 -> + (match retro.retro_int63 with + | None -> { retro with retro_int63 = Some c } + | Some c' -> check_same_types typ c c'; retro) + + | PT_float64 -> + (match retro.retro_float64 with + | None -> { retro with retro_float64 = Some c } + | Some c' -> check_same_types typ c c'; retro) + + | PT_array -> + (match retro.retro_array with + | None -> { retro with retro_array = Some c } + | Some c' -> check_same_types typ c c'; retro) + end + | Register_ind(pit,ind) -> - let retro = env.retroknowledge in - let retro = - match pit with + begin match pit with | PIT_bool -> let r = match retro.retro_bool with | None -> ((ind,1), (ind,2)) - | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in + | Some (((ind',_),_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_bool = Some r } | PIT_carry -> let r = match retro.retro_carry with | None -> ((ind,1), (ind,2)) - | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in + | Some (((ind',_),_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_carry = Some r } | PIT_pair -> let r = match retro.retro_pair with | None -> (ind,1) - | Some ((ind',_) as t) -> assert (eq_ind ind ind'); t in + | Some ((ind',_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_pair = Some r } | PIT_cmp -> let r = match retro.retro_cmp with | None -> ((ind,1), (ind,2), (ind,3)) - | Some (((ind',_),_,_) as t) -> assert (eq_ind ind ind'); t in + | Some (((ind',_),_,_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_cmp = Some r } | PIT_f_cmp -> let r = match retro.retro_f_cmp with | None -> ((ind,1), (ind,2), (ind,3), (ind,4)) - | Some (((ind',_),_,_,_) as t) -> assert (eq_ind ind ind'); t in + | Some (((ind',_),_,_,_) as t) -> check_same_inds pit ind ind'; t in { retro with retro_f_cmp = Some r } | PIT_f_class -> let r = @@ -69,10 +78,12 @@ let add_retroknowledge env action = (ind,5), (ind,6), (ind,7), (ind,8), (ind,9)) | Some (((ind',_),_,_,_,_,_,_,_,_) as t) -> - assert (eq_ind ind ind'); t in + check_same_inds pit ind ind'; t in { retro with retro_f_class = Some r } - in - set_retroknowledge env retro + end + +let add_retroknowledge env action = + set_retroknowledge env (add_retroknowledge env.retroknowledge action) let get_int_type env = match env.retroknowledge.retro_int63 with diff --git a/kernel/primred.mli b/kernel/primred.mli index 1bfaffaa44..6e9d4e297e 100644 --- a/kernel/primred.mli +++ b/kernel/primred.mli @@ -2,6 +2,13 @@ open Names open Environ (** {5 Reduction of primitives} *) +type _ action_kind = + | IncompatTypes : _ CPrimitives.prim_type -> Constant.t action_kind + | IncompatInd : _ CPrimitives.prim_ind -> inductive action_kind + +type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn + +(** May raise [IncomtibleDeclarations] *) val add_retroknowledge : env -> Retroknowledge.action -> env val get_int_type : env -> Constant.t diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 04e7a81697..48567aa564 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -88,7 +88,7 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } = univs, typ | Some (typ,Monomorphic_entry uctx) -> - assert (AUContext.is_empty auctx); + assert (AUContext.is_empty auctx); (* ensured by ComPrimitive *) let env = push_context_set ~strict:true uctx env in let u = Instance.empty in let typ = @@ -99,12 +99,14 @@ let infer_primitive env { prim_entry_type = utyp; prim_entry_content = p; } = Monomorphic uctx, typ | Some (typ,Polymorphic_entry (unames,uctx)) -> - assert (not (AUContext.is_empty auctx)); - (* push_context will check that the universes aren't repeated in the instance - so comparing the sizes works *) - assert (AUContext.size auctx = UContext.size uctx); - (* No polymorphic primitive uses constraints currently *) - assert (Constraint.is_empty (UContext.constraints uctx)); + assert (not (AUContext.is_empty auctx)); (* ensured by ComPrimitive *) + (* [push_context] will check that the universes aren't repeated in + the instance so comparing the sizes works. No polymorphic + primitive uses constraints currently. *) + if not (AUContext.size auctx = UContext.size uctx + && Constraint.is_empty (UContext.constraints uctx)) + then CErrors.user_err Pp.(str "Incorrect universes for primitive " ++ + str (op_or_type_to_string p)); let env = push_context ~strict:false uctx env in (* Now we know that uctx matches the auctx *) let typ = (Typeops.infer_type env typ).utj_val in diff --git a/test-suite/arithmetic/primitive.v b/test-suite/arithmetic/primitive.v deleted file mode 100644 index f62f6109e1..0000000000 --- a/test-suite/arithmetic/primitive.v +++ /dev/null @@ -1,12 +0,0 @@ -Section S. - Variable A : Type. - Fail Primitive int : let x := A in Set := #int63_type. - Fail Primitive add := #int63_add. -End S. - -(* [Primitive] should be forbidden in sections, otherwise its type after cooking -will be incorrect: - -Check int. - -*) diff --git a/test-suite/success/primitive.v b/test-suite/success/primitive.v new file mode 100644 index 0000000000..b2d02a0c49 --- /dev/null +++ b/test-suite/success/primitive.v @@ -0,0 +1,69 @@ +(* This file mostly tests for the error paths in declaring primitives. + Successes are tested in the various test-suite/primitive/* directories *) + +(* [Primitive] should be forbidden in sections, otherwise its type +after cooking will be incorrect. *) +Section S. + Variable A : Type. + Fail Primitive int : let x := A in Set := #int63_type. + Fail Primitive int := #int63_type. (* we fail even if section variable not used *) +End S. +Section S. + Fail Primitive int := #int63_type. (* we fail even if no section variables *) +End S. + +(* can't declare primitives with nonsense types *) +Fail Primitive xx : nat := #int63_type. + +(* non-cumulative conversion *) +Fail Primitive xx : Type := #int63_type. + +(* check evars *) +Fail Primitive xx : let x := _ in Set := #int63_type. + +(* explicit type is unified with expected type, not just converted + + extra universes are OK for monomorphic primitives (even though + their usefulness is questionable, there's no difference compared + with predeclaring them) + *) +Primitive xx : let x := Type in _ := #int63_type. + +(* double declaration *) +Fail Primitive yy := #int63_type. + +Module DoubleCarry. + (* XXX maybe should be an output test: this is the case where the new + declaration is already in the nametab so can be nicely printed *) + Module M. + Variant carry (A : Type) := + | C0 : A -> carry A + | C1 : A -> carry A. + + Register carry as kernel.ind_carry. + End M. + + Module N. + Variant carry (A : Type) := + | C0 : A -> carry A + | C1 : A -> carry A. + + Fail Register carry as kernel.ind_carry. + End N. +End DoubleCarry. + +(* univ polymorphic primitives *) + +(* universe count must be as expected *) +Fail Primitive array@{u v} : Type@{u} -> Type@{v} := #array_type. + +(* use a phantom universe to ensure we check conversion not just the universe count *) +Fail Primitive array@{u} : Set -> Set := #array_type. + +(* no constraints allowed! *) +Fail Primitive array@{u | Set < u} : Type@{u} -> Type@{u} := #array_type. + +(* unification works for polymorphic primitives too (although universe + counts mean it's not enough) *) +Fail Primitive array : let x := Type in _ -> Type := #array_type. +Primitive array : _ -> Type := #array_type. diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml index 110dcdc98a..eaa5271a73 100644 --- a/vernac/comPrimitive.ml +++ b/vernac/comPrimitive.ml @@ -38,7 +38,13 @@ let do_primitive id udecl prim typopt = Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env) env evd typ in - let evd = Evarconv.unify_delay env evd typ expected_typ in + let evd = try Evarconv.unify_delay env evd typ expected_typ + with Evarconv.UnableToUnify (evd,e) as exn -> + let _, info = Exninfo.capture exn in + Exninfo.iraise (Pretype_errors.( + PretypeError (env,evd,CannotUnify (typ,expected_typ,Some e)),info)) + in + Pretyping.check_evars_are_solved ~program_mode:false env evd; let evd = Evd.minimize_universes evd in let uvars = EConstr.universes_of_constr evd typ in let evd = Evd.restrict_universe_context evd uvars in diff --git a/vernac/himsg.ml b/vernac/himsg.ml index f9ecf10d1b..762c95fffe 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1252,6 +1252,29 @@ let explain_inductive_error = function error_large_non_prop_inductive_not_in_type () | MissingConstraints csts -> error_inductive_missing_constraints csts +(* Primitive errors *) + +let explain_incompatible_prim_declarations (type a) (act:a Primred.action_kind) (x:a) (y:a) = + let open Primred in + let env = Global.env() in + (* The newer constant/inductive (either coming from Primitive or a + Require) may be absent from the nametab as the error got raised + while adding it to the safe_env. In that case we can't use + nametab printing. + + There are still cases where the constant/inductive is added + separately from its retroknowledge (using Register), so we still + try nametab based printing. *) + match act with + | IncompatTypes typ -> + let px = try pr_constant env x with Not_found -> Constant.print x in + str "Cannot declare " ++ px ++ str " as primitive " ++ str (CPrimitives.prim_type_to_string typ) ++ + str ": " ++ pr_constant env y ++ str " is already declared." + | IncompatInd ind -> + let px = try pr_inductive env x with Not_found -> MutInd.print (fst x) in + str "Cannot declare " ++ px ++ str " as primitive " ++ str (CPrimitives.prim_ind_to_string ind) ++ + str ": " ++ pr_inductive env y ++ str " is already declared." + (* Recursion schemes errors *) let explain_recursion_scheme_error env = function @@ -1386,6 +1409,8 @@ let rec vernac_interp_error_handler = function explain_typeclass_error env sigma te | InductiveError e -> explain_inductive_error e + | Primred.IncompatibleDeclarations (act,x,y) -> + explain_incompatible_prim_declarations act x y | Modops.ModuleTypingError e -> explain_module_error e | Modintern.ModuleInternalizationError e -> |