(*
    MINIPASCAL, by Artur Miguel Dias and Luis Caires, June 2000  
	   corrigido
*)



(* Funcoes auxiliares *)

let rec len =
    function [] -> 0
           | x::xs -> 1 + len xs
;;




(* SINTAXE da linguagem MiniPascal *)

type Exp =
      NumConst of int
    | BoolConst of bool
    | Var of string
    | Add of Exp * Exp
    | Sub of Exp * Exp
    | Mult of Exp * Exp
    | Div of Exp * Exp
    | Equal of Exp * Exp
    | Diff of Exp * Exp
    | Seq of Exp * Exp
    | If of Exp * Exp * Exp
    | While of Exp * Exp
    | Val of string
    | Assign of string * Exp
    | Apply of string * (Exp list)
    | LetCon of string * Exp * Exp
    | LetVar of string * Exp * Exp
    | LetFun of string * (string list) * Exp * Exp
;;



(* VALORES = Resultados + Denotacoes *)

type Value =
      Num of int
    | Bool of bool
    | Done
    | Closure of ((string * Value) list) * Abstraction
    | Loc of int
    | Error
and Abstraction =
      Abstr of (string list * Exp)
;;




(* AMBIENTES - Um ambiente e representado por uma lista de pares
                                               (string, denotacao) *)

let rec envGet ((x,v)::xs) y =
    if y = x then v else envGet xs y
;;
let rec envUpdt d y newval =
  match d with
       [] -> [(y,newval)]
     | ((x,v)::xs) ->
             if y = x then ((x,newval)::xs) else (x,v)::envUpdt xs y newval
;;
let rec envUpdtList d =
  fun [] [] -> d
    | (x::xs) (v::vs) -> envUpdtList (envUpdt d x v) xs vs
;;
let envEmpty =
    []
;;




(* ESTADO - Um estado e representado por uma lista de pares
                                         (localizacao, resultado) *)
(* Uma localizacao e representada por um termo da forma (Loc int) *)

let rec storeGet ((x,v)::xs) (Loc l) =
    if (Loc l) = x then v else storeGet xs (Loc l)
;;
let rec storeUpdt s (Loc l) newval =
  match s with
       [] -> [((Loc l),newval)]
     | ((x,v)::xs) ->
            if (Loc l) = x then ((x,newval)::xs)
            else (x,v)::storeUpdt xs (Loc l) newval
;;
let storeAlloc s =
    Loc ((len s) + 1)
;;
let storeEmpty =
    []
;;



 
(* SEMANTICA: definida pela funcao "ev" com auxilio da funcao "eval". *)
(* Erros de execucao: a funcao "eval" gera excepcoes em todas as situacoes
  anomalas. As excepcoes sao convertidas pela funcao "ev" no resultado "Error"
*)

