src/Pure/library.ML
changeset 16825 0a28f033de03
parent 16780 aa284c1b72ad
child 16842 5979c46853d1
equal deleted inserted replaced
16824:c889f499911c 16825:0a28f033de03
     6 Basic library: functions, options, pairs, booleans, lists, integers,
     6 Basic library: functions, options, pairs, booleans, lists, integers,
     7 rational numbers, strings, lists as sets, association lists, generic
     7 rational numbers, strings, lists as sets, association lists, generic
     8 tables, balanced trees, orders, current directory, misc.
     8 tables, balanced trees, orders, current directory, misc.
     9 *)
     9 *)
    10 
    10 
    11 infix |> |-> ||> ||>> |>> |>>> #> #-> `> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
    11 infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int orf andf prefix upto downto
    12   mem mem_int mem_string union union_int union_string inter inter_int
    12   mem mem_int mem_string union union_int union_string inter inter_int
    13   inter_string subset subset_int subset_string;
    13   inter_string subset subset_int subset_string;
    14 
    14 
    15 infix 3 oo ooo oooo;
    15 infix 3 oo ooo oooo;
    16 
    16 
    27   val ||>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b
    27   val ||>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b
    28   val |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c
    28   val |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c
    29   val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
    29   val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
    30   val #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
    30   val #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
    31   val #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd
    31   val #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd
    32   val `> : 'b * ('b -> 'a) -> 'a * 'b
    32   val ` : ('b -> 'a) -> 'b -> 'a * 'b
    33   val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
    33   val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
    34   val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
    34   val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
    35   val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
    35   val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
    36   val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
    36   val apl: 'a * ('a * 'b -> 'c) -> 'b -> 'c
    37   val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
    37   val apr: ('a * 'b -> 'c) * 'b -> 'a -> 'c
   308 fun (x, y) ||> f = (x, f y);
   308 fun (x, y) ||> f = (x, f y);
   309 fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
   309 fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
   310 fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
   310 fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
   311 fun f #> g = g o f;
   311 fun f #> g = g o f;
   312 fun f #-> g = fn s => let val (v, s') = f s in g v s' end;
   312 fun f #-> g = fn s => let val (v, s') = f s in g v s' end;
   313 fun x `> h = (h x, x)
   313 fun ` h = fn s => (h s, s)
   314 
   314 
   315 (*composition with multiple args*)
   315 (*composition with multiple args*)
   316 fun (f oo g) x y = f (g x y);
   316 fun (f oo g) x y = f (g x y);
   317 fun (f ooo g) x y z = f (g x y z);
   317 fun (f ooo g) x y z = f (g x y z);
   318 fun (f oooo g) x y z w = f (g x y z w);
   318 fun (f oooo g) x y z w = f (g x y z w);