(* INTERPRETE ASTRATTO SUI TIPI: diverso Ceval, aggiunta in applyfun, e funzione per inferire i tipi funzionali *) module type interpr = sig open Expr open Tipi open Ceval open Struttrt val applyfun: eval * eval -> eval val makefun: exp * env -> eval val sem : exp -> tipo val sem1 : exp -> eval val inffuncttype : eval -> eval val initstate: unit -> unit end module Interpr: interpr = struct open Expr open Tipi open Ceval open Struttrt let initstate () = currentenv := lungh(dvalstack) let makefun ((a:exp),(x:env)) = (match a with | Fun(ii,aa) -> alfa(Funval(a,x)) | _ -> failwith ("Non-functional object")) (* applyfun con nuovo caso *) 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 | Unbound -> (match (a1,b) with | (T(v,c),T(vb,cb)) -> let v1 = newvar() in let v2 = newvar() in let sigma = unifylist( (v, (down(Mkarrow(up(v1),up(v2))))) :: (vb,v1) :: (c @ cb)) in T(applysubst sigma v2,sigma) | (T(v,c), T1(b1)) -> (match inffuncttype(b) with | T(vb,cb) -> let v1 = newvar() in let v2 = newvar() in let sigma = unifylist( (v, (down(Mkarrow(up(v1),up(v2))))) :: (vb,v1) :: (c @ cb)) in T(applysubst sigma v2,sigma) | _ -> failwith "errore in applyfun") | _ -> failwith "errore in applyfun")) (* nuova *) and inffuncttype (e) = match e with | T1 (x) -> let v1 = newvar() in initstate(); let f1 = applyfun(e,T(v1,[])) in let f2 = inffuncttype(f1) in (match f2 with | T(v2,c2) -> let sigma = unifylist(c2) in T(applysubst sigma (down(Mkarrow(up(v1),up(v2)))),sigma) | _ -> failwith "caso impossibile") | x -> x 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 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)); let r = inffuncttype(sem1(e)) in (match r with | T(v,c) -> up(v) | _ -> failwith "errore nel'inferenza dei tipi") end