let rec eval (d,s,e) =
  match e with
      NumConst i ->
        (s, Num i)
    | BoolConst b ->
        (s, Bool b)
    | Var x ->
        (s, envGet d x)
    | Add (e1,e2) ->
        let (s1, Num n1) = eval (d,s,e1) in
            let (s2, Num n2) = eval (d,s1,e2) in
                (s2, Num (n1+n2))
    | Sub (e1,e2) ->
        let (s1, Num n1) = eval (d,s,e1) in
            let (s2, Num n2) = eval (d,s1,e2) in
                (s2, Num (n1-n2))
    | Mult (e1,e2) ->
        let (s1, Num n1) = eval (d,s,e1) in
            let (s2, Num n2) = eval (d,s1,e2) in
                (s2, Num (n1*n2))
    | Div (e1,e2) ->
        let (s1, Num n1) = eval (d,s,e1) in
            let (s2, Num n2) = eval (d,s1,e2) in
                (s2, Num (n1/n2))
    | Equal (e1,e2) ->
        let (s1, Num n1) = eval (d,s,e1) in
            let (s2, Num n2) = eval (d,s1,e2) in
                (s2, Bool (n1=n2))
    | Diff (e1,e2) ->
        let (s1, Num n1) = eval (d,s,e1) in
            let (s2, Num n2) = eval (d,s1,e2) in
                (s2, Bool (n1<>n2))
    | Seq (e1,e2) ->
        let (s1,v1) = eval (d,s,e1) in
            eval (d,s1,e2)
    | If (cond,thenpart,elsepart) ->
        let (s1,Bool vcond) = eval (d,s,cond) in
            if vcond then
                eval (d,s1,thenpart)
            else eval (d,s1,elsepart)
    | While (cond,body) ->
        let (s1,Bool vcond) = eval (d,s,cond) in
            if vcond then
                eval (d,s1,Seq (body, While (cond,body)))
            else (s1, Done)
    | Val x ->
        (s, storeGet s (envGet d x))
    | Assign (x,e) ->
        let (s1,v1) = eval (d,s,e) in
            (storeUpdt s1 (envGet d x) v1, Done)
    | Apply (f,es) ->
        let (s1,vs) = evalList (d,s,es) in
            let (Closure (d1,Abstr(ys,body))) = envGet d f in
                eval ((envUpdtList d1 ([f]@ys) ([envGet d f]@vs)), s1, body)
    | LetCon (x,e,e1) ->
        let (s1,v) = eval (d,s,e) in
            eval ((envUpdt d x v), s1, e1)
    | LetVar (x,e,e1) ->
        let (s1,v) = eval (d,s,e) in
            let l = storeAlloc s1 in
                eval ((envUpdt d x l), (storeUpdt s1 l v), e1)
    | LetFun (f,ys,e,e1) ->
        eval ((envUpdt d f (Closure (d,Abstr(ys,e)))),s,e1)

and evalList (d,s,es) =
    match es with
        [] -> (s,[])
      | (x::xs) ->
           let (s1,xv) = eval (d,s,x) in
              let (sr,xr) = evalList (d,s1,xs) in
                  (sr,xv::xr)
 ;;
 
let ev e =
    try
        let (s, res) = eval (envEmpty, storeEmpty, e) in
            res
    with _ -> Error
;;

(* TESTES
#ev (NumConst 4) ;;
- : Value = Num 4
#ev (Add (NumConst 1,NumConst 2));;
- : Value = Num 3
#ev (LetCon ("c",NumConst 1,Add ((Var "c"),NumConst 1))) ;;
- : Value = Num 2
#ev (LetFun ("succ",["y"],Add(Var "y",NumConst 1),
                            (Apply ("succ",[NumConst 6])))) ;;
- : Value = Num 7
#ev (LetFun ("fact",
            ["y"],
            If (Equal (Var "y",NumConst 0),
                NumConst 1,
                Mult (Var "y",Apply ("fact",[Sub (Var "y",NumConst 1)]))),
            Apply ("fact",[NumConst 10]))) ;;
- : Value = Num 3628800
#ev (LetVar ("acc", NumConst 1,
        LetVar ("i", NumConst 10,
            Seq(
                While (Diff (Val "i", NumConst 0),
                    Seq(Assign("acc",Mult(Val "acc",Val "i")),
                        Assign("i", Sub(Val "i", NumConst 1))
                    )),
                Val "acc"
            )
    ))) ;;
- : Value = Num 3628800
#ev (Add (NumConst 1,Val "x"));;
- : Value = Error
#ev (LetCon ("c",NumConst 1,Assign ("c",NumConst 2))) ;;
- : Value = Error
#ev (LetVar ("v",NumConst 1,Assign ("v",NumConst 2))) ;;
- : Value = Done

*)





(*
    MINIPASCAL TIPIFICADO
*)



(* TIPOS *)

type Type =
      IntType
    | BoolType
    | VoidType
    | RefType of Type
    | FunType of (Type list) * Type
;;




(* SINTAXE do MiniPascal Tipificado *)

