21394

1 
(* Title: Pure/General/basics.ML


2 
ID: $Id$


3 
Author: Florian Haftmann and Makarius, TU Muenchen


4 


5 
Fundamental concepts.


6 
*)


7 


8 
infix 1 > > >> > >>


9 
infix 1 #> #> #>> ##> ##>>


10 


11 
signature BASICS =


12 
sig


13 
(*functions*)


14 
val > : 'a * ('a > 'b) > 'b


15 
val > : ('c * 'a) * ('c > 'a > 'b) > 'b


16 
val >> : ('a * 'c) * ('a > 'b) > 'b * 'c


17 
val > : ('c * 'a) * ('a > 'b) > 'c * 'b


18 
val >> : ('c * 'a) * ('a > 'd * 'b) > ('c * 'd) * 'b


19 
val #> : ('a > 'b) * ('b > 'c) > 'a > 'c


20 
val #> : ('a > 'c * 'b) * ('c > 'b > 'd) > 'a > 'd


21 
val #>> : ('a > 'c * 'b) * ('c > 'd) > 'a > 'd * 'b


22 
val ##> : ('a > 'c * 'b) * ('b > 'd) > 'a > 'c * 'd


23 
val ##>> : ('a > 'c * 'b) * ('b > 'e * 'd) > 'a > ('c * 'e) * 'd


24 
val ` : ('b > 'a) > 'b > 'a * 'b


25 
val tap: ('b > 'a) > 'b > 'b


26 


27 
(*options*)


28 
val is_some: 'a option > bool


29 
val is_none: 'a option > bool


30 
val the: 'a option > 'a


31 
val these: 'a list option > 'a list


32 
val the_list: 'a option > 'a list


33 
val the_default: 'a > 'a option > 'a


34 
val perhaps: ('a > 'a option) > 'a > 'a


35 


36 
(*partiality*)


37 
val try: ('a > 'b) > 'a > 'b option


38 
val can: ('a > 'b) > 'a > bool


39 


40 
(*lists*)


41 
val cons: 'a > 'a list > 'a list


42 
val append: 'a list > 'a list > 'a list


43 
val fold: ('a > 'b > 'b) > 'a list > 'b > 'b


44 
val fold_rev: ('a > 'b > 'b) > 'a list > 'b > 'b


45 
val fold_map: ('a > 'b > 'c * 'b) > 'a list > 'b > 'c list * 'b


46 
end;


47 


48 
structure Basics: BASICS =


49 
struct


50 


51 
(* functions *)


52 


53 
(*application and structured results*)


54 
fun x > f = f x;


55 
fun (x, y) > f = f x y;


56 
fun (x, y) >> f = (f x, y);


57 
fun (x, y) > f = (x, f y);


58 
fun (x, y) >> f = let val (z, y') = f y in ((x, z), y') end;


59 


60 
(*composition and structured results*)


61 
fun (f #> g) x = x > f > g;


62 
fun (f #> g) x = x > f > g;


63 
fun (f #>> g) x = x > f >> g;


64 
fun (f ##> g) x = x > f > g;


65 
fun (f ##>> g) x = x > f >> g;


66 


67 
(*result views*)


68 
fun `f = fn x => (f x, x);


69 
fun tap f = fn x => (f x; x);


70 


71 


72 
(* options *)


73 


74 
fun is_some (SOME _) = true


75 
 is_some NONE = false;


76 


77 
fun is_none (SOME _) = false


78 
 is_none NONE = true;


79 


80 
fun the (SOME x) = x


81 
 the NONE = raise Option;


82 


83 
fun these (SOME x) = x

23559

84 
 these NONE = [];

21394

85 


86 
fun the_list (SOME x) = [x]

23559

87 
 the_list NONE = []

21394

88 


89 
fun the_default x (SOME y) = y

23559

90 
 the_default x NONE = x;

21394

91 


92 
fun perhaps f x = the_default x (f x);


93 


94 


95 
(* partiality *)


96 


97 
fun try f x = SOME (f x)


98 
handle Interrupt => raise Interrupt  _ => NONE;


99 


100 
fun can f x = is_some (try f x);


101 


102 


103 
(* lists *)


104 


105 
fun cons x xs = x :: xs;


106 


107 
fun append xs ys = xs @ ys;


108 

23225

109 
fun fold _ [] y = y


110 
 fold f (x :: xs) y = fold f xs (f x y);

21394

111 

23225

112 
fun fold_rev _ [] y = y


113 
 fold_rev f (x :: xs) y = f x (fold_rev f xs y);

21394

114 

23225

115 
fun fold_map _ [] y = ([], y)


116 
 fold_map f (x :: xs) y =


117 
let


118 
val (x', y') = f x y;


119 
val (xs', y'') = fold_map f xs y';


120 
in (x' :: xs', y'') end;

21394

121 


122 
end;


123 


124 
open Basics;
