diff options
| -rw-r--r-- | kernel/modops.ml | 62 | ||||
| -rw-r--r-- | kernel/modops.mli | 24 | ||||
| -rw-r--r-- | kernel/reduction.ml | 6 | ||||
| -rw-r--r-- | kernel/reduction.mli | 4 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 79 | ||||
| -rw-r--r-- | lib/util.ml | 9 | ||||
| -rw-r--r-- | lib/util.mli | 2 | ||||
| -rw-r--r-- | test-suite/modules/errors.v | 70 |
8 files changed, 214 insertions, 42 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 2bcfada96..302d25194 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -38,7 +38,67 @@ let error_incompatible_modtypes _ _ = error "Incompatible module types." let error_not_equal _ _ = error "Non equal modules." -let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match.") +type signature_mismatch_error = + | InductiveFieldExpected of mutual_inductive_body + | DefinitionFieldExpected + | ModuleFieldExpected + | ModuleTypeFieldExpected + | NotConvertibleInductiveField of identifier + | NotConvertibleConstructorField of identifier + | NotConvertibleBodyField + | NotConvertibleTypeField + | NotSameConstructorNamesField + | NotSameInductiveNameInBlockField + | FiniteInductiveFieldExpected of bool + | InductiveNumbersFieldExpected of int + | InductiveParamsNumberField of int + | RecordFieldExpected of bool + | RecordProjectionsExpected of name list + | NotEqualInductiveAliases + | NoTypeConstraintExpected + +let explain_not_match_error = function + | InductiveFieldExpected _ -> + strbrk "an inductive definition is expected" + | DefinitionFieldExpected -> + strbrk "a definition is expected" + | ModuleFieldExpected -> + strbrk "a module is expected" + | ModuleTypeFieldExpected -> + strbrk "a module type is expected" + | NotConvertibleInductiveField id | NotConvertibleConstructorField id -> + str "types given to " ++ str (string_of_id id) ++ str " differ" + | NotConvertibleBodyField -> + str "the body of definitions differs" + | NotConvertibleTypeField -> + str "types differ" + | NotSameConstructorNamesField -> + str "constructor names differ" + | NotSameInductiveNameInBlockField -> + str "inductive types names differ" + | FiniteInductiveFieldExpected isfinite -> + str "type is expected to be " ++ + str (if isfinite then "coinductive" else "inductive") + | InductiveNumbersFieldExpected n -> + str "number of inductive types differs" + | InductiveParamsNumberField n -> + str "inductive type has not the right number of parameters" + | RecordFieldExpected isrecord -> + str "type is expected " ++ str (if isrecord then "" else "not ") ++ + str "to be a record" + | RecordProjectionsExpected nal -> + (if List.length nal >= 2 then str "expected projection names are " + else str "expected projection name is ") ++ + pr_enum (function Name id -> str (string_of_id id) | _ -> str "_") nal + | NotEqualInductiveAliases -> + str "Aliases to inductive types do not match" + | NoTypeConstraintExpected -> + strbrk "a definition whose type is constrained can only be subtype of a definition whose type is itself constrained" + +let error_not_match l _ why = + errorlabstrm "" + (str "Signature components for label " ++ str (string_of_label l) ++ + str " do not match:" ++ spc () ++ explain_not_match_error why ++ str ".") let error_no_such_label l = error ("No such label "^string_of_label l^".") diff --git a/kernel/modops.mli b/kernel/modops.mli index f34fa88c4..cf8d62043 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -51,6 +51,27 @@ val subst_modtype_and_resolver : module_type_body -> module_path -> env -> val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body +(** Errors *) + +type signature_mismatch_error = + | InductiveFieldExpected of mutual_inductive_body + | DefinitionFieldExpected + | ModuleFieldExpected + | ModuleTypeFieldExpected + | NotConvertibleInductiveField of identifier + | NotConvertibleConstructorField of identifier + | NotConvertibleBodyField + | NotConvertibleTypeField + | NotSameConstructorNamesField + | NotSameInductiveNameInBlockField + | FiniteInductiveFieldExpected of bool + | InductiveNumbersFieldExpected of int + | InductiveParamsNumberField of int + | RecordFieldExpected of bool + | RecordProjectionsExpected of name list + | NotEqualInductiveAliases + | NoTypeConstraintExpected + val error_existing_label : label -> 'a val error_declaration_not_path : module_struct_entry -> 'a @@ -64,7 +85,8 @@ val error_incompatible_modtypes : val error_not_equal : module_path -> module_path -> 'a -val error_not_match : label -> structure_field_body -> 'a +val error_not_match : + label -> structure_field_body -> signature_mismatch_error -> 'a val error_incompatible_labels : label -> label -> 'a diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c865c92bf..8252ffb9e 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -534,15 +534,17 @@ let dest_prod_assum env = in prodec_rec env empty_rel_context +exception NotArity + let dest_arity env c = let l, c = dest_prod_assum env c in match kind_of_term c with | Sort s -> l,s - | _ -> error "not an arity" + | _ -> raise NotArity let is_arity env c = try let _ = dest_arity env c in true - with UserError _ -> false + with NotArity -> false diff --git a/kernel/reduction.mli b/kernel/reduction.mli index e0f9c375b..525651493 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -76,5 +76,7 @@ val hnf_prod_applist : env -> types -> constr list -> types val dest_prod : env -> types -> rel_context * types val dest_prod_assum : env -> types -> rel_context * types -val dest_arity : env -> types -> arity +exception NotArity + +val dest_arity : env -> types -> arity (* raise NotArity if not an arity *) val is_arity : env -> types -> bool diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 2612afca6..808557521 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -67,26 +67,26 @@ let make_label_map mp list = in List.fold_right add_one list Labmap.empty -let check_conv_error error cst f env a1 a2 = +let check_conv_error error why cst f env a1 a2 = try union_constraints cst (f env a1 a2) with - NotConvertible -> error () + NotConvertible -> error why (* for now we do not allow reorderings *) let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= let kn1 = make_mind mp1 empty_dirpath l in let kn2 = make_mind mp2 empty_dirpath l in - let error () = error_not_match l spec2 in - let check_conv cst f = check_conv_error error cst f in + let error why = error_not_match l spec2 why in + let check_conv why cst f = check_conv_error error why cst f in let mib1 = match info1 with | IndType ((_,0), mib) -> subst_mind subst1 mib - | _ -> error () + | _ -> error (InductiveFieldExpected mib2) in let mib2 = subst_mind subst2 mib2 in - let check_inductive_type cst env t1 t2 = + let check_inductive_type cst name env t1 t2 = (* Due to sort-polymorphism in inductive types, the conclusions of t1 and t2, if in Type, are generated as the least upper bounds @@ -115,40 +115,43 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let s1,s2 = match s1, s2 with | Type _, Type _ -> (* shortcut here *) prop_sort, prop_sort - | (Prop _, Type _) | (Type _,Prop _) -> error () + | (Prop _, Type _) | (Type _,Prop _) -> + error (NotConvertibleInductiveField name) | _ -> (s1, s2) in - check_conv cst conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) + check_conv (NotConvertibleInductiveField name) + cst conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) in let check_packet cst p1 p2 = - let check f = if f p1 <> f p2 then error () in - check (fun p -> p.mind_consnames); - check (fun p -> p.mind_typename); + let check f why = if f p1 <> f p2 then error why in + check (fun p -> p.mind_consnames) NotSameConstructorNamesField; + check (fun p -> p.mind_typename) NotSameInductiveNameInBlockField; (* nf_lc later *) (* nf_arity later *) (* user_lc ignored *) (* user_arity ignored *) - check (fun p -> p.mind_nrealargs); + check (fun p -> p.mind_nrealargs) (NotConvertibleInductiveField p2.mind_typename); (* How can it fail since the type of inductive are checked below? [HH] *) (* kelim ignored *) (* listrec ignored *) (* finite done *) (* nparams done *) (* params_ctxt done because part of the inductive types *) (* Don't check the sort of the type if polymorphic *) - let cst = check_inductive_type cst env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2)) + let cst = check_inductive_type cst p2.mind_typename env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2)) in cst in let check_cons_types i cst p1 p2 = - array_fold_left2 - (fun cst t1 t2 -> check_conv cst conv env t1 t2) + array_fold_left3 + (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst conv env t1 t2) cst + p2.mind_consnames (arities_of_specif kn1 (mib1,p1)) (arities_of_specif kn1 (mib2,p2)) in - let check f = if f mib1 <> f mib2 then error () in - check (fun mib -> mib.mind_finite); - check (fun mib -> mib.mind_ntypes); + let check f why = if f mib1 <> f mib2 then error (why (f mib2)) in + check (fun mib -> mib.mind_finite) (fun x -> FiniteInductiveFieldExpected x); + check (fun mib -> mib.mind_ntypes) (fun x -> InductiveNumbersFieldExpected x); assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]); assert (Array.length mib1.mind_packets >= 1 && Array.length mib2.mind_packets >= 1); @@ -158,17 +161,17 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (* at the time of checking the inductive arities in check_packet. *) (* Notice that we don't expect the local definitions to match: only *) (* the inductive types and constructors types have to be convertible *) - check (fun mib -> mib.mind_nparams); + check (fun mib -> mib.mind_nparams) (fun x -> InductiveParamsNumberField x); begin match mind_of_delta reso2 kn2 with | kn2' when kn2=kn2' -> () | kn2' -> if not (eq_mind (mind_of_delta reso1 kn1) (subst_ind subst2 kn2')) then - error () + error NotEqualInductiveAliases end; (* we check that records and their field names are preserved. *) - check (fun mib -> mib.mind_record); + check (fun mib -> mib.mind_record) (fun x -> RecordFieldExpected x); if mib1.mind_record then begin let rec names_prod_letin t = match kind_of_term t with | Prod(n,_,t) -> n::(names_prod_letin t) @@ -183,7 +186,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 check (fun mib -> let nparamdecls = List.length mib.mind_params_ctxt in let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in - snd (list_chop nparamdecls names)); + snd (list_chop nparamdecls names)) + (fun x -> RecordProjectionsExpected x); end; (* we first check simple things *) let cst = @@ -197,7 +201,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = - let error () = error_not_match l spec2 in + let error why = error_not_match l spec2 why in let check_conv cst f = check_conv_error error cst f in let check_type cst env t1 t2 = @@ -237,13 +241,14 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = constraints of the form "univ <= max(...)" are not expressible in the system of algebraic universes: we fail (the user has to use an explicit type in the interface *) - error () - with UserError _ (* "not an arity" *) -> - error () end - | _ -> t1,t2 + error NoTypeConstraintExpected + with NotArity -> + error NotConvertibleTypeField end + | _ -> + t1,t2 else (t1,t2) in - check_conv cst conv_leq env t1 t2 + check_conv NotConvertibleTypeField cst conv_leq env t1 t2 in match info1 with @@ -284,7 +289,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = end | None -> mkConst con in - check_conv cst conv env c1 c2 + check_conv NotConvertibleBodyField cst conv env c1 c2 else match cb2.const_body with | None -> cst @@ -294,7 +299,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = | Some lc1 -> Declarations.force lc1 | None -> mkConst con in - check_conv cst conv env c1 c2 + check_conv NotConvertibleBodyField cst conv env c1 c2 in cst | IndType ((kn,i),mind1) -> @@ -304,10 +309,10 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = "inductive type and give a definition to map the old name to the new " ^ "name.")); assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; - if cb2.const_body <> None then error () ; + if cb2.const_body <> None then error DefinitionFieldExpected; let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in let typ2 = Typeops.type_of_constant_type env cb2.const_type in - check_conv cst conv_leq env arity1 typ2 + check_conv NotConvertibleTypeField cst conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> ignore (Util.error ( "The kernel does not recognize yet that a parameter can be " ^ @@ -315,11 +320,11 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = "constructor and give a definition to map the old name to the new " ^ "name.")); assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; - if cb2.const_body <> None then error () ; + if cb2.const_body <> None then error DefinitionFieldExpected; let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in let ty2 = Typeops.type_of_constant_type env cb2.const_type in - check_conv cst conv env ty1 ty2 - | _ -> error () + check_conv NotConvertibleTypeField cst conv env ty1 ty2 + | _ -> error DefinitionFieldExpected let rec check_modules cst env msb1 msb2 subst1 subst2 = let mty1 = module_type_of_module env None msb1 in @@ -348,13 +353,13 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= match info1 with | Module msb -> check_modules cst env msb msb2 subst1 subst2 - | _ -> error_not_match l spec2 + | _ -> error_not_match l spec2 ModuleFieldExpected end | SFBmodtype mtb2 -> let mtb1 = match info1 with | Modtype mtb -> mtb - | _ -> error_not_match l spec2 + | _ -> error_not_match l spec2 ModuleTypeFieldExpected in let env = add_module (module_body_of_type mtb2.typ_mp mtb2) (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in diff --git a/lib/util.ml b/lib/util.ml index a8e716e0f..242c20321 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -1000,6 +1000,15 @@ let array_fold_left2_i f a v1 v2 = if Array.length v2 <> lv1 then invalid_arg "array_fold_left2"; fold a 0 +let array_fold_left3 f a v1 v2 v3 = + let lv1 = Array.length v1 in + let rec fold a n = + if n >= lv1 then a else fold (f a v1.(n) v2.(n) v3.(n)) (succ n) + in + if Array.length v2 <> lv1 || Array.length v3 <> lv1 then + invalid_arg "array_fold_left2"; + fold a 0 + let array_fold_left_from n f a v = let rec fold a n = if n >= Array.length v then a else fold (f a v.(n)) (succ n) diff --git a/lib/util.mli b/lib/util.mli index 5248d0e6b..2216ba981 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -259,6 +259,8 @@ val array_fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c val array_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a +val array_fold_left3 : + ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a val array_fold_left2_i : (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val array_fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a diff --git a/test-suite/modules/errors.v b/test-suite/modules/errors.v new file mode 100644 index 000000000..d1658786e --- /dev/null +++ b/test-suite/modules/errors.v @@ -0,0 +1,70 @@ +(* Inductive mismatches *) + +Module Type SA. Inductive TA : nat -> Prop := CA : nat -> TA 0. End SA. +Module MA : SA. Inductive TA : Prop := CA : bool -> TA. Fail End MA. + +Module Type SA. Inductive TA := CA : nat -> TA. End SA. +Module MA : SA. Inductive TA := CA : bool -> TA. Fail End MA. + +Module Type SA. Inductive TA := CA : nat -> TA. End SA. +Module MA : SA. Inductive TA := CA : bool -> nat -> TA. Fail End MA. + +Module Type SA2. Inductive TA2 := CA2 : nat -> TA2. End SA2. +Module MA2 : SA2. Inductive TA2 := CA2 : nat -> TA2 | DA2 : TA2. Fail End MA2. + +Module Type SA3. Inductive TA3 := CA3 : nat -> TA3. End SA3. +Module MA3 : SA3. Inductive TA3 := CA3 : nat -> TA3 with UA3 := DA3. Fail End MA3. + +Module Type SA4. Inductive TA4 := CA4 : nat -> TA4 with UA4 := DA4. End SA4. +Module MA4 : SA4. Inductive TA4 := CA4 : nat -> TA4 with VA4 := DA4. Fail End MA4. + +Module Type SA5. Inductive TA5 := CA5 : nat -> TA5 with UA5 := DA5. End SA5. +Module MA5 : SA5. Inductive TA5 := CA5 : nat -> TA5 with UA5 := EA5. Fail End MA5. + +Module Type SA6. Inductive TA6 (A:Type) := CA6 : A -> TA6 A. End SA6. +Module MA6 : SA6. Inductive TA6 (A B:Type):= CA6 : A -> TA6 A B. Fail End MA6. + +Module Type SA7. Inductive TA7 (A:Type) := CA7 : A -> TA7 A. End SA7. +Module MA7 : SA7. CoInductive TA7 (A:Type):= CA7 : A -> TA7 A. Fail End MA7. + +Module Type SA8. CoInductive TA8 (A:Type) := CA8 : A -> TA8 A. End SA8. +Module MA8 : SA8. Inductive TA8 (A:Type):= CA8 : A -> TA8 A. Fail End MA8. + +Module Type SA9. Record TA9 (A:Type) := { CA9 : A }. End SA9. +Module MA9 : SA9. Inductive TA9 (A:Type):= CA9 : A -> TA9 A. Fail End MA9. + +Module Type SA10. Inductive TA10 (A:Type) := CA10 : A -> TA10 A. End SA10. +Module MA10 : SA10. Record TA10 (A:Type):= { CA10 : A }. Fail End MA10. + +Module Type SA11. Record TA11 (A:Type):= { CA11 : A }. End SA11. +Module MA11 : SA11. Record TA11 (A:Type):= { DA11 : A }. Fail End MA11. + +(* Basic mismatches *) +Module Type SB. Inductive TB := CB : nat -> TB. End SB. +Module MB : SB. Module Type TB. End TB. Fail End MB. + +Module Type SC. Module Type TC. End TC. End SC. +Module MC : SC. Inductive TC := CC : nat -> TC. Fail End MC. + +Module Type SD. Module TD. End TD. End SD. +Module MD : SD. Inductive TD := DD : nat -> TD. Fail End MD. + +Module Type SE. Definition DE := nat. End SE. +Module ME : SE. Definition DE := bool. Fail End ME. + +Module Type SF. Parameter DF : nat. End SF. +Module MF : SF. Definition DF := bool. Fail End MF. + +(* Needs a type constraint in module type *) +Module Type SG. Definition DG := Type. End SG. +Module MG : SG. Definition DG := Type : Type. Fail End MG. + +(* Should work *) +Module Type SA7. Inductive TA7 (A:Type) := CA7 : A -> TA7 A. End SA7. +Module MA7 : SA7. Inductive TA7 (B:Type):= CA7 : B -> TA7 B. End MA7. + +Module Type SA11. Record TA11 (B:Type):= { CA11 : B }. End SA11. +Module MA11 : SA11. Record TA11 (A:Type):= { CA11 : A }. End MA11. + +Module Type SE. Parameter DE : Type. End SE. +Module ME : SE. Definition DE := Type : Type. End ME. |