-- Core.hs: The core λ calculus of simpl.

-- Copyright 2014 Jack Pugmire
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
--     http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-- See the License for the specific language governing permissions and
-- limitations under the License.


module Simpl.Core where

import Data.List (find)

type Name = String
type Result a = Either String a

data Global = Global { gName  :: Name
                     , gValue :: Value
                     , gType  :: Type
                     }
type Env = [Global]

data Term = EAnn Term Type
          | EApp Term Term
          | EGlobal Name
          | ELam Term
          | EVar Int
          | EUnit Bool

data Type = TUnit
          | TFun Type Type
          | TVar Name
          deriving (Eq)

instance Show Type where
  show TUnit       = "Unit"
  show (TFun t t') = case t of
    (TFun _ _) -> "(" ++ show t ++ ") -> " ++ show t'
    _          -> show t ++ " -> " ++ show t'
  show (TVar n)    = n


data Value = VUnit Bool
           | VLam (Value -> Result Value)

instance Show Value where
  show (VUnit True)  = "T"
  show (VUnit False) = "F"
  show (VLam  _)     = "λ"


-- Look up the value of a global
lookupGlobal :: String -> Env -> Result Value
lookupGlobal n = f . find (\(Global n' _ _) -> n == n')
  where f = maybe (Left ("No such global " ++ show n)) (Right . gValue)

-- Look up the type of a global
lookupGlobalT :: Name -> Env -> Result Type
lookupGlobalT n = f . find (\(Global n' _ _) -> n == n')
  where f = maybe (Left ("No such global " ++ show n)) (Right . gType)
