diff options
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | lib/cList.ml | 7 | ||||
| -rw-r--r-- | lib/cList.mli | 2 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 2 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 2 | ||||
| -rw-r--r-- | printing/prettyp.ml | 2 |
6 files changed, 13 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8a86d3022..d4cb79775 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1386,7 +1386,7 @@ let internalize globalenv env allow_patvar lvar c = let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in let ro = f (intern env') in - let n' = Option.map (fun _ -> List.length (List.filter (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore)) n in + let n' = Option.map (fun _ -> List.count (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore) n in n', ro, List.fold_left intern_local_binder (env',rbefore) after in let n, ro, (env',rbl) = diff --git a/lib/cList.ml b/lib/cList.ml index 0ac372d8d..72f892a09 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -48,6 +48,7 @@ sig val filteri : (int -> 'a -> bool) -> 'a list -> 'a list val smartfilter : ('a -> bool) -> 'a list -> 'a list + val count : ('a -> bool) -> 'a list -> int val index : 'a eq -> 'a -> 'a list -> int val index0 : 'a eq -> 'a -> 'a list -> int val iteri : (int -> 'a -> unit) -> 'a list -> unit @@ -375,6 +376,12 @@ let rec smartfilter f l = match l with else h :: tl' else tl' +let count f l = + let rec aux acc = function + | [] -> acc + | h :: t -> if f h then aux (acc + 1) t else aux acc t in + aux 0 l + let rec index_f f x l n = match l with | [] -> raise Not_found | y :: l -> if f x y then n else index_f f x l (succ n) diff --git a/lib/cList.mli b/lib/cList.mli index 19eeb2509..1487f67a3 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -94,6 +94,8 @@ sig (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i [f ai = true], then [smartfilter f l == l] *) + val count : ('a -> bool) -> 'a list -> int + val index : 'a eq -> 'a -> 'a list -> int (** [index] returns the 1st index of an element in a list (counting from 1). *) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 7fde7b7ac..af4865401 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -299,7 +299,7 @@ let check_and_decompose_canonical_structure ref = | Construct ((indsp,1),u) -> indsp | _ -> error_not_structure ref in let s = try lookup_structure indsp with Not_found -> error_not_structure ref in - let ntrue_projs = List.length (List.filter (fun (_, x) -> x) s.s_PROJKIND) in + let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then error_not_structure ref; (sp,indsp) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index deb03f516..c44fbc0ba 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -436,7 +436,7 @@ let instance_constructor (cl,u) args = | None -> true | Some _ -> false in - let lenpars = List.length (List.filter filter (snd cl.cl_context)) in + let lenpars = List.count filter (snd cl.cl_context) in let pars = fst (List.chop lenpars args) in match cl.cl_impl with | IndRef ind -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 84649e6eb..08228cb20 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -132,7 +132,7 @@ let print_renames_list prefix l = let need_expansion impl ref = let typ = Global.type_of_global_unsafe ref in let ctx = prod_assum typ in - let nprods = List.length (List.filter (fun (_,b,_) -> Option.is_empty b) ctx) in + let nprods = List.count (fun (_,b,_) -> Option.is_empty b) ctx in not (List.is_empty impl) && List.length impl >= nprods && let _,lastimpl = List.chop nprods impl in List.exists is_status_implicit lastimpl |