module type ceval = sig 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 = | Ok | 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 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 = | Ok | T1 of ceval | Tunbound (* Astrazione di ceval *) let alfa (x) = match x with | Int(n) -> Ok | Bool(n) -> Ok | Indef -> Ok | 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) = (x = y) (* Operations on Eval: versioni astratte *) let minus x = match x with | Ok -> Ok | _ -> failwith ("type error") let iszero x = match x with | Ok -> Ok | _ -> failwith ("type error") let equ (x,y) = match (x,y) with | (Ok,Ok) -> Ok | _ -> failwith ("type error") let plus (x,y) = match (x,y) with | (Ok,Ok) -> Ok | _ -> failwith ("type error") let diff (x,y) = match (x,y) with | (Ok,Ok) -> Ok | _ -> failwith ("type error") let mult (x,y) = match (x,y) with | (Ok,Ok) -> Ok | _ -> failwith ("type error") let pair (x,y) = match (x,y) with | (Ok,Ok) -> Ok | _ -> failwith ("type error") let first x = match x with | Ok -> Ok |_ -> failwith ("type error") let snd x = match x with | Ok -> Ok |_ -> failwith ("type error") let et (x,y) = match (x,y) with | (Ok,Ok) -> Ok | _ -> failwith ("type error") let vel (x,y) = match (x,y) with | (Ok,Ok) -> Ok | _ -> failwith ("type error") let non x = match x with | Ok -> Ok | _ -> failwith ("type error") (* Gestione astratta del condizionale *) let merge (g,x,y) = match (g,x,y) with | (Ok,Ok,Ok) -> Ok | _ -> failwith ("type error") let valid (x) = false let unsatisfiable (x) = false end