(*INTERPRETE DENOTAZIONALE (procedure e fun e blocchi) *)

(* domini sintattici *)
type ide = string
type exp =
        | Eint of int
        | Ebool of bool
        | Estring of string
        | Den of ide
        | Prod of exp * exp
        | Sum of exp * exp
        | Diff of exp * exp
        | Eq of exp * exp
        | Minus of exp
        | Strlen of exp
        | Strsub of exp * exp * exp
        | Strcat of exp * exp
        | Strget of exp * exp
        | Reflect of exp
        | Iszero of exp
        | Or of exp * exp
        | And of exp * exp
        | Not of exp
        | Ifthenelse of exp * exp * exp
        | Val of exp
        | Let of ide * exp * exp
        | Newloc of exp
        | Fun of ide list * exp
        | Appl of exp * exp list
        | Rec of ide * exp
        | Proc of ide list * decl * com list
and decl = (ide * exp) list * (ide * exp) list
and com  =
        | Assign of exp * exp
        | Cifthenelse of exp * com list * com list
        | While of exp * com list
        | Block of decl * com list
        | Call of exp * exp list

(* implementazione funzionale dell'ambiente *)
(*
module Funenv:ENV =
struct *)
    exception WrongBindlist
    type 't env = string -> 't
    let emptyenv(x) = function y -> x
    let applyenv(x,y) = 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
(*)
  end
*)

(*
module type STORE =
sig
    type 't store
    type loc
    val emptystore : 't -> 't store
    val allocate : 't store * 't -> loc * 't store
    val update : 't store * loc * 't -> 't store
    val applystore : 't store * loc -> 't
end
module Funstore:STORE =
    struct
*)
        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 -> x
        let applystore(x,y) = 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)
(*
        end
*)

(* domini semantici *)
type eval =
        | Int of int
        | Bool of bool
        | String of string
        | Novalue
        | Funval of efun
and dval =
        | Dint of int
        | Dbool of bool
        | Dstring of string
        | Unbound
        | Dloc of loc
        | Dfunval of efun
        | Dprocval of proc
and mval =
        | Mint of int
        | Mbool of bool
        | Mstring of string
        | Undefined
and efun = (dval list) * (mval store) -> eval           (*scoping statico*)
and proc = (dval list) * (mval store) -> mval store

exception Nonstorable
exception Nonexpressible
let evaltomval e = match e with
    | Int n -> Mint n
    | Bool n -> Mbool n
    | String n ->Mstring n
    | _ -> raise Nonstorable
let mvaltoeval m = match m with
    | Mint n -> Int n
    | Mbool n -> Bool n
    | Mstring n -> String n
    | _ -> Novalue
let evaltodval e = match e with
    | Int n -> Dint n
    | Bool n -> Dbool n
    | String n -> Dstring n
    | Novalue -> Unbound
    | Funval n -> Dfunval n
let dvaltoeval e = match e with
    | Dint n -> Int n
    | Dbool n -> Bool n
    | Dstring n -> String n
    | Dloc n -> raise Nonexpressible
    | Dfunval n -> Funval n
    | Dprocval n -> raise Nonexpressible
    | Unbound -> Novalue

(* operazioni primitive *)
let typecheck (x, y) = match x with
    | "int" -> (match y with
                    | Int(u) -> true
                    | _ -> false)
    | "bool" -> (match y with
                        | Bool(u) -> true
                        | _ -> false)
    | "string"-> (match y with
                        | String(u)-> true
                        | _ ->false)
    | _ -> failwith ("not a valid type")
let minus x = if typecheck("int",x) then (match x with Int(y) -> Int(-y) )
    else failwith ("type error")
let iszero x = if typecheck("int",x) then (match x with Int(y) -> Bool(y=0) )
    else failwith ("type error")
let equ (x,y) = if typecheck("int",x) & typecheck("int",y)
    then (match (x,y) with (Int(u), Int(w)) -> Bool(u = w))
    else failwith ("type error")
