Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Roqc/clib/ (Beweissystem des Inria Version 9.1.0^©) Datei vom 15.8.2025 mit Größe 18 kB

Quelle cArray.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

module type S = module type of Array

include Array

let uget = Array.unsafe_get

(* Arrays *)

let compare cmp v1 v2 =
  if v1 == v2 then 0
  else
    let len = Array.length v1 in
    let c = Int.compare len (Array.length v2) in
    if c <> 0 then c else
      let rec loop i =
        if i < 0 then 0
        else
          let x = uget v1 i in
          let y = uget v2 i in
          let c = cmp x y in
          if c <> 0 then c
          else loop (i - 1)
      in
      loop (len - 1)

let equal_norefl cmp t1 t2 =
  let len = Array.length t1 in
  if not (Int.equal len (Array.length t2)) then false
  else
    let rec aux i =
      if i < 0 then true
      else
        let x = uget t1 i in
        let y = uget t2 i in
        cmp x y && aux (pred i)
    in
    aux (len - 1)

let equal cmp t1 t2 =
  if t1 == t2 then true else equal_norefl cmp t1 t2

let is_empty array = Int.equal (Array.length array) 0

let exists2 f v1 v2 =
  let rec exrec = function
    | -1 -> false
    | n -> f (uget v1 n) (uget v2 n) || (exrec (n-1))
  in
  let lv1 = Array.length v1 in
  lv1 = Array.length v2 && exrec (lv1-1)

let for_all2 f v1 v2 =
  let rec allrec = function
    | -1 -> true
    | n ->
      let ans = f (uget v1 n) (uget v2 n) in
      ans && (allrec (n-1))
  in
  let lv1 = Array.length v1 in
  lv1 = Array.length v2 && allrec (pred lv1)

let for_all3 f v1 v2 v3 =
  let rec allrec = function
    | -1 -> true
    | n ->
      let ans = f (uget v1 n)
        (uget v2 n) (uget v3 n)
      in
      ans && (allrec (n-1))
  in
  let lv1 = Array.length v1 in
  lv1 = Array.length v2 && lv1 = Array.length v3 && allrec (pred lv1)

let for_all4 f v1 v2 v3 v4 =
  let rec allrec = function
    | -1 -> true
    | n ->
      let ans = f (uget v1 n)
        (uget v2 n) (uget v3 n) (uget v4 n)
      in
      ans && (allrec (n-1))
  in
  let lv1 = Array.length v1 in
  lv1 = Array.length v2 &&
  lv1 = Array.length v3 &&
  lv1 = Array.length v4 &&
  allrec (pred lv1)

let for_all_i f i v =
  let len = Array.length v in
  let rec allrec i n =
    n = len || f i (uget v n) && allrec (i+1) (n+1) in
  allrec i 0

exception Found of int

let findi (pred: int -> 'a -> bool) (arr: 'a array) : int option =
  try
    for i=0 to Array.length arr - 1 do
      if pred i (uget arr i) then raise (Found i) done;
    None
  with Found i -> Some i

let find2_map (type a) pred arr1 arr2 =
  let exception Found of a in
  let n = Array.length arr1 in
  if not (Array.length arr2 = n) then failwith "Array.find2_map";
  try
    for i=0 to n - 1 do
      match pred (Array.unsafe_get arr1 i) (Array.unsafe_get arr2 i) with
      | Some r -> raise (Found r)
      | None -> ()
    done;
    None
  with Found i -> Some i

let hd v =
  match Array.length v with
    | 0 -> failwith "Array.hd"
    | _ -> uget v 0

let tl v =
  match Array.length v with
    | 0 -> failwith "Array.tl"
    | n -> Array.sub v 1 (pred n)

let last v =
  match Array.length v with
    | 0 -> failwith "Array.last"
    | n -> uget v (pred n)

let cons e v =
  let len = Array.length v in
  let ans = Array.make (Array.length v + 1) e in
  let () = Array.blit v 0 ans 1 len in
  ans

let rev t =
  let n=Array.length t in
    if n <=0 then ()
    else
      for i = 0 to pred (n/2) do
        let tmp = uget t ((pred n)-i) in
        Array.unsafe_set t ((pred n)-i) (uget t i);
        Array.unsafe_set t i tmp
      done

