header {* Quick introduction to ML, session 3 *}

 theory ML4_Datastructure imports Isac begin

 text{* This course follows the book:

 J.D.Ullmann, Elements of ML Programming. Prenctice Hall 1998.

 Contents:*}

 text {* 

   datastructures are tuples and list already introduced, and two further datastructures in ML,

   records and "datatypes"

 *}

 section {* 7.1 Record Structures *}

 ML {*

 val wn = {firstname = "Walther", lastname = "Neuper", age = 62, male = true};

 val tl = {firstname = "Thomas", lastname = "Leh", age = 17, male = true};

 wn = tl;

 val {firstname, ...} = tl;

 val {firstname = n, ...} = tl;

 val {age, ...} = tl;

 val {age = tage, ...} = tl;

 *}

 section {* 6.2 Datatypes *}

 ML {*

 infix +++ ***;

 datatype formula = 

     Num of int

   | Var of string

   | op +++ of formula * formula

   | op *** of formula * formula;

 *}

 ML {*

 (Num 2 *** Num 3) +++ Num 4;

 (Num 2 *** Num 3) +++ ((Num 2 *** Num 3) +++ Num 4);

 2;

 Num 2;

 (Num 2 *** Var "x") +++ ((Num 2 *** Num 3) +++ Var "c");

 *}

 section {* Preview to Isabelle's terms *}

 ML {*

 str2term;

 str2term "234 * bbb + ccc";

 *}

 ML {*

 @{term "5"}

 *}

 end