diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-08 17:11:59 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-08 17:11:59 +0000 |
| commit | b0b1710ba631f3a3a3faad6e955ef703c67cb967 (patch) | |
| tree | 9d35a8681cda8fa2dc968535371739684425d673 | |
| parent | bafb198e539998a4a64b2045a7e85125890f196e (diff) | |
Monomorphized a lot of equalities over OCaml integers, thanks to
the new Int module. Only the most obvious were removed, so there
are a lot more in the wild.
This may sound heavyweight, but it has two advantages:
1. Monomorphization is explicit, hence we do not miss particular
optimizations of equality when doing it carelessly with the generic
equality.
2. When we have removed all the generic equalities on integers, we
will be able to write something like "let (=) = ()" to retrieve all
its other uses (mostly faulty) spread throughout the code, statically.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
59 files changed, 276 insertions, 259 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d5f96e3fd..b651053db 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -274,7 +274,7 @@ let drop_implicits_in_patt cst nb_expl args = |None -> aux t |x -> x in - if nb_expl = 0 then aux impl_data + if Int.equal nb_expl 0 then aux impl_data else let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in impls_fit [] (imps,args) @@ -712,7 +712,7 @@ let rec extern inctx scopes vars r = let projs = struc.Recordops.s_PROJ in let locals = struc.Recordops.s_PROJKIND in let rec cut args n = - if n = 0 then args + if Int.equal n 0 then args else match args with | [] -> raise No_match @@ -907,7 +907,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function subscopes,impls | _ -> [], [] in - (if n = 0 then f else GApp (Loc.ghost,f,args1)), + (if Int.equal n 0 then f else GApp (Loc.ghost,f,args1)), args2, subscopes, impls | GApp (_,(GRef (_,ref) as f),args), None -> let subscopes = find_arguments_scope ref in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c204db0e0..a6b207c1d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -199,7 +199,7 @@ and spaces ntn n = let expand_notation_string ntn n = let pos = List.nth (wildcards ntn 0) n in - let hd = if pos = 0 then "" else String.sub ntn 0 pos in + let hd = if Int.equal pos 0 then "" else String.sub ntn 0 pos in let tl = if pos = String.length ntn then "" else String.sub ntn (pos+1) (String.length ntn - pos -1) in @@ -737,7 +737,7 @@ let find_remaining_scopes pl1 pl2 ref = let impls_st = implicits_of_global ref in let len_pl1 = List.length pl1 in let len_pl2 = List.length pl2 in - let impl_list = if len_pl1 = 0 + let impl_list = if Int.equal len_pl1 0 then select_impargs_size len_pl2 impls_st else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in let allscs = find_arguments_scope ref in @@ -797,7 +797,7 @@ let check_constructor_length env loc cstr len_pl pl0 = (nargs - (Inductiveops.inductive_nparams (fst cstr)))) let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 = - let impl_list = if len_pl1 = 0 + let impl_list = if Int.equal len_pl1 0 then select_impargs_size (List.length pl2) impls_st else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in let remaining_args = List.fold_left (fun i x -> if is_status_implicit x then i else succ i) in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index c5cc1438b..d3c55c1f5 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -754,7 +754,7 @@ let rec match_cases_pattern metas sigma a1 a2 = when r1 = r2 -> let l1 = add_patterns_for_params (fst r1) args1 in let le2 = List.length l2 in - if le2 = 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 + if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 then raise No_match else @@ -777,7 +777,7 @@ let match_ind_pattern metas sigma ind pats a2 = | NApp (NRef (IndRef r2),l2) when ind = r2 -> let le2 = List.length l2 in - if le2 = 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats + if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats then raise No_match else diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 9e695e3d3..deba56f73 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -108,7 +108,7 @@ let empty_comp_env ()= (*i Creation functions for comp_env *) let rec add_param n sz l = - if n = 0 then l else add_param (n - 1) sz (n+sz::l) + if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l) let comp_env_fun arity = { nb_stack = arity; @@ -280,14 +280,14 @@ let rec is_tailcall = function let rec add_pop n = function | Kpop m :: cont -> add_pop (n+m) cont | Kreturn m:: cont -> Kreturn (n+m) ::cont - | cont -> if n = 0 then cont else Kpop n :: cont + | cont -> if Int.equal n 0 then cont else Kpop n :: cont let add_grab arity lbl cont = - if arity = 1 then Klabel lbl :: cont + if Int.equal arity 1 then Klabel lbl :: cont else Krestart :: Klabel lbl :: Kgrab (arity - 1) :: cont let add_grabrec rec_arg arity lbl cont = - if arity = 1 then + if Int.equal arity 1 then Klabel lbl :: Kgrabrec 0 :: Krestart :: cont else Krestart :: Klabel lbl :: Kgrabrec rec_arg :: @@ -331,7 +331,7 @@ let init_fun_code () = fun_code := [] let code_construct tag nparams arity cont = let f_cont = add_pop nparams - (if arity = 0 then + (if Int.equal arity 0 then [Kconst (Const_b0 tag); Kreturn 0] else [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0]) in @@ -397,7 +397,7 @@ let rec str_const c = with Not_found -> (* 3/ if no special behavior is available, then the compiler falls back to the normal behavior *) - if arity = 0 then Bstrconst(Const_b0 num) + if Int.equal arity 0 then Bstrconst(Const_b0 num) else let rargs = Array.sub args nparams arity in let b_args = Array.map str_const rargs in @@ -435,7 +435,7 @@ let rec str_const c = let oip = oib.mind_packets.(j) in let num,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in - if nparams + arity = 0 then Bstrconst(Const_b0 num) + if Int.equal (nparams + arity) 0 then Bstrconst(Const_b0 num) else Bconstruct_app(num,nparams,arity,[||]) end | _ -> Bconstr c @@ -622,7 +622,7 @@ let rec compile_constr reloc c sz cont = (* Compiling regular constructor branches *) for i = 0 to Array.length tbl - 1 do let tag, arity = tbl.(i) in - if arity = 0 then + if Int.equal arity 0 then let lbl_b,code_b = label_code(compile_constr reloc branchs.(i) sz_b (branch :: !c)) in lbl_consts.(tag) <- lbl_b; @@ -669,7 +669,7 @@ and compile_str_cst reloc sc sz cont = let nargs = Array.length args in comp_args compile_str_cst reloc args sz (Kmakeblock(nargs,tag) :: cont) | Bconstruct_app(tag,nparams,arity,args) -> - if Array.length args = 0 then code_construct tag nparams arity cont + if Int.equal (Array.length args) 0 then code_construct tag nparams arity cont else comp_app (fun _ _ _ cont -> code_construct tag nparams arity cont) @@ -689,7 +689,7 @@ and compile_const = Retroknowledge.get_vm_compiling_info (!global_env).retroknowledge (kind_of_term (mkConst kn)) reloc args sz cont with Not_found -> - if nargs = 0 then + if Int.equal nargs 0 then Kgetglobal (get_allias !global_env kn) :: cont else comp_app (fun _ _ _ cont -> @@ -760,7 +760,7 @@ let compile_structured_int31 fc args = let dynamic_int31_compilation fc reloc args sz cont = if not fc then raise Not_found else let nargs = Array.length args in - if nargs = 31 then + if Int.equal nargs 31 then let (escape,labeled_cont) = make_branch cont in let else_lbl = Label.create() in comp_args compile_str_cst reloc args sz @@ -778,7 +778,7 @@ let dynamic_int31_compilation fc reloc args sz cont = fun_code := [Ksequence (add_grab 31 lbl f_cont,!fun_code)]; Kclosure(lbl,0) :: cont in - if nargs = 0 then + if Int.equal nargs 0 then code_construct cont else comp_app (fun _ _ _ cont -> code_construct cont) diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 680a5f9f2..90b4f0ae0 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -165,7 +165,7 @@ let emit_instr = function then out(opENVACC1 + n - 1) else (out opENVACC; out_int n) | Koffsetclosure ofs -> - if ofs = -2 || ofs = 0 || ofs = 2 + if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2 then out (opOFFSETCLOSURE0 + ofs / 2) else (out opOFFSETCLOSURE; out_int ofs) | Kpush -> @@ -214,7 +214,7 @@ let emit_instr = function | Kconst c -> out opGETGLOBAL; slot_for_const c | Kmakeblock(n, t) -> - if n = 0 then raise (Invalid_argument "emit_instr : block size = 0") + if Int.equal n 0 then raise (Invalid_argument "emit_instr : block size = 0") else if n < 4 then (out(opMAKEBLOCK1 + n - 1); out_int t) else (out opMAKEBLOCK; out_int n; out_int t) | Kmakeprod -> @@ -279,7 +279,7 @@ let rec emit = function else (out opPUSHENVACC; out_int n); emit c | Kpush :: Koffsetclosure ofs :: c -> - if ofs = -2 || ofs = 0 || ofs = 2 + if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2 then out(opPUSHOFFSETCLOSURE0 + ofs / 2) else (out opPUSHOFFSETCLOSURE; out_int ofs); emit c diff --git a/kernel/closure.ml b/kernel/closure.ml index 51e264106..681fb8533 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -354,7 +354,7 @@ and stack = stack_member list let empty_stack = [] let append_stack v s = - if Array.length v = 0 then s else + if Int.equal (Array.length v) 0 then s else match s with | Zapp l :: s -> Zapp (Array.append v l) :: s | _ -> Zapp v :: s @@ -398,7 +398,7 @@ let rec stack_assign s p c = match s with Zapp nargs :: s) | _ -> s let rec stack_tail p s = - if p = 0 then s else + if Int.equal p 0 then s else match s with | Zapp args :: s -> let q = Array.length args in @@ -719,7 +719,7 @@ let get_nth_arg head n stk = let bef = Array.sub args 0 n in let aft = Array.sub args (n+1) (q-n-1) in let stk' = - List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in + List.rev (if Int.equal n 0 then rstk else (Zapp bef :: rstk)) in (Some (stk', args.(n)), append_stack aft s') | Zupdate(m)::s -> strip_rec rstk (update m (h.norm,h.term)) n s @@ -764,7 +764,7 @@ let rec reloc_rargs_rec depth stk = | _ -> stk let reloc_rargs depth stk = - if depth = 0 then stk else reloc_rargs_rec depth stk + if Int.equal depth 0 then stk else reloc_rargs_rec depth stk let rec drop_parameters depth n argstk = match argstk with diff --git a/kernel/environ.ml b/kernel/environ.ml index 37a896c77..301c3b152 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -423,7 +423,7 @@ let register = let nth_digit_plus_one i n = (* calculates the nth (starting with 0) digit of i and adds 1 to it (nth_digit_plus_one 1 3 = 2) *) - if (land) i ((lsl) 1 n) = 0 then + if Int.equal (i land (1 lsl n)) 0 then 1 else 2 diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 0bd7c515c..30c2387ea 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -29,14 +29,14 @@ let el_id = ELID let rec el_shft_rec n = function | ELSHFT(el,k) -> el_shft_rec (k+n) el | el -> ELSHFT(el,n) -let el_shft n el = if n = 0 then el else el_shft_rec n el +let el_shft n el = if Int.equal n 0 then el else el_shft_rec n el (* cross n binders *) let rec el_liftn_rec n = function | ELID -> ELID | ELLFT(k,el) -> el_liftn_rec (n+k) el | el -> ELLFT(n, el) -let el_liftn n el = if n = 0 then el else el_liftn_rec n el +let el_liftn n el = if Int.equal n 0 then el else el_liftn_rec n el let el_lift el = el_liftn_rec 1 el @@ -73,7 +73,7 @@ type 'a subs = let subs_id i = ESID i -let subs_cons(x,s) = if Array.length x = 0 then s else CONS(x,s) +let subs_cons(x,s) = if Int.equal (Array.length x) 0 then s else CONS(x,s) let subs_liftn n = function | ESID p -> ESID (p+n) (* bounded identity lifted extends by p *) @@ -81,13 +81,13 @@ let subs_liftn n = function | lenv -> LIFT (n,lenv) let subs_lift a = subs_liftn 1 a -let subs_liftn n a = if n = 0 then a else subs_liftn n a +let subs_liftn n a = if Int.equal n 0 then a else subs_liftn n a let subs_shft = function | (0, s) -> s | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1) | (n, s) -> SHIFT (n,s) -let subs_shft (n,a) = if n = 0 then a else subs_shft(n,a) +let subs_shft (n,a) = if Int.equal n 0 then a else subs_shft(n,a) let subs_shift_cons = function (0, s, t) -> CONS(t,s) @@ -99,7 +99,7 @@ let rec is_subs_id = function ESID _ -> true | LIFT(_,s) -> is_subs_id s | SHIFT(0,s) -> is_subs_id s - | CONS(x,s) -> Array.length x = 0 && is_subs_id s + | CONS(x,s) -> Int.equal (Array.length x) 0 && is_subs_id s | _ -> false (* Expands de Bruijn k in the explicit substitution subs diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 1c12c9e24..6b993604d 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -349,7 +349,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = recursive parameters *) let compute_rec_par (env,n,_,_) hyps nmr largs = -if nmr = 0 then 0 else +if Int.equal nmr 0 then 0 else (* start from 0, hyps will be in reverse order *) let (lpar,_) = List.chop nmr largs in let rec find k index = @@ -371,7 +371,7 @@ let lambda_implicit_lift n a = (* This removes global parameters of the inductive types in lc (for nested inductive types only ) *) let abstract_mind_lc env ntyps npars lc = - if npars = 0 then + if Int.equal npars 0 then lc else let make_abs = @@ -411,7 +411,7 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = ienv_decompose_prod ienv' (n-1) b | _ -> assert false -let array_min nmr a = if nmr = 0 then 0 else +let array_min nmr a = if Int.equal nmr 0 then 0 else Array.fold_left (fun k (nmri,_) -> min k nmri) nmr a (* The recursive function that checks positivity and builds the list @@ -620,7 +620,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = let nconst, nblock = ref 0, ref 0 in let transf num = let arity = List.length (dest_subterms recarg).(num) in - if arity = 0 then + if Int.equal arity 0 then let p = (!nconst, 0) in incr nconst; p else diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 81e6c8f17..c53a0bcd9 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -765,7 +765,7 @@ let check_one_fix renv recpos def = | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) and check_nested_fix_body renv decr recArgsDecrArg body = - if decr = 0 then + if Int.equal decr 0 then check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body else match kind_of_term body with @@ -783,7 +783,7 @@ 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 nbfix = 0 + if Int.equal nbfix 0 or Array.length nvect <> nbfix or Array.length types <> nbfix or Array.length names <> nbfix diff --git a/kernel/names.ml b/kernel/names.ml index 96055ca16..250b4a6b5 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -88,7 +88,7 @@ let rec dir_path_ord (p1 : dir_path) (p2 : dir_path) = | _, [] -> 1 | id1 :: p1, id2 :: p2 -> let c = id_ord id1 id2 in - if c <> 0 then c else dir_path_ord p1 p2 + if Int.equal c 0 then dir_path_ord p1 p2 else c end let make_dirpath x = x @@ -116,11 +116,11 @@ let uniq_ident_ord (x : uniq_ident) (y : uniq_ident) = if x == y then 0 else match (x, y) with | (nl, idl, dpl), (nr, idr, dpr) -> - let ans = nl - nr in - if ans <> 0 then ans + let ans = Int.compare nl nr in + if not (Int.equal ans 0) then ans else let ans = id_ord idl idr in - if ans <> 0 then ans + if not (Int.equal ans 0) then ans else dir_path_ord dpl dpr @@ -180,7 +180,7 @@ let rec mp_ord mp1 mp2 = uniq_ident_ord id1 id2 | MPdot (mp1, l1), MPdot (mp2, l2) -> let c = String.compare l1 l2 in - if c <> 0 then c + if not (Int.equal c 0) then c else mp_ord mp1 mp2 | MPfile _, _ -> -1 | MPbound _, MPfile _ -> 1 @@ -226,10 +226,10 @@ let kn_ord (kn1 : kernel_name) (kn2 : kernel_name) = let mp1, dir1, l1 = kn1 in let mp2, dir2, l2 = kn2 in let c = String.compare l1 l2 in - if c <> 0 then c + if not (Int.equal c 0) then c else let c = dir_path_ord dir1 dir2 in - if c <> 0 then c + if not (Int.equal c 0) then c else MPord.compare mp1 mp2 module KNord = struct @@ -259,7 +259,7 @@ let canonical_con con = snd con let user_con con = fst con let repr_con con = fst con -let eq_constant (_,kn1) (_,kn2) = kn1=kn2 +let eq_constant (_, kn1) (_, kn2) = Int.equal (kn_ord kn1 kn2) 0 let con_label con = label (fst con) let con_modpath con = modpath (fst con) @@ -271,8 +271,9 @@ 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 lbl = l1 && lbl = l2 then con - else ((mp1,dp1,lbl),(mp2,dp2,lbl)) + if Int.equal (String.compare lbl l1) 0 && Int.equal (String.compare lbl l2) 0 + then con + else ((mp1, dp1, lbl), (mp2, dp2, lbl)) (** For the environment we distinguish constants by their user part*) module User_ord = struct @@ -319,7 +320,7 @@ let user_mind mind = fst mind let repr_mind mind = fst mind let mind_label mind = label (fst mind) -let eq_mind (_, kn1) (_, kn2) = kn_ord kn1 kn2 = 0 +let eq_mind (_, kn1) (_, kn2) = Int.equal (kn_ord kn1 kn2) 0 let string_of_mind mind = string_of_kn (fst mind) let pr_mind mind = str (string_of_mind mind) @@ -331,10 +332,10 @@ let ith_mutual_inductive (kn, _) i = (kn, i) let ith_constructor_of_inductive ind i = (ind, i) let inductive_of_constructor (ind, i) = ind let index_of_constructor (ind, i) = i -let eq_ind (kn1, i1) (kn2, i2) = - i1 - i2 = 0 && eq_mind kn1 kn2 -let eq_constructor (kn1, i1) (kn2, i2) = - i1 - i2 = 0 && eq_ind kn1 kn2 + +let eq_ind (kn1, i1) (kn2, i2) = Int.equal i1 i2 && eq_mind kn1 kn2 + +let eq_constructor (kn1, i1) (kn2, i2) = Int.equal i1 i2 && eq_ind kn1 kn2 module Mindmap = Map.Make(Canonical_ord) module Mindset = Set.Make(Canonical_ord) @@ -343,13 +344,15 @@ module Mindmap_env = Map.Make(User_ord) module InductiveOrdered = struct type t = inductive let compare (spx,ix) (spy,iy) = - let c = ix - iy in if c = 0 then Canonical_ord.compare spx spy else c + let c = Int.compare ix iy in + if Int.equal c 0 then Canonical_ord.compare spx spy else c end module InductiveOrdered_env = struct type t = inductive let compare (spx,ix) (spy,iy) = - let c = ix - iy in if c = 0 then User_ord.compare spx spy else c + let c = Int.compare ix iy in + if Int.equal c 0 then User_ord.compare spx spy else c end module Indmap = Map.Make(InductiveOrdered) @@ -358,13 +361,15 @@ module Indmap_env = Map.Make(InductiveOrdered_env) module ConstructorOrdered = struct type t = constructor let compare (indx,ix) (indy,iy) = - let c = ix - iy in if c = 0 then InductiveOrdered.compare indx indy else c + let c = Int.compare ix iy in + if Int.equal c 0 then InductiveOrdered.compare indx indy else c end module ConstructorOrdered_env = struct type t = constructor let compare (indx,ix) (indy,iy) = - let c = ix - iy in if c = 0 then InductiveOrdered_env.compare indx indy else c + let c = Int.compare ix iy in + if Int.equal c 0 then InductiveOrdered_env.compare indx indy else c end module Constrmap = Map.Make(ConstructorOrdered) @@ -418,7 +423,7 @@ module Huniqid = Hashcons.Make( let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir) let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = (x == y) || - (n1 - n2 = 0 && s1 == s2 && dir1 == dir2) + (Int.equal n1 n2 && s1 == s2 && dir1 == dir2) let hash = Hashtbl.hash end) @@ -471,7 +476,7 @@ module Hind = Hashcons.Make( type t = inductive type u = mutual_inductive -> mutual_inductive let hashcons hmind (mind, i) = (hmind mind, i) - let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && i1 = i2 + let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 let hash = Hashtbl.hash end) @@ -480,7 +485,7 @@ module Hconstruct = Hashcons.Make( type t = constructor type u = inductive -> inductive let hashcons hind (ind, j) = (hind ind, j) - let equal (ind1,j1) (ind2,j2) = ind1 == ind2 && (j1 - j2 = 0) + let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2 let hash = Hashtbl.hash end) @@ -522,15 +527,14 @@ let eq_id_key ik1 ik2 = if ik1 == ik2 then true else match ik1,ik2 with | ConstKey (u1, kn1), ConstKey (u2, kn2) -> - let ans = (kn_ord u1 u2 = 0) in - if ans then kn_ord kn1 kn2 = 0 + let ans = Int.equal (kn_ord u1 u2) 0 in + if ans then Int.equal (kn_ord kn1 kn2) 0 else ans | VarKey id1, VarKey id2 -> - id_ord id1 id2 = 0 - | RelKey k1, RelKey k2 -> - k1 - k2 = 0 + Int.equal (id_ord id1 id2) 0 + | RelKey k1, RelKey k2 -> Int.equal k1 k2 | _ -> false -let eq_con_chk (kn1,_) (kn2,_) = kn1=kn2 -let eq_mind_chk (kn1,_) (kn2,_) = kn1=kn2 -let eq_ind_chk (kn1,i1) (kn2,i2) = i1=i2&&eq_mind_chk kn1 kn2 +let eq_con_chk (kn1,_) (kn2,_) = Int.equal (kn_ord kn1 kn2) 0 +let eq_mind_chk (kn1,_) (kn2,_) = Int.equal (kn_ord kn1 kn2) 0 +let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2 diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 76dcd1d3a..1d974eada 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -129,7 +129,7 @@ let beta_appvect c v = let betazeta_appvect n c v = let rec stacklam n env t stack = - if n = 0 then applist (substl env t, stack) else + if Int.equal n 0 then applist (substl env t, stack) else match kind_of_term t, stack with Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack @@ -205,7 +205,7 @@ let rec no_arg_available = function | [] -> true | Zupdate _ :: stk -> no_arg_available stk | Zshift _ :: stk -> no_arg_available stk - | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk + | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk | Zcase _ :: _ -> true | Zfix _ :: _ -> true diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index b8626e227..8b34950da 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -191,10 +191,10 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 | Cast(t,_,_) -> names_prod_letin t | _ -> [] in - assert (Array.length mib1.mind_packets = 1); - assert (Array.length mib2.mind_packets = 1); - assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1); - assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1); + assert (Int.equal (Array.length mib1.mind_packets) 1); + assert (Int.equal (Array.length mib2.mind_packets) 1); + assert (Int.equal (Array.length mib1.mind_packets.(0).mind_user_lc) 1); + assert (Int.equal (Array.length mib2.mind_packets.(0).mind_user_lc) 1); 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 diff --git a/kernel/term.ml b/kernel/term.ml index 0937fc16b..a99262adf 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -154,7 +154,7 @@ let mkLetIn (x,c1,t,c2) = LetIn (x,c1,t,c2) (* We ensure applicative terms have at least one argument and the function is not itself an applicative term *) let mkApp (f, a) = - if Array.length a = 0 then f else + if Int.equal (Array.length a) 0 then f else match f with | App (g, cl) -> App (g, Array.append cl a) | _ -> App (f, a) @@ -623,10 +623,13 @@ let constr_ord_int f t1 t2 = ((-) =? (Array.compare f)) e1 e2 l1 l2 | Const c1, Const c2 -> kn_ord (canonical_con c1) (canonical_con c2) | Ind (spx, ix), Ind (spy, iy) -> - let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c + let c = Int.compare ix iy in + if Int.equal c 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c | Construct ((spx, ix), jx), Construct ((spy, iy), jy) -> - let c = jx - jy in if c = 0 then - (let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c) + let c = Int.compare jx jy in + if Int.equal c 0 then + (let c = Int.compare ix iy in + if Int.equal c 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c) else c | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2 @@ -665,7 +668,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) = - id_ord i1 i2 = 0 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2 + Int.equal (id_ord i1 i2) 0 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2 let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) = n1 = n2 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2 @@ -805,7 +808,7 @@ let make_substituend c = { sinfo=Unknown; sit=c } let substn_many lamv n c = let lv = Array.length lamv in - if lv = 0 then c + if Int.equal lv 0 then c else let rec substrec depth c = match kind_of_term c with | Rel k -> @@ -947,7 +950,7 @@ let appvectc f l = mkApp (f,l) (* to_lambda n (x1:T1)...(xn:Tn)T = * [x1:T1]...[xn:Tn]T *) let rec to_lambda n prod = - if n = 0 then + if Int.equal n 0 then prod else match kind_of_term prod with @@ -956,7 +959,7 @@ let rec to_lambda n prod = | _ -> errorlabstrm "to_lambda" (mt ()) let rec to_prod n lam = - if n=0 then + if Int.equal n 0 then lam else match kind_of_term lam with diff --git a/kernel/univ.ml b/kernel/univ.ml index 635991494..bdd668cbd 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -58,7 +58,7 @@ module UniverseLevel = struct let equal u v = match u,v with | Set, Set -> true | Level (i1, dp1), Level (i2, dp2) -> - i1 = i2 && (Names.dir_path_ord dp1 dp2 = 0) + Int.equal i1 i2 && Int.equal (Names.dir_path_ord dp1 dp2) 0 | _ -> false let to_string = function @@ -725,7 +725,7 @@ let sort_universes orig = let accu, continue = UniverseLMap.fold (fun u x (accu, continue) -> let continue = continue || x < 0 in let accu = - if x = 0 && u != type0 then UniverseLMap.add u i accu + if Int.equal x 0 && u != type0 then UniverseLMap.add u i accu else accu in accu, continue) distances (accu, false) in diff --git a/kernel/vm.ml b/kernel/vm.ml index d4a86cb49..b6a39b042 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -169,7 +169,7 @@ type whd = let rec whd_accu a stk = let stk = - if Obj.size a = 2 then stk + if Int.equal (Obj.size a) 2 then stk else Zapp (Obj.obj a) :: stk in let at = Obj.field a 1 in match Obj.tag at with @@ -211,7 +211,7 @@ let whd_val : values -> whd = let tag = Obj.tag o in if tag = accu_tag then ( - if Obj.size o = 1 then Obj.obj o (* sort *) + if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *) else if is_accumulate (fun_code o) then whd_accu o [] else (Vprod(Obj.obj o))) @@ -255,7 +255,7 @@ let arg args i = let apply_arguments vf vargs = let n = nargs vargs in - if n = 0 then vf + if Int.equal n 0 then vf else begin push_ra stop; @@ -265,7 +265,7 @@ let apply_arguments vf vargs = let apply_vstack vf vstk = let n = Array.length vstk in - if n = 0 then vf + if Int.equal n 0 then vf else begin push_ra stop; @@ -502,7 +502,7 @@ let type_of_switch sw = interprete sw.sw_type_code crazy_val sw.sw_env 0 let branch_arg k (tag,arity) = - if arity = 0 then ((Obj.magic tag):values) + if Int.equal arity 0 then ((Obj.magic tag):values) else let b = Obj.new_block tag arity in for i = 0 to arity - 1 do diff --git a/lib/bigint.ml b/lib/bigint.ml index 9012d9322..be207f667 100644 --- a/lib/bigint.ml +++ b/lib/bigint.ml @@ -43,8 +43,8 @@ let size = let format_size = (* How to parametrize a printf format *) - if size = 4 then Printf.sprintf "%04d" - else if size = 9 then Printf.sprintf "%09d" + if Int.equal size 4 then Printf.sprintf "%04d" + else if Int.equal size 9 then Printf.sprintf "%09d" else fun n -> let rec aux j l n = if j=size then l else aux (j+1) (string_of_int (n mod 10) :: l) (n/10) @@ -73,7 +73,7 @@ let neg_one = [|-1|] let canonical n = let ok x = (0 <= x && x < base) in - let rec ok_tail k = (k = 0) || (ok n.(k) && ok_tail (k-1)) in + let rec ok_tail k = (Int.equal k 0) || (ok n.(k) && ok_tail (k-1)) in let ok_init x = (-base <= x && x < base && x <> -1 && x <> 0) in (n = [||]) || (n = [|-1|]) || @@ -83,7 +83,7 @@ let canonical n = let normalize_pos n = let k = ref 0 in - while !k < Array.length n & n.(!k) = 0 do incr k done; + while !k < Array.length n && Int.equal n.(!k) 0 do incr k done; Array.sub n !k (Array.length n - !k) (* [normalize_neg] : avoid (-1) as first bloc. @@ -94,16 +94,16 @@ let normalize_neg n = let k = ref 1 in while !k < Array.length n & n.(!k) = base - 1 do incr k done; let n' = Array.sub n !k (Array.length n - !k) in - if Array.length n' = 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n') + if Int.equal (Array.length n') 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n') (* [normalize] : avoid 0 and (-1) as first bloc. input: an array with first bloc in [-base;base[ and others in [0;base[ output: a canonical array *) let normalize n = - if Array.length n = 0 then n - else if n.(0) = -1 then normalize_neg n - else if n.(0) = 0 then normalize_pos n + if Int.equal (Array.length n) 0 then n + else if Int.equal n.(0) (-1) then normalize_neg n + else if Int.equal n.(0) 0 then normalize_pos n else n (* Opposite (expects and returns canonical arrays) *) @@ -112,8 +112,8 @@ let neg m = if m = zero then zero else let n = Array.copy m in let i = ref (Array.length m - 1) in - while !i > 0 & n.(!i) = 0 do decr i done; - if !i = 0 then begin + while !i > 0 && Int.equal n.(!i) 0 do decr i done; + if Int.equal !i 0 then begin n.(0) <- - n.(0); (* n.(0) cannot be 0 since m is canonical *) if n.(0) = -1 then normalize_neg n @@ -261,7 +261,7 @@ let euclid m d = let q = Array.create (ql+1) 0 in let i = ref 0 in while not (less_than_shift_pos !i m d) do - if m.(!i)=0 then incr i else + if Int.equal m.(!i) 0 then incr i else if can_divide !i m d 0 then begin let v = if Array.length d > 1 && d.(0) <> m.(!i) then @@ -297,14 +297,14 @@ let of_string s = let e = if h<>"" then 1 else 0 in let l = (len - !d) / size in let a = Array.create (l + e) 0 in - if e=1 then a.(0) <- int_of_string h; - for i=1 to l do + if Int.equal e 1 then a.(0) <- int_of_string h; + for i = 1 to l do a.(i+e-1) <- int_of_string (String.sub s ((i-1)*size + !d + r) size) done; if isneg then neg a else a let to_string_pos sgn n = - if Array.length n = 0 then "0" else + if Int.equal (Array.length n) 0 then "0" else sgn ^ String.concat "" (string_of_int n.(0) :: List.map format_size (List.tl (Array.to_list n))) @@ -342,7 +342,7 @@ let mkarray n = t let ints_of_int n = - if n = 0 then [| |] + if Int.equal n 0 then [| |] else if small n then [| n |] else mkarray n @@ -352,7 +352,7 @@ let of_int n = let of_ints n = let n = normalize n in (* TODO: using normalize here seems redundant now *) if n = zero then Obj.repr 0 else - if Array.length n = 1 then Obj.repr n.(0) else + if Int.equal (Array.length n) 1 then Obj.repr n.(0) else Obj.repr n let coerce_to_int = (Obj.magic : Obj.t -> int) @@ -366,7 +366,7 @@ let int_of_ints = let maxi = mkarray max_int and mini = mkarray min_int in fun t -> let l = Array.length t in - if (l > 3) || (l = 3 && (less_than maxi t || less_than t mini)) + if (l > 3) || (Int.equal l 3 && (less_than maxi t || less_than t mini)) then failwith "Bigint.to_int: too large"; let sum = ref 0 in let pow = ref 1 in diff --git a/lib/cArray.ml b/lib/cArray.ml index bdc084f44..4615ad038 100644 --- a/lib/cArray.ml +++ b/lib/cArray.ml @@ -280,8 +280,9 @@ let smartmap f ar = Array.init ar_size copy let map2 f v1 v2 = - if Array.length v1 <> Array.length v2 then invalid_arg "Array.map2"; - if Array.length v1 == 0 then + if not (Int.equal (Array.length v1) (Array.length v2)) then + invalid_arg "Array.map2"; + if Int.equal (Array.length v1) 0 then [| |] else begin let res = Array.create (Array.length v1) (f v1.(0) v2.(0)) in @@ -292,8 +293,9 @@ let map2 f v1 v2 = end let map2_i f v1 v2 = - if Array.length v1 <> Array.length v2 then invalid_arg "Array.map2"; - if Array.length v1 == 0 then + if not (Int.equal (Array.length v1) (Array.length v2)) then + invalid_arg "Array.map2"; + if Int.equal (Array.length v1) 0 then [| |] else begin let res = Array.create (Array.length v1) (f 0 v1.(0) v2.(0)) in @@ -306,7 +308,7 @@ let map2_i f v1 v2 = let map3 f v1 v2 v3 = if Array.length v1 <> Array.length v2 || Array.length v1 <> Array.length v3 then invalid_arg "Array.map3"; - if Array.length v1 == 0 then + if Int.equal (Array.length v1) 0 then [| |] else begin let res = Array.create (Array.length v1) (f v1.(0) v2.(0) v3.(0)) in @@ -318,7 +320,7 @@ let map3 f v1 v2 v3 = let map_left f a = (* Ocaml does not guarantee Array.map is LR *) let l = Array.length a in (* (even if so), then we rewrite it *) - if l = 0 then [||] else begin + if Int.equal l 0 then [||] else begin let r = Array.create l (f a.(0)) in for i = 1 to l - 1 do r.(i) <- f a.(i) @@ -328,7 +330,7 @@ let map_left f a = (* Ocaml does not guarantee Array.map is LR *) let iter2 f v1 v2 = let n = Array.length v1 in - if Array.length v2 <> n then invalid_arg "Array.iter2" + if not (Int.equal (Array.length v2) n) then invalid_arg "Array.iter2" else for i = 0 to n - 1 do f v1.(i) v2.(i) done let pure_functional = false diff --git a/lib/cList.ml b/lib/cList.ml index 62d1ec3c1..ee6b073ea 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -377,7 +377,7 @@ let interval n m = let addn n v = let rec aux n l = - if n = 0 then l + if Int.equal n 0 then l else aux (pred n) (v :: l) in if n < 0 then invalid_arg "List.addn" @@ -525,7 +525,7 @@ let rec remove_assoc_in_triple x = function let rec assoc_snd_in_triple x = function [] -> raise Not_found - | (a,b,_)::l -> if Pervasives.compare a x = 0 then b else assoc_snd_in_triple x l + | (a,b,_)::l -> if Int.equal (Pervasives.compare a x) 0 then b else assoc_snd_in_triple x l let add_set x l = if List.mem x l then l else x :: l @@ -587,7 +587,7 @@ let rec merge_uniq cmp l1 l2 = | l1, [] -> l1 | h1 :: t1, h2 :: t2 -> let c = cmp h1 h2 in - if c = 0 + if Int.equal c 0 then h1 :: merge_uniq cmp t1 t2 else if c <= 0 then h1 :: merge_uniq cmp t1 l2 diff --git a/lib/deque.ml b/lib/deque.ml index 58049b094..335a1a267 100644 --- a/lib/deque.ml +++ b/lib/deque.ml @@ -17,9 +17,9 @@ type 'a t = { let rec split i accu l = match l with | [] -> - if i = 0 then (accu, []) else invalid_arg "split" + if Int.equal i 0 then (accu, []) else invalid_arg "split" | t :: q -> - if i = 0 then (accu, l) + if Int.equal i 0 then (accu, l) else split (pred i) (t :: accu) q let balance q = @@ -88,7 +88,7 @@ let rev q = { let length q = q.lenf + q.lenr -let is_empty q = length q = 0 +let is_empty q = Int.equal (length q) 0 let filter f q = let fold (accu, len) x = if f x then (x :: accu, succ len) else (accu, len) in diff --git a/lib/envars.ml b/lib/envars.ml index b4c72b130..846391d83 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -51,7 +51,7 @@ let expand_path_macros ~warn s = let v = safe_getenv warn (String.sub s (i+1) (n-i-1)) in let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in expand_macros s (i + String.length v) - | '~' when i = 0 -> + | '~' when Int.equal i 0 -> let n = expand_atom s (i+1) in let v = if n=i+1 then home ~warn diff --git a/lib/fmap.ml b/lib/fmap.ml index 8ca56fe7a..21bd4b898 100644 --- a/lib/fmap.ml +++ b/lib/fmap.ml @@ -52,7 +52,7 @@ module Make = functor (X:Map.OrderedType) -> struct Node(Empty, x, data, Empty, 1) | Node(l, v, d, r, h) -> let c = X.compare x v in - if c = 0 then + if Int.equal c 0 then Node(l, x, data, r, h) else if c < 0 then bal (add x data l) v d r @@ -64,7 +64,7 @@ module Make = functor (X:Map.OrderedType) -> struct raise Not_found | Node(l, v, d, r, _) -> let c = X.compare x v in - if c = 0 then d + if Int.equal c 0 then d else find x (if c < 0 then l else r) let rec mem x = function @@ -72,7 +72,7 @@ module Make = functor (X:Map.OrderedType) -> struct false | Node(l, v, d, r, _) -> let c = X.compare x v in - c = 0 || mem x (if c < 0 then l else r) + Int.equal c 0 || mem x (if c < 0 then l else r) let rec min_binding = function Empty -> raise Not_found @@ -97,7 +97,7 @@ module Make = functor (X:Map.OrderedType) -> struct Empty | Node(l, v, d, r, h) -> let c = X.compare x v in - if c = 0 then + if Int.equal c 0 then merge l r else if c < 0 then bal (remove x l) v d r diff --git a/lib/fset.ml b/lib/fset.ml index 567feaa75..c93ce535d 100644 --- a/lib/fset.ml +++ b/lib/fset.ml @@ -93,7 +93,7 @@ struct (Empty, None, Empty) | Node(l, v, r, _) -> let c = X.compare x v in - if c = 0 then (l, Some v, r) + if Int.equal c 0 then (l, Some v, r) else if c < 0 then let (ll, vl, rl) = split x l in (ll, vl, join rl v r) else @@ -109,13 +109,13 @@ struct Empty -> false | Node(l, v, r, _) -> let c = X.compare x v in - c = 0 || mem x (if c < 0 then l else r) + Int.equal c 0 || mem x (if c < 0 then l else r) let rec add x = function Empty -> Node(Empty, x, Empty, 1) | Node(l, v, r, _) as t -> let c = X.compare x v in - if c = 0 then t else + if Int.equal c 0 then t else if c < 0 then bal (add x l) v r else bal l v (add x r) let singleton x = Node(Empty, x, Empty, 1) @@ -124,7 +124,7 @@ struct Empty -> Empty | Node(l, v, r, _) -> let c = X.compare x v in - if c = 0 then merge l r else + if Int.equal c 0 then merge l r else if c < 0 then bal (remove x l) v r else bal l v (remove x r) let rec union s1 s2 = @@ -133,12 +133,12 @@ struct | (t1, Empty) -> t1 | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> if h1 >= h2 then - if h2 = 1 then add v2 s1 else begin + if Int.equal h2 1 then add v2 s1 else begin let (l2, _, r2) = split v1 s2 in join (union l1 l2) v1 (union r1 r2) end else - if h1 = 1 then add v1 s2 else begin + if Int.equal h1 1 then add v1 s2 else begin let (l1, _, r1) = split v2 s1 in join (union l1 l2) v2 (union r1 r2) end @@ -184,7 +184,7 @@ struct compare_aux [s1] [s2] let equal s1 s2 = - compare s1 s2 = 0 + Int.equal (compare s1 s2) 0 let rec subset s1 s2 = match (s1, s2) with @@ -194,7 +194,7 @@ struct false | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) -> let c = X.compare v1 v2 in - if c = 0 then + if Int.equal c 0 then subset l1 l2 && subset r1 r2 else if c < 0 then subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2 diff --git a/lib/gmap.ml b/lib/gmap.ml index 08c99daff..65971b237 100644 --- a/lib/gmap.ml +++ b/lib/gmap.ml @@ -60,7 +60,7 @@ Node(Empty, x, data, Empty, 1) | Node(l, v, d, r, h) -> let c = Pervasives.compare x v in - if c = 0 then + if Int.equal c 0 then Node(l, x, data, r, h) else if c < 0 then bal (add x data l) v d r @@ -72,7 +72,7 @@ raise Not_found | Node(l, v, d, r, _) -> let c = Pervasives.compare x v in - if c = 0 then d + if Int.equal c 0 then d else find x (if c < 0 then l else r) let rec mem x = function @@ -80,7 +80,7 @@ false | Node(l, v, d, r, _) -> let c = Pervasives.compare x v in - c = 0 || mem x (if c < 0 then l else r) + Int.equal c 0 || mem x (if c < 0 then l else r) let rec min_binding = function Empty -> raise Not_found @@ -105,7 +105,7 @@ Empty | Node(l, v, d, r, h) -> let c = Pervasives.compare x v in - if c = 0 then + if Int.equal c 0 then merge l r else if c < 0 then bal (remove x l) v d r @@ -236,7 +236,7 @@ let rec pr_com ft s = Format.pp_print_as ft (utf8_length s1) s1; match os with Some s2 -> - if String.length s2 = 0 then (com_eol := true) + if Int.equal (String.length s2) 0 then (com_eol := true) else (Format.pp_force_newline ft (); pr_com ft s2) | None -> () @@ -441,14 +441,14 @@ let pr_vertical_list pr = function let prvecti_with_sep sep elem v = let rec pr i = - if i = 0 then + if Int.equal i 0 then elem 0 v.(0) else let r = pr (i-1) and s = sep () and e = elem i v.(i) in r ++ s ++ e in let n = Array.length v in - if n = 0 then mt () else pr (n - 1) + if Int.equal n 0 then mt () else pr (n - 1) (* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *) diff --git a/lib/util.ml b/lib/util.ml index 6a0ba470a..84249e6ae 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -65,7 +65,7 @@ let strip s = let string_map f s = let l = String.length s in let r = String.create l in - for i= 0 to (l - 1) do r.[i] <- f (s.[i]) done; + for i = 0 to (l - 1) do r.[i] <- f (s.[i]) done; r let drop_simple_quotes s = @@ -118,7 +118,7 @@ let split_string_at c s = with | Not_found -> [String.sub s n (len-n)] in - if len = 0 then [] else split 0 + if Int.equal len 0 then [] else split 0 let parse_loadpath s = let l = split_string_at '/' s in @@ -207,14 +207,8 @@ let delayed_force f = f () type ('a,'b) union = Inl of 'a | Inr of 'b -module IntOrd = -struct - type t = int - external compare : int -> int -> int = "caml_int_compare" -end - -module Intset = Set.Make(IntOrd) -module Intmap = Map.Make(IntOrd) +module Intset = Set.Make(Int) +module Intmap = Map.Make(Int) (*s interruption *) diff --git a/library/lib.ml b/library/lib.ml index 688df5a0e..212e23578 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -452,7 +452,7 @@ let section_segment_of_mutual_inductive kn = let rec list_mem_assoc x = function | [] -> raise Not_found - | (a,_)::l -> compare a x = 0 or list_mem_assoc x l + | (a, _) :: l -> Int.equal (Names.id_ord a x) 0 || list_mem_assoc x l let section_instance = function | VarRef id -> diff --git a/library/libnames.ml b/library/libnames.ml index 197588f53..a07895eec 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -92,7 +92,7 @@ let sp_ord sp1 sp2 = let (p1,id1) = repr_path sp1 and (p2,id2) = repr_path sp2 in let p_bit = compare p1 p2 in - if p_bit = 0 then id_ord id1 id2 else p_bit + if Int.equal p_bit 0 then id_ord id1 id2 else p_bit module SpOrdered = struct diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 293520a55..dd32c99ba 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -229,9 +229,9 @@ let extend_constr_notation ng = (** Grammar declaration for Tactic Notation (Coq level) *) let get_tactic_entry n = - if n = 0 then + if Int.equal n 0 then weaken_entry Tactic.simple_tactic, None - else if n = 5 then + else if Int.equal n 5 then weaken_entry Tactic.binder_tactic, None else if 1<=n && n<5 then weaken_entry Tactic.tactic_expr, Some (Extend.Level (string_of_int n)) @@ -264,7 +264,7 @@ let head_is_ident tg = match tg.tacgram_prods with let add_tactic_entry tg = let entry, pos = get_tactic_entry tg.tacgram_level in let rules = - if tg.tacgram_level = 0 then begin + if Int.equal tg.tacgram_level 0 then begin if not (head_is_ident tg) then error "Notation for simple tactic must start with an identifier."; let mkact loc l = @@ -293,7 +293,7 @@ let recover_notation_grammar ntn prec = Some (vars, ng) | _ -> None in let l = List.map_filter filter !grammar_state in - assert (List.length l = 1); + let () = match l with [_] -> () | _ -> assert false in List.hd l (* Summary functions: the state of the lexer is included in that of the parser. diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml index be584b5c8..3e1c44e5a 100644 --- a/parsing/extrawit.ml +++ b/parsing/extrawit.ml @@ -49,7 +49,7 @@ let rawwit_tactic = function | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n) let tactic_genarg_level s = - if String.length s = 7 && String.sub s 0 6 = "tactic" then + if Int.equal (String.length s) 7 && String.sub s 0 6 = "tactic" then let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48) else None else None diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index a811b29b8..485b5b280 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -227,7 +227,7 @@ let linkmonad f lnkvar = let linklift lnkvar i = linkmonad (fun x -> x+i) lnkvar (* This map is used to deal with debruijn linked indices. *) -module Link = Map.Make (struct type t = int let compare = Pervasives.compare end) +module Link = Map.Make (Int) let pr_links l = Printf.printf "links:\n"; diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index beb7b4819..d42d612ae 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -243,7 +243,7 @@ let rec add_term t0 = function * MODULE: Ordered set of integers. *) -module ISet = Set.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end) +module ISet = Set.Make(Int) (** * Given a set of integers s={i0,...,iN} and a list m, return the list of diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index d9201722d..571c789c2 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -89,7 +89,7 @@ type vector = Vect.t {coeffs = v ; bound = (l,r) } models the constraints l <= v <= r **) -module ISet = Set.Make(struct type t = int let compare = Pervasives.compare end) +module ISet = Set.Make(Int) module PSet = ISet @@ -437,7 +437,7 @@ let elim_var_using_eq vr vect cst prf sys = (** [size sys] computes the number of entries in the system of constraints *) let size sys = System.fold (fun v iref s -> s + (!iref).neg + (!iref).pos) sys 0 -module IMap = Map.Make(struct type t = int let compare : int -> int -> int = Pervasives.compare end) +module IMap = Map.Make(Int) let pp_map o map = IMap.fold (fun k elt () -> Printf.fprintf o "%i -> %s\n" k (string_of_num elt)) map () diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index 1f7c083e2..339e10661 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -585,7 +585,7 @@ struct module MonT = struct module MonoMap = Map.Make(Monomial) - module IntMap = Map.Make(struct type t = int let compare = Pervasives.compare end) + module IntMap = Map.Make(Int) (** A hash table might be preferable but requires a hash function. *) let (index_of_monomial : int MonoMap.t ref) = ref (MonoMap.empty) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 7b6be410b..e7300fcea 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -988,7 +988,7 @@ let adjust_predicate_from_tomatch tomatch (current,typ as ct) pb = let rec ungeneralize n ng body = match kind_of_term body with - | Lambda (_,_,c) when ng = 0 -> + | Lambda (_,_,c) when Int.equal ng 0 -> subst1 (mkRel n) c | Lambda (na,t,c) -> (* We traverse an inner generalization *) @@ -1046,8 +1046,8 @@ let rec irrefutable env = function | PatCstr (_,cstr,args,_) -> let ind = inductive_of_constructor cstr in let (_,mip) = Inductive.lookup_mind_specif env ind in - let one_constr = Array.length mip.mind_user_lc = 1 in - one_constr & List.for_all (irrefutable env) args + let one_constr = Int.equal (Array.length mip.mind_user_lc) 1 in + one_constr && List.for_all (irrefutable env) args let first_clause_irrefutable env = function | eqn::mat -> List.for_all (irrefutable env) eqn.patterns @@ -1419,7 +1419,7 @@ let push_binder d (k,env,subst) = let rec list_assoc_in_triple x = function [] -> raise Not_found - | (a,b,_)::l -> if compare a x = 0 then b else list_assoc_in_triple x l + | (a, b, _)::l -> if Int.equal a x then b else list_assoc_in_triple x l (* Let vijk and ti be a set of dependent terms and T a type, all * defined in some environment env. The vijk and ti are supposed to be @@ -1682,7 +1682,7 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c = let signlen = List.length sign in match kind_of_term tm with | Rel n when dependent tm c - && signlen = 1 (* The term to match is not of a dependent type itself *) -> + && Int.equal signlen 1 (* The term to match is not of a dependent type itself *) -> ((n, len) :: subst, len - signlen) | Rel n when signlen > 1 (* The term is of a dependent type, maybe some variable in its type appears in the tycon. *) -> @@ -2162,7 +2162,7 @@ let build_dependent_signature env evars avoid tomatchs arsign = ([], 0, [], nar, []) tomatchs arsign in let arsign'' = List.rev arsign' in - assert(slift = 0); (* we must have folded over all elements of the arity signature *) + assert(Int.equal slift 0); (* we must have folded over all elements of the arity signature *) arsign'', allnames, nar, eqs, neqs, refls let context_of_arsign l = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index b417dc1d4..405e089a6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -69,7 +69,8 @@ let nfirsts_app_of_stack n s = let (args, _) = strip_app s in List.firstn n args let list_of_app_stack s = let (out,s') = strip_app s in - Option.init (s' = []) out + let init = match s' with [] -> true | _ -> false in + Option.init init out let array_of_app_stack s = Option.map Array.of_list (list_of_app_stack s) let rec zip = function @@ -93,7 +94,7 @@ let rec stack_assign s p c = match s with | _ -> assert false) | _ -> s let rec stack_tail p s = - if p = 0 then s else + if Int.equal p 0 then s else match s with | Zapp args :: s -> let q = List.length args in @@ -188,11 +189,11 @@ module RedFlags = (struct let fiota = 16 let fzeta = 32 let mkflags = List.fold_left (lor) 0 - let red_beta f = f land fbeta <> 0 - let red_delta f = f land fdelta <> 0 - let red_eta f = f land feta <> 0 - let red_iota f = f land fiota <> 0 - let red_zeta f = f land fzeta <> 0 + let red_beta f = not (Int.equal (f land fbeta) 0) + let red_delta f = not (Int.equal (f land fdelta) 0) + let red_eta f = not (Int.equal (f land feta) 0) + let red_iota f = not (Int.equal (f land fiota) 0) + let red_zeta f = not (Int.equal (f land fzeta) 0) end : RedFlagsSig) open RedFlags @@ -319,7 +320,7 @@ let rec whd_state_gen flags ts env sigma = match kind_of_term x' with | Rel 1 when l' = empty_stack -> let lc = Array.sub cl 0 (napp-1) in - let u = if napp=1 then f else appvect (f,lc) in + let u = if Int.equal napp 1 then f else appvect (f,lc) in if noccurn 1 u then (pop u,empty_stack) else s | _ -> s else s @@ -375,7 +376,7 @@ let local_whd_state_gen flags sigma = match kind_of_term x' with | Rel 1 when l' = empty_stack -> let lc = Array.sub cl 0 (napp-1) in - let u = if napp=1 then f else appvect (f,lc) in + let u = if Int.equal napp 1 then f else appvect (f,lc) in if noccurn 1 u then (pop u,empty_stack) else s | _ -> s else s @@ -690,7 +691,9 @@ let plain_instance s c = | _ -> map_constr_with_binders succ irec n u in - if s = [] then c else irec 0 c + match s with + | [] -> c + | _ -> irec 0 c (* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota] has (unfortunately) different subtle side effects: @@ -804,7 +807,7 @@ let splay_arity env sigma c = let sort_of_arity env sigma c = snd (splay_arity env sigma c) let splay_prod_n env sigma n = - let rec decrec env m ln c = if m = 0 then (ln,c) else + let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else match kind_of_term (whd_betadeltaiota env sigma c) with | Prod (n,a,c0) -> decrec (push_rel (n,None,a) env) @@ -814,7 +817,7 @@ let splay_prod_n env sigma n = decrec env n empty_rel_context let splay_lam_n env sigma n = - let rec decrec env m ln c = if m = 0 then (ln,c) else + let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else match kind_of_term (whd_betadeltaiota env sigma c) with | Lambda (n,a,c0) -> decrec (push_rel (n,None,a) env) @@ -941,7 +944,9 @@ let meta_instance sigma b = List.map (fun mv -> (mv,meta_value sigma mv)) (Metaset.elements b.freemetas) in - if c_sigma = [] then b.rebus else instance sigma c_sigma b.rebus + match c_sigma with + | [] -> b.rebus + | _ -> instance sigma c_sigma b.rebus let nf_meta sigma c = meta_instance sigma (mk_freelisted c) @@ -981,7 +986,9 @@ let meta_reducible_instance evd b = with Not_found -> u) | _ -> map_constr irec u in - if fm = [] then (* nf_betaiota? *) b.rebus else irec b.rebus + match fm with + | [] -> (* nf_betaiota? *) b.rebus + | _ -> irec b.rebus let head_unfold_under_prod ts env _ c = diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 97ce40a77..29d0fa05e 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -959,7 +959,7 @@ let unfold env sigma name = let unfoldoccs env sigma (occs,name) c = let unfo nowhere_except_in locs = let (nbocc,uc) = substlin env name 1 (nowhere_except_in,locs) c in - if nbocc = 1 then + if Int.equal nbocc 1 then error ((string_of_evaluable_ref env name)^" does not occur."); let rest = List.filter (fun o -> o >= nbocc) locs in if rest <> [] then error_invalid_occurrence rest; diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 2585d4489..836997228 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -221,7 +221,7 @@ let lookup_rel_id id sign = | [] -> raise Not_found | (Anonymous, _, _) :: l -> lookrec (n + 1) l | (Name id', b, t) :: l -> - if Names.id_ord id' id = 0 then (n, b, t) else lookrec (n + 1) l + if Int.equal (Names.id_ord id' id) 0 then (n, b, t) else lookrec (n + 1) l in lookrec 1 sign @@ -258,7 +258,7 @@ let rec strip_head_cast c = match kind_of_term c with let rec collapse_rec f cl2 = match kind_of_term f with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) | Cast (c,_,_) -> collapse_rec c cl2 - | _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2) + | _ -> if Int.equal (Array.length cl2) 0 then f else mkApp (f,cl2) in collapse_rec f cl | Cast (c,_,_) -> strip_head_cast c @@ -342,7 +342,7 @@ let fold_rec_types g (lna,typarray,_) e = let map_left2 f a g b = let l = Array.length a in - if l = 0 then [||], [||] else begin + if Int.equal l 0 then [||], [||] else begin let r = Array.create l (f a.(0)) in let s = Array.create l (g b.(0)) in for i = 1 to l - 1 do @@ -911,7 +911,7 @@ let eq_constr = constr_cmp Reduction.CONV let split_app c = match kind_of_term c with App(c,l) -> let len = Array.length l in - if len=0 then ([],c) else + if Int.equal len 0 then ([],c) else let last = Array.get l (len-1) in let prev = Array.sub l 0 (len-1) in c::(Array.to_list prev), last @@ -981,7 +981,7 @@ let rec eta_reduce_head c = (match kind_of_term cl.(lastn) with | Rel 1 -> let c' = - if lastn = 1 then f + if Int.equal lastn 1 then f else mkApp (f, Array.sub cl 0 lastn) in if noccurn 1 c' diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 447ee8e3b..856c5e147 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -395,7 +395,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag let tyN = get_type_of curenv sigma cN in check_compatibility curenv substn tyM tyN); (* Here we check that [cN] does not contain any local variables *) - if nb = 0 then + if Int.equal nb 0 then sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst else if noccur_between 1 nb cN then (sigma, @@ -409,7 +409,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag let tyN = Typing.meta_type sigma k in check_compatibility curenv substn tyM tyN); (* Here we check that [cM] does not contain any local variables *) - if nb = 0 then + if Int.equal nb 0 then (sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst) else if noccur_between 1 nb cM then @@ -771,7 +771,7 @@ let merge_instances env sigma flags st1 st2 c1 c2 = let applyHead env evd n c = let rec apprec n c cty evd = - if n = 0 then + if Int.equal n 0 then (evd, c) else match kind_of_term (whd_betadeltaiota env evd cty) with diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 25ea991e7..ebda3cb76 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -321,7 +321,7 @@ let split_product na' = function | _ -> anomaly "ill-formed fixpoint body" let rec split_fix n typ def = - if n = 0 then ([],typ,def) + if Int.equal n 0 then ([],typ,def) else let (na,_,def) = split_lambda def in let (na,t,typ) = split_product na typ in diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 2ec66bb34..26e9f9eb5 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -621,9 +621,10 @@ let pr_fix_tac (id,n,c) = ln nal) [] bll in let idarg,bll = set_nth_name names n bll in - let annot = - if List.length names = 1 then mt() - else spc() ++ str"{struct " ++ pr_id idarg ++ str"}" in + let annot = match names with + | [_] -> mt () + | _ -> spc() ++ str"{struct " ++ pr_id idarg ++ str"}" + in hov 1 (str"(" ++ pr_id id ++ prlist pr_binder_fix bll ++ annot ++ str" :" ++ pr_lconstrarg ty ++ str")") in @@ -973,7 +974,7 @@ in (pr_tac, pr_match_rule) let strip_prod_binders_glob_constr n (ty,_) = let rec strip_ty acc n ty = - if n=0 then (List.rev acc, (ty,None)) else + if Int.equal n 0 then (List.rev acc, (ty,None)) else match ty with Glob_term.GProd(loc,na,Explicit,a,b) -> strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 476504549..721d9b6c8 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -495,7 +495,7 @@ let rec pr_vernac = function | VernacUnfocused -> str"Unfocused" | VernacGoal c -> str"Goal" ++ pr_lconstrarg c | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id - | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i + | VernacUndo i -> if Int.equal i 1 then str"Undo" else str"Undo" ++ pr_intarg i | VernacUndoTo i -> str"Undo" ++ spc() ++ str"To" ++ pr_intarg i | VernacBacktrack (i,j,k) -> str "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k] @@ -523,7 +523,7 @@ let rec pr_vernac = function (* Resetting *) | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id | VernacResetInitial -> str"Reset Initial" - | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i + | VernacBack i -> if Int.equal i 1 then str"Back" else str"Back" ++ pr_intarg i | VernacBackTo i -> str"BackTo" ++ pr_intarg i (* State management *) @@ -634,9 +634,9 @@ let rec pr_vernac = function let pr_constructor_list b l = match l with | Constructors [] -> mt() | Constructors l -> + let fst_sep = match l with [_] -> " " | _ -> " | " in pr_com_at (begin_of_inductive l) ++ - fnl() ++ - str (if List.length l = 1 then " " else " | ") ++ + fnl() ++ str fst_sep ++ prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l | RecordDecl (c,fs) -> spc() ++ diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 5bc3161b9..78bdc194f 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -304,8 +304,8 @@ let tclDO n t = let rec dorec k = if k < 0 then errorlabstrm "Refiner.tclDO" (str"Wrong argument : Do needs a positive integer."); - if k = 0 then tclIDTAC - else if k = 1 then t else (tclTHEN t (dorec (k-1))) + if Int.equal k 0 then tclIDTAC + else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1))) in dorec n @@ -339,7 +339,7 @@ let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) (* Repeat on the first subgoal (no failure if no more subgoal) *) let rec tclREPEAT_MAIN t g = - (tclORELSE (tclTHEN_i t (fun i -> if i = 1 then (tclREPEAT_MAIN t) else + (tclORELSE (tclTHEN_i t (fun i -> if Int.equal i 1 then (tclREPEAT_MAIN t) else tclIDTAC)) tclIDTAC) g (*s Tactics handling a list of goals. *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 97c954b8a..8daf11c70 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -77,7 +77,7 @@ type hint_entry = global_reference option * types gen_auto_tactic let pri_order_int (id1, {pri=pri1}) (id2, {pri=pri2}) = let d = pri1 - pri2 in - if d == 0 then id2 - id1 + if Int.equal d 0 then id2 - id1 else d let pri_order t1 t2 = pri_order_int t1 t2 <= 0 diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index e8cde2967..819c76807 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -81,7 +81,7 @@ struct | _ -> Dn.Nothing let bounded_constr_pat_discr_st st (t,depth) = - if depth = 0 then + if Int.equal depth 0 then None else match Term_dn.constr_pat_discr_st st t with @@ -89,7 +89,7 @@ struct | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) let bounded_constr_val_discr_st st (t,depth) = - if depth = 0 then + if Int.equal depth 0 then Dn.Nothing else match constr_val_discr_st st t with @@ -98,7 +98,7 @@ struct | Dn.Everything -> Dn.Everything let bounded_constr_pat_discr (t,depth) = - if depth = 0 then + if Int.equal depth 0 then None else match Term_dn.constr_pat_discr t with @@ -106,7 +106,7 @@ struct | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) let bounded_constr_val_discr (t,depth) = - if depth = 0 then + if Int.equal depth 0 then Dn.Nothing else match constr_val_discr t with diff --git a/tactics/dn.ml b/tactics/dn.ml index a0889ab8f..ea19ecc41 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -16,7 +16,7 @@ struct None,None -> 0 | Some (l,n),Some (l',n') -> let m = Y.compare l l' in - if m = 0 then + if Int.equal m 0 then n-n' else m | Some(l,n),None -> 1 @@ -26,7 +26,7 @@ struct type t = X.t * Z.t let compare (x1,x2) (y1,y2) = let m = (X.compare x1 y1) in - if m = 0 then (Z.compare x2 y2) else + if Int.equal m 0 then (Z.compare x2 y2) else m end @@ -65,7 +65,7 @@ prefix ordering, [dna] is the function returning the main node of a pattern *) try [T.map tm lbl, true] with Not_found -> [] let rec skip_arg n tm = - if n = 0 then [tm,true] + if Int.equal n 0 then [tm,true] else List.flatten (List.map diff --git a/tactics/equality.ml b/tactics/equality.ml index 9827b6146..63cdbfa92 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -296,14 +296,14 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars frze {elimindex = None; elimbody = (elim,NoBindings)} gl let adjust_rewriting_direction args lft2rgt = - if List.length args = 1 then begin + match args with + | [_] -> (* equality to a constant, like in eq_true *) (* more natural to see -> as the rewriting to the constant *) if not lft2rgt then error "Rewriting non-symmetric equality not allowed from right-to-left."; None - end - else + | _ -> (* other equality *) Some lft2rgt @@ -931,7 +931,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let { intro = exist_term } = find_sigma_data sort_of_ty in let evdref = ref (Evd.create_goal_evar_defs sigma) in let rec sigrec_clausal_form siglen p_i = - if siglen = 0 then + if Int.equal siglen 0 then (* is the default value typable with the expected type *) let dflt_typ = type_of env sigma dflt in if Evarconv.e_cumul env evdref dflt_typ p_i then diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 69cee2148..20a52c21c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -179,7 +179,7 @@ let fix_empty_or_and_pattern nv l = let check_or_and_pattern_size loc names n = if List.length names <> n then - if n = 1 then + if Int.equal n 1 then user_err_loc (loc,"",str "Expects a conjunctive pattern.") else user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e55ba5d0e..39c669f42 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1211,7 +1211,7 @@ let keep hyps gl = (************************) let check_number_of_constructors expctdnumopt i nconstr = - if i=0 then error "The constructors are numbered starting from 1."; + if Int.equal i 0 then error "The constructors are numbered starting from 1."; begin match expctdnumopt with | Some n when n <> nconstr -> error ("Not an inductive goal with "^ @@ -1243,7 +1243,7 @@ let any_constructor with_evars tacopt gl = let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in let nconstr = Array.length (snd (Global.lookup_inductive mind)).mind_consnames in - if nconstr = 0 then error "The type has no constructors."; + if Int.equal nconstr 0 then error "The type has no constructors."; tclFIRST (List.map (fun i -> tclTHEN (constructor_tac with_evars None i NoBindings) t) @@ -1286,9 +1286,9 @@ let error_unexpected_extra_pattern loc nb pat = | IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no" | _ -> "introduction pattern", "", "none" in user_err_loc (loc,"",str "Unexpected " ++ str s1 ++ str " (" ++ - (if nb = 0 then (str s3 ++ str s2) else + (if Int.equal nb 0 then (str s3 ++ str s2) else (str "at most " ++ int nb ++ str s2)) ++ spc () ++ - str (if nb = 1 then "was" else "were") ++ + str (if Int.equal nb 1 then "was" else "were") ++ strbrk " expected in the branch).") let intro_or_and_pattern loc b ll l' tac id gl = @@ -1297,9 +1297,9 @@ let intro_or_and_pattern loc b ll l' tac id gl = let nv = mis_constr_nargs ind in let bracketed = b or not (l'=[]) in let rec adjust_names_length nb n = function - | [] when n = 0 or not bracketed -> [] + | [] when Int.equal n 0 or not bracketed -> [] | [] -> (dloc,IntroAnonymous) :: adjust_names_length nb (n-1) [] - | (loc',pat) :: _ as l when n = 0 -> + | (loc',pat) :: _ as l when Int.equal n 0 -> if bracketed then error_unexpected_extra_pattern loc' nb pat; l | ip :: l -> ip :: adjust_names_length nb (n-1) l in @@ -2239,7 +2239,7 @@ let empty_scheme = } let make_base n id = - if n=0 or n=1 then id + if Int.equal n 0 || Int.equal n 1 then id else (* This extends the name to accept new digits if it already ends with *) (* digits *) @@ -2260,7 +2260,7 @@ let make_up_names n ind_opt cname = else add_prefix ind_prefix cname in let hyprecname = make_base n base_ind in let avoid = - if n=1 (* Only one recursive argument *) or n=0 then [] + if Int.equal n 1 (* Only one recursive argument *) or Int.equal n 0 then [] else (* Forbid to use cname, cname0, hyprecname and hyprecname0 *) (* in order to get names such as f1, f2, ... *) @@ -2618,13 +2618,15 @@ let decompose_paramspred_branch_args elimt = type (See for example Empty_set_ind, as False would actually be ok). Then we must find the predicate of the conclusion to separate params_pred from args. We suppose there is only one predicate here. *) - if List.length acc2 <> 0 then acc1, acc2 , acc3, ccl - else + match acc2 with + | [] -> let hyps,ccl = decompose_prod_assum elimt in let hd_ccl_pred,_ = decompose_app ccl in - match kind_of_term hd_ccl_pred with + begin match kind_of_term hd_ccl_pred with | Rel i -> let acc3,acc1 = cut_list (i-1) hyps in acc1 , [] , acc3 , ccl | _ -> error_ind_scheme "" + end + | _ -> acc1, acc2 , acc3, ccl let exchange_hd_app subst_hd t = @@ -2694,7 +2696,7 @@ let compute_elim_sig ?elimc elimt = raise Exit end; (* 2- If no args_indargs (=!res.nargs at this point) then no indarg *) - if !res.nargs=0 then raise Exit; + if Int.equal !res.nargs 0 then raise Exit; (* 3- Look at last arg: is it the indarg? *) ignore ( match List.hd args_indargs with @@ -3166,7 +3168,7 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc gl = args *) let induct_destruct isrec with_evars (lc,elim,names,cls) gl = assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *) - if List.length lc = 1 && not (is_functional_induction elim gl) then + if Int.equal (List.length lc) 1 && not (is_functional_induction elim gl) then (* standard induction *) onOpenInductionArg (fun c -> new_induct_gen isrec with_evars elim names c cls) @@ -3182,7 +3184,8 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl = error "'in' clause not supported here."; let lc = List.map (map_induction_arg (pf_apply finish_evar_resolution gl)) lc in - if List.length lc = 1 then + begin match lc with + | [_] -> (* Hook to recover standard induction on non-standard induction schemes *) (* will be removable when is_functional_induction will be more clever *) onInductionArg @@ -3190,7 +3193,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl = if lbind <> NoBindings then error "'with' clause not supported here."; new_induct_gen_l isrec with_evars elim names [c]) (List.hd lc) gl - else + | _ -> let newlc = List.map (fun x -> match x with (* FIXME: should we deal with ElimOnIdent? *) @@ -3198,6 +3201,7 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) gl = | _ -> error "Don't know where to find some argument.") lc in new_induct_gen_l isrec with_evars elim names newlc gl + end end let induction_destruct isrec with_evars = function diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml index 2d919e966..4e4b2135d 100644 --- a/toplevel/backtrack.ml +++ b/toplevel/backtrack.ml @@ -146,7 +146,7 @@ let sync nb_opened_proofs = the end. *) let back count = - if count = 0 then 0 + if Int.equal count 0 then 0 else let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in npop count; diff --git a/toplevel/class.ml b/toplevel/class.ml index ff0e9fcfb..87310302c 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -242,7 +242,7 @@ let add_new_coercion_core coef stre source target isid = if coercion_exists coef then raise (CoercionError AlreadyExists); let tg,lp = prods_of t in let llp = List.length lp in - if llp = 0 then raise (CoercionError NotAFunction); + if Int.equal llp 0 then raise (CoercionError NotAFunction); let (cls,lvs,ind) = try get_source lp source diff --git a/toplevel/command.ml b/toplevel/command.ml index edde7c652..f707ea508 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -36,7 +36,7 @@ open Indschemes open Misctypes let rec under_binders env f n c = - if n = 0 then f env Evd.empty c else + if Int.equal n 0 then f env Evd.empty c else match kind_of_term c with | Lambda (x,t,c) -> mkLambda (x,t,under_binders (push_rel (x,None,t) env) f (n-1) c) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index c0027ef03..b6d1f981c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -312,7 +312,7 @@ let explain_ill_typed_rec_body env sigma i names vdefj vargs = let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in let pv = pr_lconstr_env env vargs.(i) in str "The " ++ - (if Array.length vdefj = 1 then mt () else pr_nth (i+1) ++ spc ()) ++ + (if Int.equal (Array.length vdefj) 1 then mt () else pr_nth (i+1) ++ spc ()) ++ str "recursive definition" ++ spc () ++ pvd ++ spc () ++ str "has type" ++ spc () ++ pvdt ++ spc () ++ str "while it should be" ++ spc () ++ pv ++ str "." @@ -809,7 +809,7 @@ let error_ill_formed_inductive env c v = let error_ill_formed_constructor env id c v nparams nargs = let pv = pr_lconstr_env env v in - let atomic = (nb_prod c = 0) in + let atomic = Int.equal (nb_prod c) 0 in str "The type of constructor" ++ brk(1,1) ++ pr_id id ++ brk(1,1) ++ str "is not valid;" ++ brk(1,1) ++ strbrk (if atomic then "it must be " else "its conclusion must be ") ++ @@ -917,8 +917,8 @@ let explain_bad_constructor env cstr ind = str "is expected." let decline_string n s = - if n = 0 then "no "^s^"s" - else if n = 1 then "1 "^s + if Int.equal n 0 then "no "^s^"s" + else if Int.equal n 1 then "1 "^s else (string_of_int n^" "^s^"s") let explain_wrong_numarg_constructor env cstr n = @@ -1020,7 +1020,7 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c) (List.rev vars @ unboundvars) ++ str ")" else mt())) ++ - (if n=2 then str " (repeated twice)" + (if Int.equal n 2 then str " (repeated twice)" else if n>2 then str " (repeated "++int n++str" times)" else mt()) in if calls <> [] then diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 747f5835f..a49305292 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -292,7 +292,7 @@ let start_proof_with_initialization kind recguard thms snl hook = else tacl)),guard | None -> - assert (List.length thms = 1); + let () = match thms with [_] -> () | _ -> assert false in (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in match thms with | [] -> anomaly "No proof to start" diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index ed6b45228..345147157 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -35,7 +35,7 @@ let cache_token (_,s) = Lexer.add_keyword s let inToken : string -> obj = declare_object {(default_object "TOKEN") with - open_function = (fun i o -> if i=1 then cache_token o); + open_function = (fun i o -> if Int.equal i 1 then cache_token o); cache_function = cache_token; subst_function = Libobject.ident_subst_function; classify_function = (fun o -> Substitute o)} @@ -84,7 +84,7 @@ let classify_tactic_notation tacobj = let inTacticGrammar : tactic_grammar_obj -> obj = declare_object {(default_object "TacticGrammar") with - open_function = (fun i o -> if i=1 then cache_tactic_notation o); + open_function = (fun i o -> if Int.equal i 1 then cache_tactic_notation o); cache_function = cache_tactic_notation; subst_function = subst_tactic_notation; classify_function = classify_tactic_notation} @@ -180,7 +180,7 @@ let parse_format ((loc, str) : lstring) = | cur::l -> (a::cur)::l | [] -> [[a]] in let push_white n l = - if n = 0 then l else push_token (UnpTerminal (String.make n ' ')) l in + if Int.equal n 0 then l else push_token (UnpTerminal (String.make n ' ')) l in let close_box i b = function | a::(_::_ as l) -> push_token (UnpBox (b,a)) l | _ -> error "Non terminated box in format." in @@ -195,7 +195,7 @@ let parse_format ((loc, str) : lstring) = if i < String.length str & str.[i] <> ' ' then if str.[i] = '\'' & quoted & (i+1 >= String.length str or str.[i+1] = ' ') - then if n=0 then error "Empty quoted token." else n + then if Int.equal n 0 then error "Empty quoted token." else n else nonspaces quoted (n+1) (i+1) else if quoted then error "Spaces are not allowed in (quoted) symbols." @@ -240,7 +240,7 @@ let parse_format ((loc, str) : lstring) = push_token (UnpTerminal (String.sub str (i-1) (n+2))) (parse_token (close_quotation (i+n)))) else - if n = 0 then [] + if Int.equal n 0 then [] else error "Ending spaces non part of a format annotation." and parse_box box i = let n = spaces 0 i in @@ -760,7 +760,7 @@ let classify_syntax_definition (local, _ as o) = let inSyntaxExtension : syntax_extension_obj -> obj = declare_object {(default_object "SYNTAX-EXTENSION") with - open_function = (fun i o -> if i = 1 then cache_syntax_extension o); + open_function = (fun i o -> if Int.equal i 1 then cache_syntax_extension o); cache_function = cache_syntax_extension; subst_function = subst_syntax_extension; classify_function = classify_syntax_definition} @@ -1008,7 +1008,7 @@ let open_notation i (_, nobj) = let scope = nobj.notobj_scope in let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in - if i = 1 & not (Notation.exists_notation_in_scope scope ntn pat) then begin + if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin (* Declare the interpretation *) Notation.declare_notation_interpretation ntn scope pat df; (* Declare the uninterpretation *) @@ -1229,7 +1229,7 @@ let load_scope_command _ (_,(scope,dlm)) = Notation.declare_scope scope let open_scope_command i (_,(scope,o)) = - if i=1 then + if Int.equal i 1 then match o with | ScopeDelim dlm -> Notation.declare_delimiters scope dlm | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 6277faf27..5210a3c9e 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -149,7 +149,7 @@ let trunc_named_context n ctx = List.firstn (len - n) ctx let rec chop_product n t = - if n = 0 then Some t + if Int.equal n 0 then Some t else match kind_of_term t with | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None @@ -645,7 +645,7 @@ let get_prog_err n = let get_any_prog_err () = try get_any_prog () with NoObligations id -> pperror (explain_no_obligations id) -let obligations_solved prg = (snd prg.prg_obligations) = 0 +let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0 let all_programs () = ProgMap.fold (fun k p l -> p :: l) !from_prg [] @@ -657,7 +657,7 @@ type progress = let obligations_message rem = if rem > 0 then - if rem = 1 then + if Int.equal rem 1 then Flags.if_verbose msg_info (int rem ++ str " obligation remaining") else Flags.if_verbose msg_info (int rem ++ str " obligations remaining") @@ -898,7 +898,7 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic let info = str (string_of_id n) ++ str " has type-checked" in let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in let obls,_ = prg.prg_obligations in - if Array.length obls = 0 then ( + if Int.equal (Array.length obls) 0 then ( Flags.if_verbose msg_info (info ++ str "."); let cst = declare_definition prg in Defined cst) diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index ec390683f..175a95165 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -56,8 +56,8 @@ let emacs_prompt_endstring() = Printer.emacs_str "</prompt>" beginning of line. *) let prompt_char ic ibuf count = let bol = match ibuf.bols with - | ll::_ -> ibuf.len == ll - | [] -> ibuf.len == 0 + | ll::_ -> Int.equal ibuf.len ll + | [] -> Int.equal ibuf.len 0 in if bol && not !print_emacs then msgerr (str (ibuf.prompt())); try diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7cff9a4ec..42b9411f8 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -170,7 +170,9 @@ let restore_timeout = function let open_utf8_file_in fname = let is_bom s = - Char.code s.[0] = 0xEF && Char.code s.[1] = 0xBB && Char.code s.[2] = 0xBF + Int.equal (Char.code s.[0]) 0xEF && + Int.equal (Char.code s.[1]) 0xBB && + Int.equal (Char.code s.[2]) 0xBF in let in_chan = open_in fname in let s = " " in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 42c36f519..71f7f39a3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -259,7 +259,7 @@ let print_namespace ns = begin match match_dirpath ns dir with | Some [] as y -> y | Some (a::ns') -> - if Names.id_ord a id = 0 then Some ns' + if Int.equal (Names.id_ord a id) 0 then Some ns' else None | None -> None end @@ -272,7 +272,7 @@ let print_namespace ns = begin match match_modulepath ns mp with | Some [] as y -> y | Some (a::ns') -> - if Names.id_ord a id = 0 then Some ns' + if Int.equal (Names.id_ord a id) 0 then Some ns' else None | None -> None end @@ -1551,7 +1551,7 @@ let vernac_undoto n = let vernac_focus gln = let p = Proof_global.give_me_the_proof () in let n = match gln with None -> 1 | Some n -> n in - if n = 0 then + if Int.equal n 0 then Errors.error "Invalid goal number: 0. Goal numbering starts with 1." else Proof.focus focus_command_cond () n p; print_subgoals () |