module HaskellCoreLite1_2 where 

{-
Differences from HCL1.1:

This version has explicit pattern-matching failure in the type of "match."
I.e., match :: P -> M Value -> M (Maybe EnvFrag)

So, now M now longer has two error types "Fatal" and "Trappable" - they're
all fatal now. Also, fatbar has gone away.

BTW, most/all of the changes are marked with comments starting with "N.b."

-}

type Name = String

data Op = Plus | Mult | IntEq | IntLess

data LS = Lazy | Strict deriving Eq

data E
  = Var Name
  | App E E
  | Abs P E
  | Let [D] E
  | Case E [Match]
  | PairExp E E
  | TupleExp [E]
  | Const Integer
---  | ConApp Name [E] 
  | ConApp Name [(E,LS)]
  | NewApp Name E
  | Boom
  | Undefined
--- Above is the "core", below various extras
  | Bin Op E E
  | Cond E E E
  | Tconst 
  | Fconst

data Match = Guarded P [(E,E)] [D]
           | Normal P E [D]

--- N.b., these are nested patterns.
data P = Pconst Integer
       | Pvar Name
       | Ppair P P
       | Ptuple [P]
       | Pcondata Name [P]  
       | Pnewdata Name P
       | Ptilde P

type D = (P,E)

showD :: D -> String
showD (p,le) =  " " ++ showP p ++ "=" ++ (showE le) ++ " " 

showDecls dcls = foldr (++) "" (map (\(p,e)-> showD (p,e)) dcls)


showOp :: Op -> String
showOp Plus = "+"
showOp Mult = "*"
showOp IntEq = "=="
showOp IntLess = "<"

showP (Pconst i) = show i
showP (Pvar n) = n
showP (Pcondata n ns) = 
                "(" ++ n ++ " " ++ 
                (foldr (\ s t -> if t/="" then (showP s) ++ "," ++ t
                                     else (showP s)) 
                        "" ns)
                ++ ")"
showP (Pnewdata n x) = "(" ++ n ++ " " ++ (showP x) ++ ")"              
showP (Ptilde p) = "~" ++ (showP p)

showM :: Match -> String
showM (Normal p e ds) = showP p ++ "->" 
                                ++ showE e 
                                ++ " where " ++ showDecls ds
showM (Guarded p glist ds) = 
    (foldr (++) "" 
       (map (\(g,b) -> showP p ++ " | " ++ showE g ++ "->" ++ showE b) glist))
                    ++ " where " ++ showDecls ds