let plus (x,y) = if typecheck("int",x) & typecheck("int",y)
    then (match (x,y) with (Int(u), Int(w)) -> Int(u+w))
    else failwith ("type error")
let diff (x,y) = if typecheck("int",x) & typecheck("int",y)
    then (match (x,y) with (Int(u), Int(w)) -> Int(u-w))
    else failwith ("type error")
let mult (x,y) = if typecheck("int",x) & typecheck("int",y)
    then (match (x,y) with (Int(u), Int(w)) -> Int(u*w))
    else failwith ("type error")
let strlen (x) =if typecheck("string", x)
    then (match (x) with (String(u))-> Int(String.length u))
    else failwith("Type error")
let strcat (x,y) =if typecheck("string", x) & typecheck("string",y)
    then (match (x,y) with (String(u), String(w)) -> String(String.concat "" [u;w]))
    else failwith("Type error")
let strsub (x,y,z) =if typecheck("string", x) & typecheck("int",y) & typecheck("int",z)
    then (match (x,y,z) with (String(u), Int(w),Int(v)) -> String(String.sub u w (v-w)))
    else failwith("Type error")
let strget (x,y) =if typecheck("string", x) & typecheck("int",y)
    then (match (x,y) with (String(u), Int(w)) -> String(String.make 1 (String.get u w)))
    else failwith("Type error")
let et (x,y) = if typecheck("bool",x) & typecheck("bool",y)
    then (match (x,y) with (Bool(u), Bool(w)) -> Bool(u & w))
    else failwith ("type error")
let vel (x,y) = if typecheck("bool",x) & typecheck("bool",y)
    then (match (x,y) with (Bool(u), Bool(w)) -> Bool(u or w))
    else failwith ("type error")
let non x = if typecheck("bool",x)
    then (match x with Bool(y) -> Bool(not y) )
    else failwith ("type error")
(*let rec elemEval (e:string) =
    let funComp=String.split_on_char '(' e in
    let funName=funComp.hd in
    let funParams=String.split_on_char ',' (funComp.nth 1) in


    match funName with
    | "Assign" -> sem Assign((funParams.nth 0),(funParams.nth 0))
  |
  (*let regExp= Str.regExp "(Assign)";;
  if Str.string_match regExp e 0
  then Assign()*)
  let reflect (x, r, s)  =if typecheck("string",x)
    then (match(x)with (String(u))-> let strList=String.split_on_char ';' u in
        for s in strList:
            elemEval s r s
    )
    else failwith("Type error");*)

(*
Togliere quadre

prova 1:
aggiungere reflect in sem con r & s

*)
(* fino a qui giusto *)


(* funzioni di valutazione semantica (denotazionale)  *)
let rec makefun ((a:exp),(x:dval env)) = match a with
    | Fun(ii,aa) -> Dfunval(function (d, s) -> sem aa (bindlist (x, ii, d)) s)
    | _ -> failwith ("Non-functional object")
and makefunrec (i, Fun(ii, aa), r) =
    let functional ff (d, s1) =
            let r1 = bind(bindlist(r, ii, d), i, Dfunval(ff)) in sem aa r1 s1 in
            let rec fix = function x -> functional fix x in Funval(fix)
and makeproc((a:exp),(x:dval env)) = match a with
    | Proc(ii,dl,cl) -> Dprocval(function (d, s) -> semb (dl,cl) (bindlist (x, ii, d)) s)
    | _ -> failwith ("Non-functional object")
and applyfun ((ev1:dval),(ev2:dval list), s) = match ev1 with
    | Dfunval(x) -> x (ev2, s)
    | _ -> failwith ("attempt to apply a non-functional object")
and applyproc ((ev1:dval),(ev2:dval list), s) = match ev1 with
    | Dprocval(x) -> x (ev2, s)
    | _ -> failwith ("attempt to apply a non-functional object")
