1.1 --- a/test/Pure/General/Basics.thy	Thu Jul 14 09:33:57 2011 +0200
     1.2 +++ b/test/Pure/General/Basics.thy	Thu Jul 14 14:32:12 2011 +0200
     1.3 @@ -2,16 +2,15 @@
     1.4      Author: Walther Neuper, TU Graz, 101027
     1.5  *)
     1.6  
     1.7 -header {* testing combinators from src/Pure/General/basics 
     1.8 -          see *}
     1.9 +header {* testing combinators from src/Pure/General/basics *}
    1.10  
    1.11  theory Basics
    1.12  imports Complex_Main
    1.13  begin
    1.14  
    1.15  ML {* op |> ;
    1.16 -  1 |> (fn x => x+10)
    1.17 -    |> (fn x => 2*x);
    1.18 +  1 |> (fn x => x + 10)
    1.19 +    |> (fn x => 2 * x);
    1.20  (*val it = 22 : int*)
    1.21  *}
    1.22  
    1.23 @@ -22,12 +21,12 @@
    1.24  *}
    1.25  
    1.26  ML {* op |>> ;
    1.27 -  (1, "a") |>> (fn x => x+10)
    1.28 +  (1, "a") |>> (fn x => x + 10)
    1.29  (*val it = (11, "a") : int * string*)
    1.30  *}
    1.31  
    1.32  ML {* op ||> ;
    1.33 -  ("a", 1) ||> (fn x => x+10)
    1.34 +  ("a", 1) ||> (fn x => x + 10)
    1.35  (*val it = ("a", 11) : string * int*)
    1.36  *}
    1.37  

     2.1 --- a/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML1_Basics.thy	Thu Jul 14 09:33:57 2011 +0200
     2.2 +++ b/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML1_Basics.thy	Thu Jul 14 14:32:12 2011 +0200
     2.3 @@ -1,10 +1,9 @@
     2.4  header {* Quick introduction to ML, session 1 *}
     2.5  theory ML1_Basics imports Isac begin
     2.6  
     2.7 -text{*
     2.8 -This course follows the book:
     2.9 +text{* This course follows the book:
    2.10  J.D.Ullmann, Elements of ML Programming. Prenctice Hall 1998.
    2.11 -Contents:
    2.12 +Contents:*}
    2.13  
    2.14  section {* 2.1 Expressions .. 2.1.5*}
    2.15  ML {*

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML3_Combinators.thy	Thu Jul 14 14:32:12 2011 +0200
     3.3 @@ -0,0 +1,96 @@
     3.4 +header {* Quick introduction to ML, session 3 *}
     3.5 +
     3.6 +theory ML3_Combinators imports Isac begin
     3.7 +
     3.8 +text{* This course follows the book:
     3.9 +J.D.Ullmann, Elements of ML Programming. Prenctice Hall 1998.
    3.10 +Contents:*}
    3.11 +
    3.12 +section {* 5.6 Higher-Order Functions *}
    3.13 +
    3.14 +subsection {* map *}ML {*
    3.15 +map;
    3.16 +fun add3 a = a + 3: int;
    3.17 +map add3 [];
    3.18 +map add3 [1,2,3,4,5];
    3.19 +*}
    3.20 +ML {*
    3.21 +fun greater a b = a > b;
    3.22 +greater 2 3;
    3.23 +greater 5 3;
    3.24 +greater 5;
    3.25 +map (greater 3) [1,2,3,4,5];
    3.26 +*}
    3.27 +
    3.28 +subsection {* fold *}
    3.29 +ML {*
    3.30 +fold;
    3.31 +fun add a b = a + b;
    3.32 +fun mult a b = a * b;
    3.33 +*}
    3.34 +ML {*
    3.35 +fold add [1,2,3,4,5] 10;
    3.36 +fold add [1,2,3,4,5] 10;
    3.37 +
    3.38 +fold mult [1,2,3] 1;
    3.39 +fold mult [1,2,3,4,5] 1;
    3.40 +*}
    3.41 +
    3.42 +section {* Bad style: local variables in functions *}
    3.43 +ML {*
    3.44 +fun xxx a b c d e f =
    3.45 +  let 
    3.46 +    val x = a + b
    3.47 +    val _ = writeln ("### xxx: x = " ^ string_of_int x)
    3.48 +    val y = c * d
    3.49 +    val z = e ^ f
    3.50 +  in (x, y , z) end;
    3.51 +xxx 1 2 3 4  "a" "b";
    3.52 +*}
    3.53 +text {* little improvement *}
    3.54 +ML {*
    3.55 +fun xxx a b c d e f =
    3.56 +  let 
    3.57 +    val x = a + b
    3.58 +    val _ = writeln (string_of_int x)
    3.59 +    val _ = string_of_int x |> writeln
    3.60 +    val y = c * d
    3.61 +    val z = e ^ f
    3.62 +  in (x, y , z) end;
    3.63 +xxx 1 2 3 4  "a" "b";
    3.64 +*}
    3.65 +
    3.66 +
    3.67 +section {* Combinators, see src/Pure/General/basics.ML *}
    3.68 +subsection {* Preliminaries *}
    3.69 +ML {*
    3.70 +(*infix +++;*)
    3.71 +fun +++ a b = a + b;
    3.72 ++++ 1 3;
    3.73 +*}
    3.74 +ML {*
    3.75 +fn x => x + 10; (* function without a name*)
    3.76 +(fn x => x + 10) 3;
    3.77 +
    3.78 +fun ??? x = x + 10;
    3.79 +*}
    3.80 +
    3.81 +subsection {* Combinators with example in test/Pure/General/Basics.thy *}
    3.82 +ML {*
    3.83 +op |> 
    3.84 +*}
    3.85 +ML {*
    3.86 +op ||> ;
    3.87 +*}
    3.88 +
    3.89 +subsection {* Still no examples in test/Pure/General/Basics.thy *}
    3.90 +text {* please, find examples for ||>> ff ! *}
    3.91 +ML {*
    3.92 +op #>>;
    3.93 +fun fff a = (a + 10, string_of_int a);
    3.94 +fun ggg b = b * 2;
    3.95 +fff #>> ggg;
    3.96 +(fff #>> ggg) 1;
    3.97 +*}
    3.98 +
    3.99 +end