(* INTERPRETE ASTRATTO SUI NOMI *) module type names = sig open Expr type ceval type eval = | Ok | T1 of ceval | Tunbound val checknames : exp -> eval end module Namecheck: names = struct open Expr type env = int type proc = exp * env and ceval = | Funval of proc | Mkpair of ceval * ceval | Int of int | Bool of bool | Unbound | Indef type eval = | Ok | T1 of ceval | Tunbound let alfa (x) = match x with | Int(n) -> Ok | Bool(n) -> Ok | Indef -> Ok | Unbound -> Tunbound | Funval(a,b) -> T1(Funval(a,b)) | _ -> failwith "manca il caso del Mkpair" let gamma (x) = match x with | T1(y) -> y | _ -> Unbound let abstrproc (b) = let b1 = gamma(b) in (match b1 with | Funval(x,y) -> true | _ -> false) let abstreq (x,y) = (x = y) let minus x = match x with | Ok -> Ok | _ -> failwith ("type error") let iszero x = match x with | Ok -> Ok | _ -> failwith ("type error") let equ (x,y) = match (x,y) with | (Ok,Ok) -> Ok | _ -> failwith ("type error") let plus (x,y) = match (x,y) with | (Ok,Ok) -> Ok | _ -> failwith ("type error") let diff (x,y) = match (x,y) with | (Ok,Ok) -> Ok | _ -> failwith ("type error") let mult (x,y) = match (x,y) with | (Ok,Ok) -> Ok | _ -> failwith ("type error") let pair (x,y) = match (x,y) with | (Ok,Ok) -> Ok | _ -> failwith ("type error") let first x = match x with | Ok -> Ok |_ -> failwith ("type error") let snd x = match x with | Ok -> Ok |_ -> failwith ("type error") let et (x,y) = match (x,y) with | (Ok,Ok) -> Ok | _ -> failwith ("type error") let vel (x,y) = match (x,y) with | (Ok,Ok) -> Ok | _ -> failwith ("type error") let non x = match x with | Ok -> Ok | _ -> failwith ("type error") let merge (g,x,y) = match (g,x,y) with | (Ok,Ok,Ok) -> Ok | _ -> failwith ("type error") let valid (x) = false let unsatisfiable (x) = false 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 tframesize(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 retained (n:env) = if access(tagstack,n) = Retained then true else false let currentenv = ref(0) let cstack = emptystack(stacksize,emptystack(1,(Tovisit,Eint(0)))) let tempvalstack = emptystack(stacksize,emptystack(1,alfa(Unbound))) let newframes(e) = let cframe = emptystack(cframesize(e),(Tovisit,e)) in let tframe = emptystack(tframesize(e),alfa(Unbound)) in push((Tovisit,e),cframe); push(cframe,cstack); push(tframe,tempvalstack) let retain () = match tagstack with (a,m) -> Array.set a !currentenv Retained; let cont = ref(lungh(dvalstack)) in while !cont > -1 & retained(!cont) do cont := !cont - 1 done; currentenv := !cont 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 let emptyclos = (Eint 1 ,-1) let tproc = Array.create size emptyclos let targ = Array.create size (alfa Unbound) let tres = Array.create size (alfa Indef) let inittables () = let i = ref(0) in while !i < size do Array.set tproc !i emptyclos; i := !i + 1 done 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")) 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 | (Ok,Ok) -> Ok | (Ok, T1(b1)) -> (match inffuncttype(b) with | Ok -> Ok | _ -> failwith "errore in applyfun") | _ -> failwith "errore in applyfun")) and inffuncttype (e) = match e with | T1 (x) -> let v1 = Ok in initstate(); let f1 = applyfun(e,v1) in let f2 = inffuncttype(f1) in (match f2 with | Ok -> Ok | _ -> 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 checknames ((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)); inffuncttype(sem1(e)) end