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

22935

26 
val flip: ('a > 'b > 'c) > 'b > 'a > 'c

21394

27 


28 
(*options*)


29 
val is_some: 'a option > bool


30 
val is_none: 'a option > bool


31 
val the: 'a option > 'a


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


33 
val the_list: 'a option > 'a list


34 
val the_default: 'a > 'a option > 'a


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


36 


37 
(*partiality*)


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


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


40 


41 
(*lists*)


42 
val cons: 'a > 'a list > 'a list


43 
val dest: 'a list > 'a * 'a list


44 
val append: 'a list > 'a list > 'a list


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


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


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


48 
val unfold: int > ('b > 'a * 'b) > 'b > 'a list * 'b


49 
val unfold_rev: int > ('b > 'a * 'b) > 'b > 'a list * 'b


50 
end;


51 


52 
structure Basics: BASICS =


53 
struct


54 


55 
(* functions *)


56 


57 
(*application and structured results*)


58 
fun x > f = f x;


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


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


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


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


63 


64 
(*composition and structured results*)


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


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


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


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


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


70 


71 
(*result views*)


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


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


74 

22936

75 
fun flip f x y = f y x;


76 

21394

77 


78 
(* options *)


79 


80 
fun is_some (SOME _) = true


81 
 is_some NONE = false;


82 


83 
fun is_none (SOME _) = false


84 
 is_none NONE = true;


85 


86 
fun the (SOME x) = x


87 
 the NONE = raise Option;


88 


89 
fun these (SOME x) = x


90 
 these _ = [];


91 


92 
fun the_list (SOME x) = [x]


93 
 the_list _ = []


94 


95 
fun the_default x (SOME y) = y


96 
 the_default x _ = x;


97 


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


99 


100 


101 
(* partiality *)


102 


103 
exception Interrupt = Interrupt; (*signals intruding execution :[*)


104 


105 
fun try f x = SOME (f x)


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


107 


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


109 


110 


111 
(* lists *)


112 


113 
fun cons x xs = x :: xs;


114 


115 
fun dest (x :: xs) = (x, xs)


116 
 dest [] = raise Empty;


117 


118 
fun append xs ys = xs @ ys;


119 


120 


121 
(* fold *)


122 


123 
fun fold f =


124 
let


125 
fun fld [] y = y


126 
 fld (x :: xs) y = fld xs (f x y);


127 
in fld end;


128 


129 
fun fold_rev f =


130 
let


131 
fun fld [] y = y


132 
 fld (x :: xs) y = f x (fld xs y);


133 
in fld end;


134 


135 
fun fold_map f =


136 
let


137 
fun fld [] y = ([], y)


138 
 fld (x :: xs) y =


139 
let


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


141 
val (xs', y'') = fld xs y';


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


143 
in fld end;


144 


145 


146 
(* unfold  with optional limit *)


147 


148 
fun unfold lim f =


149 
let


150 
fun unfld 0 ys x = (ys, x)


151 
 unfld n ys x =


152 
(case try f x of


153 
NONE => (ys, x)


154 
 SOME (y, x') => unfld (n  1) (y :: ys) x');


155 
in unfld lim [] end;


156 


157 
fun unfold_rev lim f =


158 
let


159 
fun unfld 0 x = ([], x)


160 
 unfld n x =


161 
(case try f x of


162 
NONE => ([], x)


163 
 SOME (y, x') => unfld (n  1) x' >> cons y);


164 
in unfld lim end;


165 


166 
end;


167 


168 
open Basics;
