extracted/lists.ml

   1 open Preamble
   2
   3 open Bool
   4
   5 open Relations
   6
   7 open Nat
   8
   9 open Hints_declaration
  10
  11 open Core_notation
  12
  13 open Pts
  14
  15 open Logic
  16
  17 open Types
  18
  19 open List
  20
  21 open Div_and_mod
  22
  23 open Jmeq
  24
  25 open Russell
  26
  27 open Util
  28
  29 (** val all : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
  30 let rec all p = function
  31 | List.Nil -> Bool.True
  32 | List.Cons (h, t) -> Bool.andb (p h) (all p t)
  33
  34 (** val map_All : ('a1 -> __ -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
  35 let rec map_All f l =
  36   (match l with
  37    | List.Nil -> (fun _ -> List.Nil)
  38    | List.Cons (hd, tl) -> (fun _ -> List.Cons ((f hd __), (map_All f tl))))
  39     __
  40
  41 open Setoids
  42
  43 open Monad
  44
  45 open Option
  46
  47 (** val append : 'a1 List.list List.aop **)
  48 let append =
  49   List.append
  50
  51 (** val list : Monad.monadProps **)
  52 let list =
  53   Monad.makeMonadProps (fun _ x -> List.Cons (x, List.Nil)) (fun _ _ l f ->
  54     List.foldr (fun x -> List.append (f x)) List.Nil l)
  55
  56 (** val count : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
  57 let rec count f = function
  58 | List.Nil -> Nat.O
  59 | List.Cons (x, l') ->
  60   Nat.plus
  61     (match f x with
  62      | Bool.True -> Nat.S Nat.O
  63      | Bool.False -> Nat.O) (count f l')
  64
  65 (** val position_of_safe : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
  66 let position_of_safe test l =
  67   Option.opt_safe (List.position_of test l)
  68
  69 (** val index_of : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
  70 let index_of test l =
  71   position_of_safe test l
  72
  73 (** val ordered_insert :
  74     ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> 'a1 List.list **)
  75 let rec ordered_insert lt a = function
  76 | List.Nil -> List.Cons (a, List.Nil)
  77 | List.Cons (h, t) ->
  78   (match lt a h with
  79    | Bool.True -> List.Cons (a, (List.Cons (h, t)))
  80    | Bool.False -> List.Cons (h, (ordered_insert lt a t)))
  81
  82 (** val insert_sort :
  83     ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list **)
  84 let rec insert_sort lt = function
  85 | List.Nil -> List.Nil
  86 | List.Cons (h, t) -> ordered_insert lt h (insert_sort lt t)
  87
  88 (** val range_strong_internal :
  89     Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat Types.sig0 List.list **)
  90 let rec range_strong_internal index how_many end0 =
  91   (match how_many with
  92    | Nat.O -> (fun _ -> List.Nil)
  93    | Nat.S k ->
  94      (fun _ -> List.Cons (index,
  95        (range_strong_internal (Nat.S index) k end0)))) __
  96
  97 (** val range_strong : Nat.nat -> Nat.nat Types.sig0 List.list **)
  98 let range_strong end0 =
  99   range_strong_internal Nat.O end0 end0
 100