let fold_right_i f v a =
  let rec fold a n =
    if n=0 then a
    else
      let k = n-1 in
      fold (f k (uget v k) a) k in
  fold a (Array.length v)

let fold_left_i f v a =
  let n = Array.length a in
  let rec fold i v = if i = n then v else fold (succ i) (f i v (uget a i)) in
  fold 0 v

let fold_right2 f v1 v2 a =
  let lv1 = Array.length v1 in
  let rec fold a n =
    if n=0 then a
    else
      let k = n-1 in
      fold (f (uget v1 k) (uget v2 k) a) k in
  if Array.length v2 <> lv1 then invalid_arg "Array.fold_right2";
  fold a lv1

let fold_left2 f a v1 v2 =
  let lv1 = Array.length v1 in
  let rec fold a n =
    if n >= lv1 then a else fold (f a (uget v1 n) (uget v2 n)) (succ n)
  in
  if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2";
  fold a 0

let fold_left2_i f a v1 v2 =
  let lv1 = Array.length v1 in
  let rec fold a n =
    if n >= lv1 then a else fold (f n a (uget v1 n) (uget v2 n)) (succ n)
  in
  if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2_i";
  fold a 0

let fold_right3 f v1 v2 v3 a =
  let lv1 = Array.length v1 in
  let rec fold a n =
    if n=0 then a
    else
      let k = n-1 in
      fold (f (uget v1 k) (uget v2 k) (uget v3 k) a) k in
  if Array.length v2 <> lv1 || Array.length v3 <> lv1 then invalid_arg "Array.fold_right3";
  fold a lv1

let fold_left3 f a v1 v2 v3 =
  let lv1 = Array.length v1 in
  let rec fold a n =
    if n >= lv1 then a
    else fold (f a (uget v1 n) (uget v2 n) (uget v3 n)) (succ n)
  in
  if Array.length v2 <> lv1 || Array.length v3 <> lv1 then
    invalid_arg "Array.fold_left3";
  fold a 0

let fold_left3_i f a v1 v2 v3 =
  let lv1 = Array.length v1 in
  let rec fold a n =
    if n >= lv1 then a else fold (f n a (uget v1 n) (uget v2 n) (uget v3 n)) (succ n)
  in
  if Array.length v2 <> lv1 || Array.length v3 <> lv1 then
    invalid_arg "Array.fold_left3_i";
  fold a 0

let fold_left4 f a v1 v2 v3 v4 =
  let lv1 = Array.length v1 in
  let rec fold a n =
    if n >= lv1 then a
    else fold (f a (uget v1 n) (uget v2 n) (uget v3 n) (uget v4 n)) (succ n)
  in
  if Array.length v2 <> lv1 || Array.length v3 <> lv1 || Array.length v4 <> lv1 then
    invalid_arg "Array.fold_left4";
  fold a 0

let fold_left_from n f a v =
  let len = Array.length v in
  let () = if n < 0 then invalid_arg "Array.fold_left_from" in
  let rec fold a n =
    if n >= len then a else fold (f a (uget v n)) (succ n)
  in
  fold a n

let rev_of_list = function
| [] -> [| |]
| x :: l ->
  let len = List.length l in
  let ans = Array.make (succ len) x in
  let rec set i = function
  | [] -> ()
  | x :: l ->
    Array.unsafe_set ans i x;
    set (pred i) l
  in
  let () = set (len - 1) l in
  ans

let map_to_list = CList.map_of_array

let map_of_list f l =
  let len = List.length l in
  let rec fill i v = function
  | [] -> ()
  | x :: l ->
    Array.unsafe_set v i (f x);
    fill (succ i) v l
  in
  match l with
  | [] -> [||]
  | x :: l ->
    let ans = Array.make len (f x) in
    let () = fill 1 ans l in
    ans

let chop n v =
  let vlen = Array.length v in
  if n > vlen then failwith "Array.chop";
  (Array.sub v 0 n, Array.sub v n (vlen-n))

let split v =
  (Array.map fst v, Array.map snd v)

let split3 v =
  (Array.map (fun (a, _, _) -> a) v,
   Array.map (fun (_, b, _) -> b) v,
   Array.map (fun (_, _, c) -> c) v)

let split4 v =
  (Array.map (fun (a, _, _, _) -> a) v,
   Array.map (fun (_, b, _, _) -> b) v,
   Array.map (fun (_, _, c, _) -> c) v,
   Array.map (fun (_, _, _, d) -> d) v)

