wneuper@59353: (* Quick introduction to ML, session 3 *)
neuper@42088: 
wneuper@59592: theory ML4_Datastructure imports Isac.Isac_Knowledge begin
neuper@42088: 
wneuper@59472: text\<open>This course follows the book:
neuper@42088: J.D.Ullmann, Elements of ML Programming. Prenctice Hall 1998.
wneuper@59472: Contents:\<close>
neuper@42088: 
wneuper@59472: text \<open>
neuper@42088:   datastructures are tuples and list already introduced, and two further datastructures in ML,
neuper@42088:   records and "datatypes"
wneuper@59472: \<close>
wneuper@59472: section \<open>7.1 Record Structures\<close>
neuper@42088: 
wneuper@59472: ML \<open>
neuper@42088: val wn = {firstname = "Walther", lastname = "Neuper", age = 62, male = true};
neuper@42088: val tl = {firstname = "Thomas", lastname = "Leh", age = 17, male = true};
neuper@42088: wn = tl;
neuper@42088: val {firstname, ...} = tl;
neuper@42088: val {firstname = n, ...} = tl;
neuper@42088: val {age, ...} = tl;
neuper@42088: val {age = tage, ...} = tl;
wneuper@59472: \<close>
neuper@42088: 
wneuper@59472: section \<open>6.2 Datatypes\<close>
wneuper@59472: ML \<open>
neuper@42088: infix +++ ***;
neuper@42088: datatype formula = 
neuper@42088:     Num of int
neuper@42088:   | Var of string
neuper@42088:   | op +++ of formula * formula
neuper@42088:   | op *** of formula * formula;
wneuper@59472: \<close>
wneuper@59472: ML \<open>
neuper@42088: (Num 2 *** Num 3) +++ Num 4;
neuper@42088: (Num 2 *** Num 3) +++ ((Num 2 *** Num 3) +++ Num 4);
neuper@42088: 2;
neuper@42088: Num 2;
neuper@42088: (Num 2 *** Var "x") +++ ((Num 2 *** Num 3) +++ Var "c");
wneuper@59472: \<close>
neuper@42088: 
wneuper@59472: section \<open>Preview to Isabelle's terms\<close>
wneuper@59472: ML \<open>
Walther@60565: parse_test @{context};
Walther@60565: parse_test @{context} "234 * bbb + ccc";
wneuper@59472: \<close>
neuper@42088: 
wneuper@59472: ML \<open>
neuper@42088: @{term "5"}
wneuper@59472: \<close>
neuper@42088: end