(* 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