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 dest: 'a list > 'a * 'a list


43 
val append: 'a list > 'a list > 'a list


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


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


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


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


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


49 
end;


50 


51 
structure Basics: BASICS =


52 
struct


53 


54 
(* functions *)


55 


56 
(*application and structured results*)


57 
fun x > f = f x;


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


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


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


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


62 


63 
(*composition and structured results*)


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


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 


70 
(*result views*)


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


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


73 


74 


75 
(* options *)


76 


77 
fun is_some (SOME _) = true


78 
 is_some NONE = false;


79 


80 
fun is_none (SOME _) = false


81 
 is_none NONE = true;


82 


83 
fun the (SOME x) = x


84 
 the NONE = raise Option;


85 


86 
fun these (SOME x) = x


87 
 these _ = [];


88 


89 
fun the_list (SOME x) = [x]


90 
 the_list _ = []


91 


92 
fun the_default x (SOME y) = y


93 
 the_default x _ = x;


94 


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


96 


97 


98 
(* partiality *)


99 


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


101 


102 
fun try f x = SOME (f x)


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


104 


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


106 


107 


108 
(* lists *)


109 


110 
fun cons x xs = x :: xs;


111 


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


113 
 dest [] = raise Empty;


114 


115 
fun append xs ys = xs @ ys;


116 


117 


118 
(* fold *)


119 


120 
fun fold f =


121 
let


122 
fun fld [] y = y


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


124 
in fld end;


125 


126 
fun fold_rev f =


127 
let


128 
fun fld [] y = y


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


130 
in fld end;


131 


132 
fun fold_map f =


133 
let


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


135 
 fld (x :: xs) y =


136 
let


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


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


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


140 
in fld end;


141 


142 


143 
(* unfold  with optional limit *)


144 


145 
fun unfold lim f =


146 
let


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


148 
 unfld n ys x =


149 
(case try f x of


150 
NONE => (ys, x)


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


152 
in unfld lim [] end;


153 


154 
fun unfold_rev lim f =


155 
let


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


157 
 unfld n x =


158 
(case try f x of


159 
NONE => ([], x)


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


161 
in unfld lim end;


162 


163 
end;


164 


165 
open Basics;
