(* INTERPRETE ITERATIVO IN VERSIONE COLLECTING CON TABULAZIONE *) module type interpr = sig open Expr open Ceval open Struttrt val applyfun: eval * eval -> eval val makefun: exp * env -> eval val sem : exp -> eval val sem1 : exp -> eval val initstate: unit -> unit end (* reintroduzione della ricorsione per le applicazioni di funzione, alfa dei valori concreti, trattamento collecting del condizionale, tabulazione applyfun *) module Interpr: interpr = struct open Expr open Ceval open Struttrt let makefun ((a:exp),(x:env)) = (match a with | Fun(ii,aa) -> alfa(Funval(a,x)) | _ -> failwith ("Non-functional object")) (* applyfun con memoing *) let rec applyfun ((a1:eval),(b:eval)) = (match (gamma a1) with | Funval(Fun(ii,aa),x) -> let i = ref(0) in let v = ref(alfa(Indef)) in while !i < size do if Array.get tproc !i = (Fun(ii,aa),x) & abstreq(Array.get targ !i, b) then (v := Array.get tres !i; i := size) else (if Array.get tproc !i = emptyclos then (Array.set tproc !i (Fun(ii,aa),x); Array.set targ !i b; Array.set tres !i !v; bind(x,ii,b); v := sem1(aa); Array.set tres !i !v; i := size) else i := !i +1) done; !v | _ -> failwith ("attempt to apply a non-functional object")) and 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) -> push(alfa(Int(n)),tempstack) | Ebool(b) -> push(alfa(Bool(b)),tempstack) | Var(i) -> let d = applyenv(rho,i) in if d = alfa(Unbound) then failwith "Unbound atom" else push(d,tempstack) | Pair(a,b) -> let firstarg=top(tempstack) in pop(tempstack); let sndarg=top(tempstack) in pop(tempstack); push(pair(firstarg,sndarg),tempstack) | Iszero(a) -> let arg=top(tempstack) in pop(tempstack); push(iszero(arg),tempstack) | Eq(a,b) -> let firstarg=top(tempstack) in pop(tempstack); let sndarg=top(tempstack) in pop(tempstack); push(equ(firstarg,sndarg),tempstack) | First(a) -> let arg=top(tempstack) in pop(tempstack); push(first(arg),tempstack) | Snd(a) -> let arg=top(tempstack) in pop(tempstack); push(snd(arg),tempstack) | Prod(a,b) -> let firstarg=top(tempstack) in pop(tempstack); let sndarg=top(tempstack) in pop(tempstack); push(mult(firstarg,sndarg),tempstack) | Sum(a,b) -> let firstarg=top(tempstack) in pop(tempstack); let sndarg=top(tempstack) in pop(tempstack); push(plus(firstarg,sndarg),tempstack) | Diff(a,b) -> let firstarg=top(tempstack) in pop(tempstack); let sndarg=top(tempstack) in pop(tempstack); push(diff(firstarg,sndarg),tempstack) | Minus(a) -> let arg=top(tempstack) in pop(tempstack); push(minus(arg),tempstack) | And(a,b) -> let firstarg=top(tempstack) in pop(tempstack); let sndarg=top(tempstack) in pop(tempstack); push(et(firstarg,sndarg),tempstack) | Or(a,b) -> let firstarg=top(tempstack) in pop(tempstack); let sndarg=top(tempstack) in pop(tempstack); push(vel(firstarg,sndarg),tempstack) | Not(a) -> let arg=top(tempstack) in pop(tempstack); push(non(arg),tempstack) | Ifthenelse(a,b,c) -> let arg=top(tempstack) in pop(tempstack); if valid(arg) then push((Tovisit,b),continuation) else (if unsatisfiable(arg) then push((Tovisit,c),continuation) else (push(arg,tempstack); push((Revisited,Ifthenelse(a,b,c)),continuation); push((Tovisit,b),continuation); push((Tovisit,c),continuation))) | Fun(i,a) -> push(makefun(Fun(i,a),rho),tempstack) | Appl(a,b) -> let firstarg=top(tempstack) in pop(tempstack); let sndarg=top(tempstack) in pop(tempstack); push(applyfun(firstarg,sndarg),tempstack) | Let(i,a,b) -> let arg=top(tempstack) in pop(tempstack); bind(rho,i,arg); newframes(b) | Letrec(i,a,b) -> bind(rho,i,makefun(a,lungh(dvalstack) + 1)); newframes(b)) |(Revisited,x) -> (pop(continuation); match x with | Ifthenelse(a,b,c) -> let arg3 = top(tempstack) in (pop(tempstack); let arg2 = top(tempstack) in (pop(tempstack); let arg1 = top(tempstack) in (pop(tempstack); push(merge(arg1,arg2,arg3),tempstack)))) | _ -> failwith "caso impossibile") done; let valore= top(top(tempvalstack)) in pop(cstack); pop(tempvalstack); push(valore,top(tempvalstack)); if !currentenv < lungh(dvalstack) then retain() else if abstrproc(valore) then retain() else (pop(tagstack); pop(namestack); pop(dvalstack); pop(slinkstack); while not(empty(dvalstack)) & retained(lungh(dvalstack)) do pop(tagstack); pop(namestack); pop(dvalstack); pop(slinkstack) done; currentenv := lungh(dvalstack)) done; let r = top(top(tempvalstack)) in pop(top(tempvalstack)); r (* per provare ad applicare le funzioni quando vengono ritornate, si puo' fare una sola applicazione *) let initstate () = currentenv := lungh(dvalstack) (* inizializzazioni dello stato *) let sem ((e:exp)) = svuota(cstack);svuota(tempvalstack);svuota(dvalstack); svuota(namestack);svuota(slinkstack);svuota(tagstack); inittables(); push(emptystack(2,alfa(Unbound)),tempvalstack); bind(emptyenv,Id "dummy", alfa(Unbound)); sem1(e) end