(* Ambiente e operazioni *) type 't env = string -> 't exception WrongBindlist let emptyenv(x) = function (y:string) -> x let applyenv(x,(y:string)) = x y let bind((r: 'a env) , (l:string), (e:'a)) = function lu -> if lu = l then e else applyenv(r,lu) let rec bindlist(r, il, el) = match (il,el) with | ([],[]) -> r | i::il1, e::el1 -> bindlist (bind(r, i, e), il1, el1) | _ -> raise WrongBindlist (* Memoria e operazioni *) type loc = int type 't store = loc -> 't let (newloc,initloc) = let count = ref(-1) in (fun () -> count := !count +1; !count), (fun () -> count := -1) let emptystore(x) = initloc(); function (y:loc) -> x let applystore((x: 'a store),(y: loc)) = x y let allocate((r: 'a store) , (e:'a)) = let l = newloc() in (l, function lu -> if lu = l then e else applystore(r,lu)) let update((r: 'a store) , (l:loc), (e:'a)) = function lu -> if lu = l then e else applystore(r,lu) (* SYNTACTIC DOMAINS *) type ide = string type exp = | Eint of int | Ebool of bool | Den of ide | Prod of exp * exp | Sum of exp * exp | Diff of exp * exp | Eq of exp * exp | Not of exp | Ifthenelse of exp * exp * exp | Val of exp | Newloc of exp and com = | Assign of exp * exp | Cifthenelse of exp * com list * com list | While of exp * com list (* SEMANTIC DOMAINS *) exception Nonstorable exception Nonexpressible type eval = | Int of int | Bool of bool | Novalue and dval = | Dint of int | Dbool of bool | Unbound | Dloc of loc and mval = | Mint of int | Mbool of bool | Undefined let evaltomval e = match e with | Int n -> Mint n | Bool n -> Mbool n | _ -> raise Nonstorable let mvaltoeval m = match m with | Mint n -> Int n | Mbool n -> Bool n | _ -> Novalue let evaltodval e = match e with | Int n -> Dint n | Bool n -> Dbool n | Novalue -> Unbound let dvaltoeval e = match e with | Dint n -> Int n | Dbool n -> Bool n | Dloc n -> raise Nonexpressible | Unbound -> Novalue (* Operations on Eval *) let equ (x,y) = (match (x,y) with | (Int(u), Int(w)) -> Bool(u = w) | (Bool(u), Bool(w)) -> Bool(u = w) | _ -> failwith ("type error")) let plus (x,y) = (match (x,y) with | (Int(u), Int(w)) -> Int(u+w) | _ -> failwith ("type error")) let diff (x,y) = (match (x,y) with | (Int(u), Int(w)) -> Int(u-w) | _ -> failwith ("type error")) let mult (x,y) = (match (x,y) with | (Int(u), Int(w)) -> Int(u*w) |_ -> failwith ("type error")) let non x = (match x with | Bool(y) -> Bool(not y) |_ -> failwith ("type error")) (* semantica di espressioni *) let rec sem ((e:exp), (r:dval env), (s: mval store)) = match e with | Eint(n) -> Int(n) | Ebool(b) -> Bool(b) | Den(i) -> dvaltoeval(applyenv(r,i)) | Eq(a,b) -> equ(sem(a, r, s), sem(b, r, s)) | Prod(a,b) -> mult (sem(a, r, s), sem(b, r, s)) | Sum(a,b) -> plus (sem(a, r, s), sem(b, r, s)) | Diff(a,b) -> diff (sem(a, r, s), sem(b, r, s)) | Not(a) -> non(sem(a, r, s)) | Ifthenelse(a,b,c) -> let g = sem(a, r, s) in (if g = Bool(true) then sem(b, r, s) else (if g = Bool(false) then sem(c, r, s) else failwith ("nonboolean guard"))) | Val(e) -> let (v, s1) = semden(e, r, s) in (match v with | Dloc n -> mvaltoeval(applystore(s1, n)) | _ -> failwith("not a variable")) | _ -> failwith ("nonlegal expression for sem") (* semantica di lista di espressioni *) and semlist(el, r, s) = match el with | [] -> ([], s) | e::el1 -> let (v1, s1) = semden(e, r, s) in let (v2, s2) = semlist(el1, r, s1) in (v1 :: v2, s2) (* semantica di espressioni come dval, per legarle nell'ambiente *) and semden ((e:exp), (r:dval env), (s: mval store)) = match e with | Den(i) -> (applyenv(r,i), s) | Newloc(e) -> let m = evaltomval(sem(e, r, s)) in let (l, s1) = allocate(s, m) in (Dloc l, s1) | _ -> (evaltodval(sem(e, r, s)), s) (* semantica di lista di espressioni come dval *) and semdv(dl, r, s) = match dl with | [] -> (r,s) | (i,e)::dl1 -> let (v, s1) = semden(e, r, s) in semdv(dl1, bind(r, i, v), s1) (* semantica di comandi *) and semc((c: com), (r:dval env), (s: mval store)) = match c with | Assign(e1, e2) -> let (v1, s1) = semden(e1, r, s) in (match v1 with | Dloc(n) -> update(s, n, evaltomval(sem(e2, r, s))) | _ -> failwith ("wrong location in assignment")) | Cifthenelse(e, cl1, cl2) -> let g = sem(e, r, s) in (if g = Bool(true) then semcl(cl1, r, s) else (if g = Bool(false) then semcl (cl2, r, s) else failwith ("nonboolean guard"))) | While(e, cl) -> let g = sem(e, r, s) in (if g = Bool(true) then semcl((cl @ [While(e, cl)]), r, s) else (if g = Bool(false) then s else failwith ("nonboolean guard"))) (* semantica di lista di comandi *) and semcl(cl, r, s) = match cl with | [] -> s | c::cl1 -> semcl(cl1, r, semc(c, r, s))