(********* Exercice 1 *********) true;; (* Booleans *) false;; 0;; (* Integers *) 65535;; if true then 7 else 14;; (* Conditional *) fun x -> x + 1;; (* Abstraction *) (fun x -> x + 1) 8;; (* Application *) "abcde";; (* Strings *) "meta"^"for";; (* String concatenation *) let rec fact x = (* rec indicates that the function is recursive *) if (x <= 0) then 1 else let y = x-1 in (* declaration of a local binding *) x * fact y (********* Exercice 2 *********) type value = | Red | Gray of int (* ints between 0 and 255 *) | RGB of (int * int * int);; let red_component c = match c with | Red -> 255 | Gray g -> g | RGB (r,g,b) -> r;; let c1 = Gray 100;; red_component c1 ;; (* -> 100 *) let c2 = RGB (50,150,250);; red_component c2 ;; (* -> 50 *) (********* Exercice 3 *********) TmAbs ("x", TmVar "x");; (* fun x -> x *) TmAbs ("y", TmAbs ("z", TmVar "z"));; (* fun y -> fun z -> z *) TmApp (TmAbs ("x", TmVar "x"), TmVar "z");; (* ((fun x -> x) z) *) parse "fun x -> x";; (* -> TmAbs ("x", TmVar "x") *) let rec term_to_string t = match t with | TmVar v -> "$"^(blue_string v)^"$" | TmAbs (v,e) -> "$\\lambda "^(blue_string v)^"$ . "^(term_to_string e) | TmApp (a,b) -> (term_to_string a)^" "^(term_to_string b) substitute "x" (TmVar "y") (parse "(fun x -> x) x");; (* -> ((fun x -> x) y) *) rename (parse "(fun x -> x) (fun y -> y)");; (* -> ((fun x1 -> x1) (fun x2 -> x2)) *) reduce_one (parse "(fun x -> x x) (fun y -> y)") (Ctx []);; (* -> ((fun y -> y) (fun y -> y))*) reduce (parse "(fun x -> x x) (fun y -> y)") (Ctx []);; (* -> (fun y -> y) *) (********* Exercice 4 *********)