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