(* la sintassi astratta delle lambda-expressioni *)
type lambda_exp = Var of string
  | Lambda of string * lambda_exp
  | Appl of lambda_exp * lambda_exp
  | IntConstant of int
  | BoolConstant of bool
  | Plus of lambda_exp * lambda_exp
  | And of lambda_exp * lambda_exp
  | Eq of lambda_exp * lambda_exp
  | Gt of lambda_exp * lambda_exp
  | ITE of lambda_exp * lambda_exp * lambda_exp
  | Let of string * lambda_exp * lambda_exp
  | Letrec of string * lambda_exp * lambda_exp;;

(* il tipo che descrive i bytecode *)
type bytecode =
    LOADINT of int
  | LOADBOOL of bool
  | PUSHNIL
  | PUSHCODE of bytecode list
  | PUSHINT of int
  | DUPL
  | SWAP
  | ROT
  | IROT
  | FST
  | SND
  | SETFST
  | CONS
  | SPLIT
  | PLUS
  | AND
  | EQ
  | GT
  | CALL
  | RETURN
  | BRANCH of bytecode list * bytecode list;;

(* Il tipo degli elementi dello stack *)
type value = 
    IntValue of int
  | BoolValue of bool
  | CodeValue of bytecode list
  | NilValue
  | Address of int;;

(* stack, locazioni e memoria heap *)
type stack = value list;;
type loc = int;;
type heap = loc -> value;;

let rec append l1 l2 = match l1 with
    [] -> l2
  | h::t -> h::(append t l2);;

(* COMPILAZIONE *)