and sem (e:exp) (r:dval env) (s: mval store) =
        match e with
            | Eint(n) -> Int(n)
            | Ebool(b) -> Bool(b)
            | Estring(s)-> String(s)
            | Den(i) -> dvaltoeval(applyenv(r,i))
            | Iszero(a) -> iszero((sem a r s) )
            | 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))
            | Minus(a) -> minus( (sem a r s))
            | And(a,b) -> et ( (sem a r s), (sem b r s))
            | Or(a,b) -> vel ( (sem a r s), (sem b r s))
            | Not(a) -> non( (sem a r s))
            | Strlen(a) -> strlen( (sem a r s))

    (*      | Reflect(a) -> reflect( (sem a r s) r s)*)

            | Strcat(a,b) -> strcat( (sem a r s),(sem b r s))
            | Strsub(a,b,c) -> strsub((sem a r s),(sem b r s),(sem c r s))
            | Strget (a,b) -> strget((sem a r s),(sem b r s))
            | Ifthenelse(a,b,c) -> let g = sem a r s in
                    if typecheck("bool",g) then (if g = Bool(true) then sem b r s else 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"))
            | Let(i,e1,e2) -> let (v, s1) = semden e1 r s in sem e2 (bind (r ,i, v)) s1
            | Fun(i,e1) -> dvaltoeval(makefun(e,r))
            | Rec(i,e1) -> makefunrec(i, e1, r)
            | Appl(a,b) -> let (v1, s1) = semlist b r s in applyfun(evaltodval(sem a r s), v1, s1)
            | _ -> failwith ("nonlegal expression for sem")
and semden (e:exp) (r:dval env) (s: mval store) = match e with
    | Den(i) -> (applyenv(r,i), s)
    | Fun(i, e1) -> (makefun(e, r), s)
    | Proc(i, dl, cl) -> (makeproc(e, r), 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)
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)
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(s1, n, evaltomval(sem e2 r s))
        | _ -> failwith ("wrong location in assignment"))
    | Cifthenelse(e, cl1, cl2) -> let g = sem e r s in
        if typecheck("bool",g) then
        (if g = Bool(true) then semcl cl1 r s else semcl cl2 r s)
            else failwith ("nonboolean guard")
    | While(e, cl) ->
        let functional ((fi: mval store -> mval store)) =
            function sigma ->
            let g = sem e r sigma in
            if typecheck("bool",g) then
                (if g = Bool(true) then fi(semcl cl r sigma) else sigma)
                else failwith ("nonboolean guard")
            in
            let rec ssfix = function x -> functional ssfix x in ssfix(s)
    | Call(e1, e2) -> let (p, s1) = semden e1 r s in let (v, s2) = semlist e2 r s1 in
        applyproc(p, v, s2)
    | Block(dl,cl) -> semb (dl, cl) r s
and semcl cl r s = match cl with
    | [] -> s
    | c::cl1 -> semcl cl1 r (semc c r s)
    | _ -> failwith ("wrong semcl")

(* semantica di blocchi e dichiarazioni and semb ((dl, rdl), cl) r s =*)
and semb ((dl, rdl), cl) r s =
    let (r1, s1) = semdl (dl, rdl) r s in semcl cl r1 s1
and semdl (dl, rl) r s = let (r1, s1) = semdv dl r s in
        semdr rl r1 s1
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
and semdr rl r s =
    let functional ((r1: dval env)) = (match rl with
                                            | [] -> r
                                            | (i,e) :: rl1 -> let (v, s2) = semden e r1 s in
                                                    let (r2, s3) = semdr rl1 (bind(r, i, v)) s in r2) in
    let rec rfix = function x -> functional rfix x in (rfix, s)


let d = [("x",Newloc(Estring "Prova"));("w", Newloc(Estring ""));("y", Newloc(Eint 2));("z", Newloc(Eint 4))];;
let ex =[Assign(Den "w", Strsub(Val(Den "x"),Val(Den "y"),Val(Den "z")))];;
let (rho2, sigma2) = semdv d (emptyenv Unbound) (emptystore Undefined);;
let sigma3 = semcl ex rho2 sigma2;;
sem (Val(Den "w")) rho2 sigma3