type TExp =
      TNumConst of int
    | TBoolConst of bool
    | TVar of string
    | TAdd of TExp * TExp
    | TSub of TExp * TExp
    | TMult of TExp * TExp
    | TDiv of TExp * TExp
    | TEqual of TExp * TExp
    | TDiff of TExp * TExp
    | TSeq of TExp * TExp
    | TIf of TExp * TExp * TExp
    | TWhile of TExp * TExp
    | TVal of string
    | TAssign of string * TExp
    | TApply of string * (TExp list)
    | TLetCon of string * Type * TExp * TExp
    | TLetVar of string * Type * TExp * TExp
    | TLetFun of string * (string list) * (Type list) * Type * TExp * TExp
;;





(* CONTEXTOS - Um contexto e representado por uma lista de pares
                                                 (string, tipo) *)

let rec ctxGet ((x,t)::xs) y =
    if y = x then t else ctxGet xs y
;;
let rec ctxUpdt d y newtype =
  match d with
       [] -> [(y,newtype)]
     | ((x,v)::xs) ->
              if y = x then ((x,newtype)::xs)
              else (x,v)::ctxUpdt xs y newtype
;;
let rec ctxUpdtList d =
  fun [] [] -> d
    | (x::xs) (tx::txs) -> ctxUpdtList (ctxUpdt d x tx) xs txs
;;
let ctxEmpty =
    []
;;




(* VERIFICADOR de tipos para a linguagem MiniPascal tipificada *)

let same t1 t2 =
    if t1 = t2 then ()
    else raise (Failure "")
;;

let basic t =
    if t = IntType or t = BoolType or t = VoidType then ()
    else raise (Failure "")
;;

let rec check (g,e) =
  match e with
      TNumConst i ->
        IntType
    | TBoolConst b ->
        BoolType
    | TVar x ->
        ctxGet g x
    | TAdd (e1,e2) ->
        same (check (g,e1)) IntType;
        same (check (g,e2)) IntType;
        IntType
    | TSub (e1,e2) ->
        same (check (g,e1)) IntType;
        same (check (g,e2)) IntType;
        IntType
    | TMult (e1,e2) ->
        same (check (g,e1)) IntType;
        same (check (g,e2)) IntType;
        IntType
    | TDiv (e1,e2) ->
        same (check (g,e1)) IntType;
        same (check (g,e2)) IntType;
        IntType
    | TEqual (e1,e2) ->
        same (check (g,e1)) IntType;
        same (check (g,e2)) IntType;
        BoolType
    | TDiff (e1,e2) ->
        same (check (g,e1)) IntType;
        same (check (g,e2)) IntType;
        BoolType
    | TSeq (e1,e2) ->
        check (g,e1);
        check (g,e2)
    | TIf (cond,thenpart,elsepart) ->
        same (check (g,cond)) BoolType;
        let t = check (g,thenpart) in
            same (check (g,elsepart)) t;
            t
    | TWhile (cond,body) ->
        same (check (g,cond)) BoolType;
        same (check (g,body)) VoidType;
        VoidType
    | TVal x ->
         let (RefType t) = ctxGet g x in
            t
    | TAssign (x,e) ->
        let (RefType t) = ctxGet g x in
            same (check (g,e)) t;
            VoidType
    | TApply (f,es) ->
        let (FunType (tas,tr)) = ctxGet g f in
            same (checkList (g,es)) tas;
            tr
    | TLetCon (x,tx,e,e1) ->
        basic tx;
        same (check (g,e)) tx;
        check (ctxUpdt g x tx,e1)
    | TLetVar (x,tx,e,e1) ->
        basic tx;
        same (check (g,e)) tx;
        check (ctxUpdt g x (RefType tx),e1)
    | TLetFun (f,ys,tys,tr,e,e1) ->
        basic tr;
        same (check (ctxUpdtList g ([f]@ys) ([FunType(tys,tr)]@tys),e)) tr;
        check (ctxUpdt g f (FunType(tys,tr)), e1)

and checkList (g,es) =
    match es with
        [] -> []
      | (x::xs) ->
           (check (g,x))::checkList (g,xs)
;;

let chk e =
    try
        check (ctxEmpty, e) ; true
    with _ -> false
;;