(* genera i bytecode necessari a leggere la variabile s dall'ambiente *)
let rec lookup env s = match env with
    h::t -> if (h = s) then [FST]
            else SND::(lookup t s);;

(* genera i bytecode corrispondenti alla compilazione *)
(* di una lambda espressione *)
let rec compile_aux exp env = match exp with
    IntConstant(i) -> [LOADINT(i)]
  | BoolConstant(b) -> [LOADBOOL(b)]
  | Var(s) -> lookup env s
  | Plus(IntConstant(i1),IntConstant(i2)) ->
     [LOADINT(i1+i2)]
  | Plus(IntConstant(i1),e2) ->
     append (compile_aux e2 env) [PUSHINT(i1);PLUS]
  | Plus(e1,IntConstant(i2)) ->
     append (compile_aux e1 env) [PUSHINT(i2);PLUS]
  | Plus(e1,e2) ->
     append (append (DUPL::(compile_aux e2 env))
                    (SWAP::(compile_aux e1 env))) [PLUS]
  | And(e1,e2) ->
     append (append (DUPL::(compile_aux e2 env))
                    (SWAP::(compile_aux e1 env))) [AND]
  | Eq(e1,e2) ->
     append (append (DUPL::(compile_aux e2 env))
                    (SWAP::(compile_aux e1 env))) [EQ]
  | Gt(e1,e2) ->
     append (append (DUPL::(compile_aux e2 env))
                    (SWAP::(compile_aux e1 env))) [GT]
  | ITE(e1,e2,e3) ->
     append (DUPL::(compile_aux e1 env))
       [BRANCH(append (compile_aux e2 env) [RETURN],
               append (compile_aux e3 env) [RETURN]);CALL]
  | Lambda(x,e) ->
     [PUSHCODE(append (compile_aux e (x::env)) [RETURN]); SWAP;CONS]
  | Appl(e1,IntConstant(i)) -> append [PUSHINT(i)]
     (append (SWAP::(compile_aux e1 env)) [SPLIT;IROT;CONS;SWAP;CALL])
  | Appl(e1,e2) -> append (DUPL::(compile_aux e2 env))
     (append (SWAP::(compile_aux e1 env)) [SPLIT;IROT;CONS;SWAP;CALL])
  | Let(x,e1,e2) -> append (DUPL::(compile_aux e1 env))
                           (CONS::(compile_aux e2 (x::env)))
  | Letrec(f,e1,e2) ->
     append (PUSHNIL::(compile_aux e1 (f::env)))
            (append [DUPL;ROT;CONS;SETFST;FST] (compile_aux e2 (f::env)));;

(* la compilazione avviene a partire da un ambiente statico vuoto *)
let compile exp = compile_aux exp [];;

(* INTERPRETAZIONE *)

(* scrive il valore v nella locazione l dello heap *)
let write heap l v =
  function l' -> if (l'=l) then v else (heap l');;

(* interpreta una sequenza di bytecode a partire dallo stato indicato *)
let rec interpret_aux bl (stack,heap,mr) = match (bl,stack) with
    ([],top::_) -> top
  | (LOADBOOL(b)::follow,top::rest) ->
      interpret_aux follow (BoolValue(b)::rest,heap,mr)
  | (LOADINT(i)::follow,top::rest) ->
      interpret_aux follow (IntValue(i)::rest,heap,mr)
  | (PUSHNIL::follow,_) ->
      interpret_aux follow (NilValue::stack,heap,mr)
  | (PUSHINT(i)::follow,_) ->
      interpret_aux follow (IntValue(i)::stack,heap,mr)
  | (PUSHCODE code::follow,_) ->
      interpret_aux follow (CodeValue(code)::stack,heap,mr)
  | (DUPL::follow,top::rest) ->
      interpret_aux follow (top::top::rest,heap,mr)
  | (SWAP::follow,top1::top2::rest) ->
      interpret_aux follow (top2::top1::rest,heap,mr)
  | (ROT::follow,top1::top2::top3::rest) ->
      interpret_aux follow (top2::top3::top1::rest,heap,mr)
  | (IROT::follow,top1::top2::top3::rest) ->
      interpret_aux follow (top3::top1::top2::rest,heap,mr)
  | (FST::follow,Address(l)::rest) ->
      interpret_aux follow (heap(l)::rest,heap,mr)
  | (SND::follow,Address(l)::rest) ->
      interpret_aux follow (heap(l + 1)::rest,heap,mr)
  | (SETFST::follow,v::Address(l)::rest) ->
      interpret_aux follow (Address(l)::rest,write heap l v,mr)
  | (CONS::follow,h::t::rest) ->
      interpret_aux follow
        (Address(mr)::rest,write (write heap mr h) (mr + 1) t,mr + 2)
  | (SPLIT::follow,Address(l)::rest) ->
      interpret_aux follow (heap(l)::heap(l + 1)::rest,heap,mr)
  | (PLUS::follow,IntValue(i1)::IntValue(i2)::rest) ->
      interpret_aux follow (IntValue(i1 + i2)::rest,heap,mr)
  | (AND::follow,BoolValue(b1)::BoolValue(b2)::rest) ->
      interpret_aux follow (BoolValue(b1 & b2)::rest,heap,mr)
  | (EQ::follow,top1::top2::rest) ->
      interpret_aux follow (BoolValue(top1 = top2)::rest,heap,mr)
  | (GT::follow,top1::top2::rest) ->
      interpret_aux follow (BoolValue(top1 > top2)::rest,heap,mr)
  | (CALL::follow,CodeValue(code)::par::rest) ->
      interpret_aux code (par::CodeValue(follow)::rest,heap,mr)
  | (RETURN::follow,v::CodeValue(code)::rest) ->
      interpret_aux code (v::rest,heap,mr)
  | (BRANCH(code1,code2)::follow,BoolValue(b)::rest) ->
      if (b) then interpret_aux follow (CodeValue(code1)::rest,heap,mr)
      else interpret_aux follow (CodeValue(code2)::rest,heap,mr);;

exception UndefinedLoc;;

(* L'interpretazione avviene a partire da uno stato in cui lo stack contiene
   un ambiente vuoto e lo heap e' completamente vuoto *)
let interpret bl = interpret_aux bl
  ([NilValue],(function x -> raise UndefinedLoc),0);;

(* L'esecuzione di una lambda espressione consiste nel compilarla e quindi *)
(* eseguirne il bytecode. L'espressione deve essere type-checked!!! *)
let run exp = interpret (compile exp);;

let exp0 = Plus(IntConstant(3),IntConstant(4));;
let exp1 = Lambda("z",Plus(IntConstant(3),Var "z"));;
let exp2 = Lambda("z",Lambda("y",Lambda("v",ITE(Var "z",Var "v",Var "z"))));;
let exp3 = Lambda("x",Plus(Var("x"),IntConstant(3)));;
let exp4 = Appl(Lambda("x",Plus(Var("x"),IntConstant(3))),IntConstant(4));;
let exp5 = Lambda("x",Lambda("y",Lambda("z",Appl(Var "x",ITE(Var "y",Appl(Var "z",Var "x"),IntConstant(0))))));;
let exp6 = Letrec("fib",Lambda("x",ITE
  (Eq(Var "x",IntConstant(0)),
    IntConstant(1),ITE(Eq(Var "x",IntConstant(1)),IntConstant(1),
      Plus(Appl(Var "fib",Plus(Var "x",IntConstant(-1))),
           Appl(Var "fib",Plus(Var "x",IntConstant(-2))))))),
  Appl(Var "fib",IntConstant(5)));;

let ack = Letrec
("ack",
 Lambda
 ("m",
  Lambda
  ("n",
   ITE
   (Eq(Var "m",IntConstant(0)),
      Plus(Var "n",IntConstant(1)),
      ITE
      (Eq(Var "n",IntConstant(0)),
	 Appl(Appl(Var "ack",Plus(Var "m",IntConstant(-1))),IntConstant(1)),
	 Appl(Appl(Var "ack",Plus(Var "m",IntConstant(-1))),
		  Appl(Appl(Var "ack",Var "m"),Plus(Var "n",IntConstant(-1))
			   )))))),
 Appl(Appl(Var "ack",IntConstant(3)),IntConstant(2)));