let d = [("x",Newloc(Estring "Prova"));("w", Newloc(Estring ""));("y", Newloc(Eint 2))];;
let ex =[Assign(Den("w"),Strget(Val(Den "x"),Val(Den "y")))];;
let (rho2, sigma2) = semdv d (emptyenv Unbound) (emptystore Undefined);;
let sigma3 = semcl ex rho2 sigma2;;
sem (Val(Den "w")) rho2 sigma3

(*
esempi:



FATTORIALE:
# let d = [("z",Newloc(Eint 4));("w",Newloc(Eint 1))];;
val d : (string * exp) list = ["z", Newloc (Eint 4); "w", Newloc (Eint 1)]
# let ex = [While(Not(Eq(Val(Den "z"), Eint 0)),
    [Assign(Den "w", Prod(Val(Den "w"),Val(Den "z")));
    Assign(Den "z", Diff(Val(Den "z"), Eint 1))])];;
val ex : com list =
    [While
    (Not (Eq (Val (Den "z"), Eint 0)),
        [Assign (Den "w", Prod (Val (Den "w"), Val (Den "z")));
            Assign (Den "z", Diff (Val (Den "z"), Eint 1))])]
# let (rho2, sigma2) = semdv d (emptyenv Unbound) (emptystore Undefined);;
val rho2 : dval Funenv.env = <abstr>
val sigma2 : mval Funstore.store = <abstr>
# let sigma3 = semcl ex rho2 sigma2;;
val sigma3 : mval Funstore.store = <abstr>
# sem (Val(Den "z")) rho2 sigma3;;
- : eval = Int 0
# sem (Val(Den "w")) rho2 sigma3;;
- : eval = Int 24

int z=4;
int w=1;

ex:
while(z!=0){
    w=w*z;
    z=z-1;
}

print(z); ->0
print(w); ->24
*)

(*let(mdiccom: decl * com list) =
    ([("y", Newloc (Eint 0))],
    [("impfact", Proc(["x"],
        ([("z", Newloc(Den "x")) ;("w", Newloc(Eint 1))],
        [],
        [While(Not(Eq(Val(Den "z"), Eint 0)),
            [Assign(Den "w", Prod(Val(Den "w"),Val(Den "z")));
            Assign(Den "z", Diff(Val(Den "z"), Eint 1))]);
    Cifthenelse
        (Eq (Val (Den "w"), Appl (Den "fact", [Den "x"])),
        [Assign (Den "y", Val (Den "w"))],
        [Assign (Den "y", Eint 0)])] )));
    ("fact", Fun(["x"],
        Ifthenelse (Eq (Den "x", Eint 0), Eint 1,
            Prod (Den "x", Appl (Den "fact", [Diff (Den "x", Eint 1)])))) )],
    [ Call(Den "impfact", [Eint 4])]) ;;

 let itestore1 = semb mdiccom (emptyenv Unbound) (emptystore Undefined);;
 applystore(itestore1, 0);;*)
(*- : mval = Mint 24*)
(*let mdiccom =
 ([("y", Newloc (Eint 0))],
 [("impfact", Proc(["x"],
 ([("z", Newloc(Den "x")) ;("w", Newloc(Eint 1))],
 [],
 [While(Not(Eq(Val(Den "z"), Eint 0)),
 [Assign(Den "w", Prod(Val(Den "w"),Val(Den "z")));
 Assign(Den "z", Diff(Val(Den "z"), Eint 1))]);
 Cifthenelse
 (Eq (Val (Den "w"), Appl (Den "fact", [Den "x"])),
 [Assign (Den "y", Val (Den "w"))],
 [Assign (Den "y", Eint 0)])] )));
 ("fact", Fun(["x"],
 Ifthenelse (Eq (Den "x", Eint 0), Eint 1,
 Prod (Den "x", Appl (Den "fact", [Diff (Den "x", Eint 1)])))) )],
 [ Call(Den "impfact", [Eint 4])]) ;;
 let itestore1 = semb mdiccom (emptyenv Unbound) (emptystore Undefined);;
 applystore(itestore1, 0);;*)