let transpose a =
  let n = Array.length a in
  if n = 0 then [||] else
  let n' = Array.length (Array.unsafe_get a 0) in
  Array.init n' (fun i -> Array.init n (fun j -> a.(j).(i)))

let map2_i f v1 v2 =
  let len1 = Array.length v1 in
  let len2 = Array.length v2 in
  let () = if not (Int.equal len1 len2) then invalid_arg "Array.map2" in
  if Int.equal len1 0 then
    [| |]
  else begin
    let res = Array.make len1 (f 0 (uget v1 0) (uget v2 0)) in
    for i = 1 to pred len1 do
      Array.unsafe_set res i (f i (uget v1 i) (uget v2 i))
    done;
    res
  end

let map3 f v1 v2 v3 =
  let len1 = Array.length v1 in
  let () =
    if len1 <> Array.length v2 || len1 <> Array.length v3
    then invalid_arg "Array.map3"
  in
  if Int.equal len1 0 then
    [| |]
  else begin
    let res = Array.make len1 (f (uget v1 0) (uget v2 0) (uget v3 0)) in
    for i = 1 to pred len1 do
      Array.unsafe_set res i (f (uget v1 i) (uget v2 i) (uget v3 i))
    done;
    res
  end

let map3_i f v1 v2 v3 =
  let len1 = Array.length v1 in
  let len2 = Array.length v2 in
  let len3 = Array.length v3 in
  let () = if not (Int.equal len1 len2 && Int.equal len1 len3) then invalid_arg "Array.map3_i" in
  if Int.equal len1 0 then
    [| |]
  else begin
    let res = Array.make len1 (f 0 (uget v1 0) (uget v2 0) (uget v3 0)) in
    for i = 1 to pred len1 do
      Array.unsafe_set res i (f i (uget v1 i) (uget v2 i) (uget v3 i))
    done;
    res
  end

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 Int.equal l 0 then [||] else begin
    let r = Array.make l (f (uget a 0)) in
    for i = 1 to l - 1 do
      Array.unsafe_set r i (f (uget a i))
    done;
    r
  end

let iter2_i f v1 v2 =
  let len1 = Array.length v1 in
  let len2 = Array.length v2 in
  let () = if not (Int.equal len2 len1) then invalid_arg "Array.iter2" in
  for i = 0 to len1 - 1 do f i (uget v1 i) (uget v2 i) done

let iter3 f v1 v2 v3 =
  let len1 = Array.length v1 in
  let len2 = Array.length v2 in
  let len3 = Array.length v3 in
  let () = if not (Int.equal len2 len1) || not (Int.equal len1 len3) then invalid_arg "Array.iter3" in
  for i = 0 to len1 - 1 do f (uget v1 i) (uget v2 i) (uget v3 i) done

let map_right f a =
  let l = length a in
  if l = 0 then [||] else begin
    let r = Array.make l (f (unsafe_get a (l-1))) in
    for i = l-2 downto 0 do
      unsafe_set r i (f (unsafe_get a i))
    done;
    r
  end

let map2_right f a b =
  let l = length a in
  if l <> length b then invalid_arg "CArray.map2_right: length mismatch";
  if l = 0 then [||] else begin
    let r = Array.make l (f (unsafe_get a (l-1)) (unsafe_get b (l-1))) in
    for i = l-2 downto 0 do
      unsafe_set r i (f (unsafe_get a i) (unsafe_get b i))
    done;
    r
  end

let fold_right_map f v e =
  let e' = ref e in
  let v' = map_right (fun x -> let (y,e) = f x !e' in e' := e; y) v in
  (v',!e')

let fold_left_map f e v =
  let e' = ref e in
  let v' = Array.map (fun x -> let (e,y) = f !e' x in e' := e; y) v in
  (!e',v')

