aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol-light/TacticRecording/lib.ml
blob: b1309f847185a0e05b868a03e8d0769e562e1360 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82

let rec copy n x =
  if (n > 0) then x::(copy (n-1) x)
             else [];;


let rec enumerate0 n xs =
  match xs with
    []     -> []
  | x::xs0 -> (n,x)::enumerate0 (n+1) xs0;;
let enumerate xs = enumerate0 1 xs;;


(* foldr : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b                            *)

let rec foldr f xs a =
  match xs with
    x1::xs2 -> f x1 (foldr f xs2 a)
  | []      -> a;;


(* foldl : ('b -> 'a -> 'b) -> 'b -> 'a list -> 'b                            *)

let rec foldl f a xs =
  match xs with
    x1::xs2 -> foldl f (f a x1) xs2
  | []      -> a;;


(* is_empty *)

let is_empty xs =
  match xs with
    [] -> true
  | _  -> false;;


(* front *)

let rec front xs =
  match xs with
    _::[]   -> []
  | x0::xs0 -> x0::(front xs0)
  | []      -> failwith "front: Empty list";;


(* string_option *)

let string_option x0 x_ =
  match x_ with
    Some x -> x
  | None   -> x0;;


(* print_option *)

let print_option x0 x_ =
  match x_ with
    Some x -> print_string x
  | None   -> print_string x0;;


(* seplists *)

let print_seplist p sep xs =
  if (xs = [])
    then ()
    else (p (hd xs);
          do_list (fun x -> print_string sep; p x) (tl xs));;

let print_string_seplist sep xs =
  print_seplist print_string sep xs;;


(* sum *)

let sum ns = foldl (+) 0 ns;;


(* snd_map *)

let snd_map f xys = map (fun (x,y) -> (x, f y)) xys;;