(* INTERPRETE ASTRATTO CHE CALCOLA LA DIMENSIONE MASSIMA DELLA PILA LOCALE DI TEMPORANEI *) module type size = sig open Expr val tframesize : exp -> int end module Size: size = struct open Expr type env = int type proc = exp * env type 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 = | A of int | Tunbound (* Pila astratta *) type astack = (int ref) * (int ref) (* Astrazione di ceval *) let alfa (x) = match x with | Int(n) -> A(0) | Bool(n) -> A(0) | Indef -> A(0) | Unbound -> Tunbound | Funval(a,b) -> A(0) | _ -> failwith "manca il caso del Mkpair" (* Operazioni su Eval: versioni astratte *) let minus x = x let iszero x = x let equ (x,y) = x let plus (x,y) = x let diff (x,y) = x let mult (x,y) = x let pair (x,y) = x let first x = x let snd x = x let et (x,y) = x let vel (x,y) = x let non x = x (* Gestione astratta del condizionale *) let merge (g,x,y) = x let valid (x) = false let unsatisfiable (x) = false (* operazioni sulle pile astratte *) let aemptystack (x,y) = (ref(0),ref(0)) let apush(x,((y,z):astack)) = z := !z + 1; if !z > !y then y := !z else y := !y let atop(((y,z): astack)) = A(!y) let apop(((y,z): astack)) = z := !z -1 (* supporto a run time *) type 'x stack = ('x array) * int ref let emptystack(nm,x) = (Array.create nm x, ref(-1)) let push(x,(s,n)) = if !n = (Array.length(s) - 1) then failwith("full stack") else (Array.set s (!n +1) x; n := !n +1) let top(s,n) = if !n = -1 then failwith("top is undefined") else Array.get s !n let pop(s,n) = if !n = -1 then failwith("pop is undefined") else n:= !n -1 let empty(s,n) = if !n = -1 then true else false let lungh(s,n) = !n let access ((s,n), k) = if not(k > !n) & not(k < 0) then Array.get s k else failwith("error in access") let svuota (s,n) = n := -1 type label = Tovisit| Ready| Revisited let nop = function () -> let x =ref(1) in x:= 0 let stacksize = 100 let cframesize(e) = 20 let tframesize1(e) = 20 let namestack = emptystack(stacksize,Id("dummy")) let dvalstack = emptystack(stacksize,alfa(Unbound)) let slinkstack = emptystack(stacksize, -1) type tag = Standard | Retained let tagstack = emptystack(stacksize, Standard) let currentenv = ref(0) let cstack = emptystack(stacksize,emptystack(1,(Tovisit,Eint(0)))) let tempvalstack = emptystack(stacksize,aemptystack(1,alfa(Unbound))) let newframes(e) = let cframe = emptystack(cframesize(e),(Tovisit,e)) in let tframe = aemptystack(tframesize1(e),alfa(Unbound)) in push((Tovisit,e),cframe); push(cframe,cstack); push(tframe,tempvalstack) let emptyenv = -1 let applyenv ((x: env), (y: ide)) = let n = ref(x) in let den = ref(alfa(Unbound)) in while !n > -1 do if access(namestack,!n)=y then (den := access(dvalstack,!n); n := -1) else n := access(slinkstack,!n) done; !den let bind ((r:env),i,d) = push(i,namestack); push(d,dvalstack); push(Standard,tagstack); push(r,slinkstack); currentenv:= lungh(dvalstack); !currentenv let size = 100 (* interprete astratto *) let makefun ((a:exp),(x:env)) = (match a with | Fun(ii,aa) -> alfa(Funval(a,x)) | _ -> failwith ("Non-functional object")) (* applyfun non fa nulla *) let applyfun ((a1:eval),(b:eval)) = b (* cambiano gli elementi di tempvalstack: operazioni rimpiazzate da quelle astratte *) let sem1 ((e:exp)) = let l = lungh(cstack) in newframes(e); while not(lungh(cstack) = l) do while not(empty(top(cstack))) do let continuation = top(cstack) in let tempstack = top(tempvalstack) in let rho = !currentenv in match top(continuation) with |(Tovisit,x) -> (pop(continuation); push((Ready,x),continuation); match x with | Pair(a,b) -> push((Tovisit,a),continuation); push((Tovisit,b),continuation) | Iszero(a) -> push((Tovisit,a),continuation) | Eq(a,b) -> push((Tovisit,a),continuation); push((Tovisit,b),continuation) | First(a) -> push((Tovisit,a),continuation) | Snd(a) -> push((Tovisit,a),continuation) | Prod(a,b) -> push((Tovisit,a),continuation); push((Tovisit,b),continuation) | Sum(a,b) -> push((Tovisit,a),continuation); push((Tovisit,b),continuation) | Diff(a,b) -> push((Tovisit,a),continuation); push((Tovisit,b),continuation) | Minus(a) -> push((Tovisit,a),continuation) | And(a,b) -> push((Tovisit,a),continuation); push((Tovisit,b),continuation) | Or(a,b) -> push((Tovisit,a),continuation); push((Tovisit,b),continuation) | Not(a) -> push((Tovisit,a),continuation) | Ifthenelse(a,b,c) -> push((Tovisit,a),continuation) | Appl(a,b) -> push((Tovisit,a),continuation); push((Tovisit,b),continuation) | Let(i,a,b) -> push((Tovisit,a),continuation) | (_) -> nop()) |(Ready,x) -> (pop(continuation); match x with | Eint(n) -> apush(alfa(Int(n)),tempstack) | Ebool(b) -> apush(alfa(Bool(b)),tempstack) | Var(i) -> let d = applyenv(rho,i) in (* if d = alfa(Unbound) then failwith "Unbound atom" else *) apush(d,tempstack) | Pair(a,b) -> let firstarg=atop(tempstack) in apop(tempstack); let sndarg=atop(tempstack) in apop(tempstack); apush(pair(firstarg,sndarg),tempstack) | Iszero(a) -> let arg=atop(tempstack) in apop(tempstack); apush(iszero(arg),tempstack) | Eq(a,b) -> let firstarg=atop(tempstack) in apop(tempstack); let sndarg=atop(tempstack) in apop(tempstack); apush(equ(firstarg,sndarg),tempstack) | First(a) -> let arg=atop(tempstack) in apop(tempstack); apush(first(arg),tempstack) | Snd(a) -> let arg=atop(tempstack) in apop(tempstack); apush(snd(arg),tempstack) | Prod(a,b) -> let firstarg=atop(tempstack) in apop(tempstack); let sndarg=atop(tempstack) in apop(tempstack); apush(mult(firstarg,sndarg),tempstack) | Sum(a,b) -> let firstarg=atop(tempstack) in apop(tempstack); let sndarg=atop(tempstack) in apop(tempstack); apush(plus(firstarg,sndarg),tempstack) | Diff(a,b) -> let firstarg=atop(tempstack) in apop(tempstack); let sndarg=atop(tempstack) in apop(tempstack); apush(diff(firstarg,sndarg),tempstack) | Minus(a) -> let arg=atop(tempstack) in apop(tempstack); apush(minus(arg),tempstack) | And(a,b) -> let firstarg=atop(tempstack) in apop(tempstack); let sndarg=atop(tempstack) in apop(tempstack); apush(et(firstarg,sndarg),tempstack) | Or(a,b) -> let firstarg=atop(tempstack) in apop(tempstack); let sndarg=atop(tempstack) in apop(tempstack); apush(vel(firstarg,sndarg),tempstack) | Not(a) -> let arg=atop(tempstack) in apop(tempstack); apush(non(arg),tempstack) | Ifthenelse(a,b,c) -> let arg=atop(tempstack) in apop(tempstack); if valid(arg) then push((Tovisit,b),continuation) else (if unsatisfiable(arg) then push((Tovisit,c),continuation) else (apush(arg,tempstack); push((Revisited,Ifthenelse(a,b,c)),continuation); push((Tovisit,b),continuation); push((Tovisit,c),continuation))) | Fun(i,a) -> apush(makefun(Fun(i,a),rho),tempstack) | Appl(a,b) -> let firstarg=atop(tempstack) in apop(tempstack); let sndarg=atop(tempstack) in apop(tempstack); apush(applyfun(firstarg,sndarg),tempstack) (* in Let e Letrec non si costruiscono nuovi frames: newframes(b) sostituita da un apush qualunque *) | Let(i,a,b) -> let arg=atop(tempstack) in apop(tempstack); bind(rho,i,arg); apush(alfa(Int 0),tempstack) | Letrec(i,a,b) -> bind(rho,i,makefun(a,lungh(dvalstack) + 1)); apush(alfa(Int 0),tempstack)) |(Revisited,x) -> (pop(continuation); match x with | Ifthenelse(a,b,c) -> let arg3 = atop(tempstack) in (apop(tempstack); let arg2 = atop(tempstack) in (apop(tempstack); let arg1 = atop(tempstack) in (apop(tempstack); apush(merge(arg1,arg2,arg3),tempstack)))) | _ -> failwith "caso impossibile") done; pop(cstack); done; let r = atop(top(tempvalstack)) in apop(top(tempvalstack)); r let tframesize ((e:exp)) = svuota(cstack);svuota(tempvalstack);svuota(dvalstack); svuota(namestack);svuota(slinkstack);svuota(tagstack); push(aemptystack(2,alfa(Unbound)),tempvalstack); bind(emptyenv,Id "dummy", alfa(Unbound)); match sem1(e) with | A(x) -> x end