let fold_right2_map f v1 v2 e =
  let e' = ref e in
  let v' =
    map2_right (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2
  in
  (v',!e')

let fold_left2_map f e v1 v2 =
  let e' = ref e in
  let v' = map2 (fun x1 x2 -> let (e,y) = f !e' x1 x2 in e' := e; y) v1 v2 in
  (!e',v')

let fold_left_map_i f e v =
  let e' = ref e in
  let v' = mapi (fun idx x -> let (e,y) = f idx !e' x in e' := e; y) v in
  (!e',v')

let fold_left2_map_i f e v1 v2 =
  let e' = ref e in
  let v' = map2_i (fun idx x1 x2 -> let (e,y) = f idx !e' x1 x2 in e' := e; y) v1 v2 in
  (!e',v')

let distinct v =
  let visited = Hashtbl.create 23 in
  try
    Array.iter
      (fun x ->
        if Hashtbl.mem visited x then raise_notrace Exit
        else Hashtbl.add visited x x)
      v;
    true
  with Exit -> false

let rev_to_list a =
  let rec tolist i res =
    if i >= Array.length a then res else tolist (i+1) (uget a i :: res) in
  tolist 0 []

let filter_with filter v =
  Array.of_list (CList.filter_with filter (Array.to_list v))

module Smart =
struct

  (* If none of the elements is changed by f we return ar itself.
     The while loop looks for the first such an element.
     If found, we break here and the new array is produced,
     but f is not re-applied to elements that are already checked *)
  let map f (ar : 'a array) =
    let len = Array.length ar in
    let i = ref 0 in
    let break = ref true in
    let temp = ref None in
    while !break && (!i < len) do
      let v = Array.unsafe_get ar !i in
      let v' = f v in
      if v == v' then incr i
      else begin
        break := false;
        temp := Some v';
      end
    done;
    if !i < len then begin
      (* The array is not the same as the original one *)
      let ans : 'a array = Array.copy ar in
      let v = match !temp with None -> assert false | Some x -> x in
      Array.unsafe_set ans !i v;
      incr i;
      while !i < len do
        let v = Array.unsafe_get ans !i in
        let v' = f v in
        if v != v' then Array.unsafe_set ans !i v';
        incr i
      done;
      ans
    end else ar

  (* Same as map_i but smart *)
  let map_i f (ar : 'a array) =
    let len = Array.length ar in
    let i = ref 0 in
    let break = ref true in
    let temp = ref None in
    while !break && (!i < len) do
      let v = Array.unsafe_get ar !i in
      let v' = f !i v in
      if v == v' then incr i
      else begin
        break := false;
        temp := Some v';
      end
    done;
    if !i < len then begin
      (* The array is not the same as the original one *)
      let ans : 'a array = Array.copy ar in
      let v = match !temp with None -> assert false | Some x -> x in
      Array.unsafe_set ans !i v;
      incr i;
      while !i < len do
        let v = Array.unsafe_get ans !i in
        let v' = f !i v in
        if v != v' then Array.unsafe_set ans !i v';
        incr i
      done;
      ans
    end else ar

  let map2 f aux_ar ar =
    let len = Array.length ar in
    let aux_len = Array.length aux_ar in
    let () = if not (Int.equal len aux_len) then invalid_arg "Array.Smart.map2" in
    let i = ref 0 in
    let break = ref true in
    let temp = ref None in
    while !break && (!i < len) do
      let v = Array.unsafe_get ar !i in
      let w = Array.unsafe_get aux_ar !i in
      let v' = f w v in
      if v == v' then incr i
      else begin
        break := false;
        temp := Some v';
      end
    done;
    if !i < len then begin
      (* The array is not the same as the original one *)
      let ans : 'a array = Array.copy ar in
      let v = match !temp with None -> assert false | Some x -> x in
      Array.unsafe_set ans !i v;
      incr i;
      while !i < len do
        let v = Array.unsafe_get ans !i in
        let w = Array.unsafe_get aux_ar !i in
        let v' = f w v in
        if v != v' then Array.unsafe_set ans !i v';
        incr i
      done;
      ans
    end else ar

  (** Same as [Smart.map] but threads a state meanwhile *)
  let fold_left_map f accu (ar : 'a array) =
    let len = Array.length ar in
    let i = ref 0 in
    let break = ref true in
    let r = ref accu in
    (* This variable is never accessed unset *)
    let temp = ref None in
    while !break && (!i < len) do
      let v = Array.unsafe_get ar !i in
      let (accu, v') = f !r v in
      r := accu;
      if v == v' then incr i
      else begin
        break := false;
        temp := Some v';
      end
    done;
    if !i < len then begin
      let ans : 'a array = Array.copy ar in
      let v = match !temp with None -> assert false | Some x -> x in
      Array.unsafe_set ans !i v;
      incr i;
      while !i < len do
        let v = Array.unsafe_get ar !i in
        let (accu, v') = f !r v in
        r := accu;
        if v != v' then Array.unsafe_set ans !i v';
        incr i
      done;
      !r, ans
    end else !r, ar

  (** Same as [Smart.mapi] but threads a state meanwhile *)
  let fold_left_map_i f accu (ar : 'a array) =
    let len = Array.length ar in
    let i = ref 0 in
    let break = ref true in
    let r = ref accu in
    (* This variable is never accessed unset *)
    let temp = ref None in
    while !break && (!i < len) do
      let v = Array.unsafe_get ar !i in
      let (accu, v') = f !i !r v in
      r := accu;
      if v == v' then incr i
      else begin
        break := false;
        temp := Some v';
      end
    done;
    if !i < len then begin
      let ans : 'a array = Array.copy ar in
      let v = match !temp with None -> assert false | Some x -> x in
      Array.unsafe_set ans !i v;
      incr i;
      while !i < len do
        let v = Array.unsafe_get ar !i in
        let (accu, v') = f !i !r v in
        r := accu;
        if v != v' then Array.unsafe_set ans !i v';
        incr i
      done;
      !r, ans
    end else !r, ar

  (** Same as [Smart.map2] but threads a state meanwhile *)
  let fold_left2_map f accu aux_ar ar =
    let len = Array.length ar in
    let aux_len = Array.length aux_ar in
    let () = if not (Int.equal len aux_len) then invalid_arg "Array.Smart.fold_left2_map" in
    let i = ref 0 in
    let break = ref true in
    let r = ref accu in
    (* This variable is never accessed unset *)
    let temp = ref None in
    while !break && (!i < len) do
      let v = Array.unsafe_get ar !i in
      let w = Array.unsafe_get aux_ar !i in
      let (accu, v') = f !r w v in
      r := accu;
      if v == v' then incr i
      else begin
        break := false;
        temp := Some v';
      end
    done;
    if !i < len then begin
      let ans : 'a array = Array.copy ar in
      let v = match !temp with None -> assert false | Some x -> x in
      Array.unsafe_set ans !i v;
      incr i;
      while !i < len do
        let v = Array.unsafe_get ar !i in
        let w = Array.unsafe_get aux_ar !i in
        let (accu, v') = f !r w v in
        r := accu;
        if v != v' then Array.unsafe_set ans !i v';
        incr i
      done;
      !r, ans
    end else !r, ar

end

module Fun1 =
struct

  let map f arg v = match v with
  | [| |] -> [| |]
  | _ ->
    let len = Array.length v in
    let x0 = Array.unsafe_get v 0 in
    let ans = Array.make len (f arg x0) in
    for i = 1 to pred len do
      let x = Array.unsafe_get v i in
      Array.unsafe_set ans i (f arg x)
    done;
    ans

  let iter f arg v =
    let len = Array.length v in
    for i = 0 to pred len do
      let x = uget v i in
      f arg x
    done

  let iter2 f arg v1 v2 =
    let len1 = Array.length v1 in
    let len2 = Array.length v2 in
    let () = if not (Int.equal len2 len1) then invalid_arg "Array.Fun1.iter2" in
    for i = 0 to pred len1 do
      let x1 = uget v1 i in
      let x2 = uget v2 i in
      f arg x1 x2
    done

  module Smart =
  struct

    let map f arg (ar : 'a array) =
      let len = Array.length ar in
      let i = ref 0 in
      let break = ref true in
      let temp = ref None in
      while !break && (!i < len) do
        let v = Array.unsafe_get ar !i in
        let v' = f arg v in
        if v == v' then incr i
        else begin
          break := false;
          temp := Some v';
        end
      done;
      if !i < len then begin
        (* The array is not the same as the original one *)
        let ans : 'a array = Array.copy ar in
        let v = match !temp with None -> assert false | Some x -> x in
        Array.unsafe_set ans !i v;
        incr i;
        while !i < len do
          let v = Array.unsafe_get ans !i in
          let v' = f arg v in
          if v != v' then Array.unsafe_set ans !i v';
          incr i
        done;
        ans
      end else ar

  end

end

quality99%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.