(* TESTES
#chk (TNumConst 4) ;;
- : bool = true
#chk (TAdd (TNumConst 1,TNumConst 2));;
- : bool = true
#chk (TLetCon ("c",IntType,TNumConst 1,TAdd ((TVar "c"),TNumConst 1))) ;;
- : bool = true
#chk (TLetFun ("succ",["y"],[IntType],IntType,TAdd(TVar "y",TNumConst 1),
                        (TApply ("succ",[TNumConst 6])))) ;;
- : bool = true
#chk (TLetFun
       ("fact",
        ["y"],[IntType],
           IntType,
           TIf(TEqual (TVar "y",TNumConst 0),
               TNumConst 1,
               TMult (TVar "y",TApply ("fact",[TSub (TVar "y",TNumConst 1)]))),
        TApply ("fact",[TNumConst 10]))) ;;
- : bool = true
#chk (TLetVar ("acc", IntType, TNumConst 1,
        TLetVar ("i", IntType, TNumConst 10,
            TSeq(
                TWhile (TDiff (TVal "i", TNumConst 0),
                    TSeq(TAssign("acc",TMult(TVal "acc",TVal "i")),
                        TAssign("i", TSub(TVal "i", TNumConst 1))
                    )),
                TVal "acc"
            )
    ))) ;;
- : bool = true
#chk (TAdd (TNumConst 1,TVal "x"));;
- : bool = false
#chk (TLetCon ("c",IntType,TNumConst 1,TAssign ("c",TNumConst 2))) ;;
- : bool = false
#chk (TLetVar ("v",IntType,TNumConst 1,TAssign ("v",TNumConst 2))) ;;
- : bool = true
*)





(* UNTYPE - converte uma expressao da forma tipificada para a forma
                                                  nao-tipificada *)

let rec untype =
  function 
      TNumConst i -> NumConst i
    | TBoolConst b -> BoolConst b
    | TVar x -> Var x
    | TAdd (e1,e2) -> Add (untype e1, untype e2)
    | TSub (e1,e2) -> Sub (untype e1, untype e2)
    | TMult (e1,e2) -> Mult (untype e1, untype e2)
    | TDiv (e1,e2) -> Div (untype e1, untype e2)
    | TEqual (e1,e2) -> Equal (untype e1, untype e2) 
    | TDiff (e1,e2) -> Diff (untype e1, untype e2)
    | TSeq (e1,e2) -> Seq (untype e1, untype e2)
    | TIf (cond,thenpart,elsepart) ->
               If (untype cond, untype thenpart, untype elsepart)
    | TWhile (cond,body) -> While (untype cond, untype body)
    | TVal x -> Val x
    | TAssign (x,e) -> Assign (x, untype e)
    | TApply (f,es) -> Apply (f, untypeList es)
    | TLetCon (x,tx,e,e1) -> LetCon (x, untype e, untype e1)
    | TLetVar (x,tx,e,e1) -> LetVar (x, untype e, untype e1)
    | TLetFun (f,ys,tys,tr,e,e1) -> LetFun (f,ys, untype e, untype e1)

and untypeList =
  function [] -> []
         | (x::xs) ->
               (untype x)::untypeList xs
;;


(* TESTES
#untype (TNumConst 4) ;;
- : Exp = NumConst 4
#untype (TLetFun
       ("fact",
        ["y"],[IntType],
           IntType,
           TIf(TEqual (TVar "y",TNumConst 0),
               TNumConst 1,
               TMult (TVar "y",TApply ("fact",[TSub (TVar "y",TNumConst 1)]))),
        TApply ("fact",[TNumConst 10]))) ;;
- : Exp =
 LetFun
  ("fact", ["y"],
   If
    (Equal (Var "y", NumConst 0), NumConst 1,
     Mult (Var "y", Apply ("fact", [Sub (Var "y", NumConst 1)]))),
   Apply ("fact", [NumConst 10]))
*)




(* PROCESS - Avalia o argumento se este estiver bem tipificado. *)

let rec process e =
    if chk e then
        ev (untype e)
    else
        Error
;;