Quelle range.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)         *)
(************************************************************************)

type 'a tree =
| Leaf of 'a
| Node of 'a * 'a tree * 'a tree

type 'a t = Nil | Cons of int * 'a tree * 'a t

let oob () = invalid_arg "index out of bounds"

let empty = Nil

let cons x l = match l with
| Cons (h1, t1, Cons (h2, t2, rem)) ->
  if Int.equal h1 h2 then Cons (1 + h1 + h2, Node (x, t1, t2), rem)
  else Cons (1, Leaf x, l)
| _ -> Cons (1, Leaf x, l)

let is_empty = function
| Nil -> true
| _ -> false

let rec tree_get h t i = match t with
| Leaf x ->
  if i = 0 then x else oob ()
| Node (x, t1, t2) ->
  if i = 0 then x
  else
    let h = h / 2 in
    if i <= h then tree_get h t1 (i - 1) else tree_get h t2 (i - h - 1)

let rec get l i = match l with
| Nil -> oob ()
| Cons (h, t, rem) ->
  if i < h then tree_get h t i else get rem (i - h)

let length l =
  let rec length accu = function
  | Nil -> accu
  | Cons (h, _, l) -> length (h + accu) l
  in
  length 0 l

let rec tree_map f = function
| Leaf x -> Leaf (f x)
| Node (x, t1, t2) -> Node (f x, tree_map f t1, tree_map f t2)

let rec map f = function
| Nil -> Nil
| Cons (h, t, l) -> Cons (h, tree_map f t, map f l)

let rec tree_fold_left f accu = function
| Leaf x -> f accu x
| Node (x, t1, t2) ->
  tree_fold_left f (tree_fold_left f (f accu x) t1) t2

let rec fold_left f accu = function
| Nil -> accu
| Cons (_, t, l) -> fold_left f (tree_fold_left f accu t) l

let rec tree_fold_right f t accu = match t with
| Leaf x -> f x accu
| Node (x, t1, t2) ->
  f x (tree_fold_right f t1 (tree_fold_right f t2 accu))

let rec fold_right f l accu = match l with
| Nil -> accu
| Cons (_, t, l) -> tree_fold_right f t (fold_right f l accu)

let hd = function
| Nil -> failwith "hd"
| Cons (_, Leaf x, _) -> x
| Cons (_, Node (x, _, _), _) -> x

let tl = function
| Nil -> failwith "tl"
| Cons (_, Leaf _, l) -> l
| Cons (h, Node (_, t1, t2), l) ->
  let h = h / 2 in
  Cons (h, t1, Cons (h, t2, l))

let rec skipn n l =
  if n = 0 then l
  else if is_empty l then failwith "List.skipn"
  else skipn (pred n) (tl l)

quality99%

¤ Dauer der Verarbeitung: 0.12 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.