1signature liteLib =
2sig
3   include Abbrev
4
5(*---------------------------------------------------------------------
6 * exceptions
7 *--------------------------------------------------------------------*)
8(*  exception Interrupt  (* USE THIS WITH NJSML ONLY!!! *) *)
9
10  val STRUCT_ERR  : string -> (string * string) -> 'a
11  val STRUCT_WRAP : string -> (string * exn) -> 'a
12  val fail        : unit -> 'a
13  val failwith    : string -> 'a
14
15(*---------------------------------------------------------------------
16 * options
17 *--------------------------------------------------------------------*)
18
19  val the : 'a option -> 'a
20  val is_some : 'a option -> bool
21  val is_none : 'a option -> bool
22  val option_cases : ('a -> 'b) -> 'b -> 'a option -> 'b
23  val option_app : ('a -> 'b) -> 'a option -> 'b option
24
25(*--------------------------------------------------------------------*
26 * Some extra combinators, e.g. reverse application.                  *
27 *--------------------------------------------------------------------*)
28
29  val |> : 'a * ('a -> 'b) -> 'b
30  val thenf : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
31  val orelsef : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
32  val repeat : ('a -> 'a) -> 'a -> 'a
33
34(*---------------------------------------------------------------------*
35 * Some extra list functions                                           *
36 *---------------------------------------------------------------------*)
37
38  (* from the basis *)
39  val foldr : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b
40  val foldl : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b
41
42  (* extras *)
43  val rotl : 'a list -> 'a list
44  val rotr : 'a list -> 'a list
45  val upto : (int * int) -> int list
46  val replicate : ('a * int) -> 'a list
47  val chop_list : int -> 'a list -> 'a list * 'a list
48  val splitlist : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
49  val striplist : ('a -> 'a * 'a) -> 'a -> 'a list
50  val rev_splitlist : ('a -> 'a * 'b) -> 'a -> 'a * 'b list
51  val end_foldr : ('a * 'a -> 'a) -> 'a list -> 'a
52
53(*---------------------------------------------------------------------
54 * Assoc lists.
55 *--------------------------------------------------------------------*)
56
57  val rev_assoc : ''b -> ('a * ''b) list -> 'a
58  val add_assoc : ''a * 'b -> (''a * 'b) list -> (''a * 'b) list
59  val remove_assoc : ''a -> (''a * 'b) list -> (''a * 'b) list
60
61(*---------------------------------------------------------------------
62 * Substitutions.  Nb. different to hol90.
63 *--------------------------------------------------------------------*)
64(*
65  val |-> : ('a * 'b) -> ('b * 'a)
66  val redex : ('a * 'b) -> 'b
67  val residue : ('a * 'b) -> 'a
68*)
69
70(*-------------------------------------------------------------------
71 * Partial Orders
72 *-------------------------------------------------------------------*)
73
74  val lt_of_ord : ('a * 'a -> order) -> ('a * 'a -> bool)
75  val ord_of_lt : ('a * 'a -> bool) -> ('a * 'a -> order)
76  val list_ord : ('a * 'a -> order) -> 'a list * 'a list -> order
77
78(*---------------------------------------------------------------------
79 * lazy objects
80 *--------------------------------------------------------------------*)
81
82  type ('a,'b)lazy;
83  val lazy : ('a -> 'b) -> 'a -> ('a,'b) lazy;
84  val eager: 'a -> ('b,'a) lazy;
85  val eval : ('a,'b)lazy -> 'b;
86
87
88(*--------------------------------------------------------------------*
89 * Term operators                                                     *
90 *--------------------------------------------------------------------*)
91
92    val mk_binop : term -> term * term -> term
93    val is_binop : term -> term -> bool
94    val dest_binop : term -> term -> term * term
95    val strip_binop : term -> term -> term list * term
96    val binops : term -> term -> term list
97    val lhand : term -> term
98
99    val mk_icomb : term * term -> term
100    val list_mk_icomb : term -> term list -> term
101
102    (* versions which do not treat negations as implications *)
103    val is_imp    : term -> bool
104    val dest_imp  : term -> term * term
105    val strip_imp : term -> term list * term;
106
107    val name_of_const : term -> string * string   (* (name,segment) *)
108    val alpha : term -> term -> term
109
110    val RIGHT_BETAS : term list -> thm -> thm
111    val BINDER_CONV : conv -> conv
112    val BODY_CONV : conv -> conv
113    val COMB2_CONV : conv -> conv -> conv
114    val COMB2_QCONV : conv -> conv -> conv
115    val COMB_CONV : conv -> conv
116    val COMB_QCONV : conv -> conv
117
118    val LAND_CONV : conv -> conv
119    val MK_ABSL_CONV : term list -> conv
120    val MK_ABS_CONV : term -> conv
121    val MK_BINOP : term -> thm * thm -> thm
122    val PINST : (hol_type,hol_type)subst -> (term,term)subst -> thm -> thm
123    val REPEATQC : conv -> conv
124
125    val SUB_QCONV : conv -> conv
126    val SUB_CONV : conv -> conv
127    val ABS_CONV : conv -> conv
128
129    val THENCQC : conv * conv -> conv
130    val THENQC : conv * conv -> conv
131
132    val SINGLE_DEPTH_CONV : conv -> conv
133    val ONCE_DEPTH_CONV : conv -> conv
134    val ONCE_DEPTH_QCONV : conv -> conv
135    val DEPTH_BINOP_CONV : term -> conv -> conv
136    val DEPTH_CONV : conv -> conv
137    val DEPTH_QCONV : conv -> conv
138    val REDEPTH_CONV : conv -> conv
139    val REDEPTH_QCONV : conv -> conv
140    val TOP_DEPTH_CONV : conv -> conv
141    val TOP_DEPTH_QCONV : conv -> conv
142    val TOP_SWEEP_CONV : conv -> conv
143    val TOP_SWEEP_QCONV : conv -> conv
144
145    val MK_DISJ : thm -> thm -> thm
146    val MK_CONJ : thm -> thm -> thm
147    val MK_FORALL : term -> thm -> thm
148    val MK_EXISTS : term -> thm -> thm
149
150    val SIMPLE_DISJ_CASES : thm -> thm -> thm
151    val SIMPLE_CHOOSE : term -> thm -> thm
152
153end
154