interp.hs

module Interp where
import Data.Maybe
import Data.List as List
import Ast

{-
data V =
    Litv Lit
  | Conv (Maybe (Id ConN)) [V]
  | Closure (Env VarN V) VarN Exp
  | Recclosure (Env VarN V) [(VarN, VarN, Exp)] VarN
  | Loc Int

instance Show V where
  show (Litv l) = show l
  show (Conv Nothing vs) = "(" ++ List.intercalate ", " (List.map show vs) ++ ")"
  show (Conv (Just cn) []) = show cn
  show (Conv (Just cn) vs) = show cn ++ "(" ++ List.intercalate ", " (List.map show vs) ++ ")"
  show (Closure _ _ _) = "<fn>"
  show (Recclosure _ _ _) = "<fn>"
  show (Loc i) = "<ref>"

data Error_result =
    Rtype_error
  | Rraise V

instance Show Error_result where
  show Rtype_error = "type error" 
  show (Rraise err) = show err

data Result a =
    Rval a
  | Rerr Error_result

type Store = [V]

empty_store :: Store
empty_store = []

store_lookup :: Int -> Store -> Maybe V
store_lookup l st =
  if l < List.length st then
    Just (st !! l)
  else
    Nothing

store_alloc :: V -> Store -> (Store, Int)
store_alloc v st =
  (st ++ [v], List.length st)

store_assign :: Int -> V -> Store -> Maybe Store
store_assign n v st =
  if n < List.length st then
    let l = List.drop n st in 
    Just (List.take n st ++ v : List.tail l)
  else
    Nothing

type EnvC = Env (Id ConN) (Integer, Tid_or_exn)

type EnvE = Env VarN V

type EnvM = Env ModN EnvE

newtype M_st_ex s a = M_st_ex { run_M_st_ex :: (s -> (s, Result a)) }

instance Monad (M_st_ex s) where
  return v = M_st_ex (\s -> (s, Rval v))
  (>>=) v f =
    M_st_ex (\s -> case (run_M_st_ex v) s of
                     (s,Rval v) -> (run_M_st_ex (f v)) s
                     (s,Rerr e) -> (s,Rerr e))

get :: M_st_ex s s
get = M_st_ex (\s -> (s, Rval s))

put :: s -> M_st_ex s ()
put s = M_st_ex (\s' -> (s, Rval ()))

raise :: Error_result -> M_st_ex a b
raise err = M_st_ex (\s -> (s, Rerr err))

handle :: M_st_ex s a -> (V -> M_st_ex s a) -> M_st_ex s a
handle v f =
  M_st_ex (\s -> case run_M_st_ex v s of
                   (s, Rerr (Rraise v)) -> run_M_st_ex (f v) s
                   (s,r) -> (s,r))
      

lit_same_type :: Lit -> Lit -> Bool
lit_same_type l1 l2 =
  case (l1,l2) of
      (IntLit _, IntLit _) -> True
      (Bool _, Bool _) -> True
      (Unit, Unit) -> True
      _ -> False

data Match_result =
    No_match
  | Match_type_error
  | Match EnvE

pmatch :: EnvC -> Store -> Pat -> V -> EnvE -> Match_result
pmatch envC s (Pvar x) v' env = Match (bind x v' env)
pmatch envC s (Plit l _) (Litv l') env =
  if l == l' then
    Match env
  else if lit_same_type l l' then
    No_match
  else
    Match_type_error
pmatch envC s (Pcon (Just n) ps _) (Conv (Just n') vs) env =
  case (Ast.lookup n envC, Ast.lookup n' envC) of
      (Just (l, t), Just (l', t')) ->
        if t == t' && (toInteger (List.length ps) == l) && (toInteger (List.length vs) == l') then
          if n == n' then
            pmatch_list envC s ps vs env
          else
            No_match
        else
          Match_type_error
      (_, _) -> Match_type_error
pmatch envC s (Pcon Nothing ps _) (Conv Nothing vs) env =
  if List.length ps == List.length vs then
    pmatch_list envC s ps vs env
  else
    Match_type_error
pmatch envC s (Pref p _) (Loc lnum) env =
  case store_lookup lnum s of
      Just v -> pmatch envC s p v env
      Nothing -> Match_type_error
pmatch envC _ _ _ env = Match_type_error
pmatch_list envC s [] [] env = Match env
pmatch_list envC s (p:ps) (v:vs) env =
  case pmatch envC s p v env of
      No_match -> No_match
      Match_type_error -> Match_type_error
      Match env' -> pmatch_list envC s ps vs env'
pmatch_list envC s _ _ env = Match_type_error

do_con_check :: EnvC -> Maybe (Id ConN) -> Integer -> M_st_ex a ()
do_con_check cenv n_opt l =
  case n_opt of
      Nothing -> return ()
      Just n ->
        case Ast.lookup n cenv of
            Nothing -> raise Rtype_error
            Just (l',ns) -> 
              if l == l' then
                return ()
	      else
                raise Rtype_error

lookup_var_id :: Id VarN -> EnvM -> EnvE -> Maybe V
lookup_var_id id menv envE =
  case id of
      Short x -> Ast.lookup x envE
      Long x y ->
        case Ast.lookup x menv of
            Nothing -> Nothing
            Just env -> Ast.lookup y env

do_uapp :: Store -> Uop -> V -> Maybe (Store, V)
do_uapp s uop v =
  case uop of
      Opderef ->
        case v of
            Loc n ->
              case store_lookup n s of
                  Just v -> Just (s,v)
                  Nothing -> Nothing
            _ -> Nothing
      Opref _ ->
        let (s',n) = store_alloc v s in
          Just (s', Loc n)

data Eq_result = 
    Eq_val Bool
  | Eq_closure
  | Eq_type_error

do_eq :: V -> V -> Eq_result
do_eq (Litv l1) (Litv l2) = Eq_val (l1 == l2)
do_eq (Loc l1) (Loc l2) = Eq_val (l1 == l2)
do_eq (Conv cn1 vs1) (Conv cn2 vs2) =
  if cn1 == cn2 && List.length vs1 == List.length vs2 then
    do_eq_list vs1 vs2
  else
    Eq_val False
do_eq (Closure _ _ _) (Closure _ _ _) = Eq_closure
do_eq (Closure _ _ _) (Recclosure _ _ _) = Eq_closure
do_eq (Recclosure _ _ _) (Closure _ _ _) = Eq_closure
do_eq (Recclosure _ _ _) (Recclosure _ _ _) = Eq_closure
do_eq _ _ = Eq_type_error
do_eq_list [] [] = Eq_val True
do_eq_list (v1:vs1) (v2:vs2) = 
  case do_eq v1 v2 of
      Eq_closure -> Eq_closure
      Eq_type_error -> Eq_type_error
      Eq_val r -> 
        if not r then
          Eq_val False
        else
          do_eq_list vs1 vs2
do_eq_list _ _ = Eq_val False

find_recfun :: VarN -> [(VarN, VarN, Exp)] -> Maybe (VarN, Exp)
find_recfun n funs =
  case funs of
      [] -> Nothing
      (f,x,e) : funs ->
        if f == n then
          Just (x,e)
        else
          find_recfun n funs

build_rec_env :: [(VarN, VarN, Exp)] -> EnvE -> EnvE -> EnvE
build_rec_env funs cl_env add_to_env =
  List.foldr
    (\(f,x,e) env' -> bind f (Recclosure cl_env funs f) env')
    add_to_env
    funs

do_app :: Store -> EnvE -> Op -> V -> V -> Maybe (Store, EnvE, Exp)
do_app s env' op v1 v2 =
  case (op, v1, v2) of
      (Opapp, Closure env n e, v) ->
        Just (s, bind n v env, e)
      (Opapp, Recclosure env funs n, v) ->
        case find_recfun n funs of
            Just (n,e) -> Just (s, bind n v (build_rec_env funs env env), e)
            Nothing -> Nothing
      (Opn op pos, Litv (IntLit n1), Litv (IntLit n2)) ->
        if (op == Divide || op == Modulo) && n2 == 0 then
          Just (s, env', Raise (Con (Just (Short (ConN "Div" dummy_pos))) [] dummy_pos))
        else
          Just (s, env',Lit (IntLit (opn_lookup op n1 n2)) pos)
      (Opb op pos, Litv (IntLit n1), Litv (IntLit n2)) ->
        Just (s, env', Lit (Bool (opb_lookup op n1 n2)) pos)
      (Equality pos, v1, v2) ->
        case do_eq v1 v2 of
            Eq_type_error -> Nothing
            Eq_closure -> Just (s, env', Raise (Con (Just (Short (ConN "Eq" dummy_pos))) [] dummy_pos))
            Eq_val b -> Just (s, env', Lit (Bool b) pos)
      (Opassign pos, (Loc lnum), v) ->
        case store_assign lnum v s of
          Just st -> Just (st, env', Lit Unit pos)
          Nothing -> Nothing
      _ -> Nothing

do_log :: Lop -> V -> Exp -> Maybe Exp
do_log l v e =
  case (l, v) of
      (And pos, Litv (Bool True)) -> Just e
      (Or pos, Litv (Bool False)) -> Just e
      (lop, Litv (Bool b)) -> Just (Lit (Bool b) (getPos lop))
      _ -> Nothing

do_if :: V -> Exp -> Exp -> Maybe Exp
do_if v e1 e2 =
  case v of
      Litv (Bool True) -> Just e1
      Litv (Bool False) -> Just e2
      _ -> Nothing

run_eval :: EnvM -> EnvC -> EnvE -> Exp -> M_st_ex Store V
run_eval menv cenv env (Lit l pos) = 
  return (Litv l)
run_eval menv cenv env (Raise e) =
  do v1 <- run_eval menv cenv env e;
     raise (Rraise v1)
run_eval menv cenv env (Handle e1 pes) =
  run_eval menv cenv env e1 `handle` (\v -> run_eval_match menv cenv env v pes v)
run_eval menv cenv env (Con cn es pos) =
  do do_con_check cenv cn (toInteger (List.length es));
     vs <- run_eval_list menv cenv env es;
     return (Conv cn vs)
run_eval menv cenv env (Var n) =
  case lookup_var_id n menv env of
     Nothing -> raise Rtype_error
     Just v -> return v
run_eval menv cenv env (Fun n e pos) =
   return (Closure env n e)
run_eval menv cenv env (Uapp uop e) =
  do v <- run_eval menv cenv env e;
     st <- get;
     case do_uapp st uop v of
          Nothing -> raise Rtype_error
          Just (st',v) -> 
            do put st';
               return v 
run_eval menv cenv env (App op e1 e2) =
   do v1 <- run_eval menv cenv env e1;
      v2 <- run_eval menv cenv env e2;
      st <- get;
      case do_app st env op v1 v2 of
           Nothing -> raise Rtype_error
           Just (st', env', e3) ->
             do put st';
                run_eval menv cenv env' e3
run_eval menv cenv env (Log lop e1 e2) =
   do v1 <- run_eval menv cenv env e1;
      case do_log lop v1 e2 of
           Nothing -> raise Rtype_error
           Just e' -> run_eval menv cenv env e'
run_eval menv cenv env (If e1 e2 e3) =
   do v1 <- run_eval menv cenv env e1;
      case do_if v1 e2 e3 of
           Nothing -> raise Rtype_error
           Just e' -> run_eval menv cenv env e'
run_eval menv cenv env (Mat e pes) =
   do v <- run_eval menv cenv env e;
      run_eval_match menv cenv env v pes (Conv (Just (Short (ConN "Bind" dummy_pos))) [])
run_eval menv cenv env (Let x e1 e2) =
   do v1 <- run_eval menv cenv env e1;
      run_eval menv cenv (bind x v1 env) e2
run_eval menv cenv env (Letrec funs e) =
   if isNothing (getDup (List.map (\(x,y,z) -> x) funs)) then
     run_eval menv cenv (build_rec_env funs env env) e
   else
     raise Rtype_error
run_eval_list menv cenv env [] =
   return []
run_eval_list menv cenv env (e:es) =
   do v <- run_eval menv cenv env e;
      vs <- run_eval_list menv cenv env es;
      return (v:vs)
run_eval_match menv cenv env v [] err_v =
   raise (Rraise err_v)
run_eval_match menv cenv env v ((p,e):pes) err_v =
   do st <- get;
      if isNothing (getDup (pat_bindings p [])) then
        case pmatch cenv st p v env of
             Match_type_error -> raise Rtype_error
             No_match -> run_eval_match menv cenv env v pes err_v
             Match env' -> run_eval menv cenv env' e
      else
        raise Rtype_error

build_tdefs :: Maybe ModN -> [([TvarN], TypeN, [(ConN, [T])])] -> EnvC
build_tdefs mn tds =
  listToEnv 
  (List.concat
    (List.map
      (\(tvs, tn, condefs) ->
         List.map
           (\(conN, ts) ->
              (mk_id mn conN, (toInteger (List.length ts), TypeId (mk_id mn tn))))
           condefs)
      tds))

run_eval_dec mn menv cenv st env (Dlet p e pos) =
  if isNothing (getDup (pat_bindings p [])) then
    case run_M_st_ex (run_eval menv cenv env e) st of
         (st', Rval v) ->
           (case pmatch cenv st' p v emp of
                Match env' -> (st', Rval (emp, env'))
                No_match -> (st', Rerr (Rraise (Conv (Just (Short (ConN "Bind" dummy_pos))) [])))
                Match_type_error -> (st', Rerr Rtype_error))
         (st', Rerr e) -> (st', Rerr e)
  else
    (st, Rerr Rtype_error)
run_eval_dec mn menv cenv st env (Dletrec funs) =
  if isNothing (getDup (List.map (\(x,y,z) -> x) funs)) then
    (st, Rval (emp, build_rec_env funs env emp))
  else
    (st, Rerr Rtype_error)
run_eval_dec mn menv cenv st env (Dtype tds) =
  (st, Rval (build_tdefs mn tds, emp))
{- 
  if check_dup_ctors mn cenv tds then
    (st, Rval (build_tdefs mn tds, emp))
  else
    (st, Rerr Rtype_error)
-}
run_eval_dec mn menv cenv st env (Dexn cn ts) =
  if Ast.lookup (mk_id mn cn) cenv == Nothing then
    (st, Rval (bind (mk_id mn cn) (toInteger (List.length ts), TypeExn) emp, emp))
  else
    (st, Rerr Rtype_error)


combine_dec_result :: Ord a => Env a b -> Result (Env a b) -> Result (Env a b)
combine_dec_result env r =
  case r of
     Rerr e -> Rerr e
     Rval env' -> Rval (merge env' env)

run_eval_decs mn menv cenv st env [] = (st, emp, Rval emp)
run_eval_decs mn menv cenv st env (d:ds) =
  case run_eval_dec mn menv cenv st env d of
      (st', Rval (cenv',env')) ->
         (case run_eval_decs mn menv (merge cenv' cenv) st' (merge env' env) ds of
               (st'', cenv'', r) ->
                 (st'', merge cenv'' cenv', combine_dec_result env' r))
      (st',Rerr err) -> (st',emp,Rerr err)

run_eval_top :: EnvM -> EnvC -> Store -> EnvE -> Top -> (Store, EnvC, Result (EnvM, EnvE))
run_eval_top menv cenv st env (Tdec d) = 
  case run_eval_dec Nothing menv cenv st env d of
       (st', Rval (cenv', env')) -> (st', cenv', Rval (emp, env'))
       (st', Rerr err) -> (st', emp, Rerr err)
run_eval_top menv cenv st env (Tmod mn specs ds) =
  if not (envElem mn menv) then
    case run_eval_decs (Just mn) menv cenv st env ds of
         (st', cenv', Rval env') -> (st', cenv', (Rval (listToEnv [(mn, env')], emp)))
         (st', cenv', Rerr err) -> (st', cenv', Rerr err)
  else
    (st, emp, Rerr Rtype_error)

varx = Var (Short (VarN "x" dummy_pos))
vary = Var (Short (VarN "y" dummy_pos))

init_env :: EnvE
init_env = listToEnv (List.map (\(x,y) -> (VarN x dummy_pos, Closure emp (VarN "x" dummy_pos) y))
  [("+", (Fun (VarN "y" dummy_pos) (App (Opn Plus dummy_pos) varx vary) dummy_pos)),
   ("-", (Fun (VarN "y" dummy_pos) (App (Opn Minus dummy_pos) varx vary) dummy_pos)),
   ("*", (Fun (VarN "y" dummy_pos) (App (Opn Times dummy_pos) varx vary) dummy_pos)),
   ("div", (Fun (VarN "y" dummy_pos) (App (Opn Divide dummy_pos) varx vary) dummy_pos)),
   ("mod", (Fun (VarN "y" dummy_pos) (App (Opn Modulo dummy_pos) varx vary) dummy_pos)),
   ("<", (Fun (VarN "y" dummy_pos) (App (Opb Lt dummy_pos) varx vary) dummy_pos)),
   (">", (Fun (VarN "y" dummy_pos) (App (Opb Gt dummy_pos) varx vary) dummy_pos)),
   ("<=", (Fun (VarN "y" dummy_pos) (App (Opb Leq dummy_pos) varx vary) dummy_pos)),
   (">=", (Fun (VarN "y" dummy_pos) (App (Opb Geq dummy_pos) varx vary) dummy_pos)),
   ("=", (Fun (VarN "y" dummy_pos) (App (Equality dummy_pos) varx vary) dummy_pos)),
   (":=", (Fun (VarN "y" dummy_pos) (App (Opassign dummy_pos) varx vary)) dummy_pos),
   ("~", (App (Opn Minus dummy_pos) (Lit (IntLit 0) dummy_pos) varx)),
   ("!", (Uapp Opderef varx)),
   ("ref", (Uapp (Opref dummy_pos) varx))])

init_envC =
  listToEnv ((Short (ConN "nil" dummy_pos), (0, TypeId (Short (TypeN "list" dummy_pos)))) :
             (Short (ConN "::" dummy_pos), (2, TypeId (Short (TypeN "list" dummy_pos)))) :
             List.map (\cn -> (Short (ConN cn dummy_pos), (0, TypeExn))) ["Bind", "Div", "Eq"])

-}