showE :: E -> String
showE (Const i) = show i
showE Tconst = "True"
showE Fconst = "False"
showE (Var nm) = nm
showE (Abs p d) = "(\\" ++ (showP p) ++ " -> " ++ showE d ++ ")"
showE (App d d') = "(" ++ showE d ++ " " ++ showE d' ++ ")"
showE (Let dcls d) = "let " ++ 
                          foldr (++) "" (map (\(p,e)-> showD (p,e)) dcls)
                            ++ 
                        " in " ++ showE d
showE (ConApp n l) =  "(" ++ n ++ " " ++  
                (foldr (\ (s,ls) t -> 
			    let sa = if (ls == Strict) then "!" else "" 
			    in
				 if t/="" then sa ++ (showE s) ++ "," ++ t
                                     else sa ++ (showE s)) 
                        "" l)
                      ++ ")"
showE (NewApp n x) = "(" ++ n ++ " " ++  (showE x) ++ ")"                     

showE (PairExp n l) = "<"++showE n++","++ showE l ++ ">"
showE (Bin op d d') = "(" ++ showE d ++ " " ++ showOp op ++ " " ++ 
                               showE d' ++ ")"
showE Tconst = "true"
showE Fconst = "false"
showE (Case e ms) =
      "(case " ++ showE e ++ " of " ++ 
           (foldr (++) "" (map (\m -> "[" ++ (showM m) ++ "]") ms)) ++ ")"


instance Show E where
  show = showE

----------------------------------------------------------------------
-- Values
----------------------------------------------------------------------

type EnvFrag = [(Name,M Value)]

data Value
  = 
--- scalars
    Z Integer
  | BV Bool
--- CBN functions
  | Fun (M Value -> M Value)
--- Generic structured data
  | Tagged Name [M Value]
--- values for all tuples:
  | TupleVal [M Value]

data Fix a = Fix (Fix a -> a)
fix = \ f -> (\ (Fix x) -> 
                   (f (\ a -> x (Fix x) a)))
                      (Fix (\ (Fix x) -> (f (\ a -> x (Fix x) a))))

showValue :: Value -> String
showValue (Z i) = show i
showValue (BV i) = show i
showValue (Fun _) = "(function)"
showValue (Tagged n arglist) = "(" ++ n ++ " " ++ (present (map splat arglist)) ++ ")"

present (x:(y:rest)) = (show x)++" "++(present (y:rest))
present (x:[]) = show x
present [] = ""

instance Show Value where
  show = showValue

splat phi = (deM phi (\msg -> error "hey - you're applying the empty env!"))
run le = (deM (eval le) (\msg -> error "hey - you're applying the empty env!"))

----------------------------------------------------------------------
-- Errors
----------------------------------------------------------------------

data Error a = Ok a | Err String

----------------------------------------------------------------------
-- Error monad
----------------------------------------------------------------------


errUnit :: a -> Error a
errUnit = Ok


errBind :: Error a -> (a -> Error b) -> Error b
errBind x f = case x of
                     (Ok v) -> f v
                     (Err msg) -> (Err msg)

instance Monad Error where
  return = errUnit
  (>>=) = errBind

showEC x =
       case x of
            (Ok v) -> show v
            (Err msg) -> show msg

showError :: Show a => Error a -> String
showError x =
       case x of
            (Ok v) -> show v
            (Err msg) -> show msg

instance Show a => Show (Error a) where
    show = showError

raise0 = Err

----------------------------------------------------------------------
-- Environments
----------------------------------------------------------------------

type Env = Name -> M Value

----------------------------------------------------------------------
-- M = Environment+Error 
----------------------------------------------------------------------

newtype M a = M (Env -> (Error a))

mUnit :: a -> M a
mUnit a = M (\rho -> return a)


mBind :: M a -> (a -> M b) -> M b
mBind x f =
        M (\rho -> 
                 do { v <- (deM x) rho ; deM (f v) rho })

instance Monad M where
  return = mUnit
  (>>=) = mBind

deM (M x) = x

lift :: Error a -> M a
lift ec = M (\ _ ->  ec)

----------------------------------------------------------------------
-- Non-standard Morphisms
----------------------------------------------------------------------

raise :: String -> M a
raise = \msg -> lift (raise0 msg)

rdEnv :: M Env
rdEnv = M (\rho -> return rho)

tweek f x y = \ z -> if x == z then y else f z

xEnv :: Env -> Name -> M Value -> Env
xEnv rho n phi = tweek rho n phi

inEnv :: Env -> M a -> M a
inEnv rho (M x) = M (\ _ -> x rho)

----------------------------------------------------------------------
-- 
----------------------------------------------------------------------

--- these functions/PairVal should be replaced with select/Tagged:

proj :: Int -> M Value -> M Value
proj n phi = do { (TupleVal mvals) <- phi ; mvals !! (n-1)  }

--- N.b., checkTag now strips off the tag "t"
checkTag :: Name -> M Value -> M Value
checkTag tag arg =
         do { (Tagged t mvals) <- arg
            ; if t==tag then return (TupleVal mvals)
              else raise $ "Tag " ++ t ++ "!="++tag
              }


concatM ::Monad m => [m [a]] -> m [a]
concatM x = sequence x >>= (return . concat)

---
--- N.b., the meaning of match has changed so that
--- pattern failure is explicit in the range here:
---
match :: P -> M Value -> M (Maybe EnvFrag)
match (Pvar x) arg = return $ Just [(x,arg)]
match (Ptilde p) arg = return $ Just (lazymatch p arg)
match (Pconst i) arg = do { (Z v) <- arg
                          ; if v==i then 
                                    return $ Just []
                            else return Nothing
                            }
match (Ppair p1 p2) arg = 
      do { (TupleVal mvals) <- arg
         ; vbl1 <- match p1 (head mvals)
         ; vbl2 <- match p2 (head $ tail mvals)
         ; case (vbl1,vbl2) of
             (Just vl1, Just vl2) ->return $ Just (vl1 ++ vl2) 
             _ -> return Nothing
         }
match (Ptuple ps) arg = 
   do { (TupleVal mvals) <- arg
      ; sequence (map (\(p,phi) -> match p phi) (zip ps mvals)) 
                 >>= (return . concatM)
             }
match (Pcondata tag ps) arg = 
   do { (Tagged t mvals) <- arg
      ; if tag==t 
        then
           sequence (map (\(p,phi) -> match p phi) (zip ps mvals)) 
                >>= (return . concatM)
        else return Nothing
             }
match (Pnewdata n p) arg = match p arg
  


lazymatch :: P -> M Value -> EnvFrag
lazymatch (Pconst k) mv = []
lazymatch (Pvar x) mv = [(x,mv)]
lazymatch (Ptilde p) mv = lazymatch p mv
lazymatch (Ppair p1 p2) mv = 
          lazymatch p1 (proj 1 mv) ++ lazymatch p2 (proj 2 mv)
lazymatch (Pcondata n ps) mv = 
   concat (map (\(i,p) -> lazymatch p (proj i (checkTag n mv)))
                    (zip [1..(length ps)] ps))
lazymatch (Pnewdata n p) mv = lazymatch p mv                    
lazymatch (Ptuple ps) mvals = 
   concat (map (\(i,p) -> lazymatch p (proj i mvals))
                    (zip [1..(length ps)] ps))


app :: M Value -> M Value -> M Value
app x y = do { rho <- rdEnv ; (Fun f1) <- x ; f1 (inEnv rho y) }

addBindings :: Env -> EnvFrag -> Env
addBindings rho [] = rho
addBindings rho ((n,mv):bindings) = addBindings (xEnv rho n mv) bindings

---
--- N.b. ,I use this in the definition of (eval (Let ...)) and in the 
--- meaning of matches as well 
---
letbind :: [(P,E)] -> M a -> M a
letbind pelist phi =
     do { rho <- rdEnv
        ; let rho' = 
               fix (\ r -> 
                 addBindings rho $
                   foldr (++) []  
                         (map (\(p,e)->lazymatch p (inEnv r (eval e))) pelist))
          in
               inEnv rho' phi
               }


eval :: E -> M Value
eval (Const i) = return (Z i)
eval Tconst = return $ BV True
eval Fconst = return $ BV False
eval Boom = eval Boom
eval Undefined = raise "Undefined"
eval (Var n) = do { rho <- rdEnv ; rho n }
---
--- N.b., the abstraction must check if it gets an EnvFrag back.
---
eval (Abs p l) = 
     do { rho <- rdEnv 
        ; return (Fun $ \ arg ->
                   do { vbl <- match p arg 
                      ; case vbl of
                           (Just vl) -> 
                              inEnv (addBindings rho vl) (eval l) 
                           Nothing -> raise "Match Error in Abs"
                           } ) }
eval (App l1 l2) =
     do { rho <- rdEnv
        ; (Fun f1) <- eval l1
        ; f1 (inEnv rho $ eval l2) }
eval (PairExp l1 l2) = 
     do { rho <- rdEnv
        ; return (TupleVal [inEnv rho (eval l1), inEnv rho (eval l2)])
          }
eval (TupleExp es) = 
  do { rho <- rdEnv ; return (TupleVal $ map (\e -> inEnv rho $ eval e) es) }
{-
 This is a little difficult to understand as is, although what is going on is
 quite simple. Here's how I would write it in standard mathematical notation:

[[ c e1 !e2 ]] =
     rdEnv >>= \rho ->
     [[ e2 ]] >>= \ v2 ->
        return (c* (inEnv rho [[e1]]) (return v2))

That is, e2 (annotated as strict) is evaluated early and a trivial computation
"(return v2)" is kept for it. 
-}
eval (ConApp n es) = 
  do { rho <- rdEnv
     ; let evald_es = map (\(e,ls) -> 
			   case ls of
			     Lazy -> return(inEnv rho $ eval e)
			     Strict -> eval e >>= \v -> return(return v)) es
       in
          f evald_es >>= \result -> return (Tagged n $ result)
       }
   where 
	 f [] = return []
	 f (phi:phis) = phi >>= \v-> (f phis) >>= \vs -> return (v:vs)
eval (NewApp n x) = eval x

{-
         (foldr (\ phi phis -> phi >>= \v-> (f phis) >>= \vs -> return (v:vs)) 
                (return [])
foldr (\ phi phis -> phi >>= \v-> (f phis) >>= \vs -> return (v:vs)) 
      (return [])
      es
-}

---
--- N.b., this is the new definition of case.
---
eval (Case e ms) = evalMatchList (map evalM ms) (eval e)
eval (Let pelist le) = letbind pelist $ eval le
eval (Bin op l1 l2) =
     case op of 
      Plus -> 
        do { (Z i1) <- eval l1 
           ; (Z i2) <- eval l2 
           ; return (Z (i1+i2)) }
      Mult -> 
        do { (Z i1) <- eval l1 
           ; (Z i2) <- eval l2 
           ; return (Z (i1*i2)) }
      IntEq ->
        do { (Z i1) <- eval l1 
           ; (Z i2) <- eval l2 
           ; return (BV (i1==i2)) }
      IntLess ->
        do { (Z i1) <- eval l1 
           ; (Z i2) <- eval l2 
           ; return (BV (i1<i2)) }

eval (Cond l1 l2 l3) =
     do { (BV b) <- eval l1
        ; if b then (eval l2) else (eval l3) }

-------------------------------------------------------------
-------------- Matches and their meaning  -------------------
-------------------------------------------------------------

justify :: M Value -> M (Maybe Value)
justify x = x >>= (return . Just)

evalM :: Match -> M Value -> M(Maybe Value)
evalM (Normal p e ds) arg = 
   do { mfrag <- match p arg
      ; case mfrag of
         Nothing -> return Nothing
         Just frag -> do { env <- rdEnv
                         ; inEnv (addBindings env frag) 
                                    $ letbind ds (justify (eval e))
                         }
      }
evalM (Guarded p guards ds) arg =
   do { env <- rdEnv
      ; mfrag <- match p arg
      ; case mfrag of
         Nothing   -> return Nothing
         Just frag -> inEnv (addBindings env frag) 
                               $ letbind ds (evalGuardedList guards)
      }
    where
        evalGuardedList :: [(E,E)] -> M (Maybe Value)
        evalGuardedList [] = return Nothing
        evalGuardedList ((g,b):gs) =
                           do { v <- eval g
                              ; case v of
                                   (BV True)  -> (eval b) >>= (return . Just)
                                   (BV False) -> evalGuardedList gs
                              }

evalMatchList :: [M Value -> M(Maybe Value)] -> (M Value -> M Value)
evalMatchList [] arg = raise "Match Failure"
evalMatchList (f:fs) arg = 
  do { mv <- f arg
     ; case mv of
         Nothing -> evalMatchList fs arg
         Just v -> return v
     }

--------------------------------------------------------------
--------------------------------------------------------------
--------------------------------------------------------------