(* FRAME E STACK *) type 'a bottom = Bottom | Def of 'a;; let omega x = Bottom;; let add f x y = match f x with Bottom -> let g z = if z=x then y else f z in g;; let update f x y = match f x with z when z<>Bottom -> let g z = if z=x then y else f z in g;; let rec add_stack pi x y = match pi with f::pi' -> (add f x y)::pi';; let rec update_stack pi x y = match pi with f::pi' when f x <> Bottom -> (update f x y)::pi' | f::pi' when f x = Bottom -> f :: (update_stack pi' x y);; let rec search pi x = match pi with [] -> Bottom | f :: pi' when f x <> Bottom -> f x | f :: pi' when f x = Bottom -> search pi' x;; (* SINTASSI DEL LINGUAGGIO IMPERATIVO *) type ide == string;; (* ESPRESSIONI *) type bop = Add | Sub | Mul | Div | Mod | Gt | Gte | Lt | Lte | Eq | Neq | And | Or;; type uop = Minus | Not;; type exp = Ide of ide | Num of int | Bool of bool | BinExp of exp*bop*exp | UnExp of uop*exp;; (* DICHIARAZIONI *) type dec = Var of ide | Var_init of ide * exp;; (* COMANDI *) type com = Assign of ide * exp | If_then_else of exp*com*com | If_then of exp*com | While of exp*com | Block of dec list * com list ;; type prog = Prog of dec list * com list;; (* DOMINI SEMANTICI *) (* VALORI *) type val = ValN of int | ValB of bool | Unknown ;; (* Locazioni memoria *) type mloc == int;; (* Frame ambiente *) type amb == ide -> mloc bottom;; (* Frame memoria *) type mem == mloc -> val bottom;; let succloc (m:mem list) = let rec findunused m n = match search m n with Bottom -> (n:mloc) | _ -> findunused m (n+1) in findunused m 0;; (* SEMANTICA DELLE ESPRESSIONI *) let sembop o= match o with Add -> let f v1 v2 = match (v1,v2) with (ValN n1,ValN n2) -> ValN (n1+n2) in f | Sub -> let f v1 v2 = match (v1,v2) with (ValN n1,ValN n2) -> ValN (n1-n2) in f | Mul -> let f v1 v2 = match (v1,v2) with (ValN n1,ValN n2) -> ValN (n1*n2) in f | Div -> let f v1 v2 = match (v1,v2) with (ValN n1,ValN n2) -> ValN (n1/n2) in f | Mod -> let f v1 v2 = match (v1,v2) with (ValN n1,ValN n2) -> ValN (n1 mod n2) in f | Gt -> let f v1 v2 = match (v1,v2) with (ValN n1,ValN n2) -> ValB (n1 > n2) in f | Gte -> let f v1 v2 = match (v1,v2) with (ValN n1,ValN n2) -> ValB (n1 >= n2) in f | Lt -> let f v1 v2 = match (v1,v2) with (ValN n1,ValN n2) -> ValB (n1 < n2) in f | Lte -> let f v1 v2 = match (v1,v2) with (ValN n1,ValN n2) -> ValB (n1 <= n2) in f | Eq -> let f v1 v2 = match (v1,v2) with (ValN n1,ValN n2) -> ValB (n1 = n2) in f | Neq -> let f v1 v2 = match (v1,v2) with (ValN n1,ValN n2) -> ValB (n1 <> n2) in f | And -> let f v1 v2 = match (v1,v2) with (ValB b1,ValB b2) -> ValB (b1 & b2) in f | Or -> let f v1 v2 = match (v1,v2) with (ValB b1,ValB b2) -> ValB (b1 or b2) in f ;; let semuop o = match o with Minus -> let f v1 = match v1 with ValN n -> ValN (-n) in f | Not -> let f v1 = match v1 with ValB b -> ValB (not b) in f;; (* SEM_e *) let rec semexp e (a:amb list) (m:mem list) = match e with Ide i -> (let (Def l) = search a i in let (Def v) = search m l in v) | Num n -> ValN n | Bool b -> ValB b | BinExp (e1,o,e2) -> sembop o (semexp e1 a m) (semexp e2 a m)| UnExp (o,e1) -> semuop o (semexp e1 a m);; (* SEMANTICA DELLE DICHIARAZIONI *) (* Sem_d *) let semd d (a:amb list) (m : mem list) = match d with Var x -> ((add_stack a x (Def (succloc m)), add_stack m (succloc m) (Def Unknown)): (amb list * mem list)) | Var_init(x,e) -> let v = (semexp e a m) in (add_stack a x (Def (succloc m)), add_stack m (succloc m) (Def v));; (* Sem_dl *) let rec semdl dl (a:amb list) (m : mem list) = match dl with [] -> (a,m) | d::ds -> let a',m'=semd d a m in semdl ds a' m';; (* SEMANTICA DEI COMANDI *) (* Sem_c e Sem_cl *) let rec semc c (a:amb list) (m:mem list) = match c with Assign(x,e) -> let v = (semexp e a m) and (Def l) = (search a x) in (update_stack m l (Def v): mem list) | If_then_else(e,c1,c2) -> (match semexp e a m with ValB true -> semc c1 a m | ValB false -> semc c2 a m ) | If_then(e,c1) -> (match semexp e a m with ValB true -> semc c1 a m | ValB false -> m ) | While(e,c1) -> (match semexp e a m with ValB false -> m | ValB true -> let m' = semc c1 a m in semc (While(e,c1)) a m') | Block(dl,cl) -> let (a', m') = semdl dl (omega::a) (omega::m) in let (fm :: m'') = semcl cl a' m' in m'' and semcl cl a m = match cl with [] -> m | c::cs -> semcl cs a (semc c a m) ;; (*Semantica di un programma *) (*Sem_prog *) let semprog p = match p with Prog(dl,cl) -> semc (Block(dl,cl)) [] [];;