module type ceval =
sig

  open Unif
  open Expr
  
  type env = int

  type proc = exp * env   
	 
  and ceval =
    	  Funval of proc
    	| Mkpair of ceval * ceval
      	| Int of int 
      	| Bool of bool 
      	| Unbound
      	| Indef 
  type eval = 
          | T of (gterm * ((gterm* gterm) list))
          | T1 of ceval
          | Tunbound
  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 : ceval -> eval
  val gamma : eval -> ceval
  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
  
  open Unif
  open Tipi
  open Expr
  
(* Il vecchio eval diventa ceval *)

  type env = int

  type proc = exp * env	   
	 
  and ceval =
    	  Funval of proc	  
    	| Mkpair of ceval * ceval
      	| Int of int 
      	| Bool of bool 
      	| Unbound
      	| Indef  
  


(* Il nuovo eval e' il dominio astratto *)
  
type eval = 
       | T of (gterm * ((gterm* gterm) list))
       | T1 of ceval
       | Tunbound
           
(* Astrazione di ceval *)

  let alfa (x) = match x with
       | Int(n) -> T(down(Intero),[])
       | Bool(n) -> T(down(Booleano),[])
       | Indef -> T(newvar(),[])
       | Unbound -> Tunbound
       | Funval(a,b) -> T1(Funval(a,b))
       | _ -> failwith "manca il caso del Mkpair" 

  let gamma (x) = match x with
       | T1(y) -> y
       | _ -> Unbound
       
  let abstrproc (b) = 
      let b1 = gamma(b) in
      (match b1 with 
         | Funval(x,y) -> true
         | _ -> false)
         
  let abstreq (x,y) =
      match (x,y) with
      | (T(v1,c1),T(v2,c2)) -> (v1 = v2)
      | (_,_) -> (x = y)

(* Operations on Eval: versioni astratte  *)

    let minus x = 
      match x with
        | T(v,c) -> T(down(Intero),
                               unifylist((v,down(Intero)) :: c))
        | _ -> failwith ("type error")
      
    	
    let iszero x =
      match x with
        | T(v,c) -> T(down(Booleano),
                               unifylist((v,down(Intero)) :: c))
        | _ -> failwith ("type error")
     	
    let equ (x,y) =
      match (x,y) with
        | (T(v1,c1),T(v2,c2)) -> 
                    T(down(Booleano),
                    unifylist((v1,down(Intero)) :: (v2,down(Intero)) :: 
                    (c1 @ c2)))
        | _ -> failwith ("type error")
      
    let plus (x,y) =
      match (x,y) with
        | (T(v1,c1),T(v2,c2)) -> 
                    T(down(Intero),
                    unifylist((v1,down(Intero)) :: (v2,down(Intero)) :: (c1 @ c2)))
        | _ -> failwith ("type error")
      
    let diff (x,y) =
      match (x,y) with
        | (T(v1,c1),T(v2,c2)) -> 
                    T(down(Intero),
                    unifylist((v1,down(Intero)) :: (v2,down(Intero)) :: (c1 @ c2)))
        | _ -> failwith ("type error")
      
    let mult (x,y) =
      match (x,y) with
        | (T(v1,c1),T(v2,c2)) -> 
                    T(down(Intero),
                    unifylist((v1,down(Intero)) :: (v2,down(Intero)) :: (c1 @ c2)))
        | _ -> failwith ("type error")
    
    let pair (x,y) =
      match (x,y) with
        | (T(v1,c1),T(v2,c2)) -> 
                    let sigma = unifylist(c1 @ c2) in
                    T(applysubst sigma (down(Mkprod(up(v1),up(v2)))),sigma)
        | _ -> failwith ("type error") 
    
      
    let first x =
       match x with
   	     |T(y,z) -> let f1 =newvar() in
   	               let sigma = unifylist((down(Mkprod(up(f1),up(newvar()))),y):: z) in
   	                    T(applysubst sigma f1,sigma)
   	     |_ -> failwith ("type error")
   	     
    let snd x =
       match x with
   	     |T(y,z) -> let f1 =newvar() in
   	               let sigma = unifylist((down(Mkprod(up(newvar()),up(f1))),y):: z) in
   	                    T(applysubst sigma f1,sigma)
   	     |_ -> failwith ("type error")
   	      
    let et (x,y) =
      match (x,y) with
        | (T(v1,c1),T(v2,c2)) -> 
                    T(down(Booleano),
                    unifylist((v1,down(Booleano)) :: (v2,down(Booleano)) :: 
                    (c1 @ c2)))
        | _ -> failwith ("type error")
      
    let vel (x,y) =
      match (x,y) with
        | (T(v1,c1),T(v2,c2)) -> 
                    T(down(Booleano),
                    unifylist((v1,down(Booleano)) :: (v2,down(Booleano)) :: 
                    (c1 @ c2)))
        | _ -> failwith ("type error")
      
    let non x =
      match x with
        | T(v,c) -> T(down(Booleano),
                               unifylist((v,down(Booleano)) :: c))
        | _ -> failwith ("type error")
      


(* Gestione astratta del condizionale *)

      
  let merge (g,x,y) =
    match (g,x,y) with
        | (T(v0,c0),T(v1,c1),T(v2,c2)) ->
             let sigma = unifylist((v0,down(Booleano)) :: (v1,v2) :: (c0 @ c1 @ c2)) in 
                  T(applysubst sigma v1,sigma)                    
        | _ -> failwith ("type error")
                     
  let valid (x) = false
  
  let unsatisfiable (x) = false
  
end