(* INTERPRETE OPERAZIONALE CON FUNZIONI E DICHIARAZIONI 
              (anche ricorsive) *)

(* DOMINI SINTATTICI *)

    type ide = Id of string 
    type exp = 
    	Eint of int 
      | Ebool of bool 
      | Var of ide
      | Pair of exp * exp
      | First of exp
      | Snd of exp
      | Prod of exp * exp
      | Sum of exp * exp
      | Diff of exp * exp
      | Eq of exp * exp
      | Minus of exp
      | Iszero of exp
      | Or of exp * exp
      | And of exp * exp
      | Not of exp
      | Ifthenelse of exp * exp * exp
      | Fun of ide * exp
      | Appl of exp * exp
      | Letrec of ide * exp  * exp
      | Let of ide * exp * exp;;      

(* SEMANTIC DOMAINS *)

  type env = ide -> eval
      and      
	   proc = exp * env	   
	  and
	   eval =
    	  Funval of proc	  
    	| Mkpair of eval * eval
      	| Int of int 
      	| Bool of bool 
      	| Unbound 
  let emptyenv = function (x: ide) -> Unbound 
  let applyenv ((x: env), (y: ide)) = x y
  let bind ((r:env), l, (e:eval)) = 
    function lu -> if lu = l then e else r(lu)


 


(* Operations on Eval *)

    let typecheck (x, y) =
      match x with
      | "int" ->
	  (match y with 
	  |  Int(u) -> true
	  | _ -> false)
      | "bool" ->
	  (match y with 
	  |  Bool(u) -> true
	  | _ -> false)
      | _ -> failwith ("not a valid type")
      
    let minus x =
      if typecheck("int",x) 
      then 
    	(match x with
    	| Int(y) -> Int(-y) )
      else 
    	failwith ("type error")
    	
    let iszero x =
      if typecheck("int",x) 
      then 
     	(match x with
     	| Int(y) -> Bool(y=0) )
      else 
     	failwith ("type error")
     	
    let equ (x,y) =
      if typecheck("int",x) & typecheck("int",y) 
      then 
   	(match (x,y) with
   	| (Int(u), Int(w)) -> Bool(u = w))
      else failwith ("type error")
      
    let plus (x,y) =
      if typecheck("int",x) & typecheck("int",y) 
      then 
   	(match (x,y) with
   	| (Int(u), Int(w)) -> Int(u+w))
      else failwith ("type error")
      
    let diff (x,y) =
      if typecheck("int",x) & typecheck("int",y) 
      then 
   	(match (x,y) with
   	| (Int(u), Int(w)) -> Int(u-w))
      else failwith ("type error")
      
    let mult (x,y) =
      if typecheck("int",x) & typecheck("int",y) 
      then 
   	(match (x,y) with
   	| (Int(u), Int(w)) -> Int(u*w))
      else failwith ("type error")
      
    let first x =
       match x with
   	     Mkpair(y,z) -> y
   	     |_ -> failwith ("type error")
   	     
    let snd x =
       match x with
   	     Mkpair(y,z) -> z
   	     |_ -> failwith ("type error")
   	      
    let et (x,y) =
      if typecheck("bool",x) & typecheck("bool",y) 
      then 
   	(match (x,y) with
   	| (Bool(u), Bool(w)) -> Bool(u & w))
      else failwith ("type error")
      
    let vel (x,y) =
      if typecheck("bool",x) & typecheck("bool",y) 
      then 
   	(match (x,y) with
   	| (Bool(u), Bool(w)) -> Bool(u or w))
      else failwith ("type error")
      
    let non x =
      if typecheck("bool",x) 
      then 
     	(match x with
     	| Bool(y) -> Bool(not y) )
      else failwith ("type error")
      


(* FUNZIONI DI VALUTAZIONE SEMANTICA  *)

let rec
	makefun ((a:exp),(x:env)) =
      (match a with
      |	Fun(ii,aa) -> Funval(a,x)
      |	_ -> failwith ("Non-functional object"))
    and
	applyfun ((ev1:eval),(ev2:eval)) =
      match ev1 with
      | Funval(Fun(ii,aa),x) -> sem(aa,(bind(x,ii,ev2)))
      | _ -> failwith ("attempt to apply a non-functional object")
    and sem ((e:exp),(r:env)) =
      match e with
      | Eint(n) -> Int(n)
      | Ebool(b) -> Bool(b)
      | Var(i) -> applyenv(r,i)
      | Pair(a,b) -> Mkpair(sem(a,r),sem(b,r))
      | Iszero(a) -> iszero(sem(a,r) )
      | Eq(a,b) -> equ(sem(a,r) ,sem(b,r) )
      | First(a) -> first(sem(a,r))
      | Snd(a) -> snd(sem(a,r))
      | Prod(a,b) ->  mult ( sem(a,r), sem(b,r))
      | Sum(a,b) ->  plus ( sem(a,r), sem(b,r))
      | Diff(a,b)  ->  diff ( sem(a,r), sem(b,r))
      | Minus(a) ->  minus( sem(a,r))
      | And(a,b) ->  et ( sem(a,r), sem(b,r))
      | Or(a,b) ->  vel ( sem(a,r), sem(b,r))
      | Not(a) -> non( sem(a,r))
      | Ifthenelse(a,b,c) -> 
            let g = sem(a,r) in
            if typecheck("bool",g) then
               (match g with Bool(b1) ->
               if b1 then sem(b,r) else  sem(c,r) )
            else failwith "nonboolean guard"
      | Fun(i,a) ->  makefun(Fun(i,a), r)
      | Appl(a,b) -> applyfun(sem(a,r), sem(b,r))
      
      
      | Let(i,a,b) -> sem(b,bind(r,i,sem(a,r)))
      | Letrec(i,a,b) -> sem(b, 
               (let rec ff =  
      	       function j -> 
      	       applyenv(bind(r,i,(makefun(a, ff))),j) in ff));;


(*

val makefun : exp * env -> eval = <fun>
val applyfun : eval * eval -> eval = <fun>
val sem : exp * env -> eval = <fun>

*)

       
(* ESEMPI *)

(*

let factorial = 
   Letrec
   (Id "fact",
    Fun
     (Id "x",
      Ifthenelse
       (Iszero (Diff (Var (Id "x"), Eint 1)), Eint 1,
        Prod
         (Var (Id "x"), Appl (Var (Id "fact"), Diff (Var (Id "x"), Eint 1))))),
    Appl (Var (Id "fact"), Eint 10));;
      
let expo = 
  Letrec
   (Id "expo",
    Fun
     (Id "x",
      Let
       (Id "base", First (Var (Id "x")),
        Let
         (Id "espo", Snd (Var (Id "x")),
          Ifthenelse
           (Iszero (Var (Id "espo")), Eint 1,
            Prod
             (Var (Id "base"),
              Appl
               (Var (Id "expo"),
                Pair (Var (Id "base"), Diff (Var (Id "espo"), Eint 1)))))))),
    Appl (Var (Id "expo"), Pair (Eint 2, Eint 3)));;


# sem(factorial,emptyenv);;
- : eval = Int 3628800
# sem(expo,emptyenv);;
- : eval = Int 8

*)