(* Quick introduction to ML, session 3 *)

 theory ML4_Datastructure imports Isac.Isac_Knowledge begin

 text\<open>This course follows the book:

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

 Contents:\<close>

 text \<open>

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

   records and "datatypes"

 \<close>

 section \<open>7.1 Record Structures\<close>

 ML \<open>

 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;

 \<close>

 section \<open>6.2 Datatypes\<close>

 ML \<open>

 infix +++ ***;

 datatype formula = 

     Num of int

   | Var of string

   | op +++ of formula * formula

   | op *** of formula * formula;

 \<close>

 ML \<open>

 (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");

 \<close>

 section \<open>Preview to Isabelle's terms\<close>

 ML \<open>

 parse_test @{context};

 parse_test @{context} "234 * bbb + ccc";

 \<close>

 ML \<open>

 @{term "5"}

 \<close>

 end