module type ceval =
sig

  open Expr
  
  type env = int

  type proc = exp * env 	   
	 
  and eval =
    	  | Funval of proc	  
    	  | Mkpair of eval * eval
      	| Int of int 
      	| Bool of bool 
      	| Unbound 
      	
      	| Indef
      	
  val minus : eval -> eval 
  val iszero : eval -> eval 
  val equ : eval * eval -> eval 
  val plus : eval * eval -> eval 
  val diff : eval * eval -> eval
  val mult : eval * eval -> eval 
  val pair : eval * eval -> eval 
  val first : eval -> eval 
  val snd : eval -> eval 
  val et : eval * eval -> eval
  val vel : eval * eval -> eval
  val non : eval -> eval
  val alfa : eval -> eval
  val gamma : eval -> eval
  val abstrproc : eval -> bool
  val abstreq : eval * eval -> bool    	
  val merge : eval * eval * eval -> eval   	
  val valid : eval -> bool
  val unsatisfiable : eval -> bool

end


module Ceval : ceval =
struct

(* Nuovo valore per la tabulazione *)

  open Expr
  
  type env = int

  type proc = exp * env	   
	 
  and eval =
    	  | Funval of proc	  
    	  | Mkpair of eval * eval
      	| Int of int 
      	| Bool of bool 
      	| Unbound 
      	
      	| Indef
      	
(* 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 pair (x,y) = Mkpair(x,y)
             
    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")
      	 
(* Astrazione delle costanti di eval *)

  let alfa (x:eval) = x
  
  let gamma (x:eval) = x
  
  let abstrproc (b) = 
      let b1 = gamma(b) in
      (match b1 with 
         | Funval(x,y) -> true
         | _ -> false)
         
  let abstreq (a,b) = (a = b)
   
(* Gestione collecting del condizionale *)

      
  let merge (guard,firstarg,sndarg) = 
                     if firstarg = sndarg then firstarg
                     else alfa(Unbound)
                     
  let valid (x) = 
     match x with
       | Bool(true) -> true
       | Bool(false) -> false
       | _ -> failwith "non-boolean guard"  
  
  let unsatisfiable (x) = 
     match x with
       | Bool(true) -> false
       | Bool(false) -> true       
       | _ -> failwith "non-boolean guard"
       
end