Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* DENOTATIONAL INTERPRETER *) (* SYNTACTIC DOMAIN *) type ide = Id of string type exp = Eint of int | Var of ide | Times of exp * exp | Ifthenelse of exp * exp * exp | Fun of ide * exp | Appl of exp * exp (* SEMANTIC DOMAINS *) type ceval = | Funval of (ceval -> ceval) | Int of int | Wrong type eval = | Afunval of (eval -> eval) | Top | Bottom | Zero | Zerop | Zerom | P | M let alfa x = match x with | Wrong -> Top | Int n -> if n = 0 then Zero else if n > 0 then P else M type env = ide -> eval let emptyenv = function (x: ide) -> alfa(Wrong) 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 times (x,y) = match (x,y) with | (_,Afunval(_)) -> Top | (Afunval(_),_) -> Top | (Bottom,_) -> Bottom | (_,Bottom) -> Bottom | (Zero,_) -> Zero | (_,Zero) -> Zero | (Top,_) -> Top | (_,Top) -> Top | (Zerom,Zerom) -> Zerop | (Zerom,Zerop) -> Zerom | (Zerom,M) -> Zerop | (Zerom,P) -> Zerom | (Zerop,Zerom) -> Zerom | (M,Zerom) -> Zerop | (P,Zerom) -> Zerom | (Zerop,Zerop) -> Zerop | (Zerop,M) -> Zerom | (Zerop,P) -> Zerop | (P,Zerop) -> Zerop | (M,Zerop) -> Zerom | (P,P) -> P | (M,M) -> P | (P,M) -> M | (M,P) -> M let valid x = match x with | Zero -> true | _ -> false let unsatisfiable x = match x with | M -> true | P -> true | _ -> false let lub (x,y) = if x = y then x else match (x,y) with | (Top,_) -> Top | (_,Top) -> Top | (Bottom,z) -> z | (z,Bottom) -> z | (Zero,Zerop) -> Zerop | (Zero,Zerom) -> Zerom | (Zero,P) -> Zerop | (Zero,M) -> Zerom | (Zerop,Zero) -> Zerop | (Zerom,Zero) -> Zerom | (P,Zero) -> Zerop | (M,Zero) -> Zerom | (Zerom,Zerop) -> Top | (Zerom,M) -> Zerom | (Zerom,P) -> Top | (Zerop,Zerom) -> Top | (M,Zerom) -> Zerom | (P,Zerom) -> Top | (Zerop,M) -> Top | (Zerop,P) -> Zerop | (P,Zerop) -> Zerop | (M,Zerop) -> Top | (P,M) -> Top | (M,P) -> Top let merge (a,b,c) = match a with | Afunval(_) -> Top | _ -> lub(b,c) let applyfun ((x:eval),(y:eval)) = match x with |Afunval f -> f y | _ -> alfa(Wrong) let rec makefun(ii,aa,r) = Afunval(function d -> if d = alfa(Wrong) then d else sem aa (bind(r,ii,d))) (*SEMANTIC EVALUATION FUNCTION *) and sem (e:exp) (r:env) = match e with | Eint(n) -> alfa(Int(n)) | Var(i) -> applyenv(r,i) | Times(a,b) -> times ( (sem a r), (sem b r)) | Ifthenelse(a,b,c) -> let a1 = sem a r in (if valid(a1) then sem b r else (if unsatisfiable(a1) then sem c r else merge(a1,sem b r,sem c r))) | Fun(ii,aa) -> makefun(ii,aa,r) | Appl(a,b) -> applyfun(sem a r, sem b r) (* esempi *) # let esempio = sem( Fun (Id "x", Ifthenelse (Var (Id "x"), Times (Var (Id "x"), Var (Id "x")), Times (Var (Id "x"), Eint (-1))))) emptyenv;; # applyfun(esempio,P);; - : eval = M # applyfun(esempio,Zero);; - : eval = Zero # applyfun(esempio,Zerop);; - : eval = Top # applyfun(esempio,Zerom);; - : eval = Zerop # applyfun(esempio,M);; - : eval = P (* non c'e' approssimazione sui valori veri Zero, P, M, perche' non abbiamo operazioni che introducono i valori intermedi che sono gli unici su cui si fa il lub e quindi si puo' introdurre approssimazione *)