(* =========================================================================== *)
(* Aufgabe 1:                                                                  *)
(* =========================================================================== *)

#use "Loesungen_zu_Uebung_3.ml";;

(* --------------------------------------------------------------------------- *)
(* beta_value_step e liefert entweder den Ausdruck e', der in einem beta-value *)
(* Schritt e -> e' aus e ensteht, oder wirft die exception Beta_value_NF, wenn *)
(* KEIN beta-value-Schritt mehr möglich ist (d.h. wenn e schon in "beta-value- *)
(* Normalform" ist). Ist der Ausdruck e ein Name oder eine lambda-Abstraktion, *)
(* so ist er in beta-value-Normalform. Also bleibt nur noch der Fall einer Ap- *)
(* plikation e = e1 e2. In diesem Fall ist                                     *)
(* -  e' = e1' e2, falls e1 -> e1',                                            *)
(* -  e' = e1 e2', falls e1 in beta-value-Normalform ist und e2 -> e2',        *)
(* -  e' = beta e, falls e1, e2 in beta-value-Normalform sind                  *)
(*                              und e ein beta-Redex ist.                      *)
(* Tritt keiner dieser 3 Fälle ein, so ist e in beta-value-Normalform.         *)
(* --------------------------------------------------------------------------- *)

exception Beta_value_NF;;

let rec beta_value_step (e: expression): expression =
  match e with
      Id _ | Lambda _ -> raise Beta_value_NF
    | App (e1, e2) ->
	try App (beta_value_step e1, e2)
	with Beta_value_NF ->
	  try App (e1, beta_value_step e2)
	  with Beta_value_NF -> 
	    try beta e 
	    with Not_a_redex -> raise Beta_value_NF;;

(* --------------------------------------------------------------------------- *)
(* Die gesamte beta-value-Reduktion stellen wir dieses Mal als Liste von Aus-  *)
(* drücken dar, die erst bei der Ausgabe in einen string umgewandelt wird.     *)
(* --------------------------------------------------------------------------- *)

type reduction = expression list;;

let rec beta_value (e: expression): reduction = 
  try e :: beta_value (beta_value_step e)
  with Beta_value_NF -> [e];;

let print_reduction (es: reduction): unit =
  print_string (String.concat "\n -> " (List.map exp_to_string es) ^ "\n\n");;

(* --------------------------------------------------------------------------- *)
(* Beispiele aus Übung 3, Aufgabe 2:                                           *)
(* --------------------------------------------------------------------------- *)

print_reduction (beta_value exp_2a);;

print_reduction (beta_value exp_2b);;


(* =========================================================================== *)
(* Aufgabe 3:                                                                  *)
(* =========================================================================== *)

type base_type = UNIT | BOOL | INT | FLOAT;;

type simple_type = 
    BASE of base_type 
  | ARROW of simple_type * simple_type 
  | PRODUCT of simple_type list;;
    
type identifier = string;;

type operator = 
    Not | IAdd | ISub | IMul | IDiv 
        | FAdd | FSub | FMul | FDiv;;

let op_type (op: operator): simple_type = 
  match op with 
      Not                       -> ARROW (BASE BOOL, BASE BOOL)
    | IAdd | ISub | IMul | IDiv -> ARROW (BASE INT, ARROW (BASE INT, BASE INT))
    | FAdd | FSub | FMul | FDiv -> ARROW (BASE FLOAT, ARROW (BASE FLOAT, BASE FLOAT));;

type constant = 
    Unit 
  | Bool of bool
  | Int of int 
  | Float of float 
  | Op of operator;;

let const_type (c: constant): simple_type = 
  match c with
      Unit    -> BASE UNIT
    | Bool _  -> BASE BOOL
    | Int _   -> BASE INT
    | Float _ -> BASE FLOAT 
    | Op op   -> op_type op;;

(* --------------------------------------------------------------------------- *)
(* Eine Typumgebung Gamma wird als Liste von Paaren (id, tau) dargestellt. Wir *)
(* lassen es zu, dass die Liste MEHRERE Einträge für ein- und denselben Namen  *)
(* id enthält, wobei nur der (zeitlich) LETZTE Eintrag zählt. Dann können wir  *)
(* update einfach als "cons" implementieren, und bei lookup nach dem ersten    *)
(* (d.h. zeitlich letzten) passenden Eintrag suchen.                           *)
(* --------------------------------------------------------------------------- *)

type type_env = (identifier * simple_type) list;;

exception Type_error;;

let rec lookup (gamma: type_env) (id: identifier): simple_type =
  match gamma with 
      (id', tau) :: gamma' -> if id = id' then tau else lookup gamma' id
    | _                    -> raise Type_error;;

let update (gamma: type_env) (tau: simple_type) (id: identifier): type_env = 
  (id, tau) :: gamma;;

type expression = 
    Const of constant 
  | Id of identifier 
  | App of expression * expression
  | If of expression * expression * expression
  | Tuple of expression list
  | Lambda of identifier * simple_type * expression
  | Let of identifier * expression * expression
  | Rec of identifier * simple_type * expression;;

(* --------------------------------------------------------------------------- *)
(* Die Typüberprüfung für Ausdrücke erfolgt durch "Rückwärtsanwendung" unserer *)
(* Typregeln. Die Gleichheit von Typen (die in den Regeln (APP), (COND), (REC) *)
(* überprüft werden muss) lässt sich einfach mit "=" testen.                   *)
(* --------------------------------------------------------------------------- *)

let rec exp_type (gamma: type_env) (e: expression): simple_type = 
  match e with 
      Const c -> const_type c
    | Id id -> lookup gamma id
    | App (e1, e2) -> 
	(let tau1 = exp_type gamma e1  
	 in match tau1 with 
	     ARROW (tau, tau') -> 
	       if tau = exp_type gamma e2 
	       then tau' 
	       else raise Type_error
	   | _ -> raise Type_error)
    | If (e0, e1, e2) -> 
        if exp_type gamma e0 = BASE BOOL 
	then  
	  let tau1 = exp_type gamma e1 
	  and tau2 = exp_type gamma e2
	  in if tau1 = tau2 then tau1 else raise Type_error 
	else raise Type_error 
    | Tuple es -> PRODUCT (List.map (exp_type gamma) es)
    | Lambda (id, tau, e1) -> 
	let tau' = exp_type (update gamma tau id) e1 
	in ARROW (tau, tau')
    | Let (id, e1, e2) -> 
	let tau = exp_type gamma e1 
	in exp_type (update gamma tau id) e2
    | Rec (id, tau, e1) -> 
	if tau = exp_type (update gamma tau id) e1 
	then tau 
	else raise Type_error;;

	
(* =========================================================================== *)
(* Aufgabe 2:                                                                  *)
(* =========================================================================== *)

let string_of_base_type (b: base_type): string = 
  match b with 
      UNIT  -> "unit"
    | BOOL  -> "bool"
    | INT   -> "int"
    | FLOAT -> "float";;

let rec string_of_type (tau: simple_type): string = 
  match tau with 
      BASE b -> string_of_base_type b
    | ARROW (tau1, tau2) -> "(" ^ string_of_type tau1 ^ " -> " ^ string_of_type tau2 ^ ")"
    | PRODUCT taus -> "(" ^ String.concat " * " (List.map string_of_type taus) ^ ")";;

let string_of_id (id: identifier): string = id;;

let string_of_op (op: operator): string = 
  match op with 
      Not  -> "not"
    | IAdd -> "+"  | ISub -> "-"  | IMul -> "*"  | IDiv -> "/"
    | FAdd -> "+." | FSub -> "-." | FMul -> "*." | FDiv -> "/.";;

let string_of_const (c: constant): string = 
  match c with
      Unit    -> "()"
    | Bool b  -> string_of_bool b
    | Int n   -> string_of_int n
    | Float x -> string_of_float x
    | Op op   -> string_of_op op;;

let rec string_of_exp (e: expression): string = 
  match e with
      Const c -> string_of_const c
    | Id id -> string_of_id id
    | App (e1, e2) -> "(" ^ string_of_exp e1 ^ " " ^ string_of_exp e2 ^ ")"
    | If (e0, e1, e2) -> 
	"(if " ^ string_of_exp e0 ^ 
	" then " ^ string_of_exp e1 ^ 
	" else " ^ string_of_exp e2 ^ ")"
    | Tuple es -> "(" ^ String.concat ", " (List.map string_of_exp es) ^ ")"
    | Lambda (id, tau, e) -> 
	"(lambda " ^ string_of_id id ^ 
	": " ^ string_of_type tau ^ 
	". " ^ string_of_exp e ^ ")"
    | Let (id, e1, e2) -> 
	"(let " ^ string_of_id id ^ 
	" = " ^ string_of_exp e1 ^ 
	" in " ^ string_of_exp e2 ^ ")"
    | Rec (id, tau, e) -> 
	"(rec " ^ string_of_id id ^ 
	": " ^ string_of_type tau ^ 
	". " ^ string_of_exp e ^ ")";;

let type_check (e: expression): unit = 
  print_string ("Der Ausdruck\n\n" ^ string_of_exp e ^ "\n\n" ^ 
                (try "hat den Typ\n\n" ^ string_of_type (exp_type [] e)
		 with Type_error -> "ist nicht wohlgetypt") ^ ".\n\n");;

let plus_x_1 = App (App (Const (Op IAdd), Id "x"), Const (Int 1));;

let succ = Lambda ("x", BASE INT, plus_x_1);;

let exp_2a = Let ("x", Const (Int 1), App (succ, plus_x_1));;

let plus_x_y = App (App (Const (Op IAdd), Id "x"), Id "y");;

let f_f_x = App (Id "f", App (Id "f", Id "x"));;

let exp_2b = Let ("x", Const (Int 1),
		  Let ("f", Lambda ("y", BASE INT, plus_x_y), f_f_x));;

let f_o_succ = Lambda ("x", BASE INT, App (Id "f", plus_x_1));;

let exp_2c = Let ("x", Const (Int 1),
		  Let ("f", Rec ("f", ARROW (BASE INT, BASE INT), f_o_succ), 
		       App (Id "f", Id "x")));;

type_check exp_2a;;

type_check exp_2b;;

type_check exp_2c;;