diff options
-rw-r--r-- | kernel/closure.ml | 4 | ||||
-rw-r--r-- | kernel/cooking.ml | 7 | ||||
-rw-r--r-- | kernel/declarations.ml | 8 | ||||
-rw-r--r-- | kernel/declarations.mli | 2 | ||||
-rw-r--r-- | kernel/indtypes.ml | 88 | ||||
-rw-r--r-- | kernel/inductive.ml | 46 | ||||
-rw-r--r-- | kernel/mod_subst.ml | 2 | ||||
-rw-r--r-- | kernel/mod_typing.ml | 24 | ||||
-rw-r--r-- | kernel/names.ml | 6 | ||||
-rw-r--r-- | kernel/names.mli | 6 | ||||
-rw-r--r-- | kernel/reduction.ml | 14 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 35 | ||||
-rw-r--r-- | kernel/subtyping.ml | 30 | ||||
-rw-r--r-- | kernel/term.ml | 2 | ||||
-rw-r--r-- | kernel/typeops.ml | 17 | ||||
-rw-r--r-- | kernel/univ.ml | 27 |
16 files changed, 192 insertions, 126 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 1c9b2145d..14b2a3a6e 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -692,7 +692,7 @@ let fapp_stack (m,stk) = zip m stk (* optimised for the case where there are no shifts... *) let strip_update_shift_app head stk = - assert (head.norm <> Red); + assert (match head.norm with Red -> false | _ -> true); let rec strip_rec rstk h depth = function | Zshift(k) as e :: s -> strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s @@ -706,7 +706,7 @@ let strip_update_shift_app head stk = let get_nth_arg head n stk = - assert (head.norm <> Red); + assert (match head.norm with Red -> false | _ -> true); let rec strip_rec rstk h n = function | Zshift(k) as e :: s -> strip_rec (e::rstk) (lift_fconstr k h) n s diff --git a/kernel/cooking.ml b/kernel/cooking.ml index f016a20b7..99b582fe3 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -75,6 +75,9 @@ let update_case_info ci modlist = let empty_modlist = (Cmap.empty, Mindmap.empty) +let is_empty_modlist (cm, mm) = + Cmap.is_empty cm && Mindmap.is_empty mm + let expmod_constr modlist c = let rec substrec c = match kind_of_term c with @@ -102,7 +105,7 @@ let expmod_constr modlist c = | _ -> map_constr substrec c in - if modlist = empty_modlist then c + if is_empty_modlist modlist then c else substrec c let abstract_constant_type = @@ -136,7 +139,7 @@ let cook_constant env r = in let const_hyps = Sign.fold_named_context (fun (h,_,_) hyps -> - List.filter (fun (id,_,_) -> id <> h) hyps) + List.filter (fun (id,_,_) -> not (id_eq id h)) hyps) hyps ~init:cb.const_hyps in let typ = match cb.const_type with | NonPolymorphicType t -> diff --git a/kernel/declarations.ml b/kernel/declarations.ml index b995f2e4a..3e5b10f3b 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -180,6 +180,12 @@ type recarg = | Mrec of inductive | Imbr of inductive +let eq_recarg r1 r2 = match r1, r2 with +| Norec, Norec -> true +| Mrec i1, Mrec i2 -> eq_ind i1 i2 +| Imbr i1, Imbr i2 -> eq_ind i1 i2 +| _ -> false + let subst_recarg sub r = match r with | Norec -> r | Mrec (kn,i) -> let kn' = subst_ind sub kn in @@ -204,7 +210,7 @@ let dest_recarg p = fst (Rtree.dest_node p) *) let dest_subterms p = let (ra,cstrs) = Rtree.dest_node p in - assert (ra<>Norec); + assert (match ra with Norec -> false | _ -> true); Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs let recarg_length p j = diff --git a/kernel/declarations.mli b/kernel/declarations.mli index a298d56ae..0a09ad76f 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -89,6 +89,8 @@ type recarg = | Mrec of inductive | Imbr of inductive +val eq_recarg : recarg -> recarg -> bool + val subst_recarg : substitution -> recarg -> recarg type wf_paths = recarg Rtree.t diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 6b993604d..042961879 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -90,7 +90,7 @@ let mind_check_names mie = (* Typing the arities and constructor types *) -let is_logic_type t = (t.utj_type = prop_sort) +let is_logic_type t = is_prop_sort t.utj_type (* [infos] is a sequence of pair [islogic,issmall] for each type in the product of a constructor or arity *) @@ -179,7 +179,10 @@ let infer_constructor_packet env_ar_par params lc = (* Type-check an inductive definition. Does not check positivity conditions. *) let typecheck_inductive env mie = - if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration"; + let () = match mie.mind_entry_inds with + | [] -> anomaly "empty inductive types declaration" + | _ -> () + in (* Check unicity of names *) mind_check_names mie; (* Params are typed-checked here *) @@ -233,22 +236,25 @@ let typecheck_inductive env mie = let inds = Array.of_list inds in let arities = Array.of_list arity_list in - let param_ccls = List.fold_left (fun l (_,b,p) -> - if b = None then - (* Parameter contributes to polymorphism only if explicit Type *) - let c = strip_prod_assum p in - (* Add Type levels to the ordered list of parameters contributing to *) - (* polymorphism unless there is aliasing (i.e. non distinct levels) *) - match kind_of_term c with - | Sort (Type u) -> - if List.mem (Some u) l then - None :: List.map (function Some v when u = v -> None | x -> x) l - else - Some u :: l - | _ -> - None :: l - else - l) [] params in + let fold l (_, b, p) = match b with + | None -> + (* Parameter contributes to polymorphism only if explicit Type *) + let c = strip_prod_assum p in + (* Add Type levels to the ordered list of parameters contributing to *) + (* polymorphism unless there is aliasing (i.e. non distinct levels) *) + begin match kind_of_term c with + | Sort (Type u) -> + if List.mem (Some u) l then + (** FIXME *) + None :: List.map (function Some v when Pervasives.(=) u v -> None | x -> x) l + else + Some u :: l + | _ -> + None :: l + end + | _ -> l + in + let param_ccls = List.fold_left fold [] params in (* Compute/check the sorts of the inductive types *) let ind_min_levels = inductive_levels arities inds in @@ -256,7 +262,7 @@ let typecheck_inductive env mie = Array.fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst -> let sign, s = dest_arity env full_arity in let status,cst = match s with - | Type u when ar_level <> None (* Explicitly polymorphic *) + | Type u when ar_level != None (* Explicitly polymorphic *) && no_upper_constraints u cst -> (* The polymorphic level is a function of the level of the *) (* conclusions of the parameters *) @@ -265,7 +271,11 @@ let typecheck_inductive env mie = Inr (param_ccls, lev), enforce_leq lev u cst | Type u (* Not an explicit occurrence of Type *) -> Inl (info,full_arity,s), enforce_leq lev u cst - | Prop Pos when engagement env <> Some ImpredicativeSet -> + | Prop Pos when + begin match engagement env with + | Some ImpredicativeSet -> false + | _ -> true + end -> (* Predicative set: check that the content is indeed predicative *) if not (is_type0m_univ lev) & not (is_type0_univ lev) then raise (InductiveError LargeNonPropInductiveNotInType); @@ -337,7 +347,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = | (_,Some _,_)::hyps -> check k (index+1) hyps | _::hyps -> match kind_of_term (whd_betadeltaiota env lpar.(k)) with - | Rel w when w = index -> check (k-1) (index+1) hyps + | Rel w when Int.equal w index -> check (k-1) (index+1) hyps | _ -> raise (IllFormedInd (LocalNonPar (k+1,l))) in check (nparams-1) (n-nhyps) hyps; if not (Array.for_all (noccur_between n ntypes) largs') then @@ -359,7 +369,7 @@ if Int.equal nmr 0 then 0 else | (lp,(_,Some _,_)::hyps) -> find k (index-1) (lp,hyps) | (p::lp,_::hyps) -> ( match kind_of_term (whd_betadeltaiota env p) with - | Rel w when w = index -> find (k+1) (index-1) (lp,hyps) + | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,hyps) | _ -> k) in find 0 (n-1) (lpar,List.rev hyps) @@ -403,7 +413,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = (env', newidx, ntypes, ra_env') let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = - if n=0 then (ienv,c) else + if Int.equal n 0 then (ienv,c) else let c' = whd_betadeltaiota env c in match kind_of_term c' with Prod(na,a,b) -> @@ -424,7 +434,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname let x,largs = decompose_app (whd_betadeltaiota env c) in match kind_of_term x with | Prod (na,b,d) -> - assert (largs = []); + let () = assert (List.is_empty largs) in (match weaker_noccur_between env n ntypes b with None -> failwith_non_pos_list n ntypes [b] | Some b -> @@ -466,7 +476,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname failwith_non_pos_list n ntypes auxlargs; (* We do not deal with imbricated mutual inductive types *) let auxntyp = mib.mind_ntypes in - if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n)); + if not (Int.equal auxntyp 1) then raise (IllFormedInd (LocalNonPos n)); (* The nested inductive type with parameters removed *) let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in (* Extends the environment with a variable corresponding to @@ -500,21 +510,23 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname match kind_of_term x with | Prod (na,b,d) -> - assert (largs = []); + let () = assert (List.is_empty largs) in let nmr',recarg = check_pos ienv nmr b in let ienv' = ienv_push_var ienv (na,b,mk_norec) in - check_constr_rec ienv' nmr' (recarg::lrec) d - - | hd -> - if check_head then - if hd = Rel (n+ntypes-i-1) then - check_correct_par ienv hyps (ntypes-i) largs - else - raise (IllFormedInd LocalNotConstructor) - else - if not (List.for_all (noccur_between n ntypes) largs) - then failwith_non_pos_list n ntypes largs; - (nmr,List.rev lrec) + check_constr_rec ienv' nmr' (recarg::lrec) d + | hd -> + let () = + if check_head then + begin match hd with + | Rel j when Int.equal j (n + ntypes - i - 1) -> + check_correct_par ienv hyps (ntypes - i) largs + | _ -> raise (IllFormedInd LocalNotConstructor) + end + else + if not (List.for_all (noccur_between n ntypes) largs) + then failwith_non_pos_list n ntypes largs + in + (nmr, List.rev lrec) in check_constr_rec ienv nmr [] c in let irecargs_nmr = diff --git a/kernel/inductive.ml b/kernel/inductive.ml index a44afce2b..d1cffe867 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -75,7 +75,7 @@ let instantiate_params full t args sign = sign ~init:(args,[],t) in - if rem_args <> [] then fail(); + let () = if not (List.is_empty rem_args) then fail () in substl subs ty let full_inductive_instantiate mib params sign = @@ -282,7 +282,10 @@ let build_dependent_inductive ind (_,mip) params = exception LocalArity of (sorts_family * sorts_family * arity_error) option let check_allowed_sort ksort specif = - if not (List.exists ((=) ksort) (elim_sorts specif)) then + let eq_ksort s = match ksort, s with + | InProp, InProp | InSet, InSet | InType, InType -> true + | _ -> false in + if not (List.exists eq_ksort (elim_sorts specif)) then let s = inductive_sort_family (snd specif) in raise (LocalArity (Some(ksort,s,error_elim_explain ksort s))) @@ -358,9 +361,9 @@ let type_case_branches env (ind,largs) pj c = let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if - not (eq_ind indsp ci.ci_ind) or - (mib.mind_nparams <> ci.ci_npar) or - (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) + not (eq_ind indsp ci.ci_ind) || + not (Int.equal mib.mind_nparams ci.ci_npar) || + not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls) then raise (TypeError(env,WrongCaseInfo(indsp,ci))) (************************************************************************) @@ -412,7 +415,7 @@ type subterm_spec = | Not_subterm let spec_of_tree t = lazy - (if Rtree.eq_rtree (=) (Lazy.force t) mk_norec + (if Rtree.eq_rtree eq_recarg (Lazy.force t) mk_norec then Not_subterm else Subterm(Strict,Lazy.force t)) @@ -424,7 +427,7 @@ let subterm_spec_glb = | Not_subterm, _ -> Not_subterm | _, Not_subterm -> Not_subterm | Subterm (a1,t1), Subterm (a2,t2) -> - if Rtree.eq_rtree (=) t1 t2 then Subterm (size_glb a1 a2, t1) + if Rtree.eq_rtree eq_recarg t1 t2 then Subterm (size_glb a1 a2, t1) (* branches do not return objects with same spec *) else Not_subterm in Array.fold_left glb2 Dead_code @@ -515,7 +518,7 @@ let branches_specif renv c_spec ci = (match Lazy.force c_spec with Subterm (_,t) when match_inductive ci.ci_ind (dest_recarg t) -> let vra = Array.of_list (dest_subterms t).(i) in - assert (nca = Array.length vra); + assert (Int.equal nca (Array.length vra)); Array.map (fun t -> Lazy.force (spec_of_tree (lazy t))) vra @@ -586,7 +589,7 @@ let rec subterm_specif renv stack t = subterm_specif renv'' [] strippedBody) | Lambda (x,a,b) -> - assert (l=[]); + let () = assert (List.is_empty l) in let spec,stack' = extract_stack renv a stack in subterm_specif (push_var renv (x,a,spec)) stack' b @@ -711,7 +714,7 @@ let check_one_fix renv recpos def = let stack' = push_stack_closures renv l stack in Array.iteri (fun j body -> - if i=j && (List.length stack' > decrArg) then + if Int.equal i j && (List.length stack' > decrArg) then let recArg = List.nth stack' decrArg in let arg_sp = stack_element_specif recArg in check_nested_fix_body renv' (decrArg+1) arg_sp body @@ -727,13 +730,13 @@ let check_one_fix renv recpos def = else List.iter (check_rec_call renv []) l | Lambda (x,a,b) -> - assert (l = []); + let () = assert (List.is_empty l) in check_rec_call renv [] a ; let spec, stack' = extract_stack renv a stack in check_rec_call (push_var renv (x,a,spec)) stack' b | Prod (x,a,b) -> - assert (l = [] && stack = []); + let () = assert (List.is_empty l && List.is_empty stack) in check_rec_call renv [] a; check_rec_call (push_var_renv renv (x,a)) [] b @@ -757,7 +760,8 @@ let check_one_fix renv recpos def = check_rec_call renv stack (applist(c,l)) end - | Sort _ -> assert (l = []) + | Sort _ -> + assert (List.is_empty l) (* l is not checked because it is considered as the meta's context *) | (Evar _ | Meta _) -> () @@ -784,11 +788,11 @@ let judgment_of_fixpoint (_, types, bodies) = let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = let nbfix = Array.length bodies in if Int.equal nbfix 0 - or Array.length nvect <> nbfix - or Array.length types <> nbfix - or Array.length names <> nbfix - or bodynum < 0 - or bodynum >= nbfix + || not (Int.equal (Array.length nvect) nbfix) + || not (Int.equal (Array.length types) nbfix) + || not (Int.equal (Array.length names) nbfix) + || bodynum < 0 + || bodynum >= nbfix then anomaly "Ill-formed fix term"; let fixenv = push_rec_types recdef env in let vdefj = judgment_of_fixpoint recdef in @@ -803,7 +807,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = | Lambda (x,a,b) -> if noccur_with_meta n nbfix a then let env' = push_rel (x, None, a) env in - if n = k+1 then + if Int.equal n (k + 1) then (* get the inductive type of the fixpoint *) let (mind, _) = try find_inductive env a @@ -873,7 +877,7 @@ let check_one_cofix env nbfix def deftype = let realargs = List.skipn mib.mind_nparams args in let rec process_args_of_constr = function | (t::lr), (rar::lrar) -> - if rar = mk_norec then + if Rtree.eq_rtree eq_recarg rar mk_norec then if noccur_with_meta n nbfix t then process_args_of_constr (lr, lrar) else raise (CoFixGuardError @@ -887,7 +891,7 @@ let check_one_cofix env nbfix def deftype = in process_args_of_constr (realargs, lra) | Lambda (x,a,b) -> - assert (args = []); + let () = assert (List.is_empty args) in if noccur_with_meta n nbfix a then let env' = push_rel (x, None, a) env in check_rec_call env' alreadygrd (n+1) vlra b diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index a85395497..5af6bd5bb 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -492,7 +492,7 @@ let add_delta_resolver resolver1 resolver2 = let substition_prefixed_by k mp subst = let mp_prefixmp kmp (mp_to,reso) sub = - if mp_in_mp mp kmp && mp <> kmp then + if mp_in_mp mp kmp && not (mp_eq mp kmp) then let new_key = replace_mp_in_mp mp k kmp in Umap.add_mp new_key (mp_to,reso) sub else sub diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index b2312d689..b358d805a 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -41,7 +41,7 @@ let is_modular = function let rec list_split_assoc ((k,m) as km) rev_before = function | [] -> raise Not_found - | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after + | (k',b)::after when eq_label k k' && (is_modular b) == (m : bool) -> rev_before,b,after | h::tail -> list_split_assoc km (h::rev_before) tail let discr_resolver env mtb = @@ -65,11 +65,12 @@ let rec check_with env sign with_decl alg_sign mp equiv = let sign,equiv,cst = check_with_mod env sign (idl,mp1) mp equiv in sign,With_module_body(idl,mp1),equiv,cst in - if alg_sign = None then - sign,None,equiv,cst - else - sign,Some (SEBwith(Option.get(alg_sign),wd)),equiv,cst - + match alg_sign with + | None -> + sign, None, equiv, cst + | Some s -> + sign,Some (SEBwith(s, wd)),equiv,cst + and check_with_def env sign (idl,c) mp equiv = let sig_b = match sign with | SEBstruct(sig_b) -> sig_b @@ -81,10 +82,11 @@ and check_with_def env sign (idl,c) mp equiv = in let l = label_of_id id in try - let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in + let not_empty = match idl with [] -> false | _ :: _ -> true in + let rev_before,spec,after = list_split_assoc (l, not_empty) [] sig_b in let before = List.rev rev_before in let env' = Modops.add_signature mp before equiv env in - if idl = [] then + match idl with [] -> (* Toplevel definition *) let cb = match spec with | SFBconst cb -> cb @@ -119,7 +121,7 @@ and check_with_def env sign (idl,c) mp equiv = const_constraints = cst } in SEBstruct(before@(l,SFBconst(cb'))::after),cb',cst - else + | _ -> (* Definition inside a sub-module *) let old = match spec with | SFBmodule msb -> msb @@ -156,7 +158,7 @@ and check_with_mod env sign (idl,mp1) mp equiv = let rev_before,spec,after = list_split_assoc (l,true) [] sig_b in let before = List.rev rev_before in let env' = Modops.add_signature mp before equiv env in - if idl = [] then + match idl with [] -> (* Toplevel module definition *) let old = match spec with SFBmodule msb -> msb @@ -191,7 +193,7 @@ and check_with_mod env sign (idl,mp1) mp equiv = let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) new_mb.mod_delta in SEBstruct(before@(l,new_spec)::subst_signature id_subst after), add_delta_resolver equiv new_mb.mod_delta,cst - else + | _ -> (* Module definition of a sub-module *) let old = match spec with SFBmodule msb -> msb diff --git a/kernel/names.ml b/kernel/names.ml index 08b111cd6..c4e632a3a 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -96,10 +96,13 @@ let rec dir_path_ord (p1 : dir_path) (p2 : dir_path) = if Int.equal c 0 then dir_path_ord p1 p2 else c end +let dir_path_eq p1 p2 = Int.equal (dir_path_ord p1 p2) 0 + let make_dirpath x = x let repr_dirpath x = x let empty_dirpath = [] +let is_empty_dirpath d = match d with [] -> true | _ -> false (** Printing of directory paths as ["coq_root.module.submodule"] *) @@ -155,6 +158,7 @@ let string_of_label = string_of_id let pr_label l = str (string_of_label l) let id_of_label l = l let label_of_id id = id +let eq_label = String.equal module Labset = Idset module Labmap = Idmap @@ -281,7 +285,7 @@ let debug_string_of_con con = let debug_pr_con con = str (debug_string_of_con con) let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl = - if Int.equal (String.compare lbl l1) 0 && Int.equal (String.compare lbl l2) 0 + if String.equal lbl l1 && String.equal lbl l2 then con else ((mp1, dp1, lbl), (mp2, dp2, lbl)) diff --git a/kernel/names.mli b/kernel/names.mli index 5ab3b5c3f..3eb070380 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -45,6 +45,8 @@ type dir_path val dir_path_ord : dir_path -> dir_path -> int +val dir_path_eq : dir_path -> dir_path -> bool + (** Inner modules idents on top of list (to improve sharing). For instance: A.B.C is ["C";"B";"A"] *) val make_dirpath : module_ident list -> dir_path @@ -52,6 +54,8 @@ val repr_dirpath : dir_path -> module_ident list val empty_dirpath : dir_path +val is_empty_dirpath : dir_path -> bool + (** Printing of directory paths as ["coq_root.module.submodule"] *) val string_of_dirpath : dir_path -> string @@ -66,6 +70,8 @@ val pr_label : label -> Pp.std_ppcmds val label_of_id : identifier -> label val id_of_label : label -> identifier +val eq_label : label -> label -> bool + module Labset : Set.S with type elt = label module Labmap : Map.S with type key = label diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b0ea2f7db..fb6ffd2d1 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -333,14 +333,20 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* Eta-expansion on the fly *) | (FLambda _, _) -> - if v1 <> [] then - anomaly "conversion was given unreduced term (FLambda)"; + let () = match v1 with + | [] -> () + | _ -> + anomaly "conversion was given unreduced term (FLambda)" + in let (_,_ty1,bd1) = destFLambda mk_clos hd1 in eqappr CONV l2r infos (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv | (_, FLambda _) -> - if v2 <> [] then - anomaly "conversion was given unreduced term (FLambda)"; + let () = match v2 with + | [] -> () + | _ -> + anomaly "conversion was given unreduced term (FLambda)" + in let (_,_ty2,bd2) = destFLambda mk_clos hd2 in eqappr CONV l2r infos (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 143b22c34..28052c41b 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -271,7 +271,7 @@ let add_constant dir l decl senv = | ConstantEntry ce -> translate_constant senv.env kn ce | GlobalRecipe r -> let cb = translate_recipe senv.env kn r in - if dir = empty_dirpath then hcons_const_body cb else cb + if is_empty_dirpath dir then hcons_const_body cb else cb in let senv' = add_field (l,SFBconst cb) (C kn) senv in let senv'' = match cb.const_body with @@ -284,16 +284,19 @@ let add_constant dir l decl senv = (* Insertion of inductive types. *) let add_mind dir l mie senv = - if mie.mind_entry_inds = [] then - anomaly "empty inductive types declaration"; + let () = match mie.mind_entry_inds with + | [] -> + anomaly "empty inductive types declaration" (* this test is repeated by translate_mind *) + | _ -> () + in let id = (List.nth mie.mind_entry_inds 0).mind_entry_typename in - if l <> label_of_id id then + if not (eq_label l (label_of_id id)) then anomaly ("the label of inductive packet and its first inductive"^ " type do not match"); let kn = make_mind senv.modinfo.modpath dir l in let mib = translate_mind senv.env kn mie in - let mib = if mib.mind_hyps <> [] then mib else hcons_mind mib in + let mib = match mib.mind_hyps with [] -> hcons_mind mib | _ -> mib in let senv' = add_field (l,SFBmind mib) (I kn) senv in kn, senv' @@ -358,7 +361,7 @@ let end_module l restype senv = | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end () | STRUCT params -> params, (List.length params > 0) in - if l <> modinfo.label then error_incompatible_labels l modinfo.label; + if not (eq_label l modinfo.label) then error_incompatible_labels l modinfo.label; if not (empty_context senv.env) then error_non_empty_local_context None; let functorize_struct tb = List.fold_left @@ -494,8 +497,11 @@ let end_module l restype senv = (* Adding parameters to modules or module types *) let add_module_parameter mbid mte inl senv = - if senv.revstruct <> [] or senv.loads <> [] then - anomaly "Cannot add a module parameter to a non empty module"; + let () = match senv.revstruct, senv.loads with + | [], _ :: _ | _ :: _, [] -> + anomaly "Cannot add a module parameter to a non empty module" + | _ -> () + in let mtb = translate_module_type senv.env (MPbound mbid) inl mte in let senv = full_add_module (module_body_of_type (MPbound mbid) mtb) senv @@ -559,7 +565,7 @@ let end_modtype l senv = | LIBRARY _ | NONE | STRUCT _ -> error_no_modtype_to_end () | SIG params -> params in - if l <> modinfo.label then error_incompatible_labels l modinfo.label; + if not (eq_label l modinfo.label) then error_incompatible_labels l modinfo.label; if not (empty_context senv.env) then error_non_empty_local_context None; let auto_tb = SEBstruct (List.rev senv.revstruct) @@ -629,10 +635,9 @@ type compiled_library = (* We check that only initial state Require's were performed before [start_library] was called *) -let is_empty senv = - senv.revstruct = [] && - senv.modinfo.modpath = initial_path && - senv.modinfo.variant = NONE +let is_empty senv = match senv.revstruct, senv.modinfo.variant with + | [], NONE -> mp_eq senv.modinfo.modpath initial_path + | _ -> false let start_library dir senv = if not (is_empty senv) then @@ -677,7 +682,7 @@ let export senv dir = begin match modinfo.variant with | LIBRARY dp -> - if dir <> dp then + if not (dir_path_eq dir dp) then anomaly "We are not exporting the right library!" | _ -> anomaly "We are not exporting the library" @@ -703,7 +708,7 @@ let check_imports senv needed = let check (id,stamp) = try let actual_stamp = List.assoc id imports in - if stamp <> actual_stamp then + if not (String.equal stamp actual_stamp) then error ("Inconsistent assumptions over module "^(string_of_dirpath id)^".") with Not_found -> diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 8b34950da..6aaf5b47d 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -135,14 +135,14 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 in let check_packet cst p1 p2 = - 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; + let check f test why = if not (test (f p1) (f p2)) then error why in + check (fun p -> p.mind_consnames) (Array.equal id_eq) NotSameConstructorNamesField; + check (fun p -> p.mind_typename) id_eq NotSameInductiveNameInBlockField; (* nf_lc later *) (* nf_arity later *) (* user_lc ignored *) (* user_arity ignored *) - check (fun p -> p.mind_nrealargs) (NotConvertibleInductiveField p2.mind_typename); (* How can it fail since the type of inductive are checked below? [HH] *) + check (fun p -> p.mind_nrealargs) Int.equal (NotConvertibleInductiveField p2.mind_typename); (* How can it fail since the type of inductive are checked below? [HH] *) (* kelim ignored *) (* listrec ignored *) (* finite done *) @@ -161,10 +161,10 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (arities_of_specif kn1 (mib1,p1)) (arities_of_specif kn1 (mib2,p2)) in - 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=[]); + let check f test why = if not (test (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) Int.equal (fun x -> InductiveNumbersFieldExpected x); + assert (List.is_empty mib1.mind_hyps && List.is_empty mib2.mind_hyps); assert (Array.length mib1.mind_packets >= 1 && Array.length mib2.mind_packets >= 1); @@ -173,17 +173,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) (fun x -> InductiveParamsNumberField x); + check (fun mib -> mib.mind_nparams) Int.equal (fun x -> InductiveParamsNumberField x); begin match mind_of_delta reso2 kn2 with - | kn2' when kn2=kn2' -> () + | kn2' when eq_mind kn2 kn2' -> () | kn2' -> if not (eq_mind (mind_of_delta reso1 kn1) (subst_ind subst2 kn2')) then error NotEqualInductiveAliases end; (* we check that records and their field names are preserved. *) - check (fun mib -> mib.mind_record) (fun x -> RecordFieldExpected x); + 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) @@ -198,7 +198,7 @@ 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)) (List.equal name_eq) (fun x -> RecordProjectionsExpected x); end; (* we first check simple things *) @@ -265,7 +265,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = match info1 with | Constant cb1 -> - assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; + let () = assert (List.is_empty cb1.const_hyps && List.is_empty cb2.const_hyps) in let cb1 = subst_const_body subst1 cb1 in let cb2 = subst_const_body subst2 cb2 in (* Start by checking types*) @@ -295,7 +295,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ "name.")); - assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; + let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in if constant_has_body cb2 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 @@ -306,7 +306,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ "name.")); - assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; + let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in if constant_has_body cb2 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 diff --git a/kernel/term.ml b/kernel/term.ml index 94aa7d968..627919f09 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -672,7 +672,7 @@ let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = - Int.equal (id_ord i1 i2) 0 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2 + id_eq i1 i2 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2 let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) = name_eq n1 n2 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2 diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 294d99eea..8509edaf9 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -126,9 +126,12 @@ let extract_level env p = let _,c = dest_prod_assum env p in match kind_of_term c with Sort (Type u) -> Some u | _ -> None -let extract_context_levels env = - List.fold_left - (fun l (_,b,p) -> if b=None then extract_level env p::l else l) [] +let extract_context_levels env l = + let fold l (_, b, p) = match b with + | None -> extract_level env p :: l + | _ -> 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 @@ -227,12 +230,14 @@ let sort_of_product env domsort rangsort = | (Prop _, Prop Pos) -> rangsort (* Product rule (Type,Set,?) *) | (Type u1, Prop Pos) -> - if engagement env = Some ImpredicativeSet then + begin match engagement env with + | Some ImpredicativeSet -> (* 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 (sup u1 type0_univ) + end (* Product rule (Prop,Type_i,Type_i) *) | (Prop Pos, Type u2) -> Type (sup type0_univ u2) (* Product rule (Prop,Type_i,Type_i) *) @@ -348,7 +353,7 @@ let judge_of_case env ci pj cj lfj = let type_fixpoint env lna lar vdefj = let lt = Array.length vdefj in - assert (Array.length lar = lt); + 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) with NotConvertibleVect i -> diff --git a/kernel/univ.ml b/kernel/univ.ml index 18bee0fb4..12ec4e222 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -105,9 +105,12 @@ let pr_uni = function | Max ([],[u]) -> str "(" ++ pr_uni_level u ++ str ")+1" | Max (gel,gtl) -> + let opt_sep = match gel, gtl with + | [], _ | _, [] -> mt () + | _ -> pr_comma () + in str "max(" ++ hov 0 - (prlist_with_sep pr_comma pr_uni_level gel ++ - (if gel <> [] & gtl <> [] then pr_comma () else mt ()) ++ + (prlist_with_sep pr_comma pr_uni_level gel ++ opt_sep ++ prlist_with_sep pr_comma (fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl) ++ str ")" @@ -177,7 +180,8 @@ let is_type0_univ = function | u -> false let is_univ_variable = function - | Atom a when a<>UniverseLevel.Set -> true + | Atom UniverseLevel.Set -> false + | Atom _ -> true | _ -> false (* When typing [Prop] and [Set], there is no constraint on the level, @@ -538,10 +542,10 @@ module Constraint = Set.Make( type t = univ_constraint let compare (u,c,v) (u',c',v') = let i = constraint_type_ord c c' in - if i <> 0 then i + if not (Int.equal i 0) then i else let i' = UniverseLevel.compare u u' in - if i' <> 0 then i' + if not (Int.equal i' 0) then i' else UniverseLevel.compare v v' end) @@ -830,7 +834,7 @@ let solve_constraints_system levels level_bounds = let nind = Array.length v in for i=0 to nind-1 do for j=0 to nind-1 do - if i<>j & is_direct_sort_constraint levels.(j) v.(i) then + if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then v.(i) <- sup v.(i) level_bounds.(j) done; for j=0 to nind-1 do @@ -854,7 +858,10 @@ let subst_large_constraints = let no_upper_constraints u cst = match u with - | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst + | Atom u -> + let test (u1, _, _) = + not (Int.equal (UniverseLevel.compare u1 u) 0) in + Constraint.for_all test cst | Max _ -> anomaly "no_upper_constraints" (* Is u mentionned in v (or equals to v) ? *) @@ -871,10 +878,14 @@ let pr_arc = function | _, Canonical {univ=u; lt=[]; le=[]} -> mt () | _, Canonical {univ=u; lt=lt; le=le} -> + let opt_sep = match lt, le with + | [], _ | _, [] -> mt () + | _ -> spc () + in pr_uni_level u ++ str " " ++ v 0 (pr_sequence (fun v -> str "< " ++ pr_uni_level v) lt ++ - (if lt <> [] & le <> [] then spc () else mt()) ++ + opt_sep ++ pr_sequence (fun v -> str "<= " ++ pr_uni_level v) le) ++ fnl () | u, Equiv v -> |