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 | Sum of exp * exp | Diff of exp * exp | Ifthenelse of exp * exp * exp | Fun of ide * exp | Rec of ide * exp | Appl of exp * exp | Let of ide * exp * exp | Letrec of ide * exp * exp | Letmutrec of (ide * exp) * (ide *exp) * exp (* SEMANTIC DOMAINS *) type proc = eval -> eval and eval = Funval of proc | Int of int | Wrong let alfa x = x 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 plus (x,y) = match (x,y) with |(Int nx, Int ny) -> Int (nx + ny) | _ -> Wrong let diff (x,y) = match (x,y) with |(Int nx, Int ny) -> Int (nx - ny) | _ -> Wrong let valid x = match x with |Int n -> n=0 let unsatisfiable x = match x with |Int n -> if n=0 then false else true let merge (a,b,c) = match a with |Int n -> if b=c then b else Wrong | _ -> Wrong let applyfun ((x:eval),(y:eval)) = match x with |Funval f -> f y | _ -> Wrong let rec makefun(ii,aa,r) = Funval(function d -> if d = Wrong then Wrong else sem aa (bind(r,ii,d))) and makefunrec (i,e1,r) = Funval(let rec ff = function d -> if d = Wrong then Wrong else (match funzionale (Funval ff) i e1 r with | Funval f -> f d) in ff) and makemutrec ((i1,e1),(i2,e2),r) = let rec ff1 = function d -> if d = Wrong then Wrong else (match sem e1 (bind(bind(r,i1,Funval(ff1)),i2,Funval(ff2))) with | Funval f -> f d) and ff2 = function d -> if d = Wrong then Wrong else (match sem e2 (bind(bind(r,i1,Funval(ff1)),i2,Funval(ff2))) with | Funval f -> f d) in bind(bind(r,i1,Funval(ff1)),i2,Funval(ff2)) (* lfp (funzionale ff i e r) *) (*SEMANTIC EVALUATION FUNCTION *) and sem (e:exp) (r:env) = match e with | Eint(n) -> alfa(Int(n)) | Var(i) -> applyenv(r,i) | Sum(a,b) -> plus ( (sem a r), (sem b r)) | Diff(a,b) -> diff ( (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) | Rec(i,e1) -> makefunrec (i,e1,r) | Appl(a,b) -> applyfun(sem a r, sem b r) | Let(i,e1,e2) -> let d = sem e1 r in if d = alfa(Wrong) then d else sem e2 (bind(r, i,d)) | Letrec(i,e1,e2) -> sem (Let(i,Rec(i,e1),e2)) r | Letmutrec ((i1,e1),(i2,e2),e3) -> sem e3 (makemutrec((i1,e1),(i2,e2),r)) and funzionale ff i e r = sem e (bind(r,i,ff)) (* Esempi di valutazioni concrete corrette che vengono escluse (perche' non tipabili) da ML *) (* non tipabile da ML per l'approssimazione del calcolo del punto fisso: f f1 g n x = g(f1^n(x)) *) # let rec f f1 g n x = if n=0 then g(x) else f(f1)(function x -> (function h -> g(h(x)))) (n-1) x f1 in f (function x -> x+1) (function x -> -x) 10 5;; This expression has type ('a -> 'a) -> 'b but is here used with type 'b # sem (Letrec (Id "f",Fun(Id "f1", Fun(Id "g", Fun(Id "n", Fun(Id "x", Ifthenelse(Var(Id "n"),Appl(Var(Id "g"),Var(Id "x")), Appl(Appl(Appl(Appl(Appl(Var(Id "f"),Var(Id "f1")), Fun(Id "x",Fun(Id "h", Appl(Var(Id "g"),Appl(Var(Id "h"),Var(Id "x")))))),Diff(Var(Id "n"),Eint 1)),Var(Id "x")),Var(Id "f1"))))))), Appl(Appl(Appl(Appl(Var(Id "f"),Fun(Id "x",Sum(Var(Id "x"),Eint 1))), Fun(Id "x",Var(Id "x"))), Eint 10),Eint 5) ) ) emptyenv;; - : eval = Int 15 (* l'approssimazione del punto fisso con mutua ricorsione porta a inferire un tipo peggiore di quello piu' generale e a non permettere la tipizzazione di alcune applicazioni *) # let rec f x = x and g x = f (1+x) in f f 2;; This expression has type int -> int but is here used with type int # sem (Letmutrec((Id "f",Fun(Id "x",Var(Id "x"))), (Id "g",Fun(Id "x",Appl(Var(Id "f"),Sum(Eint 1,Var(Id "x"))))), Appl(Appl(Var(Id "f"),Var(Id "f")),Eint 2))) emptyenv;; - : eval = Int 2 (* assenza di ricorsione polimorfa *) # let rec polyf x y = if x=0 then 0 else if (x-1)=0 then (polyf (x-1)) (function z -> z) else (polyf (x-2)) 0 in polyf 3 1;; This expression has type int but is here used with type 'a -> 'a # sem (Letrec (Id "polyf", Fun (Id "x", Fun (Id "y", Ifthenelse (Var (Id "x"), Eint 0, Ifthenelse (Diff (Var (Id "x"), Eint 1), Appl (Appl (Var (Id "polyf"), Diff (Var (Id "x"), Eint 1)), Fun (Id "z", Var (Id "z"))), Appl (Appl (Var (Id "polyf"), Diff (Var (Id "x"), Eint 2)), Eint 0))))), Appl(Appl(Var (Id "polyf"),Eint 3),Eint 1) )) emptyenv;; - : eval = Int 0 (* assenza di astrazione polimorfa: non riusciremo neanche noi! *) # (function x -> x x) (function x -> x) 3 This expression has type 'a -> 'b but is here used with type 'a # sem ( Appl(Appl(Fun(Id "x", Appl(Var(Id "x"),Var(Id "x"))), (Fun(Id "x",Var(Id "x")))), Eint 3) ) emptyenv;; - : eval = Int 3